Delete trailing whitespaces in all *.{v,ml*} files

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

1 files changed, 161 insertions, 161 deletions

diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index 81ed9a5726..bc0d758bd8 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -6,27 +6,27 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* Finite sets library.  
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
+(* Finite sets library.
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
 (* $Id$ *)
 
 (** * FSetFullAVL
-   
+
    This file contains some complements to [FSetAVL].
 
-   - Functor [AvlProofs] proves that trees of [FSetAVL] are not only 
+   - Functor [AvlProofs] proves that trees of [FSetAVL] are not only
    binary search trees, but moreover well-balanced ones. This is done
    by proving that all operations preserve the balancing.
 
-   - Functor [OcamlOps] contains variants of [union], [subset], 
+   - Functor [OcamlOps] contains variants of [union], [subset],
    [compare] and [equal] that are faithful to the original ocaml codes,
    while the versions in FSetAVL have been adapted to perform only
-   structural recursive code. 
-  
-   - Finally, we pack the previous elements in a [Make] functor 
+   structural recursive code.
+
+   - Finally, we pack the previous elements in a [Make] functor
    similar to the one of [FSetAVL], but richer.
 *)
 
@@ -54,7 +54,7 @@ Inductive avl : tree -> Prop :=
   | RBLeaf : avl Leaf
   | RBNode : forall x l r h, avl l -> avl r ->
       -(2) <= height l - height r <= 2 ->
-      h = max (height l) (height r) + 1 -> 
+      h = max (height l) (height r) + 1 ->
       avl (Node l x r h).
 
 (** * Automation and dedicated tactics *)
@@ -64,7 +64,7 @@ Hint Constructors avl.
 (** A tactic for cleaning hypothesis after use of functional induction. *)
 
 Ltac clearf :=
- match goal with 
+ match goal with
   | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
   | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
   | _ => idtac
@@ -77,25 +77,25 @@ Proof.
  induction s; simpl; intros; auto with zarith.
  inv avl; intuition; omega_max.
 Qed.
-Implicit Arguments height_non_negative. 
+Implicit Arguments height_non_negative.
 
 (** When [H:avl r], typing [avl_nn H] or [avl_nn r] adds [height r>=0] *)
 
-Ltac avl_nn_hyp H := 
+Ltac avl_nn_hyp H :=
      let nz := fresh "nz" in assert (nz := height_non_negative H).
 
-Ltac avl_nn h := 
-  let t := type of h in 
-  match type of t with 
+Ltac avl_nn h :=
+  let t := type of h in
+  match type of t with
    | Prop => avl_nn_hyp h
    | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
   end.
 
-(* Repeat the previous tactic. 
+(* Repeat the previous tactic.
    Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
 
 Ltac avl_nns :=
-  match goal with 
+  match goal with
      | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
      | _ => idtac
   end.
@@ -110,7 +110,7 @@ Qed.
 
 (** * Results about [avl] *)
 
-Lemma avl_node : 
+Lemma avl_node :
  forall x l r, avl l -> avl r ->
  -(2) <= height l - height r <= 2 ->
  avl (Node l x r (max (height l) (height r) + 1)).
@@ -123,7 +123,7 @@ Hint Resolve avl_node.
 (** empty *)
 
 Lemma empty_avl : avl empty.
-Proof. 
+Proof.
  auto.
 Qed.
 
@@ -137,15 +137,15 @@ Qed.
 
 (** create *)
 
-Lemma create_avl : 
- forall l x r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
+Lemma create_avl :
+ forall l x r, avl l -> avl r ->  -(2) <= height l - height r <= 2 ->
  avl (create l x r).
 Proof.
  unfold create; auto.
 Qed.
 
-Lemma create_height : 
- forall l x r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
+Lemma create_height :
+ forall l x r, avl l -> avl r ->  -(2) <= height l - height r <= 2 ->
  height (create l x r) = max (height l) (height r) + 1.
 Proof.
  unfold create; auto.
@@ -153,17 +153,17 @@ Qed.
 
 (** bal *)
 
-Lemma bal_avl : forall l x r, avl l -> avl r -> 
+Lemma bal_avl : forall l x r, avl l -> avl r ->
  -(3) <= height l - height r <= 3 -> avl (bal l x r).
 Proof.
  intros l x r; functional induction bal l x r; intros; clearf;
- inv avl; simpl in *; 
+ inv avl; simpl in *;
  match goal with |- avl (assert_false _ _ _) => avl_nns
   | _ => repeat apply create_avl; simpl in *; auto
  end; omega_max.
 Qed.
 
-Lemma bal_height_1 : forall l x r, avl l -> avl r -> 
+Lemma bal_height_1 : forall l x r, avl l -> avl r ->
  -(3) <= height l - height r <= 3 ->
  0 <= height (bal l x r) - max (height l) (height r) <= 1.
 Proof.
@@ -171,25 +171,25 @@ Proof.
  inv avl; avl_nns; simpl in *; omega_max.
 Qed.
 
-Lemma bal_height_2 : 
- forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> 
+Lemma bal_height_2 :
+ forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
  height (bal l x r) == max (height l) (height r) +1.
 Proof.
  intros l x r; functional induction bal l x r; intros; clearf;
  inv avl; simpl in *; omega_max.
 Qed.
 
-Ltac omega_bal := match goal with 
-  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] => 
-     generalize (bal_height_1 x H H') (bal_height_2 x H H'); 
+Ltac omega_bal := match goal with
+  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] =>
+     generalize (bal_height_1 x H H') (bal_height_2 x H H');
      omega_max
   end.
 
 (** add *)
 
-Lemma add_avl_1 :  forall s x, avl s -> 
+Lemma add_avl_1 :  forall s x, avl s ->
  avl (add x s) /\ 0 <= height (add x s) - height s <= 1.
-Proof. 
+Proof.
  intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *.
  intuition; try constructor; simpl; auto; try omega_max.
  (* LT *)
@@ -216,10 +216,10 @@ Hint Resolve add_avl.
 
 Lemma join_avl_1 : forall l x r, avl l -> avl r -> avl (join l x r) /\
  0<= height (join l x r) - max (height l) (height r) <= 1.
-Proof. 
+Proof.
  join_tac.
 
- split; simpl; auto. 
+ split; simpl; auto.
  destruct (add_avl_1 x H0).
  avl_nns; omega_max.
  set (l:=Node ll lx lr lh) in *.
@@ -269,8 +269,8 @@ Hint Resolve join_avl.
 
 (** remove_min *)
 
-Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> 
- avl (remove_min l x r)#1 /\ 
+Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) ->
+ avl (remove_min l x r)#1 /\
  0 <= height (Node l x r h) - height (remove_min l x r)#1 <= 1.
 Proof.
  intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
