Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)

 * FSetAVL is greatly lightened : modulo a minor change in bal, formal
   proofs of avl invariant is not needed for building a functor
   implementing FSetInterface.S (even if this invariant is still true)

 * Non-structural functions (union, subset, compare, equal) are 
   transformed into efficient structural versions

 * Both proofs of avl preservation and non-structural functions are 
   moved to a new file FSetFullAVL, that can be ignored by the average
   user.

Same for FMapAVL (still work in progress...)



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

4 files changed, 1864 insertions, 1675 deletions

diff --git a/Makefile.common b/Makefile.common
index 17dd694d8c..6fe2188633 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -616,7 +616,8 @@ FSETSBASEVO:=\
 FSETS_basic:=
 
 FSETS_all:=\
- theories/FSets/FMapAVL.vo           theories/FSets/FSetAVL.vo \
+ theories/FSets/FSetAVL.vo           theories/FSets/FSetFullAVL.vo \
+ theories/FSets/FMapAVL.vo           
 
 FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS))
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f3a20eb1c0..556d6225ac 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -105,21 +105,6 @@ Inductive bst : tree -> Prop :=
   | BSNode : forall x e l r h, bst l -> bst r -> 
      lt_tree x l -> gt_tree x r -> bst (Node l x e r h).
 
-(** * AVL trees *)
-
-(** [avl s] : [s] is a properly balanced AVL tree,
-    i.e. for any node the heights of the two children
-    differ by at most 2 *)
-
-Inductive avl : tree -> Prop :=
-  | RBLeaf : avl Leaf
-  | RBNode : forall x e l r h, 
-      avl l ->
-      avl r ->
-      -(2) <= height l - height r <= 2 ->
-      h = max (height l) (height r) + 1 -> 
-      avl (Node l x e r h).
-
 (* We should end this section before the big proofs that follows, 
     otherwise the discharge takes a lot of time. *)
 End Elt. 
@@ -130,7 +115,7 @@ Notation t := tree.
 
 (** * Automation and dedicated tactics. *)
 
-Hint Constructors tree MapsTo In bst avl.
+Hint Constructors tree MapsTo In bst.
 Hint Unfold lt_tree gt_tree.
 
 (** A tactic for cleaning hypothesis after use of functional induction. *)
@@ -158,16 +143,6 @@ Ltac inv f :=
      | _ => idtac
   end.
 
-(** Same, but with a backup of the original hypothesis. *)
-
-Ltac safe_inv f := match goal with 
-  | H:f (Node _ _ _ _ _) |- _ => 
-        generalize H; inversion_clear H; safe_inv f
-  | H:f _ (Node _ _ _ _ _) |- _ => 
-        generalize H; inversion_clear H; safe_inv f
-  | _ => intros 
- end.
-
 Ltac inv_all f := 
   match goal with 
    | H: f _ |- _ => inversion_clear H; inv f
@@ -187,39 +162,8 @@ end.
 
 Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo).
 
-(** Tactics about [avl] *)
-
-Lemma height_non_negative : forall elt (s : t elt), avl s -> 
- height s >= 0.
-Proof.
- induction s; simpl; intros; auto with zarith.
- inv avl; intuition; omega_max.
-Qed.
-
-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 
-   | Prop => avl_nn_hyp h
-   | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
-  end.
-
-(* Repeat the previous tactic. 
-   Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
-
-Ltac avl_nns :=
-  match goal with 
-     | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
-     | _ => idtac
-  end.
-
-
 
-
-(** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [avl], 
-    [height] *)
+(** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [height] *)
 
 (** Facts about [MapsTo] and [In]. *)
 
@@ -254,6 +198,13 @@ Proof.
  intros elt m x y; induction m; simpl; intuition_in; eauto.
 Qed.
 
+Lemma In_node_iff : 
+ forall elt (l:t elt) x e r h y, 
+  In y (Node l x e r h) <-> In y l \/ X.eq y x \/ In y r.
+Proof.
+ intuition_in.
+Qed.
+
 (** Results about [lt_tree] and [gt_tree] *)
 
 Lemma lt_leaf : forall elt x, lt_tree x (Leaf elt).
@@ -332,35 +283,6 @@ Qed.
 
 Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 
-(** Results about [avl] *)
-
-Lemma avl_node : forall elt x e (l:t elt) r, avl l -> avl r ->
- -(2) <= height l - height r <= 2 ->
- avl (Node l x e r (max (height l) (height r) + 1)).
-Proof.
-  intros; auto.
-Qed.
-Hint Resolve avl_node.
-
-(** Results about [height] *)
-
-Lemma height_0 : forall elt (l:t elt), avl l -> height l = 0 -> 
- l = @Leaf _.
-Proof.
- destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; elimtype False; omega_max.
-Qed.
-
-
-
-(** trick for emulating [assert false] in Coq *)
-
-Definition assert_false := Leaf.
-Lemma assert_false_cardinal : forall elt, 
- cardinal (assert_false elt) = 0%nat.
-Proof. simpl; auto. Qed.
-Opaque assert_false.
-
 
 
 (** * Helper functions *)
@@ -379,20 +301,6 @@ Proof.
 Qed.
 Hint Resolve create_bst.
 
-Lemma create_avl : 
- forall elt (l:t elt) x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
- avl (create l x e r).
-Proof.
- unfold create; auto.
-Qed.
-
-Lemma create_height : 
- forall elt (l:t elt) x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
- height (create l x e r) = max (height l) (height r) + 1.
-Proof.
- unfold create; intros; auto.
-Qed.
-
 Lemma create_in : 
  forall elt (l:t elt) x e r y,  In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
@@ -403,18 +311,20 @@ Qed.
 (** [bal l x e r] acts as [create], but performs one step of
     rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *)
 
+Definition assert_false := create.
+
 Function bal (elt:Type)(l: t elt)(x:key)(e:elt)(r:t elt) : t elt := 
   let hl := height l in 
   let hr := height r in
   if gt_le_dec hl (hr+2) then 
     match l with 
-     | Leaf => assert_false _
+     | Leaf => assert_false l x e r
      | Node ll lx le lr _ => 
        if ge_lt_dec (height ll) (height lr) then 
          create ll lx le (create lr x e r)
        else 
          match lr with 
-          | Leaf => assert_false _
+          | Leaf => assert_false l x e r
           | Node lrl lrx lre lrr _ => 
               create (create ll lx le lrl) lrx lre (create lrr x e r)
          end
@@ -422,13 +332,13 @@ Function bal (elt:Type)(l: t elt)(x:key)(e:elt)(r:t elt) : t elt :=
   else 
     if gt_le_dec hr (hl+2) then 
       match r with
-       | Leaf => assert_false _
+       | Leaf => assert_false l x e r
        | Node rl rx re rr _ =>
          if ge_lt_dec (height rr) (height rl) then 
             create (create l x e rl) rx re rr
          else 
            match rl with
-            | Leaf => assert_false _
+            | Leaf => assert_false l x e r
             | Node rll rlx rle rlr _ => 
                 create (create l x e rll) rlx rle (create rlr rx re rr) 
            end
@@ -445,53 +355,20 @@ Proof.
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
 Qed.
 
-Lemma bal_avl : forall elt (l:t elt) x e r, avl l -> avl r -> 
- -(3) <= height l - height r <= 3 -> avl (bal l x e r).
-Proof.
- intros elt l x e r; functional induction (bal l x e r); intros; clearf;
- try constructor; inv avl; repeat apply create_avl; simpl in *; auto; 
- omega_max.
-Qed.
-
-Lemma bal_height_1 : forall elt (l:t elt) x e r, avl l -> avl r -> 
- -(3) <= height l - height r <= 3 ->
- 0 <= height (bal l x e r) - max (height l) (height r) <= 1.
+Lemma bal_in : forall elt (l:t elt) x e r y,
+ In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
  intros elt l x e r; functional induction (bal l x e r); intros; clearf;
- inv avl; avl_nns; simpl in *; omega_max.
+ rewrite !create_in; intuition_in.
 Qed.
 
-Lemma bal_height_2 : 
- forall elt (l:t elt) x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> 
- height (bal l x e r) == max (height l) (height r) +1.
+Lemma bal_mapsto : forall elt (l:t elt) x e r y e',
+ MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r).
 Proof.
  intros elt l x e r; functional induction (bal l x e r); intros; clearf;
- inv avl; avl_nns; simpl in *; omega_max.
+ unfold assert_false, create; intuition_in.
 Qed.
 
-Lemma bal_in : forall elt (l:t elt) x e r y, avl l -> avl r -> 
- (In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r).
-Proof.
- intros elt l x e r; functional induction (bal l x e r); intros; clearf;
- inv avl; solve [repeat rewrite create_in; intuition_in
-                |inv avl; avl_nns; simpl in *; omega_max ].
-Qed.
-
-Lemma bal_mapsto : forall elt (l:t elt) x e r y e', avl l -> avl r -> 
- (MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r)).
-Proof.
- intros elt l x e r; functional induction (bal l x e r); intros; clearf;
- inv avl; solve [unfold create; intuition_in
-                |inv avl; avl_nns; simpl in *; omega_max ].
-Qed.
-
-Ltac omega_bal := match goal with 
-  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] => 
-     generalize (bal_height_1 x e H H') (bal_height_2 x e H H'); 
-     omega_max
-  end.
-
-
 
 (** * Insertion *)
 
@@ -506,89 +383,53 @@ Function add (elt:Type)(x:key)(e:elt)(s:t elt) { struct s } : t elt :=
       end
   end.
 
-Lemma add_avl_1 :  forall elt (m:t elt) x e, avl m -> 
- avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.
-Proof. 
- intros elt m x e; functional induction (add x e m); intros; inv avl; simpl in *.
- intuition; try constructor; simpl; auto; try omega_max.
- (* LT *)
- destruct IHt; auto.
- split.
- apply bal_avl; auto; omega_max.
- omega_bal.
- (* EQ *)
- intuition; omega_max.
- (* GT *)
- destruct IHt; auto.
- split.
- apply bal_avl; auto; omega_max.
- omega_bal.
-Qed.
-
-Lemma add_avl : forall elt (m:t elt) x e, avl m -> avl (add x e m).
-Proof.
- intros; generalize (add_avl_1 x e H); intuition.
-Qed.
-Hint Resolve add_avl.
-
-Lemma add_in : forall elt (m:t elt) x y e, avl m -> 
- (In y (add x e m) <-> X.eq y x \/ In y m).
+Lemma add_in : forall elt (m:t elt) x y e,
+ In y (add x e m) <-> X.eq y x \/ In y m.
 Proof.
  intros elt m x y e; functional induction (add x e m); auto; intros.
  intuition_in.
  (* LT *)
- inv avl.
- rewrite bal_in; auto.
- rewrite (IHt H0); intuition_in.
+ rewrite bal_in, IHt; intuition_in.
  (* EQ *)  
- inv avl.
  intuition_in.
  apply InRoot; apply X.eq_sym; eauto.
  (* GT *)
- inv avl.
- rewrite bal_in; auto.
- rewrite (IHt H1); intuition_in.
+ rewrite bal_in, IHt; intuition_in.
 Qed.
 
-Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m).
+Lemma add_bst : forall elt (m:t elt) x e, bst m -> bst (add x e m).
 Proof. 
  intros elt m x e; functional induction (add x e m); 
-   intros; inv bst; inv avl; auto; apply bal_bst; auto.
+   intros; inv bst; auto; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H4.
- intros.
- rewrite (add_in x y0 e H) in H0.
- intuition.
+ intro z; rewrite add_in; intuition.
  eauto.
  (* gt_tree -> gt_tree (add ...) *)
- red; red in H4.
- intros.
- rewrite (add_in x y0 e H5) in H0.
- intuition.
+ intro z; rewrite add_in; intuition.
  apply MX.lt_eq with x; auto.
 Qed.
 
-Lemma add_1 : forall elt (m:t elt) x y e, avl m -> X.eq x y -> MapsTo y e (add x e m).
+Lemma add_1 : forall elt (m:t elt) x y e, X.eq x y -> MapsTo y e (add x e m).
 Proof. 
  intros elt m x y e; functional induction (add x e m); 
-   intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; eauto.
+   intros; inv bst; try rewrite bal_mapsto; unfold create; eauto.
 Qed.
 
