Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision

Target

Select target project
  • iris/stdpp
  • johannes/stdpp
  • proux1/stdpp
  • dosualdo/stdpp
  • benoit/coq-stdpp
  • dfrumin/coq-stdpp
  • haidang/stdpp
  • amintimany/coq-stdpp
  • swasey/coq-stdpp
  • simongregersen/stdpp
  • proux/stdpp
  • janno/coq-stdpp
  • amaurremi/coq-stdpp
  • msammler/stdpp
  • tchajed/stdpp
  • YaZko/stdpp
  • maximedenes/stdpp
  • jakobbotsch/stdpp
  • Blaisorblade/stdpp
  • simonspies/stdpp
  • lepigre/stdpp
  • devilhena/stdpp
  • simonfv/stdpp
  • jihgfee/stdpp
  • snyke7/stdpp
  • Armael/stdpp
  • gmalecha/stdpp
  • olaure01/stdpp
  • sarahzrf/stdpp
  • atrieu/stdpp
  • herbelin/stdpp
  • arthuraa/stdpp
  • lgaeher/stdpp
  • mrhaandi/stdpp
  • mattam82/stdpp
  • Quarkbeast/stdpp
  • aa755/stdpp
  • gmevel/stdpp
  • lstefane/stdpp
  • jung/stdpp
  • vsiles/stdpp
  • dlesbre/stdpp
  • bergwerf/stdpp
  • marijnvanwezel/stdpp
  • ivanbakel/stdpp
  • tperami/stdpp
  • adamAndMath/stdpp
  • Villetaneuse/stdpp
  • sanjit/stdpp
  • yiyunliu/stdpp
  • thomas-lamiaux/stdpp
  • Tragicus/stdpp
  • kbedarka/stdpp
