Rework of FSetProperties, in order to add more easily a Properties functor

for FMap (for the moment in FMapFacts).



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

8 files changed, 850 insertions, 378 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 6b1ef79c3..115f75dc4 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -555,3 +555,474 @@ Qed.
 End BoolSpec.
 
 End Facts.
+
+Module Properties (M: S).
+ Module F:=Facts M. 
+ Import F.
+ Module O:=KeyOrderedType M.E.
+ Import O.
+ Import M.
+
+ Section Elt. 
+  Variable elt:Set.
+
+  Definition cardinal (m:t elt) := length (elements m).
+
+  Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
+
+  Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
+  Definition Below x (m:t elt) := forall y, In y m -> E.lt x y.
+
+  Section Elements.
+
+  Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
+  Proof.
+  intros.
+  unfold Empty.
+  split; intros.
+  assert (forall a, ~ List.In a (elements m)).
+   red; intros.
+   apply (H (fst a) (snd a)).
+   rewrite elements_mapsto_iff.
+   rewrite InA_alt; exists a; auto.
+   split; auto; split; auto.
+  destruct (elements m); auto.
+  elim (H0 p); simpl; auto.
+  red; intros.
+  rewrite elements_mapsto_iff in H0.
+  rewrite InA_alt in H0; destruct H0.
+  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
+  Qed.
+
+  Notation eqke := (@eqke elt).
+  Notation eqk := (@eqk elt).
+  Notation ltk := (@ltk elt).
+
+  Definition gtb (p p':key*elt) := match E.compare (fst p) (fst p') with GT _ => true | _ => false end.
+  Definition leb p := fun p' => negb (gtb p p'). 
+
+  Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.
+  Proof.
+   intros (x,e) (y,e'); unfold gtb, O.ltk; simpl.
+   destruct (E.compare x y); intuition; try discriminate; ME.order.
+  Qed.
+
+  Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p.
+  Proof.
+   intros (x,e) (y,e'); unfold leb, gtb, O.ltk; simpl.
+   destruct (E.compare x y); intuition; try discriminate; ME.order.
+  Qed.
+
+  Lemma gtb_compat : forall p, compat_bool eqke (gtb p).
+  Proof.
+   red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H.
+   generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e'')); 
+    destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto.
+   unfold O.ltk in *; simpl in *; intros.
+   symmetry; rewrite H2.
+   apply ME.eq_lt with a; auto.
+   rewrite <- H1; auto.
+   unfold O.ltk in *; simpl in *; intros.
+   rewrite H1.
+   apply ME.eq_lt with b; auto.
+   rewrite <- H2; auto.
+  Qed.
+
+  Lemma leb_compat : forall p, compat_bool eqke (leb p).
+  Proof.
+   red; intros x a b H.
+   unfold leb; f_equal; apply gtb_compat; auto.
+  Qed.
+
+  Hint Resolve gtb_compat leb_compat elements_3.
+
+  Lemma elements_split : forall p m, 
+    elements m = 
+    List.filter (gtb p) (elements m) ++ List.filter (leb p) (elements m).
+  Proof.
+  unfold leb; intros.
+  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto.
+  intros; destruct x; destruct y; destruct p.
+  rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.
+  assert (~ltk (t1,e0) (k,e1)).
+   unfold gtb, O.ltk in *; simpl in *.
+   destruct (E.compare k t1); intuition; try discriminate; ME.order.
+  unfold O.ltk in *; simpl in *; ME.order.
+  Qed.
+
+  Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt),
+   sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.
+  Proof.
+  apply SortA_equivlistA_eqlistA; eauto; 
+  unfold O.eqke, O.ltk; simpl; intuition; eauto.
+  Qed.
+
+  Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.
+
+  Lemma elements_Add : forall m m' x e, ~In x m -> Add x e m m' -> 
+    eqlistA eqke (elements m') 
+      (List.filter (gtb (x,e)) (elements m) ++ 
+       (x,e)::List.filter (leb (x,e)) (elements m)).
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  apply (@SortA_app _ eqke); auto.
+  apply (@filter_sort _ eqke); auto; clean_eauto.
+  constructor; auto.
+  apply (@filter_sort _ eqke); auto; clean_eauto.
+  rewrite (@InfA_alt _ eqke); auto; try (clean_eauto; fail).
+  apply (@filter_sort _ eqke); auto; clean_eauto.
+  intros.
+  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite leb_1 in H2.
+  destruct y; unfold O.ltk in *; simpl in *.
+  rewrite <- elements_mapsto_iff in H1.
+  assert (~E.eq x t0).
+   swap H.
+   exists e0; apply MapsTo_1 with t0; auto.
+  ME.order.
+  intros.
+  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite gtb_1 in H3.
+  destruct y; destruct x0; unfold O.ltk in *; simpl in *.
+  inversion_clear H2.
+  red in H4; simpl in *; destruct H4.
+  ME.order.
+  rewrite filter_InA in H4; auto; destruct H4.
+  rewrite leb_1 in H4.
+  unfold O.ltk in *; simpl in *; ME.order.
+  red; intros a; destruct a.
+  rewrite InA_app_iff; rewrite InA_cons.
+  do 2 (rewrite filter_InA; auto).
+  do 2 rewrite <- elements_mapsto_iff.
+  rewrite leb_1; rewrite gtb_1.
+  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
+  rewrite add_mapsto_iff.
+  unfold O.eqke, O.ltk; simpl.
+  destruct (E.compare t0 x); intuition.
+  right; split; auto; ME.order.
+  ME.order.
+  elim H.
+  exists e0; apply MapsTo_1 with t0; auto.
+  right; right; split; auto; ME.order.
+  ME.order.
+  right; split; auto; ME.order.
+  Qed.
+
+  Lemma elements_eqlistA_max : forall m m' x e, 
+   Above x m -> Add x e m m' -> 
+     eqlistA eqke (elements m') (elements m ++ (x,e)::nil).
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  apply (@SortA_app _ eqke); auto.
+  intros.
+  inversion_clear H2.
+  destruct x0; destruct y.
+  rewrite <- elements_mapsto_iff in H1.
+  unfold O.eqke, O.ltk in *; simpl in *; destruct H3.
+  apply ME.lt_eq with x; auto.
+  apply H; firstorder.
+  inversion H3.
+  red; intros a; destruct a.
+  rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
+  do 2 rewrite <- elements_mapsto_iff.
+  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
+  rewrite add_mapsto_iff; unfold O.eqke; simpl.
+  intuition.
+  destruct (ME.eq_dec x t0); auto.
+  elimtype False.
+  assert (In t0 m).
+   exists e0; auto.
+  generalize (H t0 H1).
+  ME.order.
+  Qed.
+
+  Lemma elements_eqlistA_min : forall m m' x e, 
+   Below x m -> Add x e m m' -> 
+     eqlistA eqke (elements m') ((x,e)::elements m).
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  change (sort ltk (((x,e)::nil) ++ elements m)).
+  apply (@SortA_app _ eqke); auto.
+  intros.
+  inversion_clear H1.
+  destruct y; destruct x0.
+  rewrite <- elements_mapsto_iff in H2.
+  unfold O.eqke, O.ltk in *; simpl in *; destruct H3.
+  apply ME.eq_lt with x; auto.
+  apply H; firstorder.
+  inversion H3.
+  red; intros a; destruct a.
+  rewrite InA_cons.
+  do 2 rewrite <- elements_mapsto_iff.
+  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
+  rewrite add_mapsto_iff; unfold O.eqke; simpl.
+  intuition.
+  destruct (ME.eq_dec x t0); auto.
+  elimtype False.
+  assert (In t0 m).
+   exists e0; auto.
+  generalize (H t0 H1).
+  ME.order.
+  Qed.
+
+  End Elements.
+
+  Section Cardinal.
+
+  Lemma cardinal_Empty : forall m, Empty m <-> cardinal m = 0.
+  Proof.
+   intros.
+   rewrite elements_Empty.
+   unfold cardinal.
+   destruct (elements m); intuition; discriminate.
+  Qed.
+
+  Lemma cardinal_inv_1 : forall (m:t elt), cardinal m = 0 -> Empty m. 
+  Proof. 
+    intros m; unfold cardinal; intros H e a.
+    rewrite elements_mapsto_iff.
+    destruct (elements m); simpl in *; discriminate || red; inversion 1.
+  Qed.
+
+  Lemma cardinal_inv_2 :
+   forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof. 
+    intros; unfold cardinal in *.
+    generalize (elements_2 (m:=m)).
+    destruct (elements m); try discriminate. 
+    exists p; auto.
+    destruct p; simpl; auto.
+    apply H0; constructor; red; auto.
+  Qed.
+
+  Lemma cardinal_1 : forall (m:t elt), Empty m -> cardinal m = 0.
+  Proof.
+    intros; rewrite <- cardinal_Empty; auto.
+  Qed.
+
+  Lemma cardinal_2 : forall m m' x e, ~In x m -> Add x e m m' -> 
+    cardinal m' = S (cardinal m).
+  Proof.
+  intros.
+  unfold cardinal.
+  unfold key.
+  rewrite (eqlistA_length (elements_Add H H0)); simpl.
+  rewrite app_length; simpl.
+  rewrite <- plus_n_Sm.
+  f_equal.
+  rewrite <- app_length.
+  f_equal.
+  symmetry; apply elements_split; auto.
+  Qed.
+
+  End Cardinal.
+
+  Section Min_Max_Elt.
+
+  (** We emulate two [max_elt] and [min_elt] functions. *)
+  
+  Fixpoint max_elt_aux (l:list (key*elt)) := match l with 
+    | nil => None 
+    | (x,e)::nil => Some (x,e)
+    | (x,e)::l => max_elt_aux l
+    end.
+  Definition max_elt m := max_elt_aux (elements m).
+
+  Lemma max_elt_Above : 
+   forall m x e, max_elt m = Some (x,e) -> Above x (remove x m).
+  Proof.
+  red; intros.
+  rewrite remove_in_iff in H0.
+  destruct H0.
+  rewrite elements_in_iff in H1.
+  destruct H1.
+  unfold max_elt in *.
+  generalize (elements_3 m).
+  revert x e H y x0 H0 H1.
+  induction (elements m).
+  simpl; intros; try discriminate.
+  intros.
+  destruct a; destruct l; simpl in *.
+  injection H; clear H; intros; subst.
+  inversion_clear H1.
+  red in H; simpl in *; intuition.
+  elim H0; eauto.
+  inversion H.
+  change (max_elt_aux (p::l) = Some (x,e)) in H.
+  generalize (IHl x e H); clear IHl; intros IHl.
+  inversion_clear H1; [ | inversion_clear H2; eauto ].
+  red in H3; simpl in H3; destruct H3.
+  destruct p as (p1,p2).
+  destruct (ME.eq_dec p1 x).
+  apply ME.lt_eq with p1; auto.
+   inversion_clear H2.
+   inversion_clear H5.
+   red in H2; simpl in H2; ME.order.
+  apply E.lt_trans with p1; auto.
+   inversion_clear H2.
+   inversion_clear H5.
+   red in H2; simpl in H2; ME.order.
+  eapply IHl; eauto.
+  econstructor; eauto.
+  red; eauto.
+  inversion H2; auto.
+  Qed.
+  
+  Lemma max_elt_MapsTo : 
+   forall m x e, max_elt m = Some (x,e) -> MapsTo x e m.
+  Proof.
+  intros.
+  unfold max_elt in *.
+  rewrite elements_mapsto_iff.
+  induction (elements m).
+  simpl; try discriminate.
+  destruct a; destruct l; simpl in *.
+  injection H; intros; subst; constructor; red; auto.
+  constructor 2; auto.
+  Qed.
+
+  Lemma max_elt_Empty : 
+   forall m, max_elt m = None -> Empty m.
+  Proof.
+  intros.
+  unfold max_elt in *.
+  rewrite elements_Empty.
+  induction (elements m); auto.
+  destruct a; destruct l; simpl in *; try discriminate.
+  assert (H':=IHl H); discriminate.
+  Qed.
+
+  Definition min_elt m : option (key*elt) := match elements m with 
+   | nil => None
+   | (x,e)::_ => Some (x,e)
+  end.
+
+  Lemma min_elt_Below : 
+   forall m x e, min_elt m = Some (x,e) -> Below x (remove x m).
+  Proof.
+  unfold min_elt, Below; intros.
+  rewrite remove_in_iff in H0; destruct H0.
+  rewrite elements_in_iff in H1.
+  destruct H1.
+  generalize (elements_3 m).
+  destruct (elements m).
+  try discriminate.
+  destruct p; injection H; intros; subst.
+  inversion_clear H1.
+  red in H2; destruct H2; simpl in *; ME.order.
+  inversion_clear H4.
+  rewrite (@InfA_alt _ (@eqke elt)) in H3; eauto.
+  apply (H3 (y,x0)); auto.
+  unfold lt_key; simpl; intuition; eauto.
+  unfold eqke, lt_key; simpl; intuition; eauto.
+  unfold eqke, lt_key; simpl; intuition; eauto.
+  Qed.
+  
+  Lemma min_elt_MapsTo : 
+   forall m x e, min_elt m = Some (x,e) -> MapsTo x e m.
+  Proof.
+  intros.
+  unfold min_elt in *.
+  rewrite elements_mapsto_iff.
+  destruct (elements m).
+  simpl; try discriminate.
+  destruct p; simpl in *.
+  injection H; intros; subst; constructor; red; auto.
+  Qed.
+
+  Lemma min_elt_Empty : 
+   forall m, min_elt m = None -> Empty m.
+  Proof.
+  intros.
+  unfold min_elt in *.
+  rewrite elements_Empty.
+  destruct (elements m); auto.
+  destruct p; simpl in *; discriminate.
+  Qed.
+
+  End Min_Max_Elt.
+
+  Section Induction_Principles.
+ 
+  Lemma map_induction :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
+   forall m, P m.
+  Proof.
+  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
+  apply X; apply cardinal_inv_1; auto.
+
+  destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
+  assert (Add x e (remove x m) m).
+   red; intros.
+   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto.
+  apply X0 with (remove x m) x e; auto.
+  apply IHn; auto.
+  assert (S n = S (cardinal (remove x m))).
+   rewrite Heqn; eapply cardinal_2; eauto.
+  inversion H1; auto.
+  Qed.
+
+  Lemma map_induction_max :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, Above x m -> Add x e m m' -> P m') ->
+   forall m, P m.
+  Proof.
+  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
+  apply X; apply cardinal_inv_1; auto.
+
+  case_eq (max_elt m); intros.
+  destruct p.
+  assert (Add k e (remove k m) m).
+   red; intros.
+   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto.
+   apply find_1; apply MapsTo_1 with k; auto.
+   apply max_elt_MapsTo; auto.
+  apply X0 with (remove k m) k e; auto.
+  apply IHn.
+  assert (S n = S (cardinal (remove k m))).
+   rewrite Heqn.
+   eapply cardinal_2; eauto.
+  inversion H1; auto. 
+  eapply max_elt_Above; eauto.
+
+  apply X; apply max_elt_Empty; auto.
+  Qed.
+
+  Lemma map_induction_min :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, Below x m -> Add x e m m' -> P m') ->
+   forall m, P m.
+  Proof.
+  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
+  apply X; apply cardinal_inv_1; auto.
+
+  case_eq (min_elt m); intros.
+  destruct p.
+  assert (Add k e (remove k m) m).
+   red; intros.
+   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto.
+   apply find_1; apply MapsTo_1 with k; auto.
+   apply min_elt_MapsTo; auto.
+  apply X0 with (remove k m) k e; auto.
+  apply IHn.
+  assert (S n = S (cardinal (remove k m))).
+   rewrite Heqn.
+   eapply cardinal_2; eauto.
+  inversion H1; auto. 
+  eapply min_elt_Below; eauto.
+
+  apply X; apply min_elt_Empty; auto.
+  Qed.
+
+  End Induction_Principles.
+ End Elt.
+
+End Properties.
+
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 03c64b1ef..0bd2c4525 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -13,9 +13,10 @@
 (** This file proposes an interface for finite maps *)
 
 (* begin hide *)
+Require Export Bool.
+Require Export OrderedType.
 Set Implicit Arguments.
 Unset Strict Implicit.
-Require Import FSetInterface. 
 (* end hide *)
 
 (** When compared with Ocaml Map, this signature has been split in two: 
diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v
index c5f5fd7df..5a9d3cca6 100644
--- a/theories/FSets/FMapWeakInterface.v
+++ b/theories/FSets/FMapWeakInterface.v
@@ -13,10 +13,12 @@
 (** This file proposes an interface for finite maps over keys with decidable 
      equality, but no decidable order. *)
 
+(* begin hide *)
+Require Export Bool.
+Require Export DecidableType.
 Set Implicit Arguments.
 Unset Strict Implicit.
-Require Import FSetInterface. 
-Require Import FSetWeakInterface. 
+(* end hide *)
 
 Module Type S.
 
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index a970c092d..9e1ca4058 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -478,29 +478,21 @@ Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
    add_mem_3 add_equal remove_mem_3 remove_equal : set.
 
 
-(** General recursion principes based on [cardinal] *)
+(** General recursion principle *)
 
-Lemma cardinal_set_rec:  forall (P:t->Type),
+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 n s, cardinal s=n -> P s.
+ P empty -> forall s, P s.
 Proof.
 intros.
-apply cardinal_induction with n; auto; 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 (H1 a); tauto.
+apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
 apply X0; auto with set; apply mem_3; auto.
 Qed.
 
-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 cardinal_set_rec with (cardinal s);auto.
-Qed.
-
 (** Properties of [fold] *)
 
 Lemma exclusive_set : forall s s' x,
@@ -870,9 +862,9 @@ assert (fgt : transpose (@eq _) (fun x:elt=>plus ((f x)+(g x)))). red; intros; o
 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.
+rewrite <- (fold_equal _ _ st _ fc 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ gc 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ fgc 0 _ _ H); auto.
 intros; do 3 (rewrite (fold_add _ _ st);auto).
 rewrite H0;simpl;omega.
 intros; do 3 rewrite (fold_empty _ _ st);auto.
@@ -891,7 +883,7 @@ assert (ct : transpose (@eq _) (fun x => plus (if f x then 1 else 0))).
 intros s;pattern s; apply set_rec.
 intros.
 change elt with E.t.
-rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ cc 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) .
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 6f23907b3..012f95d87 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -19,16 +19,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 (* end hide *)
 
-(** Compatibility of a  boolean function with respect to an equality. *)
-Definition compat_bool (A:Type)(eqA: A->A->Prop)(f: A-> bool) :=
-  forall x y : A, eqA x y -> f x = f y.
-
-(** Compatibility of a predicate with respect to an equality. *)
-Definition compat_P (A:Type)(eqA: A->A->Prop)(P : A -> Prop) :=
-  forall x y : A, eqA x y -> P x -> P y.
-
-Hint Unfold compat_bool compat_P.
-
 (** * Non-dependent signature
 
     Signature [S] presents sets as purely informative programs 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 76448357a..21ca1120c 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -37,8 +37,10 @@ Module Properties (M: S).
   Module FM := Facts M.
   Import FM.
 
-  Definition Add (x : elt) (s s' : t) :=
-    forall y : elt, In y s' <-> E.eq x y \/ In y s.
+  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
+  Definition Above x s := forall y, In y s -> E.lt y x.
+  Definition Below x s := forall y, In y s -> E.lt x y.
+
 
   Lemma In_dec : forall x s, {In x s} + {~ In x s}.
   Proof.
@@ -453,109 +455,182 @@ Module Properties (M: S).
     remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
     Equal_remove add_add : set.
 
-  (** * Alternative (weaker) specifications for [fold] *)
+  (** * Properties of elements *)
 
-  Section Old_Spec_Now_Properties. 
+  Section Elements.
 
-  Notation NoDup := (NoDupA E.eq).
+  Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
+  Proof.
+  intros.
+  unfold Empty.
+  split; intros.
+  assert (forall a, ~ List.In a (elements s)).
+   red; intros.
+   apply (H a).
+   rewrite elements_iff.
+   rewrite InA_alt; exists a; auto.
+  destruct (elements s); auto.
+  elim (H0 e); simpl; auto.
+  red; intros.
+  rewrite elements_iff in H0.
+  rewrite InA_alt in H0; destruct H0.
+  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
+  Qed.
 
-  (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
-        takes the set elements was unspecified. This specification reflects this fact: 
-  *)
+  Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
+  Definition leb x := fun y => negb (gtb x y).
 
-  Lemma fold_0 : 
-      forall s (A : Type) (i : A) (f : elt -> A -> A),
-      exists l : list elt,
-        NoDup l /\
-        (forall x : elt, In x s <-> InA E.eq x l) /\
-        fold f s i = fold_right f i l.
+  Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
   Proof.
-  intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto.
-  exact E.eq_trans.
-  split; intros.
-  rewrite elements_iff; do 2 rewrite InA_alt.
-  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
-  rewrite fold_left_rev_right.
-  apply fold_1.
+   intros; unfold gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
   Qed.
 
-  (** 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 leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
+  Proof.
+   intros; unfold leb, gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
+  Qed.
 
-  Lemma fold_1 :
-   forall s (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.
+  Lemma gtb_compat : forall x, compat_bool E.eq (gtb x).
   Proof.
-  unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).
-  rewrite H3; clear H3.
-  generalize H H2; clear H H2; case l; simpl; intros.
-  refl_st.
-  elim (H e).
-  elim (H2 e); intuition. 
+   red; intros x a b H.
+   generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.
+   intros.
+   symmetry; rewrite H1.
+   apply ME.eq_lt with a; auto.
+   rewrite <- H0; auto.
+   intros.
+   rewrite H0.
+   apply ME.eq_lt with b; auto.
+   rewrite <- H1; auto.
   Qed.
 
-  Lemma fold_2 :
-   forall s s' x (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)).
+  Lemma leb_compat : forall x, compat_bool E.eq (leb x).
   Proof.
-  intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
-    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
-  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
-  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
-  eauto.
-  exact eq_dec.
-  rewrite <- Hl1; auto.
-  intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
+   red; intros x a b H; unfold leb.
+   f_equal; apply gtb_compat; auto.
   Qed.
+  Hint Resolve gtb_compat leb_compat.
 
-  (** Similar specifications for [cardinal]. *)
+  Lemma elements_split : forall x s, 
+   elements s = List.filter (gtb x) (elements s) ++ List.filter (leb x) (elements s).
+  Proof.
+  unfold leb; intros.
+  eapply (@filter_split _ E.eq); eauto. ME.order. ME.order. ME.order.
+  intros.
+  rewrite gtb_1 in H.
+  assert (~E.lt y x).
+   unfold gtb in *; destruct (E.compare x y); intuition; try discriminate; ME.order.
+  ME.order.
+  Qed.
 
-  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
+  (* a specialized version of SortA_equivlistA_eqlistA: *)
+  Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
+   sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
   Proof.
-  intros; rewrite cardinal_1; rewrite M.fold_1.
-  symmetry; apply fold_left_length; auto.
+  apply SortA_equivlistA_eqlistA; eauto.
   Qed.
 
-  Lemma cardinal_0 :
-     forall s, exists l : list elt,
-        NoDupA E.eq l /\
-        (forall x : elt, In x s <-> InA E.eq x l) /\ 
-        cardinal s = length l.
-  Proof. 
-  intros; exists (elements s); intuition; apply cardinal_1.
+  Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' -> 
+    eqlistA E.eq (elements s') 
+      (List.filter (gtb x) (elements s) ++ x::List.filter (leb x) (elements s)).
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  apply (@SortA_app _ E.eq); auto.
+  apply (@filter_sort _ E.eq); auto; eauto.
+  constructor; auto.
+  apply (@filter_sort _ E.eq); auto; eauto.
+  rewrite Inf_alt; auto; intros.
+  apply (@filter_sort _ E.eq); auto; eauto.
+  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite leb_1 in H2.
+  rewrite <- elements_iff in H1.
+  assert (~E.eq x y).
+   swap H; rewrite H3; auto.
+  ME.order.
+  intros.
+  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite gtb_1 in H3.
+  inversion_clear H2.
+  ME.order.
+  rewrite filter_InA in H4; auto; destruct H4.
+  rewrite leb_1 in H4.
+  ME.order.
+  red; intros a.
+  rewrite InA_app_iff; rewrite InA_cons.
+  do 2 (rewrite filter_InA; auto).
+  do 2 rewrite <- elements_iff.
+  rewrite leb_1; rewrite gtb_1.
+  rewrite (H0 a); intuition.
+  destruct (E.compare a x); intuition.
+  right; right; split; auto.
+  ME.order.
   Qed.
 
-  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
+  Lemma elements_eqlistA_max : forall s s' x, 
+   Above x s -> Add x s s' -> 
+     eqlistA E.eq (elements s') (elements s ++ x::nil).
   Proof.
-  intros; rewrite cardinal_fold; apply fold_1; auto.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  apply (@SortA_app _ E.eq); auto.
+  intros.
+  inversion_clear H2.
+  rewrite <- elements_iff in H1.
+  apply lt_eq with x; auto.
+  inversion H3.
+  red; intros a.
+  rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
+  do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
-  Lemma cardinal_2 :
-    forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
+  Lemma elements_eqlistA_min : forall s s' x, 
+   Below x s -> Add x s s' -> 
+     eqlistA E.eq (elements s') (x::elements s).
   Proof.
-  intros; do 2 rewrite cardinal_fold.
-  change S with ((fun _ => S) x).
-  apply fold_2; auto.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  change (sort E.lt ((x::nil) ++ elements s)).
+  apply (@SortA_app _ E.eq); auto.
+  intros.
+  inversion_clear H1.
+  rewrite <- elements_iff in H2.
+  apply eq_lt with x; auto.
+  inversion H3.
+  red; intros a.
+  rewrite InA_cons.
+  do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
-  End Old_Spec_Now_Properties.
+  End Elements.
 
-  (** * Induction principle over sets *)
+  (** * Properties of cardinal (proved using [elements]) *)
+
+  Section Cardinal.
+
+  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
+  Proof.
+  intros.
+  do 2 rewrite M.cardinal_1.
+  apply (@eqlistA_length _ E.eq); auto.
+  apply sort_equivlistA_eqlistA; auto.
+  red; intro a.
+  do 2 rewrite <- elements_iff; auto.
+  Qed.
+
+  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
+  Proof.
+   intros.
+   rewrite elements_Empty.
+   rewrite cardinal_1.
+   destruct (elements s); intuition; discriminate.
+  Qed.
 
   Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. 
   Proof. 
-    intros s; rewrite M.cardinal_1; intros H a; red.
-    rewrite elements_iff.
-    destruct (elements s); simpl in *; discriminate || inversion 1.
+    intros. rewrite cardinal_Empty; auto.
   Qed.
-  Hint Resolve cardinal_inv_1.
- 
+
   Lemma cardinal_inv_2 :
    forall s n, cardinal s = S n -> { x : elt | In x s }.
   Proof. 
@@ -565,25 +640,28 @@ Module Properties (M: S).
     exists e; auto.
   Qed.
 
-  Lemma Equal_cardinal_aux :
-   forall n s s', cardinal s = n -> s[=]s' -> cardinal s = cardinal s'.
+  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
   Proof.
-     simple induction n; intros.
-     rewrite H; symmetry .
-     apply cardinal_1.
-     rewrite <- H0; auto.
-     destruct (cardinal_inv_2 H0) as (x,H2).
-     revert H0.
-     rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
-     rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); auto with set.
-     rewrite H1 in H2; auto with set.
+    intros. rewrite <- cardinal_Empty; auto.
   Qed.
 
-  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
-  Proof. 
-    intros; apply Equal_cardinal_aux with (cardinal s); auto.
+  Lemma cardinal_2 : forall s s' x, ~In x s -> Add x s s' -> 
+    cardinal s' = S (cardinal s).
+  Proof.
+  intros.
+  do 2 rewrite M.cardinal_1.
+  unfold elt.
+  rewrite (eqlistA_length (elements_Add H H0)); simpl.
+  rewrite app_length; simpl.
+  rewrite <- plus_n_Sm.
+  f_equal.
+  rewrite <- app_length.
+  f_equal.
+  symmetry; apply elements_split; auto.
   Qed.
 
+  End Cardinal.
+
   Add Morphism cardinal : cardinal_m.
   Proof.
   exact Equal_cardinal.
@@ -591,70 +669,211 @@ Module Properties (M: S).
 
   Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
 
-  Lemma cardinal_induction :
+  (** * Induction principle over sets *)
+
+  Section Induction_Principles.
+
+  Lemma set_induction :
    forall P : t -> Type,
-   (forall s, Empty s -> P s) ->
-   (forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
-   forall n s, cardinal s = n -> P s.
+   (forall s : t, Empty s -> P s) ->
+   (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
+   forall s : t, P s.
   Proof.
-  simple induction n; intros; auto.
-  destruct (cardinal_inv_2 H) as (x,H0). 
-  apply X0 with (remove x s) x; auto.
-  apply X1; auto.
-  rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto.
+  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+  destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). 
+  apply X0 with (remove x s) x; auto with set.
+  apply IHn; auto.
+  assert (S n = S (cardinal (remove x s))).
+    rewrite Heqn; apply cardinal_2 with x; auto with set.
+  inversion H; auto.
   Qed.
 
-  Lemma set_induction :
+  (** Two other induction principles on sets: we can be more restrictive 
+      on the element we add at each step.  *)
+
+  Lemma set_induction_max :
    forall P : t -> Type,
    (forall s : t, Empty s -> P s) ->
-   (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
+   (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
    forall s : t, P s.
   Proof.
-  intros; apply cardinal_induction with (cardinal s); auto.
+  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+  case_eq (max_elt s); intros.
+  apply X0 with (remove e s) e; auto with set.
+  apply IHn.
+  assert (S n = S (cardinal (remove e s))).
+   rewrite Heqn; apply cardinal_2 with e; auto with set.
+  inversion H0; auto.
+  red; intros.
+  rewrite remove_iff in H0; destruct H0.
+  generalize (@max_elt_2 s e y H H0); ME.order.
+
+  assert (H0:=max_elt_3 H).
+  rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn.
   Qed.  
 
+  Lemma set_induction_min :
+   forall P : t -> Type,
+   (forall s : t, Empty s -> P s) ->
+   (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
+   forall s : t, P s.
+  Proof.
+  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+  case_eq (min_elt s); intros.
+  apply X0 with (remove e s) e; auto with set.
+  apply IHn.
+  assert (S n = S (cardinal (remove e s))).
+   rewrite Heqn; apply cardinal_2 with e; auto with set. 
+  inversion H0; auto.
+  red; intros.
+  rewrite remove_iff in H0; destruct H0.
+  generalize (@min_elt_2 s e y H H0); ME.order.
+
+  assert (H0:=min_elt_3 H).
+  rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn.
+  Qed.
+
+  End Induction_Principles.
+
+  Section Fold_Basic. 
+
+  Notation NoDup := (NoDupA E.eq).
+ 
+  (** * Alternative (weaker) specifications for [fold] *)
+
+  (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
+        takes the set elements was unspecified. This specification reflects this fact: 
+  *)
+
+  Lemma fold_0 : 
+      forall s (A : Type) (i : A) (f : elt -> A -> A),
+      exists l : list elt,
+        NoDup l /\
+        (forall x : elt, In x s <-> InA E.eq x l) /\
+        fold f s i = fold_right f i l.
+  Proof.
+  intros; exists (rev (elements s)); split.
+  apply NoDupA_rev; auto.
+  exact E.eq_trans.
+  split; intros.
+  rewrite elements_iff; do 2 rewrite InA_alt.
+  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
+  rewrite fold_left_rev_right.
+  apply fold_1.
+  Qed.
+
+  (** 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 :
+   forall s (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; rewrite M.fold_1.
+  rewrite elements_Empty in H; rewrite H.
+  simpl; refl_st.
+  Qed.
+
+  Lemma fold_2 :
+   forall s s' x (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; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
+    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
+  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
+  eauto.
+  exact eq_dec.
+  rewrite <- Hl1; auto.
+  intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
+  Qed.
+
+  (** More properties of [fold] : behavior with respect to Above/Below *) 
+
+  Lemma fold_3 :
+   forall s s' x (A : Set) (eqA : A -> A -> Prop)
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   compat_op E.eq eqA f ->
+   Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
+  Proof.
+  intros.
+  do 2 rewrite M.fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  change (f x (fold_right f i (rev (elements s)))) with 
+    (fold_right f i (rev (x::nil)++rev (elements s))).
+  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
+  rewrite <- distr_rev.
+  apply eqlistA_rev.
+  apply elements_eqlistA_max; auto.
+  Qed.
+
+  Lemma fold_4 :
+   forall s s' x (A : Set) (eqA : A -> A -> Prop)
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   compat_op E.eq eqA f ->
+   Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
+  Proof.
+  intros.
+  do 2 rewrite M.fold_1.
+  set (g:=fun (a : A) (e : elt) => f e a).
+  change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)).
+  unfold g.
+  do 2 rewrite <- fold_left_rev_right.
+  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
+  apply eqlistA_rev.
+  apply elements_eqlistA_min; auto.
+  Qed.
+
+  End Fold_Basic.
+
   (** Other properties of [fold]. *)
 
-  Section Fold. 
+  Section Fold_More. 
   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).
 
-  Section Fold_1. 
-  Variable i i':A.
-
-  Lemma fold_empty : eqA (fold f empty i) i.
+  Lemma fold_empty : forall i, eqA (fold f empty i) i.
   Proof. 
-  apply fold_1; auto.
+  intros; apply fold_1; auto.
   Qed.
 
   Lemma fold_equal : 
-   forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
+   forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
+  Proof.
+  intros; do 2 rewrite M.fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
+  apply eqlistA_rev.
+  apply sort_equivlistA_eqlistA; auto.
+  red; intro a; do 2 rewrite <- elements_iff; auto.
+  Qed.
+
+  Lemma fold_init : forall i i' s, eqA i i' -> 
+   eqA (fold f s i) (fold f s i').
   Proof. 
-  intros s; pattern s; apply set_induction; clear s; intros.
-  trans_st i.
-  apply fold_1; auto.
-  sym_st; apply fold_1; auto.
-  rewrite <- H0; auto.
-  trans_st (f x (fold f s i)).
-  apply fold_2 with (eqA := eqA); auto.
-  sym_st; apply fold_2 with (eqA := eqA); auto.
-  unfold Add in *; intros.
-  rewrite <- H2; auto.
+  intros; do 2 rewrite M.fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  induction (rev (elements s)); simpl; auto.
   Qed.
-   
-  Lemma fold_add : forall s x, ~In x s -> 
+
+  Lemma fold_add : forall i s x, ~In x s -> 
    eqA (fold f (add x s) i) (f x (fold f s i)).
   Proof. 
   intros; apply fold_2 with (eqA := eqA); auto.
   Qed.
 
-  Lemma add_fold : forall s x, In x s -> 
+  Lemma add_fold : forall i s x, In x s -> 
    eqA (fold f (add x s) i) (fold f s i).
   Proof.
   intros; apply fold_equal; auto with set.
   Qed.
 
-  Lemma remove_fold_1: forall s x, In x s -> 
+  Lemma remove_fold_1: forall i s x, In x s -> 
    eqA (f x (fold f (remove x s) i)) (fold f s i).
   Proof.
   intros.
@@ -662,50 +881,24 @@ Module Properties (M: S).
   apply fold_2 with (eqA:=eqA); auto.
   Qed.
 
-  Lemma remove_fold_2: forall s x, ~In x s -> 
+  Lemma remove_fold_2: forall i s x, ~In x s -> 
    eqA (fold f (remove x s) i) (fold f s i).
   Proof.
   intros.
   apply fold_equal; auto with set.
   Qed.
 
-  Lemma fold_commutes : forall s x, 
+  Lemma fold_commutes : forall i s x, 
    eqA (fold f s (f x i)) (f x (fold f s i)).
   Proof.
-  intros; pattern s; apply set_induction; clear s; intros.
-  trans_st (f x i).
-  apply fold_1; auto.
-  sym_st.
-  apply Comp; auto.
-  apply fold_1; auto.
-  trans_st (f x0 (fold f s (f x i))).
-  apply fold_2 with (eqA:=eqA); auto.
-  trans_st (f x0 (f x (fold f s i))).
-  trans_st (f x (f x0 (fold f s i))).
-  apply Comp; auto.
-  sym_st.
-  apply fold_2 with (eqA:=eqA); auto.
-  Qed.
-
-  Lemma fold_init : forall s, eqA i i' -> 
-   eqA (fold f s i) (fold f s i').
-  Proof. 
-  intros; pattern s; apply set_induction; clear s; intros.
-  trans_st i.
-  apply fold_1; auto.
-  trans_st i'.
-  sym_st; apply fold_1; auto.
-  trans_st (f x (fold f s i)).
-  apply fold_2 with (eqA:=eqA); auto.
-  trans_st (f x (fold f s i')).
-  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  intros; do 2 rewrite M.fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  induction (rev (elements s)); simpl; auto.
+  refl_st.
+  trans_st (f a (f x (fold_right f i l))).
   Qed.
 
-  End Fold_1.
-  Section Fold_2.
-  Variable i:A.
-
-  Lemma fold_union_inter : forall s s',
+  Lemma fold_union_inter : forall i s s',
    eqA (fold f (union s s') (fold f (inter s s') i))
        (fold f s (fold f s' i)).
   Proof.
@@ -742,11 +935,7 @@ Module Properties (M: S).
   sym_st; apply fold_2 with (eqA:=eqA); auto.
   Qed.
 
-  End Fold_2.
-  Section Fold_3.
-  Variable i:A.
-
-  Lemma fold_diff_inter : forall s s', 
+  Lemma fold_diff_inter : forall i s s', 
    eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
   Proof.
   intros.
@@ -759,7 +948,7 @@ Module Properties (M: S).
   apply fold_1; auto with set.
   Qed.
 
-  Lemma fold_union: forall s s', (forall x, ~In x s\/~In x s') ->
+  Lemma fold_union: forall i s s', (forall x, ~In x s\/~In x s') ->
    eqA (fold f (union s s') i) (fold f s (fold f s' i)).
   Proof.
   intros.
@@ -770,28 +959,23 @@ Module Properties (M: S).
   apply fold_union_inter; auto.
   Qed.
 
-  End Fold_3.
-  End Fold.
+  End Fold_More.
 
   Lemma fold_plus :
    forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
   Proof.
-  assert (st := gen_st nat).
-  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by (unfold compat_op; auto). 
-  assert (fp : transpose (@eq _) (fun _:elt => S)) by (unfold transpose; auto).
-  intros s p; pattern s; apply set_induction; clear s; intros.
-  rewrite (fold_1 st p (fun _ => S) H).
-  rewrite (fold_1 st 0 (fun _ => S) H); trivial.
-  assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)).
-   change S with ((fun _ => S) x).  
-   intros; apply fold_2; auto.
-  rewrite H2; auto.
-  rewrite (H2 0); auto.
-  rewrite H.
-  simpl; auto.
+  intros; do 2 rewrite M.fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  induction (rev (elements s)); simpl; auto.
   Qed.
 
-  (** properties of [cardinal] *)
+  (** more properties of [cardinal] *)
+
+  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
+  Proof.
+  intros; rewrite M.cardinal_1; rewrite M.fold_1.
+  symmetry; apply fold_left_length; auto.
+  Qed.
 
   Lemma empty_cardinal : cardinal empty = 0.
   Proof.
@@ -909,162 +1093,4 @@ Module Properties (M: S).
 
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
 
-  (** Two other induction principles on sets: we can be more restrictive 
-      on the element we add at each step.  *)
-
-  Definition Above x s := forall y, In y s -> E.lt y x.
-  Definition Below x s := forall y, In y s -> E.lt x y.
-
-  Lemma set_induction_max :
-   forall P : t -> Type,
-   (forall s : t, Empty s -> P s) ->
-   (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
-   forall s : t, P s.
-  Proof.
-  intros.
-  remember (cardinal s) as n; revert s Heqn; induction n.
-  intros.
-  apply X.
-  apply cardinal_inv_1; auto.
-
-  intros.
-  case_eq (max_elt s); intros.
-  apply X0 with (remove e s) e.
-  apply IHn.
-  assert (S (cardinal (remove e s)) = S n).
-   rewrite Heqn.
-   apply remove_cardinal_1; auto.
-  inversion H0; auto.
-  red; intros.
-  rewrite remove_iff in H0; destruct H0.
-  generalize (@max_elt_2 s e y H H0).
-  intros.
-  destruct (E.compare y e); intuition.
-  elim H1; auto.
-  apply Add_remove; auto.
-
-  rewrite (cardinal_1 (max_elt_3 H)) in Heqn; inversion Heqn.
-  Qed.  
-
-  Lemma set_induction_min :
-   forall P : t -> Type,
-   (forall s : t, Empty s -> P s) ->
-   (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
-   forall s : t, P s.
-  Proof.
-  intros.
-  remember (cardinal s) as n; revert s Heqn; induction n.
-  intros.
-  apply X.
-  apply cardinal_inv_1; auto.
-
-  intros.
-  case_eq (min_elt s); intros.
-  apply X0 with (remove e s) e.
-  apply IHn.
-  assert (S (cardinal (remove e s)) = S n).
-   rewrite Heqn.
-   apply remove_cardinal_1; auto.
-  inversion H0; auto.
-  red; intros.
-  rewrite remove_iff in H0; destruct H0.
-  generalize (@min_elt_2 s e y H H0).
-  intros.
-  destruct (E.compare y e); intuition.
-  elim H1; auto.
-  apply Add_remove; auto.
-
-  rewrite (cardinal_1 (min_elt_3 H)) in Heqn; inversion Heqn.
-  Qed.  
-
-  Lemma elements_eqlistA_max : forall s s' x, 
-   Above x s -> Add x s s' -> 
-     eqlistA E.eq (elements s') (elements s ++ x::nil).
-  Proof.
-  intros.
-  eapply SortA_equivlistA_eqlistA; eauto.
-   apply E.lt_trans.
-   apply lt_eq.
-   apply eq_lt.
-  apply (@SortA_app E.t E.eq); auto.
-  intros.
-  inversion_clear H2.
-  rewrite <- elements_iff in H1.
-  apply lt_eq with x; auto.
-  inversion H3.
-  red; intros.
-  red in H0.
-  generalize (H0 x0); clear H0; intros.
-  do 2 rewrite elements_iff in H0.
-  rewrite H0; clear H0.
-  intuition.
-  rewrite InA_alt.
-  exists x; split; auto.
-  apply in_or_app; simpl; auto.
-  rewrite InA_alt in H1; destruct H1; intuition.
-  rewrite InA_alt; exists x1; split; auto; apply in_or_app; auto.
-  destruct (InA_app H0); auto.
-  inversion_clear H1; auto.
-  inversion H2.
-  Qed.
-
-  Lemma elements_eqlistA_min : forall s s' x, 
-   Below x s -> Add x s s' -> 
-     eqlistA E.eq (elements s') (x::elements s).
-  Proof.
-  intros.
-  eapply SortA_equivlistA_eqlistA; eauto.
-   apply E.lt_trans.
-   apply lt_eq.
-   apply eq_lt.
-  change (sort E.lt ((x::nil) ++ elements s)).
-  apply (@SortA_app E.t E.eq); auto.
-  intros.
-  inversion_clear H1.
-  rewrite <- elements_iff in H2.
-  apply eq_lt with x; auto.
-  inversion H3.
-  red; intros.
-  red in H0.
-  generalize (H0 x0); clear H0; intros.
-  do 2 rewrite elements_iff in H0.
-  rewrite H0; clear H0.
-  intuition.
-  inversion_clear H0; auto.
-  Qed.
-
-  Lemma fold_3 :
-   forall s s' x (A : Set) (eqA : A -> A -> Prop)
-     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
-   compat_op E.eq eqA f ->
-   Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
-  Proof.
-  intros.
-  do 2 rewrite M.fold_1.
-  do 2 rewrite <- fold_left_rev_right.
-  change (f x (fold_right f i (rev (elements s)))) with 
-    (fold_right f i (rev (x::nil)++rev (elements s))).
-  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
-  rewrite <- distr_rev.
-  apply eqlistA_rev.
-  apply elements_eqlistA_max; auto.
-  Qed.
-
-  Lemma fold_4 :
-   forall s s' x (A : Set) (eqA : A -> A -> Prop)
-     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
-   compat_op E.eq eqA f ->
-   Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
-  Proof.
-  intros.
-  do 2 rewrite M.fold_1.
-  set (g:=fun (a : A) (e : elt) => f e a).
-  change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)).
-  unfold g.
-  do 2 rewrite <- fold_left_rev_right.
-  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
-  apply eqlistA_rev.
-  apply elements_eqlistA_min; auto.
-  Qed.
-
 End Properties.
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 960d82ce7..72084d034 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -17,16 +17,6 @@ Require Export DecidableType.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** Compatibility of a  boolean function with respect to an equality. *)
-Definition compat_bool (A:Type)(eqA: A->A->Prop)(f: A-> bool) :=
-  forall x y : A, eqA x y -> f x = f y.
-
-(** Compatibility of a predicate with respect to an equality. *)
-Definition compat_P (A:Type)(eqA: A->A->Prop)(P : A -> Prop) :=
-  forall x y : A, eqA x y -> P x -> P y.
-
-Hint Unfold compat_bool compat_P.
-
 (** * Non-dependent signature
 
     Signature [S] presents sets as purely informative programs 
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index 69bcf436e..d59a9a354 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -137,9 +137,9 @@ Ltac abstraction := match goal with
  | H1: ~lt ?x ?y, H2: ~eq ?y ?x |- _ => 
      generalize (le_neq H1 (neq_sym H2)); clear H1 H2; intro; abstraction
  (* Then, we generalize all interesting facts *)
- | H : lt ?x ?y |- _ => revert H; abstraction
- | H : ~lt ?x ?y |- _ => revert H; abstraction  
  | H : ~eq ?x ?y |- _ =>  revert H; abstraction
+ | H : ~lt ?x ?y |- _ => revert H; abstraction  
+ | H : lt ?x ?y |- _ => revert H; abstraction
  | H : eq ?x ?y |- _ =>  revert H; abstraction
  | _ => idtac
 end.
@@ -192,7 +192,7 @@ Ltac do_lt x y LT := match goal with
  | |- lt ?z x -> _ => let H := fresh "H" in 
      (intro H; generalize (lt_trans H LT); intro); do_lt x y LT
  | |- lt _ _ -> _ => intro; do_lt x y LT
- (* Ge *)
+ (* GE *)
  | |- ~lt y x -> _ => intros _; do_lt x y LT
  | |- ~lt x ?z -> _ => let H := fresh "H" in 
      (intro H; generalize (le_lt_trans H LT); intro); do_lt x y LT