Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps

Thanks to Elie's work and especially "Include Type ...", full sets can
be simply expressed as extensions of weak sets. Moreover, Facts and
Properties functors can be factorized almost completely. As a result,
things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB,

Same with maps / weak maps ...

No backward compatibility intended for weak sets / maps, but porting
scripts should mostly amounts to name changes (see above). 




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

1 files changed, 914 insertions, 6 deletions

diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 89fae94e6..e0e83c57c 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -12,20 +12,928 @@
 
 (** This module proves many properties of finite sets that 
     are consequences of the axiomatization in [FsetInterface] 
-    Contrary to the functor in [FsetWeakProperties] it uses 
+    Contrary to the functor in [FsetProperties] it uses 
     sets operations instead of predicates over sets, i.e.
     [mem x s=true] instead of [In x s], 
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
 Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
 
-(** Since the properties that used to be there do not depend on 
-    the element ordering, we now simply import them from 
-    FSetWeakEqProperties *)
+Module WEqProperties (Import E:DecidableType)(M:WSfun E). 
+Module Import MP := WProperties E M.
+Import FM.
+Import M.
 
-Require FSetWeakEqProperties.
+Definition Add := MP.Add.
+
+Section BasicProperties. 
+
+(** Some old specifications written with boolean equalities. *) 
+
+Variable s s' s'': t.
+Variable x y z : elt.
+
+Lemma mem_eq: 
+  E.eq x y -> mem x s=mem y s.
+Proof. 
+intro H; rewrite H; auto.
+Qed.
+
+Lemma equal_mem_1: 
+  (forall a, mem a s=mem a s') -> equal s s'=true.
+Proof. 
+intros; apply equal_1; unfold Equal; intros.
+do 2 rewrite mem_iff; rewrite H; tauto.
+Qed.
+
+Lemma equal_mem_2: 
+  equal s s'=true -> forall a, mem a s=mem a s'.
+Proof. 
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma subset_mem_1: 
+  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
+Proof. 
+intros; apply subset_1; unfold Subset; intros a.
+do 2 rewrite mem_iff; auto.
+Qed.
+
+Lemma subset_mem_2: 
+  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
+Proof. 
+intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
+Qed.
+  
+Lemma empty_mem: mem x empty=false.
+Proof. 
+rewrite <- not_mem_iff; auto with set.
+Qed.
+
+Lemma is_empty_equal_empty: is_empty s = equal s empty.
+Proof. 
+apply bool_1; split; intros.
+rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
+rewrite <- is_empty_iff; auto with set.
+Qed.
+  
+Lemma choose_mem_1: choose s=Some x -> mem x s=true.
+Proof.  
+auto with set.
+Qed.
+
+Lemma choose_mem_2: choose s=None -> is_empty s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_mem_1: mem x (add x s)=true.
+Proof.
+auto with set.
+Qed.  
+ 
+Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
+Proof. 
+apply add_neq_b.
+Qed.
+
+Lemma remove_mem_1: mem x (remove x s)=false.
+Proof. 
+rewrite <- not_mem_iff; auto with set.
+Qed. 
+ 
+Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
+Proof. 
+apply remove_neq_b.
+Qed.
+
+Lemma singleton_equal_add: 
+  equal (singleton x) (add x empty)=true.
+Proof.
+rewrite (singleton_equal_add x); auto with set.
+Qed.  
+
+Lemma union_mem: 
+  mem x (union s s')=mem x s || mem x s'.
+Proof. 
+apply union_b.
+Qed.
+
+Lemma inter_mem: 
+  mem x (inter s s')=mem x s && mem x s'.
+Proof. 
+apply inter_b.
+Qed.
+
+Lemma diff_mem: 
+  mem x (diff s s')=mem x s && negb (mem x s').
+Proof. 
+apply diff_b.
+Qed.
+
+(** properties of [mem] *)
+
+Lemma mem_3 : ~In x s -> mem x s=false.
+Proof.
+intros; rewrite <- not_mem_iff; auto.
+Qed.
+
+Lemma mem_4 : mem x s=false -> ~In x s.
+Proof.
+intros; rewrite not_mem_iff; auto.
+Qed.
+
+(** Properties of [equal] *) 
+
+Lemma equal_refl: equal s s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma equal_sym: equal s s'=equal s' s.
+Proof.
+intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
+Qed.
+
+Lemma equal_trans: 
+ equal s s'=true -> equal s' s''=true -> equal s s''=true.
+Proof.
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma equal_equal: 
+ equal s s'=true -> equal s s''=equal s' s''.
+Proof.
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma equal_cardinal: 
+ equal s s'=true -> cardinal s=cardinal s'.
+Proof.
+auto with set.
+Qed.
+
+(* Properties of [subset] *)
+
+Lemma subset_refl: subset s s=true. 
+Proof.
+auto with set.
+Qed.
+
+Lemma subset_antisym: 
+ subset s s'=true -> subset s' s=true -> equal s s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma subset_trans: 
+ subset s s'=true -> subset s' s''=true -> subset s s''=true.
+Proof.
+do 3 rewrite <- subset_iff; intros.
+apply subset_trans with s'; auto.
+Qed.
+
+Lemma subset_equal: 
+ equal s s'=true -> subset s s'=true.
+Proof.
+auto with set.
+Qed.
+
+(** Properties of [choose] *)
+
+Lemma choose_mem_3: 
+ is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
+Proof.
+intros.
+generalize (@choose_1 s) (@choose_2 s).
+destruct (choose s);intros.
+exists e;auto with set.
+generalize (H1 (refl_equal None)); clear H1.
+intros; rewrite (is_empty_1 H1) in H; discriminate.
+Qed.
+
+Lemma choose_mem_4: choose empty=None.
+Proof.
+generalize (@choose_1 empty).
+case (@choose empty);intros;auto.
+elim (@empty_1 e); auto.
+Qed.
+
+(** Properties of [add] *)
+
+Lemma add_mem_3: 
+ mem y s=true -> mem y (add x s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_equal: 
+ mem x s=true -> equal (add x s) s=true.
+Proof.
+auto with set.
+Qed.
+
+(** Properties of [remove] *)
+
+Lemma remove_mem_3: 
+ mem y (remove x s)=true -> mem y s=true.
+Proof.
+rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
+Qed.
+
+Lemma remove_equal: 
+ mem x s=false -> equal (remove x s) s=true.
+Proof.
+intros; apply equal_1; apply remove_equal.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma add_remove: 
+ mem x s=true -> equal (add x (remove x s)) s=true.
+Proof.
+intros; apply equal_1; apply add_remove; auto with set.
+Qed.
+
+Lemma remove_add: 
+ mem x s=false -> equal (remove x (add x s)) s=true.
+Proof.
+intros; apply equal_1; apply remove_add; auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+(** Properties of [is_empty] *)
+
+Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
+Proof.
+intros; apply bool_1; split; intros.
+rewrite MP.cardinal_1; simpl; auto with set.
+assert (cardinal s = 0) by (apply zerob_true_elim; auto).
+auto with set.
+Qed.
+
+(** Properties of [singleton] *)
+
+Lemma singleton_mem_1: mem x (singleton x)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
+Proof.
+intros; rewrite singleton_b.
+unfold eqb; destruct (eq_dec x y); intuition.
+Qed.
+
+Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
+Proof.
+intros; apply singleton_1; auto with set.
+Qed.
+
+(** Properties of [union] *)
+
+Lemma union_sym:
+ equal (union s s') (union s' s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_equal: 
+ subset s s'=true -> equal (union s s') s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_equal_1: 
+ equal s s'=true-> equal (union s s'') (union s' s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_equal_2: 
+ equal s' s''=true-> equal (union s s') (union s s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_assoc: 
+ equal (union (union s s') s'') (union s (union s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_union_singleton: 
+ equal (add x s) (union (singleton x) s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_add: 
+ equal (union (add x s) s') (add x (union s s'))=true.
+Proof.
+auto with set.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma union_subset_1: subset s (union s s')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_2: subset s' (union s s')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_3:
+ subset s s''=true -> subset s' s''=true -> 
+  subset (union s s') s''=true.
+Proof.
+intros; apply subset_1; apply union_subset_3; auto with set.
+Qed.
+
+(** Properties of [inter] *) 
+
+Lemma inter_sym: equal (inter s s') (inter s' s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_equal: 
+ subset s s'=true -> equal (inter s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_equal_1: 
+ equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_equal_2: 
+ equal s' s''=true -> equal (inter s s') (inter s s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_assoc: 
+ equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_inter_1: 
+ equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_inter_2: 
+ equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_add_1: mem x s'=true -> 
+ equal (inter (add x s) s') (add x (inter s s'))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_add_2: mem x s'=false -> 
+ equal (inter (add x s) s') (inter s s')=true.
+Proof.
+intros; apply equal_1; apply inter_add_2.
+rewrite not_mem_iff; auto.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma inter_subset_1: subset (inter s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_2: subset (inter s s') s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_3:
+ subset s'' s=true -> subset s'' s'=true -> 
+  subset s'' (inter s s')=true.
+Proof.
+intros; apply subset_1; apply inter_subset_3; auto with set.
+Qed.
+
+(** Properties of [diff] *)
+
+Lemma diff_subset: subset (diff s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_subset_equal:
+ subset s s'=true -> equal (diff s s') empty=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma remove_inter_singleton: 
+ equal (remove x s) (diff s (singleton x))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_inter_empty:
+ equal (inter (diff s s') (inter s s')) empty=true. 
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_inter_all: 
+ equal (union (diff s s') (inter s s')) s=true.
+Proof.
+auto with set.
+Qed.
+
+End BasicProperties.
+
+Hint Immediate empty_mem is_empty_equal_empty add_mem_1
+   remove_mem_1 singleton_equal_add union_mem inter_mem
+   diff_mem equal_sym add_remove remove_add : set. 
+Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
+   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
+   subset_refl subset_equal subset_antisym
+   add_mem_3 add_equal remove_mem_3 remove_equal : set.
+
+
+(** General recursion principle *)
+
+Lemma set_rec:  forall (P:t->Type),
+ (forall s s', equal s s'=true -> P s -> P s') -> 
+ (forall s x, mem x s=false -> P s -> P (add x s)) -> 
+ P empty -> forall s, P s.
+Proof.
+intros.
+apply set_induction; auto; intros.
+apply X with empty; auto with set.
+apply X with (add x s0); auto with set.
+apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
+apply X0; auto with set; apply mem_3; auto.
+Qed.
+
+(** Properties of [fold] *)
+
+Lemma exclusive_set : forall s s' x,
+ ~(In x s/\In x s') <-> mem x s && mem x s'=false.
+Proof.
+intros; do 2 rewrite mem_iff.
+destruct (mem x s); destruct (mem x s'); intuition.
+Qed.
+
+Section Fold. 
+Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
+Variables (i:A).
+Variables (s s':t)(x:elt).
+ 
+Lemma fold_empty: (fold f empty i) = i.
+Proof. 
+apply fold_empty; auto.
+Qed.
+
+Lemma fold_equal: 
+ equal s s'=true -> eqA (fold f s i) (fold f s' i).
+Proof. 
+intros; apply fold_equal with (eqA:=eqA); auto with set.
+Qed.
+   
+Lemma fold_add: 
+ mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
+Proof. 
+intros; apply fold_add with (eqA:=eqA); auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma add_fold: 
+  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
+Proof.
+intros; apply add_fold with (eqA:=eqA); auto with set.
+Qed.
+
+Lemma remove_fold_1: 
+ mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
+Proof.
+intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
+Qed.
+
+Lemma remove_fold_2: 
+ mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
+Proof.
+intros; apply remove_fold_2 with (eqA:=eqA); auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma fold_union: 
+ (forall x, mem x s && mem x s'=false) -> 
+ eqA (fold f (union s s') i) (fold f s (fold f s' i)).
+Proof.
+intros; apply fold_union with (eqA:=eqA); auto.
+intros; rewrite exclusive_set; auto.
+Qed.
+
+End Fold.
+
+(** Properties of [cardinal] *)
+
+Lemma add_cardinal_1: 
+ forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_cardinal_2: 
+ forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
+Proof.
+intros; apply add_cardinal_2; auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma remove_cardinal_1: 
+ forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
+Proof.
+intros; apply remove_cardinal_1; auto with set.
+Qed.
+
+Lemma remove_cardinal_2: 
+ forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
+Proof.
+intros; apply Equal_cardinal; apply equal_2; auto with set.
+Qed.
+
+Lemma union_cardinal: 
+ forall s s', (forall x, mem x s && mem x s'=false) -> 
+ cardinal (union s s')=cardinal s+cardinal s'.
+Proof.
+intros; apply union_cardinal; auto; intros.
+rewrite exclusive_set; auto.
+Qed.
+
+Lemma subset_cardinal: 
+ forall s s', subset s s'=true -> cardinal s<=cardinal s'.
+Proof.
+intros; apply subset_cardinal; auto with set.
+Qed.
+
+Section Bool.
+
+(** Properties of [filter] *)
+
+Variable f:elt->bool.
+Variable Comp: compat_bool E.eq f.
+
+Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Proof.
+unfold compat_bool in *; intros; f_equal; auto.
+Qed.
+
+Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
+Proof. 
+intros; apply filter_b; auto.
+Qed.
+
+Lemma for_all_filter: 
+ forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
+Proof. 
+intros; apply bool_1; split; intros.
+apply is_empty_1.
+unfold Empty; intros. 
+rewrite filter_iff; auto.
+red; destruct 1.
+rewrite <- (@for_all_iff s f) in H; auto.
+rewrite (H a H0) in H1; discriminate.
+apply for_all_1; auto; red; intros.
+revert H; rewrite <- is_empty_iff.
+unfold Empty; intro H; generalize (H x); clear H.
+rewrite filter_iff; auto.
+destruct (f x); auto.
+Qed.
+
+Lemma exists_filter : 
+ forall s, exists_ f s=negb (is_empty (filter f s)).
+Proof. 
+intros; apply bool_1; split; intros. 
+destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
+apply bool_6.
+red; intros; apply (@is_empty_2 _ H0 a); auto with set.
+generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
+destruct (choose (filter f s)).
+intros H0 _; apply exists_1; auto.
+exists e; generalize (H0 e); rewrite filter_iff; auto.
+intros _ H0.
+rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
+Qed.
+
+Lemma partition_filter_1: 
+ forall s, equal (fst (partition f s)) (filter f s)=true.
+Proof. 
+auto with set.
+Qed.
+
+Lemma partition_filter_2: 
+ forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
+Proof. 
+auto with set.
+Qed.
+
+Lemma filter_add_1 : forall s x, f x = true -> 
+ filter f (add x s) [=] add x (filter f s). 
+Proof.
+red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+rewrite <- H; apply Comp; auto.
+Qed.
+
+Lemma filter_add_2 : forall s x, f x = false -> 
+ filter f (add x s) [=] filter f s. 
+Proof.
+red; intros; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+assert (f x = f a) by (apply Comp; auto).
+rewrite H in H1; rewrite H2 in H1; discriminate.
+Qed.
+
+Lemma add_filter_1 : forall s s' x, 
+ f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
+Proof.
+unfold Add, MP.Add; intros.
+repeat rewrite filter_iff; auto.
+rewrite H0; clear H0.
+assert (E.eq x y -> f y = true) by 
+ (intro H0; rewrite <- (Comp _ _ H0); auto).
+tauto.
+Qed.
+
+Lemma add_filter_2 : forall s s' x, 
+ f x=false -> (Add x s s') -> filter f s [=] filter f s'.
+Proof.
+unfold Add, MP.Add, Equal; intros.
+repeat rewrite filter_iff; auto.
+rewrite H0; clear H0.
+assert (f a = true -> ~E.eq x a).
+ intros H0 H1.
+ rewrite (Comp _ _ H1) in H.
+ rewrite H in H0; discriminate.
+tauto. 
+Qed.
+
+Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
+  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
+Proof.
+clear Comp' Comp f.
+intros.
+assert (compat_bool E.eq (fun x => orb (f x) (g x))).
+  unfold compat_bool; intros.
+  rewrite (H x y H1);  rewrite (H0 x y H1); auto.
+unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
+assert (f a || g a = true <-> f a = true \/ g a = true).
+  split; auto with bool.
+  intro H3; destruct (orb_prop _ _ H3); auto.
+tauto.
+Qed.
+
+Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
+Proof.
+unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
+(** Properties of [for_all] *)
+
+Lemma for_all_mem_1: forall s, 
+ (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
+Proof.
+intros.
+rewrite for_all_filter; auto.
+rewrite is_empty_equal_empty.
+apply equal_mem_1;intros.
+rewrite filter_b; auto.
+rewrite empty_mem.
+generalize (H a); case (mem a s);intros;auto.
+rewrite H0;auto.
+Qed.
+
+Lemma for_all_mem_2: forall s, 
+ (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
+Proof.
+intros.
+rewrite for_all_filter in H; auto.
+rewrite is_empty_equal_empty in H.
+generalize (equal_mem_2 _ _ H x).
+rewrite filter_b; auto.
+rewrite empty_mem.
+rewrite H0; simpl;intros.
+replace true with (negb false);auto;apply negb_sym;auto.
+Qed.
+
+Lemma for_all_mem_3: 
+ forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
+Proof.
+intros.
+apply (bool_eq_ind (for_all f s));intros;auto.
+rewrite for_all_filter in H1; auto.
+rewrite is_empty_equal_empty in H1.
+generalize (equal_mem_2 _ _ H1 x).
+rewrite filter_b; auto.
+rewrite empty_mem.
+rewrite H.
+rewrite H0.
+simpl;auto.
+Qed.
+
+Lemma for_all_mem_4: 
+ forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
+Proof.
+intros.
+rewrite for_all_filter in H; auto.
+destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
+exists x.
+rewrite filter_b in H1; auto.
+elim (andb_prop _ _ H1).
+split;auto.
+replace false with (negb true);auto;apply negb_sym;auto.
+Qed.
+
+(** Properties of [exists] *)
+
+Lemma for_all_exists: 
+ forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
+Proof.
+intros.
+rewrite for_all_b; auto.
+rewrite exists_b; auto.
+induction (elements s); simpl; auto.
+destruct (f a); simpl; auto.
+Qed.
+
+End Bool.
+Section Bool'.
+
+Variable f:elt->bool.
+Variable Comp: compat_bool E.eq f.
+
+Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Proof.
+unfold compat_bool in *; intros; f_equal; auto.
+Qed.
+
+Lemma exists_mem_1: 
+ forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
+Proof.
+intros.
+rewrite for_all_exists; auto.
+rewrite for_all_mem_1;auto with bool.
+intros;generalize (H x H0);intros. 
+symmetry;apply negb_sym;simpl;auto.
+Qed.
+
+Lemma exists_mem_2: 
+ forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
+Proof.
+intros.
+rewrite for_all_exists in H; auto.
+replace false with (negb true);auto;apply negb_sym;symmetry.
+rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
+replace true with (negb false);auto;apply negb_sym;auto.
+Qed.
+
+Lemma exists_mem_3: 
+ forall s x, mem x s=true -> f x=true -> exists_ f s=true.
+Proof.
+intros.
+rewrite for_all_exists; auto.
+symmetry;apply negb_sym;simpl.
+apply for_all_mem_3 with x;auto.
+rewrite H0;auto.
+Qed.
+
+Lemma exists_mem_4: 
+ forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
+Proof.
+intros.
+rewrite for_all_exists in H; auto.
+elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
+elim p;intros.
+exists x;split;auto.
+replace true with (negb false);auto;apply negb_sym;auto.
+replace false with (negb true);auto;apply negb_sym;auto.
+Qed.
+
+End Bool'.
+
+Section Sum.
+
+(** Adding a valuation function on all elements of a set. *)
+
+Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
+Notation compat_opL := (compat_op E.eq (@Logic.eq _)).
+Notation transposeL := (transpose (@Logic.eq _)).
+
+Lemma sum_plus : 
+  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
+    forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
+Proof.
+unfold sum.
+intros f g Hf Hg.
+assert (fc : compat_opL (fun x:elt =>plus (f x))).  auto.
+assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
+assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
+assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
+assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
+assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
+assert (st := gen_st nat).
+intros s;pattern s; apply set_rec.
+intros.
+rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
+intros; do 3 (rewrite (fold_add _ _ st);auto).
+rewrite H0;simpl;omega.
+do 3 rewrite fold_empty;auto.
+Qed.
+
+Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
+  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
+Proof.
+unfold sum; intros f Hf.
+assert (st := gen_st nat).
+assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). 
+ red; intros.
+ rewrite (Hf x x' H); auto.
+assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
+ red; intros; omega.
+intros s;pattern s; apply set_rec.
+intros.
+change elt with E.t.
+rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
+rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
+intros; rewrite (fold_add _ _ st _ cc ct); auto.
+generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
+assert (~ In x (filter f s0)).
+ intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
+case (f x); simpl; intros.
+rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
+rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
+intros; rewrite fold_empty;auto.
+rewrite MP.cardinal_1; auto.
+unfold Empty; intros.
+rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
+Lemma fold_compat : 
+  forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
+  (f g:elt->A->A),
+  (compat_op E.eq eqA f) -> (transpose eqA f) -> 
+  (compat_op E.eq eqA g) -> (transpose eqA g) -> 
+  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
+  (eqA (fold f s i) (fold g s i)).
+Proof.
+intros A eqA st f g fc ft gc gt i.
+intro s; pattern s; apply set_rec; intros.
+trans_st (fold f s0 i).
+apply fold_equal with (eqA:=eqA); auto.
+rewrite equal_sym; auto.
+trans_st (fold g s0 i).
+apply H0; intros; apply H1; auto with set.
+elim  (equal_2 H x); auto with set; intros.
+apply fold_equal with (eqA:=eqA); auto with set.
+trans_st (f x (fold f s0 i)).
+apply fold_add with (eqA:=eqA); auto with set.
+trans_st (g x (fold f s0 i)); auto with set.
+trans_st (g x (fold g s0 i)); auto with set.
+sym_st; apply fold_add with (eqA:=eqA); auto.
+do 2 rewrite fold_empty; refl_st.
+Qed.
+
+Lemma sum_compat : 
+  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
+  forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
+intros.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
+red; intros; omega.
+red; intros; omega.
+Qed.
+
+End Sum.
+
+End WEqProperties.
+
+
+(** Now comes a special version dedicated to full sets. For this
+    one, only one argument [(M:S)] is necessary. *)
 
 Module EqProperties (M:S).
   Module D := OT_as_DT M.E.
-  Include FSetWeakEqProperties.EqProperties M D.
+  Include WEqProperties D M.
 End EqProperties.