diff --git a/theories/collections.v b/theories/collections.v index f2979bd81e02d81b3e71a789000581d3d2e63018..dae4a4696e83f3f474e1f1b6316fa593e585f3d8 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -253,19 +253,18 @@ Ltac set_unfold := (** Since [firstorder] fails or loops on very small goals generated by [set_solver] already. We use the [naive_solver] tactic as a substitute. This tactic either fails or proves the goal. *) -Tactic Notation "set_solver" tactic3(tac) := +Tactic Notation "set_solver" "by" tactic3(tac) := setoid_subst; decompose_empty; set_unfold; naive_solver tac. -Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) := - clear Hs; set_solver tac. -Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) := - revert Hs; clear; set_solver tac. -Tactic Notation "set_solver" := set_solver idtac. +Tactic Notation "set_solver" "-" hyp_list(Hs) "by" tactic3(tac) := + clear Hs; set_solver by tac. +Tactic Notation "set_solver" "+" hyp_list(Hs) "by" tactic3(tac) := + clear -Hs; set_solver by tac. +Tactic Notation "set_solver" := set_solver by idtac. Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver. -Tactic Notation "set_solver" "+" hyp_list(Hs) := - revert Hs; clear; set_solver. +Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver. (** * More theorems *) Section collection. @@ -537,10 +536,10 @@ Section collection_monad. Global Instance collection_fmap_mono {A B} : Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B). - Proof. intros f g ? X Y ?; set_solver eauto. Qed. + Proof. intros f g ? X Y ?; set_solver by eauto. Qed. Global Instance collection_fmap_proper {A B} : Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B). - Proof. intros f g ? X Y [??]; split; set_solver eauto. Qed. + Proof. intros f g ? X Y [??]; split; set_solver by eauto. Qed. Global Instance collection_bind_mono {A B} : Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B). Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed. @@ -575,12 +574,12 @@ Section collection_monad. l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k. Proof. split. - - revert l. induction k; set_solver eauto. + - revert l. induction k; set_solver by eauto. - induction 1; set_solver. 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; set_solver eauto. Qed. + Proof. revert l; induction k; set_solver by eauto. 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.