Revision of the FSetWeak Interface, so that it becomes a precise

subtype of the FSet Interface (and idem for FMapWeak / FMap). 

1) No eq_dec is officially required in FSetWeakInterface.S.E
(EqualityType instead of DecidableType). But of course,
implementations still needs this eq_dec. 

2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In
FSetWeak we rename it into elements_3w, whereas in FSet we
artificially add elements_3w along to the original elements_3.

Initial steps toward factorization of FSetFacts and FSetWeakFacts, 
and so on...

Even if it's not required, FSetWeakList provides a eq_dec on sets, 
allowing weak sets of weak sets. 





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

20 files changed, 363 insertions, 111 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 6e4c4b26f..b7947cddd 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1070,6 +1070,10 @@ Proof.
 Qed.
 Hint Resolve elements_sort.
 
+Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s).
+Proof.
+ intros; apply Sort_NoDupA; auto.
+Qed.
 
 (** * Fold *)
 
@@ -1816,6 +1820,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma elements_3 : forall m, sort lt_key (elements m).  
  Proof. intros m; exact (@Raw.elements_sort elt m.(this) m.(is_bst)). Qed.
 
+ Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
+ Proof. intros m; exact (@Raw.elements_nodup elt m.(this) m.(is_bst)). Qed.
+
  Definition Equal cmp m m' := 
    (forall k, In k m <-> In k m') /\ 
    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index 6ad24f1cc..b5fe6722b 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -258,7 +258,13 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   apply alist_sorted_sort.
   apply alist_of_Map_sorts.
   Qed.
-  
+
+  Lemma elements_3w : NoDupA eq_key (elements m). 
+  Proof.
+  change eq_key with (@PE.eqk A).
+  apply PE.Sort_NoDupA; apply elements_3; auto.
+  Qed. 
+
   Lemma elements_1 : 
      MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
   Proof.
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index d4e07461c..c235976bd 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -161,6 +161,9 @@ Module Type S.
       Parameter elements_2 : 
         InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
       Parameter elements_3 : sort lt_key (elements m).  
+      (* We add artificially elements_3w, a weaker version of 
+         elements_3, for allowing FMapWeak < FMap subtyping. *)
+      Parameter elements_3w : NoDupA eq_key (elements m).  
 
     (** Specification of [fold] *)  
       Parameter fold_1 :
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 60a48396d..b2cedaabb 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -347,6 +347,13 @@ Proof.
  auto.
 Qed.
 
+Lemma elements_3w : forall m (Hm:Sort m), NoDupA eqk (elements m). 
+Proof. 
+ intros.
+ apply Sort_NoDupA.
+ apply elements_3; auto.
+Qed.
+
 (** * [fold] *)
 
 Function fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc:A) {struct m} :  A :=
@@ -1113,6 +1120,8 @@ Section Elt.
  Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed.
  Lemma elements_3 : forall m, sort lt_key (elements m).  
  Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(sorted)). Qed.
+ Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
+ Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(sorted)). Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c3bdc773b..7bf944b85 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -166,6 +166,7 @@ Qed.
 Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
+  Module ME:=KeyOrderedType E.
 
   Definition key := positive.
 
@@ -788,6 +789,12 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   apply xelements_sort; auto.
   Qed.
 
+  Lemma elements_3w : NoDupA eq_key (elements m).
+  Proof.
+  change eq_key with (@ME.eqk A).
+  apply ME.Sort_NoDupA; apply elements_3; auto.
+  Qed.
+
   End FMapSpec.
 
   (** [map] and [mapi] *)
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index e0f5e1c93..5d401126a 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -21,10 +21,12 @@ Require Export FMapWeakInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Facts (M: S).
+Module Facts (M:S)(D:DecidableType with Definition t:=M.E.t 
+                                   with Definition eq:=M.E.eq).
 Import M.
-Import Logic. (* to unmask [eq] *)  
-Import Peano. (* to unmask [lt] *)
+
+Notation eq_dec := D.eq_dec.
+Definition eqb x y := if eq_dec x y then true else false.
 
 Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), 
   MapsTo x e m -> MapsTo x e' m -> e=e'.
@@ -110,7 +112,7 @@ Lemma add_mapsto_iff : forall m x y e e',
 Proof. 
 intros.
 intuition.
