changement de spécif du fold

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

5 files changed, 389 insertions, 224 deletions

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 257aa9e8b..c3a4be64d 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -100,27 +100,22 @@ Module DepOfNodep [M:S] <: Sdep with Module E := M.E.
   Save.   
 
   Definition fold :
-   (A:Set)
-   (f:elt->A->A)
-   { fold:t -> A -> A | (s,s':t)(a:A)
-      (eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
-      ((Empty s) -> (eqA (fold s a) a)) /\
-      ((compat_op E.eq eqA f)->(transpose eqA f) ->
-         (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }.
-  Proof.
-    Intros; Exists (!fold A f); Intros.
-    Split; Intros.
-    Apply fold_1; Auto.
-    Apply (!fold_2 s s' x A eqA); Auto.
+   (A:Set)(f:elt->A->A)(s:t)(i:A) 
+   { r : A | (EX l:(list elt) | 
+                  (Unique E.eq l) /\
+                  ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+                  r = (fold_right f i l)) }.
+  Proof.
+    Intros; Exists (!fold A f s i); Exact (fold_1 s i f).
   Save.  
 
   Definition cardinal :
-    {cardinal : t -> nat | (s,s':t)
-       ((Empty s) -> (cardinal s)=O) /\
-       ((x:elt) (Add x s s') -> ~(In x s) -> 
-	          (cardinal s')=(S (cardinal s))) }.
+    (s:t) { r : nat | (EX l:(list elt) | 
+                              (Unique E.eq l) /\ 
+                              ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+                              r = (length l)) }.
   Proof.
-    Intros; Exists cardinal; EAuto.
+    Intros; Exists (cardinal s); Exact (cardinal_1 s).
   Save.    
 
   Definition fdec := 
@@ -544,38 +539,30 @@ Module NodepOfDep [M:Sdep] <: S with Module E := M.E.
     Intros s s' x; Unfold diff; Case (M.diff s s'); Ground.
   Save.
 
-  Definition cardinal : t -> nat := let (f,_)= M.cardinal in f.
+  Definition cardinal : t -> nat := [s]let (f,_)= (M.cardinal s) in f.
 
-  Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O.
-  Proof. 
-    Intros; Unfold cardinal; Case M.cardinal; Ground.
-  Qed.
-
-  Lemma cardinal_2 : 
-    (s,s':t)(x:elt)~(In x s) -> (Add x s s') -> 
-	(cardinal s')=(S (cardinal s)).
-  Proof. 
-    Intros; Unfold cardinal; Case M.cardinal; Ground.
+  Lemma cardinal_1 : 
+    (s:t)(EX l:(list elt) | 
+             (Unique E.eq l) /\
+             ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+             (cardinal s)=(length l)).
+  Proof.
+    Intros; Unfold cardinal; Case (M.cardinal s); Ground.
   Qed.
 
   Definition fold : (B:Set)(elt->B->B)->t->B->B :=  
-       [B,f]let (fold,_)= (M.fold f) in fold.
+       [B,f,i,s]let (fold,_)= (M.fold f i s) in fold.
 
   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).
+   (s:t)(A:Set)(i:A)(f:elt->A->A)
+   (EX l:(list elt) | 
+       (Unique E.eq l) /\ 
+       ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+       (fold f s i)=(fold_right f i l)).
   Proof.
-    Intros; Unfold fold; Case (M.fold f); Ground.
+    Intros; Unfold fold; Case (M.fold f s i); Ground.
   Save.  
 
-  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; Unfold fold; Case (M.fold f); Ground.
-  Save.
-
   Definition f_dec : 
     (f: elt -> bool)(x:elt){ (f x)=true } + { (f x)<>true }.
   Proof.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index ddd12838d..70d9ff962 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -23,16 +23,9 @@ 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  boolean function with respect to an equality. *)
 Definition compat_bool := [f:A->bool] (x,y:A)(eqA x y) -> (f x)=(f y).
 
-(** 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 predicate with respect to an equality. *)
 Definition compat_P := [P:A->Prop](x,y:A)(eqA x y) -> (P x) -> (P y).
 
@@ -41,12 +34,18 @@ Inductive InList [x:A] : (list A) -> Prop :=
   | InList_cons_hd : (y:A)(l:(list A))(eqA x y) -> (InList x (cons y l))
   | InList_cons_tl : (y:A)(l:(list A))(InList x l) -> (InList x (cons y l)).
 
+(** A list without redondancy. *)
+Inductive Unique : (list A) -> Prop := 
+  | Unique_nil : (Unique (nil A)) 
+  | Unique_cons : (x:A)(l:(list A)) ~(InList x l) -> (Unique l) -> (Unique (cons x l)).
+
 End Misc.
 
 Hint InList := Constructors InList.
+Hint InList := Constructors Unique.
 Hint sort := Constructors sort.
 Hint lelistA := Constructors lelistA.
-Hints Unfold transpose compat_bool compat_op compat_P.
+Hints Unfold compat_bool compat_P.
 
 (** * Ordered types *)
 
@@ -265,18 +264,18 @@ Module Type S.
  
   (** Specification of [fold] *)  
   Parameter fold_1: 
-   (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).
-   
-  Parameter fold_2: 
-    (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))).
+   (A:Set)(i:A)(f:elt->A->A)
+   (EX l:(list elt) | 
+       (Unique E.eq l) /\ 
+       ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+       (fold f s i)=(fold_right f i l)).
 
   (** Specification of [cardinal] *)  
-  Parameter cardinal_1: (Empty s) -> (cardinal s)=O.
-  Parameter cardinal_2:  
-    ~(In x s) -> (Add x s s') -> (cardinal s')=(S (cardinal s)).
+  Parameter cardinal_1: 
+    (EX l:(list elt) | 
+        (Unique E.eq l) /\
+        ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+        (cardinal s)=(length l)).
 
   Section Filter.
   
@@ -359,7 +358,6 @@ Module Type S.
   union_1 union_2 union_3
   inter_1 inter_2 inter_3 
   diff_1 diff_2 diff_3
-  cardinal_1 cardinal_2
   filter_1 filter_2 filter_3
   for_all_1 for_all_2
   exists_1 exists_2
@@ -428,18 +426,17 @@ Module Type Sdep.
   Parameter subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }.
 
   Parameter fold : 
-   (A:Set)
-   (f:elt->A->A) 
-   { fold:t -> A -> A | (s,s':t)(a:A)
-      (eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
-      ((Empty s) -> (eqA (fold s a) a)) /\
-      ((compat_op E.eq eqA f)->(transpose eqA f) ->
-        (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }.  
+   (A:Set)(f:elt->A->A)(s:t)(i:A) 
+   { r : A | (EX l:(list elt) | 
+                  (Unique E.eq l) /\
+                  ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+                  r = (fold_right f i l)) }.
 
   Parameter cardinal : 
-    {cardinal : t -> nat | (s,s':t)
-       ((Empty s) -> (cardinal s)=O) /\
-       ((x:elt) (Add x s s') -> ~(In x s) -> (cardinal s')=(S (cardinal s)))}.
+    (s:t) { r : nat | (EX l:(list elt) | 
+                              (Unique E.eq l) /\ 
+                              ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+                              r = (length l)) }.
 
   Parameter filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
      { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.
@@ -639,5 +636,16 @@ Module MoreOrderedType [O:OrderedType].
   Save.
   Hints Resolve In_InList.
 
+  Lemma Sort_Unique : (l:(list O.t))(Sort l) -> (Unique O.eq l).
+  Proof.
+  Induction l; Auto.
+  Intros x l' H H0.
+  Inversion_clear H0.
+  Constructor; Auto.  
+  Intro.
+  Absurd (O.lt x x); Auto.
+  EApply In_sort; EAuto.
+  Qed.
+
 End MoreOrderedType.
 
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index cec133b8c..5b6065c26 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -674,6 +674,30 @@ Module Raw [X : OrderedType].
   Definition choose_2: (s:t)(choose s)=(None ?) -> (Empty s)
      := min_elt_3.
 
+  Lemma fold_1 : 
+    (s:t)(Hs:(Sort s))(A:Set)(i:A)(f:elt->A->A)
+       (EX l:(list elt) | (Unique E.eq l) /\ 
+                               ((x:elt)(In x s)<->(InList E.eq x l)) /\ (fold f s i)=(fold_right f i l)).
+  Proof.
+  Intros; Exists s; Split; Intuition.
+  Apply ME.Sort_Unique; Auto.
+  Induction s; Simpl; Trivial.
+  Rewrite Hrecs; Trivial.
+  Inversion_clear Hs; Trivial.
+  Qed.
+
+  Lemma cardinal_1 : 
+    (s:t)(Hs:(Sort s))(EX l:(list elt) | (Unique E.eq l) /\ 
+                                   ((x:elt)(In x s)<->(InList E.eq x l)) /\ (cardinal s)=(length l)).
+  Proof.
+  Intros; Exists s; Split; Intuition.
+  Apply ME.Sort_Unique; Auto.  
+  Unfold cardinal; Induction s; Simpl; Trivial.
+  Rewrite Hrecs; Trivial.
+  Inversion_clear Hs; Trivial.
+  Qed.
+  
+(*
   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.
@@ -828,6 +852,7 @@ Module Raw [X : OrderedType].
   Refine (!fold_2 s s' Hs Hs' x nat (eq ?) ? O [_]S H1 H2 H H0).
   Intuition EAuto; Transitivity y; Auto.
   Qed.
+*)
 
   Lemma filter_Inf : 
     (s:t)(Hs:(Sort s))(x:elt)(f:elt->bool)(Inf x s) -> (Inf x (filter f s)).
@@ -1173,12 +1198,10 @@ Module Make [X:OrderedType] <: S with Module E := X.
  Definition choose_2 := min_elt_3.
  
  Definition fold := [B:Set; f: elt->B->B; s:t](!Raw.fold B f s). 
- Definition fold_1 := [s:t](!Raw.fold_1 s). 
- Definition fold_2 := [s,s':t](Raw.fold_2 (sorted s) (sorted s')).
+ Definition fold_1 := [s:t](Raw.fold_1 (sorted s)). 
  
  Definition cardinal := [s:t](Raw.cardinal s).
- Definition cardinal_1 := [s:t](!Raw.cardinal_1 s). 
- Definition cardinal_2 := [s,s':t](Raw.cardinal_2 (sorted s) (sorted s')).
+ Definition cardinal_1 := [s:t](Raw.cardinal_1 (sorted s)). 
  
  Definition filter := [f: elt->bool; s:t](Build_slist (Raw.filter_sort (sorted s) f)).
  Definition filter_1 := [s:t](!Raw.filter_1 s).
@@ -1216,63 +1239,3 @@ Module Make [X:OrderedType] <: S with Module E := X.
  Defined.
 
 End Make.
-
-(* TODO: functions in Raw should be all tail-recursive; 
-   here is a beginning
-
-  Fixpoint rev_append [s:t] : t -> t := Cases s of
-    nil => [s']s'
-  | (cons x l) => [s'](rev_append l x::s')
-  end.
-
-  Lemma rev_append_correct : (s,s':t)(rev_append s s')=(app (rev s) s').
-  Proof.
-  Induction s; Simpl; Auto.
-  Intros.
-  Rewrite H.
-  Rewrite app_ass.
-  Simpl; Auto.
-  Qed.
-
-  (* a tail_recursive [rev]. *)
-  Definition rev_tl := [s:t](rev_append s []).
-
-  Lemma rev_tl_correct : (s:t)(rev_tl s)=(rev s).
-  Proof.
-  Unfold rev_tl; Intros; Rewrite rev_append_correct; Symmetry;
-    Exact (app_nil_end (rev s)).
-  Qed.
-
-  (* a tail_recursive [union] *)
-  Fixpoint union_tl_aux [acc,s:t] : t -> t := Cases s of
-    nil => [s'](rev_append s' acc)
-  | (cons x l) =>
-       (Fix union_aux { union_aux / 2 : t -> t -> t := [acc,s']Cases s' of
-           nil => (rev_append s acc)
-         | (cons x' l') => Cases (E.compare x x') of
-              (Lt _ ) => (union_tl_aux x::acc l s')
-            | (Eq _ ) => (union_tl_aux x::acc l l')
-            | (Gt _) => (union_aux x'::acc l')
-            end
-         end} acc)
-   end.
-
-  Definition union_tl := [s,s':t](rev_tl (union_tl_aux [] s s')).
-
-  Lemma union_tl_correct :
-    (s,s':t)(union_tl s s')=(union s s').
-  Proof.
-  Assert  (s,s',acc:t)(union_tl_aux acc s s')=(rev_append (union s s') acc).
-   Induction s.
-   Simpl; Auto.
-   Intros x l Hrec; Induction s'; Auto; Intros x' l' Hrec' acc.
-   Simpl; Case (E.compare x x'); Simpl; Intros; Auto.
-   Change (union_tl_aux x'::acc x::l l')=(rev_append (union x::l l') x'::acc); Ground.
-  Unfold union_tl; Intros; Rewrite H; Auto.
-  Change (rev_append (union s s') []) with (rev_tl (union s s')).
-  Do 2 Rewrite rev_tl_correct.
-  Exact (idempot_rev (union s s')).
-  Qed.
-
-*)
-
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 226205877..ad27ff326 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -22,6 +22,24 @@ 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 ].
@@ -31,7 +49,6 @@ Definition gen_st : (A:Set)(Setoid_Theory ? (eq A)).
 Auto.
 Qed.
 
-
 Module Properties [M:S].
   Import M.
   Import Logic. (* for unmasking eq. *)  
@@ -41,6 +58,247 @@ Module Properties [M:S].
 
   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.
 
@@ -321,15 +579,6 @@ Module Properties [M:S].
 
   End Fold.
 
-  Lemma cardinal_fold: (cardinal s)=(fold [_]S s O).
-  Proof. 
-    Pattern s; Apply set_induction; Intros.
-    Rewrite cardinal_1; Auto; Symmetry; Apply fold_1;Auto.
-    Rewrite (!cardinal_2 s0 s'0 x0);Auto.
-    Rewrite H; Symmetry; Change S with ([_]S x0). 
-    Apply fold_2 with eqA:=(eq nat); Auto.
-  Qed.
-
   Section Filter.
   
   Variable f:elt->bool.
@@ -1327,10 +1576,6 @@ Section Sum.
 
 Definition sum := [f:elt -> nat; s:t](fold [x](plus (f x)) s 0). 
 
-Definition compat_nat := [A:Set][eqA:A->A->Prop][f:A->nat]
- (x,x':A)(eqA x x') -> (f x)=(f x').
-Hints Unfold compat_nat.
-
 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).
@@ -1478,6 +1723,5 @@ Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H0 H3); Auto with bool].
 Qed.
 
 End MoreProperties.
-Hints Unfold compat_nat.
 
 End Properties. 
diff --git a/theories/FSets/FSetRBT.v b/theories/FSets/FSetRBT.v
index c91dc719a..791920be7 100644
--- a/theories/FSets/FSetRBT.v
+++ b/theories/FSets/FSetRBT.v
@@ -1842,96 +1842,59 @@ Module Make [X : OrderedType] <: Sdep with Module E := X.
    [A:Set; f:elt->A->A; s:tree] (Lists.Raw.fold f (elements_tree s)).
   Implicits fold_tree' [1].
 
-  Lemma fold_tree_compat : (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
-      (s:tree)(f:elt->A->A)(compat_op E.eq eqA f) -> (a,a':A)(eqA a a') ->
-      (eqA (fold_tree f s a) (fold_tree f s a')).
-  Proof. 
-  Induction s; Simpl; Auto.
-  Qed.  
-
-  Lemma fold_tree_equiv_aux : (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
-     (s:tree)(f:elt->A->A)(compat_op E.eq eqA f) -> (a:A; acc : (list elt))
-     (eqA (Lists.Raw.fold f (elements_tree_aux acc s) a)
-                 (fold_tree f s (Lists.Raw.fold f acc a))).
+  Lemma fold_tree_equiv_aux : 
+     (A:Set)(s:tree)(f:elt->A->A)(a:A; acc : (list elt))
+     (Lists.Raw.fold f (elements_tree_aux acc s) a)
+     = (fold_tree f s (Lists.Raw.fold f acc a)).
   Proof.
   Induction s.
   Simpl; Intuition.
   Simpl; Intros.
-  EApply (Seq_trans ?? st).
-  Apply H; Auto.
-  Apply (fold_tree_compat A eqA); Simpl; Auto.
+  Rewrite H.
+  Rewrite <- H0.
+  Simpl; Auto.
   Qed.
 
-   Lemma fold_tree_equiv : 
-     (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
-     (s:tree)(f:elt->A->A; a:A)(compat_op E.eq eqA f) -> 
-     (eqA (fold_tree f s a) (fold_tree' f s a)).
-   Proof.
-   Unfold fold_tree' elements_tree. 
-   Induction s; Simpl; Auto; Intros.
-   Apply Seq_refl; Auto.
-   Apply Seq_sym; Auto.
-   EApply (Seq_trans ?? st).
-   Apply (fold_tree_equiv_aux ? eqA); Simpl; Auto.
-   Apply (fold_tree_compat ? eqA); Simpl; Auto.
-   Apply Seq_sym; Auto.
-   Qed.
-
-  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_tree f s i) i).
-  Proof.
-    Intros (s,Hs,Hrb); Unfold Empty Add In; Simpl; Clear Hs Hrb.
-    Case s; Simpl; Intuition.
-    Elim (H t1); Auto.
-  Save.   
-
-  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_tree f s' i) (f x (fold_tree f s i))).
-  Proof.
-  Intros (s,Hs,Hrb) (s',Hs',Hrb'); Unfold Add In; Simpl; Intros.
-  EApply (Seq_trans ?? st).
-  Apply (fold_tree_equiv ? eqA); Auto.
-  EApply (Seq_trans ?? st) with (f x (fold_tree' f s i)).
-  Unfold fold_tree'. 
-  Generalize (elements_tree_sort s Hs) (elements_tree_sort s' Hs').
-  LetTac l := (elements_tree s).
-  LetTac l' := (elements_tree s').
-  Intros Hl Hl'.
-  Apply (!Lists.Raw.fold_2 l l' Hl Hl' x A eqA) ; Auto.  
-  Unfold Lists.Raw.Add l l'; Split; Intros; Elim (H2 y);  Intuition; Elim H4; Auto.
-  Apply (Seq_sym ?? st).
-  Apply H; Auto.
-  Apply (fold_tree_equiv ? eqA); Auto.
+  Lemma fold_tree_equiv : 
+     (A:Set)(s:tree)(f:elt->A->A; a:A)
+     (fold_tree f s a)=(fold_tree' f s a).
+  Proof.
+  Unfold fold_tree' elements_tree. 
+  Induction s; Simpl; Auto; Intros.
+  Rewrite fold_tree_equiv_aux.
+  Rewrite H0.
+  Simpl; Auto.
   Qed.
 
   Definition fold : 
-   (A:Set)
-   (f:elt->A->A) 
-   { fold:t -> A -> A | (s,s':t)(a:A)
-      (eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
-      ((Empty s) -> (eqA (fold s a) a)) /\
-      ((compat_op E.eq eqA f)->(transpose eqA f) ->
-        (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }.  
-  Proof.
-    Intros A f; Exists [s:t](fold_tree f s); Split; Intros.
-    Apply fold_1; Auto.
-    Apply (fold_2 s s' x A eqA); Auto.
+   (A:Set)(f:elt->A->A)(s:t)(i:A) 
+   { r : A | (EX l:(list elt) | 
+                  (Unique E.eq l) /\
+                  ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+                  r = (fold_right f i l)) }.
+  Proof.
+    Intros A f s i; Exists (fold_tree f s i).
+    Rewrite fold_tree_equiv.
+    Unfold fold_tree'.
+    Elim (Lists.Raw.fold_1 (elements_tree_sort ? (is_bst s)) i f); Intro l.
+    Exists l; Elim H; Clear H; Intros H1 (H2,H3); Split; Auto.
+    Split; Auto.
+    Intros x; Generalize (elements_tree_1 s x) (elements_tree_2 s x).
+    Generalize (H2 x); Unfold In; Ground.
   Defined.
 
   (** * Cardinal *)
 
   Definition cardinal : 
-    {cardinal : t -> nat | (s,s':t)
-       ((Empty s) -> (cardinal s)=O) /\
-       ((x:elt) (Add x s s') -> ~(In x s) -> (cardinal s')=(S (cardinal s)))}.
-  Proof.
-    Assert st : (Setoid_Theory ? (eq nat)).
-     Constructor; Auto; Intros; EApply trans_eq; EAuto.
-    Elim (fold nat [_]S); Intro f; Exists [s:t](f s O); Split; Intros.
-    Elim (p s s O ? st); Auto.
-    Elim (p s s' O ? st); Intros; EApply H2; EAuto.
+     (s:t) { r : nat | (EX l:(list elt) | 
+                              (Unique E.eq l) /\ 
+                              ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
+                              r = (length l)) }.
+  Proof.
+    Intros; Elim (fold nat [_]S s O); Intro n; Exists n.
+    Assert (l:(list elt))(length l)=(fold_right [_]S O l). 
+     Induction l; Simpl; Auto.
+    Elim p; Intro l; Exists l; Rewrite H; Auto.
   Qed.
 
   (** * Filter *)