suppression de FSets (redevient une contrib)

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

1 files changed, 0 insertions, 1727 deletions

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
deleted file mode 100644
index ad27ff3262..0000000000
--- a/theories/FSets/FSetProperties.v
+++ /dev/null
@@ -1,1727 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** This module proves many properties of finite sets that 
-    are consequences of the axiomatization in [FSetInterface] *) 
-
-Require Omega.
-
-Import nat_scope.
-Open Scope nat_scope.
-
-Require Export FSetInterface. 
-Require Export Bool.
-Require Export Sumbool.
-Require Export Zerob. 
-Set Implicit Arguments.
-
-Section Misc.
-Variable A,B : Set.
-Variable eqA : A -> A -> Prop. 
-Variable eqB : B -> B -> Prop.
-
-(** Two-argument functions that allow to reorder its arguments. *)
-Definition transpose := [f:A->B->B](x,y:A)(z:B)(eqB (f x (f y z)) (f y (f x z))). 
-
-(** Compatibility of a two-argument function with respect to two equalities. *)
-Definition compat_op := [f:A->B->B](x,x':A)(y,y':B)(eqA x x') -> (eqB y y') -> 
- (eqB (f x y) (f x' y')).
-
-(** Compatibility of a function upon natural numbers. *)
-Definition compat_nat := [f:A->nat] (x,x':A)(eqA x x') -> (f x)=(f x').
-
-End Misc.
-Hints Unfold transpose compat_op compat_nat.
-
-(* For proving (Setoid_Theory ? (eq ?)) *)
-Tactic Definition ST :=
-  Constructor; Intros;[ Trivial | Symmetry; Trivial | EApply trans_eq; EAuto ].
-Hint st : core := Extern 1 (Setoid_Theory ? (eq ?)) ST.
-
-Definition gen_st : (A:Set)(Setoid_Theory ? (eq A)).
-Auto.
-Qed.
-
-Module Properties [M:S].
-  Import M.
-  Import Logic. (* for unmasking eq. *)  
-  Import Peano. (* for unmasking lt *)
-  
-  Module ME := MoreOrderedType E.  
-
-  Section Old_Spec_Now_Properties. 
-
-  (* Usual syntax for lists. 
-   CAVEAT: the Coq cast "::" will no longer be available. *)
-  Notation "[]" := (nil ?) (at level 1).
-  Notation "a :: l" := (cons a l) (at level 1, l at next level).
-
-   Section Unique_Remove.
-   (** auxiliary results used in the alternate [fold] specification [fold_1] and [fold_2]. *)
-
-   Fixpoint remove_list [x:elt;s:(list elt)] : (list elt) := Cases s of 
-      nil => []
-    | (cons y l) => if (ME.eq_dec x y) then [_]l else [_]y::(remove_list x l)
-   end. 
-
-   Lemma remove_list_correct : 
-    (s:(list elt))(x:elt)(Unique E.eq s) -> 
-    (Unique E.eq (remove_list x s)) /\ 
-    ((y:elt)(InList E.eq y (remove_list x s))<->(InList E.eq y s)/\~(E.eq x y)).
-   Proof.
-   Induction s; Simpl.
-   Split; Auto.
-   Intuition.
-   Inversion H0.
-   Intros; Inversion_clear H0; Case (ME.eq_dec x a); Trivial.  
-   Intuition.
-   Apply H1; EApply ME.In_eq with y; EAuto.
-   Inversion_clear H3; Auto.
-   Elim H4; EAuto. 
-   Elim (H x H2); Intros.
-   Split.
-   Elim (H3 a); Constructor; Intuition.
-   Intro y; Elim (H3 y); Clear H3; Intros.
-   Intuition.  
-   Inversion_clear H4; Auto.
-   Elim (H3 H6); Auto.
-   Inversion_clear H4; Auto.
-   Intuition EAuto.
-   Elim (H3 H7); Ground.
-   Inversion_clear H6; Ground. 
-   Qed. 
-
-   Local ListEq := [l,l'](y:elt)(InList E.eq y l)<->(InList E.eq y l').
-   Local ListAdd := [x,l,l'](y:elt)(InList E.eq y l')<->(E.eq y x)\/(InList E.eq y l).
-
-   Lemma remove_list_equal : 
-    (s,s':(list elt))(x:elt)(Unique E.eq x::s) -> (Unique E.eq s') -> 
-    (ListEq x::s s') -> (ListEq s (remove_list x s')).
-   Proof.  
-   Unfold ListEq; Intros. 
-   Inversion_clear H.
-   Elim (remove_list_correct x H0); Intros.
-   Elim (H4 y); Intros.
-   Elim (H1 y); Intros.
-   Split; Intros.
-   Apply H6; Split; Auto. 
-   Intro.
-   Elim H2; Apply ME.In_eq with y; EAuto.
-   Elim (H5 H9); Intros.
-   Assert H12 := (H8 H10). 
-   Inversion_clear H12; Auto.
-   Elim H11; EAuto. 
-   Qed. 
-
-   Lemma remove_list_add : 
-    (s,s':(list elt))(x,x':elt)(Unique E.eq s) -> (Unique E.eq x'::s') -> 
-    ~(E.eq x x') -> ~(InList E.eq x s) -> 
-    (ListAdd x s x'::s') -> (ListAdd x (remove_list x' s) s').
-   Proof.
-   Unfold ListAdd; Intros.
-   Inversion_clear H0.
-   Elim (remove_list_correct x' H); Intros.
-   Elim (H6 y); Intros.
-   Elim (H3 y); Intros.
-   Split; Intros.
-   Elim H9; Auto; Intros.
-   Elim (ME.eq_dec y x); Auto; Intros.
-   Right; Apply H8; Split; Auto.
-   Intro; Elim H4; Apply ME.In_eq with y; Auto.
-   Inversion_clear H11.
-   Assert (InList E.eq y x'::s'). Auto.
-   Inversion_clear H11; Auto.
-   Elim H1; EAuto.
-   Elim (H7 H12); Intros.
-   Assert (InList E.eq y x'::s'). Auto.
-   Inversion_clear H14; Auto.
-   Elim H13; Auto. 
-   Qed.
-
-   Lemma remove_list_fold_right : 
-    (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
-    (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) -> 
-    (s:(list elt))(x:elt)(Unique E.eq s) -> (InList E.eq x s) -> 
-    (eqA (fold_right f i s) (f x (fold_right f i (remove_list x s)))).
-   Proof.
-   Induction s; Simpl.  
-   Intros; Inversion H2.
-   Intros.
-   Inversion_clear H2.
-   Case  (ME.eq_dec x a); Simpl; Intros.
-   Apply H; Auto. 
-   Apply Seq_refl; Auto. 
-   Inversion_clear H3. 
-   Elim n; Auto.
-   Apply (Seq_trans ?? st) with (f a (f x (fold_right f i (remove_list x l)))).
-   Apply H; Auto.
-   Apply H0; Auto.
-   Qed.   
-
-   Lemma fold_right_equal : 
-    (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
-    (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) -> 
-    (s,s':(list elt))(Unique E.eq s) -> (Unique E.eq s') -> (ListEq s s') -> 
-    (eqA (fold_right f i s) (fold_right f i s')).
-   Proof.
-   Induction s.
-   Intro s'; Case s'; Simpl. 
-   Intros; Apply Seq_refl; Auto.
-   Unfold ListEq; Intros.
-   Elim (H3 e); Intros. 
-   Assert X : (InList E.eq e []); Auto; Inversion X.
-   Intros x l Hrec s' U U' E.
-   Simpl.   
-   Apply (Seq_trans ?? st) with (f x (fold_right f i (remove_list x s'))).
-   Apply H; Auto.
-   Apply Hrec; Auto.
-   Inversion U; Auto.
-   Elim (remove_list_correct x U'); Auto.
-   Apply remove_list_equal; Auto.
-   Apply Seq_sym; Auto.
-   Apply remove_list_fold_right with eqA:=eqA; Auto.
-   Unfold ListEq in E; Ground.
-   Qed.
-
-   Lemma fold_right_add : 
-    (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
-    (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) -> 
-    (s',s:(list elt))(x:elt)(Unique E.eq s) -> (Unique E.eq s') -> ~(InList E.eq x s) -> 
-    (ListAdd x s s') -> 
-    (eqA (fold_right f i s') (f x (fold_right f i s))).
-   Proof.   
-   Induction s'.
-   Unfold ListAdd; Intros.
-   Elim (H4 x); Intros. 
-   Assert X : (InList E.eq x []); Auto; Inversion X.
-   Intros x' l' Hrec s x U U' IN EQ; Simpl.
-   (* if x=x' *)
-   Case (ME.eq_dec x x'); Intros.
-   Apply H; Auto.
-   Apply fold_right_equal with eqA:=eqA; Auto.
-   Inversion_clear U'; Trivial.
-   Unfold ListEq; Unfold ListAdd in EQ.
-   Intros. 
-   Elim (EQ y); Intros.
-   Split; Intros.
-   Elim H1; Auto.
-   Intros; Inversion_clear U'.
-   Elim H5; Apply ME.In_eq with y; EAuto.
-   Assert (InList E.eq y x'::l'); Auto; Inversion_clear H4; Auto.
-   Elim IN; Apply ME.In_eq with y; EAuto.
-   (* else x<>x' *)   
-   Apply (Seq_trans ?? st) with (f x' (f x (fold_right f i (remove_list x' s)))).
-   Apply H; Auto.
-   Apply Hrec; Auto.
-   Elim (remove_list_correct x' U); Auto.
-   Inversion_clear U'; Auto.
-   Elim (remove_list_correct x' U); Intros; Intro.
-   Ground.
-   Apply remove_list_add; Auto.
-   Apply (Seq_trans ?? st) with (f x (f x' (fold_right f i (remove_list x' s)))).
-   Apply H0; Auto.
-   Apply H; Auto.
-   Apply Seq_sym; Auto.
-   Apply remove_list_fold_right with eqA:=eqA; Auto.
-   Elim (EQ x'); Intros. 
-   Elim H1; Auto; Intros; Elim n; Auto.
-   Qed.
-
-  End Unique_Remove.
-
-  (** An alternate (and previous) specification for [fold] was based on the recursive 
-      structure of a set. It is now lemmas [fold_1] and [fold_2]. *)
-
-  Lemma fold_1:
-   (s:t)(A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))(i:A)(f:elt->A->A)
-   (Empty s) -> (eqA (fold f s i) i).
-  Proof.
-  Intros; Elim (M.fold_1 s i f); Intros l (H1,(H2,H3)).
-  Rewrite H3; Clear H3.
-  Unfold Empty in H; Generalize H H2; Clear H H2; Case l; Simpl; Intros.
-  Apply Seq_refl; Trivial.
-  Elim (H e).
-  Elim (H2 e); Intuition. 
-  Qed.
-
-  Lemma fold_2 : 
-     (s,s':t)(x:elt)(A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
-     (i:A)(f:elt->A->A)(compat_op E.eq eqA f) -> (transpose eqA f) -> ~(In x s) -> 
-     (Add x s s') -> (eqA (fold f s' i) (f x (fold f s i))).
-  Proof.
-  Intros; Elim (M.fold_1 s i f); Intros l (Hl,(Hl1,Hl2)).
-  Elim (M.fold_1 s' i f); Intros l' (Hl',(Hl'1,Hl'2)).
-  Rewrite Hl2; Clear Hl2.
-  Rewrite Hl'2; Clear Hl'2.
-  Assert (y:elt)(InList E.eq y l')<->(E.eq y x)\/(InList E.eq y l).
-   Intros; Elim (H2 y); Intros; Split; 
-    Elim (Hl1 y); Intros; Elim (Hl'1 y); Intuition.
-  Assert ~(InList E.eq x l).
-   Intro; Elim H1; Ground.
-  Clear H1 H2 Hl'1 Hl1 H1 s' s.
-  Apply fold_right_add with eqA:=eqA; Auto.
-  Qed.
-
-  (** idem, for [cardinal. *)
-
-  Lemma cardinal_fold : (s:t)(cardinal s)=(fold [_]S s O).
-  Proof.
-  Intros; Elim (M.cardinal_1 s); Intros l (Hl,(Hl1,Hl2)).
-  Elim (M.fold_1 s O [_]S); Intros l' (Hl',(Hl'1,Hl'2)).
-  Rewrite Hl2; Rewrite Hl'2; Clear Hl2 Hl'2.
-  Assert (l:(list elt))(length l)=(fold_right [_]S O l).
-   Induction l0; Simpl; Auto.
-  Rewrite H.
-  Apply fold_right_equal with eqA:=(eq nat); Auto; Ground.
-  Qed.
-
-  Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O.
-  Proof.
-  Intros; Rewrite cardinal_fold; Apply fold_1; Auto.
-  Qed.
-
-  Lemma cardinal_2 : 
-    (s,s':t)(x:elt)~(In x s) -> (Add  x s s') -> (cardinal s') = (S (cardinal s)).
-  Proof.
-  Intros; Do 2 Rewrite cardinal_fold.
-  Change S with ([_]S x).
-  Apply fold_2 with eqA:=(eq nat); Auto.
-  Qed.
-
-  Hints Resolve cardinal_1 cardinal_2.
-
-  (** Other old specifications written with boolean equalities. *) 
-
-  Variable s,s' : t.
-  Variable x,y,z : elt.
-
-  Lemma mem_eq: 
-    (E.eq x y) -> (mem x s)=(mem y s).
-  Proof. 
-  Intros; Apply bool_1.
-  Generalize (!mem_1 s x) (!mem_1 s y) (!mem_2 s x) (!mem_2 s y).
-  Intuition. 
-  EAuto.
-  Apply H0; Apply In_1 with y; Auto.
-  Qed.
-
-  Lemma equal_mem_1: 
-    ((a:elt)(mem a s)=(mem a s')) -> (equal s s')=true.
-  Proof. 
-  Intros; Apply equal_1; Unfold Equal; Intuition; EAuto.
-  Qed.
-
-  Lemma equal_mem_2: 
-    (equal s s')=true -> (a:elt)(mem a s)=(mem a s').
-  Proof. 
-  Intros; Apply bool_1.
-  Intros; Cut (Equal s s'); [Clear H; Unfold Equal|Auto].
-  Intros H; Generalize (H a); Intuition.
-  Qed.
-
-  Lemma subset_mem_1: 
-    ((a:elt)(mem a s)=true->(mem a s')=true) -> (subset s s')=true.
-  Proof. 
-  Intros; Apply subset_1; Unfold Subset; Intuition; EAuto.
-  Qed.
-
-  Lemma subset_mem_2: 
-    (subset s s')=true -> (a:elt)(mem a s)=true -> (mem a s')=true.
-  Proof. 
-  Intros; Apply bool_1.
-  Cut (Subset s s'); [Clear H; Unfold Subset|Auto].
-  Intros H; Generalize (H a); Intuition.
-  Qed.
-  
-  Lemma empty_mem: (mem x empty)=false.
-  Proof. 
-  Apply not_true_is_false; Intro; Absurd (In x empty); Auto.
-  Qed.
-
-  Lemma is_empty_equal_empty: (is_empty s)=(equal s empty).
-  Proof. 
-  Generalize empty_1 (!is_empty_1 s) (!is_empty_2 s) 
-            (!equal_1 s empty) (!equal_2 s empty).
-  Unfold Empty Equal.
-  Case (is_empty s); Case (equal s empty); Intuition.
-  Clear H3 H1.
-  Symmetry; Apply H2; Intuition.
-  Generalize (H4 a); Intuition.
-  Generalize (H a); Intuition.
-  Clear H1 H3.
-  Apply H0; Intuition.
-  Generalize (H4 a); Intuition.
-  Generalize (H a); Intuition.
-  Qed.
-  
-  Lemma choose_mem_1: (choose s)=(Some ? x) -> (mem x s)=true.
-  Proof.  
-  Auto.
-  Qed.
-
-  Lemma choose_mem_2: (choose s)=(None ?) -> (is_empty s)=true.
-  Proof.
-  Auto.
-  Qed.
-
-  Lemma add_mem_1: (mem x (add x s))=true.
-  Proof.
-  Auto.
-  Qed.  
- 
-  Lemma add_mem_2: 
-  ~ (E.eq x y) -> (mem y (add x s))=(mem y s).
-  Proof. 
-  Intros; Apply bool_1; Intuition; EAuto.
-  Qed.
-
-  Lemma remove_mem_1: (mem x (remove x s))=false.
-  Proof. 
-  Apply not_true_is_false; Intro; Absurd (In x (remove x s)); Auto.
-  Qed. 
- 
-  Lemma remove_mem_2: 
-  ~ (E.eq x y) -> (mem y (remove x s))=(mem y s).
-  Proof. 
-  Intros; Apply bool_1; Intuition; EAuto. 
-  Qed.
-
-  Lemma singleton_equal_add: 
-    (equal (singleton x) (add x empty))=true.
-  Proof.
-  Apply equal_1; Unfold Equal; Intuition.
-  Apply In_1 with x; Auto.
-  Assert (E.eq a x); Auto.
-  Elim (ME.eq_dec a x); Auto.
-  Intros; Assert (In a empty). 
-  EApply add_3; EAuto.  
-  Generalize (empty_1 H0); Intuition.
-  Qed.  
-
-  Lemma union_mem: 
-    (mem x (union s s'))=(orb (mem x s) (mem x s')).
-  Proof. 
-  Apply bool_1; Intuition.
-  Elim (!union_1 s s' x); Intuition.
-  Elim (orb_prop ? ? H); Intuition.
-  Qed.
-
-  Lemma inter_mem: 
-    (mem x (inter s s'))=(andb (mem x s) (mem x s')).
-  Proof. 
-  Apply bool_1; Intuition.
-  Apply andb_true_intro; Intuition EAuto.
-  Elim (andb_prop ?? H); Intuition.
-  Qed.
-
-  Lemma diff_mem: 
-    (mem x (diff s s'))=(andb (mem x s) (negb (mem x s'))).
-  Proof. 
-  Generalize (!diff_1 s s' x) (!diff_2 s s' x) (!diff_3 s s' x).
-  LetTac s0 := (diff s s').
-  Generalize (!mem_1 s x) (!mem_1 s' x) (!mem_1 s0 x) 
-             (!mem_2 s x) (!mem_2 s' x) (!mem_2 s0 x).
-  Case (mem x s); Case (mem x s'); Case (mem x s0); Intuition.
-  Qed.
-
-  Section Cardinal.
-  
-  Lemma Add_add : 
-    (s:t)(x:elt)(Add x s (add x s)).
-  Proof.
-    Unfold Add; Intros; Intuition.
-    Elim (ME.eq_dec x0 y0); Intros; Auto.
-    Right.
-    EApply add_3; EAuto.
-    Apply In_1 with x0; Auto. 
-  Qed.
-
-  Lemma Add_remove : (s:t)(x:elt)(In x s) -> (Add x (remove x s) s). 
-  Proof. 
-    Intros; Unfold Add; Intuition.
-    Elim (ME.eq_dec x0 y0); Intros; Auto.
-    Apply In_1 with x0; Auto.
-    EAuto.
-  Qed.
- 
-  Hints Resolve Add_add Add_remove. 
-
-  Lemma Equal_remove : (s,s':t)(x:elt)(In x s)->(Equal s s')-> 
-     (Equal (remove x s) (remove x s')).
-  Proof.
-     Unfold Equal; Intros.
-     Elim (ME.eq_dec x0 a); Intros; Auto. 
-     Split; Intros.
-     Absurd (In x0 (remove x0 s0)); Auto; Apply In_1 with a; Auto.
-     Absurd (In x0 (remove x0 s'0)); Auto; Apply In_1 with a; Auto. 
-     Elim (H0 a); Intros. 
-     Split; Intros; Apply remove_2; Auto; 
-      [Apply H1|Apply H2]; EApply remove_3;EAuto.    
-  Save.
-
-  Hints Resolve Equal_remove.
-
-  Lemma cardinal_inv_1 : (s:t)(cardinal s)=O -> (Empty s). 
-  Proof. 
-    Intros; Generalize (!choose_1 s0) (!choose_2 s0).
-    Elim (choose s0); Intuition.
-    Clear H1; Assert (In a s0); Auto.
-    Rewrite (!cardinal_2 (remove a s0) s0 a) in H; Auto.
-    Inversion H.
-  Save.
-  Hints Resolve cardinal_inv_1.
- 
-  Lemma cardinal_inv_2 : 
-     (s:t)(n:nat)(cardinal s)=(S n) -> (EX x:elt | (In x s)).
-  Proof. 
-    Intros; Generalize (!choose_1 s0) (!choose_2 s0).
-    Elim (choose s0); Intuition. 
-    Exists a; Auto.
-    Intros; Rewrite cardinal_1 in H; Auto; Inversion H.
-  Qed.
-
-  Lemma Equal_cardinal_aux : (n:nat)(s,s':t)(cardinal s)=n -> 
-       (Equal s s')->(cardinal s)=(cardinal s').
-  Proof.
-     Induction n.
-     Intros.  
-     Rewrite H.
-     Symmetry.
-     Apply cardinal_1.
-     Generalize (cardinal_inv_1 H) H0.
-     Unfold Empty Equal; Intuition.
-     Generalize (H1 a) (H2 a); Intuition.
-     Intros.
-     Elim (cardinal_inv_2 H0); Intros.
-     Assert (In x0 s'0). 
-       Generalize (H1 x0); Intuition.  
-     Generalize H0.
-     Rewrite (!cardinal_2 (remove x0 s0) s0 x0);Auto.
-     Rewrite (!cardinal_2 (remove x0 s'0) s'0 x0); Auto.
-  Qed.
-
-  Lemma Equal_cardinal : (s,s':t)(Equal s s')->(cardinal s)=(cardinal s').
-  Proof. 
-    Intros; EApply Equal_cardinal_aux; EAuto.
-  Qed.
-
-  End Cardinal.
-
-  Hints Resolve Add_add Add_remove Equal_remove 
-                cardinal_inv_1 Equal_cardinal.
-
-  Lemma cardinal_induction : (P : t -> Prop)
-     ((s:t)(Empty s)->(P s)) -> 
-     ((s,s':t)(P s) -> (x:elt)~(In x s) -> (Add x s s') -> (P s')) -> 
-     (n:nat)(s:t)(cardinal s)=n -> (P s).
-  Proof.
-  Induction n.
-  Intros; Apply H; Auto.
-  Intros; Elim (cardinal_inv_2 H2); Intros. 
-  Apply H0 with (remove x0 s0) x0; Auto.
-  Apply H1; Auto.
-  Assert (S (cardinal (remove x0 s0))) = (S n0); Auto. 
-  Rewrite <- H2; Symmetry.
-  EApply cardinal_2; EAuto.
-  Qed.
-
-  Lemma set_induction : (P : t -> Prop)
-     ((s:t)(Empty s)->(P s)) -> 
-     ((s,s':t)(P s) -> (x:elt)~(In x s) -> (Add x s s') -> (P s')) -> 
-     (s:t)(P s).
-  Proof.
-  Intros; EApply cardinal_induction; EAuto.
-  Qed.  
-
-  Section Fold. 
-
-  Variable A:Set. 
-  Variable eqA:A->A->Prop.
-  Variable st:(Setoid_Theory ? eqA).
-  Variable i:A.
-  Variable f:elt->A->A.
-  Variable Comp:(compat_op E.eq eqA f). 
-  Variable Assoc:(transpose eqA f).
- 
-  Lemma fold_empty: (eqA (fold f empty i) i).
-  Proof. 
-  Apply fold_1; Auto.
-  Qed.
-
-  Lemma fold_equal: 
-    (equal s s')=true -> (eqA (fold f s i) (fold f s' i)).
-  Proof. 
-     Pattern s; Apply set_induction; Intros.
-     Apply (Seq_trans ?? st) with i; Auto.
-     Apply fold_1; Auto.
-     Apply Seq_sym; Auto; Apply fold_1; Auto.
-     Apply cardinal_inv_1; Rewrite <- (Equal_cardinal (equal_2 H0)); Auto.
-     Apply (Seq_trans ?? st) with (f x0 (fold f s0 i)); Auto.
-     Apply fold_2 with eqA:=eqA; Auto.
-     Apply Seq_sym; Auto; Apply fold_2 with eqA := eqA; Auto.
-     Generalize (equal_2 H2) H1; Unfold Add Equal; Intros; 
-       Elim (H4 y0); Elim (H3 y0); Intuition.
-  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_2 with eqA:=eqA; Auto.
-    Intro; Rewrite mem_1 in H; Auto; Discriminate H. 
-  Qed.
-
-  End Fold.
-
-  Section Filter.
-  
-  Variable f:elt->bool.
-  Variable Comp: (compat_bool E.eq f).
-
-  Lemma filter_mem: (mem x (filter f s))=(andb (mem x s) (f x)).
-  Proof. 
-  Apply bool_1; Intuition.
-  Apply andb_true_intro; Intuition; EAuto.
-  Elim (andb_prop ?? H); Intuition. 
-  Qed.
-
-  Lemma for_all_filter: 
-    (for_all f s)=(is_empty (filter [x](negb (f x)) s)).
-  Proof. 
-  Assert Comp' : (compat_bool E.eq [x](negb (f x))). 
-    Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb); Auto. 
-  Apply bool_1; Intuition. 
-  Apply is_empty_1.
-  Unfold Empty; Intros. 
-  Intro.
-  Assert (In a s); EAuto.
-  Generalize (filter_2 Comp' H0).
-  Generalize (for_all_2 Comp H H1); Auto.
-  Intros Eq; Rewrite Eq; Intuition.
-  Apply for_all_1; Unfold For_all; Intros; Auto. 
-  Apply bool_3.
-  Red; Intros.
-  Elim (is_empty_2 H 3!x0); Auto.
-  Qed.
-
-  Lemma exists_filter: 
-    (exists f s)=(negb (is_empty (filter f s))).
-  Proof. 
-  Apply bool_1; Intuition. 
-  Elim (exists_2 Comp H); Intuition.
-  Apply bool_6.
-  Red; Intros; Apply (is_empty_2 H0 3!x0); Auto.
-  Generalize (!choose_1 (filter f s)) (!choose_2 (filter f s)).
-  Case (choose (filter f s)).
-  Intros. 
-  Clear H1. 
-  Apply exists_1; Auto.
-  Exists e; Generalize (H0 e); Intuition; EAuto.
-  Intros. 
-  Clear H0.
-  Rewrite (!is_empty_1 (filter f s)) in H; Auto.
-  Discriminate H.
-  Qed.
-
-  Lemma partition_filter_1: 
-    (equal (fst ? ? (partition f s)) (filter f s))=true.
-  Proof. 
-  Auto.
-  Qed.
-
-  Lemma partition_filter_2: 
-    (equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s))=true.
-  Proof. 
-  Auto.
-  Qed.
-
-  End Filter.
-  End Old_Spec_Now_Properties.
-
-  Hints Immediate 
-  empty_mem   
-  is_empty_equal_empty 
-  add_mem_1
-  remove_mem_1
-  singleton_equal_add
-  union_mem
-  inter_mem
-  diff_mem 
-  cardinal_fold 
-  filter_mem
-  for_all_filter
-  exists_filter : set. 
-
-  Hints Resolve 
-  equal_mem_1
-  subset_mem_1
-  choose_mem_1
-  choose_mem_2
-  add_mem_2
-  remove_mem_2 : set.
-
-Section MoreProperties.
-
-(*s Properties of [equal] *) 
-
-Lemma equal_refl: (s:t)(equal s s)=true.
-Proof.
-Auto with set.
-Qed.
-
-Lemma equal_sym: (s,s':t)(equal s s')=(equal s' s).
-Proof.
-Intros.
-Apply bool_eq_ind;Intros.
-Rewrite equal_mem_1;Auto.
-Symmetry;Apply equal_mem_2;Auto.
-Apply (bool_eq_ind (equal s s'));Intros;Auto.
-Rewrite equal_mem_1 in H;Auto.
-Symmetry;Apply equal_mem_2;Auto.
-Qed.
-
-Lemma equal_trans: 
- (s,u,v:t)(equal s u)=true -> (equal u v)=true -> (equal s v)=true.
-Proof.
-Intros.
-Apply equal_mem_1;Intros.
-Rewrite (equal_mem_2 H).
-Apply equal_mem_2;Assumption.
-Qed.
-
-Lemma equal_equal: 
- (s,t_,u:t)(equal s t_)=true -> (equal s u)=(equal t_ u).
-Proof.
-Intros.
-Apply bool_eq_ind;Intros.
-Apply equal_trans with t_;Auto with set.
-Symmetry; Apply bool_eq_ind;Intros;Auto.
-Rewrite <- H0.
-Apply equal_trans with s;Auto with set.
-Rewrite equal_sym;Auto.
-Qed.
-
-Lemma equal_cardinal: 
- (s,s':t)(equal s s')=true -> (cardinal s)=(cardinal s').
-Proof.
-Intros; Apply Equal_cardinal; Auto.
-Qed.
-
-Hints Resolve equal_refl equal_cardinal equal_equal:set.
-Hints Immediate equal_sym :set.
-
-(* Properties of [subset] *)
-
-Lemma subset_refl: (s:t)(subset s s)=true. 
-Proof.
-Auto with set.
-Qed.
-
-Lemma subset_antisym: 
- (s,s':t)(subset s s')=true -> (subset s' s)=true -> (equal s s')=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Apply bool_eq_ind;Intros.
-EApply subset_mem_2;EAuto.
-Apply (bool_eq_ind (mem a s));Intros;Auto.
-Rewrite <- (subset_mem_2 H H2);Assumption.
-Qed.
-
-Lemma subset_trans: 
- (s,t_,u:t)(subset s t_)=true -> (subset t_ u)=true -> (subset s u)=true.
-Proof.
-Intros.
-Apply subset_mem_1;Intros.
-Apply subset_mem_2 with t_;Intros;Auto.
-Apply subset_mem_2 with s;Auto.
-Qed.
-
-Lemma subset_equal: 
- (s,s':t)(equal s s')=true -> (subset s s')=true.
-Proof.
-Intros.
-Apply subset_mem_1;Intros.
-Rewrite <- (equal_mem_2 H);Auto.
-Qed.
-
-Hints Resolve subset_refl subset_equal subset_antisym :set.
-
-(*s Properties of [empty] *)
-
-Lemma empty_cardinal: (cardinal empty)=O.
-Proof.
-Rewrite cardinal_fold; Auto with set.
-Apply fold_1; Auto.
-Qed.
-
-Hints Immediate empty_cardinal :set.
-
-(*s Properties of [choose] *)
-
-Lemma choose_mem_3: 
- (s:t)(is_empty s)=false -> {x:elt|(choose s)=(Some ? x)/\(mem x s)=true}.
-Proof.
-Intros.
-Generalize (!choose_mem_1 s).
-Generalize (!choose_mem_2 s).
-Case (choose s);Intros.
-Exists e;Auto.
-LApply H0;Trivial;Intros.
-Rewrite H in H2;Discriminate H2.
-Qed.
-
-Lemma choose_mem_4: (choose empty)=(None ?).
-Proof.
-Generalize (!choose_mem_1 empty).
-Case (!choose empty);Intros;Auto.
-Absurd true=false;Auto with bool.
-Rewrite <- (H e);Auto with set.
-Qed.
-
-(*s Properties of [add] *)
-
-Lemma add_mem_3: 
- (s:t)(x,y:elt)(mem y s)=true -> (mem y (add x s))=true.
-Proof.
-Auto.
-Qed.
-
-Lemma add_equal: 
- (s:t)(x:elt)(mem x s)=true -> (equal (add x s) s)=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Elim (ME.eq_dec x a); Intros; Auto with set.
-Rewrite <- mem_eq with x:=x;Auto.
-Rewrite <- (mem_eq s a0);Auto.
-Rewrite H;Auto with set.
-Qed.
-
-Hints Resolve add_mem_3 add_equal :set.
-
-Lemma add_fold: 
- (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
- (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
- (s:t)(x:elt)(mem x s)=true -> (eqA (fold f (add x s) i) (fold f s i)).
-Proof.
-Intros; Apply fold_equal with eqA:=eqA; Auto with set.
-Qed.
-
-Lemma add_cardinal_1: 
- (s:t)(x:elt)(mem x s)=true -> (cardinal (add x s))=(cardinal s).
-Proof.
-Auto with set.
-Qed.
-
-Lemma add_cardinal_2: 
- (s:t)(x:elt)(mem x s)=false -> (cardinal (add x s))=(S (cardinal s)).
-Proof.
-Intros.
-Do 2 Rewrite cardinal_fold.
-Change S with ([_]S x); Apply fold_add with eqA:=(eq nat); Auto.
-Qed.
-
-(*s Properties of [remove] *)
-
-Lemma remove_mem_3: 
- (s:t)(x,y:elt)(mem y (remove x s))=true -> (mem y s)=true.
-Proof.
-Intros s x y;Elim (ME.eq_dec x y); Intro e.
-Rewrite <- mem_eq with x:=x;Auto.
-Rewrite <- (mem_eq s e);Auto.
-Rewrite (remove_mem_1 s x);Intro H;Discriminate H.
-Intros;Rewrite <- H;Symmetry;Auto with set.
-Qed.
-
-Lemma remove_equal: 
- (s:t)(x:elt)(mem x s)=false -> (equal (remove x s) s)=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Elim (ME.eq_dec x a); Intros;Auto with set.
-Rewrite <- mem_eq with x:=x;Auto.
-Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set.
-Qed.
-
-Hints Resolve remove_mem_3 remove_equal :set.
-
-Lemma add_remove: 
- (s:t)(x:elt)(mem x s)=true -> (equal (add x (remove x s)) s)=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Elim (ME.eq_dec x a); Intros;Auto with set.
-Rewrite <- mem_eq with x:=x;Auto.
-Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set.
-Transitivity (mem a (remove x s));Auto with set.
-Qed.
-
-Lemma remove_add: 
- (s:t)(x:elt)(mem x s)=false -> (equal (remove x (add x s)) s)=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Elim (ME.eq_dec x a); Intros;Auto with set.
-Rewrite <- mem_eq with x:=x;Auto.
-Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set.
-Transitivity (mem a (add x s));Auto with set.
-Qed.
-
-Hints Immediate add_remove remove_add :set.
-
-Lemma remove_fold_1: 
- (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
- (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
- (s:t)(x:elt)(mem x s)=true -> 
- (eqA (f x (fold f (remove x s) i)) (fold f s i)).
-Proof.
-Intros.
-Apply Seq_sym; Auto.
-Apply fold_2 with eqA:=eqA; Auto.
-Apply Add_remove; Auto.
-Qed.
-
-Lemma remove_fold_2: 
- (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
- (f:elt->A->A)(i:A) (compat_op E.eq eqA f) -> (transpose eqA f) ->
- (s:t)(x:elt)(mem x s)=false -> 
- (eqA (fold f (remove x s) i) (fold f s i)).
-Proof.
-Intros.
-Apply fold_equal with eqA:=eqA; Auto with set.
-Qed.
-
-Lemma remove_cardinal_1: 
- (s:t)(x:elt)(mem x s)=true -> (S (cardinal (remove x s)))=(cardinal s).
-Proof.
-Intros.
-Do 2 Rewrite cardinal_fold.
-Change S with ([_]S x).
-Apply remove_fold_1 with eqA:=(eq nat); Auto.
-Qed.
-
-Lemma remove_cardinal_2: 
- (s:t)(x:elt)(mem x s)=false -> (cardinal (remove x s))=(cardinal s).
-Proof.
-Auto with set.
-Qed.
-
-(* Properties of [is_empty] *)
-
-Lemma is_empty_cardinal: (s:t)(is_empty s)=(zerob (cardinal s)).
-Proof.
-Intros.
-Apply (bool_eq_ind (is_empty s));Intros.
-Rewrite (equal_cardinal 1!s 2!empty).
-Rewrite empty_cardinal;Simpl;Trivial.
-Rewrite <- H;Symmetry;Auto with set.
-Elim (choose_mem_3 H);Intros.
-Elim p;Intros.
-Rewrite <- (remove_cardinal_1 H1).
-Simpl;Trivial.
-Qed.
-
-(*s Properties of [singleton] *)
-
-Lemma singleton_mem_1: (x:elt)(mem x (singleton x))=true.
-Proof.
-Intros.
-Rewrite (equal_mem_2 (singleton_equal_add x));Auto with set.
-Qed.
-
-Lemma singleton_mem_2: (x,y:elt)~(E.eq x y) -> (mem y (singleton x))=false.
-Proof.
-Intros.
-Rewrite (equal_mem_2 (singleton_equal_add x)).
-Rewrite <- (empty_mem y);Auto with set.
-Qed.
-
-Lemma singleton_mem_3: (x,y:elt)(mem y (singleton x))=true -> (E.eq x y).
-Proof.
-Intros.
-Elim (ME.eq_dec x y);Intros;Auto.
-Qed.
-
-Lemma singleton_cardinal: (x:elt)(cardinal (singleton x))=(S O).
-Proof.
-Intros.
-Rewrite (equal_cardinal (singleton_equal_add x)).
-Rewrite add_cardinal_2;Auto with set.
-Qed.
-
-(* General recursion principes based on [cardinal] *)
-
-Lemma cardinal_set_rec:  (P:t->Set)
- ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> 
- ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
- (P empty) -> (n:nat)(s:t)(cardinal s)=n -> (P s).
-Proof.
-NewInduction n; Intro s; Generalize (is_empty_cardinal s); 
-  Intros eq1 eq2; Rewrite eq2 in eq1; Simpl in eq1.
-Rewrite is_empty_equal_empty in eq1.
-Rewrite equal_sym in eq1.
-Apply (H empty s eq1);Auto.
-Elim (choose_mem_3 eq1);Intros;Elim p;Clear p;Intros.
-Apply (H (add x (remove x s)) s);Auto with set.
-Apply H0;Auto with set.
-Apply IHn.
-Rewrite <- (remove_cardinal_1 H3) in eq2.
-Inversion eq2;Trivial.
-Qed.
-
-Lemma set_rec:  (P:t->Set)
- ((s,s':t)(equal s s')=true -> (P s) -> (P s')) ->
- ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
- (P empty) -> (s:t)(P s).
-Proof.
-Intros;EApply cardinal_set_rec;EAuto.
-Qed.
-
-Lemma cardinal_set_ind:  (P:t->Prop)
- ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> 
- ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
- (P empty) -> (n:nat)(s:t)(cardinal s)=n -> (P s).
-Proof.
-NewInduction n; Intro s; Generalize (is_empty_cardinal s); 
-  Intros eq1 eq2; Rewrite eq2 in eq1; Simpl in eq1.
-Rewrite is_empty_equal_empty in eq1.
-Rewrite equal_sym in eq1.
-Apply (H empty s eq1);Auto.
-Elim (choose_mem_3 eq1);Intros;Elim p;Clear p;Intros.
-Apply (H (add x (remove x s)) s);Auto with set.
-Apply H0;Auto with set.
-Apply IHn.
-Rewrite <- (remove_cardinal_1 H3) in eq2.
-Inversion eq2;Trivial.
-Qed.
-
-Lemma set_ind:  (P:t->Prop)
- ((s,s':t)(equal s s')=true -> (P s) -> (P s')) ->
- ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
- (P empty) -> (s:t)(P s).
-Proof.
-Intros;EApply cardinal_set_ind;EAuto.
-Qed.
-
-(*s Properties of [fold] *)
-
-Lemma fold_commutes:
- (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
- (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) -> (s:t)(x:elt)
- (eqA (fold f s (f x i)) (f x (fold f s i))).
-Proof.
-Intros; Pattern s; Apply set_ind.
-Intros.
-Apply (Seq_trans ?? st) with (fold f s0 (f x i)).
-Apply fold_equal with eqA:=eqA; Auto with set.
-Rewrite equal_sym; Auto.
-Apply (Seq_trans ?? st) with (f x (fold f s0 i)); Auto.
-Apply H; Auto.
-Apply fold_equal with eqA:=eqA; Auto.
-Intros. 
-Apply (Seq_trans ?? st) with (f x0 (fold f s0 (f x i))).
-Apply fold_add with eqA:=eqA; Auto.
-Apply (Seq_trans ?? st) with (f x0 (f x (fold f s0 i))).
-Apply H; Auto.
-Apply (Seq_trans ?? st) with (f x (f x0 (fold f s0 i))).
-Apply H0; Auto.
-Apply H; Auto.
-Apply Seq_sym; Auto.
-Apply fold_add with eqA:=eqA; Auto.
-Apply (Seq_trans ?? st) with (f x i).
-Apply fold_empty; Auto.
-Apply Seq_sym; Auto.
-Apply H; Auto.
-Apply fold_empty; Auto.
-Qed.
-
-Lemma fold_plus: 
- (s:t)(p:nat)(fold [_]S s p)=(fold [_]S s O)+p.
-Proof.
-Assert st := (gen_st nat).
-Assert fe: (compat_op E.eq (eq ?) [_:elt]S). Unfold compat_op; Auto. 
-Assert fp: (transpose (eq ?) [_:elt]S). Unfold transpose;Auto.
-Intros s p;Pattern s;Apply set_ind.
-Intros; Rewrite <- (fold_equal st p fe fp H).
-Rewrite <- (fold_equal st O fe fp H);Assumption.
-Intros.
-Assert (p:nat)(fold [_]S (add x s0) p) = (S (fold [_]S s0 p)).
-Change S with ([_]S x). 
-Intros; Apply fold_add with eqA:=(eq nat); Auto.
-Rewrite (H1 p).
-Rewrite (H1 O).
-Rewrite H0.
-Simpl; Auto.
-Intros; Do 2 Rewrite (fold_empty st);Auto.
-Qed.
-
-(*s Properties of [union] *)
-
-Lemma union_sym:
- (s,s':t)(equal (union s s') (union s' s))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 2 Rewrite union_mem;Auto with bool.
-Qed.
-
-Lemma union_subset_equal: 
- (s,s':t)(subset s s')=true->(equal (union s s') s')=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite union_mem.
-Apply (bool_eq_ind (mem a s));Intros;Simpl;Auto with set.
-Rewrite (subset_mem_2 H H0);Auto.
-Qed.
-
-Lemma union_equal_1: 
- (s,s',s'':t)(equal s s')=true->
- (equal (union s s'') (union s' s''))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 2 (Rewrite union_mem;Idtac).
-Rewrite (equal_mem_2 H a);Auto.
-Qed.
-
-Lemma union_equal_2: 
- (s,s',s'':t)(equal s' s'')=true->
- (equal (union s s') (union s s''))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 2 (Rewrite union_mem;Idtac).
-Rewrite (equal_mem_2 H a);Auto.
-Qed.
-
-Lemma union_assoc: 
- (s,s',s'':t)
- (equal (union (union s s') s'') (union s (union s' s'')))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 4 Rewrite union_mem.
-Rewrite orb_assoc;Auto.
-Qed.
-
-Lemma add_union_singleton: 
- (s:t)(x:elt)(equal (add x s) (union (singleton x) s))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite union_mem.
-Elim (ME.eq_dec x a);Intros.
-Rewrite <- (mem_eq (add x s) a0).
-Rewrite <- (mem_eq (singleton x) a0).
-Rewrite <- (mem_eq s a0).
-Rewrite add_mem_1;Rewrite singleton_mem_1;Simpl;Auto.
-Rewrite singleton_mem_2;Simpl;Auto with set.
-Qed.
-
-Lemma union_add: 
- (s,s':t)(x:elt)
- (equal (union (add x s) s') (add x (union s s')))=true.
-Proof.
-Intros;Apply equal_trans with (union (union (singleton x) s) s').
-Apply union_equal_1;Apply add_union_singleton.
-Apply equal_trans with (union (singleton x) (union s s')).
-Apply union_assoc.
-Rewrite equal_sym;Apply add_union_singleton.
-Qed.
-
-(* caracterisation of [union] via [subset] *)
-
-Lemma union_subset_1:
- (s,s':t)(subset s (union s s'))=true.
-Proof.
-Intros;Apply subset_mem_1;Intros;Rewrite union_mem;Rewrite H;Auto.
-Qed.
-
-Lemma union_subset_2:
- (s,s':t)(subset s' (union s s'))=true.
-Proof.
-Intros;Apply subset_mem_1;Intros;Rewrite union_mem;Rewrite H;Apply orb_b_true.
-Qed.
-
-Lemma union_subset_3:
- (s,s',s'':t)(subset s s'')=true -> (subset s' s'')=true -> 
-    (subset (union s s') s'')=true.
-Proof.
-Intros;Apply subset_mem_1;Intros;Rewrite union_mem in H1.
-Elim (orb_true_elim ? ? H1);Intros.
-Apply (subset_mem_2 H a0).
-Apply (subset_mem_2 H0 b).
-Qed.
-
-(*s Properties of [inter] *) 
-
-Lemma inter_sym:
- (s,s':t)(equal (inter s s') (inter s' s))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 2 Rewrite inter_mem.
-Auto with bool.
-Qed.
-
-Lemma inter_subset_equal: 
- (s,s':t)(subset s s')=true->(equal (inter s s') s)=true.
-Proof.
-Intros.
-Apply equal_mem_1;Intros.
-Rewrite inter_mem.
-Apply (bool_eq_ind (mem a s));Intros;Simpl;Auto.
-Rewrite (subset_mem_2 H H0);Auto.
-Qed.
-
-Lemma inter_equal_1: 
- (s,s',s'':t)(equal s s')=true->
- (equal (inter s s'') (inter s' s''))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 2 (Rewrite inter_mem;Idtac).
-Rewrite (equal_mem_2 H a);Auto.
-Qed.
-
-Lemma inter_equal_2: 
- (s,s',s'':t)(equal s' s'')=true->
- (equal (inter s s') (inter s s''))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 2 (Rewrite inter_mem;Idtac).
-Rewrite (equal_mem_2 H a);Auto.
-Qed.
-
-Lemma inter_assoc: 
- (s,s',s'':t)
- (equal (inter (inter s s') s'') (inter s (inter s' s'')))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Do 4 Rewrite inter_mem.
-Rewrite andb_assoc;Auto.
-Qed.
-
-Lemma union_inter_1: 
- (s,s',s'':t)
- (equal (inter (union s s') s'') (union (inter s s'') (inter s' s'')))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite union_mem.
-Do 3 Rewrite inter_mem.
-Rewrite union_mem. 
-Apply demorgan2.
-Qed.
-
-Lemma union_inter_2: 
- (s,s',s'':t)
- (equal (union (inter s s') s'') (inter (union s s'') (union s' s'')))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite union_mem.
-Do 2 Rewrite inter_mem.
-Do 2 Rewrite union_mem. 
-Apply demorgan4.
-Qed.
-
-Lemma inter_add_1: 
- (s,s':t)(x:elt)(mem x s')=true -> 
- (equal (inter (add x s) s') (add x (inter s s')))=true.
-Proof.
-Intros;Apply equal_trans with (inter (union (singleton x) s) s').
-Apply inter_equal_1;Apply add_union_singleton.
-Apply equal_trans with (union (inter (singleton x) s') (inter s s')).
-Apply union_inter_1.
-Apply equal_trans with (union (singleton x) (inter s s')).
-Apply union_equal_1.
-Apply inter_subset_equal.
-Apply subset_mem_1;Intros.
-Rewrite <- (mem_eq s' (singleton_mem_3 H0));Auto.
-Rewrite equal_sym;Apply add_union_singleton.
-Qed.
-
-Lemma inter_add_2: 
- (s,s':t)(x:elt)(mem x s')=false -> 
- (equal (inter (add x s) s') (inter s s'))=true.
-Proof.
-Intros;Apply equal_trans with (inter (union (singleton x) s) s').
-Apply inter_equal_1;Apply add_union_singleton.
-Apply equal_trans with (union (inter (singleton x) s') (inter s s')).
-Apply union_inter_1.
-Apply union_subset_equal.
-Apply subset_mem_1;Intros.
-Rewrite inter_mem in H0.
-Elim (andb_prop ? ? H0);Intros.
-Absurd (mem a s')=true;Auto.
-Rewrite <- (mem_eq s' (singleton_mem_3 H1));Auto.
-Rewrite H;Auto with bool.
-Qed.
-
-(* caracterisation of [union] via [subset] *)
-
-Lemma inter_subset_1:
- (s,s':t)(subset (inter s s') s)=true.
-Proof.
-Intros;Apply subset_mem_1;Intros;Rewrite inter_mem in H;Elim (andb_prop ? ? H);Auto.
-Qed.
-
-Lemma inter_subset_2:
- (s,s':t)(subset (inter s s') s')=true.
-Proof.
-Intros;Apply subset_mem_1;Intros;Rewrite inter_mem in H;Elim (andb_prop ? ? H);Auto.
-Qed.
-
-Lemma inter_subset_3:
- (s,s',s'':t)(subset s'' s)=true -> (subset s'' s')=true -> 
-    (subset s'' (inter s s'))=true.
-Intros;Apply subset_mem_1;Intros;Rewrite inter_mem.
-Rewrite (subset_mem_2 H H1);Rewrite (subset_mem_2 H0 H1);Auto.
-Qed.
-
-(*s Properties of [union],[inter],[fold] and [cardinal] *)
-
-Lemma fold_union_inter: 
- (A:Set)
- (f:elt->A->A)(i:A)(compat_op E.eq (eq ?) f) -> (transpose (eq ?) f) -> 
- (s,s':t)(fold f (union s s') (fold f (inter s s') i))
-  = (fold f s (fold f s' i)).
-Proof.
-Intro A.
-LetTac st := (gen_st A).
-Intros;Pattern s;Apply set_ind.
-Intros; Rewrite <- (fold_equal st i H H0 (inter_equal_1 s' H1)).
-Rewrite <- (fold_equal st (fold f s' i) H H0 H1).
-Rewrite <- (fold_equal st (fold f (inter s0 s') i)  H H0 (union_equal_1 s' H1));Auto.
-Intros.
-Rewrite 
- (fold_equal st (fold f (inter (add x s0) s') i) H H0 (union_add s0 s' x)).
-Generalize (refl_equal ? (mem x s')); Pattern -1 (mem x s'); Case (mem x s');Intros.
-Rewrite (fold_equal st i H H0 (inter_add_1 s0 H3)).
-Cut (mem x (inter s0 s'))=false;Intros.
-Cut (mem x (union s0 s'))=true;Intros.
-Rewrite (fold_add st i H H0 H4).
-Rewrite (fold_commutes st);Auto.
-Rewrite (fold_equal st (fold f (inter s0 s') i) H H0 (add_equal H5)).
-Rewrite (fold_add st (fold f s' i) H H0 H1).
-Rewrite H2;Auto.
-Rewrite union_mem;Rewrite H3;Apply orb_b_true.
-Rewrite inter_mem;Rewrite H1;Simpl;Auto.
-Rewrite (fold_equal st i H H0 (inter_add_2 s0 H3)).
-Cut (mem x (union s0 s'))=false;Intros.
-Rewrite (fold_add st (fold f (inter s0 s') i) H H0 H4).
-Rewrite (fold_add st (fold f s' i) H H0 H1).
-Rewrite H2;Auto.
-Rewrite union_mem;Rewrite H3; Rewrite H1;Auto.
-Cut (subset empty s')=true;Intros.
-Rewrite (fold_equal st i H H0 (inter_subset_equal H1)).
-Do 2 Rewrite (fold_empty st);Apply fold_equal with eqA:=(eq A);Auto.
-Apply union_subset_equal;Auto.
-Apply subset_mem_1;Intros.
-Rewrite empty_mem in H1;Absurd true=false;Auto with bool.
-Qed.
-
-Lemma union_inter_cardinal: 
- (s,s':t)(cardinal (union s s'))+(cardinal (inter s s'))
-  = (cardinal s)+(cardinal s').
-Proof.
-Intros.
-Do 4 Rewrite cardinal_fold.
-Do 2 Rewrite <- fold_plus.
-Apply fold_union_inter;Auto.
-Qed.
-
-Lemma fold_union: 
- (A:Set)(f:elt->A->A)(i:A)(compat_op E.eq (eq A) f) -> (transpose (eq A) f) -> 
- (s,s':t)((x:elt)(andb (mem x s) (mem x s'))=false) -> 
- (fold f (union s s') i)=(fold f s (fold f s' i)).
-Proof.
-Intros.
-Assert st:= (gen_st A).
-Rewrite <- (fold_union_inter i H H0 s s').
-Cut (equal (inter s s') empty)=true;Intros.
-Rewrite (fold_equal st i H H0 H2). 
-Rewrite (fold_empty st);Auto.
-Apply equal_mem_1;Intros.
-Rewrite inter_mem; Rewrite empty_mem;Auto.
-Qed.
-
-Lemma union_cardinal: 
- (s,s':t)((x:elt)(andb (mem x s) (mem x s'))=false) -> 
- (cardinal (union s s'))=(cardinal s)+(cardinal s').
-Proof.
-Intros.
-Do 3 Rewrite cardinal_fold.
-Rewrite fold_union;Auto.
-Apply fold_plus;Auto.
-Qed.
-
-(*s Properties of [diff] *)
-
-Lemma diff_subset: 
- (s,s':t)(subset (diff s s') s)=true.
-Proof.
-Intros.
-Apply subset_mem_1;Intros.
-Rewrite diff_mem in H.
-Elim (andb_prop ? ? H);Auto.
-Qed.
-
-Lemma diff_subset_equal:
- (s,s':t)(subset s s')=true->(equal (diff s s') empty)=true.
-Proof.
-Intros.
-Apply equal_mem_1;Intros.
-Rewrite empty_mem.
-Rewrite diff_mem.
-Generalize (!subset_mem_2 ?? H a).
-Case (mem a s);Simpl;Intros;Auto.
-Rewrite H0;Auto.
-Qed.
-
-Lemma remove_inter_singleton: 
- (s:t)(x:elt)(equal (remove x s) (diff s (singleton x)))=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite diff_mem.
-Elim (ME.eq_dec x a); Intros.
-Rewrite <- (mem_eq (remove x s) a0).
-Rewrite <- (mem_eq s a0).
-Rewrite <- (mem_eq (singleton x) a0).
-Rewrite remove_mem_1;Rewrite singleton_mem_1;Rewrite andb_b_false;Auto.
-Rewrite singleton_mem_2;Auto;Simpl;Rewrite andb_b_true;Auto with set.
-Qed.
-
-Lemma diff_inter_empty:
- (s,s':t)(equal (inter (diff s s') (inter s s')) empty)=true. 
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite empty_mem;Do 2 Rewrite inter_mem;Rewrite diff_mem.
-Case (mem a s);Case (mem a s');Simpl;Auto.
-Qed.
-
-Lemma diff_inter_all: 
-(s,s':t)(equal (union (diff s s') (inter s s')) s)=true.
-Proof.
-Intros;Apply equal_mem_1;Intros.
-Rewrite union_mem;Rewrite inter_mem;Rewrite diff_mem.
-Case (mem a s);Case (mem a s');Simpl;Auto.
-Qed.
-
-Lemma fold_diff_inter: 
- (A:Set)(f:elt->A->A)(i:A)(compat_op E.eq (eq A) f) -> (transpose (eq A) f) ->
- (s,s':t)(fold f (diff s s') (fold f (inter s s') i))=(fold f s i).
-Proof.
-Intros.
-Assert st := (gen_st A).
-Rewrite <- (fold_union_inter i H H0 (diff s s') (inter s s')).
-Rewrite (fold_equal st i H H0 (diff_inter_empty s s')).
-Rewrite (fold_empty st).
-Apply fold_equal with eqA:=(eq A);Auto.
-Apply diff_inter_all.
-Qed.
-
-Lemma diff_inter_cardinal: 
- (s,s':t)(cardinal (diff s s'))+(cardinal (inter s s'))=(cardinal s).
-Proof.
-Intros.
-Do 3 Rewrite cardinal_fold.
-Rewrite <- fold_plus.
-Apply fold_diff_inter; Auto.
-Qed.
-
-Lemma subset_cardinal: 
- (s,s':t)(subset s s')=true -> (le (cardinal s) (cardinal s')).
-Proof.
-Intros.
-Rewrite <- (diff_inter_cardinal s' s).
-Rewrite (equal_cardinal (inter_sym s' s)).
-Rewrite (equal_cardinal (inter_subset_equal H)); Auto with arith.
-Qed.
-
-(*s Properties of [for_all] *)
-
-Section For_all.
-
-Variable f : elt->bool.
-Variable Comp : (compat_bool E.eq f).
-
-Local Comp' : (compat_bool E.eq [x](negb (f x))).
-Proof.
-Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb);Auto.
-Qed.
-
-Lemma for_all_mem_1: 
- (s:t)((x:elt)(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_mem; Auto.
-Rewrite empty_mem.
-Generalize (H a); Case (mem a s);Intros;Auto.
-Rewrite H0;Auto.
-Qed.
-
-Lemma for_all_mem_2: 
- (s:t)(for_all f s)=true -> (x:elt)(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_mem; Auto.
-Rewrite empty_mem.
-Rewrite H0; Simpl;Intros.
-Replace true with (negb false);Auto;Apply negb_sym;Auto.
-Qed.
-
-Lemma for_all_mem_3: 
- (s:t)(x:elt)(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_mem; Auto.
-Rewrite empty_mem.
-Rewrite H.
-Rewrite H0.
-Simpl;Auto.
-Qed.
-
-Lemma for_all_mem_4: 
- (s:t)(for_all f s)=false -> {x:elt | (mem x s)=true /\ (f x)=false}.
-Intros.
-Rewrite for_all_filter in H; Auto.
-Elim (choose_mem_3 H);Intros;Elim p;Intros.
-Exists x.
-Rewrite filter_mem in H1; Auto.
-Elim (andb_prop ? ? H1).
-Split;Auto.
-Replace false with (negb true);Auto;Apply negb_sym;Auto.
-Qed.
-
-End For_all.
-
-(*s Properties of [exists] *)
-
-Section Exists.
-
-Variable f : elt->bool.
-Variable Comp : (compat_bool E.eq f).
-
-Local Comp' : (compat_bool E.eq [x](negb (f x))).
-Proof.
-Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb);Auto.
-Qed.
-
-Lemma for_all_exists: 
- (s:t)(exists f s)=(negb (for_all [x](negb (f x)) s)).
-Proof.
-Intros.
-Rewrite for_all_filter; Auto.
-Rewrite exists_filter; Auto.
-Apply (f_equal ? ? negb).
-Do 2 Rewrite is_empty_equal_empty.
-Apply equal_equal.
-Apply equal_mem_1;Intros.
-Do 2 (Rewrite filter_mem; Auto).
-Rewrite negb_elim;Auto.
-Generalize Comp'; Unfold compat_bool; Intros; Apply (f_equal ? ?  negb); Auto.
-Qed.
-
-Lemma exists_mem_1: 
- (s:t)((x:elt)(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: 
- (s:t)(exists f s)=false -> (x:elt)(mem x s)=true -> (f x)=false. 
-Proof.
-Intros.
-Rewrite for_all_exists in H.
-Replace false with (negb true);Auto;Apply negb_sym;Symmetry.
-Rewrite (for_all_mem_2 1![x](negb (f x)) Comp' 3!s);Simpl;Auto.
-Replace true with (negb false);Auto;Apply negb_sym;Auto.
-Qed.
-
-Lemma exists_mem_3: 
- (s:t)(x:elt)(mem x s)=true -> (f x)=true -> (exists f s)=true.
-Proof.
-Intros.
-Rewrite for_all_exists.
-Symmetry;Apply negb_sym;Simpl.
-Apply for_all_mem_3 with x;Auto.
-Rewrite H0;Auto.
-Qed.
-
-Lemma exists_mem_4: 
- (s:t)(exists f s)=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
-Proof.
-Intros.
-Rewrite for_all_exists in H.
-Elim (for_all_mem_4 1![x](negb (f x)) Comp' 3!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 Exists.
-
-Section Sum.
-
-
-Definition sum := [f:elt -> nat; s:t](fold [x](plus (f x)) s 0). 
-
-Lemma sum_plus : 
-  (f,g:elt ->nat)(compat_nat E.eq f) -> (compat_nat E.eq g) -> 
-     (s:t)(sum [x]((f x)+(g x)) s) = (sum f s)+(sum g s).
-Proof.
-Unfold sum.
-Intros f g Hf Hg.
-Assert fc : (compat_op E.eq (eq ?) [x:elt](plus (f x))).  Auto.
-Assert ft : (transpose (eq ?) [x:elt](plus (f x))). Red; Intros; Omega.
-Assert gc : (compat_op E.eq (eq ?) [x:elt](plus (g x))). Auto.
-Assert gt : (transpose (eq ?) [x:elt](plus (g x))). Red; Intros; Omega.
-Assert fgc : (compat_op E.eq (eq ?) [x:elt](plus ((f x)+(g x)))). Auto.
-Assert fgt : (transpose (eq ?) [x:elt](plus ((f x)+(g x)))). Red; Intros; Omega.
-Assert st := (gen_st nat).
-Intros s;Pattern s; Apply set_ind.
-Intros.
-Rewrite <- (fold_equal st O fc ft H).
-Rewrite <- (fold_equal st O gc gt H).
-Rewrite <- (fold_equal st O fgc fgt H); Auto.
-Assert fold_add' := [s:t; t:elt](!fold_add s t ?? st).
-Intros; Do 3 (Rewrite fold_add';Auto).
-Rewrite H0;Simpl;Omega.
-Intros; Do 3 Rewrite (fold_empty st);Auto.
-Qed.
-
-Lemma filter_equal : (f:elt -> bool)(compat_bool E.eq f) -> 
-     (s,s':t)(Equal s s') -> (Equal (filter f s) (filter f s')).
-Proof.
-Unfold Equal; Split; Intros; Elim (H0 a); Intros; Apply filter_3; EAuto.
-Qed.
-
-Lemma add_filter_1 :  (f:elt -> bool)(compat_bool E.eq f) -> 
-  (s,s':t)(x:elt) (f x)=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
-Proof.
-Unfold Add; Split; Intros; Elim (H1 y); Clear H1; Intros.
-Elim H1; [ Auto | Right; EAuto | EAuto ].
-Apply filter_3; Auto.
-Elim H2; Intros.
-Intuition.
-Apply H3; Right; EAuto.
-Elim H2; Intros.
-Rewrite <- H0; Auto.
-EAuto.
-Qed.
-
-Lemma add_filter_2 :  (f:elt -> bool)(compat_bool E.eq f) -> 
-  (s,s':t)(x:elt) (f x)=false -> (Add x s s') -> (Equal (filter f s) (filter f s')).
-Proof.
-Unfold Add Equal; Split; Intros; Elim (H1 a); Clear H1; Intros.
-Elim H1; Intros. 
-Absurd true=false; Auto with bool.
-Rewrite <- H0. 
-Rewrite <- (filter_2 H H2); Auto.
-Apply filter_3; EAuto.
-Apply H3; Right; EAuto.
-
-Elim H1; Intros. 
-Absurd true=false; Auto with bool.
-Rewrite <- H0. 
-Rewrite <- (filter_2 H H2); Auto.
-EAuto.
-EAuto.
-Qed.
-
-Lemma sum_filter : (f:elt -> bool)(compat_bool E.eq f) -> 
-  (s:t)(sum [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 fold_add' := [s:t; t:elt](!fold_add s t ?? st).
-Assert cc : (compat_op E.eq (eq ?) [x:elt](plus (if (f x) then 1 else 0))). 
- Unfold compat_op; Intros.
- Rewrite (Hf x x' H); Auto.
-Assert ct : (transpose (eq ?) [x:elt](plus (if (f x) then 1 else 0))).
- Unfold transpose; Intros; Omega.
-Intros s;Pattern s; Apply set_ind.
-Intros.
-Rewrite <- (fold_equal st O  cc ct H).
-Rewrite <- (Equal_cardinal (filter_equal Hf (equal_2 H))); Auto.
-Intros; Rewrite fold_add'; 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; Intuition.
-Rewrite (cardinal_2 H1 (H4 (Add_add s0 x))); Auto.
-Rewrite <- (Equal_cardinal (H4 (Add_add s0 x))); Auto.
-Intros; Rewrite (fold_empty st);Auto.
-Rewrite cardinal_1; Auto.
-Unfold Empty; Intuition.
-Elim (!empty_1 a); EAuto.
-Qed.
-
-Lemma fold_compat : 
-  (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) -> 
-  (i:A)(s:t)((x:elt)(In x s) -> (y:A)(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_ind; Intros.
-Apply (Seq_trans ?? st) with (fold f s0 i).
-Apply fold_equal with eqA:=eqA; Auto.
-Rewrite equal_sym; Auto.
-Apply (Seq_trans ?? st) with (fold g s0 i).
-Apply H0; Intros; Apply H1; Auto.
-Elim  (equal_2 H x); Intuition.
-Apply fold_equal with eqA:=eqA; Auto.
-Apply (Seq_trans ?? st) with (f x (fold f s0 i)).
-Apply fold_add with eqA:=eqA; Auto.
-Apply (Seq_trans ?? st) with (g x (fold f s0 i)).
-Apply H1; Auto with set.
-Apply (Seq_trans ?? st) with (g x (fold g s0 i)).
-Apply gc; Auto.
-Apply Seq_sym; Auto; Apply fold_add with eqA:=eqA; Auto.
-Apply (Seq_trans ?? st) with i; [Idtac | Apply Seq_sym; Auto]; Apply fold_empty; Auto.
-Qed.
-
-Lemma sum_compat : 
-  (f,g:elt->nat)(compat_nat E.eq f) -> (compat_nat E.eq g) -> 
-  (s:t)((x:elt)(In x s) -> (f x)=(g x)) -> (sum f s)=(sum g s).
-Intros.
-Unfold sum; Apply (!fold_compat ? (eq nat)); Auto.
-Unfold transpose; Intros; Omega.
-Unfold transpose; Intros; Omega.
-Qed.
-
-End Sum.
-
-Lemma filter_orb: (f,g:elt->bool)(compat_bool E.eq f) -> (compat_bool E.eq g) ->
-  (s:t)(Equal (filter [x:elt](orb (f x) (g x)) s) (union (filter f s) (filter g s))).
-Proof.
-Intros.
-Assert (compat_bool E.eq [x](orb (f x) (g x))).
-  Unfold compat_bool; Intros.
-  Rewrite (H x y H1).
-  Rewrite (H0 x y H1); Auto.
-Unfold Equal; Split; Intros.
-Assert H3 := (filter_1 H1 H2).
-Assert H4 := (filter_2 H1 H2).
-Elim (orb_prop ?? H4); Intros; EAuto.
-Elim (union_1 H2); Intros. 
-Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H H3); Auto ].
-Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H0 H3); Auto with bool].
-Qed.
-
-End MoreProperties.
-
-End Properties.