-destruct (E.eq_dec x y); [left|right].
+destruct (eq_dec x y); [left|right].
 split; auto.
 symmetry; apply (MapsTo_fun (e':=e) H); auto with map.
 split; auto; apply add_3 with x e; auto.
@@ -121,10 +123,10 @@ Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m.
 Proof. 
 unfold In; split.
 intros (e',H).
-destruct (E.eq_dec x y) as [E|E]; auto.
+destruct (eq_dec x y) as [E|E]; auto.
 right; exists e'; auto.
 apply (add_3 E H).
-destruct (E.eq_dec x y) as [E|E]; auto.
+destruct (eq_dec x y) as [E|E]; auto.
 intros.
 exists e; apply add_1; auto.
 intros [H|(e',H)].
@@ -289,8 +291,6 @@ Ltac map_iff :=
 
 Section BoolSpec.
 
-Definition eqb x y := if E.eq_dec x y then true else false.
-
 Lemma mem_find_b : forall (elt:Set)(m:t elt)(x:key), mem x m = if find x m then true else false. 
 Proof.
 intros.
@@ -360,9 +360,9 @@ Qed.
 Hint Resolve add_neq_o : map.
 
 Lemma add_o : forall m x y e, 
- find y (add x e m) = if E.eq_dec x y then Some e else find y m.
+ find y (add x e m) = if eq_dec x y then Some e else find y m.
 Proof.
-intros; destruct (E.eq_dec x y); auto with map.
+intros; destruct (eq_dec x y); auto with map.
 Qed.
 
 Lemma add_eq_b : forall m x y e, 
@@ -381,7 +381,7 @@ Lemma add_b : forall m x y e,
  mem y (add x e m) = eqb x y || mem y m. 
 Proof.
 intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb.
-destruct (E.eq_dec x y); simpl; auto.
+destruct (eq_dec x y); simpl; auto.
 Qed.
 
 Lemma remove_eq_o : forall m x y, 
@@ -408,9 +408,9 @@ Qed.
 Hint Resolve remove_neq_o : map.
 
 Lemma remove_o : forall m x y, 
- find y (remove x m) = if E.eq_dec x y then None else find y m.
+ find y (remove x m) = if eq_dec x y then None else find y m.
 Proof.
-intros; destruct (E.eq_dec x y); auto with map.
+intros; destruct (eq_dec x y); auto with map.
 Qed.
 
 Lemma remove_eq_b : forall m x y, 
@@ -429,7 +429,7 @@ Lemma remove_b : forall m x y,
  mem y (remove x m) = negb (eqb x y) && mem y m.
 Proof.
 intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.
-destruct (E.eq_dec x y); auto.
+destruct (eq_dec x y); auto.
 Qed.
 
 Definition option_map (A:Set)(B:Set)(f:A->B)(o:option A) : option B := 
@@ -515,10 +515,10 @@ intros.
 assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)).
  intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff.
 assert (NoDupA (eq_key (elt:=elt)) (elements m)). 
- exact (elements_3 m).
-generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans E.eq_dec (elements m) x e H0).
+ exact (elements_3w m).
+generalize (fun e => @findA_NoDupA _ _ _ D.eq_sym D.eq_trans eq_dec (elements m) x e H0).
 unfold eqb.
-destruct (find x m); destruct (findA (fun y : E.t => if E.eq_dec x y then true else false) (elements m)); 
+destruct (find x m); destruct (findA (fun y:D.t => if eq_dec x y then true else false) (elements m)); 
  simpl; auto; intros.
 symmetry; rewrite <- H1; rewrite <- H; auto.
 symmetry; rewrite <- H1; rewrite <- H; auto.
@@ -538,12 +538,12 @@ rewrite InA_alt in He.
 destruct He as ((y,e'),(Ha1,Ha2)).
 compute in Ha1; destruct Ha1; subst e'.
 exists (y,e); split; simpl; auto.
-unfold eqb; destruct (E.eq_dec x y); intuition.
+unfold eqb; destruct (eq_dec x y); intuition.
 rewrite <- H; rewrite H0.
 destruct H1 as (H1,_).
 destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|].
 simpl in Ha2.
-unfold eqb in *; destruct (E.eq_dec x y); auto; try discriminate.
+unfold eqb in *; destruct (eq_dec x y); auto; try discriminate.
 exists e; rewrite InA_alt.
 exists (y,e); intuition.
 compute; auto.
@@ -554,8 +554,10 @@ End BoolSpec.
 End Facts.
 
 
-Module Properties (M: S).
- Module F:=Facts M. 
+Module Properties 
+ (M:S)(D:DecidableType with Definition t:=M.E.t 
+                       with Definition eq:=M.E.eq).
+ Module F:=Facts M D. 
  Import F.
  Import M.
 
@@ -623,8 +625,8 @@ Module Properties (M: S).
    intuition; eauto; congruence.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
   apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
   red; intros.
   do 2 rewrite InA_rev.
   destruct x; do 2 rewrite <- elements_mapsto_iff.
@@ -651,8 +653,8 @@ Module Properties (M: S).
   change (f x e (fold_right f' i (rev (elements m1))))
    with (f' (x,e) (fold_right f' i (rev (elements m1)))).
   apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
   rewrite InA_rev.
   swap H1.
   exists e.
@@ -663,7 +665,7 @@ Module Properties (M: S).
   do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
   rewrite H2.
   rewrite add_o.
-  destruct (E.eq_dec x a); intuition.
+  destruct (eq_dec x a); intuition.
   inversion H3; auto.
   f_equal; auto.
   elim H1.
@@ -735,7 +737,7 @@ Module Properties (M: S).
   destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
   assert (Add x e (remove x m) m).
    red; intros.
-   rewrite add_o; rewrite remove_o; destruct (E.eq_dec x y); eauto with map.
+   rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map.
   apply X0 with (remove x m) x e; auto with map.
   apply IHn; auto with map.
   assert (S n = S (cardinal (remove x m))).
diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v
index c4bfad59a..49dcb5214 100644
--- a/theories/FSets/FMapWeakInterface.v
+++ b/theories/FSets/FMapWeakInterface.v
@@ -19,7 +19,10 @@ Unset Strict Implicit.
 
 Module Type S.
 
-  Declare Module E : DecidableType.
+  (** The module E of base objects is meant to be a DecidableType
+     (and used to be so). But requiring only an EqualityType here
+     allows subtyping between FMap and FMapWeak *)
+  Declare Module E : EqualityType.
 
   Definition key := E.t.
 
@@ -149,7 +152,9 @@ Module Type S.
         MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
       Parameter elements_2 : 
         InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
-      Parameter elements_3 : NoDupA eq_key (elements m).  
+      (** When compared with ordered FMap, here comes the only 
+         property that is really weaker: *)
+      Parameter elements_3w : NoDupA eq_key (elements m).  
 
     (** Specification of [fold] *)  
       Parameter fold_1 :
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 76d2b9c3b..0afdf5d00 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -340,7 +340,7 @@ Proof.
 auto.
 Qed.
 
-Lemma elements_3 : forall m (Hm:NoDupA m), NoDupA (elements m). 
+Lemma elements_3w : forall m (Hm:NoDupA m), NoDupA (elements m). 
 Proof. 
  auto.
 Qed.
@@ -951,8 +951,8 @@ Section Elt.
  Proof. intros m; exact (@Raw.elements_1 elt m.(this)). Qed.
  Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
  Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed.
- Lemma elements_3 : forall m, NoDupA eq_key (elements m).  
- Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(NoDup)). Qed.
+ Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
+ Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(NoDup)). Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index fa10809cc..20fdae9fe 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1404,6 +1404,11 @@ Proof.
 Qed.
 Hint Resolve elements_sort.
 
+Lemma elements_nodup : forall s : tree, bst s -> NoDupA X.eq (elements s).
+Proof.
+ auto.
+Qed.
+
 (** * Filter *)
 
 Section F.
@@ -2886,6 +2891,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma elements_3 : sort E.lt (elements s).
  Proof. exact (Raw.elements_sort _ (is_bst s)). Qed.
 
+ Lemma elements_3w : NoDupA E.eq (elements s).
+ Proof. exact (Raw.elements_nodup _ (is_bst s)). Qed.
+
  Lemma min_elt_1 : min_elt s = Some x -> In x s. 
  Proof. exact (Raw.min_elt_1 s x). Qed.
  Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index c5656402f..993475757 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -478,6 +478,10 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Proof. 
     intros; unfold elements in |- *; case (M.elements s); firstorder.
   Qed.
+  Hint Resolve elements_3.
+ 
+  Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).
+  Proof. auto. Qed.
 
   Definition min_elt (s : t) : option elt :=
     match min_elt s with
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 4a99a44a3..5ff52495a 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -290,7 +290,7 @@ Qed.
 Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
 Proof.
 intros; rewrite singleton_b.
-unfold ME.eqb; destruct (ME.eq_dec x y); intuition.
+unfold eqb; destruct (eq_dec x y); intuition.
 Qed.
 
 Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index e83b861fb..7eb9b04f6 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -16,16 +16,22 @@
   Moreover, we prove that [E.Eq] and [Equal] are setoid equalities.
 *)
 
