diff options
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetDecide.v | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index 1646ea7fa..6abd19111 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -480,6 +480,13 @@ the above form: F.union_iff F.inter_iff F.diff_iff : set_simpl. + Lemma eq_refl_iff (x : E.t) : E.eq x x <-> True. + Proof. + now split. + Qed. + + Hint Rewrite eq_refl_iff : set_eq_simpl. + (** ** Decidability of MSet Propositions *) (** [In] is decidable. *) @@ -556,8 +563,10 @@ the above form: Ltac substMSet := repeat ( match goal with + | H: E.eq ?x ?x |- _ => clear H | H: E.eq ?x ?y |- _ => rewrite H in *; clear H - end). + end); + autorewrite with set_eq_simpl in *. (** ** Considering Decidability of Base Propositions This tactic adds assertions about the decidability of @@ -637,13 +646,7 @@ the above form: (** Here is the crux of the proof search. Recursion through [intuition]! (This will terminate if I correctly understand the behavior of [intuition].) *) - Ltac fsetdec_rec := - try (match goal with - | H: E.eq ?x ?x -> False |- _ => destruct H - end); - (reflexivity || - contradiction || - (progress substMSet; intuition fsetdec_rec)). + Ltac fsetdec_rec := progress substMSet; intuition fsetdec_rec. (** If we add [unfold Empty, Subset, Equal in *; intros;] to the beginning of this tactic, it will satisfy the same @@ -651,12 +654,13 @@ the above form: be much slower than necessary without the pre-processing done by the wrapper tactic [fsetdec]. *) Ltac fsetdec_body := + autorewrite with set_eq_simpl in *; inst_MSet_hypotheses; - autorewrite with set_simpl in *; + autorewrite with set_simpl set_eq_simpl in *; push not in * using MSet_decidability; substMSet; assert_decidability; - auto using (@Equivalence_Reflexive _ _ E.eq_equiv); + auto; (intuition fsetdec_rec) || fail 1 "because the goal is beyond the scope of this tactic". @@ -874,5 +878,5 @@ Require Import MSetInterface. the subtyping [WS<=S], the [Decide] functor which is meant to be used on modules [(M:S)] can simply be an alias of [WDecide]. *) -Module WDecide (M:WSets) := WDecideOn M.E M. +Module WDecide (M:WSets) := !WDecideOn M.E M. Module Decide := WDecide. |