Library zoo.common.list
Require Ltac2.Ltac2.
Require stdpp.list.
Require stdpp.sorting.
Require Import zoo.prelude.
Require Import zoo.common.math.
Require Import zoo.options.
Export stdpp.list.
Export stdpp.sorting.
Create HintDb simp_length.
#[global] Hint Rewrite
@length_reverse
@length_app
@length_insert
@length_take
@length_drop
@length_fmap
@length_replicate
@length_seq
@length_seqZ
@length_zip_with
: simp_length.
Tactic Notation "simp_length" :=
autorewrite with simp_length; try done.
Tactic Notation "simp_length" "/=" :=
repeat (progress csimpl in × || simp_length).
Tactic Notation "simp_length" "in" ne_hyp_list(Hs) :=
autorewrite with simp_length in Hs; try done.
Tactic Notation "simp_length" "/=" "in" ne_hyp_list(Hs) :=
repeat (progress csimpl in × || simp_length in Hs).
Tactic Notation "simp_length" "in" "*" :=
autorewrite with simp_length in *; try done.
Tactic Notation "simp_length" "/=" "in" "*" :=
repeat (progress csimpl in × || simp_length in × ).
Module lengths.
Import Ltac2.
Ltac2 main () :=
Control.enter (fun () ⇒
List.iter (fun (hyp, _, ty) ⇒
lazy_match! ty with
| _ = _ ⇒
try (apply (f_equal length) in $hyp as ?)
| _ ≡ₚ _ ⇒
apply Permutation_length in $hyp as ?
| _ ⊆+ _ ⇒
apply submseteq_length in $hyp as ?
| _ `prefix_of` _ ⇒
apply prefix_length in $hyp as ?
| _ ⇒
()
end
) (Control.hyps ())
).
End lengths.
Tactic Notation "lengths" :=
ltac2:(lengths.main ());
simp_length in ×.
Tactic Notation "lengths" "/=" :=
ltac2:(lengths.main ());
simp_length/= in ×.
Section basic.
Context {A : Type}.
Implicit Type x y z : A.
Implicit Type l : list A.
Lemma listｰeq l1 l2 :
l1 = l2 ↔
length l1 = length l2 ∧
∀ i x1 x2,
l1 !! i = Some x1 →
l2 !! i = Some x2 →
x1 = x2.
Lemma appｰnotｰnil l1 l2 :
l1 ≠ [] ∨ l2 ≠ [] →
l1 ++ l2 ≠ [].
Lemma appｰnotｰnilｰl l1 l2 :
l1 ≠ [] →
l1 ++ l2 ≠ [].
Lemma appｰnotｰnilｰr l1 l2 :
l2 ≠ [] →
l1 ++ l2 ≠ [].
Lemma lookupｰappｰrｰSome l1 l2 i y :
length l1 ≤ i →
l2 !! (i - length l1) = Some y →
(l1 ++ l2) !! i = Some y.
Lemma lookupｰconsｰrｰSome x l i y :
0 < i →
l !! (i - 1) = Some y →
(x :: l) !! i = Some y.
Lemma elem_ofｰappｰl l1 l2 x :
x ∈ l1 →
x ∈ l1 ++ l2.
Lemma elem_ofｰappｰr l1 l2 x :
x ∈ l2 →
x ∈ l1 ++ l2.
Lemma reverseｰnilｰiff l :
reverse l = [] ↔
l = [].
Lemma foldrｰinsertｰstrong `(f : A → B → B) comp l i x y acc :
l !! i = Some x →
( ∀ x acc,
f x (f y acc) = f y (f x acc)
) →
( ∀ acc,
f (comp y x) acc = f y (f x acc)
) →
foldr f acc (<[i := comp y x]> l) = f y (foldr f acc l).
Lemma foldrｰinsertｰstrong' op `{!Assoc (=) op} `{!Comm (=) op} comp l i x y acc :
l !! i = Some x →
( ∀ acc,
op (comp y x) acc = op y (op x acc)
) →
foldr op acc (<[i := comp y x]> l) = op y (foldr op acc l).
Lemma foldrｰinsert op `{!Assoc (=) op} `{!Comm (=) op} l i x y acc :
l !! i = Some x →
foldr op acc (<[i := op y x]> l) = op y (foldr op acc l).
Lemma lengthｰlookupｰlast l i :
is_Some (l !! i) →
l !! ˖i = None →
length l = ˖i.
Lemma tailｰapp l1 l2 :
l1 ≠ [] →
tail (l1 ++ l2) = tail l1 ++ l2.
Lemma lengthｰtail l :
length (tail l) ≤ length l.
Lemma headｰapp l1 l2 :
0 < length l1 →
head (l1 ++ l2) = head l1.
Lemma headｰappｰcons l1 x l2 :
head (l1 ++ x :: l2) = head (l1 ++ [x]).
Lemma headｰdropｰSome l i x :
l !! i = Some x →
head (drop i l) = Some x.
Lemma headｰdrop l i :
head (drop i l) = l !! i.
Lemma hdｰcorrect default l x :
0 < length l →
hd default l = x →
head l = Some x.
Lemma hdｰapp default l1 l2 :
0 < length l1 →
hd default (l1 ++ l2) = hd default l1.
Lemma hdｰappｰcons default l1 x l2 :
hd default (l1 ++ x :: l2) = hd default (l1 ++ [x]).
Lemma hdｰdropｰSome default l i x :
l !! i = Some x →
hd default (drop i l) = x.
Lemma lastｰcons' x l :
last (x :: l) = Some $ default x (last l).
Lemma lastｰtake l i x :
l !! i = Some x →
last (take ˖i l) = Some x.
Lemma lastｰtake' l i :
is_Some (l !! i) →
last (take i l) = nat۰elim None (l !!.) i.
Lemma lastｰremovelast l x :
last l = Some x →
l = removelast l ++ [x].
Lemma dropｰlookupｰNone l i :
l !! i = None →
drop i l = [].
Lemma dropｰconsｰinv i l x l' :
drop i l = x :: l' →
l !! i = Some x ∧
l' = drop ˖i l.
Lemma insertｰconsｰl i x y l :
i = 0 →
<[i := x]> (y :: l) = x :: l.
Lemma insertｰconsｰr i x y l :
0 < i →
<[i := x]> (y :: l) = y :: <[i - 1 := x]> l.
Lemma insertｰappｰrｰ0 i x l1 l2 :
i = length l1 →
<[i := x]> (l1 ++ l2) = l1 ++ <[0 := x]> l2.
Lemma listｰdeleteｰinsertｰeq l i x :
i < length l →
delete i (<[i := x]> l) = delete i l.
End basic.
Section suffix.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
Lemma suffixｰtail l1 l2 :
l1 `suffix_of` l2 →
tail l1 `suffix_of` l2.
Lemma suffixｰfmap `(f : A → B) `{!Inj (=) (=) f} l1 l2 :
suffix (f <$> l1) (f <$> l2) →
suffix l1 l2.
End suffix.
Section seqZ.
Lemma seqZｰprefix {i n1} n2 :
(0 ≤ n2 ≤ n1)%Z →
seqZ i n2 `prefix_of` seqZ i n1.
Lemma seqZｰsuffix {i1 n1} i2 n2 :
(i1 ≤ i2 ≤ i1 + n1)%Z →
(i2 - i1 = n1 - n2)%Z →
seqZ i2 n2 `suffix_of` seqZ i1 n1.
End seqZ.
Section zip.
Context {A1 A2 : Type}.
Lemma prod_mapｰzip {B1 B2} (f1 : A1 → B1) (f2 : A2 → B2) l1 l2 :
prod_map f1 f2 <$> (zip l1 l2) = zip (f1 <$> l1) (f2 <$> l2).
End zip.
Section zip3_with.
Context {A1 A2 A3 B : Type}.
Implicit Type f : A1 → A2 → A3 → B.
Fixpoint zip3_with f l1 l2 l3 :=
match l1, l2, l3 with
| x1 :: l1, x2 :: l2, x3 :: l3 ⇒
f x1 x2 x3 :: zip3_with f l1 l2 l3
| _, _, _ ⇒
[]
end.
#[global] Arguments zip3_with _ !_ !_ !_ / : assert.
Lemma lengthｰzip3_with f l1 l2 l3 :
length l1 = length l2 →
length l1 = length l3 →
length (zip3_with f l1 l2 l3) = length l1.
Lemma lookupｰzip3_withｰSome f l1 l2 l3 i x :
zip3_with f l1 l2 l3 !! i = Some x ↔
∃ x1 x2 x3,
l1 !! i = Some x1 ∧
l2 !! i = Some x2 ∧
l3 !! i = Some x3 ∧
x = f x1 x2 x3.
End zip3_with.
#[global] Hint Rewrite
@lengthｰzip3_with
: simp_length.
Section zip3.
Context {A1 A2 A3 : Type}.
Definition zip3 :=
zip3_with (B := A1 × A2 × A3) $ λ x1 x2 x3,
(x1, x2, x3).
Lemma zip3ｰcons x1 l1 x2 l2 x3 l3 :
zip3 (x1 :: l1) (x2 :: l2) (x3 :: l3) = (x1, x2, x3) :: zip3 l1 l2 l3.
Lemma lengthｰzip3 l1 l2 l3 :
length l1 = length l2 →
length l1 = length l3 →
length (zip3 l1 l2 l3) = length l1.
Lemma zipｰzip l1 l2 l3 :
zip (zip l1 l2) l3 = zip3 l1 l2 l3.
End zip3.
#[global] Hint Rewrite
@lengthｰzip3
: simp_length.
Section foldri.
Implicit Type i : nat.
Fixpoint foldri' `(f : nat → A → B → B) acc l i :=
match l with
| [] ⇒
acc
| x :: l ⇒
f i x (foldri' f acc l ˖i)
end.
#[global] Arguments foldri' _ _ _ _ !_ _ / : assert.
Definition foldri `(f : nat → A → B → B) acc l :=
foldri' f acc l 0.
#[local] Lemma foldri'ｰapp `(f : nat → A → B → B) acc l1 l2 i :
foldri' f acc (l1 ++ l2) i =
foldri' f (foldri' f acc l2 (i + (length l1))) l1 i.
Lemma foldriｰapp `(f : nat → A → B → B) acc l1 l2 :
foldri f acc (l1 ++ l2) =
foldri f (foldri' f acc l2 (length l1)) l1.
#[local] Lemma foldri'ｰfmap `(f : nat → A → B → B) `(g : C → A) acc l i :
foldri' f acc (g <$> l) i = foldri' (λ i x, f i (g x)) acc l i.
Lemma foldriｰfmap `(f : nat → A → B → B) `(g : C → A) acc l :
foldri f acc (g <$> l) = foldri (λ i x, f i (g x)) acc l.
#[local] Lemma foldri'ｰcomm `(f : nat → A → B → B) `(g : B → C) h acc l i :
( ∀ i x acc,
h i x (g acc) = g (f i x acc)
) →
foldri' h (g acc) l i = g (foldri' f acc l i).
Lemma foldriｰcomm `(f : nat → A → B → B) `(g : B → C) h acc l :
( ∀ i x acc,
h i x (g acc) = g (f i x acc)
) →
foldri h (g acc) l = g (foldri f acc l).
End foldri.
Section foldr2.
Context {A1 A2 B : Type}.
Fixpoint foldr2 (f : A1 → A2 → B → B) acc l1 l2 :=
match l1 with
| [] ⇒
acc
| x1 :: l1 ⇒
match l2 with
| [] ⇒
acc
| x2 :: l2 ⇒
f x1 x2 (foldr2 f acc l1 l2)
end
end.
#[global] Arguments foldr2 _ _ !_ !_ / : assert.
Lemma foldr2ｰapp f acc l11 l12 l21 l22 :
length l11 = length l21 →
foldr2 f acc (l11 ++ l12) (l21 ++ l22) =
foldr2 f (foldr2 f acc l12 l22) l11 l21.
End foldr2.
Section Forall.
Context `(P : A → Prop).
Lemma Forallｰelem_of l x :
Forall P l →
x ∈ l →
P x.
End Forall.
Section Forall'.
Context `(P : A → Prop).
Fixpoint Forall' l :=
match l with
| [] ⇒
True
| x :: l ⇒
P x ∧ Forall' l
end.
#[global] Arguments Forall' !_ / : assert.
Lemma Forall'ｰForall l :
Forall' l ↔ Forall P l.
End Forall'.
Section Foralli.
Context `(P : nat → A → Prop).
#[local] Fixpoint Foralli' l i :=
match l with
| [] ⇒
True
| x :: l ⇒
P i x ∧ Foralli' l ˖i
end.
#[global] Arguments Foralli' !_ _ / : assert.
Definition Foralli l :=
Foralli' l 0.
#[local] Lemma Foralli'ｰlookup₁ l i j x :
Foralli' l i →
l !! j = Some x →
P (i + j) x.
Lemma Foralliｰlookup₁ {l} i x :
Foralli l →
l !! i = Some x →
P i x.
Lemma Foralli'ｰlookup₂ l i :
(∀ j x, l !! j = Some x → P (i + j) x) →
Foralli' l i.
Lemma Foralliｰlookup₂ l :
(∀ i x, l !! i = Some x → P i x) →
Foralli l.
Lemma Foralliｰlookup l :
Foralli l ↔
∀ i x, l !! i = Some x → P i x.
End Foralli.
Section Forall2.
Context `(P : A1 → A1 → Prop).
Lemma Forall2ｰinsertｰl {l1 l2} i x1 x2 :
l2 !! i = Some x2 →
Forall2 P l1 l2 →
P x1 x2 →
Forall2 P (<[i := x1]> l1) l2.
Lemma Forall2ｰinsertｰr {l1 l2} i x1 x2 :
l1 !! i = Some x1 →
Forall2 P l1 l2 →
P x1 x2 →
Forall2 P l1 (<[i := x2]> l2).
End Forall2.
Section Forall2'.
Context `(P : A1 → A2 → Prop).
Fixpoint Forall2' l1 l2 :=
match l1, l2 with
| [], [] ⇒
True
| x1 :: l1, x2 :: l2 ⇒
P x1 x2 ∧ Forall2' l1 l2
| _, _ ⇒
False
end.
#[global] Arguments Forall2' !_ !_ / : assert.
Lemma Forall2'ｰForall2 l1 l2 :
Forall2' l1 l2 ↔ Forall2 P l1 l2.
#[global] Instance Forall2'ｰdec `{!RelDecision P} :
RelDecision Forall2'.
Lemma Forall2'ｰlength l1 l2 :
Forall2' l1 l2 →
length l1 = length l2.
End Forall2'.
Section Forall2'.
Context `(P : A → A → Prop).
Lemma Forall2'ｰrefl :
(∀ x, P x x) →
Reflexive (Forall2' P).
#[global] Instance Forall2'ｰreflexive `{!Reflexive P} :
Reflexive (Forall2' P).
Lemma Forall2'ｰsym :
(∀ x1 x2, P x1 x2 → P x2 x1) →
Symmetric (Forall2' P).
#[global] Instance Forall2'ｰsymmetric `{!Symmetric P} :
Symmetric (Forall2' P).
Lemma Forall2'ｰtrans :
(∀ x1 x2 x3, P x1 x2 → P x2 x3 → P x1 x3) →
Transitive (Forall2' P).
#[global] Instance Forall2'ｰtransitive `{!Transitive P} :
Transitive (Forall2' P).
End Forall2'.
Section Forall2i.
Context `(P : nat → A1 → A2 → Prop).
#[local] Fixpoint Forall2i' l1 l2 i :=
match l1, l2 with
| [], [] ⇒
True
| x1 :: l1, x2 :: l2 ⇒
P i x1 x2 ∧ Forall2i' l1 l2 ˖i
| _, _ ⇒
False
end.
#[global] Arguments Forall2i' !_ !_ _ / : assert.
Definition Forall2i l1 l2 :=
Forall2i' l1 l2 0.
#[local] Lemma Forall2i'ｰlength l1 l2 i :
Forall2i' l1 l2 i →
length l1 = length l2.
Lemma Forall2iｰlength l1 l2 :
Forall2i l1 l2 →
length l1 = length l2.
#[local] Lemma Forall2i'ｰlookupｰlr l1 l2 i j x1 x2 :
Forall2i' l1 l2 i →
l1 !! j = Some x1 →
l2 !! j = Some x2 →
P (i + j) x1 x2.
Lemma Forall2iｰlookupｰlr {l1 l2} i x1 x2 :
Forall2i l1 l2 →
l1 !! i = Some x1 →
l2 !! i = Some x2 →
P i x1 x2.
Lemma Forall2iｰlookupｰr l1 l2 i x1 :
Forall2i l1 l2 →
l1 !! i = Some x1 →
∃ x2,
l2 !! i = Some x2 ∧
P i x1 x2.
Lemma Forall2iｰlookupｰl l1 l2 i x2 :
Forall2i l1 l2 →
l2 !! i = Some x2 →
∃ x1,
l1 !! i = Some x1 ∧
P i x1 x2.
#[local] Lemma Forall2i'ｰsame_lengthｰlookup₂ l1 l2 i :
length l1 = length l2 →
( ∀ j x1 x2,
l1 !! j = Some x1 →
l2 !! j = Some x2 →
P (i + j) x1 x2
) →
Forall2i' l1 l2 i.
Lemma Forall2iｰsame_lengthｰlookup₂ l1 l2 :
length l1 = length l2 →
( ∀ i x1 x2,
l1 !! i = Some x1 →
l2 !! i = Some x2 →
P i x1 x2
) →
Forall2i l1 l2.
Lemma Forall2iｰsame_lengthｰlookup l1 l2 :
Forall2i l1 l2 ↔
length l1 = length l2 ∧
∀ i x1 x2,
l1 !! i = Some x1 →
l2 !! i = Some x2 →
P i x1 x2.
End Forall2i.
Section fmap.
Context {A B : Type}.
Implicit Type x : A.
Implicit Type 𝑥 : B.
Implicit Type l : list A.
Implicit Type 𝑙 : list B.
Implicit Type f : A → B.
Lemma fmapｰappｰconsｰinv f l 𝑙1 𝑥 𝑙2 :
f <$> l = 𝑙1 ++ 𝑥 :: 𝑙2 →
∃ l1 x l2,
l = l1 ++ x :: l2 ∧
𝑙1 = f <$> l1 ∧
𝑥 = f x ∧
𝑙2 = f <$> l2.
Lemma fmapｰsnocｰinv f l 𝑙 𝑥 :
f <$> l = 𝑙 ++ [𝑥] →
∃ l' x,
l = l' ++ [x] ∧
𝑙 = f <$> l' ∧
𝑥 = f x.
Lemma listｰfmapｰaltｰForall2ｰl f 𝑙 l :
Forall2 (λ b a, b = f a) 𝑙 l →
𝑙 = f <$> l.
Lemma listｰfmapｰaltｰForall2ｰr f l 𝑙 :
Forall2 (λ a b, f a = b) l 𝑙 →
𝑙 = f <$> l.
End fmap.
Section Permutation.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
#[global] Instance Permutationｰdisjoint :
Proper (Permutation ==> Permutation ==> iff) (disjoint (A := list A)).
Lemma Permutationｰswap' l i1 x1 i2 x2 :
l !! i1 = Some x1 →
l !! i2 = Some x2 →
<[i1 := x2]> (<[i2 := x1]> l) ≡ₚ l.
End Permutation.
Section slice.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
Definition slice i n l :=
take n (drop i l).
Lemma sliceｰcons i n x l :
l !! i = Some x →
x :: slice ˖i n l = slice i ˖n l.
Lemma sliceｰcons' i n x l :
l !! i = Some x →
n ≠ 0 →
x :: slice ˖i (n - 1) l = slice i n l.
Lemma sliceｰsnoc i n l x :
l !! (i + n) = Some x →
slice i n l ++ [x] = slice i ˖n l.
Lemma lengthｰslice i n l :
length (slice i n l) = n `min` (length l - i).
Lemma lengthｰslice' i n l :
i + n ≤ length l →
length (slice i n l) = n.
Lemma sliceｰlookupｰSomeｰinv i n l k x :
slice i n l !! k = Some x →
k < n.
Lemma sliceｰ0 n l :
slice 0 n l = take n l.
End slice.
#[global] Hint Rewrite
@lengthｰslice
: simp_length.
Section with_slice.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l s : list A.
Definition with_slice i n l s :=
take i l ++ s ++ drop (i + n) l.
Lemma lengthｰwith_slice i n l s :
length (with_slice i n l s) = i `min` length l + length s + (length l - i - n).
Lemma lengthｰwith_slice' i n l s :
i + n ≤ length l →
length s = n →
length (with_slice i n l s) = length l.
Lemma with_sliceｰ0 n l s :
with_slice 0 n l s = s ++ drop n l.
Lemma with_sliceｰall n l s :
length l ≤ n →
with_slice 0 n l s = s.
Lemma with_sliceｰappｰl i n l1 l2 s :
i + n ≤ length l1 →
with_slice i n (l1 ++ l2) s = with_slice i n l1 s ++ l2.
Lemma with_sliceｰappｰr i n l1 l2 s :
length l1 ≤ i →
with_slice i n (l1 ++ l2) s = l1 ++ with_slice (i - length l1) n l2 s.
Lemma with_sliceｰappｰlength n l1 l2 s :
with_slice (length l1) n (l1 ++ l2) s = l1 ++ s ++ drop n l2.
Lemma with_sliceｰappｰlength' i n l1 l2 s :
i = length l1 →
with_slice i n (l1 ++ l2) s = l1 ++ s ++ drop n l2.
Lemma with_sliceｰsliceｰnil i l s :
with_slice i 0 l [] = l.
Lemma with_sliceｰsliceｰsnoc i n l s x :
i + n < length l →
length s = n →
with_slice i ˖n l (s ++ [x]) = <[i + n := x]> (with_slice i n l s).
Lemma with_sliceｰlookupｰleft {i n l s} k x :
l !! k = Some x →
k < i →
with_slice i n l s !! k = Some x.
Lemma with_sliceｰlookupｰmiddle {i n l s} k x :
s !! (k - i) = Some x →
i ≤ length l →
i ≤ k →
with_slice i n l s !! k = Some x.
Lemma with_sliceｰlookupｰmiddle' {i n l s} k1 k2 x :
s !! k2 = Some x →
k2 = k1 - i →
i ≤ length l →
i ≤ k1 →
with_slice i n l s !! k1 = Some x.
Lemma with_sliceｰlookupｰright {i n l s} k x :
l !! k = Some x →
length s = n →
i + n ≤ k →
with_slice i n l s !! k = Some x.
End with_slice.
#[global] Hint Rewrite
@lengthｰwith_slice
: simp_length.
Section rotation.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
Definition rotation n l :=
drop n l ++ take n l.
Lemma rotationｰ0 l :
rotation 0 l = l.
Lemma rotationｰS n x l :
n ≤ length l →
rotation ˖n (x :: l) = rotation n (l ++ [x]).
Lemma rotationｰadd n1 n2 l :
n1 + n2 = length l →
rotation n1 (rotation n2 l) = rotation (n1 + n2) l.
Lemma rotationｰlength n l :
n = length l →
rotation n l = l.
Lemma rotationｰPermutation n l :
rotation n l ≡ₚ l.
Lemma lengthｰrotation n l :
length (rotation n l) = length l.
Lemma rotationｰreplicate n k x :
rotation n (replicate k x) = replicate k x.
End rotation.
#[global] Hint Rewrite
@lengthｰrotation
: simp_length.
Section omap.
Context {A : Type}.
Context {B : Type}.
Implicit Type x y : A.
Implicit Type 𝑥 𝑦 : B.
Implicit Type o : option B.
Implicit Type l : list A.
Implicit Type 𝑙 : list B.
Implicit Type f : A → option B.
Lemma lengthｰomap f l :
length (omap f l) ≤ length l.
Lemma listｰomapｰinsertｰNone {f l} i x1 x2 o :
l !! i = Some x1 →
f x1 = None →
f x2 = o →
omap f (<[i := x2]> l) ≡ₚ
match o with
| None ⇒
id
| Some 𝑥 ⇒
cons 𝑥
end $
omap f l.
Lemma listｰomapｰinsertｰNoneｰSome {f l} i x1 x2 𝑥 :
l !! i = Some x1 →
f x1 = None →
f x2 = Some 𝑥 →
omap f (<[i := x2]> l) ≡ₚ 𝑥 :: omap f l.
Lemma listｰomapｰinsertｰNoneｰNone {f l} i x1 x2 :
l !! i = Some x1 →
f x1 = None →
f x2 = None →
omap f (<[i := x2]> l) ≡ₚ omap f l.
Lemma listｰomapｰinsertｰSomeｰNone {f l} i x1 𝑥 x2 :
l !! i = Some x1 →
f x1 = Some 𝑥 →
f x2 = None →
omap f (<[i := x2]> l) = delete (length $ omap f $ take i l) (omap f l).
End omap.
#[global] Hint Rewrite
@lengthｰomap
: simp_length.
Section oflatten.
Context {A : Type}.
Implicit Type x y : A.
Implicit Type o : option A.
Implicit Type l : list (option A).
Definition oflatten l :=
omap id l.
Lemma lengthｰoflatten l :
length (oflatten l) ≤ length l.
Lemma oflattenｰcons o l :
oflatten (o :: l) = from_option (λ x, [x]) [] o ++ oflatten l.
Lemma oflattenｰconsｰNone l :
oflatten (None :: l) = oflatten l.
Lemma oflattenｰconsｰSome x l :
oflatten (Some x :: l) = x :: oflatten l.
Lemma oflattenｰapp l1 l2 :
oflatten (l1 ++ l2) = oflatten l1 ++ oflatten l2.
Lemma oflattenｰsnoc l o :
oflatten (l ++ [o]) = oflatten l ++ from_option (λ x, [x]) [] o.
Lemma oflattenｰsnocｰNone l :
oflatten (l ++ [None]) = oflatten l.
Lemma oflattenｰsnocｰSome l x :
oflatten (l ++ [Some x]) = oflatten l ++ [x].
Lemma elem_ofｰoflatten l x :
x ∈ oflatten l ↔
Some x ∈ l.
Lemma oflattenｰlookupｰSome l i x :
l !! i = Some $ Some x →
oflatten l !! (length $ oflatten $ take i l) = Some x.
Lemma oflattenｰinsertｰNone {l} i o :
l !! i = Some None →
oflatten (<[i := o]> l) ≡ₚ
match o with
| None ⇒
id
| Some x ⇒
cons x
end $
oflatten l.
Lemma oflattenｰinsertｰNoneｰSome {l} i x :
l !! i = Some None →
oflatten (<[i := Some x]> l) ≡ₚ x :: oflatten l.
Lemma oflattenｰinsertｰNoneｰNone {l} i x :
l !! i = Some None →
oflatten (<[i := None]> l) ≡ₚ oflatten l.
Lemma oflattenｰinsertｰSomeｰNone {l} i x :
l !! i = Some $ Some x →
oflatten (<[i := None]> l) = delete (length $ oflatten $ take i l) (oflatten l).
End oflatten.
#[global] Hint Rewrite
@lengthｰoflatten
: simp_length.
Section Sorted.
Context `(R : A → A → Prop).
Implicit Type x : A.
Implicit Type l : list A.
Lemma StronglySortedｰnil :
StronglySorted R [].
Lemma StronglySortedｰsingleton x :
StronglySorted R [x].
Lemma StronglySortedｰtrivial l :
length l ≤ 1 →
StronglySorted R l.
Lemma StronglySortedｰappｰcons `{!Transitive R} l1 x l2 :
StronglySorted R l1 →
Forall (flip R x) l1 →
Forall (R x) l2 →
StronglySorted R l2 →
StronglySorted R (l1 ++ x :: l2).
End Sorted.
Require stdpp.list.
Require stdpp.sorting.
Require Import zoo.prelude.
Require Import zoo.common.math.
Require Import zoo.options.
Export stdpp.list.
Export stdpp.sorting.
Create HintDb simp_length.
#[global] Hint Rewrite
@length_reverse
@length_app
@length_insert
@length_take
@length_drop
@length_fmap
@length_replicate
@length_seq
@length_seqZ
@length_zip_with
: simp_length.
Tactic Notation "simp_length" :=
autorewrite with simp_length; try done.
Tactic Notation "simp_length" "/=" :=
repeat (progress csimpl in × || simp_length).
Tactic Notation "simp_length" "in" ne_hyp_list(Hs) :=
autorewrite with simp_length in Hs; try done.
Tactic Notation "simp_length" "/=" "in" ne_hyp_list(Hs) :=
repeat (progress csimpl in × || simp_length in Hs).
Tactic Notation "simp_length" "in" "*" :=
autorewrite with simp_length in *; try done.
Tactic Notation "simp_length" "/=" "in" "*" :=
repeat (progress csimpl in × || simp_length in × ).
Module lengths.
Import Ltac2.
Ltac2 main () :=
Control.enter (fun () ⇒
List.iter (fun (hyp, _, ty) ⇒
lazy_match! ty with
| _ = _ ⇒
try (apply (f_equal length) in $hyp as ?)
| _ ≡ₚ _ ⇒
apply Permutation_length in $hyp as ?
| _ ⊆+ _ ⇒
apply submseteq_length in $hyp as ?
| _ `prefix_of` _ ⇒
apply prefix_length in $hyp as ?
| _ ⇒
()
end
) (Control.hyps ())
).
End lengths.
Tactic Notation "lengths" :=
ltac2:(lengths.main ());
simp_length in ×.
Tactic Notation "lengths" "/=" :=
ltac2:(lengths.main ());
simp_length/= in ×.
Section basic.
Context {A : Type}.
Implicit Type x y z : A.
Implicit Type l : list A.
Lemma listｰeq l1 l2 :
l1 = l2 ↔
length l1 = length l2 ∧
∀ i x1 x2,
l1 !! i = Some x1 →
l2 !! i = Some x2 →
x1 = x2.
Lemma appｰnotｰnil l1 l2 :
l1 ≠ [] ∨ l2 ≠ [] →
l1 ++ l2 ≠ [].
Lemma appｰnotｰnilｰl l1 l2 :
l1 ≠ [] →
l1 ++ l2 ≠ [].
Lemma appｰnotｰnilｰr l1 l2 :
l2 ≠ [] →
l1 ++ l2 ≠ [].
Lemma lookupｰappｰrｰSome l1 l2 i y :
length l1 ≤ i →
l2 !! (i - length l1) = Some y →
(l1 ++ l2) !! i = Some y.
Lemma lookupｰconsｰrｰSome x l i y :
0 < i →
l !! (i - 1) = Some y →
(x :: l) !! i = Some y.
Lemma elem_ofｰappｰl l1 l2 x :
x ∈ l1 →
x ∈ l1 ++ l2.
Lemma elem_ofｰappｰr l1 l2 x :
x ∈ l2 →
x ∈ l1 ++ l2.
Lemma reverseｰnilｰiff l :
reverse l = [] ↔
l = [].
Lemma foldrｰinsertｰstrong `(f : A → B → B) comp l i x y acc :
l !! i = Some x →
( ∀ x acc,
f x (f y acc) = f y (f x acc)
) →
( ∀ acc,
f (comp y x) acc = f y (f x acc)
) →
foldr f acc (<[i := comp y x]> l) = f y (foldr f acc l).
Lemma foldrｰinsertｰstrong' op `{!Assoc (=) op} `{!Comm (=) op} comp l i x y acc :
l !! i = Some x →
( ∀ acc,
op (comp y x) acc = op y (op x acc)
) →
foldr op acc (<[i := comp y x]> l) = op y (foldr op acc l).
Lemma foldrｰinsert op `{!Assoc (=) op} `{!Comm (=) op} l i x y acc :
l !! i = Some x →
foldr op acc (<[i := op y x]> l) = op y (foldr op acc l).
Lemma lengthｰlookupｰlast l i :
is_Some (l !! i) →
l !! ˖i = None →
length l = ˖i.
Lemma tailｰapp l1 l2 :
l1 ≠ [] →
tail (l1 ++ l2) = tail l1 ++ l2.
Lemma lengthｰtail l :
length (tail l) ≤ length l.
Lemma headｰapp l1 l2 :
0 < length l1 →
head (l1 ++ l2) = head l1.
Lemma headｰappｰcons l1 x l2 :
head (l1 ++ x :: l2) = head (l1 ++ [x]).
Lemma headｰdropｰSome l i x :
l !! i = Some x →
head (drop i l) = Some x.
Lemma headｰdrop l i :
head (drop i l) = l !! i.
Lemma hdｰcorrect default l x :
0 < length l →
hd default l = x →
head l = Some x.
Lemma hdｰapp default l1 l2 :
0 < length l1 →
hd default (l1 ++ l2) = hd default l1.
Lemma hdｰappｰcons default l1 x l2 :
hd default (l1 ++ x :: l2) = hd default (l1 ++ [x]).
Lemma hdｰdropｰSome default l i x :
l !! i = Some x →
hd default (drop i l) = x.
Lemma lastｰcons' x l :
last (x :: l) = Some $ default x (last l).
Lemma lastｰtake l i x :
l !! i = Some x →
last (take ˖i l) = Some x.
Lemma lastｰtake' l i :
is_Some (l !! i) →
last (take i l) = nat۰elim None (l !!.) i.
Lemma lastｰremovelast l x :
last l = Some x →
l = removelast l ++ [x].
Lemma dropｰlookupｰNone l i :
l !! i = None →
drop i l = [].
Lemma dropｰconsｰinv i l x l' :
drop i l = x :: l' →
l !! i = Some x ∧
l' = drop ˖i l.
Lemma insertｰconsｰl i x y l :
i = 0 →
<[i := x]> (y :: l) = x :: l.
Lemma insertｰconsｰr i x y l :
0 < i →
<[i := x]> (y :: l) = y :: <[i - 1 := x]> l.
Lemma insertｰappｰrｰ0 i x l1 l2 :
i = length l1 →
<[i := x]> (l1 ++ l2) = l1 ++ <[0 := x]> l2.
Lemma listｰdeleteｰinsertｰeq l i x :
i < length l →
delete i (<[i := x]> l) = delete i l.
End basic.
Section suffix.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
Lemma suffixｰtail l1 l2 :
l1 `suffix_of` l2 →
tail l1 `suffix_of` l2.
Lemma suffixｰfmap `(f : A → B) `{!Inj (=) (=) f} l1 l2 :
suffix (f <$> l1) (f <$> l2) →
suffix l1 l2.
End suffix.
Section seqZ.
Lemma seqZｰprefix {i n1} n2 :
(0 ≤ n2 ≤ n1)%Z →
seqZ i n2 `prefix_of` seqZ i n1.
Lemma seqZｰsuffix {i1 n1} i2 n2 :
(i1 ≤ i2 ≤ i1 + n1)%Z →
(i2 - i1 = n1 - n2)%Z →
seqZ i2 n2 `suffix_of` seqZ i1 n1.
End seqZ.
Section zip.
Context {A1 A2 : Type}.
Lemma prod_mapｰzip {B1 B2} (f1 : A1 → B1) (f2 : A2 → B2) l1 l2 :
prod_map f1 f2 <$> (zip l1 l2) = zip (f1 <$> l1) (f2 <$> l2).
End zip.
Section zip3_with.
Context {A1 A2 A3 B : Type}.
Implicit Type f : A1 → A2 → A3 → B.
Fixpoint zip3_with f l1 l2 l3 :=
match l1, l2, l3 with
| x1 :: l1, x2 :: l2, x3 :: l3 ⇒
f x1 x2 x3 :: zip3_with f l1 l2 l3
| _, _, _ ⇒
[]
end.
#[global] Arguments zip3_with _ !_ !_ !_ / : assert.
Lemma lengthｰzip3_with f l1 l2 l3 :
length l1 = length l2 →
length l1 = length l3 →
length (zip3_with f l1 l2 l3) = length l1.
Lemma lookupｰzip3_withｰSome f l1 l2 l3 i x :
zip3_with f l1 l2 l3 !! i = Some x ↔
∃ x1 x2 x3,
l1 !! i = Some x1 ∧
l2 !! i = Some x2 ∧
l3 !! i = Some x3 ∧
x = f x1 x2 x3.
End zip3_with.
#[global] Hint Rewrite
@lengthｰzip3_with
: simp_length.
Section zip3.
Context {A1 A2 A3 : Type}.
Definition zip3 :=
zip3_with (B := A1 × A2 × A3) $ λ x1 x2 x3,
(x1, x2, x3).
Lemma zip3ｰcons x1 l1 x2 l2 x3 l3 :
zip3 (x1 :: l1) (x2 :: l2) (x3 :: l3) = (x1, x2, x3) :: zip3 l1 l2 l3.
Lemma lengthｰzip3 l1 l2 l3 :
length l1 = length l2 →
length l1 = length l3 →
length (zip3 l1 l2 l3) = length l1.
Lemma zipｰzip l1 l2 l3 :
zip (zip l1 l2) l3 = zip3 l1 l2 l3.
End zip3.
#[global] Hint Rewrite
@lengthｰzip3
: simp_length.
Section foldri.
Implicit Type i : nat.
Fixpoint foldri' `(f : nat → A → B → B) acc l i :=
match l with
| [] ⇒
acc
| x :: l ⇒
f i x (foldri' f acc l ˖i)
end.
#[global] Arguments foldri' _ _ _ _ !_ _ / : assert.
Definition foldri `(f : nat → A → B → B) acc l :=
foldri' f acc l 0.
#[local] Lemma foldri'ｰapp `(f : nat → A → B → B) acc l1 l2 i :
foldri' f acc (l1 ++ l2) i =
foldri' f (foldri' f acc l2 (i + (length l1))) l1 i.
Lemma foldriｰapp `(f : nat → A → B → B) acc l1 l2 :
foldri f acc (l1 ++ l2) =
foldri f (foldri' f acc l2 (length l1)) l1.
#[local] Lemma foldri'ｰfmap `(f : nat → A → B → B) `(g : C → A) acc l i :
foldri' f acc (g <$> l) i = foldri' (λ i x, f i (g x)) acc l i.
Lemma foldriｰfmap `(f : nat → A → B → B) `(g : C → A) acc l :
foldri f acc (g <$> l) = foldri (λ i x, f i (g x)) acc l.
#[local] Lemma foldri'ｰcomm `(f : nat → A → B → B) `(g : B → C) h acc l i :
( ∀ i x acc,
h i x (g acc) = g (f i x acc)
) →
foldri' h (g acc) l i = g (foldri' f acc l i).
Lemma foldriｰcomm `(f : nat → A → B → B) `(g : B → C) h acc l :
( ∀ i x acc,
h i x (g acc) = g (f i x acc)
) →
foldri h (g acc) l = g (foldri f acc l).
End foldri.
Section foldr2.
Context {A1 A2 B : Type}.
Fixpoint foldr2 (f : A1 → A2 → B → B) acc l1 l2 :=
match l1 with
| [] ⇒
acc
| x1 :: l1 ⇒
match l2 with
| [] ⇒
acc
| x2 :: l2 ⇒
f x1 x2 (foldr2 f acc l1 l2)
end
end.
#[global] Arguments foldr2 _ _ !_ !_ / : assert.
Lemma foldr2ｰapp f acc l11 l12 l21 l22 :
length l11 = length l21 →
foldr2 f acc (l11 ++ l12) (l21 ++ l22) =
foldr2 f (foldr2 f acc l12 l22) l11 l21.
End foldr2.
Section Forall.
Context `(P : A → Prop).
Lemma Forallｰelem_of l x :
Forall P l →
x ∈ l →
P x.
End Forall.
Section Forall'.
Context `(P : A → Prop).
Fixpoint Forall' l :=
match l with
| [] ⇒
True
| x :: l ⇒
P x ∧ Forall' l
end.
#[global] Arguments Forall' !_ / : assert.
Lemma Forall'ｰForall l :
Forall' l ↔ Forall P l.
End Forall'.
Section Foralli.
Context `(P : nat → A → Prop).
#[local] Fixpoint Foralli' l i :=
match l with
| [] ⇒
True
| x :: l ⇒
P i x ∧ Foralli' l ˖i
end.
#[global] Arguments Foralli' !_ _ / : assert.
Definition Foralli l :=
Foralli' l 0.
#[local] Lemma Foralli'ｰlookup₁ l i j x :
Foralli' l i →
l !! j = Some x →
P (i + j) x.
Lemma Foralliｰlookup₁ {l} i x :
Foralli l →
l !! i = Some x →
P i x.
Lemma Foralli'ｰlookup₂ l i :
(∀ j x, l !! j = Some x → P (i + j) x) →
Foralli' l i.
Lemma Foralliｰlookup₂ l :
(∀ i x, l !! i = Some x → P i x) →
Foralli l.
Lemma Foralliｰlookup l :
Foralli l ↔
∀ i x, l !! i = Some x → P i x.
End Foralli.
Section Forall2.
Context `(P : A1 → A1 → Prop).
Lemma Forall2ｰinsertｰl {l1 l2} i x1 x2 :
l2 !! i = Some x2 →
Forall2 P l1 l2 →
P x1 x2 →
Forall2 P (<[i := x1]> l1) l2.
Lemma Forall2ｰinsertｰr {l1 l2} i x1 x2 :
l1 !! i = Some x1 →
Forall2 P l1 l2 →
P x1 x2 →
Forall2 P l1 (<[i := x2]> l2).
End Forall2.
Section Forall2'.
Context `(P : A1 → A2 → Prop).
Fixpoint Forall2' l1 l2 :=
match l1, l2 with
| [], [] ⇒
True
| x1 :: l1, x2 :: l2 ⇒
P x1 x2 ∧ Forall2' l1 l2
| _, _ ⇒
False
end.
#[global] Arguments Forall2' !_ !_ / : assert.
Lemma Forall2'ｰForall2 l1 l2 :
Forall2' l1 l2 ↔ Forall2 P l1 l2.
#[global] Instance Forall2'ｰdec `{!RelDecision P} :
RelDecision Forall2'.
Lemma Forall2'ｰlength l1 l2 :
Forall2' l1 l2 →
length l1 = length l2.
End Forall2'.
Section Forall2'.
Context `(P : A → A → Prop).
Lemma Forall2'ｰrefl :
(∀ x, P x x) →
Reflexive (Forall2' P).
#[global] Instance Forall2'ｰreflexive `{!Reflexive P} :
Reflexive (Forall2' P).
Lemma Forall2'ｰsym :
(∀ x1 x2, P x1 x2 → P x2 x1) →
Symmetric (Forall2' P).
#[global] Instance Forall2'ｰsymmetric `{!Symmetric P} :
Symmetric (Forall2' P).
Lemma Forall2'ｰtrans :
(∀ x1 x2 x3, P x1 x2 → P x2 x3 → P x1 x3) →
Transitive (Forall2' P).
#[global] Instance Forall2'ｰtransitive `{!Transitive P} :
Transitive (Forall2' P).
End Forall2'.
Section Forall2i.
Context `(P : nat → A1 → A2 → Prop).
#[local] Fixpoint Forall2i' l1 l2 i :=
match l1, l2 with
| [], [] ⇒
True
| x1 :: l1, x2 :: l2 ⇒
P i x1 x2 ∧ Forall2i' l1 l2 ˖i
| _, _ ⇒
False
end.
#[global] Arguments Forall2i' !_ !_ _ / : assert.
Definition Forall2i l1 l2 :=
Forall2i' l1 l2 0.
#[local] Lemma Forall2i'ｰlength l1 l2 i :
Forall2i' l1 l2 i →
length l1 = length l2.
Lemma Forall2iｰlength l1 l2 :
Forall2i l1 l2 →
length l1 = length l2.
#[local] Lemma Forall2i'ｰlookupｰlr l1 l2 i j x1 x2 :
Forall2i' l1 l2 i →
l1 !! j = Some x1 →
l2 !! j = Some x2 →
P (i + j) x1 x2.
Lemma Forall2iｰlookupｰlr {l1 l2} i x1 x2 :
Forall2i l1 l2 →
l1 !! i = Some x1 →
l2 !! i = Some x2 →
P i x1 x2.
Lemma Forall2iｰlookupｰr l1 l2 i x1 :
Forall2i l1 l2 →
l1 !! i = Some x1 →
∃ x2,
l2 !! i = Some x2 ∧
P i x1 x2.
Lemma Forall2iｰlookupｰl l1 l2 i x2 :
Forall2i l1 l2 →
l2 !! i = Some x2 →
∃ x1,
l1 !! i = Some x1 ∧
P i x1 x2.
#[local] Lemma Forall2i'ｰsame_lengthｰlookup₂ l1 l2 i :
length l1 = length l2 →
( ∀ j x1 x2,
l1 !! j = Some x1 →
l2 !! j = Some x2 →
P (i + j) x1 x2
) →
Forall2i' l1 l2 i.
Lemma Forall2iｰsame_lengthｰlookup₂ l1 l2 :
length l1 = length l2 →
( ∀ i x1 x2,
l1 !! i = Some x1 →
l2 !! i = Some x2 →
P i x1 x2
) →
Forall2i l1 l2.
Lemma Forall2iｰsame_lengthｰlookup l1 l2 :
Forall2i l1 l2 ↔
length l1 = length l2 ∧
∀ i x1 x2,
l1 !! i = Some x1 →
l2 !! i = Some x2 →
P i x1 x2.
End Forall2i.
Section fmap.
Context {A B : Type}.
Implicit Type x : A.
Implicit Type 𝑥 : B.
Implicit Type l : list A.
Implicit Type 𝑙 : list B.
Implicit Type f : A → B.
Lemma fmapｰappｰconsｰinv f l 𝑙1 𝑥 𝑙2 :
f <$> l = 𝑙1 ++ 𝑥 :: 𝑙2 →
∃ l1 x l2,
l = l1 ++ x :: l2 ∧
𝑙1 = f <$> l1 ∧
𝑥 = f x ∧
𝑙2 = f <$> l2.
Lemma fmapｰsnocｰinv f l 𝑙 𝑥 :
f <$> l = 𝑙 ++ [𝑥] →
∃ l' x,
l = l' ++ [x] ∧
𝑙 = f <$> l' ∧
𝑥 = f x.
Lemma listｰfmapｰaltｰForall2ｰl f 𝑙 l :
Forall2 (λ b a, b = f a) 𝑙 l →
𝑙 = f <$> l.
Lemma listｰfmapｰaltｰForall2ｰr f l 𝑙 :
Forall2 (λ a b, f a = b) l 𝑙 →
𝑙 = f <$> l.
End fmap.
Section Permutation.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
#[global] Instance Permutationｰdisjoint :
Proper (Permutation ==> Permutation ==> iff) (disjoint (A := list A)).
Lemma Permutationｰswap' l i1 x1 i2 x2 :
l !! i1 = Some x1 →
l !! i2 = Some x2 →
<[i1 := x2]> (<[i2 := x1]> l) ≡ₚ l.
End Permutation.
Section slice.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
Definition slice i n l :=
take n (drop i l).
Lemma sliceｰcons i n x l :
l !! i = Some x →
x :: slice ˖i n l = slice i ˖n l.
Lemma sliceｰcons' i n x l :
l !! i = Some x →
n ≠ 0 →
x :: slice ˖i (n - 1) l = slice i n l.
Lemma sliceｰsnoc i n l x :
l !! (i + n) = Some x →
slice i n l ++ [x] = slice i ˖n l.
Lemma lengthｰslice i n l :
length (slice i n l) = n `min` (length l - i).
Lemma lengthｰslice' i n l :
i + n ≤ length l →
length (slice i n l) = n.
Lemma sliceｰlookupｰSomeｰinv i n l k x :
slice i n l !! k = Some x →
k < n.
Lemma sliceｰ0 n l :
slice 0 n l = take n l.
End slice.
#[global] Hint Rewrite
@lengthｰslice
: simp_length.
Section with_slice.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l s : list A.
Definition with_slice i n l s :=
take i l ++ s ++ drop (i + n) l.
Lemma lengthｰwith_slice i n l s :
length (with_slice i n l s) = i `min` length l + length s + (length l - i - n).
Lemma lengthｰwith_slice' i n l s :
i + n ≤ length l →
length s = n →
length (with_slice i n l s) = length l.
Lemma with_sliceｰ0 n l s :
with_slice 0 n l s = s ++ drop n l.
Lemma with_sliceｰall n l s :
length l ≤ n →
with_slice 0 n l s = s.
Lemma with_sliceｰappｰl i n l1 l2 s :
i + n ≤ length l1 →
with_slice i n (l1 ++ l2) s = with_slice i n l1 s ++ l2.
Lemma with_sliceｰappｰr i n l1 l2 s :
length l1 ≤ i →
with_slice i n (l1 ++ l2) s = l1 ++ with_slice (i - length l1) n l2 s.
Lemma with_sliceｰappｰlength n l1 l2 s :
with_slice (length l1) n (l1 ++ l2) s = l1 ++ s ++ drop n l2.
Lemma with_sliceｰappｰlength' i n l1 l2 s :
i = length l1 →
with_slice i n (l1 ++ l2) s = l1 ++ s ++ drop n l2.
Lemma with_sliceｰsliceｰnil i l s :
with_slice i 0 l [] = l.
Lemma with_sliceｰsliceｰsnoc i n l s x :
i + n < length l →
length s = n →
with_slice i ˖n l (s ++ [x]) = <[i + n := x]> (with_slice i n l s).
Lemma with_sliceｰlookupｰleft {i n l s} k x :
l !! k = Some x →
k < i →
with_slice i n l s !! k = Some x.
Lemma with_sliceｰlookupｰmiddle {i n l s} k x :
s !! (k - i) = Some x →
i ≤ length l →
i ≤ k →
with_slice i n l s !! k = Some x.
Lemma with_sliceｰlookupｰmiddle' {i n l s} k1 k2 x :
s !! k2 = Some x →
k2 = k1 - i →
i ≤ length l →
i ≤ k1 →
with_slice i n l s !! k1 = Some x.
Lemma with_sliceｰlookupｰright {i n l s} k x :
l !! k = Some x →
length s = n →
i + n ≤ k →
with_slice i n l s !! k = Some x.
End with_slice.
#[global] Hint Rewrite
@lengthｰwith_slice
: simp_length.
Section rotation.
Context {A : Type}.
Implicit Type x : A.
Implicit Type l : list A.
Definition rotation n l :=
drop n l ++ take n l.
Lemma rotationｰ0 l :
rotation 0 l = l.
Lemma rotationｰS n x l :
n ≤ length l →
rotation ˖n (x :: l) = rotation n (l ++ [x]).
Lemma rotationｰadd n1 n2 l :
n1 + n2 = length l →
rotation n1 (rotation n2 l) = rotation (n1 + n2) l.
Lemma rotationｰlength n l :
n = length l →
rotation n l = l.
Lemma rotationｰPermutation n l :
rotation n l ≡ₚ l.
Lemma lengthｰrotation n l :
length (rotation n l) = length l.
Lemma rotationｰreplicate n k x :
rotation n (replicate k x) = replicate k x.
End rotation.
#[global] Hint Rewrite
@lengthｰrotation
: simp_length.
Section omap.
Context {A : Type}.
Context {B : Type}.
Implicit Type x y : A.
Implicit Type 𝑥 𝑦 : B.
Implicit Type o : option B.
Implicit Type l : list A.
Implicit Type 𝑙 : list B.
Implicit Type f : A → option B.
Lemma lengthｰomap f l :
length (omap f l) ≤ length l.
Lemma listｰomapｰinsertｰNone {f l} i x1 x2 o :
l !! i = Some x1 →
f x1 = None →
f x2 = o →
omap f (<[i := x2]> l) ≡ₚ
match o with
| None ⇒
id
| Some 𝑥 ⇒
cons 𝑥
end $
omap f l.
Lemma listｰomapｰinsertｰNoneｰSome {f l} i x1 x2 𝑥 :
l !! i = Some x1 →
f x1 = None →
f x2 = Some 𝑥 →
omap f (<[i := x2]> l) ≡ₚ 𝑥 :: omap f l.
Lemma listｰomapｰinsertｰNoneｰNone {f l} i x1 x2 :
l !! i = Some x1 →
f x1 = None →
f x2 = None →
omap f (<[i := x2]> l) ≡ₚ omap f l.
Lemma listｰomapｰinsertｰSomeｰNone {f l} i x1 𝑥 x2 :
l !! i = Some x1 →
f x1 = Some 𝑥 →
f x2 = None →
omap f (<[i := x2]> l) = delete (length $ omap f $ take i l) (omap f l).
End omap.
#[global] Hint Rewrite
@lengthｰomap
: simp_length.
Section oflatten.
Context {A : Type}.
Implicit Type x y : A.
Implicit Type o : option A.
Implicit Type l : list (option A).
Definition oflatten l :=
omap id l.
Lemma lengthｰoflatten l :
length (oflatten l) ≤ length l.
Lemma oflattenｰcons o l :
oflatten (o :: l) = from_option (λ x, [x]) [] o ++ oflatten l.
Lemma oflattenｰconsｰNone l :
oflatten (None :: l) = oflatten l.
Lemma oflattenｰconsｰSome x l :
oflatten (Some x :: l) = x :: oflatten l.
Lemma oflattenｰapp l1 l2 :
oflatten (l1 ++ l2) = oflatten l1 ++ oflatten l2.
Lemma oflattenｰsnoc l o :
oflatten (l ++ [o]) = oflatten l ++ from_option (λ x, [x]) [] o.
Lemma oflattenｰsnocｰNone l :
oflatten (l ++ [None]) = oflatten l.
Lemma oflattenｰsnocｰSome l x :
oflatten (l ++ [Some x]) = oflatten l ++ [x].
Lemma elem_ofｰoflatten l x :
x ∈ oflatten l ↔
Some x ∈ l.
Lemma oflattenｰlookupｰSome l i x :
l !! i = Some $ Some x →
oflatten l !! (length $ oflatten $ take i l) = Some x.
Lemma oflattenｰinsertｰNone {l} i o :
l !! i = Some None →
oflatten (<[i := o]> l) ≡ₚ
match o with
| None ⇒
id
| Some x ⇒
cons x
end $
oflatten l.
Lemma oflattenｰinsertｰNoneｰSome {l} i x :
l !! i = Some None →
oflatten (<[i := Some x]> l) ≡ₚ x :: oflatten l.
Lemma oflattenｰinsertｰNoneｰNone {l} i x :
l !! i = Some None →
oflatten (<[i := None]> l) ≡ₚ oflatten l.
Lemma oflattenｰinsertｰSomeｰNone {l} i x :
l !! i = Some $ Some x →
oflatten (<[i := None]> l) = delete (length $ oflatten $ take i l) (oflatten l).
End oflatten.
#[global] Hint Rewrite
@lengthｰoflatten
: simp_length.
Section Sorted.
Context `(R : A → A → Prop).
Implicit Type x : A.
Implicit Type l : list A.
Lemma StronglySortedｰnil :
StronglySorted R [].
Lemma StronglySortedｰsingleton x :
StronglySorted R [x].
Lemma StronglySortedｰtrivial l :
length l ≤ 1 →
StronglySorted R l.
Lemma StronglySortedｰappｰcons `{!Transitive R} l1 x l2 :
StronglySorted R l1 →
Forall (flip R x) l1 →
Forall (R x) l2 →
StronglySorted R l2 →
StronglySorted R (l1 ++ x :: l2).
End Sorted.