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

1 files changed, 7 insertions, 0 deletions

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.