-Require Export FSetInterface. 
+Require Import DecidableTypeEx (*FSetWeakInterface*).
+Require Export FSetInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Facts (M: S).
-Module ME := OrderedTypeFacts M.E.  
-Import ME.
+Module Facts (M:S).
+Module D:=OT_as_DT M.E.
+(* To Do Later, switch to: 
+   Module Facts (M:FSetWeakInterface.S)
+                (D:DecidableType with Definition t:=M.E.t 
+                                 with Definition eq:=M.E.eq) *)
+Import M.E.
 Import M.
-Import Logic. (* to unmask [eq] *)  
-Import Peano. (* to unmask [lt] *)
+
+Notation eq_dec := D.eq_dec.
+Definition eqb x y := if eq_dec x y then true else false.
 
 (** * Specifications written using equivalences *)
 
@@ -258,8 +264,9 @@ apply H0; auto.
 symmetry.
 rewrite H0; intros.
 destruct H1 as (_,H1).
-apply H1; auto with set.
-apply elements_2; auto with set.
+apply H1; auto.
+rewrite H2.
+rewrite InA_alt; eauto.
 Qed.
 
 Lemma exists_b : compat_bool E.eq f -> 
@@ -272,7 +279,8 @@ destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros.
 rewrite <- H1; intros.
 destruct H0 as (H0,_).
 destruct H0 as (a,(Ha1,Ha2)); auto.