@@ -278,25 +278,25 @@ Proof.
  avl_nns; omega_max.
  inversion_clear H.
  rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto.
- split; simpl in *. 
+ split; simpl in *.
  apply bal_avl; auto; omega_max.
  omega_bal.
 Qed.
 
-Lemma remove_min_avl : forall l x r h, avl (Node l x r h) -> 
-    avl (remove_min l x r)#1. 
+Lemma remove_min_avl : forall l x r h, avl (Node l x r h) ->
+    avl (remove_min l x r)#1.
 Proof.
  intros; destruct (remove_min_avl_1 H); auto.
 Qed.
 
 (** merge *)
 
-Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 -> 
- -(2) <= height s1 - height s2 <= 2 -> 
- avl (merge s1 s2) /\ 
+Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 ->
+ -(2) <= height s1 - height s2 <= 2 ->
+ avl (merge s1 s2) /\
  0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
 Proof.
- intros s1 s2; functional induction (merge s1 s2); intros; 
+ intros s1 s2; functional induction (merge s1 s2); intros;
  try factornode _x _x0 _x1 _x2 as s1.
  simpl; split; auto; avl_nns; omega_max.
  simpl; split; auto; avl_nns; simpl in *; omega_max.
@@ -308,16 +308,16 @@ Proof.
  simpl in *; omega_bal.
 Qed.
 
-Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 -> 
+Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 ->
   -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2).
-Proof. 
+Proof.
  intros; destruct (merge_avl_1 H H0 H1); auto.
 Qed.
 
 
 (** remove *)
 
-Lemma remove_avl_1 : forall s x, avl s -> 
+Lemma remove_avl_1 : forall s x, avl s ->
  avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
 Proof.
  intros s x; functional induction (remove x s); intros.
@@ -325,25 +325,25 @@ Proof.
  (* LT *)
  inv avl.
  destruct (IHt H0).
- split. 
+ split.
  apply bal_avl; auto.
  omega_max.
  omega_bal.
  (* EQ *)
- inv avl. 
+ inv avl.
  generalize (merge_avl_1 H0 H1 H2).
  intuition omega_max.
  (* GT *)
  inv avl.
  destruct (IHt H1).