53 results
Select Git revision
Show changes
......@@ -177,6 +177,25 @@ Proof.
- simpl. by rewrite dom_insert, IH.
Qed.
Lemma map_first_key_dom {A B} (m1 : M A) (m2 : M B) i :
dom m1 dom m2 map_first_key m1 i map_first_key m2 i.
Proof.
intros Hm. apply map_first_key_dom'. intros j.
by rewrite <-!elem_of_dom, Hm.
Qed.
Lemma map_first_key_dom_L {A B} (m1 : M A) (m2 : M B) i :
dom m1 = dom m2 map_first_key m1 i map_first_key m2 i.
Proof. intros Hm. apply map_first_key_dom. by rewrite Hm. Qed.
Lemma map_Forall2_dom {A B} (P : K A B Prop) (m1 : M A) (m2 : M B) :
map_Forall2 P m1 m2 dom m1 dom m2.
Proof.
revert m2. induction m1 as [|i x1 m1 ? IH] using map_ind; intros m2.
{ intros ->%map_Forall2_empty_inv_l. by rewrite !dom_empty. }
intros (x2 & m2' & -> & ? & ? & ?)%map_Forall2_insert_inv_l; last done.
by rewrite !dom_insert, IH by done.
Qed.
(** Alternative definition of [dom] in terms of [map_to_list]. *)
Lemma dom_alt {A} (m : M A) :
dom m list_to_set (map_to_list m).*1.
......@@ -314,6 +333,7 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Section leibniz.
Context `{!LeibnizEquiv D}.
Lemma dom_filter_L {A} (P : K * A Prop) `{!∀ x, Decision (P x)} (m : M A) X :
( i, i X x, m !! i = Some x P (i, x))
dom (filter P m) = X.
......@@ -348,6 +368,9 @@ Section leibniz.
Proof. unfold_leibniz; apply dom_difference. Qed.
Lemma dom_fmap_L {A B} (f : A B) (m : M A) : dom (f <$> m) = dom m.
Proof. unfold_leibniz; apply dom_fmap. Qed.
Lemma map_Forall2_dom_L {A B} (P : K A B Prop) (m1 : M A) (m2 : M B) :
map_Forall2 P m1 m2 dom m1 = dom m2.
Proof. unfold_leibniz. apply map_Forall2_dom. Qed.
Lemma dom_imap_L {A B} (f: K A option B) (m: M A) X :
( i, i X x, m !! i = Some x is_Some (f i x))
dom (map_imap f m) = X.
......
This diff is collapsed.
......@@ -194,7 +194,7 @@ Qed.
Lemma size_union X Y : X ## Y size (X Y) = size X + size Y.
Proof.
intros. unfold size, set_size. simpl. rewrite <-app_length.
intros. unfold size, set_size. simpl. rewrite <-length_app.
apply Permutation_length, NoDup_Permutation.
- apply NoDup_elements.
- apply NoDup_app; repeat split; try apply NoDup_elements.
......@@ -298,28 +298,112 @@ Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
Lemma set_fold_singleton {B} (f : A B B) (b : B) (a : A) :
set_fold f b ({[a]} : C) = f a b.
Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
(** The following lemma shows that folding over two sets separately (using the
result of the first fold as input for the second fold) is equivalent to folding
over the union, *if* the function is idempotent for the elements that will be
processed twice ([X ∩ Y]) and does not care about the order in which elements
are processed.
This is a generalization of [set_fold_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
Lemma set_fold_union_strong {B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) X Y :
( x, Proper (R ==> R) (f x))
( x b',
(** This is morally idempotence for elements of [X ∩ Y] *)
x X Y
(** We cannot write this in the usual direction of idempotence properties
(i.e., [R (f x (f x b'))) (f x b')]) because [R] is not symmetric. *)
R (f x b') (f x (f x b')))
( x1 x2 b',
(** This is morally commutativity + associativity for elements of [X ∪ Y] *)
x1 X Y x2 X Y x1 x2
R (f x1 (f x2 b')) (f x2 (f x1 b')))
X ## Y
R (set_fold f b (X Y)) (set_fold f (set_fold f b X) Y).
Proof.
intros ? Hf Hdisj. unfold set_fold; simpl.
rewrite <-foldr_app. apply (foldr_permutation R f b).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf.
(** This lengthy proof involves various steps by transitivity of [R].
Roughly, we show that the LHS is related to folding over:
elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y)
and the RHS is related to folding over:
elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∩ Y) ++ elements (Y ∖ X)
These steps are justified by lemma [foldr_permutation]. In the middle we
remove the repeated folding over [elements (X ∩ Y)] using [foldr_idemp_strong].
Most of the proof work concerns the side conditions of [foldr_permutation]
and [foldr_idemp_strong], which require relating results about lists and
sets. *)
intros ?.
assert ( b1 b2 l, R b1 b2 R (foldr f b1 l) (foldr f b2 l)) as Hff.
{ intros b1 b2 l Hb. induction l as [|x l]; simpl; [done|]. by f_equiv. }
intros Hfidemp Hfcomm. unfold set_fold; simpl.
trans (foldr f b (elements (Y X) ++ elements (X Y) ++ elements (X Y))).
{ apply (foldr_permutation R f b).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. pose proof (NoDup_elements (X Y)).
by eapply Hj, NoDup_lookup.
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x X)), (decide (x Y)); set_solver. }
trans (foldr f (foldr f b (elements (X Y) ++ elements (X Y)))
(elements (Y X) ++ elements (X Y))).
{ rewrite !foldr_app. apply Hff. apply (foldr_idemp_strong (flip R)).
- solve_proper.
- intros j a b' ?%elem_of_list_lookup_2. apply Hfidemp. set_solver.
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ intros ->. pose proof (NoDup_elements (X Y)).
by eapply Hj, NoDup_lookup. }
trans (foldr f (foldr f b (elements (X Y) ++ elements (X Y))) (elements Y)).
{ apply (foldr_permutation R f _).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. assert (NoDup (elements (Y X) ++ elements (X Y))).
{ rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
by eapply Hj, NoDup_lookup.
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x X)); set_solver. }
apply Hff. apply (foldr_permutation R f _).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. pose proof (NoDup_elements (X Y)).
+ intros ->. assert (NoDup (elements (X Y) ++ elements (X Y))).
{ rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
by eapply Hj, NoDup_lookup.
- by rewrite elements_disj_union, (comm (++)).
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x Y)); set_solver.
Qed.
Lemma set_fold_union (f : A A A) (b : A) X Y :
IdemP (=) f
Comm (=) f
Assoc (=) f
set_fold f b (X Y) = set_fold f (set_fold f b X) Y.
Proof.
intros. apply (set_fold_union_strong _ _ _ _ _ _).
- intros x b' _. by rewrite (assoc_L f), (idemp f).
- intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
Qed.
(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) X Y :
( x, Proper (R ==> R) (f x))
( x1 x2 b',
(** This is morally commutativity + associativity for elements of [X ∪ Y] *)
x1 X Y x2 X Y x1 x2
R (f x1 (f x2 b')) (f x2 (f x1 b')))
X ## Y
R (set_fold f b (X Y)) (set_fold f (set_fold f b X) Y).
Proof. intros. apply set_fold_union_strong; set_solver. Qed.
Lemma set_fold_disj_union (f : A A A) (b : A) X Y :
Comm (=) f
Assoc (=) f
......@@ -345,7 +429,7 @@ Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
(** * Minimal elements *)
Lemma minimal_exists R `{!Transitive R, x y, Decision (R x y)} (X : C) :
Lemma minimal_exists_elem_of R `{!Transitive R, x y, Decision (R x y)} (X : C) :
X x, x X minimal R x X.
Proof.
pattern X; apply set_ind; clear X.
......@@ -361,10 +445,20 @@ Proof.
exists x; split; [set_solver|].
rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
x y, Decision (R x y)} (X : C) :
X x, x X minimal R x X.
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
Lemma minimal_exists R `{!Transitive R,
x y, Decision (R x y)} `{!Inhabited A} (X : C) :
x, minimal R x X.
Proof.
destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
- edestruct (minimal_exists_elem_of R X) as (x & Hel & Hmin); first set_solver.
exists x. done.
- exists inhabitant. intros y Hel. set_solver.
Qed.
(** * Filter *)
Lemma elem_of_filter (P : A Prop) `{!∀ x, Decision (P x)} X x :
......@@ -701,7 +795,7 @@ Section infinite.
Forall_fresh X xs Y X Forall_fresh Y xs.
Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
Lemma fresh_list_length n X : length (fresh_list n X) = n.
Lemma length_fresh_list n X : length (fresh_list n X) = n.
Proof. revert X. induction n; simpl; auto. Qed.
Lemma fresh_list_is_fresh n X x : x fresh_list n X x X.
Proof.
......@@ -726,5 +820,5 @@ Lemma size_set_seq `{FinSet nat C} start len :
Proof.
rewrite <-list_to_set_seq, size_list_to_set.
2:{ apply NoDup_seq. }
rewrite seq_length. done.
rewrite length_seq. done.
Qed.
......@@ -120,7 +120,7 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
Proof.
intros. apply submseteq_length_Permutation.
- by apply finite_inj_submseteq.
- rewrite fmap_length. by apply Nat.eq_le_incl.
- rewrite length_fmap. by apply Nat.eq_le_incl.
Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A B)
`{!Inj (=) (=) f} : card A = card B Surj (=) f.
......@@ -146,7 +146,7 @@ Proof.
{ exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
- intros [f ?]. unfold card. rewrite <-(fmap_length f).
- intros [f ?]. unfold card. rewrite <-(length_fmap f).
by apply submseteq_length, (finite_inj_submseteq f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
......@@ -216,7 +216,7 @@ Section enc_finite.
split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
Qed.
Lemma enc_finite_card : card A = c.
Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
Proof. unfold card. simpl. by rewrite length_fmap, length_seq. Qed.
End enc_finite.
(** If we have a surjection [f : A → B] and [A] is finite, then [B] is finite
......@@ -262,7 +262,7 @@ Next Obligation.
apply elem_of_list_fmap. eauto using elem_of_enum.
Qed.
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite fmap_length. Qed.
Proof. unfold card. simpl. by rewrite length_fmap. Qed.
Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
......@@ -297,7 +297,7 @@ Next Obligation.
[left|right]; (eexists; split; [done|apply elem_of_enum]).
Qed.
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
Proof. unfold card. simpl. by rewrite length_app, !length_fmap. Qed.
Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := a enum A; (a,.) <$> enum B |}.
......@@ -315,7 +315,7 @@ Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
unfold card; simpl. induction (enum A); simpl; auto.
rewrite app_length, fmap_length. auto.
rewrite length_app, length_fmap. auto.
Qed.
Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
......@@ -343,18 +343,18 @@ Proof.
unfold card; simpl. induction n as [|n IH]; simpl; [done|].
rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
by rewrite app_length, fmap_length, IH.
by rewrite length_app, length_fmap, IH.
Qed.
Global Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
Proof.
refine (bijective_finite (λ v : vec A n, vec_to_list v vec_to_list_length _)).
refine (bijective_finite (λ v : vec A n, vec_to_list v length_vec_to_list _)).
- abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
- abstract (intros [l <-]; exists (list_to_vec l);
apply (sig_eq_pi _), vec_to_list_to_vec).
Defined.
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Proof. unfold card; simpl. rewrite fmap_length. apply vec_card. Qed.
Proof. unfold card; simpl. rewrite length_fmap. apply vec_card. Qed.
Fixpoint fin_enum (n : nat) : list (fin n) :=
match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
......@@ -369,7 +369,7 @@ Next Obligation.
rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
Qed.
Lemma fin_card n : card (fin n) = n.
Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
Proof. unfold card; simpl. induction n; simpl; rewrite ?length_fmap; auto. Qed.
(* shouldn’t be an instance (cycle with [sig_finite]): *)
Lemma finite_sig_dec `{!EqDecision A} (P : A Prop) `{Finite (sig P)} x :
......@@ -415,7 +415,7 @@ Section sig_finite.
split; [by destruct p | apply elem_of_enum].
Qed.
Lemma sig_card : card (sig P) = length (filter P (enum A)).
Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
Proof. by rewrite <-list_filter_sig_filter, length_fmap. Qed.
End sig_finite.
Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A B) :
......
......@@ -63,6 +63,7 @@ Global Arguments GNodes {A P} _.
Record gmap_key K `{Countable K} (q : positive) :=
GMapKey { _ : encode (A:=K) <$> decode q = Some q }.
Add Printing Constructor gmap_key.
Global Arguments GMapKey {_ _ _ _} _.
Lemma gmap_key_encode `{Countable K} (k : K) : gmap_key K (encode k).
......@@ -71,6 +72,7 @@ Global Instance gmap_key_pi `{Countable K} q : ProofIrrel (gmap_key K q).
Proof. intros [?] [?]. f_equal. apply (proof_irrel _). Qed.
Record gmap K `{Countable K} A := GMap { gmap_car : gmap_dep A (gmap_key K) }.
Add Printing Constructor gmap.
Global Arguments GMap {_ _ _ _} _.
Global Arguments gmap_car {_ _ _ _} _.
......@@ -442,45 +444,68 @@ Section gmap_merge.
Qed.
End gmap_merge.
Section gmap_fold.
Context {A B} (f : positive A B B).
Local Lemma gmap_dep_fold_GNode {P} i y (ml : gmap_dep A P~0) mx mr :
GNode_valid ml mx mr
gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
(gmap_dep_fold f i~0
match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
Proof. by destruct ml, mx as [[]|], mr. Qed.
Local Lemma gmap_dep_fold_GNode {A B} (f : positive A B B)
{P} i y (ml : gmap_dep A P~0) mx mr :
gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
(gmap_dep_fold f i~0
match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
Proof. by destruct ml, mx as [[]|], mr. Qed.
Local Lemma gmap_dep_fold_ind {P} (Q : B gmap_dep A P Prop) (b : B) j :
Q b GEmpty
( i p x mt r, gmap_dep_lookup i mt = None
Q r mt
Q (f (Pos.reverse_go i j) x r) (gmap_dep_partial_alter (λ _, Some x) i p mt))
mt, Q (gmap_dep_fold f j b mt) mt.
Proof.
intros Hemp Hinsert mt. revert Q b j Hemp Hinsert.
induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
intros Q b j Hemp Hinsert; [done|].
rewrite gmap_dep_fold_GNode by done.
apply (IHr (λ y mt, Q y (GNode ml mx mt))).
{ apply (IHl (λ y mt, Q y (GNode mt mx GEmpty))).
{ destruct mx as [[p x]|]; [|done].
replace (GNode GEmpty (Some (p,x)) GEmpty) with
(gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
by apply Hinsert. }
intros i p x mt r ??.
replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
Local Lemma gmap_dep_fold_ind {A} {P} (Q : gmap_dep A P Prop) :
Q GEmpty
( i p x mt,
gmap_dep_lookup i mt = None
( j A' B (f : positive A' B B) (g : A A') b x',
gmap_dep_fold f j b
(gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
= f (Pos.reverse_go i j) x' (gmap_dep_fold f j b (gmap_dep_fmap g mt)))
Q mt Q (gmap_dep_partial_alter (λ _, Some x) i p mt))
mt, Q mt.
Proof.
intros Hemp Hinsert mt. revert Q Hemp Hinsert.
induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
intros Q Hemp Hinsert; [done|].
apply (IHr (λ mt, Q (GNode ml mx mt))).
{ apply (IHl (λ mt, Q (GNode mt mx GEmpty))).
{ destruct mx as [[p x]|]; [|done].
replace (GNode GEmpty (Some (p,x)) GEmpty) with
(gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
by apply Hinsert. }
intros i p x mt r ? Hfold.
replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
by (by destruct mt, mx as [[]|]).
apply Hinsert.
- by rewrite gmap_dep_lookup_GNode.
- intros j A' B f g b x'.
replace (gmap_dep_partial_alter (λ _, Some x') (i~0) p
(gmap_dep_fmap g (GNode mt mx GEmpty)))
with (GNode (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
(prod_map id g <$> mx) GEmpty)
by (by destruct mt, mx as [[]|]).
replace (gmap_dep_fmap g (GNode mt mx GEmpty))
with (GNode (gmap_dep_fmap g mt) (prod_map id g <$> mx) GEmpty)
by (by destruct mt, mx as [[]|]).
apply Hinsert; by rewrite ?gmap_dep_lookup_GNode. }
intros i p x mt r ??.
replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
rewrite !gmap_dep_fold_GNode; simpl; auto.
- done. }
intros i p x mt r ? Hfold.
replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
by (by destruct ml, mx as [[]|], mt).
apply Hinsert.
- by rewrite gmap_dep_lookup_GNode.
- intros j A' B f g b x'.
replace (gmap_dep_partial_alter (λ _, Some x') (i~1) p
(gmap_dep_fmap g (GNode ml mx mt)))
with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx)
(gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt)))
by (by destruct ml, mx as [[]|], mt).
apply Hinsert; by rewrite ?gmap_dep_lookup_GNode.
Qed.
End gmap_fold.
replace (gmap_dep_fmap g (GNode ml mx mt))
with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx) (gmap_dep_fmap g mt))
by (by destruct ml, mx as [[]|], mt).
rewrite !gmap_dep_fold_GNode; simpl; auto.
- done.
Qed.
(** Instance of the finite map type class *)
Global Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
......@@ -494,11 +519,16 @@ Proof.
- intros A b f [mt] i. apply gmap_dep_lookup_fmap.
- intros A B f [mt] i. apply gmap_dep_lookup_omap.
- intros A B C f [mt1] [mt2] i. apply gmap_dep_lookup_merge.
- intros A B P f b Hemp Hinsert [mt].
apply (gmap_dep_fold_ind _ (λ r mt, P r (GMap mt))); clear mt; [done|].
intros i [Hk] x mt r ??; simpl. destruct (fmap_Some_1 _ _ _ Hk) as (k&->&->).
assert (GMapKey Hk = gmap_key_encode k) as -> by (apply proof_irrel).
by apply (Hinsert _ _ (GMap mt)).
- done.
- intros A P Hemp Hins [mt].
apply (gmap_dep_fold_ind (λ mt, P (GMap mt))); clear mt; [done|].
intros i [Hk] x mt ? Hfold. destruct (fmap_Some_1 _ _ _ Hk) as (k&Hk'&->).
assert (GMapKey Hk = gmap_key_encode k) as Hkk by (apply proof_irrel).
rewrite Hkk in Hfold |- *. clear Hk Hkk.
apply (Hins k x (GMap mt)); [done|]. intros A' B f g b x'.
trans ((match decode (encode k) with Some k => f k x' | None => id end)
(map_fold f b (g <$> GMap mt))); [apply (Hfold 1)|].
by rewrite Hk'.
Qed.
Global Program Instance gmap_countable
......@@ -581,10 +611,10 @@ Section curry_uncurry.
Lemma lookup_gmap_uncurry (m : gmap K1 (gmap K2 A)) i j :
gmap_uncurry m !! (i,j) = m !! i ≫= (.!! j).
Proof.
apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
apply (map_fold_weak_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
{ by rewrite !lookup_empty. }
clear m; intros i' m2 m m12 Hi' IH.
apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
apply (map_fold_weak_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
{ rewrite IH. destruct (decide (i' = i)) as [->|].
- rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
- by rewrite lookup_insert_ne by done. }
......@@ -598,7 +628,7 @@ Section curry_uncurry.
Lemma lookup_gmap_curry (m : gmap (K1 * K2) A) i j :
gmap_curry m !! i ≫= (.!! j) = m !! (i, j).
Proof.
apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
apply (map_fold_weak_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
{ by rewrite !lookup_empty. }
clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|].
......@@ -611,8 +641,8 @@ Section curry_uncurry.
Lemma lookup_gmap_curry_None (m : gmap (K1 * K2) A) i :
gmap_curry m !! i = None ( j, m !! (i, j) = None).
Proof.
apply (map_fold_ind (λ mr m, mr !! i = None ( j, m !! (i, j) = None)));
[done|].
apply (map_fold_weak_ind
(λ mr m, mr !! i = None ( j, m !! (i, j) = None))); [done|].
clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|].
- split; [by rewrite lookup_partial_alter|].
......@@ -793,4 +823,25 @@ Section gset.
Qed.
End gset.
Section gset_cprod.
Context `{Countable A, Countable B}.
Global Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) :=
λ X Y, set_bind (λ e1, set_map (e1,.) Y) X.
Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :
x cprod X Y x.1 X x.2 Y.
Proof. unfold cprod, gset_cprod. destruct x. set_solver. Qed.
Global Instance set_unfold_gset_cprod (X : gset A) (Y : gset B) x (P : Prop) Q :
SetUnfoldElemOf x.1 X P SetUnfoldElemOf x.2 Y Q
SetUnfoldElemOf x (cprod X Y) (P Q).
Proof using.
intros ??; constructor.
by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 X P),
(set_unfold_elem_of x.2 Y Q).
Qed.
End gset_cprod.
Global Typeclasses Opaque gset.
......@@ -61,12 +61,19 @@ Section definitions.
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
let (X) := X in dom X.
Definition gmultiset_map `{Countable B} (f : A B)
(X : gmultiset A) : gmultiset B :=
GMultiSet $ map_fold
(λ x n, partial_alter (Some from_option (Pos.add n) n) (f x))
(gmultiset_car X).
End definitions.
Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom gmultiset_map.
Section basic_lemmas.
Context `{Countable A}.
......@@ -152,6 +159,13 @@ Section basic_lemmas.
Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
Lemma gmultiset_elem_of_dom x X : x dom X x X.
Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver lia.
Qed.
End basic_lemmas.
(** * A solver for multisets *)
......@@ -292,6 +306,9 @@ Section multiset_unfold.
intros ??; constructor. rewrite gmultiset_elem_of_intersection.
by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
Global Instance set_unfold_gmultiset_dom x X :
SetUnfoldElemOf x (dom X) (x X).
Proof. constructor. apply gmultiset_elem_of_dom. Qed.
End multiset_unfold.
(** Step 3: instantiate hypotheses *)
......@@ -485,6 +502,9 @@ Section more_lemmas.
Global Instance list_to_set_disj_perm :
Proper (() ==> (=)) (list_to_set_disj (C:=gmultiset A)).
Proof. induction 1; multiset_solver. Qed.
Lemma list_to_set_disj_replicate n x :
list_to_set_disj (replicate n x) =@{gmultiset A} n *: {[+ x +]}.
Proof. induction n; multiset_solver. Qed.
(** Properties of the elements operation *)
Lemma gmultiset_elements_empty : elements ( : gmultiset A) = [].
......@@ -544,12 +564,6 @@ Section more_lemmas.
exists (x,n); split; [|by apply elem_of_map_to_list].
apply elem_of_replicate; auto with lia.
Qed.
Lemma gmultiset_elem_of_dom x X : x dom X x X.
Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver lia.
Qed.
(** Properties of the set_fold operation *)
Lemma gmultiset_set_fold_empty {B} (f : A B B) (b : B) :
......@@ -640,7 +654,7 @@ Section more_lemmas.
Lemma gmultiset_size_disj_union X Y : size (X Y) = size X + size Y.
Proof.
unfold size, gmultiset_size; simpl.
by rewrite gmultiset_elements_disj_union, app_length.
by rewrite gmultiset_elements_disj_union, length_app.
Qed.
Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n * size X.
Proof.
......@@ -655,15 +669,17 @@ Section more_lemmas.
Local Lemma gmultiset_subseteq_alt X Y :
X Y
map_relation Pos.le (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
map_relation (λ _, Pos.le) (λ _ _, False) (λ _ _, True)
(gmultiset_car X) (gmultiset_car Y).
Proof.
apply forall_proper; intros x. unfold multiplicity.
destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
Qed.
Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
Proof.
refine (λ X Y, cast_if (decide (map_relation Pos.le
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
refine (λ X Y, cast_if (decide (map_relation
(λ _, Pos.le) (λ _ _, False) (λ _ _, True)
(gmultiset_car X) (gmultiset_car Y))));
by rewrite gmultiset_subseteq_alt.
Defined.
......@@ -774,3 +790,120 @@ Section more_lemmas.
apply Hinsert, IH; multiset_solver.
Qed.
End more_lemmas.
(** * Map *)
Section map.
Context `{Countable A, Countable B}.
Context (f : A B).
Lemma gmultiset_map_alt X :
gmultiset_map f X = list_to_set_disj (f <$> elements X).
Proof.
destruct X as [m]. unfold elements, gmultiset_map. simpl.
induction m as [|x n m ?? IH] using map_first_key_ind; [done|].
rewrite map_to_list_insert_first_key, map_fold_insert_first_key by done.
csimpl. rewrite fmap_app, fmap_replicate, list_to_set_disj_app, <-IH.
apply gmultiset_eq; intros y.
rewrite multiplicity_disj_union, list_to_set_disj_replicate.
rewrite multiplicity_scalar_mul, multiplicity_singleton'.
unfold multiplicity; simpl. destruct (decide (y = f x)) as [->|].
- rewrite lookup_partial_alter; simpl. destruct (_ !! f x); simpl; lia.
- rewrite lookup_partial_alter_ne by done. lia.
Qed.
Lemma gmultiset_map_empty : gmultiset_map f = ∅.
Proof. done. Qed.
Lemma gmultiset_map_disj_union X Y :
gmultiset_map f (X Y) = gmultiset_map f X gmultiset_map f Y.
Proof.
apply gmultiset_eq; intros x.
rewrite !gmultiset_map_alt, gmultiset_elements_disj_union, fmap_app.
by rewrite list_to_set_disj_app.
Qed.
Lemma gmultiset_map_singleton x :
gmultiset_map f {[+ x +]} = {[+ f x +]}.
Proof.
rewrite gmultiset_map_alt, gmultiset_elements_singleton.
multiset_solver.
Qed.
Lemma elem_of_gmultiset_map X y :
y gmultiset_map f X x, y = f x x X.
Proof.
rewrite gmultiset_map_alt, elem_of_list_to_set_disj, elem_of_list_fmap.
by setoid_rewrite gmultiset_elem_of_elements.
Qed.
Lemma multiplicity_gmultiset_map X x :
Inj (=) (=) f
multiplicity (f x) (gmultiset_map f X) = multiplicity x X.
Proof.
intros. induction X as [|y X IH] using gmultiset_ind; [multiset_solver|].
rewrite gmultiset_map_disj_union, gmultiset_map_singleton,
!multiplicity_disj_union.
multiset_solver.
Qed.
Global Instance gmultiset_map_inj :
Inj (=) (=) f Inj (=) (=) (gmultiset_map f).
Proof.
intros ? X Y HXY. apply gmultiset_eq; intros x.
by rewrite <-!(multiplicity_gmultiset_map _ _ _), HXY.
Qed.
Global Instance set_unfold_gmultiset_map X (P : A Prop) y :
( x, SetUnfoldElemOf x X (P x))
SetUnfoldElemOf y (gmultiset_map f X) ( x, y = f x P x).
Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed.
Global Instance multiset_unfold_map x X n :
Inj (=) (=) f
MultisetUnfold x X n
MultisetUnfold (f x) (gmultiset_map f X) n.
Proof.
intros ? [HX]; constructor. by rewrite multiplicity_gmultiset_map, HX.
Qed.
End map.
(** * Big disjoint unions *)
Section disj_union_list.
Context `{Countable A}.
Implicit Types X Y : gmultiset A.
Implicit Types Xs Ys : list (gmultiset A).
Lemma gmultiset_disj_union_list_nil :
⋃+ (@nil (gmultiset A)) = ∅.
Proof. done. Qed.
Lemma gmultiset_disj_union_list_cons X Xs :
⋃+ (X :: Xs) = X ⋃+ Xs.
Proof. done. Qed.
Lemma gmultiset_disj_union_list_singleton X :
⋃+ [X] = X.
Proof. simpl. by rewrite (right_id_L _). Qed.
Lemma gmultiset_disj_union_list_app Xs1 Xs2 :
⋃+ (Xs1 ++ Xs2) = ⋃+ Xs1 ⋃+ Xs2.
Proof.
induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id_L _)|].
by rewrite IH, (assoc_L _).
Qed.
Lemma elem_of_gmultiset_disj_union_list Xs x :
x ⋃+ Xs X, X Xs x X.
Proof. induction Xs; multiset_solver. Qed.
Lemma multiplicity_gmultiset_disj_union_list x Xs :
multiplicity x (⋃+ Xs) = sum_list (multiplicity x <$> Xs).
Proof.
induction Xs as [|X Xs IH]; [done|]; simpl.
by rewrite multiplicity_disj_union, IH.
Qed.
Global Instance gmultiset_disj_union_list_proper :
Proper (() ==> (=)) (@disj_union_list (gmultiset A) _ _).
Proof. induction 1; multiset_solver. Qed.
End disj_union_list.
......@@ -45,7 +45,7 @@ Section search_infinite.
split; [done|]. apply elem_of_list_filter; naive_solver lia. }
intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
intros n1; constructor; intros n2 [Hn Hs].
apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
Qed.
Definition search_infinite_go (xs : list B) (n : nat)
......@@ -143,7 +143,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
Next Obligation.
intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
apply elem_of_list_fmap. eexists; split; [|done].
unfold fresh. by rewrite replicate_length.
unfold fresh. by rewrite length_replicate.
Qed.
Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(** This file collects general purpose definitions and theorems on
lists of numbers that are not in the Coq standard library. *)
From stdpp Require Export list.
From stdpp Require Export list_basics list_monad list_misc list_tactics.
From stdpp Require Import options.
Module Export list.
(** * Definitions *)
(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
......@@ -51,6 +53,12 @@ Fixpoint little_endian_to_Z (n : Z) (bs : list Z) : Z :=
Section seq.
Implicit Types m n i j : nat.
(* TODO: Coq 8.20 has the same lemma under the same name, so remove our version
once we require Coq 8.20. In Coq 8.19 and before, this lemma is called
[seq_length]. *)
Lemma length_seq m n : length (seq m n) = n.
Proof. revert m. induction n; intros; f_equal/=; auto. Qed.
Lemma fmap_add_seq j j' n : Nat.add j <$> seq j' n = seq (j + j') n.
Proof.
revert j'. induction n as [|n IH]; intros j'; csimpl; [reflexivity|].
......@@ -92,6 +100,12 @@ Section seq.
k seq j n j k < j + n.
Proof. rewrite elem_of_list_In, in_seq. done. Qed.
Lemma seq_nil n m : seq n m = [] m = 0.
Proof. by destruct m. Qed.
Lemma seq_subseteq_mono m n1 n2 : n1 n2 seq m n1 seq m n2.
Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
Lemma Forall_seq (P : nat Prop) i n :
Forall P (seq i n) j, i j < i + n P j.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
......@@ -112,6 +126,7 @@ Section seq.
- rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
- destruct m; simpl; auto with f_equal.
Qed.
End seq.
(** ** Properties of the [seqZ] function *)
......@@ -128,8 +143,8 @@ Section seqZ.
rewrite <-fmap_S_seq, <-list_fmap_compose.
apply map_ext; naive_solver lia.
Qed.
Lemma seqZ_length m n : length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
Lemma length_seqZ m n : length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite length_fmap, length_seq. Qed.
Lemma fmap_add_seqZ m m' n : Z.add m <$> seqZ m' n = seqZ (m + m') n.
Proof.
revert m'. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m'.
......@@ -217,7 +232,7 @@ Section sum_list.
sum_list szs = length l mjoin (reshape szs l) = l.
Proof.
revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|].
by rewrite IH, take_drop by (rewrite drop_length; lia).
by rewrite IH, take_drop by (rewrite length_drop; lia).
Qed.
Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
Proof. induction m; simpl; auto. Qed.
......@@ -237,9 +252,9 @@ Section mjoin.
Implicit Types l k : list A.
Implicit Types ls : list (list A).
Lemma join_length ls:
Lemma length_join ls:
length (mjoin ls) = sum_list (length <$> ls).
Proof. induction ls; [done|]; csimpl. rewrite app_length. lia. Qed.
Proof. induction ls; [done|]; csimpl. rewrite length_app. lia. Qed.
Lemma join_lookup_Some ls i x :
mjoin ls !! i = Some x j l i', ls !! j = Some l l !! i' = Some x
......@@ -262,7 +277,7 @@ Section mjoin.
intros Hl. rewrite join_lookup_Some.
f_equiv; intros j. f_equiv; intros l. f_equiv; intros i'.
assert (ls !! j = Some l j < length ls) by eauto using lookup_lt_Some.
rewrite (sum_list_fmap_same n), take_length by auto using Forall_take.
rewrite (sum_list_fmap_same n), length_take by auto using Forall_take.
naive_solver lia.
Qed.
......@@ -358,7 +373,7 @@ Section Z_little_endian.
rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia.
Qed.
Lemma Z_to_little_endian_length m n z :
Lemma length_Z_to_little_endian m n z :
0 m
Z.of_nat (length (Z_to_little_endian m n z)) = m.
Proof.
......@@ -430,3 +445,5 @@ Section Z_little_endian.
by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
Qed.
End Z_little_endian.
End list.
This diff is collapsed.
From Coq Require Export Permutation.
From stdpp Require Export numbers base option list_basics list_relations list_monad.
From stdpp Require Import options.
Module Export list.
(** * Reflection over lists *)
(** We define a simple data structure [rlist] to capture a syntactic
representation of lists consisting of constants, applications and the nil list.
Note that we represent [(x ::.)] as [rapp (rnode [x])]. For now, we abstract
over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *)
Inductive rlist (A : Type) :=
rnil : rlist A | rnode : A rlist A | rapp : rlist A rlist A rlist A.
Global Arguments rnil {_} : assert.
Global Arguments rnode {_} _ : assert.
Global Arguments rapp {_} _ _ : assert.
Module rlist.
Fixpoint to_list {A} (t : rlist A) : list A :=
match t with
| rnil => [] | rnode l => [l] | rapp t1 t2 => to_list t1 ++ to_list t2
end.
Notation env A := (list (list A)) (only parsing).
Definition eval {A} (E : env A) : rlist nat list A :=
fix go t :=
match t with
| rnil => []
| rnode i => default [] (E !! i)
| rapp t1 t2 => go t1 ++ go t2
end.
(** A simple quoting mechanism using type classes. [QuoteLookup E1 E2 x i]
means: starting in environment [E1], look up the index [i] corresponding to the
constant [x]. In case [x] has a corresponding index [i] in [E1], the original
environment is given back as [E2]. Otherwise, the environment [E2] is extended
with a binding [i] for [x]. *)
Section quote_lookup.
Context {A : Type}.
Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat) := {}.
Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0 := {}.
Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0 := {}.
Global Instance quote_lookup_further E1 E2 x i y :
QuoteLookup E1 E2 x i QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000 := {}.
End quote_lookup.
Section quote.
Context {A : Type}.
Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
Global Instance quote_nil E1 : Quote E1 E1 [] rnil := {}.
Global Instance quote_node E1 E2 l i:
QuoteLookup E1 E2 l i Quote E1 E2 l (rnode i) | 1000 := {}.
Global Instance quote_cons E1 E2 E3 x l i t :
QuoteLookup E1 E2 [x] i
Quote E2 E3 l t Quote E1 E3 (x :: l) (rapp (rnode i) t) := {}.
Global Instance quote_app E1 E2 E3 l1 l2 t1 t2 :
Quote E1 E2 l1 t1 Quote E2 E3 l2 t2 Quote E1 E3 (l1 ++ l2) (rapp t1 t2) := {}.
End quote.
Section eval.
Context {A} (E : env A).
Lemma eval_alt t : eval E t = to_list t ≫= default [] (E !!.).
Proof.
induction t; csimpl.
- done.
- by rewrite (right_id_L [] (++)).
- rewrite bind_app. by f_equal.
Qed.
Lemma eval_eq t1 t2 : to_list t1 = to_list t2 eval E t1 = eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
Lemma eval_Permutation t1 t2 :
to_list t1 to_list t2 eval E t1 eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
Lemma eval_submseteq t1 t2 :
to_list t1 ⊆+ to_list t2 eval E t1 ⊆+ eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
End eval.
End rlist.
(** * Tactics *)
Ltac quote_Permutation :=
match goal with
| |- ?l1 ?l2 =>
match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
change (rlist.eval E3 t1 rlist.eval E3 t2)
end end
end.
Ltac solve_Permutation :=
quote_Permutation; apply rlist.eval_Permutation;
compute_done.
Ltac quote_submseteq :=
match goal with
| |- ?l1 ⊆+ ?l2 =>
match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
change (rlist.eval E3 t1 ⊆+ rlist.eval E3 t2)
end end
end.
Ltac solve_submseteq :=
quote_submseteq; apply rlist.eval_submseteq;
compute_done.
Ltac decompose_elem_of_list := repeat
match goal with
| H : ?x [] |- _ => by destruct (not_elem_of_nil x)
| H : _ _ :: _ |- _ => apply elem_of_cons in H; destruct H
| H : _ _ ++ _ |- _ => apply elem_of_app in H; destruct H
end.
Ltac solve_length :=
simplify_eq/=;
repeat (rewrite length_fmap || rewrite length_app);
repeat match goal with
| H : _ =@{list _} _ |- _ => apply (f_equal length) in H
| H : Forall2 _ _ _ |- _ => apply Forall2_length in H
| H : context[length (_ <$> _)] |- _ => rewrite length_fmap in H
end; done || congruence.
Ltac simplify_list_eq ::= repeat
match goal with
| _ => progress simplify_eq/=
| H : [?x] !! ?i = Some ?y |- _ =>
destruct i; [change (Some x = Some y) in H | discriminate]
| H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
| H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
| H : zip_with _ _ _ = [] |- _ => apply zip_with_nil_inv in H; destruct H
| H : [] = zip_with _ _ _ |- _ => symmetry in H
| |- context [(_ ++ _) ++ _] => rewrite <-(assoc_L (++))
| H : context [(_ ++ _) ++ _] |- _ => rewrite <-(assoc_L (++)) in H
| H : context [_ <$> (_ ++ _)] |- _ => rewrite fmap_app in H
| |- context [_ <$> (_ ++ _)] => rewrite fmap_app
| |- context [_ ++ []] => rewrite (right_id_L [] (++))
| H : context [_ ++ []] |- _ => rewrite (right_id_L [] (++)) in H
| |- context [take _ (_ <$> _)] => rewrite <-fmap_take
| H : context [take _ (_ <$> _)] |- _ => rewrite <-fmap_take in H
| |- context [drop _ (_ <$> _)] => rewrite <-fmap_drop
| H : context [drop _ (_ <$> _)] |- _ => rewrite <-fmap_drop in H
| H : _ ++ _ = _ ++ _ |- _ =>
repeat (rewrite <-app_comm_cons in H || rewrite <-(assoc_L (++)) in H);
apply app_inj_1 in H; [destruct H|solve_length]
| H : _ ++ _ = _ ++ _ |- _ =>
repeat (rewrite app_comm_cons in H || rewrite (assoc_L (++)) in H);
apply app_inj_2 in H; [destruct H|solve_length]
| |- context [zip_with _ (_ ++ _) (_ ++ _)] =>
rewrite zip_with_app by solve_length
| |- context [take _ (_ ++ _)] => rewrite take_app_length' by solve_length
| |- context [drop _ (_ ++ _)] => rewrite drop_app_length' by solve_length
| H : context [zip_with _ (_ ++ _) (_ ++ _)] |- _ =>
rewrite zip_with_app in H by solve_length
| H : context [take _ (_ ++ _)] |- _ =>
rewrite take_app_length' in H by solve_length
| H : context [drop _ (_ ++ _)] |- _ =>
rewrite drop_app_length' in H by solve_length
| H : ?l !! ?i = _, H2 : context [(_ <$> ?l) !! ?i] |- _ =>
rewrite list_lookup_fmap, H in H2
end.
Ltac decompose_Forall_hyps :=
repeat match goal with
| H : Forall _ [] |- _ => clear H
| H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
| H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
| H : Forall2 _ [] [] |- _ => clear H
| H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
| H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
| H : Forall2 _ [] ?k |- _ => apply Forall2_nil_inv_l in H
| H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H
| H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
apply Forall2_cons_1 in H; destruct H
| H : Forall2 _ (_ :: _) ?k |- _ =>
let k_hd := fresh k "_hd" in let k_tl := fresh k "_tl" in
apply Forall2_cons_inv_l in H; destruct H as (k_hd&k_tl&?&?&->);
rename k_tl into k
| H : Forall2 _ ?l (_ :: _) |- _ =>
let l_hd := fresh l "_hd" in let l_tl := fresh l "_tl" in
apply Forall2_cons_inv_r in H; destruct H as (l_hd&l_tl&?&?&->);
rename l_tl into l
| H : Forall2 _ (_ ++ _) ?k |- _ =>
let k1 := fresh k "_1" in let k2 := fresh k "_2" in
apply Forall2_app_inv_l in H; destruct H as (k1&k2&?&?&->)
| H : Forall2 _ ?l (_ ++ _) |- _ =>
let l1 := fresh l "_1" in let l2 := fresh l "_2" in
apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
| _ => progress simplify_eq/=
| H : Forall3 _ _ (_ :: _) _ |- _ =>
apply Forall3_cons_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
| H : Forall2 _ (_ :: _) ?k |- _ =>
apply Forall2_cons_inv_l in H; destruct H as (?&?&?&?&?)
| H : Forall2 _ ?l (_ :: _) |- _ =>
apply Forall2_cons_inv_r in H; destruct H as (?&?&?&?&?)
| H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
apply Forall2_app_inv in H; [destruct H|solve_length]
| H : Forall2 _ ?l (_ ++ _) |- _ =>
apply Forall2_app_inv_r in H; destruct H as (?&?&?&?&?)
| H : Forall2 _ (_ ++ _) ?k |- _ =>
apply Forall2_app_inv_l in H; destruct H as (?&?&?&?&?)
| H : Forall3 _ _ (_ ++ _) _ |- _ =>
apply Forall3_app_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
| H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
(* to avoid some stupid loops, not fool proof *)
unless (P x) by auto using Forall_app_2, Forall_nil_2;
let E := fresh in
assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E
| H : Forall2 ?P ?l ?k |- _ =>
match goal with
| H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ =>
unless (P x y) by done; let E := fresh in
assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y));
lazy beta in E
| H1 : l !! ?i = Some ?x |- _ =>
try (match goal with _ : k !! i = Some _ |- _ => fail 2 end);
destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
| H2 : k !! ?i = Some ?y |- _ =>
try (match goal with _ : l !! i = Some _ |- _ => fail 2 end);
destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
end
| H : Forall3 ?P ?l ?l' ?k |- _ =>
lazymatch goal with
| H1:l !! ?i = Some ?x, H2:l' !! ?i = Some ?y, H3:k !! ?i = Some ?z |- _ =>
unless (P x y z) by done; let E := fresh in
assert (P x y z) as E by (by apply (Forall3_lookup_lmr P l l' k i x y z));
lazy beta in E
| H1 : l !! _ = Some ?x |- _ =>
destruct (Forall3_lookup_l P _ _ _ _ _ H H1) as (?&?&?&?&?)
| H2 : l' !! _ = Some ?y |- _ =>
destruct (Forall3_lookup_m P _ _ _ _ _ H H2) as (?&?&?&?&?)
| H3 : k !! _ = Some ?z |- _ =>
destruct (Forall3_lookup_r P _ _ _ _ _ H H3) as (?&?&?&?&?)
end
end.
Ltac list_simplifier :=
simplify_eq/=;
repeat match goal with
| _ => progress decompose_Forall_hyps
| _ => progress simplify_list_eq
| H : _ <$> _ = _ :: _ |- _ =>
apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
| H : _ :: _ = _ <$> _ |- _ => symmetry in H
| H : _ <$> _ = _ ++ _ |- _ =>
apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
| H : _ ++ _ = _ <$> _ |- _ => symmetry in H
| H : zip_with _ _ _ = _ :: _ |- _ =>
apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
| H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
| H : zip_with _ _ _ = _ ++ _ |- _ =>
apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?&?)
| H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
end.
Ltac decompose_Forall := repeat
match goal with
| |- Forall _ _ => by apply Forall_true
| |- Forall _ [] => constructor
| |- Forall _ (_ :: _) => constructor
| |- Forall _ (_ ++ _) => apply Forall_app_2
| |- Forall _ (_ <$> _) => apply Forall_fmap
| |- Forall _ (_ ≫= _) => apply Forall_bind
| |- Forall2 _ _ _ => apply Forall_Forall2_diag
| |- Forall2 _ [] [] => constructor
| |- Forall2 _ (_ :: _) (_ :: _) => constructor
| |- Forall2 _ (_ ++ _) (_ ++ _) => first
[ apply Forall2_app; [by decompose_Forall |]
| apply Forall2_app; [| by decompose_Forall]]
| |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
| |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
| _ => progress decompose_Forall_hyps
| H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
| H : Forall _ (_ ≫= _) |- _ => rewrite Forall_bind in H
| |- Forall _ _ =>
apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
| |- Forall2 _ _ _ =>
apply Forall2_same_length_lookup_2; [solve_length|];
intros ?????; progress decompose_Forall_hyps
end.
(** The [simplify_suffix] tactic removes [suffix] hypotheses that are
tautologies, and simplifies [suffix] hypotheses involving [(::)] and
[(++)]. *)
Ltac simplify_suffix := repeat
match goal with
| H : suffix (_ :: _) _ |- _ => destruct (suffix_cons_not _ _ H)
| H : suffix (_ :: _) [] |- _ => apply suffix_nil_inv in H
| H : suffix (_ ++ _) (_ ++ _) |- _ => apply suffix_app_inv in H
| H : suffix (_ :: _) (_ :: _) |- _ =>
destruct (suffix_cons_inv _ _ _ _ H); clear H
| H : suffix ?x ?x |- _ => clear H
| H : suffix ?x (_ :: ?x) |- _ => clear H
| H : suffix ?x (_ ++ ?x) |- _ => clear H
| _ => progress simplify_eq/=
end.
(** The [solve_suffix] tactic tries to solve goals involving [suffix]. It
uses [simplify_suffix] to simplify hypotheses and tries to solve [suffix]
conclusions. This tactic either fails or proves the goal. *)
Ltac solve_suffix := by intuition (repeat
match goal with
| _ => done
| _ => progress simplify_suffix
| |- suffix [] _ => apply suffix_nil
| |- suffix _ _ => reflexivity
| |- suffix _ (_ :: _) => apply suffix_cons_r
| |- suffix _ (_ ++ _) => apply suffix_app_r
| H : suffix _ _ False |- _ => destruct H
end).
End list.
This diff is collapsed.
......@@ -7,6 +7,7 @@ From stdpp Require Import options.
Local Open Scope N_scope.
Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
Add Printing Constructor Nmap.
Global Arguments Nmap_0 {_} _ : assert.
Global Arguments Nmap_pos {_} _ : assert.
Global Arguments NMap {_} _ _ : assert.
......@@ -56,12 +57,14 @@ Proof.
- intros ??? [??] []; simpl; [done|]. apply lookup_fmap.
- intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
- intros ??? f [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
- intros A B P f b Hemp Hinsert [mx t]. unfold map_fold; simpl.
apply (map_fold_ind (λ r t, P r (NMap mx t))); clear t.
- done.
- intros A P Hemp Hins [mx t].
induction t as [|i x t ? Hfold IH] using map_fold_fmap_ind.
{ destruct mx as [x|]; [|done].
replace (NMap (Some x) ) with (<[0:=x]> : Nmap _) by done.
by apply Hinsert. }
intros i x t r ??. by apply (Hinsert (N.pos i) x (NMap mx t)).
by apply Hins. }
apply (Hins (N.pos i) x (NMap mx t)); [done| |done].
intros A' B f g b. apply Hfold.
Qed.
(** * Finite sets *)
......
......@@ -165,7 +165,8 @@ Module Nat.
Global Instance divide_dec : RelDecision Nat.divide.
Proof.
refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
refine (λ x y, cast_if (decide (lcm x y = y)));
abstract (by rewrite Nat.divide_lcm_iff).
Defined.
Global Instance divide_po : PartialOrder divide.
Proof.
......@@ -339,7 +340,7 @@ Module Pos.
Fixpoint length (p : positive) : nat :=
match p with 1 => 0%nat | p~0 | p~1 => S (length p) end.
Lemma app_length p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
Lemma length_app p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
Proof. by induction p2; f_equal/=. Qed.
Lemma lt_sum (x y : positive) : x < y z, y = x + z.
......@@ -1018,7 +1019,7 @@ Module Qp.
Global Instance eq_dec : EqDecision Qp.
Proof.
refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
by rewrite <-to_Qc_inj_iff.
abstract (by rewrite <-to_Qc_inj_iff).
Defined.
Definition add (p q : Qp) : Qp :=
......@@ -1063,13 +1064,13 @@ Module Qp.
Global Instance le_dec : RelDecision le.
Proof.
refine (λ p q, cast_if (decide (Qp_to_Qc p Qp_to_Qc q)%Qc));
by rewrite to_Qc_inj_le.
Qed.
abstract (by rewrite to_Qc_inj_le).
Defined.
Global Instance lt_dec : RelDecision lt.
Proof.
refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
by rewrite to_Qc_inj_lt.
Qed.
abstract (by rewrite to_Qc_inj_lt).
Defined.
Global Instance lt_pi p q : ProofIrrel (lt p q).
Proof. destruct p, q; apply _. Qed.
......
This diff is collapsed.
......@@ -113,7 +113,7 @@ Proof. apply _. Qed.
Global Instance pretty_Z : Pretty Z := λ x,
match x with
| Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
end%string.
end.
Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
Proof.
unfold pretty, pretty_Z.
......
......@@ -6,13 +6,14 @@ Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
Add Printing Constructor propset.
Global Arguments PropSet {_} _ : assert.
Global Arguments propset_car {_} _ _ : assert.
(** Here we are using the notation "at level 200 as pattern" because we want to
(** Here we are using the notation "as pattern" because we want to
be compatible with all the rules that start with [ {[ TERM ] such as
records, singletons, and map singletons. See
https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#binders-bound-in-the-notation-and-parsed-as-terms
and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003 *)
and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003.
We don't set a level to be consistent with the notation for singleton sets. *)
Notation "{[ x | P ]}" := (PropSet (λ x, P))
(at level 1, x at level 200 as pattern, format "{[ x | P ]}") : stdpp_scope.
(at level 1, x as pattern, format "{[ x | P ]}") : stdpp_scope.
Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
......