-exists a; intuition; auto with set.
+exists a; split; auto.
+rewrite H2; rewrite InA_alt; eauto.
 symmetry.
 rewrite H0.
 destruct H1 as (_,H1).
@@ -349,7 +357,9 @@ Qed.
 Add Morphism singleton : singleton_m.
 Proof.
 unfold Equal; intros x y H a.
-do 2 rewrite singleton_iff; split; order.
+do 2 rewrite singleton_iff; split; intros.
+apply E.eq_trans with x; auto.
+apply E.eq_trans with y; auto.
 Qed.
 
 Add Morphism add : add_m.
@@ -486,5 +496,15 @@ Qed.
 Add Morphism cardinal ; cardinal_m.
 *)
 
-
 End Facts.
+
+(* Two Annoying Things: 
+  1) Imports work strangly: 
+    After a (M:S)(E:DecidableType) and an Import M 
+    (which contains some E), then E.eq_dec is visible
+    even though it is not in M.E. 
+
+  2) Syntaxe of functor application forbids this: 
+  Module Facts (M:FSetInterface.S) := WeakFacts M (OT_as_DT M.E). 
+  Hence we cannot factor FSetWeakFacts and FSetFacts.
+*)
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index ded81426d..f701dcf12 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -247,6 +247,9 @@ Module Type S.
   Parameter elements_1 : In x s -> InA E.eq x (elements s).
   Parameter elements_2 : InA E.eq x (elements s) -> In x s.
   Parameter elements_3 : sort E.lt (elements s).  
+  (* We add artificially elements_3w, a weaker version of 
+     elements_3, for allowing FSetWeak < FSet subtyping. *)
+  Parameter elements_3w : NoDupA E.eq (elements s).
 
   (** Specification of [min_elt] *)
   Parameter min_elt_1 : min_elt s = Some x -> In x s. 
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index dd7effdb8..4393c67f7 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -649,6 +649,11 @@ Module Raw (X: OrderedType).
   unfold elements; auto.
   Qed.
 
+  Lemma elements_3w : forall (s : t) (Hs : Sort s), NoDupA E.eq (elements s).  
+  Proof. 
+  unfold elements; auto.
+  Qed.
+
   Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s. 
   Proof.
   intro s; case s; simpl; intros; inversion H; auto.
@@ -1233,6 +1238,8 @@ Module Make (X: OrderedType) <: S with Module E := X.
   Proof. exact (fun H => Raw.elements_2 H). Qed.
   Lemma elements_3 : sort E.lt (elements s).
   Proof. exact (Raw.elements_3 s.(sorted)). Qed.
+  Lemma elements_3w : NoDupA E.eq (elements s).
+  Proof. exact (Raw.elements_3w s.(sorted)). Qed.
 
   Lemma min_elt_1 : min_elt s = Some x -> In x s. 
   Proof. exact (fun H => Raw.min_elt_1 H). Qed.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index d6c978c05..2315dc532 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -29,19 +29,17 @@ Module Properties (M: S).
   Import ME. (* for ME.eq_dec *)
   Import M.E.
   Import M.
+  Module FM := Facts M.
+  Import FM.
   Import Logic. (* to unmask [eq] *)  
   Import Peano. (* to unmask [lt] *)
-  
-   (** Results about lists without duplicates *)
 