-Lemma add_2 : forall elt (m:t elt) x y e e', avl m -> ~X.eq x y -> 
+Lemma add_2 : forall elt (m:t elt) x y e e', ~X.eq x y -> 
  MapsTo y e m -> MapsTo y e (add x e' m).
 Proof.
  intros elt m x y e e'; induction m; simpl; auto.
  destruct (X.compare x k);
- intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; auto; 
+ intros; inv bst; try rewrite bal_mapsto; unfold create; auto; 
    inv MapsTo; auto; order.
 Qed.
 
-Lemma add_3 : forall elt (m:t elt) x y e e', avl m -> ~X.eq x y -> 
+Lemma add_3 : forall elt (m:t elt) x y e e', ~X.eq x y -> 
  MapsTo y e (add x e' m) -> MapsTo y e m.
 Proof.
  intros elt m x y e e'; induction m; simpl; auto. 
- intros; inv avl; inv MapsTo; auto; order.
- destruct (X.compare x k); intro; inv avl; 
+ intros; inv MapsTo; auto; order.
+ destruct (X.compare x k); intro; 
   try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; 
   order.
 Qed.
@@ -608,66 +449,33 @@ Function remove_min (elt:Type)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t
     | Node ll lx le lr lh => let (l',m) := (remove_min ll lx le lr : t elt*(key*elt)) in (bal l' x e r, m)
   end.
 
-Lemma remove_min_avl_1 : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> 
- avl (remove_min l x e r)#1 /\ 
- 0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1.
-Proof.
- intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
- inv avl; simpl in *; split; auto.
- avl_nns; omega_max.
- (* l = Node *)
- inversion_clear H.
- destruct (IHp lh); auto.
- split; simpl in *.
- rewrite e1 in *. simpl in *.
- apply bal_avl; subst;auto; omega_max.
- rewrite_all e1;simpl in *;omega_bal.
-Qed.
-
-Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> 
-    avl (remove_min l x e r)#1. 
-Proof.
- intros; generalize (remove_min_avl_1 H); intuition.
-Qed.
-
-Lemma remove_min_in : forall elt (l:t elt) x e r h y, avl (Node l x e r h) -> 
- (In y (Node l x e r h) <-> 
-  X.eq y (remove_min l x e r)#2#1 \/ In y (remove_min l x e r)#1).
+Lemma remove_min_in : forall elt (l:t elt) x e r h y,
+ In y (Node l x e r h) <-> 
+  X.eq y (remove_min l x e r)#2#1 \/ In y (remove_min l x e r)#1.
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in.
- (* l = Node *)
- inversion_clear H.
- generalize (remove_min_avl H0).
- 
  rewrite e1 in *; simpl; intros.
- rewrite bal_in; auto.
- generalize (IHp lh y H0).
- intuition.
- inversion_clear H7; intuition.
+ rewrite bal_in, In_node_iff, IHp; intuition.
 Qed.
 
-Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> 
- (MapsTo y e' (Node l x e r h) <-> 
+Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e',
+  MapsTo y e' (Node l x e r h) <-> 
    ((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2)
-    \/ MapsTo y e' (remove_min l x e r)#1).
+    \/ MapsTo y e' (remove_min l x e r)#1.
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in; subst; auto.
- (* l = Node *)
- inversion_clear H.
- generalize (remove_min_avl H0).
  rewrite e1 in *; simpl; intros.
  rewrite bal_mapsto; auto; unfold create.
  simpl in *;destruct (IHp lh y e').
- auto.
  intuition.
- inversion_clear H2; intuition.
- inversion_clear H9; intuition.
+ inversion_clear H1; intuition.
+ inversion_clear H3; intuition.
 Qed.
 
 Lemma remove_min_bst : forall elt (l:t elt) x e r h, 
- bst (Node l x e r h) -> avl (Node l x e r h) -> bst (remove_min l x e r)#1.
+ bst (Node l x e r h) -> bst (remove_min l x e r)#1.
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
@@ -675,29 +483,28 @@ Proof.
  apply bal_bst; auto.
  rewrite e1 in *; simpl in *; apply (IHp lh); auto.
  intro; intros.
- generalize (remove_min_in y H).
+ generalize (remove_min_in ll lx le lr lh y).
  rewrite e1; simpl in *.
  destruct 1.
- apply H3; intuition.
+ apply H2; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, 
- bst (Node l x e r h) -> avl (Node l x e r h) -> 
+ bst (Node l x e r h) -> 
  gt_tree (remove_min l x e r)#2#1 (remove_min l x e r)#1.
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H0.
+ inversion_clear H.
  intro; intro.
  rewrite e1 in *;simpl in *.
- generalize (IHp lh H1 H); clear H7 H6 IHp.
- generalize (remove_min_avl H).
- generalize (remove_min_in m#1 H).
+ generalize (IHp lh H0).
+ generalize (remove_min_in ll lx le lr lh m#1).
  rewrite e1; simpl; intros.
- rewrite (bal_in x e y H7 H5) in H0.
- assert (In m#1 (Node ll lx le lr lh)) by (rewrite H6; auto); clear H6.
+ rewrite (bal_in l' x e r y) in H.
+ assert (In m#1 (Node ll lx le lr lh)) by (rewrite H4; auto); clear H4.
  assert (X.lt m#1 x) by order.
- decompose [or] H0; order.
+ decompose [or] H; order.
 Qed.
 
 
@@ -718,46 +525,20 @@ Function merge (elt:Type) (s1 s2 : t elt) : tree elt :=  match s1,s2 with
     end
 end.
 
-Lemma merge_avl_1 : forall elt (s1 s2:t elt), 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 elt s1 s2; functional induction (merge s1 s2); simpl in *; intros.
- split; auto; avl_nns; omega_max.
- destruct s1;try contradiction;clear y.
- split; auto; avl_nns; simpl in *; omega_max.
- destruct s1;try contradiction;clear y.
- generalize (remove_min_avl_1 H0).
- rewrite e3; simpl;destruct 1.
- split.
- apply bal_avl; auto.
- omega_max.
- omega_bal.
-Qed.
-
-Lemma merge_avl : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> 
-  -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2).
-Proof. 
- intros; generalize (merge_avl_1 H H0 H1); intuition.
-Qed.
-
-Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> bst s2 -> 
  (In y (merge s1 s2) <-> In y s1 \/ In y s2).
 Proof. 
  intros elt s1 s2; functional induction (merge s1 s2);intros.
  intuition_in.
  intuition_in.
  destruct s1;try contradiction;clear y.
-(*  rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *)
  replace s2' with ((remove_min l2 x2 e2 r2)#1) by (rewrite e3; auto).
  rewrite bal_in; auto.
- generalize (remove_min_in y0 H2); rewrite e3; simpl; intro.
- rewrite H3; intuition.
- generalize (remove_min_avl H2); rewrite e3; simpl; auto.
+ generalize (remove_min_in l2 x2 e2 r2 h2 y0); rewrite e3; simpl; intro.
+ rewrite H1; intuition.
 Qed.
 
-Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> bst s2 -> 
   (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2).
 Proof.
  intros elt s1 s2; functional induction (@merge elt s1 s2); intros.
@@ -766,13 +547,12 @@ Proof.
  destruct s1;try contradiction;clear y.
  replace s2' with ((remove_min l2 x2 e2 r2)#1); [|rewrite e3; auto].
  rewrite bal_mapsto; auto; unfold create.
- generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro.
- rewrite H3; intuition (try subst; auto).
- inversion_clear H3; intuition.
- generalize (remove_min_avl H2); rewrite e3; simpl; auto.
+ generalize (remove_min_mapsto l2 x2 e2 r2 h2 y0 e); rewrite e3; simpl; intro.
+ rewrite H1; intuition (try subst; auto).
+ inversion_clear H1; intuition.
 Qed.
 
-Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> bst s2 -> 
  (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (merge s1 s2). 
 Proof.
@@ -780,14 +560,14 @@ Proof.
 
  apply bal_bst; auto.
  destruct s1;try contradiction.
- generalize (remove_min_bst H1); rewrite e3; simpl in *; auto.
+ generalize (remove_min_bst H0); rewrite e3; simpl in *; auto.
  destruct s1;try contradiction.
  intro; intro.
- apply H3; auto.
- generalize (remove_min_in x H2); rewrite e3; simpl; intuition.
+ apply H1; auto.
+ generalize (remove_min_in l2 x2 e2 r2 h2 x); rewrite e3; simpl; intuition.
  destruct s1;try contradiction.
- generalize (remove_min_gt_tree H1); rewrite e3; simpl; auto.
-Qed. 
+ generalize (remove_min_gt_tree H0); rewrite e3; simpl; auto.
+Qed.
 
 
 
@@ -803,83 +583,52 @@ Function remove (elt:Type)(x:key)(s:t elt) { struct s } : t elt := match s with
       end
    end.
 
-Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> 
- avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
-Proof.
- intros elt s x; functional induction (@remove elt x s); intros.
- split; auto; omega_max.
- (* LT *)
- inv avl.
- destruct (IHt H0).
- split. 
- apply bal_avl; auto.
- omega_max.
- omega_bal.
- (* EQ *)
- inv avl. 
- generalize (merge_avl_1 H0 H1 H2).
- intuition omega_max.
- (* GT *)
- inv avl.
- destruct (IHt H1).
- split. 
- apply bal_avl; auto.
- omega_max.
- omega_bal.
-Qed.
-
-Lemma remove_avl : forall elt (s:t elt) x, avl s -> avl (remove x s).
-Proof. 
- intros; generalize (remove_avl_1 x H); intuition.
-Qed.
-Hint Resolve remove_avl.
-
-Lemma remove_in : forall elt (s:t elt) x y, bst s -> avl s -> 
+Lemma remove_in : forall elt (s:t elt) x y, bst s -> 
  (In y (remove x s) <-> ~ X.eq y x /\ In y s).
 Proof.
  intros elt s x; functional induction (@remove elt x s); simpl; intros.
  intuition_in.
  (* LT *)
- inv avl; inv bst; clear e1.
+ inv bst; clear e1.
  rewrite bal_in; auto.
  generalize (IHt y0 H0); intuition; [ order | order | intuition_in ].
  (* EQ *)
- inv avl; inv bst; clear e1.
+ inv bst; clear e1.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
- elim H9; eauto.
+ elim H4; eauto.
  (* GT *)
- inv avl; inv bst; clear e1.
+ inv bst; clear e1.
  rewrite bal_in; auto.
- generalize (IHt y0 H5); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
 Qed.
 
-Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s).
+Lemma remove_bst : forall elt (s:t elt) x, bst s -> bst (remove x s).
 Proof. 
  intros elt s x; functional induction (@remove elt x s); simpl; intros.
  auto.
  (* LT *)
- inv avl; inv bst.
+ inv bst.
  apply bal_bst; auto.
  intro; intro.
  rewrite (remove_in x y0 H0) in H; auto.
  destruct H; eauto.
  (* EQ *)
- inv avl; inv bst.
+ inv bst.
  apply merge_bst; eauto.
  (* GT *) 
- inv avl; inv bst.
+ inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in x y0 H5) in H; auto.
+ rewrite (remove_in x y0 H1) in H; auto.
  destruct H; eauto.
 Qed.
 
-Lemma remove_1 : forall elt (m:t elt) x y, bst m -> avl m -> X.eq x y -> ~ In y (remove x m).
+Lemma remove_1 : forall elt (m:t elt) x y, bst m -> X.eq x y -> ~ In y (remove x m).
 Proof. 
  intros; rewrite remove_in; intuition.
 Qed. 
 
-Lemma remove_2 : forall elt (m:t elt) x y e, bst m -> avl m -> ~X.eq x y -> 
+Lemma remove_2 : forall elt (m:t elt) x y e, bst m -> ~X.eq x y -> 
  MapsTo y e m -> MapsTo y e (remove x m).
 Proof.
  intros elt m x y e; induction m; simpl; auto.
@@ -890,13 +639,13 @@ Proof.
  inv MapsTo; auto; order.
 Qed.
 
-Lemma remove_3 : forall elt (m:t elt) x y e, bst m -> avl m ->
+Lemma remove_3 : forall elt (m:t elt) x y e, bst m ->
  MapsTo y e (remove x m) -> MapsTo y e m.
 Proof.
  intros elt m x y e; induction m; simpl; auto.
- destruct (X.compare x k); intros Bs Av; inv avl; inv bst; 
+ destruct (X.compare x k); intros Bs; inv bst; 
   try rewrite bal_mapsto; auto; unfold create.
-  intros; inv MapsTo; auto. 
+  intros; inv MapsTo; auto.
   rewrite merge_mapsto; intuition.
   intros; inv MapsTo; auto.
 Qed.
@@ -920,11 +669,6 @@ Proof.
  unfold empty; auto.
 Qed.
 
-Lemma empty_avl : avl empty.
-Proof. 
- unfold empty; auto.
-Qed.
-
 Lemma empty_1 : Empty empty.
 Proof.
  unfold empty, Empty; intuition_in.
@@ -1002,7 +746,7 @@ Qed.
 
 (** An all-in-one spec for [add] used later in the naive [map2] *)
 
-Lemma add_spec : forall m x y e , bst m -> avl m -> 
+Lemma add_spec : forall m x y e , bst m -> 
   find x (add y e m) = if MX.eq_dec x y then Some e else find x m.
 Proof.
 intros.
@@ -1017,7 +761,7 @@ apply add_bst; auto.
 apply add_2; auto.
 apply find_2; auto.
 case_eq (find x (add y e m)); auto; intros.
-rewrite <- H1; symmetry.
+rewrite <- H0; symmetry.
 apply find_1; auto.
 eapply add_3; eauto.
 apply find_2; eauto.
@@ -1270,16 +1014,9 @@ Qed.
 
 (** termination of [compare_aux] *)
 
-Open Scope nat_scope.
-
-Fixpoint measure_e_t (s : t elt) : nat := match s with
-  | Leaf => 0
-  | Node l _ _ r _ => 1 + measure_e_t l + measure_e_t r
- end.
-
-Fixpoint measure_e (e : enumeration) : nat := match e with
-  | End => 0
-  | More _ _ s r => 1 + measure_e_t s + measure_e r
+Fixpoint cardinal_e (e : enumeration) : nat := match e with
+  | End => 0%nat
+  | More _ _ s r => S (cardinal s + cardinal_e r)
  end.
 
 (** [cons t e] adds the elements of tree [t] on the head of 
@@ -1291,8 +1028,8 @@ Fixpoint cons s e {struct s} : enumeration :=
   | Node l x d r h => cons l (More x d r e)
  end.
 
-Lemma cons_measure_e : forall s e, 
- measure_e (cons s e) = measure_e_t s + measure_e e.
+Lemma cons_cardinal_e : forall s e, 
+ cardinal_e (cons s e) = (cardinal s + cardinal_e e)%nat.
 Proof.
  induction s; simpl; intros; auto.
  rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith.
@@ -1322,11 +1059,11 @@ Proof.
  apply flatten_e_elements.
 Qed.
 
-Definition measure2 e := (measure_e e#1 + measure_e e#2)%nat.
+Definition cardinal_e_2 e := (cardinal_e e#1 + cardinal_e e#2)%nat.
 
 Function equal_aux 
  (cmp: elt -> elt -> bool)(e:enumeration*enumeration)
- { measure measure2 e } : bool := 
+ { measure cardinal_e_2 e } : bool := 
  match e with 
  | (End,End) => true
  | (End,More _ _ _ _) => false
@@ -1339,8 +1076,8 @@ Function equal_aux
        end
  end.
 Proof.
-intros; unfold measure2; simpl; 
-abstract (do 2 rewrite cons_measure_e; romega with *).
+intros; unfold cardinal_e_2; simpl; 
+abstract (do 2 rewrite cons_cardinal_e; romega with *).
 Defined.
 
 Definition equal (cmp: elt -> elt -> bool) s s' := 
@@ -1386,8 +1123,6 @@ Proof.
  split; [apply L.equal_2|apply L.equal_1]; auto.
 Qed.
 
-Close Scope nat_scope.
-
 End Elt2.
 
 Section Elts. 
@@ -1408,12 +1143,6 @@ Proof.
 destruct m; simpl; auto.
 Qed.
 
-Lemma map_avl : forall m, avl m -> avl (map m).
-Proof.
-induction m; simpl; auto.
-inversion_clear 1; constructor; auto; do 2 rewrite map_height; auto.
-Qed.
-
 Lemma map_1 : forall (m: tree elt)(x:key)(e:elt), 
     MapsTo x e m -> MapsTo x (f e) (map m).
 Proof.
@@ -1449,12 +1178,6 @@ Proof.
 destruct m; simpl; auto.
 Qed.
 
-Lemma mapi_avl : forall m, avl m -> avl (mapi m).
-Proof.
-induction m; simpl; auto.
-inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto.
-Qed.
-
 Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), 
     MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi m).
 Proof.
@@ -1494,30 +1217,14 @@ Definition anti_elements (l:list (key*elt'')) := L.fold (@add _) l (empty _).
 Definition map2 (m:t elt)(m':t elt') : t elt'' := 
   anti_elements (L.map2 f (elements m) (elements m')).
 
-Lemma anti_elements_avl_aux : forall (l:list (key*elt''))(m:t elt''), 
-  avl m -> avl (L.fold (@add _) l m).
-Proof.
-unfold anti_elements; induction l.
-simpl; auto.
-simpl; destruct a; intros.
-apply IHl.
-apply add_avl; auto.
-Qed.
-
-Lemma anti_elements_avl : forall l, avl (anti_elements l).
-Proof.
-unfold anti_elements, empty; intros; apply anti_elements_avl_aux; auto.
-Qed.
-
 Lemma anti_elements_bst_aux : forall (l:list (key*elt''))(m:t elt''), 
-  bst m -> avl m -> bst (L.fold (@add _) l m).
+  bst m -> bst (L.fold (@add _) l m).
 Proof.
 induction l.
 simpl; auto.
 simpl; destruct a; intros.
 apply IHl.
 apply add_bst; auto.
-apply add_avl; auto.
 Qed.
 
 Lemma anti_elements_bst : forall l, bst (anti_elements l).
@@ -1526,42 +1233,42 @@ unfold anti_elements, empty; intros; apply anti_elements_bst_aux; auto.
 Qed.
 
 Lemma anti_elements_mapsto_aux : forall (l:list (key*elt'')) m k e,
-  bst m -> avl m -> NoDupA (PX.eqk (elt:=elt'')) l -> 
+  bst m -> NoDupA (PX.eqk (elt:=elt'')) l -> 
   (forall x, L.PX.In x l -> In x m -> False) -> 
   (MapsTo k e (L.fold (@add _) l m) <-> L.PX.MapsTo k e l \/ MapsTo k e m).
 Proof.
 induction l. 
 simpl; auto.
 intuition.
-inversion H4.
+inversion H3.
 simpl; destruct a; intros.
-rewrite IHl; clear IHl; auto using add_bst, add_avl.
+rewrite IHl; clear IHl; auto using add_bst.
 intuition.
 assert (find k0 (add k e m) = Some e0).
  apply find_1; auto.
  apply add_bst; auto.
-clear H4. 
-rewrite add_spec in H3; auto.
+clear H3.
+rewrite add_spec in H2; auto.
 destruct (MX.eq_dec k0 k).
-inversion_clear H3; subst; auto.
+inversion_clear H2; subst; auto.
 right; apply find_2; auto.
-inversion_clear H4; auto.
-compute in H3; destruct H3.
+inversion_clear H3; auto.
+compute in H2; destruct H2.
 subst; right; apply add_1; auto.
-inversion_clear H1.
+inversion_clear H0.
 destruct (MX.eq_dec k0 k).
-destruct (H2 k); eauto.
+destruct (H1 k); eauto.
 right; apply add_2; auto.
-inversion H1; auto.
+inversion H0; auto.
 intros.
-inversion_clear H1.
+inversion_clear H0.
 assert (~X.eq x k).
- contradict H5.
- destruct H3.
+ contradict H4.
+ destruct H2.
  apply InA_eqA with (x,x0); eauto.
-apply (H2 x).
-destruct H3; exists x0; auto.
-revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto.
+apply (H1 x).
+destruct H2; exists x0; auto.
+revert H3; do 2 rewrite <- In_alt; destruct 1; exists x0; auto.
 eapply add_3; eauto.
 Qed.
 
@@ -1576,11 +1283,6 @@ inversion H1.
 inversion 2.
 Qed.
 
-Lemma map2_avl : forall (m: t elt)(m': t elt'), avl (map2 m m').
-Proof.
-unfold map2; intros; apply anti_elements_avl; auto.
-Qed.
-
 Lemma map2_bst : forall (m: t elt)(m': t elt'), bst (map2 m m').
 Proof.
 unfold map2; intros; apply anti_elements_bst; auto.
@@ -1666,10 +1368,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Module E := X.
  Module Raw := Raw I X. 
 
- Record bbst (elt:Type) := 
-  Bbst {this :> Raw.tree elt; is_bst : Raw.bst this; is_avl: Raw.avl this}.
+ Record bst (elt:Type) := 
+  Bst {this :> Raw.tree elt; is_bst : Raw.bst this}.
  
- Definition t := bbst. 
+ Definition t := bst. 
  Definition key := E.t.
  
  Section Elt. 
@@ -1679,20 +1381,17 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Implicit Types x y : key. 
  Implicit Types e : elt. 
 
- Definition empty : t elt := Bbst (Raw.empty_bst elt) (Raw.empty_avl elt).
+ Definition empty : t elt := Bst (Raw.empty_bst elt).
  Definition is_empty m : bool := Raw.is_empty m.(this).
- Definition add x e m : t elt := 
-  Bbst (Raw.add_bst x e m.(is_bst) m.(is_avl)) (Raw.add_avl x e m.(is_avl)).
- Definition remove x m : t elt := 
-  Bbst (Raw.remove_bst x m.(is_bst) m.(is_avl)) (Raw.remove_avl x m.(is_avl)). 
+ Definition add x e m : t elt := Bst (Raw.add_bst x e m.(is_bst)).
+ Definition remove x m : t elt := Bst (Raw.remove_bst x m.(is_bst)). 
  Definition mem x m : bool := Raw.mem x m.(this).
  Definition find x m : option elt := Raw.find x m.(this).
- Definition map f m : t elt' := 
-  Bbst (Raw.map_bst f m.(is_bst)) (Raw.map_avl f m.(is_avl)).
+ Definition map f m : t elt' := Bst (Raw.map_bst f m.(is_bst)).
  Definition mapi (f:key->elt->elt') m : t elt' := 
-  Bbst (Raw.mapi_bst f m.(is_bst)) (Raw.mapi_avl f m.(is_avl)).
+  Bst (Raw.mapi_bst f m.(is_bst)).
  Definition map2 f m (m':t elt') : t elt'' := 
-  Bbst (Raw.map2_bst f m m') (Raw.map2_avl f m m').
+  Bst (Raw.map2_bst f m m').
  Definition elements m : list (key*elt) := Raw.elements m.(this).
  Definition cardinal m := Raw.cardinal m.(this).
  Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i.
@@ -1729,22 +1428,21 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. intros m; exact (@Raw.is_empty_2 _ m.(this)). Qed.
 
  Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
- Proof. intros m x y e; exact (@Raw.add_1 elt _ x y e m.(is_avl)). Qed.
+ Proof. intros m x y e; exact (@Raw.add_1 elt _ x y e). Qed.
  Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
- Proof. intros m x y e e'; exact (@Raw.add_2 elt _ x y e e' m.(is_avl)). Qed.
+ Proof. intros m x y e e'; exact (@Raw.add_2 elt _ x y e e'). Qed.
  Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
- Proof. intros m x y e e'; exact (@Raw.add_3 elt _ x y e e' m.(is_avl)). Qed.
+ Proof. intros m x y e e'; exact (@Raw.add_3 elt _ x y e e'). Qed.
 
  Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
  Proof.
  unfold In, remove; intros m x y; rewrite Raw.In_alt; simpl; apply Raw.remove_1; auto.
  apply m.(is_bst).
- apply m.(is_avl).
  Qed.
  Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
- Proof. intros m x y e; exact (@Raw.remove_2 elt _ x y e m.(is_bst) m.(is_avl)). Qed.
+ Proof. intros m x y e; exact (@Raw.remove_2 elt _ x y e m.(is_bst)). Qed.
  Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
- Proof. intros m x y e; exact (@Raw.remove_3 elt _ x y e m.(is_bst) m.(is_avl)). Qed.
+ Proof. intros m x y e; exact (@Raw.remove_3 elt _ x y e m.(is_bst)). Qed.
 
 
  Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. 
@@ -1795,16 +1493,16 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma equal_1 : forall m m' cmp, 
    Equivb cmp m m' -> equal cmp m m' = true. 
  Proof. 
- unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
+ unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; 
   intros; simpl in *; rewrite Raw.equal_Equivb; auto.
  Qed. 
 
  Lemma equal_2 : forall m m' cmp, 
    equal cmp m m' = true -> Equivb cmp m m'.
  Proof. 
- unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
+ unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; 
   intros; simpl in *; rewrite <-Raw.equal_Equivb; auto.
- Qed.  
+ Qed.
 
  End Elt.
 
@@ -1869,10 +1567,8 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Definition elements (m:t) := 
     LO.MapS.Build_slist (Raw.elements_sort m.(is_bst)).
 
-  Open Scope nat_scope.
-
   Function compare_aux (e:Raw.enumeration D.t * Raw.enumeration D.t) 
-   { measure Raw.measure2 e } : comparison := 
+   { measure Raw.cardinal_e_2 e } : comparison := 
   match e with 
   | (Raw.End, Raw.End) => Eq
   | (Raw.End, Raw.More _ _ _ _) => Lt
@@ -1889,8 +1585,8 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
       end
   end.
   Proof.
-  intros; unfold Raw.measure2; simpl; 
-  abstract (do 2 rewrite Raw.cons_measure_e; romega with *).
+  intros; unfold Raw.cardinal_e_2; simpl; 
+  abstract (do 2 rewrite Raw.cons_cardinal_e; romega with *).
   Defined.
 
   Lemma compare_aux_Eq : 
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 83dc3f1c4e..5973b21ece 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1,4 +1,3 @@
-
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -14,8 +13,29 @@
 
 (* $Id$ *)
 
+(** * FSetAVL *)
+
 (** This module implements sets using AVL trees.
-    It follows the implementation from Ocaml's standard library. *)
+    It follows the implementation from Ocaml's standard library,
+    
+    All operations given here expect and produce well-balanced trees
+    (in the ocaml sense: heigths of subtrees shouldn't differ by more
+    than 2), and hence has low complexities (e.g. add is logarithmic
+    in the size of the set). But proving these balancing preservations
+    is in fact not necessary for ensuring correct operational behavior
+    and hence fulfilling the FSet interface. As a consequence,
+    balancing results are not part of this file anymore, they can 
+    now be found in [FSetFullAVL].
+
+    Four operations ([union], [subset], [compare] and [equal]) have
+    been slightly adapted in order to have only structural recursive
+    calls. The precise ocaml versions of these operations have also
+    been formalized (thanks to Function+measure), see [ocaml_union],
+    [ocaml_subset], [ocaml_compare] and [ocaml_equal] in
+    [FSetFullAVL]. The structural variants compute faster in Coq,
+    whereas the other variants produce nicer and/or (slightly) faster
+    code after extraction.
+*)
 
 Require Import Recdef FSetInterface FSetList ZArith Int.
 
@@ -23,8 +43,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Module Raw (Import I:Int)(X:OrderedType).
-Module Import II:=MoreInt(I).
-Open Scope Int_scope.
+Open Local Scope Int_scope.
 Module MX := OrderedTypeFacts X.
 
 Definition elt := X.t.
@@ -87,35 +106,11 @@ Inductive bst : tree -> Prop :=
   | BSNode : forall x l r h, bst l -> bst r -> 
      lt_tree x l -> gt_tree x r -> bst (Node l x r h).
 
-(** * AVL trees *)
-
-(** [avl s] : [s] is a properly balanced AVL tree,
-    i.e. for any node the heights of the two children
-    differ by at most 2 *)
-
-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 -> 
-      avl (Node l x r h).
-
-
-
 (** * Automation and dedicated tactics *)
 
-Hint Constructors In bst avl.
+Hint Constructors In bst.
 Hint Unfold lt_tree gt_tree.
 
-(** A tactic for cleaning hypothesis after use of functional induction. *)
-
-Ltac clearf :=
- match goal with 
-  | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
-  | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
-  | _ => idtac
- end.
-
 (** A tactic to repeat [inversion_clear] on all hyps of the 
     form [(f (Node _ _ _ _))] *)
 
@@ -128,14 +123,6 @@ Ltac inv f :=
      | _ => idtac
   end.
 
-(** Same, but with a backup of the original hypothesis. *)
-
-Ltac safe_inv f := match goal with 
-  | H:f (Node _ _ _ _) |- _ => 
-        generalize H; inversion_clear H; safe_inv f
-  | _ => intros 
- end.
-
 Ltac intuition_in := repeat progress (intuition; inv In).
 
 (** Helper tactic concerning order of elements. *)
@@ -146,39 +133,8 @@ Ltac order := match goal with
  | _ => MX.order
 end.
 
-(** Tactics about [avl] *)
-
-Lemma height_non_negative : forall s : tree, avl s -> height s >= 0.
-Proof.
- induction s; simpl; intros; auto with zarith.
- inv avl; intuition; omega_max.
-Qed.
-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 := 
-     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 
-   | Prop => avl_nn_hyp h
-   | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
-  end.
-
-(* Repeat the previous tactic. 
-   Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
-
-Ltac avl_nns :=
-  match goal with 
-     | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
-     | _ => idtac
-  end.
-
-
-
-(** * Basic results about [In], [lt_tree], [gt_tree], [avl], [height] *)
+(** * Basic results about [In], [lt_tree], [gt_tree], [height] *)
 
 (** [In] is compatible with [X.eq] *)
 
@@ -189,6 +145,13 @@ Proof.
 Qed.
 Hint Immediate In_1.
 
+Lemma In_node_iff : 
+ forall l x r h y, 
+  In y (Node l x r h) <-> In y l \/ X.eq y x \/ In y r.
+Proof.
+ intuition_in.
+Qed.
+
 (** Results about [lt_tree] and [gt_tree] *)
 
 Lemma lt_leaf : forall x : elt, lt_tree x Leaf.
@@ -243,26 +206,6 @@ Qed.
 
 Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 
-(** Results about [avl] *)
-
-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)).
-Proof.
-  intros; auto.
-Qed.
-Hint Resolve avl_node.
-
-(** Results about [height] *)
-
-Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.
-Proof.
- destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; elimtype False; omega_max.
-Qed.
-
-
 
 (** * Some shortcuts. *)
 
@@ -273,35 +216,21 @@ Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
 Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
 
 
-
-(** trick for emulating [assert false] in Coq. *)
-
-Definition assert_false := Leaf.
-Lemma assert_false_cardinal : cardinal assert_false = 0%nat.
-Proof. simpl; auto. Qed.
-Opaque assert_false.
-
-
-
 (** * Empty set *)
 
 Definition empty := Leaf.
 
-Lemma empty_bst : bst empty.
+Lemma empty_1 : Empty empty.
 Proof.
- auto.
+ intro; intro.
+ inversion H.
 Qed.
 
-Lemma empty_avl : avl empty.
-Proof. 
+Lemma empty_bst : bst empty.
+Proof.
  auto.
 Qed.
 
-Lemma empty_1 : Empty empty.
-Proof.
- intro; intro.
- inversion H.
-Qed.
 
 (** * Emptyness test *)
 
@@ -337,7 +266,7 @@ Function mem (x:elt)(s:t) { struct s } : bool :=
 
 Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true.
 Proof.
- intros s x; functional induction mem x s; auto; intros; clearf;
+ intros s x; functional induction mem x s; auto; intros; try clear e0; 
   inv bst; intuition_in; order.
 Qed.
 
@@ -352,17 +281,6 @@ Qed.
 
 Definition singleton (x : elt) := Node Leaf x Leaf 1.
 
-Lemma singleton_bst : forall x : elt, bst (singleton x).
-Proof.
- unfold singleton; auto.
-Qed.
-
-Lemma singleton_avl : forall x : elt, avl (singleton x).
-Proof.
- unfold singleton; intro.
- constructor; auto; try red; simpl; omega_max.
-Qed.
-
 Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y. 
 Proof. 
  unfold singleton; intros; inv In; order.
@@ -373,6 +291,11 @@ Proof.
  unfold singleton; auto.
 Qed.
 
+Lemma singleton_bst : forall x : elt, bst (singleton x).
+Proof.
+ unfold singleton; auto.
+Qed.
+
 
 
 (** * Helper functions *)
@@ -383,6 +306,12 @@ Qed.
 Definition create l x r := 
    Node l x r (max (height l) (height r) + 1).
 
+Lemma create_in : 
+ forall l x r y,  In y (create l x r) <-> X.eq y x \/ In y l \/ In y r.
+Proof.
+ unfold create; split; [ inversion_clear 1 | ]; intuition.
+Qed.
+
 Lemma create_bst : 
  forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> 
  bst (create l x r).
@@ -391,42 +320,24 @@ Proof.
 Qed.
 Hint Resolve create_bst.
 
-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 -> 
- height (create l x r) = max (height l) (height r) + 1.
-Proof.
- unfold create; intros; auto.
-Qed.
-
-Lemma create_in : 
- forall l x r y,  In y (create l x r) <-> X.eq y x \/ In y l \/ In y r.
-Proof.
- unfold create; split; [ inversion_clear 1 | ]; intuition.
-Qed.
-
 
 (** [bal l x r] acts as [create], but performs one step of
     rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *)
 
+Definition assert_false := create.
+
 Function bal (l:t)(x:elt)(r:t) : t := 
   let hl := height l in 
   let hr := height r in
   if gt_le_dec hl (hr+2) then 
     match l with 
-     | Leaf => assert_false
+     | Leaf => assert_false l x r
      | Node ll lx lr _ => 
        if ge_lt_dec (height ll) (height lr) then 
          create ll lx (create lr x r)
        else 
          match lr with 
-          | Leaf => assert_false 
+          | Leaf => assert_false l x r
           | Node lrl lrx lrr _ => 
               create (create ll lx lrl) lrx (create lrr x r)
          end
@@ -434,13 +345,13 @@ Function bal (l:t)(x:elt)(r:t) : t :=
   else 
     if gt_le_dec hr (hl+2) then 
       match r with
-       | Leaf => assert_false
+       | Leaf => assert_false l x r
        | Node rl rx rr _ =>
          if ge_lt_dec (height rr) (height rl) then 
             create (create l x rl) rx rr
          else 
            match rl with
-            | Leaf => assert_false
+            | Leaf => assert_false l x r
             | Node rll rlx rlr _ => 
                 create (create l x rll) rlx (create rlr rx rr) 
            end
@@ -448,6 +359,13 @@ Function bal (l:t)(x:elt)(r:t) : t :=
     else 
       create l x r. 
 
+Lemma bal_in : forall l x r y, 
+ In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r.
+Proof.
+ intros l x r; functional induction bal l x r; intros; try clear e0; 
+ rewrite !create_in; intuition_in.
+Qed.
+
 Lemma bal_bst : forall l x r, bst l -> bst r -> 
  lt_tree x l -> gt_tree x r -> bst (bal l x r).
 Proof.
@@ -456,51 +374,7 @@ Proof.
  (apply lt_tree_node || apply gt_tree_node); auto; 
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
 Qed.
-
-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; repeat apply create_avl; simpl in *; auto; omega_max.
-Qed.
-
-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.
- intros l x r; functional induction bal l x r; intros; clearf;
- 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 -> 
- 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.
-
-Lemma bal_in : forall l x r y, avl l -> avl r -> 
- (In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r).
-Proof.
- intros l x r; functional induction bal l x r; intros; clearf;
- solve [repeat rewrite create_in; intuition_in
-       |inv avl; avl_nns; simpl in *; omega_max ].
-Qed.
-
-Lemma bal_cardinal : forall l x r, 
- (cardinal (bal l x r) <= S (cardinal l + cardinal r))%nat.
-Proof.
- intros l x r; functional induction bal l x r; intros; clearf;
- simpl; auto with arith; romega with *.
-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'); 
-     omega_max
-  end. 
-
+Hint Resolve bal_bst.
 
 
 (** * Insertion *)
@@ -515,76 +389,33 @@ Function add (x:elt)(s:t) { struct s } : t := match s with
       end
   end.
 
-Lemma add_avl_1 :  forall s x, avl s -> 
- avl (add x s) /\ 0 <= height (add x s) - height s <= 1.
-Proof. 
- intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *.
- intuition; try constructor; simpl; auto; try omega_max.
- (* LT *)
- destruct IHt; auto.
- split.
- apply bal_avl; auto; omega_max.
- omega_bal.
- (* EQ *)
- intuition; omega_max.
- (* GT *)
- destruct IHt; auto.
- split.
- apply bal_avl; auto; omega_max.
- omega_bal.
-Qed.
-
-Lemma add_avl : forall s x, avl s -> avl (add x s).
-Proof.
- intros; destruct (@add_avl_1 s x H); auto.
-Qed.
-Hint Resolve add_avl.
-
-Lemma add_in : forall s x y, avl s -> 
- (In y (add x s) <-> X.eq y x \/ In y s).
+Lemma add_in : forall s x y,
+ In y (add x s) <-> X.eq y x \/ In y s.
 Proof.
- intros s x; functional induction (add x s); auto; intros.
- intuition_in.
- (* LT *)
- inv avl.
- rewrite bal_in; auto.
- rewrite (IHt y0 H0); intuition_in.
- (* EQ *)  
- inv avl.
- intuition.
+ intros s x; functional induction (add x s); auto; intros; 
+ try rewrite bal_in, IHt; intuition_in.
  eapply In_1; eauto.
- (* GT *)
- inv avl.
- rewrite bal_in; auto.
- rewrite (IHt y0 H1); intuition_in.
 Qed.
 
-Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s).
+Lemma add_bst : forall s x, bst s -> bst (add x s).
 Proof. 
- intros s x; functional induction (add x s); auto; intros.
- inv bst; inv avl; apply bal_bst; auto.
+ intros s x; functional induction (add x s); auto; intros; 
+ inv bst; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H4.
+ red; red in H3.
  intros.
- rewrite (add_in x y0 H) in H0.
+ rewrite add_in in H.
  intuition.
  eauto.
- inv bst; inv avl; apply bal_bst; auto.
+ inv bst; auto using bal_bst.
  (* gt_tree -> gt_tree (add ...) *)
- red; red in H4.
+ red; red in H3.
  intros.
- rewrite (add_in x y0 H5) in H0.
+ rewrite add_in in H.
  intuition.
  apply MX.lt_eq with x; auto.
 Qed.
-
-Lemma add_cardinal : forall x s, 
- (cardinal (add x s) <= S (cardinal s))%nat.
-Proof.
- intros; functional induction add x s; simpl; auto with arith.
- generalize (bal_cardinal (add x l) y r); romega with *.
- generalize (bal_cardinal l y (add x r)); romega with *.
-Qed.
+Hint Resolve add_bst.
 
 
 
@@ -607,7 +438,7 @@ Fixpoint join (l:t) : elt -> t -> t :=
           end
   end.
 
-(* XXX: Comment utiliser Function pour definit join et eviter join_tac ? *)
+(* Function can't deal with internal fix. Let's do its job by hand: *)
 
 Ltac join_tac := 
  intro l; induction l as [| ll _ lx lr Hlr lh]; 
@@ -624,128 +455,33 @@ Ltac join_tac :=
            end
          | ] ] ] ]; intros.
 
-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. 
- join_tac.
-
- split; simpl; auto. 
- destruct (add_avl_1 x H0).
- avl_nns; omega_max.
- split; auto.
- set (l:=Node ll lx lr lh) in *.
- destruct (add_avl_1 x H).
- simpl (height Leaf).
- avl_nns; omega_max.
-
- inversion_clear H.
- assert (height (Node rl rx rr rh) = rh); auto.
- set (r := Node rl rx rr rh) in *; clearbody r.
- destruct (Hlr x r H2 H0); clear Hrl Hlr.
- set (j := join lr x r) in *; clearbody j.
- simpl.
- assert (-(3) <= height ll - height j <= 3) by omega_max.
- split.
- apply bal_avl; auto.
- omega_bal.
-
- inversion_clear H0.
- assert (height (Node ll lx lr lh) = lh); auto.
- set (l := Node ll lx lr lh) in *; clearbody l.
- destruct (Hrl H H1); clear Hrl Hlr.
- set (j := join l x rl) in *; clearbody j.
- simpl.
- assert (-(3) <= height j - height rr <= 3) by omega_max.
- split.
- apply bal_avl; auto.
- omega_bal.
-
- clear Hrl Hlr.
- assert (height (Node ll lx lr lh) = lh); auto.
- assert (height (Node rl rx rr rh) = rh); auto.
- set (l := Node ll lx lr lh) in *; clearbody l.
- set (r := Node rl rx rr rh) in *; clearbody r.
- assert (-(2) <= height l - height r <= 2) by omega_max.
- split.
- apply create_avl; auto.
- rewrite create_height; auto; omega_max.
-Qed.
-
-Lemma join_avl : forall l x r, avl l -> avl r -> avl (join l x r).
-Proof.
- intros; destruct (@join_avl_1 l x r H H0); auto.
-Qed.
-Hint Resolve join_avl.
-
-Lemma join_in : forall l x r y, avl l -> avl r -> 
-     (In y (join l x r) <-> X.eq y x \/ In y l \/ In y r).
+Lemma join_in : forall l x r y, 
+ In y (join l x r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
  join_tac.
  simpl.
  rewrite add_in; intuition_in.
-
  rewrite add_in; intuition_in.
-
- inv avl.
- rewrite bal_in; auto.
- rewrite Hlr; clear Hlr Hrl; intuition_in.
-
- inv avl.
- rewrite bal_in; auto.
- rewrite Hrl; clear Hlr Hrl; intuition_in.
-
+ rewrite bal_in, Hlr; clear Hlr Hrl; intuition_in.
+ rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in.
  apply create_in.
 Qed.
 
-Lemma join_bst : forall l x r, bst l -> avl l -> bst r -> avl r -> 
+Lemma join_bst : forall l x r, bst l -> bst r -> 
  lt_tree x l -> gt_tree x r -> bst (join l x r).
 Proof.
- join_tac.
- apply add_bst; auto.
- apply add_bst; auto.
-
- inv bst; safe_inv avl.
- apply bal_bst; auto.
- clear Hrl Hlr H13 H14 H16 H17 z; intro; intros.
- set (r:=Node rl rx rr rh) in *; clearbody r.
- rewrite (@join_in lr x r y) in H13; auto.
- intuition.
- apply MX.lt_eq with x; eauto.
- eauto.
-
- inv bst; safe_inv avl.
- apply bal_bst; auto.
- clear Hrl Hlr H13 H14 H16 H17 z; intro; intros.
- set (l:=Node ll lx lr lh) in *; clearbody l.
- rewrite (@join_in l x rl y) in H13; auto.
- intuition.
- apply MX.eq_lt with x; eauto.
- eauto.
-
- apply create_bst; auto.
-Qed.
-
-Lemma join_cardinal : forall l x r, 
- (cardinal (join l x r) <= S (cardinal l + cardinal r))%nat.
-Proof.
- join_tac; simpl; auto with arith.
- apply add_cardinal.
- destruct X.compare; simpl; auto with arith.
- 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); 
-  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 *.
- generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr).
- simpl in *; romega with *.
+ join_tac; auto; inv bst; apply bal_bst; auto; 
+ clear Hrl Hlr z; intro; intros; rewrite join_in in *.
+ intuition; [ apply MX.lt_eq with x | ]; eauto.
+ intuition; [ apply MX.eq_lt with x | ]; eauto.
 Qed.
+Hint Resolve join_bst.
 
 
 
 (** * Extraction of minimum element
 
-  morally, [remove_min] is to be applied to a non-empty tree 
+  Morally, [remove_min] is to be applied to a non-empty tree 
   [t = Node l x r h]. Since we can't deal here with [assert false] 
   for [t=Leaf], we pre-unpack [t] (and forget about [h]). 
 *)
@@ -757,75 +493,40 @@ Function remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt :=
        let (l',m) := remove_min ll lx lr in (bal l' x r, m)
   end.
 
-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.
- inv avl; simpl in *; split; auto.
- avl_nns; omega_max.
- (* l = Node *)
- inversion_clear H.
- rewrite e0 in IHp;simpl in IHp;destruct (IHp lh); auto.
- 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. 
-Proof.
- intros; destruct (@remove_min_avl_1 l x r h H); auto.
-Qed.
-
-Lemma remove_min_in : forall l x r h y, avl (Node l x r h) -> 
- (In y (Node l x r h) <-> 
-  X.eq y (remove_min l x r)#2 \/ In y (remove_min l x r)#1).
+Lemma remove_min_in : forall l x r h y, 
+ In y (Node l x r h) <-> 
+  X.eq y (remove_min l x r)#2 \/ In y (remove_min l x r)#1.
 Proof.
  intros l x r; functional induction (remove_min l x r); simpl in *; intros.
  intuition_in.
- (* l = Node *)
- inversion_clear H.
- generalize (remove_min_avl H0).
- rewrite e0; simpl; intros.
- rewrite bal_in; auto.
- rewrite e0 in IHp;generalize (IHp lh y H0).
- intuition.
- inversion_clear H7; intuition.
+ rewrite bal_in, In_node_iff, IHp, e0; simpl; intuition.
 Qed.
 
 Lemma remove_min_bst : forall l x r h, 
- bst (Node l x r h) -> avl (Node l x r h) -> bst (remove_min l x r)#1.
+ bst (Node l x r h) -> bst (remove_min l x r)#1.
 Proof.
  intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H0.
- rewrite_all e0;simpl in *.
+ inversion_clear H.
+ specialize IHp with (1:=H0); rewrite e0 in IHp; auto.
  apply bal_bst; auto.
- apply (IHp lh); auto.
- intro; intros.
- generalize (remove_min_in y H).
- rewrite e0; simpl.
- destruct 1.
- apply H3; intuition.
+ intro y; specialize (H2 y).
+ rewrite remove_min_in, e0 in H2; simpl in H2; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall l x r h, 
- bst (Node l x r h) -> avl (Node l x r h) -> 
+ bst (Node l x r h) ->
  gt_tree (remove_min l x r)#2 (remove_min l x r)#1.
 Proof.
  intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H0.
- intro; intro.
- generalize (IHp lh H1 H); clear H6 H7 IHp.
- generalize (remove_min_in m H)(remove_min_avl H).
- rewrite e0; simpl; intros.
- rewrite (bal_in x y H7 H5) in H0.
- assert (In m (Node ll lx lr lh)) by (rewrite H6; auto); clear H6.
- assert (X.lt m x) by order.
- decompose [or] H0; order.
+ inversion_clear H.
+ specialize IHp with (1:=H0); rewrite e0 in IHp; simpl in IHp.
+ intro y; rewrite bal_in; intuition; 
+  specialize (H2 m); rewrite remove_min_in, e0 in H2; simpl in H2; 
+  [ apply MX.lt_eq with x | ]; eauto.
 Qed.
+Hint Resolve remove_min_bst remove_min_gt_tree.
 
 
 
@@ -843,56 +544,28 @@ Function merge (s1 s2 :t) : t:=  match s1,s2 with
         let (s2',m) := remove_min l2 x2 r2 in bal s1 m s2'
 end.
 
-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.
+Lemma merge_in : forall s1 s2 y,
+ In y (merge s1 s2) <-> In y s1 \/ In y s2.
 Proof.
- intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
- split; auto; avl_nns; omega_max.
- split; auto; avl_nns; simpl in *; omega_max.
- destruct s1;try contradiction;clear y.
- generalize (remove_min_avl_1 H0).
- rewrite e1; simpl; destruct 1.
- split.
- apply bal_avl; auto.
- simpl; omega_max.
- omega_bal.
-Qed.
-
-Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 -> 
-  -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2).
-Proof. 
- intros; destruct (@merge_avl_1 s1 s2 H H0 H1); auto.
-Qed.
-
-Lemma merge_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
- (In y (merge s1 s2) <-> In y s1 \/ In y s2).
-Proof. 
  intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros.
  intuition_in.
  intuition_in.
- destruct s1;try contradiction;clear y.
- replace s2' with ((remove_min l2 x2 r2)#1); [|rewrite e1; auto].
- rewrite bal_in; auto.
- generalize (remove_min_in y0 H2); rewrite e1; simpl; intro.
- rewrite H3 ; intuition.
- generalize (remove_min_avl H2); rewrite e1; simpl; auto.
+ rewrite bal_in, remove_min_in, e1; simpl; intuition.
 Qed.
 
-Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma merge_bst : forall s1 s2, bst s1 -> bst s2 -> 
  (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
- bst (merge s1 s2). 
+ bst (merge s1 s2).
 Proof.
- intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto.
- destruct s1;try contradiction;clear y.
+ intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros; auto; clear y.
  apply bal_bst; auto.
- generalize (remove_min_bst H1 H2); rewrite e1; simpl in *; auto.
- intro; intro.
- apply H3; auto.
- generalize (remove_min_in m H2); rewrite e1; simpl; intuition.
- generalize (remove_min_gt_tree H1 H2); rewrite e1; simpl; auto.
-Qed. 
+ change s2' with ((s2',m)#1); rewrite <-e1; eauto.
+ intros y Hy.
+ apply H1; auto.
+ rewrite remove_min_in, e1; simpl; auto.
+ change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto.
+Qed.
+Hint Resolve merge_bst.
 
 
 
@@ -908,76 +581,33 @@ Function remove (x:elt)(s:t) { struct s } : t := match s with
       end
    end.
 
-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); subst;simpl; intros.
- intuition; omega_max.
- (* LT *)
- inv avl.
- destruct (IHt H0).
- split. 
- apply bal_avl; auto.
- omega_max.
- omega_bal.
- (* EQ *)
- inv avl. 
- generalize (merge_avl_1 H0 H1 H2).
- intuition omega_max.
- (* GT *)
- inv avl.
- destruct (IHt H1).
- split. 
- apply bal_avl; auto.
- omega_max.
- omega_bal.
-Qed.
-
-Lemma remove_avl : forall s x, avl s -> avl (remove x s).
-Proof. 
- intros; destruct (@remove_avl_1 s x H); auto.
-Qed.
-Hint Resolve remove_avl.
-
-Lemma remove_in : forall s x y, bst s -> avl s -> 
+Lemma remove_in : forall s x y, bst s ->
  (In y (remove x s) <-> ~ X.eq y x /\ In y s).
 Proof.
- intros s x; functional induction (remove x s); subst;simpl; intros.
+ intros s x; functional induction (remove x s); subst; simpl; 
+  intros; inv bst.
  intuition_in.
- (* LT *)
- inv avl; inv bst; clear e0.
- rewrite bal_in; auto.
- generalize (IHt y0 H0); intuition; [ order | order | intuition_in ].
- (* EQ *)
- inv avl; inv bst; clear e0.
- rewrite merge_in; intuition; [ order | order | intuition_in ].
- elim H9; eauto.
- (* GT *)
- inv avl; inv bst; clear e0.
- rewrite bal_in; auto.
- generalize (IHt y0 H5); intuition; [ order | order | intuition_in ].
+ rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in].
+ rewrite merge_in; clear e0; intuition; [order|order|intuition_in].
+ elim H4; eauto.
+ rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in].
 Qed.
 
-Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s).
+Lemma remove_bst : forall s x, bst s -> bst (remove x s).
 Proof. 
- intros s x; functional induction (remove x s); simpl; intros.
+ intros s x; functional induction (remove x s); simpl; 
+  intros; inv bst.
  auto.
  (* LT *)
- inv avl; inv bst.
  apply bal_bst; auto.
- intro; intro.
- rewrite (remove_in x y0 H0) in H; auto.
- destruct H; eauto.
+ intro z; rewrite remove_in; auto; destruct 1; eauto.
  (* EQ *)
- inv avl; inv bst.
- apply merge_bst; eauto.
+ eauto.
  (* GT *) 
- inv avl; inv bst.
  apply bal_bst; auto.
- intro; intro.
- rewrite (remove_in x y0 H5) in H; auto.
- destruct H; eauto.
+ intro z; rewrite remove_in; auto; destruct 1; eauto.
 Qed.
+Hint Resolve remove_bst.
 
 
 
@@ -998,7 +628,7 @@ Proof.
  destruct l; auto.
 Qed.
 
-Lemma min_elt_2 : forall s x y, bst s -> 
+Lemma min_elt_2 : forall s x y, bst s ->
  min_elt s = Some x -> In y s -> ~ X.lt y x. 
 Proof.
  intro s; functional induction (min_elt s); subst;simpl.
@@ -1088,11 +718,11 @@ Proof.
  exact min_elt_3.
 Qed.
 
-Lemma choose_3 : forall s s', bst s -> avl s -> bst s' -> avl s' -> 
+Lemma choose_3 : forall s s', bst s -> bst s' -> 
  forall x x', choose s = Some x -> choose s' = Some x' -> 
   Equal s s' -> X.eq x x'.
 Proof.
- unfold choose, Equal; intros s s' Hb Ha Hb' Ha' x x' Hx Hx' H.
+ unfold choose, Equal; intros s s' Hb Hb' x x' Hx Hx' H.
  assert (~X.lt x x').
   apply min_elt_2 with s'; auto.
   rewrite <-H; auto using min_elt_1.
@@ -1118,45 +748,28 @@ Function concat (s1 s2 : t) : t  :=
             join s1 m s2'
    end.
 
-Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
+Lemma concat_in : forall s1 s2 y, 
+ In y (concat s1 s2) <-> In y s1 \/ In y s2.
 Proof.
- intros s1 s2; functional induction (concat s1 s2); subst;auto.
- destruct s1;try contradiction;clear y.
- intros; apply join_avl; auto.
- generalize (remove_min_avl H0); rewrite e1; simpl; auto.
+ intros s1 s2; functional induction (concat s1 s2);subst;simpl;intros.
+ intuition_in.
+ intuition_in.
+ rewrite join_in, remove_min_in, e1; simpl; intuition.
 Qed.
  
-Lemma concat_bst :   forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma concat_bst :   forall s1 s2, bst s1 -> bst s2 -> 
  (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (concat s1 s2).
 Proof. 
- intros s1 s2; functional induction (concat s1 s2); subst ;auto.
- destruct s1;try contradiction;clear y. 
- intros;  apply join_bst; auto.
- generalize (remove_min_bst H1 H2); rewrite e1; simpl; auto.
- generalize (remove_min_avl H2); rewrite e1; simpl; auto.
- generalize (remove_min_in m H2); rewrite e1; simpl; auto.
- destruct 1; intuition.
- generalize (remove_min_gt_tree H1 H2); rewrite e1; simpl; auto.
+ intros s1 s2; functional induction (concat s1 s2); subst; auto; clear y.
+ intros; apply join_bst; auto.
+ change (bst (s2',m)#1); rewrite <-e1; eauto.
+ intros y Hy.
+ apply H1; auto.
+ rewrite remove_min_in, e1; simpl; auto.
+ change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto.
 Qed.
-
-Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
- (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
- (In y (concat s1 s2) <-> In y s1 \/ In y s2).
-Proof.
- intros s1 s2; functional induction (concat s1 s2);subst;simpl.
- intuition.
- inversion_clear H5.
- destruct s1;try contradiction;clear y;intuition.
- inversion_clear H5.
- destruct s1;try contradiction;clear y; intros. 
- rewrite (@join_in _ m s2' y H0).
- generalize (remove_min_in y H2); rewrite e1; simpl.
- intro EQ; rewrite EQ; intuition.
- generalize (remove_min_avl H2); rewrite e1; simpl; auto.
-Qed.
-
-Hint Resolve concat_avl concat_bst.
+Hint Resolve concat_bst.
 
 
 
@@ -1182,118 +795,51 @@ Function split (x:elt)(s:t) { struct s } : t * (bool * t) := match s with
      end
  end.
 
-Lemma split_avl : forall s x, avl s -> 
-  avl (split x s)#1 /\ avl (split x s)#2#2.
-Proof. 
- intros s x; functional induction (split x s);subst;simpl in *.
- auto.
- rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
- simpl; inversion_clear 1; auto.
- rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
-Qed.
-
-Lemma split_in_1 : forall s x y, bst s -> avl s -> 
+Lemma split_in_1 : forall s x y, bst s -> 
  (In y (split x s)#1 <-> In y s /\ X.lt y x).
-Proof. 
- intros s x; functional induction (split x s);subst;simpl in *.
- intuition; try inversion_clear H1.
- (* LT *)
- rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear  H7 H6.
- rewrite (IHp y0 H0 H4); clear IHp e0.
- intuition.
- inversion_clear H6; auto; order.
- (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0.
- intuition.
- order.
+Proof.
+ intros s x; functional induction (split x s); subst; simpl; intros; 
+  inv bst; try clear e0.
+ intuition_in.
+ rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
  intuition_in; order.
- (* GT *)
- rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
- rewrite join_in; auto.
- rewrite (IHp y0 H1 H5); clear e1.
- intuition; [ eauto | eauto | intuition_in ].
- generalize (split_avl x H5); rewrite e1; simpl; intuition.
+ rewrite join_in.
+ rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
 Qed.
 
-Lemma split_in_2 : forall s x y, bst s -> avl s -> 
+Lemma split_in_2 : forall s x y, bst s -> 
  (In y (split x s)#2#2 <-> In y s /\ X.lt x y).
 Proof. 
- intros s x; functional induction (split x s);subst;simpl in *.
- intuition; try inversion_clear H1.
- (* LT *)
- rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
- rewrite join_in; auto.
- rewrite (IHp y0 H0 H4); clear IHp e0.
- intuition; [ order | order | intuition_in ].
- generalize (split_avl x H4); rewrite e1; simpl; intuition.
- (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0.
- intuition; [ order | intuition_in; order ]. 
- (* GT *)
- rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
- rewrite (IHp y0 H1 H5); clear IHp e0.
- intuition; intuition_in; order. 
+ intros s x; functional induction (split x s); subst; simpl; intros; 
+  inv bst; try clear e0.
+ intuition_in.
+ rewrite join_in.
+ rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ intuition_in; order.
+ rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
 Qed.
 
-Lemma split_in_3 : forall s x, bst s -> avl s -> 
+Lemma split_in_3 : forall s x, bst s -> 
  ((split x s)#2#1 = true <-> In x s).
 Proof. 
- intros s x; functional induction (split x s);subst;simpl in *.
- intuition; try inversion_clear H1.
- (* LT *)
- rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
- rewrite IHp; auto.
- intuition_in; absurd (X.lt x y); eauto.
- (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; intuition.
- (* GT *)
- rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
- rewrite IHp; auto.
- intuition_in; absurd (X.lt y x); eauto.
+ intros s x; functional induction (split x s); subst; simpl; intros; 
+  inv bst; try clear e0.
+ intuition_in; try discriminate.
+ rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ intuition.
+ rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
 Qed.
 
-Lemma split_bst : forall s x, bst s -> avl s -> 
+Lemma split_bst : forall s x, bst s -> 
  bst (split x s)#1 /\ bst (split x s)#2#2.
 Proof. 
- intros s x; functional induction (split x s);subst;simpl in *.  
- intuition.
- (* LT *)
- rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
- intuition.
- apply join_bst; auto.
- generalize (split_avl x H4); rewrite e1; simpl; intuition.
- intro; intro.
- generalize (split_in_2 x y0 H0 H4); rewrite e1; simpl; intuition.
- (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; intuition.
- (* GT *)
- rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
- intuition.
- apply join_bst; auto.
- generalize (split_avl x H5); rewrite e1; simpl; intuition.
- intro; intro.
- generalize (split_in_1 x y0 H1 H5); rewrite e1; simpl; intuition.
-Qed.
-
-Lemma split_cardinal_1 : forall x s, 
- (cardinal (split x s)#1 <= cardinal s)%nat.
-Proof.
- intros x s; functional induction split x s; simpl; auto.
- rewrite e1 in IHp; simpl in *.
- romega with *.
- romega with *.
- rewrite e1 in IHp; simpl in *.
- generalize (@join_cardinal l y rl); romega with *.
-Qed.
-
-Lemma split_cardinal_2 : forall x s, 
- (cardinal (split x s)#2#2 <= cardinal s)%nat.
-Proof.
- intros x s; functional induction split x s; simpl; auto.
- rewrite e1 in IHp; simpl in *.
- generalize (@join_cardinal rl y r); romega with *.
- romega with *.
- rewrite e1 in IHp; simpl in *; romega with *.
+ intros s x; functional induction (split x s); subst; simpl; intros; 
+  inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition;
+  apply join_bst; auto.
+ intros y0.
+ generalize (split_in_2 x y0 H0); rewrite e1; simpl; intuition.
+ intros y0.
+ generalize (split_in_1 x y0 H1); rewrite e1; simpl; intuition.
 Qed.
 
 
@@ -1310,57 +856,45 @@ Function inter (s1 s2 : t) { struct s1 } : t := match s1, s2 with
             end
     end.
 
-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; 
- inv avl; auto.
-Qed.
-Hint Resolve inter_avl.
-
-Lemma inter_bst_in : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma inter_bst_in : forall s1 s2, bst s1 -> bst s2 -> 
  bst (inter s1 s2) /\ (forall y, In y (inter s1 s2) <-> In y s1 /\ In y s2).
 Proof.
- intros s1 s2; functional induction inter s1 s2; intros B1 A1 B2 A2; 
+ intros s1 s2; functional induction inter s1 s2; intros B1 B2; 
  [intuition_in|intuition_in | | ]; 
  set (r:=Node l2 x2 r2 h2) in *; 
- generalize (split_avl x1 A2)(split_bst x1 B2 A2); 
-  rewrite e1; simpl; destruct 1; destruct 1; 
- inv avl; inv bst; 
+ generalize (split_bst x1 B2); 
+  rewrite e1; simpl; destruct 1; inv bst; 
  destruct IHt as (IHb1,IHi1); auto; 
  destruct IHt0 as (IHb2,IHi2); auto; 
- destruct (distr_pair e1); clear e1; 
- destruct (distr_pair H12); clear H12; split.
+ destruct (distr_pair e1); clear e1;
+ destruct (distr_pair H6); clear H6; split.
  (* bst join *)
  apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition.
  (* In join *)
- intros; rewrite join_in; auto; rewrite IHi1; rewrite IHi2.
- rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto.
- rewrite split_in_3 in H13; intuition_in.
+ intros.
+ rewrite join_in, IHi1, IHi2, <- H5, <- H8, split_in_1, split_in_2; auto.
+ rewrite split_in_3 in H7; intuition_in.
  apply In_1 with x1; auto.
  (* bst concat *)
  apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* In concat *)
- intros; rewrite concat_in; auto.
- rewrite IHi1; rewrite IHi2.
- rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto.
- assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto).
+ intros.
+ rewrite concat_in, IHi1, IHi2, <- H5, <- H8, split_in_1, split_in_2; auto.
+ assert (~In x1 r) by (rewrite <- split_in_3, H7; auto).
  intuition_in.
- elim H12.
+ elim H6.
  apply In_1 with y; auto.
- intros y1 y2; rewrite IHi1, IHi2; intuition; order.
 Qed.
 
-Lemma inter_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
- bst (inter s1 s2). 
+Lemma inter_in : forall s1 s2 y, bst s1 -> bst s2 -> 
+ (In y (inter s1 s2) <-> In y s1 /\ In y s2).
 Proof. 
- intros s1 s2 B1 A1 B2 A2; destruct (inter_bst_in B1 A1 B2 A2); auto.
+ intros s1 s2 y B1 B2; destruct (inter_bst_in B1 B2); auto.
 Qed.
 
-Lemma inter_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
- (In y (inter s1 s2) <-> In y s1 /\ In y s2).
+Lemma inter_bst : forall s1 s2, bst s1 -> bst s2 -> bst (inter s1 s2).
 Proof. 
- intros s1 s2 y B1 A1 B2 A2; destruct (inter_bst_in B1 A1 B2 A2); auto.
+ intros s1 s2 B1 B2; destruct (inter_bst_in B1 B2); auto.
 Qed.
 
 
@@ -1377,173 +911,95 @@ Function diff (s1 s2 : t) { struct s1 } : t := match s1, s2 with
     end
 end.
 
-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; 
- inv avl; auto.
-Qed.
-Hint Resolve diff_avl.
-
-Lemma diff_bst_in : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
+Lemma diff_bst_in : forall s1 s2, bst s1 -> bst s2 -> 
  bst (diff s1 s2) /\ (forall y, In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
 Proof.
- intros s1 s2; functional induction diff s1 s2; intros B1 A1 B2 A2; 
+ intros s1 s2; functional induction diff s1 s2; intros B1 B2; 
  [intuition_in|intuition_in | | ]; 
  set (r:=Node l2 x2 r2 h2) in *; 
- generalize (split_avl x1 A2)(split_bst x1 B2 A2); 
-  rewrite e1; simpl; destruct 1; destruct 1; 
+ generalize (split_bst x1 B2); 
+  rewrite e1; simpl; destruct 1; 
  inv avl; inv bst; 
  destruct IHt as (IHb1,IHi1); auto; 
  destruct IHt0 as (IHb2,IHi2); auto; 
  destruct (distr_pair e1); clear e1; 
- destruct (distr_pair H12); clear H12; split.
+ destruct (distr_pair H6); clear H6; split.
  (* bst concat *)
  apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* In concat *)
- intros; rewrite concat_in; auto.
- rewrite IHi1; rewrite IHi2.
- rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto.
- rewrite split_in_3 in H13; intuition_in.
- elim H17.
+ intros.
+ rewrite concat_in, IHi1, IHi2, <-H5, <- H8, split_in_1, split_in_2; auto.
+ rewrite split_in_3 in H7; intuition_in.
+ elim H10.
  apply In_1 with x1; auto.
- intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* bst join *)
  apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition.
  (* In join *)
- intros; rewrite join_in; auto; rewrite IHi1; rewrite IHi2.
- rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto.
- assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto).
+ intros.
+ rewrite join_in, IHi1, IHi2, <-H5, <-H8, split_in_1, split_in_2; auto.
+ assert (~In x1 r) by (rewrite <- split_in_3, H7; auto).
  intuition_in.
- elim H12.
+ elim H6.
  apply In_1 with y; auto.
 Qed.
 
-Lemma diff_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
- bst (diff s1 s2). 
+Lemma diff_in : forall s1 s2 y, bst s1 -> bst s2 -> 
+ (In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
 Proof. 
- intros s1 s2 B1 A1 B2 A2; destruct (diff_bst_in B1 A1 B2 A2); auto.
+ intros s1 s2 y B1 B2; destruct (diff_bst_in B1 B2); auto.
 Qed.
 
-Lemma diff_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
- (In y (diff s1 s2) <-> In y s1 /\ ~In y s2).
+Lemma diff_bst : forall s1 s2, bst s1 -> bst s2 -> bst (diff s1 s2). 
 Proof. 
- intros s1 s2 y B1 A1 B2 A2; destruct (diff_bst_in B1 A1 B2 A2); auto.
+ intros s1 s2 B1 B2; destruct (diff_bst_in B1 B2); auto.
 Qed.
 
 
 
 (** * Union *)
 
-Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat.
-
-Ltac 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); 
-  rewrite H; simpl; romega with *
- end.
+(** In ocaml, heights of [s1] and [s2] are compared each time in order
+   to recursively perform the split on the smaller set.
+   Unfortunately, this leads to a non-structural algorithm. The
+   following code is a simplification of the ocaml version: no
+   comparison of heights. It might be slightly slower, but
+   experimentally all the tests I've made in ocaml have shown this
+   potential slowdown to be non-significant. Anyway, the exact code
+   of ocaml has also been formalized thanks to Function+measure, see
+   [ocaml_union] in [FSetFullAVL].  
+*)
 
-Function union (s : t * t) { measure cardinal2 s } : t  :=
- 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) => 
-        if ge_lt_dec h1 h2 then
-          if eq_dec h2 1 then add x2 s#1 else
-          let (l2',r2') := split x1 s#2 in 
-             join (union (l1,l2')) x1 (union (r1,r2'#2))
-        else
-          if eq_dec h1 1 then add x1 s#2 else
-          let (l1',r1') := split x2 s#1 in 
-             join (union (l1',l2)) x2 (union (r1'#2,r2))
+Function union (s1 s2 : t) { struct s1 } : t := 
+ match s1, s2 with 
+  | Leaf, _ => s2
+  | Node _ _ _ _, Leaf => s1
+  | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => 
+     let (l2',r2') := split x1 s2 in 
+     join (union l1 l2') x1 (union r1 r2'#2)
  end.
-Proof.
-abstract union_tac.
-abstract union_tac.
-abstract union_tac.
-abstract union_tac.
-Defined.
-
-Lemma union_avl : forall s, 
- avl s#1 -> avl s#2 -> avl (union s).
-Proof.
- intros s; functional induction 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.
- intros A1 A2; generalize (split_avl x2 A1); rewrite e2; simpl.
- inv avl; destruct 1; auto.
-Qed.
-Hint Resolve union_avl.
 
-Lemma union_in : forall s y, 
- bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> 
- (In y (union s) <-> In y s#1 \/ In y s#2).
+Lemma union_in : forall s1 s2 y, bst s1 -> bst s2 -> 
+ (In y (union s1 s2) <-> In y s1 \/ In y s2).
 Proof.
- intros s; functional induction union s; intros y B1 A1 B2 A2; 
-  simpl fst in *; simpl snd in *; try clear e0 e1.
+ intros s1 s2; functional induction union s1 s2; intros y B1 B2.
  intuition_in.
  intuition_in.
- intuition_in.
- (* add x2 s#1 *)
- inv avl.
- rewrite (height_0 H); [ | avl_nn l2; omega_max].
- rewrite (height_0 H0); [ | avl_nn r2; omega_max].
- rewrite add_in; auto; intuition_in.
- (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *)
- generalize 
-  (split_avl x1 A2) (split_bst x1 B2 A2)
-  (split_in_1 x1 y B2 A2) (split_in_2 x1 y B2 A2).
- rewrite e2; simpl.
- destruct 1; destruct 1; inv avl; inv bst.
- rewrite join_in; auto.
- rewrite IHt; auto.
- rewrite IHt0; auto.
+ generalize (split_bst x1 B2) (split_in_1 x1 y B2) (split_in_2 x1 y B2).
+ rewrite e1; simpl.
+ destruct 1; inv bst.
+ rewrite join_in, IHt, IHt0; auto.
  do 2 (intro Eq; rewrite Eq; clear Eq).
  case (X.compare y x1); intuition_in.
- (* add x1 s#2 *)
- inv avl.
- rewrite (height_0 H3); [ | avl_nn l1; omega_max].
- rewrite (height_0 H4); [ | avl_nn r1; omega_max].
- rewrite add_in; auto; intuition_in.
- (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *)
- generalize 
-  (split_avl x2 A1) (split_bst x2 B1 A1)
-  (split_in_1 x2 y B1 A1) (split_in_2 x2 y B1 A1).
- rewrite e2; simpl.
- destruct 1; destruct 1; inv avl; inv bst.
- rewrite join_in; auto.
- rewrite IHt; auto.
- rewrite IHt0; auto.
- do 2 (intro Eq; rewrite Eq; clear Eq).
- case (X.compare y x2); intuition_in.
 Qed.
 
-Lemma union_bst : forall s,
- bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (union s).
+Lemma union_bst : forall s1 s2, bst s1 -> bst s2 -> 
+ bst (union s1 s2).
 Proof.
- intros s; functional induction union s; intros B1 A1 B2 A2;
-  simpl fst in *; simpl snd in *; try clear e0 e1; 
-  try apply add_bst; auto.
- (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *)
- generalize (split_avl x1 A2) (split_bst x1 B2 A2).
- rewrite e2; simpl.
- destruct 1; destruct 1.
- destruct (distr_pair e2) as (L,R); clear e2.
- inv bst; inv avl.
- apply join_bst; auto.
- intro y; rewrite union_in; auto; simpl.
- rewrite <- L, split_in_1; auto; intuition_in.
- intro y; rewrite union_in; auto; simpl.
- rewrite <- R, split_in_2; auto; intuition_in.
- (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *)
- generalize (split_avl x2 A1) (split_bst x2 B1 A1).
- rewrite e2; simpl.
- destruct 1; destruct 1.
- destruct (distr_pair e2) as (L,R); clear e2.
- inv bst; inv avl.
+ intros s1 s2; functional induction union s1 s2; intros B1 B2; auto.
+ generalize (split_bst x1 B2) .
+ inv bst.
+ rewrite e1; simpl; destruct 1.
+ destruct (distr_pair e1) as (L,R); clear e1.
  apply join_bst; auto.
  intro y; rewrite union_in; auto; simpl.
  rewrite <- L, split_in_1; auto; intuition_in.
@@ -1644,65 +1100,43 @@ Fixpoint filter_acc (acc:t)(s:t) { struct s } : t := match s with
 
 Definition filter := filter_acc Leaf. 
 
-Lemma filter_acc_avl : forall s acc, avl s -> avl acc -> 
- avl (filter_acc acc s).
-Proof.
- induction s; simpl; auto.
- intros.
- inv avl.
- apply IHs2; auto.
- apply IHs1; auto.
- destruct (f t); auto.
-Qed. 
-Hint Resolve filter_acc_avl.
-
-Lemma filter_acc_bst : forall s acc, bst s -> avl s -> bst acc -> avl acc -> 
- bst (filter_acc acc s).
-Proof.
- induction s; simpl; auto.
- intros.
- inv avl; inv bst.
- destruct (f t); auto.
- apply IHs2; auto.
- apply IHs1; auto.
- apply add_bst; auto.
-Qed. 
-
-Lemma filter_acc_in : forall s acc, avl s -> avl acc -> 
+Lemma filter_acc_in : forall s acc, 
  compat_bool X.eq f -> forall x : elt, 
  In x (filter_acc acc s) <-> In x acc \/ In x s /\ f x = true.
 Proof.  
  induction s; simpl; intros.
  intuition_in.
- inv bst; inv avl.
- rewrite IHs2 by (destruct (f t); auto).
- rewrite IHs1 by (destruct (f t); auto).
+ rewrite IHs2, IHs1 by (destruct (f t); auto).
  case_eq (f t); intros.
  rewrite (add_in); auto.
  intuition_in.
- rewrite (H1 _ _ H8).
+ rewrite (H _ _ H2).
  intuition.
  intuition_in.
- rewrite (H1 _ _ H8) in H9.
- rewrite H in H9; discriminate.
-Qed. 
-
-Lemma filter_avl : forall s, avl s -> avl (filter s). 
-Proof.
- unfold filter; intros; apply filter_acc_avl; auto.
+ rewrite (H _ _ H2) in H3.
+ rewrite H0 in H3; discriminate.
 Qed.
 
-Lemma filter_bst : forall s, bst s -> avl s -> bst (filter s). 
+Lemma filter_acc_bst : forall s acc, bst s -> bst acc -> 
+ bst (filter_acc acc s).
 Proof.
- unfold filter; intros; apply filter_acc_bst; auto.
+ induction s; simpl; auto.
+ intros.
+ inv bst.
+ destruct (f t); auto.
 Qed.
 
-Lemma filter_in : forall s, avl s -> 
+Lemma filter_in : forall s,
  compat_bool X.eq f -> forall x : elt, 
  In x (filter s) <-> In x s /\ f x = true.
 Proof.
  unfold filter; intros; rewrite filter_acc_in; intuition_in.
-Qed. 
+Qed.
+
+Lemma filter_bst : forall s, bst s -> bst (filter s). 
+Proof.
+ unfold filter; intros; apply filter_acc_bst; auto.
+Qed.
 
 
 
@@ -1720,62 +1154,7 @@ Fixpoint partition_acc (acc : t*t)(s : t) { struct s } : t*t :=
 
 Definition partition := partition_acc (Leaf,Leaf).
 
-Lemma partition_acc_avl_1 : forall s acc, avl s -> 
- avl acc#1 -> avl (partition_acc acc s)#1.
-Proof.
- induction s; simpl; auto.
- destruct acc as [acct accf]; simpl in *.
- intros.
- inv avl.
- apply IHs2; auto.
- apply IHs1; auto.
- destruct (f t); simpl; auto.
-Qed. 
-
-Lemma partition_acc_avl_2 : forall s acc, avl s -> 
- avl acc#2 -> avl (partition_acc acc s)#2.
-Proof.
- induction s; simpl; auto.
- destruct acc as [acct accf]; simpl in *.
- intros.
- inv avl.
- apply IHs2; auto.
- apply IHs1; auto.
- destruct (f t); simpl; auto.
-Qed. 
-Hint Resolve partition_acc_avl_1 partition_acc_avl_2.
-
-Lemma partition_acc_bst_1 : forall s acc, bst s -> avl s -> 
- bst acc#1 -> avl acc#1 -> 
- bst (partition_acc acc s)#1.
-Proof.
- induction s; simpl; auto.
- destruct acc as [acct accf]; simpl in *.
- intros.
- inv avl; inv bst.
- destruct (f t); auto.
- apply IHs2; simpl; auto.
- apply IHs1; simpl; auto.
- apply add_bst; auto.
- apply partition_acc_avl_1; simpl; auto.
-Qed. 
-
-Lemma partition_acc_bst_2 : forall s acc, bst s -> avl s -> 
- bst acc#2 -> avl acc#2 -> 
- bst (partition_acc acc s)#2.
-Proof.
- induction s; simpl; auto.
- destruct acc as [acct accf]; simpl in *.
- intros.
- inv avl; inv bst.
- destruct (f t); auto.
- apply IHs2; simpl; auto.
- apply IHs1; simpl; auto.
- apply add_bst; auto.
- apply partition_acc_avl_2; simpl; auto.
-Qed. 
-
-Lemma partition_acc_in_1 : forall s acc, avl s -> avl acc#1 -> 
+Lemma partition_acc_in_1 : forall s acc, 
  compat_bool X.eq f -> forall x : elt, 
  In x (partition_acc acc s)#1 <-> 
  In x acc#1 \/ In x s /\ f x = true.
@@ -1783,21 +1162,20 @@ Proof.
  induction s; simpl; intros.
  intuition_in.
  destruct acc as [acct accf]; simpl in *.
- inv bst; inv avl.
  rewrite IHs2 by 
   (destruct (f t); auto; apply partition_acc_avl_1; simpl; auto).
  rewrite IHs1 by (destruct (f t); simpl; auto).
  case_eq (f t); simpl; intros.
  rewrite (add_in); auto.
  intuition_in.
- rewrite (H1 _ _ H8).
+ rewrite (H _ _ H2).
  intuition.
  intuition_in.
- rewrite (H1 _ _ H8) in H9.
- rewrite H in H9; discriminate.
+ rewrite (H _ _ H2) in H3.
+ rewrite H0 in H3; discriminate.
 Qed.
 
-Lemma partition_acc_in_2 : forall s acc, avl s -> avl acc#2 -> 
+Lemma partition_acc_in_2 : forall s acc, 
  compat_bool X.eq f -> forall x : elt, 
  In x (partition_acc acc s)#2 <-> 
  In x acc#2 \/ In x s /\ f x = false.
@@ -1805,44 +1183,21 @@ Proof.
  induction s; simpl; intros.
  intuition_in.
  destruct acc as [acct accf]; simpl in *.
- inv bst; inv avl.
  rewrite IHs2 by 
   (destruct (f t); auto; apply partition_acc_avl_2; simpl; auto).
  rewrite IHs1 by (destruct (f t); simpl; auto).
  case_eq (f t); simpl; intros.
  intuition.
  intuition_in.
- rewrite (H1 _ _ H8) in H9.
- rewrite H in H9; discriminate.
+ rewrite (H _ _ H2) in H3.
+ rewrite H0 in H3; discriminate.
  rewrite (add_in); auto.
  intuition_in.
- rewrite (H1 _ _ H8).
+ rewrite (H _ _ H2).
  intuition.
-Qed. 
-
-Lemma partition_avl_1 : forall s, avl s -> avl (partition s)#1. 
-Proof.
- unfold partition; intros; apply partition_acc_avl_1; auto.
-Qed.
-
-Lemma partition_avl_2 : forall s, avl s -> avl (partition s)#2. 
-Proof.
- unfold partition; intros; apply partition_acc_avl_2; auto.
-Qed.
-
-Lemma partition_bst_1 : forall s, bst s -> avl s -> 
- bst (partition s)#1. 
-Proof.
- unfold partition; intros; apply partition_acc_bst_1; auto.
 Qed.
 
-Lemma partition_bst_2 : forall s, bst s -> avl s -> 
- bst (partition s)#2. 
-Proof.
- unfold partition; intros; apply partition_acc_bst_2; auto.
-Qed.
-
-Lemma partition_in_1 : forall s, avl s -> 
+Lemma partition_in_1 : forall s, 
  compat_bool X.eq f -> forall x : elt, 
  In x (partition s)#1 <-> In x s /\ f x = true.
 Proof.
@@ -1850,7 +1205,7 @@ Proof.
  simpl in *; intuition_in.
 Qed. 
 
-Lemma partition_in_2 : forall s, avl s -> 
+Lemma partition_in_2 : forall s,
  compat_bool X.eq f -> forall x : elt, 
  In x (partition s)#2 <-> In x s /\ f x = false.
 Proof.
@@ -1858,6 +1213,40 @@ Proof.
  simpl in *; intuition_in.
 Qed. 
 
+Lemma partition_acc_bst_1 : forall s acc, bst s -> bst acc#1 -> 
+ bst (partition_acc acc s)#1.
+Proof.
+ induction s; simpl; auto.
+ destruct acc as [acct accf]; simpl in *.
+ intros.
+ inv bst.
+ destruct (f t); auto.
+ apply IHs2; simpl; auto.
+ apply IHs1; simpl; auto.
+Qed.
+
+Lemma partition_acc_bst_2 : forall s acc, bst s -> bst acc#2 -> 
+ bst (partition_acc acc s)#2.
+Proof.
+ induction s; simpl; auto.
+ destruct acc as [acct accf]; simpl in *.
+ intros.
+ inv bst.
+ destruct (f t); auto.
+ apply IHs2; simpl; auto.
+ apply IHs1; simpl; auto.
+Qed.
+
+Lemma partition_bst_1 : forall s, bst s -> bst (partition s)#1. 
+Proof.
+ unfold partition; intros; apply partition_acc_bst_1; auto.
+Qed.
+
+Lemma partition_bst_2 : forall s, bst s -> bst (partition s)#2. 
+Proof.
+ unfold partition; intros; apply partition_acc_bst_2; auto.
+Qed.
+
 
 
 (** * [for_all] and [exists] *)
@@ -1976,56 +1365,141 @@ Qed.
 
 (** * Subset *)
 
-Function subset (s:t*t) { measure cardinal2 s } : bool := 
- match s with 
-  | (Leaf, _) => true
-  | (Node _ _ _ _, Leaf) => false
-  | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => 
+(** In ocaml, recursive calls are made on "half-trees" such as 
+   (Node l1 x1 Leaf _) and (Node Leaf x1 r1 _). Instead of these
+   non-structural calls, we propose here two specialized functions for
+   these situations. This version should be almost as efficient as 
+   the one of ocaml (closures as arguments may slow things a bit),  
+   it is simply less compact. The exact ocaml version has also been
+   formalized (thanks to Function+measure), see [ocaml_subset] in 
+   [FSetFullAVL].
+ *)
+
+Fixpoint subsetl (subset_l1:t->bool) x1 s2 : bool := 
+ match s2 with 
+  | Leaf => false
+  | Node l2 x2 r2 h2 => 
+     match X.compare x1 x2 with 
+      | EQ _ => subset_l1 l2 
+      | LT _ => subsetl subset_l1 x1 l2
+      | GT _ => mem x1 r2 && subset_l1 s2
+     end
+ end.
+
+Fixpoint subsetr (subset_r1:t->bool) x1 s2 : bool := 
+ match s2 with 
+  | Leaf => false
+  | Node l2 x2 r2 h2 => 
+     match X.compare x1 x2 with 
+      | EQ _ => subset_r1 r2 
+      | LT _ => mem x1 l2 && subset_r1 s2
+      | GT _ => subsetr subset_r1 x1 r2
+     end
+ end.
+
+Fixpoint subset s1 s2 : bool := match s1, s2 with 
+  | Leaf, _ => true
+  | Node _ _ _ _, Leaf => false
+  | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => 
      match X.compare x1 x2 with 
-      | EQ _ => subset (l1,l2) && subset (r1,r2)
-      | LT _ => subset (Node l1 x1 Leaf 0, l2) && subset (r1,s#2)
-      | GT _ => subset (Node Leaf x1 r1 0, r2) && subset (l1,s#2)
+      | EQ _ => subset l1 l2 && subset r1 r2
+      | LT _ => subsetl (subset l1) x1 l2 && subset r1 s2
+      | GT _ => subsetr (subset r1) x1 r2 && subset l1 s2
      end
  end.
 
+Lemma subsetl_12 : forall subset_l1 l1 x1 h1 s2,
+ bst (Node l1 x1 Leaf h1) -> bst s2 ->
+ (forall s, bst s -> (subset_l1 s = true <-> Subset l1 s)) -> 
+ (subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ).
 Proof.
- intros; unfold cardinal2; simpl; abstract romega with *.
- intros; unfold cardinal2; simpl; abstract romega with *.
- intros; unfold cardinal2; simpl; abstract romega with *.
- intros; unfold cardinal2; simpl; abstract romega with *.
- intros; unfold cardinal2; simpl; abstract romega with *.
- intros; unfold cardinal2; simpl; abstract romega with *.
-Defined.
+ induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
+ unfold Subset; intuition; try discriminate.
+ assert (H': In x1 Leaf) by auto; inversion H'.
+ inversion_clear H0.
+ specialize (IHl2 H H2 H1).
+ specialize (IHr2 H H3 H1).
+ inv bst. clear H8.
+ destruct X.compare.
+ 
+ rewrite IHl2; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 
-Lemma subset_12 : forall s, 
- bst s#1 -> bst s#2 ->
- (Subset s#1 s#2 <-> subset s = true).
+ rewrite H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (H':=mem_2 H6); apply In_1 with x1; auto.
+ apply mem_1; auto.
+ assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+Qed.
+
+
+Lemma subsetr_12 : forall subset_r1 r1 x1 h1 s2,
+ bst (Node Leaf x1 r1 h1) -> bst s2 ->
+ (forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) -> 
+ (subsetr subset_r1 x1 s2 = true <-> Subset (Node Leaf x1 r1 h1) s2).
 Proof.
- intros s; functional induction subset s; simpl;
-  intros B1 B2; try clear e0.
- intuition.
- red; auto; inversion 1.
- split; intros; try discriminate.
- assert (H': In _x0 Leaf) by auto; inversion H'.
- (**)
- simpl in *; inv bst.
- rewrite andb_true_iff.
- rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0.
+ induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
+ unfold Subset; intuition; try discriminate.
+ assert (H': In x1 Leaf) by auto; inversion H'.
+ inversion_clear H0.
+ specialize (IHl2 H H2 H1).
+ specialize (IHr2 H H3 H1).
+ inv bst. clear H7.
+ destruct X.compare.
+
+ rewrite andb_true_iff, H1 by auto;  clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (H':=mem_2 H1); apply In_1 with x1; auto.
+ apply mem_1; auto.
+ assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ 
+ rewrite IHr2; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+Qed.
+
+
+Lemma subset_12 : forall s1 s2, bst s1 -> bst s2 -> 
+ (subset s1 s2 = true <-> Subset s1 s2).
+Proof.
+ induction s1 as [|l1 IHl1 x1 r1 IHr1 h1]; simpl; intros.
+ unfold Subset; intuition_in.
+ destruct s2 as [|l2 x2 r2 h2]; simpl; intros.
+ unfold Subset; intuition_in; try discriminate.
+ assert (H': In x1 Leaf) by auto; inversion H'.
+ inv bst.
+ destruct X.compare.
+
+ rewrite andb_true_iff, IHr1 by auto.
+ rewrite (@subsetl_12 (subset l1) l1 x1 h1) by auto.
+ clear IHl1 IHr1.
  unfold Subset; intuition_in.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- assert (X.eq a x2) by order; intuition_in.
- (**)
- simpl in *; inv bst.
- rewrite andb_true_iff.
- rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0.
+
+ rewrite andb_true_iff, IHl1, IHr1 by auto.
+ clear IHl1 IHr1.
  unfold Subset; intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- (**)
- simpl in *; inv bst.
- rewrite andb_true_iff.
- rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0.
+ 
+ rewrite andb_true_iff, IHl1 by auto.
+ rewrite (@subsetr_12 (subset r1) r1 x1 h1) by auto.
+ clear IHl1 IHr1.
  unfold Subset; intuition_in.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
@@ -2037,8 +1511,6 @@ Qed.
 
 (** ** Relations [eq] and [lt] over trees *)
 
-(* NB: Don't use name eq yet otherwise Function won't work *)
-
 Lemma eq_refl : forall s : t, Equal s s. 
 Proof.
  unfold Equal; intuition.
@@ -2081,8 +1553,28 @@ Proof.
  apply L.lt_not_eq with (s := elements s) (s' := elements s'); auto.
 Qed.
 
+Lemma L_eq_cons :
+ forall (l1 l2 : list elt) (x y : elt),
+ X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2).
+Proof.
+ unfold L.eq, L.Equal in |- *; intuition.
+ inversion_clear H1; generalize (H0 a); clear H0; intuition.
+ apply InA_eqA with x; eauto.
+ inversion_clear H1; generalize (H0 a); clear H0; intuition.
+ apply InA_eqA with y; eauto.
+Qed.
+Hint Resolve L_eq_cons.
+
 
-(** * A new comparison algorithm suggested by Xavier Leroy *)
+(** * A new comparison algorithm suggested by Xavier Leroy
+
+    Transformation in C.P.S. suggested by Benjamin Grégoire.
+    The original ocaml code (with non-structural recursive calls)
+    has also been formalized (thanks to Function+measure), see
+    [ocaml_compare] in [FSetFullAVL]. The following code with 
+    continuations computes dramatically faster in Coq, and 
+    should be almost as efficient after extraction.
+*)
 
 (** ** Enumeration of the elements of a tree *)
 
@@ -2116,80 +1608,49 @@ Inductive sorted_e : enumeration -> Prop :=
   | SortedEEnd : sorted_e End
   | SortedEMore :
       forall (x : elt) (s : tree) (e : enumeration),
-      bst s ->
-      (gt_tree x s) ->
-      sorted_e e ->
-      (forall y : elt, In_e y e -> X.lt x y) ->
-      (forall y : elt,
-       In y s -> forall z : elt, In_e z e -> X.lt y z) ->
+      bst s -> gt_tree x s -> sorted_e e ->
+      (forall y, In_e y e -> X.lt x y) ->
+      (forall y, In y s -> forall z, In_e z e -> X.lt y z) ->
       sorted_e (More x s e).
 
 Hint Constructors In_e sorted_e.
 
 Lemma elements_app :
- forall (s : tree) (acc : list elt), elements_aux acc s = elements s ++ acc.
+ forall s acc, elements_aux acc s = elements s ++ acc.
 Proof.
- simple induction s; simpl in |- *; intuition.
- rewrite H0.
- rewrite H.
+ induction s; simpl; intuition.
+ rewrite IHs1, IHs2.
  unfold elements; simpl.
- do 2 rewrite H.
- rewrite H0.
- repeat rewrite <- app_nil_end.
- repeat rewrite app_ass; auto.
+ rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto.
 Qed.
 
 Lemma compare_flatten_1 :
- forall (t0 t2 : tree) (t1 : elt) (z : int) (l : list elt),
- elements t0 ++ t1 :: elements t2 ++ l =
- elements (Node t0 t1 t2 z) ++ l.
+ forall l x r h acc,
+ elements l ++ x :: elements r ++ acc =
+ elements (Node l x r h) ++ acc.
 Proof.
- simpl in |- *; unfold elements in |- *; simpl in |- *; intuition.
- repeat rewrite elements_app.
- repeat rewrite <- app_nil_end.
- repeat rewrite app_ass; auto.
+ unfold elements; simpl; intuition.
+ rewrite !elements_app, <- !app_nil_end, !app_ass; auto.
 Qed.
 
 (** key lemma for correctness *)
 
 Lemma flatten_e_elements :
- forall (x : elt) (l r : tree) (z : int) (e : enumeration),
- elements l ++ flatten_e (More x r e) = elements (Node l x r z) ++ flatten_e e.
+ forall l x r h e,
+ elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ flatten_e e.
 Proof.
- intros; simpl.
- apply compare_flatten_1.
+ intros; simpl; apply compare_flatten_1.
 Qed.
 
-(** termination of [compare_aux] *)
-
-Open Scope nat_scope.
- 
-Fixpoint measure_e_t (s : tree) : nat := match s with
-  | Leaf => 0
-  | Node l _ r _ => 1 + measure_e_t l + measure_e_t r
- end.
-
-Fixpoint measure_e (e : enumeration) : nat := match e with
-  | End => 0
-  | More _ s r => 1 + measure_e_t s + measure_e r
- end.
-
 (** [cons t e] adds the elements of tree [t] on the head of 
     enumeration [e]. *)
 
-Fixpoint cons s e {struct s} : enumeration := 
+Fixpoint cons s e : enumeration := 
  match s with 
   | Leaf => e
   | Node l x r h => cons l (More x r e)
  end.
 
-Lemma cons_measure_e : forall s e, 
- measure_e (cons s e) = measure_e_t s + measure_e e.
-Proof.
- induction s; simpl; intros; auto.
- rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith.
-Qed.
-
 Lemma cons_1 : forall s e, 
   bst s -> sorted_e e ->
   (forall (x y : elt), In x s -> In_e y e -> X.lt x y) ->
@@ -2205,115 +1666,97 @@ Proof.
  apply flatten_e_elements.
 Qed.
 
-Lemma l_eq_cons :
- forall (l1 l2 : list elt) (x y : elt),
- X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2).
-Proof.
- unfold L.eq, L.Equal in |- *; intuition.
- inversion_clear H1; generalize (H0 a); clear H0; intuition.
- apply InA_eqA with x; eauto.
- inversion_clear H1; generalize (H0 a); clear H0; intuition.
- apply InA_eqA with y; eauto.
-Qed.
+(** One step of comparison of elements *)
 
-Definition measure2 e := measure_e e#1 + measure_e e#2.
-
-Function compare_aux 
- (e:enumeration*enumeration) { measure measure2 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 
-        | EQ _ => compare_aux (cons r1 e1, cons r2 e2)
-        | LT _ => Lt 
-        | GT _ => Gt 
-       end
+Definition compare_more x1 (cont:enumeration->comparison) e2 :=
+ match e2 with
+ | End => Gt
+ | More x2 r2 e2 =>
+     match X.compare x1 x2 with
+      | EQ _ => cont (cons r2 e2)
+      | LT _ => Lt
+      | GT _ => Gt
+     end
  end.
 
-Proof.
-intros; unfold measure2; simpl; 
-abstract (do 2 rewrite cons_measure_e; romega with *).
-Defined.
+(** Comparison of left tree, middle element, then right tree *)
 
-Definition compare s1 s2 := compare_aux (cons s1 End, cons s2 End).
+Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 := 
+ match s1 with
+  | Leaf => cont e2
+  | Node l1 x1 r1 _ =>
+     compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
+  end.
 
-Lemma compare_aux_Eq : forall e, 
- sorted_e e#1 -> sorted_e e#2 -> 
- compare_aux e = Eq -> L.eq (flatten_e e#1) (flatten_e e#2).
-Proof.
- intros e; functional induction compare_aux e; simpl; intros; auto; 
-  try discriminate.
- apply L.eq_refl.
- apply l_eq_cons; auto.
- inversion H; subst; clear H.
- inversion H0; subst; clear H0.
- destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto.
- rewrite <- H0; rewrite <- H3; auto.
-Qed.
+(** Initial continuation *)
 
-Lemma compare_aux_Lt : forall e, 
- sorted_e e#1 -> sorted_e e#2 -> 
- compare_aux e = Lt -> L.lt (flatten_e e#1) (flatten_e e#2).
-Proof.
- intros e; functional induction compare_aux e; simpl; intros; auto; 
-  try discriminate.
- apply L.lt_cons_eq; auto.
- inversion H; subst; clear H.
- inversion H0; subst; clear H0.
- destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto.
- rewrite <- H0; rewrite <- H3; auto.
-Qed.
+Definition compare_end e2 := 
+ match e2 with End => Eq | _ => Lt end.
+
+(** The complete comparison *)
+
+Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End).
 
-Lemma compare_aux_Gt : forall e, 
- sorted_e e#1 -> sorted_e e#2 -> 
- compare_aux e = Gt -> L.lt (flatten_e e#2) (flatten_e e#1).
+(** Correctness of this comparison *)
+
+Definition Cmp c := 
+ match c with 
+  | Eq => L.eq
+  | Lt => L.lt
+  | Gt => (fun l1 l2 => L.lt l2 l1)
+ end.
+
+Lemma cons_Cmp : forall c x1 x2 l1 l2, X.eq x1 x2 ->
+ Cmp c l1 l2 -> Cmp c (x1::l1) (x2::l2). 
 Proof.
- intros e; functional induction compare_aux e; simpl; intros; auto; 
-  try discriminate.
- apply L.lt_cons_eq; auto.
- inversion H; subst; clear H.
- inversion H0; subst; clear H0.
- destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto.
- rewrite <- H0; rewrite <- H3; auto.
+ destruct c; simpl; auto.
 Qed.
+Hint Resolve cons_Cmp.
 
-Lemma compare_Eq : forall s1 s2, bst s1 -> bst s2 -> 
- compare s1 s2 = Eq -> Equal s1 s2.
+Lemma compare_end_Cmp : 
+ forall e2, Cmp (compare_end e2) nil (flatten_e e2).
 Proof.
- unfold compare; intros.
- destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2.
- destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2.
- simpl in *; rewrite <- app_nil_end in *.
- apply L_eq_eq; rewrite <-E1, <-E2.
- apply (@compare_aux_Eq (cons s1 End, cons s2 End)); simpl; auto.
+ destruct e2; simpl; auto.
+ apply L.eq_refl.
 Qed.
 
-Lemma compare_Lt : forall s1 s2, bst s1 -> bst s2 -> 
- compare s1 s2 = Lt -> lt s1 s2.
+Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l, 
+  Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> 
+   Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l) 
+      (flatten_e (More x2 r2 e2)).
 Proof.
- unfold compare; intros.
- destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2.
- destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2.
- simpl in *; rewrite <- app_nil_end in *.
- red; rewrite <- E1, <- E2.
- apply (@compare_aux_Lt (cons s1 End, cons s2 End)); simpl; auto.
+ simpl; intros; destruct X.compare; simpl; auto.
 Qed.
 
-Lemma compare_Gt : forall s1 s2, bst s1 -> bst s2 ->
- compare s1 s2 = Gt -> lt s2 s1.
+Lemma compare_cont_Cmp : forall s1 cont e2 l,
+ bst s1 -> sorted_e e2 ->
+ (forall e, sorted_e e -> Cmp (cont e) l (flatten_e e)) -> 
+ Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
 Proof.
- unfold compare; intros.
- destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2.
- destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2.
- simpl in *; rewrite <- app_nil_end in *.
- red; rewrite <- E1, <- E2.
- apply (@compare_aux_Gt (cons s1 End, cons s2 End)); simpl; auto.
+ induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto.
+ inv bst.
+ rewrite <- compare_flatten_1; simpl.
+ apply Hl1; auto. clear e2 H0. intros [|x2 r2 e2] He2.
+ simpl; auto.
+ apply compare_more_Cmp.
+ inversion_clear He2.
+ destruct (cons_1 H H6); auto.
+ rewrite <- H10; auto.
+Qed.
+
+Lemma compare_Cmp : forall s1 s2, bst s1 -> bst s2 ->
+ Cmp (compare s1 s2) (elements s1) (elements s2).
+Proof.
+ intros; unfold compare.
+ rewrite (app_nil_end (elements s1)), (app_nil_end (elements s2)).
+ destruct (@cons_1 s2 End); auto.
+ inversion 2.
+ simpl in H2. unfold elt in *; rewrite <- H2.
+ apply compare_cont_Cmp; auto.
+ intros.
+ apply compare_end_Cmp; auto.
 Qed.
 
-Close Scope nat_scope.
-
 (** * Equality test *)
 
 Definition equal s1 s2 : bool := 
@@ -2326,17 +1769,17 @@ Lemma equal_1 : forall s1 s2, bst s1 -> bst s2 ->
  Equal s1 s2 -> equal s1 s2 = true.
 Proof.
 unfold equal; intros s1 s2 B1 B2 E.
-generalize (compare_Lt B1 B2)(compare_Gt B1 B2).
-destruct (compare s1 s2); auto; intros.
-elim (lt_not_eq B1 B2 (H (refl_equal Lt)) E); auto.
-elim (lt_not_eq B2 B1 (H0 (refl_equal Gt)) (eq_sym E)); auto.
+generalize (compare_Cmp B1 B2). 
+destruct (compare s1 s2); simpl in *; auto; intros.
+elim (lt_not_eq B1 B2 H E); auto.
+elim (lt_not_eq B2 B1 H (eq_sym E)); auto.
 Qed.
 
 Lemma equal_2 : forall s1 s2, bst s1 -> bst s2 ->   
  equal s1 s2 = true -> Equal s1 s2.
 Proof.
 unfold equal; intros s1 s2 B1 B2 E.
-generalize (compare_Eq B1 B2); 
+generalize (compare_Cmp B1 B2); 
  destruct compare; auto; discriminate.
 Qed.
 
@@ -2347,76 +1790,66 @@ End Raw.
 (** * Encapsulation
 
    Now, in order to really provide a functor implementing [S], we 
-   need to encapsulate everything into a type of balanced binary search trees. *)
+   need to encapsulate everything into a type of binary search trees. 
+   They also happen to be well-balanced, but this has no influence 
+   on the correctness of operations, so we won't state this here, 
+   see [FSetFullAVL] if you need more than just the FSet interface.
+*)
 
 Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Module E := X.
- Module Raw := Raw I X. 
+ Module Raw := Raw I X.
 
- Record bbst := Bbst {this :> Raw.t; is_bst : Raw.bst this; is_avl: Raw.avl this}.
- Definition t := bbst.
+ Record bst := Bst {this :> Raw.t; is_bst : Raw.bst this}.
+ Definition t := bst.
  Definition elt := E.t.
  
- Definition In (x : elt) (s : t) : Prop := Raw.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.
-  
+ Definition In (x : elt) (s : t) := Raw.In x s.
+ Definition Equal (s s':t) := forall a : elt, In a s <-> In a s'.
+ Definition Subset (s s':t) := forall a : elt, In a s -> In a s'.
+ Definition Empty (s:t) := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop) (s:t) := forall x, In x s -> P x.
+ Definition Exists (P : elt -> Prop) (s:t) := 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. 
  Proof. intro s; exact (@Raw.In_1 s). Qed.
  
  Definition mem (x:elt)(s:t) : bool := Raw.mem x s.
 
- Definition empty : t := Bbst Raw.empty_bst Raw.empty_avl.
+ Definition empty : t := Bst Raw.empty_bst.
  Definition is_empty (s:t) : bool := Raw.is_empty s.
- Definition singleton (x:elt) : t := Bbst (Raw.singleton_bst x) (Raw.singleton_avl x).
- Definition add (x:elt)(s:t) : t := 
-   Bbst (Raw.add_bst x (is_bst s) (is_avl s)) 
-        (Raw.add_avl x (is_avl s)). 
- Definition remove (x:elt)(s:t) : t := 
-   Bbst (Raw.remove_bst x (is_bst s) (is_avl s)) 
-        (Raw.remove_avl x (is_avl s)). 
- Definition inter (s s':t) : t := 
-   Bbst (Raw.inter_bst (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
-        (Raw.inter_avl (is_avl s) (is_avl s')).
- Definition union (s s':t) : t := 
-   let (s,b,a) := s in let (s',b',a') := s' in 
-   Bbst (@Raw.union_bst (s,s') b a b' a')  
-        (@Raw.union_avl (s,s') a a').
- Definition diff (s s':t) : t := 
-   Bbst (Raw.diff_bst (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
-        (Raw.diff_avl (is_avl s) (is_avl s')).
+ Definition singleton (x:elt) : t := Bst (Raw.singleton_bst x).
+ Definition add (x:elt)(s:t) : t := Bst (Raw.add_bst x (is_bst s)). 
+ Definition remove (x:elt)(s:t) : t := Bst (Raw.remove_bst x (is_bst s)).
+ Definition inter (s s':t) : t := Bst (Raw.inter_bst (is_bst s) (is_bst s')).
+ Definition union (s s':t) : t := Bst (Raw.union_bst (is_bst s) (is_bst s')).
+ Definition diff (s s':t) : t := Bst (Raw.diff_bst (is_bst s) (is_bst s')).
  Definition elements (s:t) : list elt := Raw.elements s.
  Definition min_elt (s:t) : option elt := Raw.min_elt s.
  Definition max_elt (s:t) : option elt := Raw.max_elt s.
  Definition choose (s:t) : option elt := Raw.choose s.
- Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. 
+ Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s.
  Definition cardinal (s:t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s:t) : t := 
-   Bbst (Raw.filter_bst f (is_bst s) (is_avl s))
-        (Raw.filter_avl f (is_avl s)). 
+   Bst (Raw.filter_bst f (is_bst s)).
  Definition for_all (f : elt -> bool) (s:t) : bool := Raw.for_all f s.
  Definition exists_ (f : elt -> bool) (s:t) : bool := Raw.exists_ f s.
  Definition partition (f : elt -> bool) (s:t) : t * t :=
    let p := Raw.partition f s in
-   (@Bbst (fst p) (Raw.partition_bst_1 f (is_bst s) (is_avl s)) 
-                  (Raw.partition_avl_1 f (is_avl s)),
-    @Bbst (snd p) (Raw.partition_bst_2 f (is_bst s) (is_avl s)) 
-                  (Raw.partition_avl_2 f (is_avl s))).
+   (@Bst (fst p) (Raw.partition_bst_1 f (is_bst s)), 
+    @Bst (snd p) (Raw.partition_bst_2 f (is_bst s))).
 
  Definition equal (s s':t) : bool := Raw.equal s s'.
- Definition subset (s s':t) : bool := Raw.subset (s.(this),s'.(this)).
+ Definition subset (s s':t) : bool := Raw.subset s s'.
 
  Definition eq (s s':t) : Prop := Raw.Equal s s'.
  Definition lt (s s':t) : Prop := Raw.lt s s'.
 
  Definition compare (s s':t) : Compare lt eq s s'.
- Proof. 
-  intros (s,b,a) (s',b',a').
-  generalize (Raw.compare_Eq b b') (Raw.compare_Lt b b') (Raw.compare_Gt b b').
+ Proof.
+  intros (s,b) (s',b').
+  generalize (Raw.compare_Cmp b b').
   destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
  Defined.
 
@@ -2425,7 +1858,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Variable s s' s'': t. 
  Variable x y : elt.
 
- Hint Resolve is_bst is_avl.
+ Hint Resolve is_bst.
  
  Lemma mem_1 : In x s -> mem x s = true. 
  Proof. exact (Raw.mem_1 (is_bst s)). Qed.
@@ -2437,15 +1870,12 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma equal_2 : equal s s' = true -> Equal s s'.
  Proof. exact (Raw.equal_2 (is_bst s) (is_bst s')). Qed.
 
- Lemma subset_1 : Subset s s' -> subset s s' = true.
- Proof. 
- unfold subset; rewrite <- Raw.subset_12; simpl; auto.
- Qed.
+ Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.
 
+ Lemma subset_1 : Subset s s' -> subset s s' = true.
+ Proof. wrap subset Raw.subset_12. Qed.
  Lemma subset_2 : subset s s' = true -> Subset s s'.
- Proof. 
- unfold subset; rewrite <- Raw.subset_12; simpl; auto.
- Qed.
+ Proof. wrap subset Raw.subset_12. Qed.
 
  Lemma empty_1 : Empty empty.
  Proof. exact Raw.empty_1. Qed.
@@ -2456,35 +1886,18 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@Raw.is_empty_2 s). Qed.
  
  Lemma add_1 : E.eq x y -> In y (add x s).
- Proof. 
- unfold add, In; simpl; rewrite Raw.add_in; auto.
- Qed.
-
+ Proof. wrap add Raw.add_in. Qed.
  Lemma add_2 : In y s -> In y (add x s).
- Proof.
- unfold add, In; simpl; rewrite Raw.add_in; auto.
- Qed.
-
+ Proof. wrap add Raw.add_in. Qed.
  Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
- Proof. 
- unfold add, In; simpl; rewrite Raw.add_in; intuition.
- elim H; auto.
- Qed.
+ Proof. wrap add Raw.add_in. elim H; auto. Qed.
 
  Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
- Proof. 
- unfold remove, In; simpl; rewrite Raw.remove_in; intuition.
- Qed.
-
+ Proof. wrap remove Raw.remove_in. Qed.
  Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
- Proof. 
- unfold remove, In; simpl; rewrite Raw.remove_in; intuition.
- Qed.
-
+ Proof. wrap remove Raw.remove_in. Qed.
  Lemma remove_3 : In y (remove x s) -> In y s.
- Proof. 
- unfold remove, In; simpl; rewrite Raw.remove_in; intuition.
- Qed.
+ Proof. wrap remove Raw.remove_in. Qed.
 
  Lemma singleton_1 : In y (singleton x) -> E.eq x y. 
  Proof. exact (@Raw.singleton_1 x y). Qed.
@@ -2492,52 +1905,25 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@Raw.singleton_2 x y). Qed.
 
  Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
- Proof.
- unfold union, In; simpl.
- destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto.
- Qed.
-
+ Proof. wrap union Raw.union_in. Qed.
  Lemma union_2 : In x s -> In x (union s s'). 
- Proof.
- unfold union, In; simpl.
- destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto.
- Qed.
-
+ Proof. wrap union Raw.union_in. Qed.
  Lemma union_3 : In x s' -> In x (union s s').
- Proof.
- unfold union, In; simpl.
- destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto.
- Qed.
+ Proof. wrap union Raw.union_in. Qed.
 
  Lemma inter_1 : In x (inter s s') -> In x s.
- Proof.
- unfold inter, In; simpl; rewrite Raw.inter_in; intuition.
- Qed.
-
+ Proof. wrap inter Raw.inter_in. Qed.
  Lemma inter_2 : In x (inter s s') -> In x s'.
- Proof. 
- unfold inter, In; simpl; rewrite Raw.inter_in; intuition.
- Qed.
-
+ Proof. wrap inter Raw.inter_in. Qed.
  Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
- Proof. 
- unfold inter, In; simpl; rewrite Raw.inter_in; intuition.
- Qed.
+ Proof. wrap inter Raw.inter_in. Qed.
  
  Lemma diff_1 : In x (diff s s') -> In x s. 
- Proof. 
- unfold diff, In; simpl; rewrite Raw.diff_in; intuition.
- Qed.
-
+ Proof. wrap diff Raw.diff_in. Qed.
  Lemma diff_2 : In x (diff s s') -> ~ In x s'.
- Proof. 
- unfold diff, In; simpl; rewrite Raw.diff_in; intuition.
- Qed.
-
+ Proof. wrap diff Raw.diff_in. Qed.
  Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
- Proof. 
- unfold diff, In; simpl; rewrite Raw.diff_in; intuition.
- Qed.
+ Proof. wrap diff Raw.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.
@@ -2554,19 +1940,11 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Variable f : elt -> bool.
 
  Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
- Proof. 
- intro; unfold filter, In; simpl; rewrite Raw.filter_in; intuition.
- Qed.
-
+ Proof. intro. wrap filter Raw.filter_in. Qed.
  Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
- Proof. 
- intro; unfold filter, In; simpl; rewrite Raw.filter_in; intuition.
- Qed.
-
+ Proof. intro. wrap filter Raw.filter_in. Qed. 
  Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
- Proof. 
- intro; unfold filter, In; simpl; rewrite Raw.filter_in; intuition.
- Qed.
+ Proof. intro. wrap filter Raw.filter_in. Qed.
 
  Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true.
  Proof. exact (@Raw.for_all_1 f s). Qed.
@@ -2582,16 +1960,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
   Equal (fst (partition f s)) (filter f s).
  Proof.
  unfold partition, filter, Equal, In; simpl ;intros H a.
- rewrite Raw.partition_in_1; auto.
- rewrite Raw.filter_in; intuition.
+ rewrite Raw.partition_in_1, Raw.filter_in; intuition.
  Qed.
 
  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.
- rewrite Raw.partition_in_2; auto.
- rewrite Raw.filter_in; intuition.
+ rewrite Raw.partition_in_2, Raw.filter_in; intuition.
  rewrite H2; auto.
  destruct (f a); auto.
  red; intros; f_equal.
@@ -2601,18 +1977,11 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  End Filter.
 
  Lemma elements_1 : In x s -> InA E.eq x (elements s).
- Proof. 
- unfold elements, In; rewrite Raw.elements_in; auto.
- Qed.
-
+ Proof. wrap elements Raw.elements_in. Qed.
  Lemma elements_2 : InA E.eq x (elements s) -> In x s.
- Proof. 
- unfold elements, In; rewrite Raw.elements_in; auto.
- Qed.
-
+ Proof. wrap elements Raw.elements_in. Qed.
  Lemma elements_3 : sort E.lt (elements s).
  Proof. exact (Raw.elements_sort (is_bst s)). Qed.
-
  Lemma elements_3w : NoDupA E.eq (elements s).
  Proof. exact (Raw.elements_nodup (is_bst s)). Qed.
 
@@ -2636,9 +2005,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@Raw.choose_2 s). Qed.
  Lemma choose_3 : choose s = Some x -> choose s' = Some y -> 
   Equal s s' -> E.eq x y.
- Proof. 
-  exact (@Raw.choose_3 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') x y).
- Qed.
+ Proof. exact (@Raw.choose_3 _ _ (is_bst s) (is_bst s') x y). Qed.
 
  Lemma eq_refl : eq s s. 
  Proof. exact (Raw.eq_refl s). Qed.
@@ -2660,4 +2027,3 @@ End IntMake.
 Module Make (X: OrderedType) <: S with Module E := X
  :=IntMake(Z_as_Int)(X).
 
-
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
new file mode 100644
index 0000000000..748658c9ca
--- /dev/null
+++ b/theories/FSets/FSetFullAVL.v
@@ -0,0 +1,1126 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* 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 
+   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], 
+   [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 
+   similar to the one of [FSetAVL], but richer.
+*)
+
+Require Import Recdef FSetInterface FSetList ZArith Int FSetAVL.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Module AvlProofs (Import I:Int)(X:OrderedType).
+Module Import Raw := Raw I X.
+Module Import II := MoreInt I.
+Open Local Scope Int_scope.
+
+(** * AVL trees *)
+
+(** [avl s] : [s] is a properly balanced AVL tree,
+    i.e. for any node the heights of the two children
+    differ by at most 2 *)
+
+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 -> 
+      avl (Node l x r h).
+
+(** * Automation and dedicated tactics *)
+
+Hint Constructors avl.
+
+(** A tactic for cleaning hypothesis after use of functional induction. *)
+
+Ltac clearf :=
+ match goal with 
+  | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
+  | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
+  | _ => idtac
+ end.
+
+(** Tactics about [avl] *)
+
+Lemma height_non_negative : forall s : tree, avl s -> height s >= 0.
+Proof.
+ induction s; simpl; intros; auto with zarith.
+ inv avl; intuition; omega_max.
+Qed.
+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 := 
+     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 
+   | Prop => avl_nn_hyp h
+   | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
+  end.
+
+(* Repeat the previous tactic. 
+   Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
+
+Ltac avl_nns :=
+  match goal with 
+     | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
+     | _ => idtac
+  end.
+
+(** Results about [height] *)
+
+Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.
+Proof.
+ destruct 1; intuition; simpl in *.
+ avl_nns; simpl in *; elimtype False; omega_max.
+Qed.
+
+(** * Results about [avl] *)
+
+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)).
+Proof.
+  intros; auto.
+Qed.
+Hint Resolve avl_node.
+
+
+(** empty *)
+
+Lemma empty_avl : avl empty.
+Proof. 
+ auto.
+Qed.
+
+(** singleton *)
+
+Lemma singleton_avl : forall x : elt, avl (singleton x).
+Proof.
+ unfold singleton; intro.
+ constructor; auto; try red; simpl; omega_max.
+Qed.
+
+(** create *)
+
+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 -> 
+ height (create l x r) = max (height l) (height r) + 1.
+Proof.
+ unfold create; auto.
+Qed.
+
+(** bal *)
+
+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 *; 
+ 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 -> 
+ -(3) <= height l - height r <= 3 ->
+ 0 <= 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; 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 -> 
+ 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'); 
+     omega_max
+  end.
+
+(** add *)
+
+Lemma add_avl_1 :  forall s x, avl s -> 
+ avl (add x s) /\ 0 <= height (add x s) - height s <= 1.
+Proof. 
+ intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *.
+ intuition; try constructor; simpl; auto; try omega_max.
+ (* LT *)
+ destruct IHt; auto.
+ split.
+ apply bal_avl; auto; omega_max.
+ omega_bal.
+ (* EQ *)
+ intuition; omega_max.
+ (* GT *)
+ destruct IHt; auto.
+ split.
+ apply bal_avl; auto; omega_max.
+ omega_bal.
+Qed.
+
+Lemma add_avl : forall s x, avl s -> avl (add x s).
+Proof.
+ intros; destruct (add_avl_1 x H); auto.
+Qed.
+Hint Resolve add_avl.
+
+(** join *)
+
+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. 
+ join_tac.
+
+ split; simpl; auto. 
+ destruct (add_avl_1 x H0).
+ avl_nns; omega_max.
+ set (l:=Node ll lx lr lh) in *.
+ split; auto.
+ destruct (add_avl_1 x H).
+ simpl (height Leaf).
+ avl_nns; omega_max.
+
+ inversion_clear H.
+ assert (height (Node rl rx rr rh) = rh); auto.
+ set (r := Node rl rx rr rh) in *; clearbody r.
+ destruct (Hlr x r H2 H0); clear Hrl Hlr.
+ set (j := join lr x r) in *; clearbody j.
+ simpl.
+ assert (-(3) <= height ll - height j <= 3) by omega_max.
+ split.
+ apply bal_avl; auto.
+ omega_bal.
+
+ inversion_clear H0.
+ assert (height (Node ll lx lr lh) = lh); auto.
+ set (l := Node ll lx lr lh) in *; clearbody l.
+ destruct (Hrl H H1); clear Hrl Hlr.
+ set (j := join l x rl) in *; clearbody j.
+ simpl.
+ assert (-(3) <= height j - height rr <= 3) by omega_max.
+ split.
+ apply bal_avl; auto.
+ omega_bal.
+
+ clear Hrl Hlr.
+ assert (height (Node ll lx lr lh) = lh); auto.
+ assert (height (Node rl rx rr rh) = rh); auto.
+ set (l := Node ll lx lr lh) in *; clearbody l.
+ set (r := Node rl rx rr rh) in *; clearbody r.
+ assert (-(2) <= height l - height r <= 2) by omega_max.
+ split.
+ apply create_avl; auto.
+ rewrite create_height; auto; omega_max.
+Qed.
+
+Lemma join_avl : forall l x r, avl l -> avl r -> avl (join l x r).
+Proof.
+ intros; destruct (join_avl_1 x H H0); auto.
+Qed.
+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 /\ 
+ 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.
+ inv avl; simpl in *; split; auto.
+ avl_nns; omega_max.
+ inversion_clear H.
+ rewrite e0 in IHp;simpl in IHp;destruct (IHp lh); auto.
+ 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. 
+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) /\ 
+ 0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
+Proof.
+ intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
+ split; auto; avl_nns; omega_max.
+ split; auto; avl_nns; simpl in *; omega_max.
+ destruct s1;try contradiction;clear y.
+ generalize (remove_min_avl_1 H0).
+ rewrite e1; simpl; destruct 1.
+ split.
+ apply bal_avl; auto.
+ simpl; omega_max.
+ omega_bal.
+Qed.
+
+Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 -> 
+  -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2).
+Proof. 
+ intros; destruct (merge_avl_1 H H0 H1); auto.
+Qed.
+
+
+(** remove *)
+
+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); subst;simpl; intros.
+ intuition; omega_max.
+ (* LT *)
+ inv avl.
+ destruct (IHt H0).
+ split. 
+ apply bal_avl; auto.
+ omega_max.
+ omega_bal.
+ (* EQ *)
+ inv avl. 
+ generalize (merge_avl_1 H0 H1 H2).
+ intuition omega_max.
+ (* GT *)
+ inv avl.
+ destruct (IHt H1).
+ split. 
+ apply bal_avl; auto.
+ omega_max.
+ omega_bal.
+Qed.
+
+Lemma remove_avl : forall s x, avl s -> avl (remove x s).
+Proof. 
+ intros; destruct (remove_avl_1 x H); auto.
+Qed.
+Hint Resolve remove_avl.
+
+(** concat *)
+
+Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
+Proof.
+ intros s1 s2; functional induction (concat s1 s2); subst;auto.
+ destruct s1;try contradiction;clear y.
+ intros; apply join_avl; auto.
+ generalize (remove_min_avl H0); rewrite e1; simpl; auto.
+Qed.
+Hint Resolve concat_avl.
+
+(** split *)
+
+Lemma split_avl : forall s x, avl s -> 
+  avl (split x s)#1 /\ avl (split x s)#2#2.
+Proof. 
+ intros s x; functional induction (split x s);subst;simpl in *.
+ auto.
+ rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
+ simpl; inversion_clear 1; auto.
+ rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
+Qed.
+
+(** inter *)
+
+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; 
+ inv avl; auto.
+Qed.
+
+(** diff *)
+
+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; 
+ inv avl; auto.
+Qed.
+
+(** union *)
+
+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; 
+ inv avl; auto.
+Qed.
+
+(** filter *)
+
+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. 
+Hint Resolve filter_acc_avl.
+
+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 -> 
+ avl acc#1 -> avl (partition_acc f acc s)#1.
+Proof.
+ induction s; simpl; auto.
+ destruct acc as [acct accf]; simpl in *.
+ intros.
+ inv avl.
+ apply IHs2; auto.
+ apply IHs1; auto.
+ destruct (f t); simpl; auto.
+Qed.
+
+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.
+ destruct acc as [acct accf]; simpl in *.
+ intros.
+ inv avl.
+ apply IHs2; auto.
+ apply IHs1; auto.
+ destruct (f t); simpl; auto.
+Qed. 
+
+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. 
+Proof.
+ unfold partition; intros; apply partition_acc_avl_2; auto.
+Qed.
+
+End AvlProofs.
+
+
+Module OcamlOps (Import I:Int)(X:OrderedType).
+Module Import AvlProofs := AvlProofs I X.
+Import Raw.
+Import II.
+Open Local Scope nat_scope.
+
+(** Properties of cardinal *)
+
+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, 
+ cardinal (add x s) <= S (cardinal s).
+Proof.
+ intros; functional induction add x s; simpl; auto with arith; 
+ rewrite bal_cardinal; romega with *.
+Qed.
+
+Lemma join_cardinal : forall l x r, 
+ cardinal (join l x r) <= S (cardinal l + cardinal r).
+Proof.
+ join_tac; simpl; auto with arith.
+ apply add_cardinal.
+ destruct X.compare; simpl; auto with arith.
+ 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); 
+  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 *.
+ generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr).
+ simpl in *; romega with *.
+Qed.
+
+Lemma split_cardinal_1 : forall x s, 
+ (cardinal (split x s)#1 <= cardinal s)%nat.
+Proof.
+ intros x s; functional induction split x s; simpl; auto.
+ rewrite e1 in IHp; simpl in *.
+ romega with *.
+ romega with *.
+ rewrite e1 in IHp; simpl in *.
+ generalize (@join_cardinal l y rl); romega with *.
+Qed.
+
+Lemma split_cardinal_2 : forall x s, 
+ (cardinal (split x s)#2#2 <= cardinal s)%nat.
+Proof.
+ intros x s; functional induction split x s; simpl; auto.
+ rewrite e1 in IHp; simpl in *.
+ generalize (@join_cardinal rl y r); romega with *.
+ romega with *.
+ rewrite e1 in IHp; simpl in *; romega with *.
+Qed.
+
+(** * [ocaml_union], an union faithful to the original ocaml code *)
+
+Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat.
+
+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); 
+  rewrite H; simpl; romega with *
+ end.
+
+Function ocaml_union (s : t * t) { measure cardinal2 s } : t  :=
+ 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) => 
+        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 
+             join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2'#2))
+        else
+          if eq_dec h1 1%I then add x1 s#2 else
+          let (l1',r1') := split x2 s#1 in 
+             join (ocaml_union (l1',l2)) x2 (ocaml_union (r1'#2,r2))
+ end.
+Proof.
+abstract ocaml_union_tac.
+abstract ocaml_union_tac.
+abstract ocaml_union_tac.
+abstract ocaml_union_tac.
+Defined.
+
+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; 
+  simpl fst in *; simpl snd in *; try clear e0 e1.
+ intuition_in.
+ intuition_in.
+ intuition_in.
+ (* add x2 s#1 *)
+ inv avl.
+ rewrite (height_0 H); [ | avl_nn l2; omega_max].
+ rewrite (height_0 H0); [ | avl_nn r2; omega_max].
+ rewrite add_in; intuition_in.
+ (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *)
+ generalize
+  (split_avl x1 A2) (split_bst x1 B2)
+  (split_in_1 x1 y B2) (split_in_2 x1 y B2).
+ rewrite e2; simpl.
+ destruct 1; destruct 1; inv avl; inv bst.
+ rewrite join_in, IHt, IHt0; auto.
+ do 2 (intro Eq; rewrite Eq; clear Eq).
+ case (X.compare y x1); intuition_in.
+ (* add x1 s#2 *)
+ inv avl.
+ rewrite (height_0 H3); [ | avl_nn l1; omega_max].
+ rewrite (height_0 H4); [ | avl_nn r1; omega_max].
+ rewrite add_in; auto; intuition_in.
+ (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *)
+ generalize 
+  (split_avl x2 A1) (split_bst x2 B1)
+  (split_in_1 x2 y B1) (split_in_2 x2 y B1).
+ rewrite e2; simpl.
+ destruct 1; destruct 1; inv avl; inv bst.
+ rewrite join_in, IHt, IHt0; auto.
+ do 2 (intro Eq; rewrite Eq; clear Eq).
+ case (X.compare y x2); intuition_in.
+Qed.
+
+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; 
+  try apply add_bst; auto.
+ (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *)
+ generalize (split_avl x1 A2) (split_bst x1 B2).
+ rewrite e2; simpl.
+ destruct 1; destruct 1.
+ destruct (distr_pair e2) as (L,R); clear e2.
+ inv bst; inv avl.
+ apply join_bst; auto.
+ intro y; rewrite ocaml_union_in; auto; simpl.
+ rewrite <- L, split_in_1; auto; intuition_in.
+ intro y; rewrite ocaml_union_in; auto; simpl.
+ rewrite <- R, split_in_2; auto; intuition_in.
+ (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *)
+ generalize (split_avl x2 A1) (split_bst x2 B1).
+ rewrite e2; simpl.
+ destruct 1; destruct 1.
+ destruct (distr_pair e2) as (L,R); clear e2.
+ inv bst; inv avl.
+ apply join_bst; auto.
+ intro y; rewrite ocaml_union_in; auto; simpl.
+ rewrite <- L, split_in_1; auto; intuition_in.
+ intro y; rewrite ocaml_union_in; auto; simpl.
+ rewrite <- R, split_in_2; auto; intuition_in.
+Qed.
+
+Lemma ocaml_union_avl : forall s, 
+ avl s#1 -> avl s#2 -> avl (ocaml_union s).
+Proof.
+ 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.
+ intros A1 A2; generalize (split_avl x2 A1); rewrite e2; simpl.
+ inv avl; destruct 1; auto.
+Qed.
+
+Lemma ocaml_union_alt : forall s, bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 ->
+ Equal (ocaml_union s) (union s#1 s#2).
+Proof.
+ red; intros; rewrite ocaml_union_in, union_in; simpl; intuition.
+Qed.
+
+
+(** * [ocaml_subset], a subset faithful to the original ocaml code *)
+
+Function ocaml_subset (s:t*t) { measure cardinal2 s } : bool :=
+ match s with
+  | (Leaf, _) => true
+  | (Node _ _ _ _, Leaf) => false
+  | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) =>
+     match X.compare x1 x2 with
+      | EQ _ => ocaml_subset (l1,l2) && ocaml_subset (r1,r2)
+      | LT _ => ocaml_subset (Node l1 x1 Leaf 0%I, l2) && ocaml_subset (r1,s#2)
+      | GT _ => ocaml_subset (Node Leaf x1 r1 0%I, r2) && ocaml_subset (l1,s#2)
+     end
+ end.
+
+Proof.
+ intros; unfold cardinal2; simpl; abstract romega with *.
+ intros; unfold cardinal2; simpl; abstract romega with *.
+ intros; unfold cardinal2; simpl; abstract romega with *.
+ intros; unfold cardinal2; simpl; abstract romega with *.
+ intros; unfold cardinal2; simpl; abstract romega with *.
+ intros; unfold cardinal2; simpl; abstract romega with *.
+Defined.
+
+Lemma ocaml_subset_12 : forall s, 
+ bst s#1 -> bst s#2 ->
+ (ocaml_subset s = true <-> Subset s#1 s#2).
+Proof.
+ intros s; functional induction ocaml_subset s; simpl;
+  intros B1 B2; try clear e0.
+ intuition.
+ red; auto; inversion 1.
+ split; intros; try discriminate.
+ assert (H': In _x0 Leaf) by auto; inversion H'.
+ (**)
+ simpl in *; inv bst.
+ rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
+ unfold Subset; intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ (**)
+ simpl in *; inv bst.
+ rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
+ unfold Subset; intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ (**)
+ simpl in *; inv bst.
+ rewrite andb_true_iff, IHb, IHb0; auto; clear IHb IHb0.
+ unfold Subset; intuition_in.
+ assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ 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 -> 
+ ocaml_subset s = subset s#1 s#2.
+Proof.
+ intros.
+ generalize (ocaml_subset_12 H H0); rewrite <-subset_12 by auto.
+ destruct ocaml_subset; destruct subset; intuition.
+Qed.
+
+
+
+(** [ocaml_compare], a compare faithful to the original ocaml code *)
+
+(** termination of [compare_aux] *)
+
+Fixpoint cardinal_e e := match e with
+  | End => 0
+  | More _ s r => S (cardinal s + cardinal_e r)
+ end.
+
+Lemma cons_cardinal_e : forall s e, 
+ cardinal_e (cons s e) = cardinal s + cardinal_e e.
+Proof.
+ induction s; simpl; intros; auto.
+ rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith.
+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 
+ | (End,End) => Eq
+ | (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 
+       end
+ end.
+
+Proof.
+intros; unfold cardinal_e_2; simpl; 
+abstract (do 2 rewrite cons_cardinal_e; romega with *).
+Defined.
+
+Definition ocaml_compare s1 s2 := 
+ ocaml_compare_aux (cons s1 End, cons s2 End).
+
+Lemma ocaml_compare_aux_Cmp : forall e, 
+ sorted_e e#1 -> sorted_e e#2 -> 
+ Cmp (ocaml_compare_aux e) (flatten_e e#1) (flatten_e e#2).
+Proof.
+ intros e; functional induction ocaml_compare_aux e; simpl; intros; 
+  auto; try discriminate.
+ apply L.eq_refl.
+ simpl in *.
+ apply cons_Cmp; auto.
+ inversion H; subst; clear H.
+ inversion H0; subst; clear H0.
+ destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto.
+ rewrite <-H0, <-H2; auto.
+Qed.
+
+Lemma ocaml_compare_Cmp : forall s1 s2, bst s1 -> bst s2 ->
+ Cmp (ocaml_compare s1 s2) (elements s1) (elements s2).
+Proof.
+ unfold ocaml_compare; intros.
+ destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2.
+ destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2.
+ simpl in *; rewrite <- app_nil_end, <- E1, <- E2 in *.
+ apply (@ocaml_compare_aux_Cmp (cons s1 End, cons s2 End)); simpl; auto.
+Qed.
+
+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 B1 B2)(compare_Cmp B1 B2). 
+ unfold Cmp.
+ destruct ocaml_compare; destruct compare; auto; intros; elimtype False.
+ elim (lt_not_eq B1 B2 H0); auto.
+ elim (lt_not_eq B2 B1 H0); auto.
+  apply eq_sym; auto.
+ elim (lt_not_eq B1 B2 H); auto.
+  elim (lt_not_eq B1 B1).
+  red; eapply L.lt_trans; eauto.
+  apply eq_refl.
+ elim (lt_not_eq B2 B1 H); auto.
+  apply eq_sym; auto.
+ elim (lt_not_eq B1 B2 H0); auto.
+  elim (lt_not_eq B1 B1).
+  red; eapply L.lt_trans; eauto.
+  apply eq_refl.
+Qed.
+
+
+(** * Equality test *)
+
+Definition ocaml_equal s1 s2 : bool := 
+ match ocaml_compare s1 s2 with 
+  | Eq => true
+  | _ => false 
+ end.
+
+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.
+generalize (ocaml_compare_Cmp B1 B2).
+destruct (ocaml_compare s1 s2); auto; intros.
+elim (lt_not_eq B1 B2 H E); auto.
+elim (lt_not_eq B2 B1 H (eq_sym E)); auto.
+Qed.
+
+Lemma ocaml_equal_2 : forall s1 s2, bst s1 -> bst s2 ->
+ ocaml_equal s1 s2 = true -> Equal s1 s2.
+Proof.
+unfold ocaml_equal; intros s1 s2 B1 B2 E.
+generalize (ocaml_compare_Cmp B1 B2); 
+ destruct ocaml_compare; auto; discriminate.
+Qed.
+
+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.
+Qed.
+
+End OcamlOps.
+
+
+
+(** * Encapsulation
+
+   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 
+   [ocaml_union], [ocaml_subset], [ocaml_compare], [ocaml_equal].
+*) 
+
+Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
+
+ Module E := X.
+ Module Import OcamlOps := OcamlOps I X.
+ Import AvlProofs.
+ Import Raw.
+
+ 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. 
+ Proof. intro s; exact (@In_1 s). Qed.
+ 
+ Definition mem (x:elt)(s:t) : bool := mem x s.
+
+ Definition empty : t := Bbst Raw.empty_bst empty_avl.
+ Definition is_empty (s:t) : bool := is_empty s.
+ 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 := 
+   Bbst (remove_bst x (is_bst s)) (remove_avl x (is_avl s)).
+ 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)) 
+          (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 := 
+   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 cardinal (s:t) : nat := cardinal s.
+ 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 (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 := 
+  ocaml_subset (s.(this),s'.(this)).
+
+ Definition eq (s s':t) : Prop := Equal s s'.
+ Definition lt (s s':t) : Prop := lt s s'.
+
+ Definition compare (s s':t) : Compare lt eq s s'.
+ Proof.
+  intros (s,b,a) (s',b',a').
+  generalize (compare_Cmp b b').
+  destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
+  change (Raw.Equal s s'); auto.
+ Defined.
+
+ Definition ocaml_compare (s s':t) : Compare lt eq s s'.
+ Proof.
+  intros (s,b,a) (s',b',a').
+  generalize (ocaml_compare_Cmp b b').
+  destruct ocaml_compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
+  change (Raw.Equal s s'); auto.
+ Defined.
+
+ (* specs *)
+ 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. 
+ 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.
+
+ Lemma equal_1 : Equal s s' -> equal s s' = true.
+ Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed.
+ Lemma equal_2 : equal s s' = true -> Equal s s'.
+ Proof. exact (equal_2 (is_bst s) (is_bst s')). Qed.
+
+ Lemma ocaml_equal_alt : ocaml_equal s s' = equal s s'.
+ 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 (is_bst s) (is_bst s')). Qed. 
+
+ Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition.
+
+ Lemma subset_1 : Subset s s' -> subset s s' = true.
+ Proof. wrap subset subset_12. Qed.
+ Lemma subset_2 : subset s s' = true -> Subset s s'.
+ Proof. wrap subset subset_12. Qed.
+
+ Lemma ocaml_subset_alt : ocaml_subset s s' = subset s s'.
+ Proof. 
+  destruct s; destruct s'; unfold ocaml_subset, subset; simpl.
+  rewrite ocaml_subset_alt; auto.
+ Qed.
+
+ Lemma ocaml_subset_1 : Subset s s' -> ocaml_subset s s' = true.
+ Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed.
+ Lemma ocaml_subset_2 : ocaml_subset s s' = true -> Subset s s'.
+ Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed.
+
+ Lemma empty_1 : Empty empty.
+ Proof. exact empty_1. Qed.
+
+ 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. 
+ 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. 
+ Proof. wrap add add_in. elim H; auto. Qed.
+
+ Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
+ Proof. wrap remove remove_in. Qed.
+ Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
+ Proof. wrap remove remove_in. Qed.
+ 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. 
+ Proof. exact (@singleton_1 x y). Qed.
+ 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'). 
+ 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. 
+  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').
+ Qed.
+
+ Lemma ocaml_union_1 : In x (ocaml_union s s') -> In x s \/ In x s'.
+ Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
+ Lemma ocaml_union_2 : In x s -> In x (ocaml_union s s').
+ Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
+ Lemma ocaml_union_3 : In x s' -> In x (ocaml_union s s').
+ Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed.
+
+ Lemma inter_1 : In x (inter s s') -> In x s.
+ Proof. wrap inter inter_in. Qed.
+ Lemma inter_2 : In x (inter s s') -> In x s'.
+ 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. 
+ 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. 
+ unfold fold, elements; intros; apply fold_1; auto.
+ Qed.
+
+ Lemma cardinal_1 : cardinal s = length (elements s).
+ 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. 
+ 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.
+
+ Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true.
+ Proof. exact (@for_all_1 f s). Qed.
+ Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s.
+ Proof. exact (@for_all_2 f s). Qed.
+
+ Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
+ Proof. exact (@exists_1 f s). Qed.
+ 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 -> 
+  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 -> 
+  Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+ Proof.
+ unfold partition, filter, Equal, In; simpl ;intros H a.
+ rewrite partition_in_2, filter_in; intuition.
+ rewrite H2; auto.
+ destruct (f a); auto.
+ red; intros; f_equal.
+ rewrite (H _ _ H0); auto.
+ Qed.
+
+ End Filter.
+
+ Lemma elements_1 : In x s -> InA E.eq x (elements s).
+ Proof. wrap elements elements_in. Qed.
+ Lemma elements_2 : InA E.eq x (elements s) -> In x s.
+ Proof. wrap elements elements_in. Qed.
+ Lemma elements_3 : sort E.lt (elements s).
+ Proof. exact (elements_sort (is_bst s)). Qed.
+ 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. 
+ 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. 
+ 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.
+ Lemma max_elt_3 : max_elt s = None -> Empty s.
+ Proof. exact (@max_elt_3 s). Qed.
+
+ Lemma choose_1 : choose s = Some x -> In x s.
+ 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 -> 
+  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. 
+ 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'.
+ Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed.
+
+ End Specs.
+End IntMake.
+
+(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *)
+
+Module Make (X: OrderedType) <: S with Module E := X
+ :=IntMake(Z_as_Int)(X).
+