Improved handling of element equalities in fsetdec (fix #2467)

 - We now handle things like (H : E.eq x x -> ...)  by rewriting
   E.eq x x into True.

 - There was also a confusion between E.t and its various equivalent
   (but syntactically different) forms. This should be solved by
   preventing inlining during an inner functor application.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7

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.