-  Module FM := Facts M.
-  Import FM.
+  (** Results about lists without duplicates *)
 
   Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
   Definition Above x s := forall y, In y s -> E.lt y x.
   Definition Below x s := forall y, In y s -> E.lt x y.
 
-
   Lemma In_dec : forall x s, {In x s} + {~ In x s}.
   Proof.
   intros; generalize (mem_iff s x); case (mem x s); intuition.
@@ -231,14 +229,14 @@ Module Properties (M: S).
    union (remove x s) (add x s') [=] union (add x s) (remove x s').
   Proof.
   unfold Equal; intros; set_iff.
-  destruct (ME.eq_dec x a); intuition.
+  destruct (eq_dec x a); intuition.
   Qed.
 
   Lemma union_remove_add_2 : In x s -> 
    union (remove x s) (add x s') [=] union s s'.
   Proof.
   unfold Equal; intros; set_iff.
-  destruct (ME.eq_dec x a); intuition.
+  destruct (eq_dec x a); intuition.
   left; eauto with set.
   Qed.
 
diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v
index 798a3f855..ff98648dc 100644
--- a/theories/FSets/FSetWeakFacts.v
+++ b/theories/FSets/FSetWeakFacts.v
@@ -16,14 +16,19 @@
   Moreover, we prove that [E.Eq] and [Equal] are setoid equalities.
 *)
 
+Require Import DecidableTypeEx.
 Require Export FSetWeakInterface. 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Facts (M: S).
+Module Facts 
+ (M:FSetWeakInterface.S)
+ (D:DecidableType with Definition t:=M.E.t with Definition eq:=M.E.eq).
 Import M.E.
 Import M.
-Import Logic. (* to unmask [eq] *)  
+
+Notation eq_dec := D.eq_dec.
+Definition eqb x y := if eq_dec x y then true else false.
 
 (** * Specifications written using equivalences *)
 
@@ -146,8 +151,6 @@ Ltac set_iff :=
 
 (**  * Specifications written using boolean predicates *)
 
-Definition eqb x y := if eq_dec x y then true else false.
-
 Section BoolSpec.
 Variable s s' s'' : t.
 Variable x y z : elt.
@@ -273,8 +276,7 @@ destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros.
 rewrite <- H1; intros.
 destruct H0 as (H0,_).
 destruct H0 as (a,(Ha1,Ha2)); auto.
-exists a; auto.
-split; auto.
+exists a; split; auto.
 rewrite H2; rewrite InA_alt; eauto.
 symmetry.
 rewrite H0.
@@ -296,14 +298,22 @@ Proof.
 constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
 Qed.
 
-Add Setoid elt E.eq E_ST as EltSetoid.
-
 Definition Equal_ST : Setoid_Theory t Equal.
 Proof. 
-constructor; unfold Equal; firstorder.
+constructor; [apply eq_refl | apply eq_sym | apply eq_trans].
 Qed.
 
-Add Setoid t Equal Equal_ST as EqualSetoid.
+Add Relation elt E.eq 
+ reflexivity proved by E.eq_refl 
+ symmetry proved by E.eq_sym
+ transitivity proved by E.eq_trans 
+ as EltSetoid.
+
+Add Relation t Equal 
+ reflexivity proved by eq_refl 
+ symmetry proved by eq_sym
+ transitivity proved by eq_trans 
+ as EqualSetoid.
 
 Add Morphism In with signature E.eq ==> Equal ==> iff as In_m.
 Proof.
@@ -344,9 +354,9 @@ Qed.
 Add Morphism singleton : singleton_m.
 Proof.
 unfold Equal; intros x y H a.
-do 2 rewrite singleton_iff; split.
-intros; apply E.eq_trans with x; auto.
-intros; apply E.eq_trans with y; auto.
+do 2 rewrite singleton_iff; split; intros.
+apply E.eq_trans with x; auto.
+apply E.eq_trans with y; auto.
 Qed.
 
 Add Morphism add : add_m.
@@ -402,6 +412,65 @@ rewrite H in H1; rewrite H0 in H1; intuition.
 rewrite H in H1; rewrite H0 in H1; intuition.
 Qed.
 