- split. 
+ split.
  apply bal_avl; auto.
  omega_max.
  omega_bal.
 Qed.
 
 Lemma remove_avl : forall s x, avl s -> avl (remove x s).
-Proof. 
+Proof.
  intros; destruct (remove_avl_1 x H); auto.
 Qed.
 Hint Resolve remove_avl.
@@ -360,9 +360,9 @@ Hint Resolve concat_avl.
 
 (** split *)
 
-Lemma split_avl : forall s x, avl s -> 
+Lemma split_avl : forall s x, avl s ->
   avl (split x s)#l /\ avl (split x s)#r.
-Proof. 
+Proof.
  intros s x; functional induction (split x s); simpl; auto.
  rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
  simpl; inversion_clear 1; auto.
@@ -371,19 +371,19 @@ Qed.
 
 (** inter *)
 
-Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2). 
+Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2).
 Proof.
  intros s1 s2; functional induction inter s1 s2; auto; intros A1 A2;
- generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1; 
+ generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
  inv avl; auto.
 Qed.
 
 (** diff *)
 
-Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2). 
-Proof. 
+Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2).
+Proof.
  intros s1 s2; functional induction diff s1 s2; auto; intros A1 A2;
- generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1; 
+ generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
  inv avl; auto.
 Qed.
 
@@ -392,30 +392,30 @@ Qed.
 Lemma union_avl : forall s1 s2, avl s1 -> avl s2 -> avl (union s1 s2).
 Proof.
  intros s1 s2; functional induction union s1 s2; auto; intros A1 A2;
- generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1; 
+ generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1;
  inv avl; auto.
 Qed.
 
 (** filter *)
 
-Lemma filter_acc_avl : forall f s acc, avl s -> avl acc -> 
+Lemma filter_acc_avl : forall f s acc, avl s -> avl acc ->
  avl (filter_acc f acc s).
 Proof.
  induction s; simpl; auto.
  intros.
  inv avl.
  destruct (f t); auto.
-Qed. 
+Qed.
 Hint Resolve filter_acc_avl.
 
-Lemma filter_avl : forall f s, avl s -> avl (filter f s). 
+Lemma filter_avl : forall f s, avl s -> avl (filter f s).
 Proof.
  unfold filter; intros; apply filter_acc_avl; auto.
 Qed.
 
 (** partition *)
 
-Lemma partition_acc_avl_1 : forall f s acc, avl s -> 
+Lemma partition_acc_avl_1 : forall f s acc, avl s ->
  avl acc#1 -> avl (partition_acc f acc s)#1.
 Proof.
  induction s; simpl; auto.
@@ -427,7 +427,7 @@ Proof.
  destruct (f t); simpl; auto.
 Qed.
 
-Lemma partition_acc_avl_2 : forall f s acc, avl s -> 
+Lemma partition_acc_avl_2 : forall f s acc, avl s ->
  avl acc#2 -> avl (partition_acc f acc s)#2.
 Proof.
  induction s; simpl; auto.
@@ -437,14 +437,14 @@ Proof.
  apply IHs2; auto.
  apply IHs1; auto.
  destruct (f t); simpl; auto.
-Qed. 
+Qed.
 
-Lemma partition_avl_1 : forall f s, avl s -> avl (partition f s)#1. 
+Lemma partition_avl_1 : forall f s, avl s -> avl (partition f s)#1.
 Proof.
  unfold partition; intros; apply partition_acc_avl_1; auto.
 Qed.
 
-Lemma partition_avl_2 : forall f s, avl s -> avl (partition f s)#2. 
+Lemma partition_avl_2 : forall f s, avl s -> avl (partition f s)#2.
 Proof.
  unfold partition; intros; apply partition_acc_avl_2; auto.
 Qed.
@@ -462,29 +462,29 @@ Open Local Scope nat_scope.
 
 (** Properties of cardinal *)
 
-Lemma bal_cardinal : forall l x r, 
+Lemma bal_cardinal : forall l x r,
  cardinal (bal l x r) = S (cardinal l + cardinal r).
 Proof.
  intros l x r; functional induction bal l x r; intros; clearf;
  simpl; auto with arith; romega with *.
 Qed.
 
-Lemma add_cardinal : forall x s, 
+Lemma add_cardinal : forall x s,
  cardinal (add x s) <= S (cardinal s).
 Proof.
- intros; functional induction add x s; simpl; auto with arith; 
+ intros; functional induction add x s; simpl; auto with arith;
  rewrite bal_cardinal; romega with *.
 Qed.
 
-Lemma join_cardinal : forall l x r, 
+Lemma join_cardinal : forall l x r,
  cardinal (join l x r) <= S (cardinal l + cardinal r).
 Proof.
  join_tac; auto with arith.
  simpl; apply add_cardinal.
  simpl; destruct X.compare; simpl; auto with arith.
- generalize (bal_cardinal (add x ll) lx lr) (add_cardinal x ll); 
+ generalize (bal_cardinal (add x ll) lx lr) (add_cardinal x ll);
   romega with *.
- generalize (bal_cardinal ll lx (add x lr)) (add_cardinal x lr); 
+ generalize (bal_cardinal ll lx (add x lr)) (add_cardinal x lr);
   romega with *.
  generalize (bal_cardinal ll lx (join lr x (Node rl rx rr rh)))
   (Hlr x (Node rl rx rr rh)); simpl; romega with *.
@@ -492,7 +492,7 @@ Proof.
  romega with *.
 Qed.
 
-Lemma split_cardinal_1 : forall x s, 
+Lemma split_cardinal_1 : forall x s,
  (cardinal (split x s)#l <= cardinal s)%nat.
 Proof.
  intros x s; functional induction split x s; simpl; auto.
@@ -503,7 +503,7 @@ Proof.
  generalize (@join_cardinal l y rl); romega with *.
 Qed.
 
-Lemma split_cardinal_2 : forall x s, 
+Lemma split_cardinal_2 : forall x s,
  (cardinal (split x s)#r <= cardinal s)%nat.
 Proof.
  intros x s; functional induction split x s; simpl; auto.
@@ -517,26 +517,26 @@ Qed.
 
 Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat.
 
-Ltac ocaml_union_tac := 
+Ltac ocaml_union_tac :=
  intros; unfold cardinal2; simpl fst in *; simpl snd in *;
- match goal with H: split ?x ?s = _ |- _ => 
-  generalize (split_cardinal_1 x s) (split_cardinal_2 x s); 
+ match goal with H: split ?x ?s = _ |- _ =>
+  generalize (split_cardinal_1 x s) (split_cardinal_2 x s);
   rewrite H; simpl; romega with *
  end.
 
 Function ocaml_union (s : t * t) { measure cardinal2 s } : t  :=
- match s with 
+ match s with
   | (Leaf, Leaf) => s#2
   | (Leaf, Node _ _ _ _) => s#2
   | (Node _ _ _ _, Leaf) => s#1
-  | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => 
+  | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) =>
         if ge_lt_dec h1 h2 then
           if eq_dec h2 1%I then add x2 s#1 else
-          let (l2',_,r2') := split x1 s#2 in 
+          let (l2',_,r2') := split x1 s#2 in
              join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2'))
         else
           if eq_dec h1 1%I then add x1 s#2 else
-          let (l1',_,r1') := split x2 s#1 in 
+          let (l1',_,r1') := split x2 s#1 in
              join (ocaml_union (l1',l2)) x2 (ocaml_union (r1',r2))
  end.
 Proof.
@@ -546,11 +546,11 @@ abstract ocaml_union_tac.
 abstract ocaml_union_tac.
 Defined.
 
-Lemma ocaml_union_in : forall s y, 
+Lemma ocaml_union_in : forall s y,
  bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 ->
  (In y (ocaml_union s) <-> In y s#1 \/ In y s#2).
 Proof.
- intros s; functional induction ocaml_union s; intros y B1 A1 B2 A2; 
+ intros s; functional induction ocaml_union s; intros y B1 A1 B2 A2;
   simpl fst in *; simpl snd in *; try clear e0 e1.
  intuition_in.
  intuition_in.
@@ -575,7 +575,7 @@ Proof.
  rewrite (height_0 H4); [ | avl_nn r1; omega_max].
  rewrite add_in; auto; intuition_in.
  (* join (union (l1',l2)) x1 (union (r1',r2)) *)
- generalize 
+ generalize
   (split_avl x2 A1) (split_bst x2 B1)
   (split_in_1 x2 y B1) (split_in_2 x2 y B1).
  rewrite e2; simpl.
@@ -589,7 +589,7 @@ Lemma ocaml_union_bst : forall s,
  bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (ocaml_union s).
 Proof.
  intros s; functional induction ocaml_union s; intros B1 A1 B2 A2;
-  simpl fst in *; simpl snd in *; try clear e0 e1; 
+  simpl fst in *; simpl snd in *; try clear e0 e1;
   try apply add_bst; auto.
  (* join (union (l1,l2')) x1 (union (r1,r2')) *)
  clear _x _x0; factornode l2 x2 r2 h2 as s2.
@@ -613,10 +613,10 @@ Proof.
  intro y; rewrite ocaml_union_in, H4; intuition_in.
 Qed.
 
-Lemma ocaml_union_avl : forall s, 
+Lemma ocaml_union_avl : forall s,
  avl s#1 -> avl s#2 -> avl (ocaml_union s).
 Proof.
- intros s; functional induction ocaml_union s; 
+ intros s; functional induction ocaml_union s;
   simpl fst in *; simpl snd in *; auto.
  intros A1 A2; generalize (split_avl x1 A2); rewrite e2; simpl.
  inv avl; destruct 1; auto.
@@ -654,7 +654,7 @@ Proof.
  intros; unfold cardinal2; simpl; abstract romega with *.
 Defined.
 
-Lemma ocaml_subset_12 : forall s, 
+Lemma ocaml_subset_12 : forall s,
  bst s#1 -> bst s#2 ->
  (ocaml_subset s = true <-> Subset s#1 s#2).
 Proof.
@@ -685,7 +685,7 @@ Proof.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 Qed.
 
-Lemma ocaml_subset_alt : forall s, bst s#1 -> bst s#2 -> 
+Lemma ocaml_subset_alt : forall s, bst s#1 -> bst s#2 ->
  ocaml_subset s = subset s#1 s#2.
 Proof.
  intros.
@@ -704,7 +704,7 @@ Fixpoint cardinal_e e := match e with
   | More _ s r => S (cardinal s + cardinal_e r)
  end.
 
-Lemma cons_cardinal_e : forall s e, 
+Lemma cons_cardinal_e : forall s e,
  cardinal_e (cons s e) = cardinal s + cardinal_e e.
 Proof.
  induction s; simpl; intros; auto.
@@ -713,32 +713,32 @@ Qed.
 
 Definition cardinal_e_2 e := cardinal_e e#1 + cardinal_e e#2.
 
-Function ocaml_compare_aux 
- (e:enumeration*enumeration) { measure cardinal_e_2 e } : comparison := 
- match e with 
+Function ocaml_compare_aux
+ (e:enumeration*enumeration) { measure cardinal_e_2 e } : comparison :=
+ match e with
  | (End,End) => Eq
- | (End,More _ _ _) => Lt 
- | (More _ _ _, End) => Gt 
- | (More x1 r1 e1, More x2 r2 e2) => 
-       match X.compare x1 x2 with 
+ | (End,More _ _ _) => Lt
+ | (More _ _ _, End) => Gt
+ | (More x1 r1 e1, More x2 r2 e2) =>
+       match X.compare x1 x2 with
         | EQ _ => ocaml_compare_aux (cons r1 e1, cons r2 e2)
-        | LT _ => Lt 
-        | GT _ => Gt 
+        | LT _ => Lt
+        | GT _ => Gt
        end
  end.
 
 Proof.
-intros; unfold cardinal_e_2; simpl; 
+intros; unfold cardinal_e_2; simpl;
 abstract (do 2 rewrite cons_cardinal_e; romega with *).
 Defined.
 
-Definition ocaml_compare s1 s2 := 
+Definition ocaml_compare s1 s2 :=
  ocaml_compare_aux (cons s1 End, cons s2 End).
 
-Lemma ocaml_compare_aux_Cmp : forall e, 
+Lemma ocaml_compare_aux_Cmp : forall e,
  Cmp (ocaml_compare_aux e) (flatten_e e#1) (flatten_e e#2).
 Proof.
- intros e; functional induction ocaml_compare_aux e; simpl; intros; 
+ intros e; functional induction ocaml_compare_aux e; simpl; intros;
   auto; try discriminate.
  apply L.eq_refl.
  simpl in *.
@@ -756,11 +756,11 @@ Proof.
  apply (@ocaml_compare_aux_Cmp (cons s1 End, cons s2 End)).
 Qed.
 
-Lemma ocaml_compare_alt : forall s1 s2, bst s1 -> bst s2 -> 
+Lemma ocaml_compare_alt : forall s1 s2, bst s1 -> bst s2 ->
  ocaml_compare s1 s2 = compare s1 s2.
 Proof.
  intros s1 s2 B1 B2.
- generalize (ocaml_compare_Cmp s1 s2)(compare_Cmp s1 s2). 
+ generalize (ocaml_compare_Cmp s1 s2)(compare_Cmp s1 s2).
  unfold Cmp.
  destruct ocaml_compare; destruct compare; auto; intros; elimtype False.
  elim (lt_not_eq B1 B2 H0); auto.
@@ -781,13 +781,13 @@ Qed.
 
 (** * Equality test *)
 
-Definition ocaml_equal s1 s2 : bool := 
- match ocaml_compare s1 s2 with 
+Definition ocaml_equal s1 s2 : bool :=
+ match ocaml_compare s1 s2 with
   | Eq => true
-  | _ => false 
+  | _ => false
  end.
 
-Lemma ocaml_equal_1 : forall s1 s2, bst s1 -> bst s2 ->  
+Lemma ocaml_equal_1 : forall s1 s2, bst s1 -> bst s2 ->
  Equal s1 s2 -> ocaml_equal s1 s2 = true.
 Proof.
 unfold ocaml_equal; intros s1 s2 B1 B2 E.
@@ -801,11 +801,11 @@ Lemma ocaml_equal_2 : forall s1 s2,
  ocaml_equal s1 s2 = true -> Equal s1 s2.
 Proof.
 unfold ocaml_equal; intros s1 s2 E.
-generalize (ocaml_compare_Cmp s1 s2); 
+generalize (ocaml_compare_Cmp s1 s2);
  destruct ocaml_compare; auto; discriminate.
 Qed.
 
-Lemma ocaml_equal_alt : forall s1 s2, bst s1 -> bst s2 -> 
+Lemma ocaml_equal_alt : forall s1 s2, bst s1 -> bst s2 ->
  ocaml_equal s1 s2 = equal s1 s2.
 Proof.
 intros; unfold ocaml_equal, equal; rewrite ocaml_compare_alt; auto.
@@ -817,14 +817,14 @@ End OcamlOps.
 
 (** * Encapsulation
 
-   We can implement [S] with balanced binary search trees. 
+   We can implement [S] with balanced binary search trees.
    When compared to [FSetAVL], we maintain here two invariants
    (bst and avl) instead of only bst, which is enough for fulfilling
    the FSet interface.
 
-   This encapsulation propose the non-structural variants 
+   This encapsulation propose the non-structural variants
    [ocaml_union], [ocaml_subset], [ocaml_compare], [ocaml_equal].
-*) 
+*)
 
 Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
@@ -837,61 +837,61 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Record bbst := Bbst {this :> Raw.t; is_bst : bst this; is_avl : avl this}.
  Definition t := bbst.
  Definition elt := E.t.
- 
+
  Definition In (x : elt) (s : t) : Prop := In x s.
  Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
  Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
  Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) (s:t) : Prop := forall x, In x s -> P x.
  Definition Exists (P : elt -> Prop) (s:t) : Prop := exists x, In x s /\ P x.
-  
- Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s. 
+
+ Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s.
  Proof. intro s; exact (@In_1 s). Qed.
- 
+
  Definition mem (x:elt)(s:t) : bool := mem x s.
 
  Definition empty : t := Bbst empty_bst empty_avl.
  Definition is_empty (s:t) : bool := is_empty s.
- Definition singleton (x:elt) : t := 
+ Definition singleton (x:elt) : t :=
    Bbst (singleton_bst x) (singleton_avl x).
- Definition add (x:elt)(s:t) : t := 
-   Bbst (add_bst x (is_bst s)) (add_avl x (is_avl s)). 
- Definition remove (x:elt)(s:t) : t := 
+ Definition add (x:elt)(s:t) : t :=
+   Bbst (add_bst x (is_bst s)) (add_avl x (is_avl s)).
+ Definition remove (x:elt)(s:t) : t :=
    Bbst (remove_bst x (is_bst s)) (remove_avl x (is_avl s)).
- Definition inter (s s':t) : t := 
+ Definition inter (s s':t) : t :=
    Bbst (inter_bst (is_bst s) (is_bst s'))
         (inter_avl (is_avl s) (is_avl s')).
  Definition union (s s':t) : t :=
    Bbst (union_bst (is_bst s) (is_bst s'))
         (union_avl (is_avl s) (is_avl s')).
  Definition ocaml_union (s s':t) : t :=
-   Bbst (@ocaml_union_bst (s.(this),s'.(this)) 
+   Bbst (@ocaml_union_bst (s.(this),s'.(this))
           (is_bst s) (is_avl s) (is_bst s') (is_avl s'))
         (@ocaml_union_avl (s.(this),s'.(this)) (is_avl s) (is_avl s')).
- Definition diff (s s':t) : t := 
+ Definition diff (s s':t) : t :=
    Bbst (diff_bst (is_bst s) (is_bst s'))
         (diff_avl (is_avl s) (is_avl s')).
  Definition elements (s:t) : list elt := elements s.
  Definition min_elt (s:t) : option elt := min_elt s.
  Definition max_elt (s:t) : option elt := max_elt s.
  Definition choose (s:t) : option elt := choose s.
- Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := fold f s. 
+ Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := fold f s.
  Definition cardinal (s:t) : nat := cardinal s.
- Definition filter (f : elt -> bool) (s:t) : t := 
+ Definition filter (f : elt -> bool) (s:t) : t :=
    Bbst (filter_bst f (is_bst s)) (filter_avl f (is_avl s)).
  Definition for_all (f : elt -> bool) (s:t) : bool := for_all f s.
  Definition exists_ (f : elt -> bool) (s:t) : bool := exists_ f s.
  Definition partition (f : elt -> bool) (s:t) : t * t :=
    let p := partition f s in
-   (@Bbst (fst p) (partition_bst_1 f (is_bst s)) 
-                 (partition_avl_1 f (is_avl s)), 
+   (@Bbst (fst p) (partition_bst_1 f (is_bst s))
+                 (partition_avl_1 f (is_avl s)),
     @Bbst (snd p) (partition_bst_2 f (is_bst s))
                  (partition_avl_2 f (is_avl s))).
 
  Definition equal (s s':t) : bool := equal s s'.
  Definition ocaml_equal (s s':t) : bool := ocaml_equal s s'.
  Definition subset (s s':t) : bool := subset s s'.
- Definition ocaml_subset (s s':t) : bool := 
+ Definition ocaml_subset (s s':t) : bool :=
   ocaml_subset (s.(this),s'.(this)).
 
  Definition eq (s s':t) : Prop := Equal s s'.
@@ -922,13 +922,13 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Defined.
 
  (* specs *)
- Section Specs. 
- Variable s s' s'': t. 
+ Section Specs.
+ Variable s s' s'': t.
  Variable x y : elt.
 
  Hint Resolve is_bst is_avl.
- 
- Lemma mem_1 : In x s -> mem x s = true. 
+
+ Lemma mem_1 : In x s -> mem x s = true.
  Proof. exact (mem_1 (is_bst s)). Qed.
  Lemma mem_2 : mem x s = true -> In x s.
  Proof. exact (@mem_2 s x). Qed.
@@ -939,15 +939,15 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@equal_2 s s'). Qed.
 
  Lemma ocaml_equal_alt : ocaml_equal s s' = equal s s'.
- Proof. 
+ Proof.
   destruct s; destruct s'; unfold ocaml_equal, equal; simpl.
   apply ocaml_equal_alt; auto.
  Qed.
- 
+
  Lemma ocaml_equal_1 : Equal s s' -> ocaml_equal s s' = true.
  Proof. exact (ocaml_equal_1 (is_bst s) (is_bst s')). Qed.
  Lemma ocaml_equal_2 : ocaml_equal s s' = true -> Equal s s'.
- Proof. exact (@ocaml_equal_2 s s'). Qed. 
+ Proof. exact (@ocaml_equal_2 s s'). Qed.
 
  Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.
 
@@ -957,7 +957,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. wrap subset subset_12. Qed.
 
  Lemma ocaml_subset_alt : ocaml_subset s s' = subset s s'.
- Proof. 
+ Proof.
   destruct s; destruct s'; unfold ocaml_subset, subset; simpl.
   rewrite ocaml_subset_alt; auto.
  Qed.
@@ -972,14 +972,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Lemma is_empty_1 : Empty s -> is_empty s = true.
  Proof. exact (@is_empty_1 s). Qed.
- Lemma is_empty_2 : is_empty s = true -> Empty s. 
+ Lemma is_empty_2 : is_empty s = true -> Empty s.
  Proof. exact (@is_empty_2 s). Qed.
- 
+
  Lemma add_1 : E.eq x y -> In y (add x s).
  Proof. wrap add add_in. Qed.
  Lemma add_2 : In y s -> In y (add x s).
  Proof. wrap add add_in. Qed.
- Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
+ Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
  Proof. wrap add add_in. elim H; auto. Qed.
 
  Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
@@ -989,20 +989,20 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma remove_3 : In y (remove x s) -> In y s.
  Proof. wrap remove remove_in. Qed.
 
- Lemma singleton_1 : In y (singleton x) -> E.eq x y. 
+ Lemma singleton_1 : In y (singleton x) -> E.eq x y.
  Proof. exact (@singleton_1 x y). Qed.
- Lemma singleton_2 : E.eq x y -> In y (singleton x). 
+ Lemma singleton_2 : E.eq x y -> In y (singleton x).
  Proof. exact (@singleton_2 x y). Qed.
 
  Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
  Proof. wrap union union_in. Qed.
- Lemma union_2 : In x s -> In x (union s s'). 
+ Lemma union_2 : In x s -> In x (union s s').
  Proof. wrap union union_in. Qed.
  Lemma union_3 : In x s' -> In x (union s s').
  Proof. wrap union union_in. Qed.
 
  Lemma ocaml_union_alt : Equal (ocaml_union s s') (union s s').
- Proof. 
+ Proof.
   unfold ocaml_union, union, Equal, In.
   destruct s as (s0,b,a); destruct s' as (s0',b',a'); simpl.
   exact (@ocaml_union_alt (s0,s0') b a b' a').
@@ -1021,32 +1021,32 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. wrap inter inter_in. Qed.
  Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
  Proof. wrap inter inter_in. Qed.
- 
- Lemma diff_1 : In x (diff s s') -> In x s. 
+
+ Lemma diff_1 : In x (diff s s') -> In x s.
  Proof. wrap diff diff_in. Qed.
  Lemma diff_2 : In x (diff s s') -> ~ In x s'.
  Proof. wrap diff diff_in. Qed.
  Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
  Proof. wrap diff diff_in. Qed.
- 
+
  Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
- Proof. 
+ Proof.
  unfold fold, elements; intros; apply fold_1; auto.
  Qed.
 
  Lemma cardinal_1 : cardinal s = length (elements s).
- Proof. 
+ Proof.
  unfold cardinal, elements; intros; apply elements_cardinal; auto.
  Qed.
 
  Section Filter.
  Variable f : elt -> bool.
 
- Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
+ Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
+ Proof. intro. wrap filter filter_in. Qed.
+ Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
  Proof. intro. wrap filter filter_in. Qed.
- Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
- Proof. intro. wrap filter filter_in. Qed. 
  Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
  Proof. intro. wrap filter filter_in. Qed.
 
@@ -1060,14 +1060,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
  Proof. exact (@exists_2 f s). Qed.
 
- Lemma partition_1 : compat_bool E.eq f -> 
+ Lemma partition_1 : compat_bool E.eq f ->
   Equal (fst (partition f s)) (filter f s).
  Proof.
  unfold partition, filter, Equal, In; simpl ;intros H a.
  rewrite partition_in_1, filter_in; intuition.
  Qed.
 
- Lemma partition_2 : compat_bool E.eq f -> 
+ Lemma partition_2 : compat_bool E.eq f ->
   Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
  Proof.
  unfold partition, filter, Equal, In; simpl ;intros H a.
@@ -1089,14 +1089,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma elements_3w : NoDupA E.eq (elements s).
  Proof. exact (elements_nodup (is_bst s)). Qed.
 
- Lemma min_elt_1 : min_elt s = Some x -> In x s. 
+ Lemma min_elt_1 : min_elt s = Some x -> In x s.
  Proof. exact (@min_elt_1 s x). Qed.
  Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
  Proof. exact (@min_elt_2 s x y (is_bst s)). Qed.
  Lemma min_elt_3 : min_elt s = None -> Empty s.
  Proof. exact (@min_elt_3 s). Qed.
 
- Lemma max_elt_1 : max_elt s = Some x -> In x s. 
+ Lemma max_elt_1 : max_elt s = Some x -> In x s.
  Proof. exact (@max_elt_1 s x). Qed.
  Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
  Proof. exact (@max_elt_2 s x y (is_bst s)). Qed.
@@ -1107,17 +1107,17 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@choose_1 s x). Qed.
  Lemma choose_2 : choose s = None -> Empty s.
  Proof. exact (@choose_2 s). Qed.
- Lemma choose_3 : choose s = Some x -> choose s' = Some y -> 
+ Lemma choose_3 : choose s = Some x -> choose s' = Some y ->
   Equal s s' -> E.eq x y.
  Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed.
 
- Lemma eq_refl : eq s s. 
+ Lemma eq_refl : eq s s.
  Proof. exact (eq_refl s). Qed.
  Lemma eq_sym : eq s s' -> eq s' s.
  Proof. exact (@eq_sym s s'). Qed.
  Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
  Proof. exact (@eq_trans s s' s''). Qed.
-  
+
  Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
  Proof. exact (@lt_trans s s' s''). Qed.
  Lemma lt_not_eq : lt s s' -> ~eq s s'.