File stdpp_ext
(* Extensions to the stdpp library *)
From Coq Require Export ssreflect ssrfun ssrbool String.
From Coq.Logic Require Import Classical_Prop Classical_Pred_Type Eqdep_dec.
From stdpp Require Export list propset sets pmap gmap mapset coGset.
Export list. (* to overwrite module qualifiers *)
Lemma foldl_fold_left :
∀ {A B} f (l : list A) (b : B),
foldl f b l = fold_left f l b.
Fixpoint index_of_helper (x : string) (l : list string) (n : nat) : option nat :=
match l with
| [] ⇒ None
| y::ys ⇒ match string_dec x y with
| left _ ⇒ Some n
| right _ ⇒ index_of_helper x ys (S n)
end
end.
Definition index_of x l := index_of_helper x l 0.
Lemma decide_eq_same (A : Type) {dec : ∀ (t1 t2 : A), Decision (t1 = t2)} t:
decide (t = t) = left erefl.
Lemma pmap_to_list_lookup {A} (M : Pmap A) (i : positive) (x : A)
: (i,x) ∈ (map_to_list M) ↔ lookup i M = Some x.
(* Lemma gmap_to_list_lookup `{Countable K} {A} (M : gmap K A) (k : K) (a : A):
((k,a) ∈ (gmap_to_list M)) <-> (M !! k = Some a).
Proof.
unfold elem_of.
unfold lookup.
destruct M as PM PMwf eqn: HM. simpl.
unfold gmap_wf in PMwf.
split; intros H'.
+ apply pmap_to_list_lookup.
apply elem_of_list_omap in H'.
destruct H' as [k' a'] [HxinPM H'].
apply fmap_Some_1 in H'.
destruct H' as k'' [H1 H2]. inversion H2. subst. clear H2.
assert (Hk': k' = encode k'').
{ apply bool_decide_unpack in PMwf.
unfold map_Forall in PMwf.
apply pmap_to_list_lookup in HxinPM.
specialize (PMwf k' a' HxinPM).
apply (inj Some). rewrite <- PMwf.
apply fmap_Some_2. apply H1. }
subst. apply HxinPM.
+ apply pmap_to_list_lookup in H'.
apply elem_of_list_omap.
exists (encode k, a). firstorder.
rewrite -> decode_encode. simpl. reflexivity.
Qed. *)
#[global]
Program Instance inj_unit_r {K} : @Inj (K × ()) K (@eq (K × ())) (@eq K) (@fst K ()).
Lemma gset_to_list_elem_of `{Countable K} (S : gset K) (k : K) : k ∈ (mapset_elements S) ↔ k ∈ S.
Lemma mapset_elements_to_set `{Countable K} (X : gset K) : list_to_set (mapset_elements X) = X.
Lemma rev_tail_rev_app A (l : list A) (a : A) :
l ≠ [] → rev (tail (l ++ [a])) = a :: rev (tail l).
(* 1,2,3,4,5 -> 5,4,3,2,1 -> 4,3,2,1 -> 1,2,3,4 *)
Lemma rev_tail_rev_app_last A (l : list A) (xlast : A):
stdpp.list.last l = Some xlast →
(rev (tail (rev l)) ++ [xlast]) = l.
Lemma length_tail_zero A l: @length A (tail l) = 0 ↔ (@length A l = 0 ∨ @length A l = 1).
Lemma hd_error_app A (a b : A) (l : list A) :
hd_error ((l ++ [a]) ++ [b]) = hd_error (l ++ [a]).
Lemma last_rev_head A (l : list A) (x : A) : stdpp.list.last (x :: l) = hd_error (rev l ++ [x]).
(* The same lemma for stdpp's `reverse *)
Lemma last_reverse_head A (l : list A) (x : A) : stdpp.list.last (x :: l) = hd_error (reverse l ++ [x]).
Lemma hd_error_lookup A (l : list A) :
l !! 0 = hd_error l.
Lemma list_len_slice A (l1 l2 : list A) (a b : A) :
a :: l1 = l2 ++ [b] → length l1 = length l2.
Fixpoint skip_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :=
match l with
| nil ⇒ nil
| (x,y) :: xs ⇒
match (decide (x=y)) with
| left _ ⇒ @skip_eq _ eqdec xs
| right _ ⇒ l
end
end.
Lemma skip_eq_head_not_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :
∀ x y, hd_error (skip_eq l) = Some (x,y) → x ≠ y.
Definition tail_skip_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :=
reverse (skip_eq (reverse l)).
Lemma tail_skip_eq_last_not_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :
∀ x y, stdpp.list.last (tail_skip_eq l) = Some (x, y) → x ≠ y.
Fixpoint common_length {A} {eqdec: EqDecision A} (l₁ l₂ : list A) :=
match l₁,l₂ with
| nil,nil ⇒ 0
| nil,_ ⇒ 0
| _,nil ⇒ 0
| (x::xs),(y::ys) ⇒
match (decide (x=y)) with
| left _ ⇒ S (@common_length _ eqdec xs ys)
| right _ ⇒ 0
end
end.
Lemma common_length_l_nil {A} {eqdec: EqDecision A} (l₁ : list A) :
common_length l₁ nil = 0.
Lemma common_length_sym {A} {eqdec: EqDecision A} (l₁ l₂ : list A) :
common_length l₁ l₂ = common_length l₂ l₁.
Lemma common_length_rev {A} {eqdec: EqDecision A} (x y : A) (xs ys : list A) :
common_length (reverse (x::xs)) (y::ys) =
match (decide ((stdpp.list.last (x::xs)) = Some y)) with
| left _ ⇒ S (common_length (reverse (tail (reverse (x::xs)))) ys)
| right _ ⇒ 0
end.
Lemma last_app_singleton {A} (m : A) (l : list A) :
stdpp.list.last (l ++ [m]) = Some m.
Lemma rev_reverse {A} (l : list A) :
rev l = reverse l.
Lemma forall_zip_flip {A B : Type} (f : A → B → Prop) (xs : list A) (ys: list B) :
Forall (uncurry f) (zip xs ys) ↔ Forall (uncurry (flip f)) (zip ys xs).
Lemma tail_app_nonempty {A : Type} (x : A) (xs ys : list A) :
tail ((x::xs) ++ ys) = (tail (x::xs)) ++ ys.
Lemma tail_app_nonempty' {A : Type} (xs ys : list A) :
length xs ≥ 1 →
tail (xs ++ ys) = (tail xs) ++ ys.
Lemma length_tail {A : Type} (l : list A) :
length (tail l) = length l - 1.
Lemma zip_smaller :
∀ {T1 T2} (l1 : list T1) (l2 : list T2), length l1 = length l2 →
∀ l3, zip l1 l2 = zip l1 (l2 ++ l3).
Lemma reverse_zip_tail_r {A : Type} (m : A) (l : list A) :
reverse (zip (m :: l) (tail (m :: l)))
= zip (tail (reverse (m :: l))) (reverse (m :: l)).
Lemma Forall_zip_flip_reverse {A : Type} (f : A → A → Prop) (m : A) (l : list A) :
Forall (uncurry f) (zip (m::l) (tail (m::l)))
↔
Forall (uncurry (flip f)) (zip (reverse (m::l)) (tail (reverse (m::l)))).
Lemma Forall_drop {A : Type} (P : A → Prop) (n : nat) (l : list A) :
Forall P l → Forall P (drop n l).
Lemma last_drop {A : Type} (l : list A) (n : nat) (x : A) :
stdpp.list.last l = Some x →
n < length l →
stdpp.list.last (drop n l) = Some x.
Lemma tail_drop {A : Type} (l : list A) (n : nat) :
tail (drop n l) = drop (S n) l.
Lemma drop_tail {A : Type} (l : list A) (n : nat) :
drop n (tail l) = drop (S n) l.
Lemma tail_drop_comm {A : Type} (l : list A) (n : nat) :
tail (drop n l) = drop n (tail l).
Lemma hd_drop_lookup {A : Type} (l : list A) (n : nat) (m : A) :
l !! n = Some m →
hd_error (drop n l) = Some m.
Lemma list_ex_elem {A : Type} (l : list A) (n : nat) :
n < length l → ∃ x, l!!n = Some x.
Lemma list_last_length {A : Type} (l : list A):
stdpp.list.last l = l !! (length l - 1).
Lemma equal_up_to_common_length {A : Type} {eqdec: EqDecision A} (l₁ l₂ : list A) :
∀ (n:nat),
n < common_length l₁ l₂ →
l₁ !! n = l₂ !! n.
Lemma last_tail {A : Type} (l : list A) (lst m : A) :
stdpp.list.last l = Some lst →
head (tail l) = Some m →
stdpp.list.last (tail l) = Some lst.
Lemma tail_zip_with {A B C : Type} (f : A → B → C) (l₁ : list A) (l₂ : list B) :
tail (zip_with f l₁ l₂) = zip_with f (tail l₁) (tail l₂).
Lemma tail_zip {A : Type} (l₁ l₂ : list A) :
tail (zip l₁ l₂) = zip (tail l₁) (tail l₂).
Lemma common_length_impl_eq {A : Type} {eqdec: EqDecision A} (l₁ l₂ : list A) :
length l₁ = length l₂ →
common_length l₁ l₂ = length l₂ →
l₁ = l₂.
Lemma not_elem_of_larger_impl_not_elem_of {A C : Type} {H : ElemOf A C} (x : A) (S B : C) :
S ⊆ B →
x ∉ B →
x ∉ S.
Tactic Notation "solve_set_inclusion" int_or_var(depth) :=
apply elem_of_subseteq;
let x := fresh "x" in
let H := fresh "Hxin" in
(* TODO: maybe we need something like: *)
(*rewrite -!union_assoc_L.*)
(* We may also want to remove duplicates, at least those that are neighbors *)
intros x H;
repeat (
match H with
| ?L ∧ ?R ⇒ fail "Not implemented: destruct H"
| _ ⇒ eauto depth using @sets.elem_of_union_l, @sets.elem_of_union_r with typeclass_instances
end
).
Lemma map_take {A B : Type} (f : A → B) (l : list A) (n : nat) :
map f (take n l) = take n (map f l).
Lemma map_drop {A B : Type} (f : A → B) (l : list A) (n : nat) :
map f (drop n l) = drop n (map f l).
Lemma foldr_andb_true_take n l:
foldr andb true l →
foldr andb true (take n l).
Lemma foldr_andb_true_drop n l:
foldr andb true l →
foldr andb true (drop n l).
Definition propset_fa_union {T C : Type} (f : C → propset T) : propset T
:= PropSet (fun (x : T) ⇒ ∃ (c : C), x ∈ f c).
Lemma propset_fa_union_same {T C : Type} {LE : LeibnizEquiv (propset T)} (f f' : C → propset T):
(∀ c, (f c) = (f' c)) →
(propset_fa_union f) = (propset_fa_union f').
Global Instance propset_fa_union_proper {T C : Type}
: Proper (pointwise_relation C (≡) ==> (≡)) (@propset_fa_union T C).
Lemma propset_fa_union_empty {T C : Type} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_union f = ∅) ↔ (∀ (c : C), (f c) = ∅).
Lemma propset_fa_union_full {T C : Type} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_union f = ⊤) ↔ (∀ (t : T), ∃ (c : C), t ∈ (f c)).
Lemma propset_fa_union_included : ∀ T C : Type, ∀ f f' : C → propset T,
(∀ c, (f c) ⊆ (f' c)) →
(propset_fa_union f) ⊆ (propset_fa_union f').
Definition propset_fa_intersection {T C : Type} (f : C → propset T) : propset T
:= PropSet (fun (x : T) ⇒ ∀ (c : C), x ∈ f c).
Lemma propset_fa_intersection_empty {T C : Type} {INH : Inhabited C} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_intersection f = ∅) ↔ (∀ (t : T), ∃ (c : C), t ∉ (f c)).
Lemma propset_fa_intersection_full {T C : Type} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_intersection f = ⊤) ↔ (∀ (c : C), (f c) = ⊤).
Lemma Not_Empty_Contains_Elements {T : Type} {LE : LeibnizEquiv (propset T)} (S : propset T):
S ≠ ∅ → ∃ x : T, x ∈ S.
Lemma Contains_Elements_Not_Empty {T : Type} (S : propset T):
(∃ x : T, x ∈ S) → S ≠ ∅.
Lemma Not_Empty_iff_Contains_Elements {T : Type} {LE : LeibnizEquiv (propset T)} (S : propset T):
S ≠ ∅ ↔
∃ x : T, x ∈ S.
Lemma Compl_Compl_propset {T : Type} {LE : LeibnizEquiv (propset T)} (A : propset T):
(⊤ ∖ (⊤ ∖ A)) = A.
Lemma Compl_Union_Compl_Inters_propset_alt {T : Type} {LE : LeibnizEquiv (propset T)} (L R : propset T):
(⊤ ∖ ((⊤ ∖ L) ∪ (⊤ ∖ R))) = (L ∩ R).
Lemma complement_full_iff_empty {T : Type} {LE : LeibnizEquiv (propset T)} (A : propset T):
(⊤ ∖ A = ⊤) ↔ (A = ∅).
Lemma complement_empty_iff_full {T : Type} {LE : LeibnizEquiv (propset T)} (A : propset T):
(⊤ ∖ A = ∅) ↔ (A = ⊤).
Lemma intersection_full_iff_both_full {T : Type} {LE : LeibnizEquiv (propset T)} (L R : propset T):
(L ∩ R = ⊤) ↔ (L = ⊤ ∧ R = ⊤).
Lemma union_with_complement {T : Type} {LE : LeibnizEquiv (propset T)} (X : propset T):
(⊤ ∖ X) ∪ X = ⊤.
Lemma elem_of_compl {T : Type} {LE : LeibnizEquiv (propset T)} (X : propset T) (x : T):
(x ∈ (⊤ ∖ X)) ↔ (x ∉ X).
Lemma elem_of_singleton_sym
{A C : Type} {H : ElemOf A C} {H0 : Empty C} {H1 : Singleton A C}
{H2 : Union C} {H3 : SemiSet A C} :
∀ (x y : A), x ∈ (@singleton A C H1 y) ↔ y ∈ (@singleton A C H1 x).
Global Instance set_unfold_gset_to_coGset
{A : Type} {_eqA : EqDecision A} {_cntA : Countable A} (x : A) (X : @gmap.gset A _eqA _cntA) P
:
SetUnfoldElemOf x X P →
SetUnfoldElemOf x (gset_to_coGset X) P.
Lemma foldr_ind {A B} (P : B → Prop) (Q : A → Prop) (f : A → B → B) (b : B) (l : list A) : P b → Forall Q l → (∀ a b, Q a → P b → P (f a b)) → P (foldr f b l).
Lemma foldr_ind_set {A B} (P : B → Set) (Q : A → Set) (f : A → B → B) (b : B) (l : list A) : P b → foldr (prod ∘ Q) True l → (∀ a b, Q a → P b → P (f a b)) → P (foldr f b l).
Lemma fold_left_ind {A B} (P : B → Prop) (Q : A → Prop) (f : B → A → B) (b : B) (l : list A) : P b → Forall Q l → (∀ a b, Q a → P b → P (f b a)) → P (fold_left f l b).
Lemma foldr_andb_equiv_foldr_conj {A : Type} (t : A → bool) (xs : list A) : foldr (fun c a ⇒ t c && a) true xs ↔ foldr (fun c a ⇒ (t c) = true ∧ a) True xs.
Lemma foldr_map {A B C : Type} (f : A → B → B) (g : C → A) (x : B) (xs : list C) : foldr f x (map g xs) = foldr (fun c a ⇒ f (g c) a) x xs.
(* Existing lemmas restated for Set. *)
Lemma set_choose_or_empty' `{FinSet A C} (X : C) : (sig (.∈ X)) + (X ≡ ∅).
Lemma set_ind' `{FinSet A C, !LeibnizEquiv C} (P : C → Set) :
P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Lemma set_fold_ind' {B} `{FinSet A C, !LeibnizEquiv C} (P : B → C → Set) (f : A → B → B) (b : B) :
P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
∀ X, P (set_fold f b X) X.
Lemma propset_top_elem_of {A}:
∀ S : propset A, S = ⊤ → ∀ t, t ∈ S.
From Coq Require Export ssreflect ssrfun ssrbool String.
From Coq.Logic Require Import Classical_Prop Classical_Pred_Type Eqdep_dec.
From stdpp Require Export list propset sets pmap gmap mapset coGset.
Export list. (* to overwrite module qualifiers *)
Lemma foldl_fold_left :
∀ {A B} f (l : list A) (b : B),
foldl f b l = fold_left f l b.
Fixpoint index_of_helper (x : string) (l : list string) (n : nat) : option nat :=
match l with
| [] ⇒ None
| y::ys ⇒ match string_dec x y with
| left _ ⇒ Some n
| right _ ⇒ index_of_helper x ys (S n)
end
end.
Definition index_of x l := index_of_helper x l 0.
Lemma decide_eq_same (A : Type) {dec : ∀ (t1 t2 : A), Decision (t1 = t2)} t:
decide (t = t) = left erefl.
Lemma pmap_to_list_lookup {A} (M : Pmap A) (i : positive) (x : A)
: (i,x) ∈ (map_to_list M) ↔ lookup i M = Some x.
(* Lemma gmap_to_list_lookup `{Countable K} {A} (M : gmap K A) (k : K) (a : A):
((k,a) ∈ (gmap_to_list M)) <-> (M !! k = Some a).
Proof.
unfold elem_of.
unfold lookup.
destruct M as PM PMwf eqn: HM. simpl.
unfold gmap_wf in PMwf.
split; intros H'.
+ apply pmap_to_list_lookup.
apply elem_of_list_omap in H'.
destruct H' as [k' a'] [HxinPM H'].
apply fmap_Some_1 in H'.
destruct H' as k'' [H1 H2]. inversion H2. subst. clear H2.
assert (Hk': k' = encode k'').
{ apply bool_decide_unpack in PMwf.
unfold map_Forall in PMwf.
apply pmap_to_list_lookup in HxinPM.
specialize (PMwf k' a' HxinPM).
apply (inj Some). rewrite <- PMwf.
apply fmap_Some_2. apply H1. }
subst. apply HxinPM.
+ apply pmap_to_list_lookup in H'.
apply elem_of_list_omap.
exists (encode k, a). firstorder.
rewrite -> decode_encode. simpl. reflexivity.
Qed. *)
#[global]
Program Instance inj_unit_r {K} : @Inj (K × ()) K (@eq (K × ())) (@eq K) (@fst K ()).
Lemma gset_to_list_elem_of `{Countable K} (S : gset K) (k : K) : k ∈ (mapset_elements S) ↔ k ∈ S.
Lemma mapset_elements_to_set `{Countable K} (X : gset K) : list_to_set (mapset_elements X) = X.
Lemma rev_tail_rev_app A (l : list A) (a : A) :
l ≠ [] → rev (tail (l ++ [a])) = a :: rev (tail l).
(* 1,2,3,4,5 -> 5,4,3,2,1 -> 4,3,2,1 -> 1,2,3,4 *)
Lemma rev_tail_rev_app_last A (l : list A) (xlast : A):
stdpp.list.last l = Some xlast →
(rev (tail (rev l)) ++ [xlast]) = l.
Lemma length_tail_zero A l: @length A (tail l) = 0 ↔ (@length A l = 0 ∨ @length A l = 1).
Lemma hd_error_app A (a b : A) (l : list A) :
hd_error ((l ++ [a]) ++ [b]) = hd_error (l ++ [a]).
Lemma last_rev_head A (l : list A) (x : A) : stdpp.list.last (x :: l) = hd_error (rev l ++ [x]).
(* The same lemma for stdpp's `reverse *)
Lemma last_reverse_head A (l : list A) (x : A) : stdpp.list.last (x :: l) = hd_error (reverse l ++ [x]).
Lemma hd_error_lookup A (l : list A) :
l !! 0 = hd_error l.
Lemma list_len_slice A (l1 l2 : list A) (a b : A) :
a :: l1 = l2 ++ [b] → length l1 = length l2.
Fixpoint skip_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :=
match l with
| nil ⇒ nil
| (x,y) :: xs ⇒
match (decide (x=y)) with
| left _ ⇒ @skip_eq _ eqdec xs
| right _ ⇒ l
end
end.
Lemma skip_eq_head_not_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :
∀ x y, hd_error (skip_eq l) = Some (x,y) → x ≠ y.
Definition tail_skip_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :=
reverse (skip_eq (reverse l)).
Lemma tail_skip_eq_last_not_eq {A} {eqdec: EqDecision A} (l : list (A × A)) :
∀ x y, stdpp.list.last (tail_skip_eq l) = Some (x, y) → x ≠ y.
Fixpoint common_length {A} {eqdec: EqDecision A} (l₁ l₂ : list A) :=
match l₁,l₂ with
| nil,nil ⇒ 0
| nil,_ ⇒ 0
| _,nil ⇒ 0
| (x::xs),(y::ys) ⇒
match (decide (x=y)) with
| left _ ⇒ S (@common_length _ eqdec xs ys)
| right _ ⇒ 0
end
end.
Lemma common_length_l_nil {A} {eqdec: EqDecision A} (l₁ : list A) :
common_length l₁ nil = 0.
Lemma common_length_sym {A} {eqdec: EqDecision A} (l₁ l₂ : list A) :
common_length l₁ l₂ = common_length l₂ l₁.
Lemma common_length_rev {A} {eqdec: EqDecision A} (x y : A) (xs ys : list A) :
common_length (reverse (x::xs)) (y::ys) =
match (decide ((stdpp.list.last (x::xs)) = Some y)) with
| left _ ⇒ S (common_length (reverse (tail (reverse (x::xs)))) ys)
| right _ ⇒ 0
end.
Lemma last_app_singleton {A} (m : A) (l : list A) :
stdpp.list.last (l ++ [m]) = Some m.
Lemma rev_reverse {A} (l : list A) :
rev l = reverse l.
Lemma forall_zip_flip {A B : Type} (f : A → B → Prop) (xs : list A) (ys: list B) :
Forall (uncurry f) (zip xs ys) ↔ Forall (uncurry (flip f)) (zip ys xs).
Lemma tail_app_nonempty {A : Type} (x : A) (xs ys : list A) :
tail ((x::xs) ++ ys) = (tail (x::xs)) ++ ys.
Lemma tail_app_nonempty' {A : Type} (xs ys : list A) :
length xs ≥ 1 →
tail (xs ++ ys) = (tail xs) ++ ys.
Lemma length_tail {A : Type} (l : list A) :
length (tail l) = length l - 1.
Lemma zip_smaller :
∀ {T1 T2} (l1 : list T1) (l2 : list T2), length l1 = length l2 →
∀ l3, zip l1 l2 = zip l1 (l2 ++ l3).
Lemma reverse_zip_tail_r {A : Type} (m : A) (l : list A) :
reverse (zip (m :: l) (tail (m :: l)))
= zip (tail (reverse (m :: l))) (reverse (m :: l)).
Lemma Forall_zip_flip_reverse {A : Type} (f : A → A → Prop) (m : A) (l : list A) :
Forall (uncurry f) (zip (m::l) (tail (m::l)))
↔
Forall (uncurry (flip f)) (zip (reverse (m::l)) (tail (reverse (m::l)))).
Lemma Forall_drop {A : Type} (P : A → Prop) (n : nat) (l : list A) :
Forall P l → Forall P (drop n l).
Lemma last_drop {A : Type} (l : list A) (n : nat) (x : A) :
stdpp.list.last l = Some x →
n < length l →
stdpp.list.last (drop n l) = Some x.
Lemma tail_drop {A : Type} (l : list A) (n : nat) :
tail (drop n l) = drop (S n) l.
Lemma drop_tail {A : Type} (l : list A) (n : nat) :
drop n (tail l) = drop (S n) l.
Lemma tail_drop_comm {A : Type} (l : list A) (n : nat) :
tail (drop n l) = drop n (tail l).
Lemma hd_drop_lookup {A : Type} (l : list A) (n : nat) (m : A) :
l !! n = Some m →
hd_error (drop n l) = Some m.
Lemma list_ex_elem {A : Type} (l : list A) (n : nat) :
n < length l → ∃ x, l!!n = Some x.
Lemma list_last_length {A : Type} (l : list A):
stdpp.list.last l = l !! (length l - 1).
Lemma equal_up_to_common_length {A : Type} {eqdec: EqDecision A} (l₁ l₂ : list A) :
∀ (n:nat),
n < common_length l₁ l₂ →
l₁ !! n = l₂ !! n.
Lemma last_tail {A : Type} (l : list A) (lst m : A) :
stdpp.list.last l = Some lst →
head (tail l) = Some m →
stdpp.list.last (tail l) = Some lst.
Lemma tail_zip_with {A B C : Type} (f : A → B → C) (l₁ : list A) (l₂ : list B) :
tail (zip_with f l₁ l₂) = zip_with f (tail l₁) (tail l₂).
Lemma tail_zip {A : Type} (l₁ l₂ : list A) :
tail (zip l₁ l₂) = zip (tail l₁) (tail l₂).
Lemma common_length_impl_eq {A : Type} {eqdec: EqDecision A} (l₁ l₂ : list A) :
length l₁ = length l₂ →
common_length l₁ l₂ = length l₂ →
l₁ = l₂.
Lemma not_elem_of_larger_impl_not_elem_of {A C : Type} {H : ElemOf A C} (x : A) (S B : C) :
S ⊆ B →
x ∉ B →
x ∉ S.
Tactic Notation "solve_set_inclusion" int_or_var(depth) :=
apply elem_of_subseteq;
let x := fresh "x" in
let H := fresh "Hxin" in
(* TODO: maybe we need something like: *)
(*rewrite -!union_assoc_L.*)
(* We may also want to remove duplicates, at least those that are neighbors *)
intros x H;
repeat (
match H with
| ?L ∧ ?R ⇒ fail "Not implemented: destruct H"
| _ ⇒ eauto depth using @sets.elem_of_union_l, @sets.elem_of_union_r with typeclass_instances
end
).
Lemma map_take {A B : Type} (f : A → B) (l : list A) (n : nat) :
map f (take n l) = take n (map f l).
Lemma map_drop {A B : Type} (f : A → B) (l : list A) (n : nat) :
map f (drop n l) = drop n (map f l).
Lemma foldr_andb_true_take n l:
foldr andb true l →
foldr andb true (take n l).
Lemma foldr_andb_true_drop n l:
foldr andb true l →
foldr andb true (drop n l).
Definition propset_fa_union {T C : Type} (f : C → propset T) : propset T
:= PropSet (fun (x : T) ⇒ ∃ (c : C), x ∈ f c).
Lemma propset_fa_union_same {T C : Type} {LE : LeibnizEquiv (propset T)} (f f' : C → propset T):
(∀ c, (f c) = (f' c)) →
(propset_fa_union f) = (propset_fa_union f').
Global Instance propset_fa_union_proper {T C : Type}
: Proper (pointwise_relation C (≡) ==> (≡)) (@propset_fa_union T C).
Lemma propset_fa_union_empty {T C : Type} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_union f = ∅) ↔ (∀ (c : C), (f c) = ∅).
Lemma propset_fa_union_full {T C : Type} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_union f = ⊤) ↔ (∀ (t : T), ∃ (c : C), t ∈ (f c)).
Lemma propset_fa_union_included : ∀ T C : Type, ∀ f f' : C → propset T,
(∀ c, (f c) ⊆ (f' c)) →
(propset_fa_union f) ⊆ (propset_fa_union f').
Definition propset_fa_intersection {T C : Type} (f : C → propset T) : propset T
:= PropSet (fun (x : T) ⇒ ∀ (c : C), x ∈ f c).
Lemma propset_fa_intersection_empty {T C : Type} {INH : Inhabited C} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_intersection f = ∅) ↔ (∀ (t : T), ∃ (c : C), t ∉ (f c)).
Lemma propset_fa_intersection_full {T C : Type} {LE : LeibnizEquiv (propset T)} (f : C → propset T) :
(propset_fa_intersection f = ⊤) ↔ (∀ (c : C), (f c) = ⊤).
Lemma Not_Empty_Contains_Elements {T : Type} {LE : LeibnizEquiv (propset T)} (S : propset T):
S ≠ ∅ → ∃ x : T, x ∈ S.
Lemma Contains_Elements_Not_Empty {T : Type} (S : propset T):
(∃ x : T, x ∈ S) → S ≠ ∅.
Lemma Not_Empty_iff_Contains_Elements {T : Type} {LE : LeibnizEquiv (propset T)} (S : propset T):
S ≠ ∅ ↔
∃ x : T, x ∈ S.
Lemma Compl_Compl_propset {T : Type} {LE : LeibnizEquiv (propset T)} (A : propset T):
(⊤ ∖ (⊤ ∖ A)) = A.
Lemma Compl_Union_Compl_Inters_propset_alt {T : Type} {LE : LeibnizEquiv (propset T)} (L R : propset T):
(⊤ ∖ ((⊤ ∖ L) ∪ (⊤ ∖ R))) = (L ∩ R).
Lemma complement_full_iff_empty {T : Type} {LE : LeibnizEquiv (propset T)} (A : propset T):
(⊤ ∖ A = ⊤) ↔ (A = ∅).
Lemma complement_empty_iff_full {T : Type} {LE : LeibnizEquiv (propset T)} (A : propset T):
(⊤ ∖ A = ∅) ↔ (A = ⊤).
Lemma intersection_full_iff_both_full {T : Type} {LE : LeibnizEquiv (propset T)} (L R : propset T):
(L ∩ R = ⊤) ↔ (L = ⊤ ∧ R = ⊤).
Lemma union_with_complement {T : Type} {LE : LeibnizEquiv (propset T)} (X : propset T):
(⊤ ∖ X) ∪ X = ⊤.
Lemma elem_of_compl {T : Type} {LE : LeibnizEquiv (propset T)} (X : propset T) (x : T):
(x ∈ (⊤ ∖ X)) ↔ (x ∉ X).
Lemma elem_of_singleton_sym
{A C : Type} {H : ElemOf A C} {H0 : Empty C} {H1 : Singleton A C}
{H2 : Union C} {H3 : SemiSet A C} :
∀ (x y : A), x ∈ (@singleton A C H1 y) ↔ y ∈ (@singleton A C H1 x).
Global Instance set_unfold_gset_to_coGset
{A : Type} {_eqA : EqDecision A} {_cntA : Countable A} (x : A) (X : @gmap.gset A _eqA _cntA) P
:
SetUnfoldElemOf x X P →
SetUnfoldElemOf x (gset_to_coGset X) P.
Lemma foldr_ind {A B} (P : B → Prop) (Q : A → Prop) (f : A → B → B) (b : B) (l : list A) : P b → Forall Q l → (∀ a b, Q a → P b → P (f a b)) → P (foldr f b l).
Lemma foldr_ind_set {A B} (P : B → Set) (Q : A → Set) (f : A → B → B) (b : B) (l : list A) : P b → foldr (prod ∘ Q) True l → (∀ a b, Q a → P b → P (f a b)) → P (foldr f b l).
Lemma fold_left_ind {A B} (P : B → Prop) (Q : A → Prop) (f : B → A → B) (b : B) (l : list A) : P b → Forall Q l → (∀ a b, Q a → P b → P (f b a)) → P (fold_left f l b).
Lemma foldr_andb_equiv_foldr_conj {A : Type} (t : A → bool) (xs : list A) : foldr (fun c a ⇒ t c && a) true xs ↔ foldr (fun c a ⇒ (t c) = true ∧ a) True xs.
Lemma foldr_map {A B C : Type} (f : A → B → B) (g : C → A) (x : B) (xs : list C) : foldr f x (map g xs) = foldr (fun c a ⇒ f (g c) a) x xs.
(* Existing lemmas restated for Set. *)
Lemma set_choose_or_empty' `{FinSet A C} (X : C) : (sig (.∈ X)) + (X ≡ ∅).
Lemma set_ind' `{FinSet A C, !LeibnizEquiv C} (P : C → Set) :
P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Lemma set_fold_ind' {B} `{FinSet A C, !LeibnizEquiv C} (P : B → C → Set) (f : A → B → B) (b : B) :
P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
∀ X, P (set_fold f b X) X.
Lemma propset_top_elem_of {A}:
∀ S : propset A, S = ⊤ → ∀ t, t ∈ S.
This page has been generated by coqdoc