+
+(* [Subset] is a setoid order *)
+
+Lemma Subset_refl : forall s, s[<=]s.
+Proof. red; auto. Qed.
+
+Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.
+Proof. unfold Subset; eauto. Qed.
+
+Add Relation t Subset 
+ reflexivity proved by Subset_refl
+ transitivity proved by Subset_trans
+ as SubsetSetoid.
+
+Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
+Proof.
+unfold Subset, impl; intros; eauto with set.
+Qed.
+
+Add Morphism Empty with signature Subset --> impl as Empty_s_m.
+Proof. 
+unfold Subset, Empty, impl; firstorder.
+Qed.
+
+Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
+Proof.
+unfold Subset; intros x y H s s' H0 a.
+do 2 rewrite add_iff; rewrite H; intuition.
+Qed.
+
+Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m.
+Proof.
+unfold Subset; intros x y H s s' H0 a.
+do 2 rewrite remove_iff; rewrite H; intuition.
+Qed.
+
+Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite union_iff; intuition.
+Qed.
+
+Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite inter_iff; intuition.
+Qed.
+
+Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m.
+Proof.
+unfold Subset; intros s s' H s'' s''' H0 a.
+do 2 rewrite diff_iff; intuition.
+Qed.
+
+Add Morphism Subset with signature Subset --> Subset ++> impl as  Subset_s_m.
+Proof.
+unfold Subset, impl; auto.
+Qed.
+
 (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
    without additional hypothesis on [f]. For instance: *)
 
@@ -411,6 +480,12 @@ Proof.
 unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto.
 Qed.
 
+Lemma filter_subset : forall f, compat_bool E.eq f -> 
+  forall s s', s[<=]s' -> filter f s [<=] filter f s'.
+Proof.
+unfold Subset; intros; rewrite filter_iff in *; intuition.
+Qed.
+
 (* For [elements], [min_elt], [max_elt] and [choose], we would need setoid 
    structures on [list elt] and [option elt]. *)
 
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 3079ec871..5fa6c757f 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -23,7 +23,10 @@ Unset Strict Implicit.
 
 Module Type S.
 
-  Declare Module E : DecidableType.
+  (** The module E of base objects is meant to be a DecidableType
+     (and used to be so). But requiring only an EqualityType here
+     allows subtyping between FSet and FSetWeak *)
+  Declare Module E : EqualityType.
   Definition elt := E.t.
 
   Parameter t : Set. (** the abstract type of sets *)
@@ -68,6 +71,12 @@ Module Type S.
   Parameter diff : t -> t -> t.
   (** Set difference. *)
 
+  Definition eq : t -> t -> Prop := Equal.
+  (** EqualityType is a subset of this interface, but not 
+  DecidableType, in order to have FSetWeak < FSet. 
+  Hence no weak sets of weak sets in general, but it works 
+  at least with FSetWeakList.make that provides an eq_dec. *)
+
   Parameter equal : t -> t -> bool.
   (** [equal s1 s2] tests whether the sets [s1] and [s2] are
   equal, that is, contain equal elements. *)
@@ -121,12 +130,17 @@ Module Type S.
 
   Section Spec. 
 
-  Variable s s' : t.
+  Variable s s' s'': t.
   Variable x y : elt.
 
   (** Specification of [In] *)
   Parameter In_1 : E.eq x y -> In x s -> In y s.
- 
+
+  (** Specification of [eq] *)
+  Parameter eq_refl : eq s s. 
+  Parameter eq_sym : eq s s' -> eq s' s.
+  Parameter eq_trans : eq s s' -> eq s' s'' -> eq s s''.
+
   (** Specification of [mem] *)
   Parameter mem_1 : In x s -> mem x s = true.
   Parameter mem_2 : mem x s = true -> In x s. 
@@ -220,7 +234,9 @@ Module Type S.
   (** Specification of [elements] *)
   Parameter elements_1 : In x s -> InA E.eq x (elements s).
   Parameter elements_2 : InA E.eq x (elements s) -> In x s.
-  Parameter elements_3 : NoDupA E.eq (elements s).
+  (** When compared with ordered FSet, here comes the only 
+      property that is really weaker: *)
+  Parameter elements_3w : NoDupA E.eq (elements s).
 
   (** Specification of [choose] *)
   Parameter choose_1 : choose s = Some x -> In x s.
@@ -232,7 +248,7 @@ Module Type S.
     is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
     remove_2 singleton_2 union_1 union_2 union_3
     inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
-    partition_1 partition_2 elements_1 elements_3 
+    partition_1 partition_2 elements_1 elements_3w 
     : set.
   Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
     remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 0ca05c5d5..e45c2c343 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -287,7 +287,7 @@ Module Raw (X: DecidableType).
   unfold elements; auto.
   Qed.
  
-  Lemma elements_3 : forall (s : t) (Hs : NoDup s), NoDup (elements s).  
+  Lemma elements_3w : forall (s : t) (Hs : NoDup s), NoDup (elements s).  
   Proof. 
   unfold elements; auto.
   Qed.
