Skip to content
Snippets Groups Projects
Commit 8ee34859 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove elem_of_tactic that uses intuition. 

This one (previously solve_elem_of) was hardly used. The tactic that uses
naive_solver (previously esolve_elem_of, now solve_elem_of) has been
extended with flags to say which hypotheses should be cleared/kept.
parent b13debed
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
modures/sts.v
+ 11
− 11
View file @ 8ee34859
...@@ -65,10 +65,10 @@ Global Instance sts_minus : Minus (t R tok) := λ x1 x2, ...@@ -65,10 +65,10 @@ Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
| auth s T1, auth _ T2 => frag (up (T1 ∖ T2) s) (T1 ∖ T2) | auth s T1, auth _ T2 => frag (up (T1 ∖ T2) s) (T1 ∖ T2)
end. end.
Hint Extern 10 (equiv (A:=set _) _ _) => esolve_elem_of : sts. Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬(equiv (A:=set _) _ _)) => esolve_elem_of : sts. Hint Extern 10 (¬(equiv (A:=set _) _ _)) => solve_elem_of : sts.
Hint Extern 10 (_ ∈ _) => esolve_elem_of : sts. Hint Extern 10 (_ ∈ _) => solve_elem_of : sts.
Hint Extern 10 (_ ⊆ _) => esolve_elem_of : sts. Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts.
Instance: Equivalence ((≡) : relation (t R tok)). Instance: Equivalence ((≡) : relation (t R tok)).
Proof. Proof.
split. split.
...@@ -89,7 +89,7 @@ Lemma closed_op T1 T2 S1 S2 : ...@@ -89,7 +89,7 @@ Lemma closed_op T1 T2 S1 S2 :
closed T1 S1 → closed T2 S2 → closed T1 S1 → closed T2 S2 →
T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (T1 ∪ T2) (S1 ∩ S2). T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (T1 ∪ T2) (S1 ∩ S2).
Proof. Proof.
intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|esolve_elem_of|]. intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split. intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
* apply Hstep1 with s3, Frame_step with T3 T4; auto with sts. * apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
* apply Hstep2 with s3, Frame_step with T3 T4; auto with sts. * apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
...@@ -112,7 +112,7 @@ Lemma closed_up_set S T : ...@@ -112,7 +112,7 @@ Lemma closed_up_set S T :
(∀ s, s ∈ S → tok s ∩ T ≡ ∅) → S ≢ ∅ → closed T (up_set T S). (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → S ≢ ∅ → closed T (up_set T S).
Proof. Proof.
intros HS Hne; unfold up_set; split. intros HS Hne; unfold up_set; split.
* assert (∀ s, s ∈ up T s) by eauto using elem_of_up. esolve_elem_of. * assert (∀ s, s ∈ up T s) by eauto using elem_of_up. solve_elem_of.
* intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
specialize (HS s' Hs'); clear Hs' Hne S. specialize (HS s' Hs'); clear Hs' Hne S.
induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto. induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto.
...@@ -125,7 +125,7 @@ Proof. eauto using closed_up_set with sts. Qed. ...@@ -125,7 +125,7 @@ Proof. eauto using closed_up_set with sts. Qed.
Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed T (up T s). Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed T (up T s).
Proof. Proof.
intros; rewrite -(collection_bind_singleton (up T) s). intros; rewrite -(collection_bind_singleton (up T) s).
apply closed_up_set; esolve_elem_of. apply closed_up_set; solve_elem_of.
Qed. Qed.
Lemma closed_up_empty s : closed ∅ (up ∅ s). Lemma closed_up_empty s : closed ∅ (up ∅ s).
Proof. eauto using closed_up with sts. Qed. Proof. eauto using closed_up with sts. Qed.
...@@ -145,7 +145,7 @@ Proof. ...@@ -145,7 +145,7 @@ Proof.
* by do 2 destruct 1; constructor; setoid_subst. * by do 2 destruct 1; constructor; setoid_subst.
* assert (∀ T T' S s, * assert (∀ T T' S s,
closed T S → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅). closed T S → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
{ intros S T T' s [??]; esolve_elem_of. } { intros S T T' s [??]; solve_elem_of. }
destruct 3; simpl in *; auto using closed_op with sts. destruct 3; simpl in *; auto using closed_op with sts.
* intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts. * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
* intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst; * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
...@@ -158,7 +158,7 @@ Proof. ...@@ -158,7 +158,7 @@ Proof.
* destruct 3; constructor; auto with sts. * destruct 3; constructor; auto with sts.
* intros [|S T]; constructor; auto using elem_of_up with sts. * intros [|S T]; constructor; auto using elem_of_up with sts.
assert (S ⊆ up_set ∅ S ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne. assert (S ⊆ up_set ∅ S ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne.
esolve_elem_of. solve_elem_of.
* intros [|S T]; constructor; auto with sts. * intros [|S T]; constructor; auto with sts.
assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts. assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts.
* intros [s T|S T]; constructor; auto with sts. * intros [s T|S T]; constructor; auto with sts.
...@@ -166,7 +166,7 @@ Proof. ...@@ -166,7 +166,7 @@ Proof.
+ rewrite (up_closed (up_set _ _)); + rewrite (up_closed (up_set _ _));
eauto using closed_up_set, closed_ne with sts. eauto using closed_up_set, closed_ne with sts.
* intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_ands. * intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_ands.
+ destruct Hxz;inversion_clear Hy;constructor;unfold up_set;esolve_elem_of. + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
+ destruct Hxz; inversion_clear Hy; simpl; + destruct Hxz; inversion_clear Hy; simpl;
auto using closed_up_set_empty, closed_up_empty with sts. auto using closed_up_set_empty, closed_up_empty with sts.
+ destruct Hxz; inversion_clear Hy; constructor; + destruct Hxz; inversion_clear Hy; constructor;
...@@ -198,7 +198,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf : ...@@ -198,7 +198,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf :
Proof. Proof.
inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto. inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
* eapply Hstep with s1, Frame_step with T1 T2; auto with sts. * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
* clear Hstep Hs1 Hs2; esolve_elem_of. * solve_elem_of -Hstep Hs1 Hs2.
Qed. Qed.
End sts_core. End sts_core.
End sts. End sts.
......
prelude/collections.v
+ 47
− 52
View file @ 8ee34859
...@@ -248,27 +248,22 @@ Ltac unfold_elem_of := ...@@ -248,27 +248,22 @@ Ltac unfold_elem_of :=
| |- context [ _ ∈ of_list _ ] => setoid_rewrite elem_of_of_list | |- context [ _ ∈ of_list _ ] => setoid_rewrite elem_of_of_list
end. end.
(** The tactic [solve_elem_of tac] composes the above tactic with [intuition]. (** Since [firstorder] fails or loops on very small goals generated by
For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is [solve_elem_of] already. We use the [naive_solver] tactic as a substitute.
generally powerful enough. This tactic either fails or proves the goal. *) This tactic either fails or proves the goal. *)
Tactic Notation "solve_elem_of" tactic3(tac) := Tactic Notation "solve_elem_of" tactic3(tac) :=
setoid_subst;
decompose_empty;
unfold_elem_of;
solve [intuition (simplify_equality; tac)].
Tactic Notation "solve_elem_of" := solve_elem_of auto.
(** For goals with quantifiers we could use the above tactic but with
[firstorder] instead of [intuition] as finishing tactic. However, [firstorder]
fails or loops on very small goals generated by [solve_elem_of] already. We
use the [naive_solver] tactic as a substitute. This tactic either fails or
proves the goal. *)
Tactic Notation "esolve_elem_of" tactic3(tac) :=
setoid_subst; setoid_subst;
decompose_empty; decompose_empty;
unfold_elem_of; unfold_elem_of;
naive_solver tac. naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. Tactic Notation "solve_elem_of" "-" hyp_list(Hs) "/" tactic3(tac) :=
clear Hs; solve_elem_of tac.
Tactic Notation "solve_elem_of" "+" hyp_list(Hs) "/" tactic3(tac) :=
revert Hs; clear; solve_elem_of tac.
Tactic Notation "solve_elem_of" := solve_elem_of eauto.
Tactic Notation "solve_elem_of" "-" hyp_list(Hs) := clear Hs; solve_elem_of.
Tactic Notation "solve_elem_of" "+" hyp_list(Hs) :=
revert Hs; clear; solve_elem_of.
(** * More theorems *) (** * More theorems *)
Section collection. Section collection.
...@@ -284,21 +279,21 @@ Section collection. ...@@ -284,21 +279,21 @@ Section collection.
by rewrite !elem_of_difference, HX, HY. by rewrite !elem_of_difference, HX, HY.
Qed. Qed.
Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}. Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y. Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma subseteq_empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅. Lemma subseteq_empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma difference_diag X : X ∖ X ≡ ∅. Lemma difference_diag X : X ∖ X ≡ ∅.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z. Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma difference_union_distr_r X Y Z : Z ∖ (X ∪ Y) ≡ (Z ∖ X) ∩ (Z ∖ Y). Lemma difference_union_distr_r X Y Z : Z ∖ (X ∪ Y) ≡ (Z ∖ X) ∩ (Z ∖ Y).
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y. Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Section leibniz. Section leibniz.
Context `{!LeibnizEquiv C}. Context `{!LeibnizEquiv C}.
...@@ -335,10 +330,10 @@ Section collection. ...@@ -335,10 +330,10 @@ Section collection.
Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
Proof. Proof.
intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
destruct (decide (x ∈ X)); esolve_elem_of. destruct (decide (x ∈ X)); solve_elem_of.
Qed. Qed.
Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y. Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y.
Proof. intros ? x ?; apply dec_stable; esolve_elem_of. Qed. Proof. intros ? x ?; apply dec_stable; solve_elem_of. Qed.
Context `{!LeibnizEquiv C}. Context `{!LeibnizEquiv C}.
Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
Proof. unfold_leibniz. apply union_difference. Qed. Proof. unfold_leibniz. apply union_difference. Qed.
...@@ -397,23 +392,23 @@ Section NoDup. ...@@ -397,23 +392,23 @@ Section NoDup.
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma elem_of_upto_elem_of x X : x ∈ X → elem_of_upto x X. Lemma elem_of_upto_elem_of x X : x ∈ X → elem_of_upto x X.
Proof. unfold elem_of_upto. esolve_elem_of. Qed. Proof. unfold elem_of_upto. solve_elem_of. Qed.
Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅. Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅.
Proof. unfold elem_of_upto. esolve_elem_of. Qed. Proof. unfold elem_of_upto. solve_elem_of. Qed.
Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y. Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y.
Proof. unfold elem_of_upto. esolve_elem_of. Qed. Proof. unfold elem_of_upto. solve_elem_of. Qed.
Lemma elem_of_upto_union X Y x : Lemma elem_of_upto_union X Y x :
elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y. elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y.
Proof. unfold elem_of_upto. esolve_elem_of. Qed. Proof. unfold elem_of_upto. solve_elem_of. Qed.
Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y. Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y.
Proof. unfold elem_of_upto. esolve_elem_of. Qed. Proof. unfold elem_of_upto. solve_elem_of. Qed.
Lemma set_NoDup_empty: set_NoDup ∅. Lemma set_NoDup_empty: set_NoDup ∅.
Proof. unfold set_NoDup. solve_elem_of. Qed. Proof. unfold set_NoDup. solve_elem_of. Qed.
Lemma set_NoDup_add x X : Lemma set_NoDup_add x X :
¬elem_of_upto x X → set_NoDup X → set_NoDup ({[ x ]} ∪ X). ¬elem_of_upto x X → set_NoDup X → set_NoDup ({[ x ]} ∪ X).
Proof. unfold set_NoDup, elem_of_upto. esolve_elem_of. Qed. Proof. unfold set_NoDup, elem_of_upto. solve_elem_of. Qed.
Lemma set_NoDup_inv_add x X : Lemma set_NoDup_inv_add x X :
x ∉ X → set_NoDup ({[ x ]} ∪ X) → ¬elem_of_upto x X. x ∉ X → set_NoDup ({[ x ]} ∪ X) → ¬elem_of_upto x X.
Proof. Proof.
...@@ -445,16 +440,16 @@ Section quantifiers. ...@@ -445,16 +440,16 @@ Section quantifiers.
Proof. unfold set_Forall. solve_elem_of. Qed. Proof. unfold set_Forall. solve_elem_of. Qed.
Lemma set_Exists_empty : ¬set_Exists ∅. Lemma set_Exists_empty : ¬set_Exists ∅.
Proof. unfold set_Exists. esolve_elem_of. Qed. Proof. unfold set_Exists. solve_elem_of. Qed.
Lemma set_Exists_singleton x : set_Exists {[ x ]} ↔ P x. Lemma set_Exists_singleton x : set_Exists {[ x ]} ↔ P x.
Proof. unfold set_Exists. esolve_elem_of. Qed. Proof. unfold set_Exists. solve_elem_of. Qed.
Lemma set_Exists_union_1 X Y : set_Exists X → set_Exists (X ∪ Y). Lemma set_Exists_union_1 X Y : set_Exists X → set_Exists (X ∪ Y).
Proof. unfold set_Exists. esolve_elem_of. Qed. Proof. unfold set_Exists. solve_elem_of. Qed.
Lemma set_Exists_union_2 X Y : set_Exists Y → set_Exists (X ∪ Y). Lemma set_Exists_union_2 X Y : set_Exists Y → set_Exists (X ∪ Y).
Proof. unfold set_Exists. esolve_elem_of. Qed. Proof. unfold set_Exists. solve_elem_of. Qed.
Lemma set_Exists_union_inv X Y : Lemma set_Exists_union_inv X Y :
set_Exists (X ∪ Y) → set_Exists X ∨ set_Exists Y. set_Exists (X ∪ Y) → set_Exists X ∨ set_Exists Y.
Proof. unfold set_Exists. esolve_elem_of. Qed. Proof. unfold set_Exists. solve_elem_of. Qed.
End quantifiers. End quantifiers.
Section more_quantifiers. Section more_quantifiers.
...@@ -511,7 +506,7 @@ Section fresh. ...@@ -511,7 +506,7 @@ Section fresh.
Qed. Qed.
Lemma Forall_fresh_subseteq X Y xs : Lemma Forall_fresh_subseteq X Y xs :
Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs. Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
Proof. rewrite !Forall_fresh_alt; esolve_elem_of. Qed. Proof. rewrite !Forall_fresh_alt; solve_elem_of. Qed.
Lemma fresh_list_length n X : length (fresh_list n X) = n. Lemma fresh_list_length n X : length (fresh_list n X) = n.
Proof. revert X. induction n; simpl; auto. Qed. Proof. revert X. induction n; simpl; auto. Qed.
...@@ -538,41 +533,41 @@ Section collection_monad. ...@@ -538,41 +533,41 @@ Section collection_monad.
Global Instance collection_fmap_proper {A B} : Global Instance collection_fmap_proper {A B} :
Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B). Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
Proof. intros f g ? X Y [??]; split; esolve_elem_of. Qed. Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed.
Global Instance collection_bind_proper {A B} : Global Instance collection_bind_proper {A B} :
Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B). Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y [??]; split; esolve_elem_of. Qed. Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed.
Global Instance collection_join_proper {A} : Global Instance collection_join_proper {A} :
Proper ((≡) ==> (≡)) (@mjoin M _ A). Proper ((≡) ==> (≡)) (@mjoin M _ A).
Proof. intros X Y [??]; split; esolve_elem_of. Qed. Proof. intros X Y [??]; split; solve_elem_of. Qed.
Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x. Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → guard P; X ≡ X. Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → guard P; X ≡ X.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) : Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
g ∘ f <$> X ≡ g <$> (f <$> X). g ∘ f <$> X ≡ g <$> (f <$> X).
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) : Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) :
y ∈ f <$> X → ∃ x, y = f x ∧ x ∈ X. y ∈ f <$> X → ∃ x, y = f x ∧ x ∈ X.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma elem_of_fmap_2 {A B} (f : A → B) (X : M A) (x : A) : Lemma elem_of_fmap_2 {A B} (f : A → B) (X : M A) (x : A) :
x ∈ X → f x ∈ f <$> X. x ∈ X → f x ∈ f <$> X.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma elem_of_fmap_2_alt {A B} (f : A → B) (X : M A) (x : A) (y : B) : Lemma elem_of_fmap_2_alt {A B} (f : A → B) (X : M A) (x : A) (y : B) :
x ∈ X → y = f x → y ∈ f <$> X. x ∈ X → y = f x → y ∈ f <$> X.
Proof. esolve_elem_of. Qed. Proof. solve_elem_of. Qed.
Lemma elem_of_mapM {A B} (f : A → M B) l k : Lemma elem_of_mapM {A B} (f : A → M B) l k :
l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k. l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
Proof. Proof.
split. split.
* revert l. induction k; esolve_elem_of. * revert l. induction k; solve_elem_of.
* induction 1; esolve_elem_of. * induction 1; solve_elem_of.
Qed. Qed.
Lemma collection_mapM_length {A B} (f : A → M B) l k : Lemma collection_mapM_length {A B} (f : A → M B) l k :
l ∈ mapM f k → length l = length k. l ∈ mapM f k → length l = length k.
Proof. revert l; induction k; esolve_elem_of. Qed. Proof. revert l; induction k; solve_elem_of. Qed.
Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k : Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l. Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
Proof. Proof.
...@@ -606,9 +601,9 @@ Section finite. ...@@ -606,9 +601,9 @@ Section finite.
rewrite elem_of_union, elem_of_app; naive_solver. rewrite elem_of_union, elem_of_app; naive_solver.
Qed. Qed.
Lemma union_finite_inv_l X Y : set_finite (X ∪ Y) → set_finite X. Lemma union_finite_inv_l X Y : set_finite (X ∪ Y) → set_finite X.
Proof. intros [l ?]; exists l; esolve_elem_of. Qed. Proof. intros [l ?]; exists l; solve_elem_of. Qed.
Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y. Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y.
Proof. intros [l ?]; exists l; esolve_elem_of. Qed. Proof. intros [l ?]; exists l; solve_elem_of. Qed.
End finite. End finite.
Section more_finite. Section more_finite.
......
prelude/fin_collections.v
+ 6
− 6
View file @ 8ee34859
...@@ -83,7 +83,7 @@ Proof. ...@@ -83,7 +83,7 @@ Proof.
apply Permutation_length, NoDup_Permutation. apply Permutation_length, NoDup_Permutation.
* apply NoDup_elements. * apply NoDup_elements.
* apply NoDup_app; repeat split; try apply NoDup_elements. * apply NoDup_app; repeat split; try apply NoDup_elements.
intros x; rewrite !elem_of_elements; esolve_elem_of. intros x; rewrite !elem_of_elements; solve_elem_of.
* intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. * intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Qed. Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
...@@ -107,7 +107,7 @@ Qed. ...@@ -107,7 +107,7 @@ Qed.
Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
Proof. Proof.
rewrite <-size_union by solve_elem_of. rewrite <-size_union by solve_elem_of.
setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by esolve_elem_of. setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of.
rewrite <-union_difference, (commutative (∪)); solve_elem_of. rewrite <-union_difference, (commutative (∪)); solve_elem_of.
Qed. Qed.
Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
...@@ -129,7 +129,7 @@ Proof. ...@@ -129,7 +129,7 @@ Proof.
{ apply collection_wf. } { apply collection_wf. }
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
* rewrite (union_difference {[ x ]} X) by solve_elem_of. * rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH. esolve_elem_of. apply Hadd. solve_elem_of. apply IH; solve_elem_of.
* by rewrite HX. * by rewrite HX.
Qed. Qed.
Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
...@@ -143,10 +143,10 @@ Proof. ...@@ -143,10 +143,10 @@ Proof.
symmetry. apply elem_of_elements. } symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl. induction 1 as [|x l ?? IH]; simpl.
* intros X HX. setoid_rewrite elem_of_nil in HX. * intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. esolve_elem_of. rewrite equiv_empty. done. solve_elem_of.
* intros X HX. setoid_rewrite elem_of_cons in HX. * intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite (union_difference {[ x ]} X) by esolve_elem_of. rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH. esolve_elem_of. apply Hadd. solve_elem_of. apply IH. solve_elem_of.
Qed. Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R} Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f} (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
......
prelude/fin_map_dom.v
+ 2
− 2
View file @ 8ee34859
...@@ -54,7 +54,7 @@ Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m. ...@@ -54,7 +54,7 @@ Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
Proof. Proof.
apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom. apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_insert_Some. unfold is_Some. setoid_rewrite lookup_insert_Some.
destruct (decide (i = j)); esolve_elem_of. destruct (decide (i = j)); solve_elem_of.
Qed. Qed.
Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m). Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
Proof. rewrite (dom_insert _). solve_elem_of. Qed. Proof. rewrite (dom_insert _). solve_elem_of. Qed.
...@@ -66,7 +66,7 @@ Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed. ...@@ -66,7 +66,7 @@ Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed.
Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}. Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
Proof. Proof.
apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom. apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_delete_Some. esolve_elem_of. unfold is_Some. setoid_rewrite lookup_delete_Some. solve_elem_of.
Qed. Qed.
Lemma delete_partial_alter_dom {A} (m : M A) i f : Lemma delete_partial_alter_dom {A} (m : M A) i f :
i ∉ dom D m → delete i (partial_alter f i m) = m. i ∉ dom D m → delete i (partial_alter f i m) = m.
......
prelude/hashset.v
+ 1
− 1
View file @ 8ee34859
...@@ -155,7 +155,7 @@ Proof. ...@@ -155,7 +155,7 @@ Proof.
* revert x. induction l as [|y l IH]; intros x; simpl. * revert x. induction l as [|y l IH]; intros x; simpl.
{ by rewrite elem_of_empty. } { by rewrite elem_of_empty. }
rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto. rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
* induction 1; esolve_elem_of. * induction 1; solve_elem_of.
Qed. Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l). Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof. Proof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment