Library zoo.common.list
From stdpp Require
list
sorting.
From zoo Require Import
prelude.
From zoo.common Require Import
math.
From zoo Require Import
options.
Export stdpp.list.
Export stdpp.sorting.
Create HintDb simpl_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
: simpl_length.
Tactic Notation "simpl_length" :=
autorewrite with simpl_length; try done.
Tactic Notation "simpl_length" "/=" :=
repeat (progress csimpl in × || simpl_length).
Tactic Notation "simpl_length" "in" ne_hyp_list(Hs) :=
autorewrite with simpl_length in Hs; try done.
Tactic Notation "simpl_length" "/=" "in" ne_hyp_list(Hs) :=
repeat (progress csimpl in × || simpl_length in Hs).
Tactic Notation "simpl_length" "in" "*" :=
autorewrite with simpl_length in *; try done.
Tactic Notation "simpl_length" "/=" "in" "*" :=
repeat (progress csimpl in × || simpl_length in × ).
Section basic.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types 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 !! S i = None →
length l = S 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 (S 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 (S 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 Types x : A.
Implicit Types 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 Types 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
: simpl_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
: simpl_length.
Section foldri.
Implicit Types 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 (S 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 (S i)
end.
#[global] Arguments Foralli' !_ _ / : assert.
Definition Foralli l :=
Foralli' l 0.
#[local] Lemma Foralli'_lookup_1 l i j x :
Foralli' l i →
l !! j = Some x →
P (i + j) x.
Lemma Foralli_lookup_1 {l} i x :
Foralli l →
l !! i = Some x →
P i x.
Lemma Foralli'_lookup_2 l i :
(∀ j x, l !! j = Some x → P (i + j) x) →
Foralli' l i.
Lemma Foralli_lookup_2 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 (S 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_2 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_2 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 Types x : A.
Implicit Types 𝑥 : B.
Implicit Types l : list A.
Implicit Types 𝑙 : list B.
Implicit Types 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 Types x : A.
Implicit Types 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 Types x : A.
Implicit Types 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 (S i) n l = slice i (S n) l.
Lemma slice_cons' i n x l :
l !! i = Some x →
n ≠ 0 →
x :: slice (S 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 (S 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
: simpl_length.
Section with_slice.
Context {A : Type}.
Implicit Types x : A.
Implicit Types 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 (S 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
: simpl_length.
Section rotation.
Context {A : Type}.
Implicit Types x : A.
Implicit Types 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 (S 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
: simpl_length.
Section omap.
Context {A : Type}.
Context {B : Type}.
Implicit Types x y : A.
Implicit Types 𝑥 𝑦 : B.
Implicit Types o : option B.
Implicit Types l : list A.
Implicit Types 𝑙 : list B.
Implicit Types 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
: simpl_length.
Section oflatten.
Context {A : Type}.
Implicit Types x y : A.
Implicit Types o : option A.
Implicit Types 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
: simpl_length.
Section Sorted.
Context `(R : A → A → Prop).
Implicit Types x : A.
Implicit Types 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.
list
sorting.
From zoo Require Import
prelude.
From zoo.common Require Import
math.
From zoo Require Import
options.
Export stdpp.list.
Export stdpp.sorting.
Create HintDb simpl_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
: simpl_length.
Tactic Notation "simpl_length" :=
autorewrite with simpl_length; try done.
Tactic Notation "simpl_length" "/=" :=
repeat (progress csimpl in × || simpl_length).
Tactic Notation "simpl_length" "in" ne_hyp_list(Hs) :=
autorewrite with simpl_length in Hs; try done.
Tactic Notation "simpl_length" "/=" "in" ne_hyp_list(Hs) :=
repeat (progress csimpl in × || simpl_length in Hs).
Tactic Notation "simpl_length" "in" "*" :=
autorewrite with simpl_length in *; try done.
Tactic Notation "simpl_length" "/=" "in" "*" :=
repeat (progress csimpl in × || simpl_length in × ).
Section basic.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types 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 !! S i = None →
length l = S 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 (S 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 (S 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 Types x : A.
Implicit Types 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 Types 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
: simpl_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
: simpl_length.
Section foldri.
Implicit Types 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 (S 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 (S i)
end.
#[global] Arguments Foralli' !_ _ / : assert.
Definition Foralli l :=
Foralli' l 0.
#[local] Lemma Foralli'_lookup_1 l i j x :
Foralli' l i →
l !! j = Some x →
P (i + j) x.
Lemma Foralli_lookup_1 {l} i x :
Foralli l →
l !! i = Some x →
P i x.
Lemma Foralli'_lookup_2 l i :
(∀ j x, l !! j = Some x → P (i + j) x) →
Foralli' l i.
Lemma Foralli_lookup_2 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 (S 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_2 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_2 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 Types x : A.
Implicit Types 𝑥 : B.
Implicit Types l : list A.
Implicit Types 𝑙 : list B.
Implicit Types 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 Types x : A.
Implicit Types 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 Types x : A.
Implicit Types 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 (S i) n l = slice i (S n) l.
Lemma slice_cons' i n x l :
l !! i = Some x →
n ≠ 0 →
x :: slice (S 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 (S 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
: simpl_length.
Section with_slice.
Context {A : Type}.
Implicit Types x : A.
Implicit Types 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 (S 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
: simpl_length.
Section rotation.
Context {A : Type}.
Implicit Types x : A.
Implicit Types 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 (S 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
: simpl_length.
Section omap.
Context {A : Type}.
Context {B : Type}.
Implicit Types x y : A.
Implicit Types 𝑥 𝑦 : B.
Implicit Types o : option B.
Implicit Types l : list A.
Implicit Types 𝑙 : list B.
Implicit Types 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
: simpl_length.
Section oflatten.
Context {A : Type}.
Implicit Types x y : A.
Implicit Types o : option A.
Implicit Types 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
: simpl_length.
Section Sorted.
Context `(R : A → A → Prop).
Implicit Types x : A.
Implicit Types 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.