@@ -732,22 +732,68 @@ Module Raw (X: DecidableType).
   generalize (Hrec H0 f).
   case (f x); case (partition f l); simpl; auto.
   Qed.
- 
+
   Definition eq : t -> t -> Prop := Equal.
 
-  Lemma eq_refl : forall s : t, eq s s. 
-  Proof. 
-  unfold eq, Equal; intuition.
-  Qed.
+  Lemma eq_refl : forall s, eq s s. 
+  Proof. firstorder. Qed.
 
-  Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s.
-  Proof. 
-  unfold eq, Equal; firstorder.
-  Qed.
+  Lemma eq_sym : forall s s', eq s s' -> eq s' s.
+  Proof. firstorder. Qed.
 
-  Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
-  Proof. 
-  unfold eq, Equal; firstorder.
+  Lemma eq_trans : 
+   forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
+  Proof. firstorder. Qed.
+
+  Definition eq_dec : forall (s s':t)(Hs:NoDup s)(Hs':NoDup s'), 
+   { eq s s' }+{ ~eq s s' }.
+  Proof.
+  unfold eq.
+  induction s; intros s'.
+  (* nil *)
+   destruct s'; [left|right].
+   firstorder.
+   unfold not, Equal.
+   intros H; generalize (H e); clear H.
+   rewrite InA_nil, InA_cons; intuition.
+  (* cons *)
+   intros.
+   case_eq (mem a s'); intros H; 
+    [ destruct (IHs (remove a s')) as [H'|H']; 
+      [ | | left|right]|right]; 
+    clear IHs.
+   inversion_clear Hs; auto.
+   apply remove_unique; auto.
+   (* In a s' /\ s [=] remove a s' *)
+   generalize (mem_2 H); clear H; intro H.
+   unfold Equal in *; intros b.
+   rewrite InA_cons; split.
+   destruct 1.
+   apply In_eq with a; auto.
+   rewrite H' in H0.
+   apply remove_3 with a; auto.
+   destruct (X.eq_dec b a); [left|right]; auto.
+   rewrite H'.
+   apply remove_2; auto.
+   (* In a s' /\ ~ s [=] remove a s' *)
+   generalize (mem_2 H); clear H; intro H.
+   swap H'.
+   unfold Equal in *; intros b.
+   split; intros.
+   apply remove_2; auto.
+   inversion_clear Hs.
+   swap H2; apply In_eq with b; auto.
+   rewrite <- H0; rewrite InA_cons; auto.
+   assert (In b s') by (apply remove_3 with a; auto).
+   rewrite <- H0, InA_cons in H2; destruct H2; auto.
+   elim (remove_1 Hs' (X.eq_sym H2) H1).
+   (* ~ In a s' *)
+   assert (~In a s').
+    red; intro H'; rewrite (mem_1 H') in H; discriminate.
+   swap H0.
+   unfold Equal in *.
+   rewrite <- H1.
+   rewrite InA_cons; auto.
   Qed.
 
   End ForNotations.
@@ -923,8 +969,8 @@ Module Make (X: DecidableType) <: S with Module E := X.
   Proof. exact (fun H => Raw.elements_1 H). Qed.
   Lemma elements_2 : InA E.eq x (elements s) -> In x s.
   Proof. exact (fun H => Raw.elements_2 H). Qed.
-  Lemma elements_3 : NoDupA E.eq (elements s).
-  Proof. exact (Raw.elements_3 s.(unique)). Qed.
+  Lemma elements_3w : NoDupA E.eq (elements s).
+  Proof. exact (Raw.elements_3w s.(unique)). Qed.
 
   Lemma choose_1 : choose s = Some x -> In x s.
   Proof. exact (fun H => Raw.choose_1 H). Qed.
@@ -933,4 +979,22 @@ Module Make (X: DecidableType) <: S with Module E := X.
 
  End Spec.
 
+ Definition eq : t -> t -> Prop := Equal.
+
+ Lemma eq_refl : forall s, eq s s. 
+ Proof. firstorder. Qed.
+
+ Lemma eq_sym : forall s s', eq s s' -> eq s' s.
+ Proof. firstorder. Qed.
+
+ Lemma eq_trans : 
+  forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
+ Proof. firstorder. Qed.
+
+ Definition eq_dec : forall (s s':t), 
+  { eq s s' }+{ ~eq s s' }.
+ Proof. 
+  intros s s'; exact (Raw.eq_dec s.(unique) s'.(unique)). 
+ Qed.
+
 End Make.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
index 07e087241..fa04b4fbf 100644
--- a/theories/FSets/FSetWeakProperties.v
+++ b/theories/FSets/FSetWeakProperties.v
@@ -27,19 +27,20 @@ Unset Strict Implicit.
 Hint Unfold transpose compat_op.
 Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
 
-Module Properties (M: S).
+Module Properties 
+ (M:FSetWeakInterface.S)
+ (D:DecidableType with Definition t:=M.E.t 
+                  with Definition eq:=M.E.eq).
   Import M.E.
   Import M.
+  Module FM := Facts M D.
+  Import FM.
   Import Logic. (* to unmask [eq] *)  
   Import Peano. (* to unmask [lt] *)
-  
-   (** Results about lists without duplicates *)
 
-  Module FM := Facts M.
-  Import FM.
+  (** Results about lists without duplicates *)
 
-  Definition Add (x : elt) (s s' : t) :=
-    forall y : elt, In y s' <-> E.eq x y \/ In y s.
+  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
 
   Lemma In_dec : forall x s, {In x s} + {~ In x s}.
   Proof.
@@ -52,21 +53,21 @@ Module Properties (M: S).
 
   Lemma equal_refl : forall s, s[=]s.
   Proof.
-  unfold Equal; intuition.
+  exact eq_refl.
   Qed.
 
   Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
   Proof.
-  unfold Equal; intros.
-  rewrite H; intuition.
+  exact eq_sym.
   Qed.
 
   Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
   Proof.
-  unfold Equal; intros.
-  rewrite H; exact (H0 a).
+  exact eq_trans.
   Qed.
 
+  Hint Immediate equal_refl equal_sym : set.
+
   Variable s s' s'' s1 s2 s3 : t.
   Variable x x' : elt.
 
@@ -74,22 +75,24 @@ Module Properties (M: S).
   
   Lemma subset_refl : s[<=]s. 
   Proof.
-  unfold Subset; intuition.
+  apply Subset_refl.
   Qed.
 
-  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
+  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
   Proof.
-  unfold Subset, Equal; intuition.
+  apply Subset_trans.
   Qed.
 
-  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
+  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
   Proof.
-  unfold Subset; intuition.
+  unfold Subset, Equal; intuition.
   Qed.
 
+  Hint Immediate subset_refl : set.
+
   Lemma subset_equal : s[=]s' -> s[<=]s'.
   Proof.
-  unfold Subset, Equal; firstorder.
+  unfold Subset, Equal; intros; rewrite <- H; auto.
   Qed.
 
   Lemma subset_empty : empty[<=]s.
@@ -120,7 +123,7 @@ Module Properties (M: S).
 
   Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
   Proof.
-  unfold Subset; intuition.
+  intros; rewrite <- H0; auto.
   Qed.
  
   Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
@@ -224,6 +227,21 @@ Module Properties (M: S).
   unfold Equal; intros; set_iff; tauto.
   Qed.
 
+  Lemma union_remove_add_1 : 
+   union (remove x s) (add x s') [=] union (add x s) (remove x s').
+  Proof.
+  unfold Equal; intros; set_iff.
+  destruct (eq_dec x a); intuition.
+  Qed.
+
+  Lemma union_remove_add_2 : In x s -> 
+   union (remove x s) (add x s') [=] union s s'.
+  Proof.
+  unfold Equal; intros; set_iff.
+  destruct (eq_dec x a); intuition.
+  left; eauto with set.
+  Qed.
+
   Lemma union_subset_1 : s [<=] union s s'.
   Proof.
   unfold Subset; intuition.
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index d59a9a354..ddee6c289 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -12,13 +12,6 @@ Require Export SetoidList.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(* TODO concernant la tactique order: 
-   * propagate_lt n'est sans doute pas complet
-   * un propagate_le
-   * exploiter les hypotheses negatives restant a la fin
-   * faire que ca marche meme quand une hypothese depend d'un eq ou lt.
-*) 
-
 (** * Ordered types *)
 
 Inductive Compare (X : Set) (lt eq : X -> X -> Prop) (x y : X) : Set :=
@@ -122,6 +115,13 @@ Module OrderedTypeFacts (O: OrderedType).
    intuition.
   Qed.
 
+(* TODO concernant la tactique order: 
+   * propagate_lt n'est sans doute pas complet
+   * un propagate_le
+   * exploiter les hypotheses negatives restant a la fin
+   * faire que ca marche meme quand une hypothese depend d'un eq ou lt.
+*) 
+
 Ltac abstraction := match goal with 
  (* First, some obvious simplifications *)
  | H : False |- _ => elim H