Commit 4b4e270e authored by Robbert Krebbers's avatar Robbert Krebbers

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 932ff6bd
......@@ -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.
......
......@@ -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}
......
......@@ -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.
......
......@@ -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.
......
Markdown is supported
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