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, 88 insertions, 13 deletions

diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v
index 798a3f8559..ff98648dc5 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]. *)