fsetdec : non-atomic elements are now transformed as variables first (fix #2464)

 Btw, we also get rid of equalities on something else than elements or sets

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

3 files changed, 89 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2464.v b/test-suite/bugs/closed/shouldsucceed/2464.v
new file mode 100644
index 000000000..af7085872
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2464.v
@@ -0,0 +1,39 @@
+Require Import FSetWeakList.
+Require Import FSetDecide.
+
+Parameter Name : Set.
+Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}.
+
+Module DecidableName.
+Definition t := Name.
+Definition eq := @eq Name.
+Definition eq_refl := @refl_equal Name.
+Definition eq_sym := @sym_eq Name.
+Definition eq_trans := @trans_eq Name.
+Definition eq_dec := eq_Name_dec.
+End DecidableName.
+
+Module NameSetMod := Make(DecidableName).
+
+Module NameSetDec := WDecide (NameSetMod).
+
+Class PartPatchUniverse (pu_type1 pu_type2 : Type)
+                       : Type := mkPartPatchUniverse {
+}.
+Class PatchUniverse {pu_type : Type}
+                    (ppu : PartPatchUniverse pu_type pu_type)
+                  : Type := mkPatchUniverse {
+    pu_nameOf : pu_type -> Name
+}.
+
+Lemma foo : forall (pu_type : Type)
+                   (ppu : PartPatchUniverse pu_type pu_type)
+                   (patchUniverse : PatchUniverse ppu)
+                   (ns ns1 ns2 : NameSetMod.t)
+                   (containsOK : NameSetMod.Equal ns1 ns2)
+                   (p : pu_type)
+                   (HX1 : NameSetMod.Equal ns1 (NameSetMod.add (pu_nameOf p) ns)),
+            NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns).
+Proof.
+NameSetDec.fsetdec.
+Qed.
\ No newline at end of file
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 550a6900b..f64df9fe1 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -366,6 +366,23 @@ the above form:
       "else" tactic(t2) :=
       first [ t; first [ t1 | fail 2 ] | t2 ].
 
+    Ltac abstract_term t :=
+      if (is_var t) then fail "no need to abstract a variable"
+      else (let x := fresh "x" in set (x := t) in *; try clearbody x).
+
+    Ltac abstract_elements :=
+      repeat
+        (match goal with
+           | |- context [ singleton ?t ] => abstract_term t
+           | _ : context [ singleton ?t ] |- _ => abstract_term t
+           | |- context [ add ?t _ ] => abstract_term t
+           | _ : context [ add ?t _ ] |- _ => abstract_term t
+           | |- context [ remove ?t _ ] => abstract_term t
+           | _ : context [ remove ?t _ ] |- _ => abstract_term t
+           | |- context [ In ?t _ ] => abstract_term t
+           | _ : context [ In ?t _ ] |- _ => abstract_term t
+         end).
+
     (** [prop P holds by t] succeeds (but does not modify the
         goal or context) if the proposition [P] can be proved by
         [t] in the current context.  Otherwise, the tactic
@@ -458,9 +475,12 @@ the above form:
         tactic). *)
     Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
     Ltac discard_nonFSet :=
-      decompose records;
       repeat (
         match goal with
+        | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
+          if (change T with E.t in H) then fail
+          else if (change T with t in H) then fail
+          else clear H
         | H : ?P |- _ =>
           if prop (FSet_Prop P) holds by
             (auto 100 with FSet_Prop)
@@ -679,6 +699,10 @@ the above form:
         [intros] to leave us with a goal of [~ P] than a goal of
         [False]. *)
     fold any not; intros;
+    (** We don't care about the value of elements : complex ones are
+        abstracted as new variables (avoiding potential dependencies,
+        see bug #2464) *)
+    abstract_elements;
     (** We remove dependencies to logical hypothesis. This way,
         later "clear" will work nicely (see bug #2136) *)
     no_logical_interdep;
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index 6abd19111..eefd2951f 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -366,6 +366,23 @@ the above form:
       "else" tactic(t2) :=
       first [ t; first [ t1 | fail 2 ] | t2 ].
 
+    Ltac abstract_term t :=
+      if (is_var t) then fail "no need to abstract a variable"
+      else (let x := fresh "x" in set (x := t) in *; try clearbody x).
+
+    Ltac abstract_elements :=
+      repeat
+        (match goal with
+           | |- context [ singleton ?t ] => abstract_term t
+           | _ : context [ singleton ?t ] |- _ => abstract_term t
+           | |- context [ add ?t _ ] => abstract_term t
+           | _ : context [ add ?t _ ] |- _ => abstract_term t
+           | |- context [ remove ?t _ ] => abstract_term t
+           | _ : context [ remove ?t _ ] |- _ => abstract_term t
+           | |- context [ In ?t _ ] => abstract_term t
+           | _ : context [ In ?t _ ] |- _ => abstract_term t
+         end).
+
     (** [prop P holds by t] succeeds (but does not modify the
         goal or context) if the proposition [P] can be proved by
         [t] in the current context.  Otherwise, the tactic
@@ -458,9 +475,12 @@ the above form:
         tactic). *)
     Hint Constructors MSet_elt_Prop MSet_Prop : MSet_Prop.
     Ltac discard_nonMSet :=
-      decompose records;
       repeat (
         match goal with
+        | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
+          if (change T with E.t in H) then fail
+          else if (change T with t in H) then fail
+          else clear H
         | H : ?P |- _ =>
           if prop (MSet_Prop P) holds by
             (auto 100 with MSet_Prop)
@@ -679,6 +699,10 @@ the above form:
         [intros] to leave us with a goal of [~ P] than a goal of
         [False]. *)
     fold any not; intros;
+    (** We don't care about the value of elements : complex ones are
+        abstracted as new variables (avoiding potential dependencies,
+        see bug #2464) *)
+    abstract_elements;
     (** We remove dependencies to logical hypothesis. This way,
         later "clear" will work nicely (see bug #2136) *)
     no_logical_interdep;