diff --git a/theories/collections.v b/theories/collections.v index 65cc0e194caaa02eebe7325f20509edfbee1f9ba..2b54cd0ca8d26005ae7eee19ba88f4263be75e8d 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -248,27 +248,22 @@ Ltac unfold_elem_of := | |- context [ _ ∈ of_list _ ] => setoid_rewrite elem_of_of_list end. -(** The tactic [solve_elem_of tac] composes the above tactic with [intuition]. -For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is -generally powerful enough. This tactic either fails or proves the goal. *) +(** Since [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 "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; decompose_empty; unfold_elem_of; 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 *) Section collection. @@ -284,21 +279,21 @@ Section collection. by rewrite !elem_of_difference, HX, HY. Qed. 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. - Proof. esolve_elem_of. Qed. + Proof. solve_elem_of. Qed. 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 ≡ ∅. - 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. - 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). - 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. - Proof. esolve_elem_of. Qed. + Proof. solve_elem_of. Qed. Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y. - Proof. esolve_elem_of. Qed. + Proof. solve_elem_of. Qed. Section leibniz. Context `{!LeibnizEquiv C}. @@ -335,10 +330,10 @@ Section collection. Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. - destruct (decide (x ∈ X)); esolve_elem_of. + destruct (decide (x ∈ X)); solve_elem_of. Qed. 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}. Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. unfold_leibniz. apply union_difference. Qed. @@ -397,23 +392,23 @@ Section NoDup. Proof. firstorder. Qed. 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 ∅. - 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. - 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 : 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. - Proof. unfold elem_of_upto. esolve_elem_of. Qed. + Proof. unfold elem_of_upto. solve_elem_of. Qed. Lemma set_NoDup_empty: set_NoDup ∅. Proof. unfold set_NoDup. solve_elem_of. Qed. Lemma set_NoDup_add 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 : x ∉ X → set_NoDup ({[ x ]} ∪ X) → ¬elem_of_upto x X. Proof. @@ -445,16 +440,16 @@ Section quantifiers. Proof. unfold set_Forall. solve_elem_of. Qed. 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. - 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). - 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). - Proof. unfold set_Exists. esolve_elem_of. Qed. + Proof. unfold set_Exists. solve_elem_of. Qed. Lemma set_Exists_union_inv X 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. Section more_quantifiers. @@ -511,7 +506,7 @@ Section fresh. Qed. Lemma Forall_fresh_subseteq X 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. Proof. revert X. induction n; simpl; auto. Qed. @@ -538,41 +533,41 @@ Section collection_monad. Global Instance collection_fmap_proper {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} : 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} : 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. - 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. - 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) : 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) : 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) : 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) : 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 : l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k. Proof. split. - * revert l. induction k; esolve_elem_of. - * induction 1; esolve_elem_of. + * revert l. induction k; solve_elem_of. + * induction 1; solve_elem_of. Qed. Lemma collection_mapM_length {A B} (f : A → M B) l 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 : Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l. Proof. @@ -606,9 +601,9 @@ Section finite. rewrite elem_of_union, elem_of_app; naive_solver. Qed. 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. - Proof. intros [l ?]; exists l; esolve_elem_of. Qed. + Proof. intros [l ?]; exists l; solve_elem_of. Qed. End finite. Section more_finite. diff --git a/theories/fin_collections.v b/theories/fin_collections.v index 60e971e5f01f266dabae251cb5a2e218f84bd2b4..2f7a573d0ed171de1a6fcfe86a5c92cb5ccf5b1d 100644 --- a/theories/fin_collections.v +++ b/theories/fin_collections.v @@ -83,7 +83,7 @@ Proof. apply Permutation_length, NoDup_Permutation. * 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. Qed. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. @@ -107,7 +107,7 @@ Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). Proof. 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. Qed. Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. @@ -129,7 +129,7 @@ Proof. { apply collection_wf. } intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. * 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. Qed. Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : @@ -143,10 +143,10 @@ Proof. symmetry. apply elem_of_elements. } induction 1 as [|x l ?? IH]; simpl. * 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. - rewrite (union_difference {[ x ]} X) by esolve_elem_of. - apply Hadd. solve_elem_of. apply IH. esolve_elem_of. + rewrite (union_difference {[ x ]} X) by solve_elem_of. + apply Hadd. solve_elem_of. apply IH. solve_elem_of. Qed. Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R} (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f} diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v index 6d6836a88f689072b04a4b6f172cbdfd8347372d..e8169bf034f25fe67e6b10ee24899b4d578bbb52 100644 --- a/theories/fin_map_dom.v +++ b/theories/fin_map_dom.v @@ -54,7 +54,7 @@ Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m. Proof. apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_insert_Some. - destruct (decide (i = j)); esolve_elem_of. + destruct (decide (i = j)); solve_elem_of. Qed. 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. @@ -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 ]}. Proof. 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. Lemma delete_partial_alter_dom {A} (m : M A) i f : i ∉ dom D m → delete i (partial_alter f i m) = m. diff --git a/theories/hashset.v b/theories/hashset.v index efddcf1b36e9005f2886a49116fe0d39e945c50d..c6327dad01118aa1f8b86fd9ea91aa17e1fdd4ce 100644 --- a/theories/hashset.v +++ b/theories/hashset.v @@ -155,7 +155,7 @@ Proof. * revert x. induction l as [|y l IH]; intros x; simpl. { by rewrite elem_of_empty. } rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto. - * induction 1; esolve_elem_of. + * induction 1; solve_elem_of. Qed. Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l). Proof.