Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 1842 insertions, 0 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
new file mode 100644
index 00000000..c41df7c2
--- /dev/null
+++ b/theories/MSets/MSetAVL.v
@@ -0,0 +1,1842 @@
+(* -*- coding: utf-8 -*- *)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(** * MSetAVL : Implementation of MSetInterface via AVL trees *)
+
+(** This module implements finite sets using AVL trees.
+    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 MSet interface. As a consequence,
+    balancing results are not part of this file anymore, they can
+    now be found in [MSetFullAVL].
+
+    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
+    [MSetFullAVL]. The structural variants compute faster in Coq,
+    whereas the other variants produce nicer and/or (slightly) faster
+    code after extraction.
+*)
+
+Require Import MSetInterface ZArith Int.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+(* for nicer extraction, we create only logical inductive principles *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
+(** * Ops : the pure functions *)
+
+Module Ops (Import I:Int)(X:OrderedType) <: WOps X.
+Local Open Scope Int_scope.
+Local Open Scope lazy_bool_scope.
+
+Definition elt := X.t.
+
+(** ** Trees
+
+   The fourth field of [Node] is the height of the tree *)
+
+Inductive tree :=
+  | Leaf : tree
+  | Node : tree -> X.t -> tree -> int -> tree.
+
+Definition t := tree.
+
+(** ** Basic functions on trees: height and cardinal *)
+
+Definition height (s : t) : int :=
+  match s with
+  | Leaf => 0
+  | Node _ _ _ h => h
+  end.
+
+Fixpoint cardinal (s : t) : nat :=
+  match s with
+   | Leaf => 0%nat
+   | Node l _ r _ => S (cardinal l + cardinal r)
+  end.
+
+(** ** Empty Set *)
+
+Definition empty := Leaf.
+
+(** ** Emptyness test *)
+
+Definition is_empty s :=
+  match s with Leaf => true | _ => false end.
+
+(** ** Appartness *)
+
+(** The [mem] function is deciding appartness. It exploits the
+    binary search tree invariant to achieve logarithmic complexity. *)
+
+Fixpoint mem x s :=
+   match s with
+     |  Leaf => false
+     |  Node l y r _ => match X.compare x y with
+             | Lt => mem x l
+             | Eq => true
+             | Gt => mem x r
+         end
+   end.
+
+(** ** Singleton set *)
+
+Definition singleton x := Node Leaf x Leaf 1.
+
+(** ** Helper functions *)
+
+(** [create l x r] creates a node, assuming [l] and [r]
+    to be balanced and [|height l - height r| <= 2]. *)
+
+Definition create l x r :=
+   Node l x r (max (height l) (height r) + 1).
+
+(** [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.
+
+Definition bal l x r :=
+  let hl := height l in
+  let hr := height r in
+  if gt_le_dec hl (hr+2) then
+    match l with
+     | 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 l x r
+          | Node lrl lrx lrr _ =>
+              create (create ll lx lrl) lrx (create lrr x r)
+         end
+    end
+  else
+    if gt_le_dec hr (hl+2) then
+      match r with
+       | 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 l x r
+            | Node rll rlx rlr _ =>
+                create (create l x rll) rlx (create rlr rx rr)
+           end
+      end
+    else
+      create l x r.
+
+(** ** Insertion *)
+
+Fixpoint add x s := match s with
+   | Leaf => Node Leaf x Leaf 1
+   | Node l y r h =>
+      match X.compare x y with
+         | Lt => bal (add x l) y r
+         | Eq => Node l y r h
+         | Gt => bal l y (add x r)
+      end
+  end.
+
+(** ** Join
+
+    Same as [bal] but does not assume anything regarding heights
+    of [l] and [r].
+*)
+
+Fixpoint join l : elt -> t -> t :=
+  match l with
+    | Leaf => add
+    | Node ll lx lr lh => fun x =>
+       fix join_aux (r:t) : t := match r with
+          | Leaf =>  add x l
+          | Node rl rx rr rh =>
+               if gt_le_dec lh (rh+2) then bal ll lx (join lr x r)
+               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr
+               else create l x r
+          end
+  end.
+
+(** ** Extraction of minimum element
+
+  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]).
+*)
+
+Fixpoint remove_min l x r : t*elt :=
+  match l with
+    | Leaf => (r,x)
+    | Node ll lx lr lh =>
+       let (l',m) := remove_min ll lx lr in (bal l' x r, m)
+  end.
+
+(** ** Merging two trees
+
+  [merge t1 t2] builds the union of [t1] and [t2] assuming all elements
+  of [t1] to be smaller than all elements of [t2], and
+  [|height t1 - height t2| <= 2].
+*)
+
+Definition merge s1 s2 :=  match s1,s2 with
+  | Leaf, _ => s2
+  | _, Leaf => s1
+  | _, Node l2 x2 r2 h2 =>
+        let (s2',m) := remove_min l2 x2 r2 in bal s1 m s2'
+end.
+
+(** ** Deletion *)
+
+Fixpoint remove x s := match s with
+  | Leaf => Leaf
+  | Node l y r h =>
+      match X.compare x y with
+         | Lt => bal (remove x l) y r
+         | Eq => merge l r
+         | Gt => bal l  y (remove x r)
+      end
+   end.
+
+(** ** Minimum element *)
+
+Fixpoint min_elt s := match s with
+   | Leaf => None
+   | Node Leaf y _  _ => Some y
+   | Node l _ _ _ => min_elt l
+end.
+
+(** ** Maximum element *)
+
+Fixpoint max_elt s := match s with
+   | Leaf => None
+   | Node _ y Leaf  _ => Some y
+   | Node _ _ r _ => max_elt r
+end.
+
+(** ** Any element *)
+
+Definition choose := min_elt.
+
+(** ** Concatenation
+
+    Same as [merge] but does not assume anything about heights.
+*)
+
+Definition concat s1 s2 :=
+   match s1, s2 with
+      | Leaf, _ => s2
+      | _, Leaf => s1
+      | _, Node l2 x2 r2 _ =>
+            let (s2',m) := remove_min l2 x2 r2 in
+            join s1 m s2'
+   end.
+
+(** ** Splitting
+
+    [split x s] returns a triple [(l, present, r)] where
+    - [l] is the set of elements of [s] that are [< x]
+    - [r] is the set of elements of [s] that are [> x]
+    - [present] is [true] if and only if [s] contains  [x].
+*)
+
+Record triple := mktriple { t_left:t; t_in:bool; t_right:t }.
+Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
+
+Fixpoint split x s : triple := match s with
+  | Leaf => << Leaf, false, Leaf >>
+  | Node l y r h =>
+     match X.compare x y with
+      | Lt => let (ll,b,rl) := split x l in << ll, b, join rl y r >>
+      | Eq => << l, true, r >>
+      | Gt => let (rl,b,rr) := split x r in << join l y rl, b, rr >>
+     end
+ end.
+
+(** ** Intersection *)
+
+Fixpoint inter s1 s2 := match s1, s2 with
+    | Leaf, _ => Leaf
+    | _, Leaf => Leaf
+    | Node l1 x1 r1 h1, _ =>
+            let (l2',pres,r2') := split x1 s2 in
+            if pres then join (inter l1 l2') x1 (inter r1 r2')
+            else concat (inter l1 l2') (inter r1 r2')
+    end.
+
+(** ** Difference *)
+
+Fixpoint diff s1 s2 := match s1, s2 with
+ | Leaf, _ => Leaf
+ | _, Leaf => s1
+ | Node l1 x1 r1 h1, _ =>
+    let (l2',pres,r2') := split x1 s2 in
+    if pres then concat (diff l1 l2') (diff r1 r2')
+    else join (diff l1 l2') x1 (diff r1 r2')
+end.
+
+(** ** Union *)
+
+(** 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 [MSetFullAVL].
+*)
+
+Fixpoint union s1 s2 :=
+ match s1, s2 with
+  | Leaf, _ => s2
+  | _, Leaf => s1
+  | Node l1 x1 r1 h1, _ =>
+     let (l2',_,r2') := split x1 s2 in
+     join (union l1 l2') x1 (union r1 r2')
+ end.
+
+(** ** Elements *)
+
+(** [elements_tree_aux acc t] catenates the elements of [t] in infix
+    order to the list [acc] *)
+
+Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t :=
+  match s with
+   | Leaf => acc
+   | Node l x r _ => elements_aux (x :: elements_aux acc r) l
+  end.
+
+(** then [elements] is an instanciation with an empty [acc] *)
+
+Definition elements := elements_aux nil.
+
+(** ** Filter *)
+
+Fixpoint filter_acc (f:elt->bool) acc s := match s with
+  | Leaf => acc
+  | Node l x r h =>
+     filter_acc f (filter_acc f (if f x then add x acc else acc) l) r
+ end.
+
+Definition filter f := filter_acc f Leaf.
+
+
+(** ** Partition *)
+
+Fixpoint partition_acc (f:elt->bool)(acc : t*t)(s : t) : t*t :=
+  match s with
+   | Leaf => acc
+   | Node l x r _ =>
+      let (acct,accf) := acc in
+      partition_acc f
+        (partition_acc f
+           (if f x then (add x acct, accf) else (acct, add x accf)) l) r
+  end.
+
+Definition partition f := partition_acc f (Leaf,Leaf).
+
+(** ** [for_all] and [exists] *)
+
+Fixpoint for_all (f:elt->bool) s := match s with
+  | Leaf => true
+  | Node l x r _ => f x &&& for_all f l &&& for_all f r
+end.
+
+Fixpoint exists_ (f:elt->bool) s := match s with
+  | Leaf => false
+  | Node l x r _ => f x ||| exists_ f l ||| exists_ f r
+end.
+
+(** ** Fold *)
+
+Fixpoint fold (A : Type) (f : elt -> A -> A)(s : t) : A -> A :=
+ fun a => match s with
+  | Leaf => a
+  | Node l x r _ => fold f r (f x (fold f l a))
+ end.
+Implicit Arguments fold [A].
+
+
+(** ** Subset *)
+
+(** 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
+   [MSetFullAVL].
+ *)
+
+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 => subsetl (subset l1) x1 l2 &&& subset r1 s2
+      | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2
+     end
+ end.
+
+(** ** 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 [MSetFullAVL]. 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 *)
+
+Inductive enumeration :=
+ | End : enumeration
+ | More : elt -> t -> enumeration -> enumeration.
+
+
+(** [cons t e] adds the elements of tree [t] on the head of
+    enumeration [e]. *)
+
+Fixpoint cons s e : enumeration :=
+ match s with
+  | Leaf => e
+  | Node l x r h => cons l (More x r e)
+ end.
+
+(** One step of comparison of elements *)
+
+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.
+
+(** Comparison of left tree, middle element, then right tree *)
+
+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.
+
+(** Initial continuation *)
+
+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).
+
+(** ** Equality test *)
+
+Definition equal s1 s2 : bool :=
+ match compare s1 s2 with
+  | Eq => true
+  | _ => false
+ end.
+
+End Ops.
+
+
+
+(** * MakeRaw
+
+   Functor of pure functions + a posteriori proofs of invariant
+   preservation *)
+
+Module MakeRaw (Import I:Int)(X:OrderedType) <: RawSets X.
+Include Ops I X.
+
+(** * Invariants *)
+
+(** ** Occurrence in a tree *)
+
+Inductive InT (x : elt) : tree -> Prop :=
+  | IsRoot : forall l r h y, X.eq x y -> InT x (Node l y r h)
+  | InLeft : forall l r h y, InT x l -> InT x (Node l y r h)
+  | InRight : forall l r h y, InT x r -> InT x (Node l y r h).
+
+Definition In := InT.
+
+(** ** Some shortcuts *)
+
+Definition Equal s s' := forall a : elt, InT a s <-> InT a s'.
+Definition Subset s s' := forall a : elt, InT a s -> InT a s'.
+Definition Empty s := forall a : elt, ~ InT a s.
+Definition For_all (P : elt -> Prop) s := forall x, InT x s -> P x.
+Definition Exists (P : elt -> Prop) s := exists x, InT x s /\ P x.
+
+(** ** Binary search trees *)
+
+(** [lt_tree x s]: all elements in [s] are smaller than [x]
+   (resp. greater for [gt_tree]) *)
+
+Definition lt_tree x s := forall y, InT y s -> X.lt y x.
+Definition gt_tree x s := forall y, InT y s -> X.lt x y.
+
+(** [bst t] : [t] is a binary search tree *)
+
+Inductive bst : tree -> Prop :=
+  | BSLeaf : bst Leaf
+  | BSNode : forall x l r h, bst l -> bst r ->
+     lt_tree x l -> gt_tree x r -> bst (Node l x r h).
+
+(** [bst] is the (decidable) invariant our trees will have to satisfy. *)
+
+Definition IsOk := bst.
+
+Class Ok (s:t) : Prop := ok : bst s.
+
+Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }.
+
+Fixpoint ltb_tree x s :=
+ match s with
+  | Leaf => true
+  | Node l y r _ =>
+     match X.compare x y with
+      | Gt => ltb_tree x l && ltb_tree x r
+      | _ => false
+     end
+ end.
+
+Fixpoint gtb_tree x s :=
+ match s with
+  | Leaf => true
+  | Node l y r _ =>
+     match X.compare x y with
+      | Lt => gtb_tree x l && gtb_tree x r
+      | _ => false
+     end
+ end.
+
+Fixpoint isok s :=
+ match s with
+  | Leaf => true
+  | Node l x r _ => isok l && isok r && ltb_tree x l && gtb_tree x r
+ end.
+
+
+(** * Correctness proofs *)
+
+Module Import MX := OrderedTypeFacts X.
+
+(** * Automation and dedicated tactics *)
+
+Scheme tree_ind := Induction for tree Sort Prop.
+
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Immediate MX.eq_sym.
+Local Hint Unfold In lt_tree gt_tree.
+Local Hint Constructors InT bst.
+Local Hint Unfold Ok.
+
+Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
+ "as" ident(s) :=
+ set (s:=Node l x r h) in *; clearbody s; clear l x r h.
+
+(** Automatic treatment of [Ok] hypothesis *)
+
+Ltac inv_ok := match goal with
+ | H:Ok (Node _ _ _ _) |- _ => inversion_clear H; inv_ok
+ | H:Ok Leaf |- _ => clear H; inv_ok
+ | H:bst ?x |- _ => change (Ok x) in H; inv_ok
+ | _ => idtac
+end.
+
+(** A tactic to repeat [inversion_clear] on all hyps of the
+    form [(f (Node _ _ _ _))] *)
+
+Ltac is_tree_constr c :=
+  match c with
+   | Leaf => idtac
+   | Node _ _ _ _ => idtac
+   | _ => fail
+  end.
+
+Ltac invtree f :=
+  match goal with
+     | H:f ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
+     | H:f _ ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
+     | H:f _ _ ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
+     | _ => idtac
+  end.
+
+Ltac inv := inv_ok; invtree InT.
+
+Ltac intuition_in := repeat progress (intuition; inv).
+
+(** Helper tactic concerning order of elements. *)
+
+Ltac order := match goal with
+ | U: lt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
+ | U: gt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
+ | _ => MX.order
+end.
+
+
+(** [isok] is indeed a decision procedure for [Ok] *)
+
+Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true.
+Proof.
+ induction s as [|l IHl y r IHr h]; simpl.
+ unfold lt_tree; intuition_in.
+ elim_compare x y.
+ split; intros; try discriminate. assert (X.lt y x) by auto. order.
+ split; intros; try discriminate. assert (X.lt y x) by auto. order.
+ rewrite !andb_true_iff, <-IHl, <-IHr.
+  unfold lt_tree; intuition_in; order.
+Qed.
+
+Lemma gtb_tree_iff : forall x s, gt_tree x s <-> gtb_tree x s = true.
+Proof.
+ induction s as [|l IHl y r IHr h]; simpl.
+ unfold gt_tree; intuition_in.
+ elim_compare x y.
+ split; intros; try discriminate. assert (X.lt x y) by auto. order.
+ rewrite !andb_true_iff, <-IHl, <-IHr.
+  unfold gt_tree; intuition_in; order.
+ split; intros; try discriminate. assert (X.lt x y) by auto. order.
+Qed.
+
+Lemma isok_iff : forall s, Ok s <-> isok s = true.
+Proof.
+ induction s as [|l IHl y r IHr h]; simpl.
+ intuition_in.
+ rewrite !andb_true_iff, <- IHl, <-IHr, <- ltb_tree_iff, <- gtb_tree_iff.
+ intuition_in.
+Qed.
+
+Instance isok_Ok s : isok s = true -> Ok s | 10.
+Proof. intros; apply <- isok_iff; auto. Qed.
+
+
+(** * Basic results about [In], [lt_tree], [gt_tree], [height] *)
+
+(** [In] is compatible with [X.eq] *)
+
+Lemma In_1 :
+ forall s x y, X.eq x y -> InT x s -> InT y s.
+Proof.
+ induction s; simpl; intuition_in; eauto.
+Qed.
+Local Hint Immediate In_1.
+
+Instance In_compat : Proper (X.eq==>eq==>iff) InT.
+Proof.
+apply proper_sym_impl_iff_2; auto with *.
+repeat red; intros; subst. apply In_1 with x; auto.
+Qed.
+
+Lemma In_node_iff :
+ forall l x r h y,
+  InT y (Node l x r h) <-> InT y l \/ X.eq y x \/ InT y r.
+Proof.
+ intuition_in.
+Qed.
+
+(** Results about [lt_tree] and [gt_tree] *)
+
+Lemma lt_leaf : forall x : elt, lt_tree x Leaf.
+Proof.
+ red; inversion 1.
+Qed.
+
+Lemma gt_leaf : forall x : elt, gt_tree x Leaf.
+Proof.
+ red; inversion 1.
+Qed.
+
+Lemma lt_tree_node :
+ forall (x y : elt) (l r : tree) (h : int),
+ lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y r h).
+Proof.
+ unfold lt_tree; intuition_in; order.
+Qed.
+
+Lemma gt_tree_node :
+ forall (x y : elt) (l r : tree) (h : int),
+ gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y r h).
+Proof.
+ unfold gt_tree; intuition_in; order.
+Qed.
+
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+
+Lemma lt_tree_not_in :
+ forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t.
+Proof.
+ intros; intro; order.
+Qed.
+
+Lemma lt_tree_trans :
+ forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t.
+Proof.
+ eauto.
+Qed.
+
+Lemma gt_tree_not_in :
+ forall (x : elt) (t : tree), gt_tree x t -> ~ InT x t.
+Proof.
+ intros; intro; order.
+Qed.
+
+Lemma gt_tree_trans :
+ forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t.
+Proof.
+ eauto.
+Qed.
+
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+
+(** * Inductions principles for some of the set operators *)
+
+Functional Scheme bal_ind := Induction for bal Sort Prop.
+Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
+Functional Scheme merge_ind := Induction for merge Sort Prop.
+Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
+Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.
+Functional Scheme concat_ind := Induction for concat Sort Prop.
+Functional Scheme inter_ind := Induction for inter Sort Prop.
+Functional Scheme diff_ind := Induction for diff Sort Prop.
+Functional Scheme union_ind := Induction for union Sort Prop.
+
+Ltac induct s x :=
+ induction s as [|l IHl x' r IHr h]; simpl; intros;
+ [|elim_compare x x'; intros; inv].
+
+
+(** * Notations and helper lemma about pairs and triples *)
+
+Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
+Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
+Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope.
+Notation "t #b" := (t_in t) (at level 9, format "t '#b'") : pair_scope.
+Notation "t #r" := (t_right t) (at level 9, format "t '#r'") : pair_scope.
+
+Open Local Scope pair_scope.
+
+
+(** * Empty set *)
+
+Lemma empty_spec : Empty empty.
+Proof.
+ intro; intro.
+ inversion H.
+Qed.
+
+Instance empty_ok : Ok empty.
+Proof.
+ auto.
+Qed.
+
+(** * Emptyness test *)
+
+Lemma is_empty_spec : forall s, is_empty s = true <-> Empty s.
+Proof.
+ destruct s as [|r x l h]; simpl; auto.
+ split; auto. red; red; intros; inv.
+ split; auto. try discriminate. intro H; elim (H x); auto.
+Qed.
+
+(** * Appartness *)
+
+Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
+Proof.
+ split.
+ induct s x; auto; try discriminate.
+ induct s x; intuition_in; order.
+Qed.
+
+
+(** * Singleton set *)
+
+Lemma singleton_spec : forall x y, InT y (singleton x) <-> X.eq y x.
+Proof.
+ unfold singleton; intuition_in.
+Qed.
+
+Instance singleton_ok x : Ok (singleton x).
+Proof.
+ unfold singleton; auto.
+Qed.
+
+
+
+(** * Helper functions *)
+
+Lemma create_spec :
+ forall l x r y,  InT y (create l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ unfold create; split; [ inversion_clear 1 | ]; intuition.
+Qed.
+
+Instance create_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (create l x r).
+Proof.
+ unfold create; auto.
+Qed.
+
+Lemma bal_spec : forall l x r y,
+ InT y (bal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ intros l x r; functional induction bal l x r; intros; try clear e0;
+ rewrite !create_spec; intuition_in.
+Qed.
+
+Instance bal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (bal l x r).
+Proof.
+ functional induction bal l x r; intros;
+ inv; repeat apply create_ok; auto; unfold create;
+ (apply lt_tree_node || apply gt_tree_node); auto;
+ (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
+Qed.
+
+
+(** * Insertion *)
+
+Lemma add_spec' : forall s x y,
+ InT y (add x s) <-> X.eq y x \/ InT y s.
+Proof.
+ induct s x; try rewrite ?bal_spec, ?IHl, ?IHr; intuition_in.
+ setoid_replace y with x'; eauto.
+Qed.
+
+Lemma add_spec : forall s x y `{Ok s},
+ InT y (add x s) <-> X.eq y x \/ InT y s.
+Proof. intros; apply add_spec'. Qed.
+
+Instance add_ok s x `(Ok s) : Ok (add x s).
+Proof.
+ induct s x; auto; apply bal_ok; auto;
+  intros y; rewrite add_spec'; intuition; order.
+Qed.
+
+
+Open Scope Int_scope.
+
+(** * Join *)
+
+(* Function/Functional Scheme 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];
+   [ | intros x r; induction r as [| rl Hrl rx rr _ rh]; unfold join;
+     [ | destruct (gt_le_dec lh (rh+2));
+       [ match goal with |- context b [ bal ?a ?b ?c] =>
+           replace (bal a b c)
+           with (bal ll lx (join lr x (Node rl rx rr rh))); [ | auto]
+         end
+       | destruct (gt_le_dec rh (lh+2));
+         [ match goal with |- context b [ bal ?a ?b ?c] =>
+             replace (bal a b c)
+             with (bal (join (Node ll lx lr lh) x rl) rx rr); [ | auto]
+           end
+         | ] ] ] ]; intros.
+
+Lemma join_spec : forall l x r y,
+ InT y (join l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ join_tac.
+ simpl.
+ rewrite add_spec'; intuition_in.
+ rewrite add_spec'; intuition_in.
+ rewrite bal_spec, Hlr; clear Hlr Hrl; intuition_in.
+ rewrite bal_spec, Hrl; clear Hlr Hrl; intuition_in.
+ apply create_spec.
+Qed.
+
+Instance join_ok : forall l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r),
+ Ok (join l x r).
+Proof.
+ join_tac; auto with *; inv; apply bal_ok; auto;
+ clear Hrl Hlr z; intro; intros; rewrite join_spec in *.
+ intuition; [ setoid_replace y with x | ]; eauto.
+ intuition; [ setoid_replace y with x | ]; eauto.
+Qed.
+
+
+(** * Extraction of minimum element *)
+
+Lemma remove_min_spec : forall l x r h y,
+ InT y (Node l x r h) <->
+  X.eq y (remove_min l x r)#2 \/ InT y (remove_min l x r)#1.
+Proof.
+ intros l x r; functional induction (remove_min l x r); simpl in *; intros.
+ intuition_in.
+ rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition.
+Qed.
+
+Instance remove_min_ok l x r : forall h `(Ok (Node l x r h)),
+ Ok (remove_min l x r)#1.
+Proof.
+ functional induction (remove_min l x r); simpl; intros.
+ inv; auto.
+ assert (O : Ok (Node ll lx lr _x)) by (inv; auto).
+ assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto).
+ specialize IHp with (1:=O); rewrite e0 in IHp; auto; simpl in *.
+ apply bal_ok; auto.
+ inv; auto.
+ intro y; specialize (L y).
+ rewrite remove_min_spec, e0 in L; simpl in L; intuition.
+ inv; auto.
+Qed.
+
+Lemma remove_min_gt_tree : forall l x r h `{Ok (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); simpl; intros.
+ inv; auto.
+ assert (O : Ok (Node ll lx lr _x)) by (inv; auto).
+ assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto).
+ specialize IHp with (1:=O); rewrite e0 in IHp; simpl in IHp.
+ intro y; rewrite bal_spec; intuition;
+  specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L;
+   [setoid_replace y with x|inv]; eauto.
+Qed.
+Local Hint Resolve remove_min_gt_tree.
+
+
+
+(** * Merging two trees *)
+
+Lemma merge_spec : forall s1 s2 y,
+ InT y (merge s1 s2) <-> InT y s1 \/ InT y s2.
+Proof.
+ intros s1 s2; functional induction (merge s1 s2); intros;
+ try factornode _x _x0 _x1 _x2 as s1.
+ intuition_in.
+ intuition_in.
+ rewrite bal_spec, remove_min_spec, e1; simpl; intuition.
+Qed.
+
+Instance merge_ok s1 s2 : forall `(Ok s1, Ok s2)
+ `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
+ Ok (merge s1 s2).
+Proof.
+ functional induction (merge s1 s2); intros; auto;
+ try factornode _x _x0 _x1 _x2 as s1.
+ apply bal_ok; auto.
+ change s2' with ((s2',m)#1); rewrite <-e1; eauto with *.
+ intros y Hy.
+ apply H1; auto.
+ rewrite remove_min_spec, e1; simpl; auto.
+ change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto.
+Qed.
+
+
+
+(** * Deletion *)
+
+Lemma remove_spec : forall s x y `{Ok s},
+ (InT y (remove x s) <-> InT y s /\ ~ X.eq y x).
+Proof.
+ induct s x.
+ intuition_in.
+ rewrite merge_spec; intuition; [order|order|intuition_in].
+ elim H6; eauto.
+ rewrite bal_spec, IHl; clear IHl IHr; intuition; [order|order|intuition_in].
+ rewrite bal_spec, IHr; clear IHl IHr; intuition; [order|order|intuition_in].
+Qed.
+
+Instance remove_ok s x `(Ok s) : Ok (remove x s).
+Proof.
+ induct s x.
+ auto.
+ (* EQ *)
+ apply merge_ok; eauto.
+ (* LT *)
+ apply bal_ok; auto.
+ intro z; rewrite remove_spec; auto; destruct 1; eauto.
+ (* GT *)
+ apply bal_ok; auto.
+ intro z; rewrite remove_spec; auto; destruct 1; eauto.
+Qed.
+
+
+(** * Minimum element *)
+
+Lemma min_elt_spec1 : forall s x, min_elt s = Some x -> InT x s.
+Proof.
+ intro s; functional induction (min_elt s); auto; inversion 1; auto.
+Qed.
+
+Lemma min_elt_spec2 : forall s x y `{Ok s},
+ min_elt s = Some x -> InT y s -> ~ X.lt y x.
+Proof.
+ intro s; functional induction (min_elt s);
+ try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1.
+ discriminate.
+ intros x y0 U V W.
+ inversion V; clear V; subst.
+ inv; order.
+ intros; inv; auto.
+ assert (X.lt x y) by (apply H4; apply min_elt_spec1; auto).
+ order.
+ assert (X.lt x1 y) by auto.
+ assert (~X.lt x1 x) by auto.
+ order.
+Qed.
+
+Lemma min_elt_spec3 : forall s, min_elt s = None -> Empty s.
+Proof.
+ intro s; functional induction (min_elt s).
+ red; red; inversion 2.
+ inversion 1.
+ intro H0.
+ destruct (IHo H0 _x2); auto.
+Qed.
+
+
+
+(** * Maximum element *)
+
+Lemma max_elt_spec1 : forall s x, max_elt s = Some x -> InT x s.
+Proof.
+ intro s; functional induction (max_elt s); auto; inversion 1; auto.
+Qed.
+
+Lemma max_elt_spec2 : forall s x y `{Ok s},
+ max_elt s = Some x -> InT y s -> ~ X.lt x y.
+Proof.
+ intro s; functional induction (max_elt s);
+ try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1.
+ discriminate.
+ intros x y0 U V W.
+ inversion V; clear V; subst.
+ inv; order.
+ intros; inv; auto.
+ assert (X.lt y x1) by auto.
+ assert (~ X.lt x x1) by auto.
+ order.
+ assert (X.lt y x) by (apply H5; apply max_elt_spec1; auto).
+ order.
+Qed.
+
+Lemma max_elt_spec3 : forall s, max_elt s = None -> Empty s.
+Proof.
+ intro s; functional induction (max_elt s).
+ red; auto.
+ inversion 1.
+ intros H0; destruct (IHo H0 _x2); auto.
+Qed.
+
+
+
+(** * Any element *)
+
+Lemma choose_spec1 : forall s x, choose s = Some x -> InT x s.
+Proof.
+ exact min_elt_spec1.
+Qed.
+
+Lemma choose_spec2 : forall s, choose s = None -> Empty s.
+Proof.
+ exact min_elt_spec3.
+Qed.
+
+Lemma choose_spec3 : forall s s' x x' `{Ok s, Ok s'},
+  choose s = Some x -> choose s' = Some x' ->
+  Equal s s' -> X.eq x x'.
+Proof.
+ unfold choose, Equal; intros s s' x x' Hb Hb' Hx Hx' H.
+ assert (~X.lt x x').
+  apply min_elt_spec2 with s'; auto.
+  rewrite <-H; auto using min_elt_spec1.
+ assert (~X.lt x' x).
+  apply min_elt_spec2 with s; auto.
+  rewrite H; auto using min_elt_spec1.
+ elim_compare x x'; intuition.
+Qed.
+
+
+(** * Concatenation *)
+
+Lemma concat_spec : forall s1 s2 y,
+ InT y (concat s1 s2) <-> InT y s1 \/ InT y s2.
+Proof.
+ intros s1 s2; functional induction (concat s1 s2); intros;
+ try factornode _x _x0 _x1 _x2 as s1.
+ intuition_in.
+ intuition_in.
+ rewrite join_spec, remove_min_spec, e1; simpl; intuition.
+Qed.
+
+Instance concat_ok s1 s2 : forall `(Ok s1, Ok s2)
+ `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
+ Ok (concat s1 s2).
+Proof.
+ functional induction (concat s1 s2); intros; auto;
+ try factornode _x _x0 _x1 _x2 as s1.
+ apply join_ok; auto.
+ change (Ok (s2',m)#1); rewrite <-e1; eauto with *.
+ intros y Hy.
+ apply H1; auto.
+ rewrite remove_min_spec, e1; simpl; auto.
+ change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto.
+Qed.
+
+
+
+(** * Splitting *)
+
+Lemma split_spec1 : forall s x y `{Ok s},
+ (InT y (split x s)#l <-> InT y s /\ X.lt y x).
+Proof.
+ induct s x.
+ intuition_in.
+ intuition_in; order.
+ specialize (IHl x y).
+ destruct (split x l); simpl in *. rewrite IHl; intuition_in; order.
+ specialize (IHr x y).
+ destruct (split x r); simpl in *. rewrite join_spec, IHr; intuition_in; order.
+Qed.
+
+Lemma split_spec2 : forall s x y `{Ok s},
+ (InT y (split x s)#r <-> InT y s /\ X.lt x y).
+Proof.
+ induct s x.
+ intuition_in.
+ intuition_in; order.
+ specialize (IHl x y).
+ destruct (split x l); simpl in *. rewrite join_spec, IHl; intuition_in; order.
+ specialize (IHr x y).
+ destruct (split x r); simpl in *. rewrite IHr; intuition_in; order.
+Qed.
+
+Lemma split_spec3 : forall s x `{Ok s},
+ ((split x s)#b = true <-> InT x s).
+Proof.
+ induct s x.
+ intuition_in; try discriminate.
+ intuition.
+ specialize (IHl x).
+ destruct (split x l); simpl in *. rewrite IHl; intuition_in; order.
+ specialize (IHr x).
+ destruct (split x r); simpl in *. rewrite IHr; intuition_in; order.
+Qed.
+
+Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r.
+Proof.
+ induct s x; simpl; auto.
+ specialize (IHl x).
+ generalize (fun y => @split_spec2 _ x y H1).
+ destruct (split x l); simpl in *; intuition. apply join_ok; auto.
+ intros y; rewrite H; intuition.
+ specialize (IHr x).
+ generalize (fun y => @split_spec1 _ x y H2).
+ destruct (split x r); simpl in *; intuition. apply join_ok; auto.
+ intros y; rewrite H; intuition.
+Qed.
+
+Instance split_ok1 s x `(Ok s) : Ok (split x s)#l.
+Proof. intros; destruct (@split_ok s x); auto. Qed.
+
+Instance split_ok2 s x `(Ok s) : Ok (split x s)#r.
+Proof. intros; destruct (@split_ok s x); auto. Qed.
+
+
+(** * Intersection *)
+
+Ltac destruct_split := match goal with
+ | H : split ?x ?s = << ?u, ?v, ?w >> |- _ =>
+   assert ((split x s)#l = u) by (rewrite H; auto);
+   assert ((split x s)#b = v) by (rewrite H; auto);
+   assert ((split x s)#r = w) by (rewrite H; auto);
+   clear H; subst u w
+ end.
+
+Lemma inter_spec_ok : forall s1 s2 `{Ok s1, Ok s2},
+ Ok (inter s1 s2) /\ (forall y, InT y (inter s1 s2) <-> InT y s1 /\ InT y s2).
+Proof.
+ intros s1 s2; functional induction inter s1 s2; intros B1 B2;
+ [intuition_in|intuition_in | | ];
+ factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv;
+ destruct IHt0 as (IHo1,IHi1), IHt1 as (IHo2,IHi2); auto with *;
+ split; intros.
+ (* Ok join *)
+ apply join_ok; auto with *; intro y; rewrite ?IHi1, ?IHi2; intuition.
+ (* InT join *)
+ rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in.
+ setoid_replace y with x1; auto. rewrite <- split_spec3; auto.
+ (* Ok concat *)
+ apply concat_ok; auto with *; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
+ (* InT concat *)
+ rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; auto.
+ intuition_in.
+ absurd (InT x1 s2).
+  rewrite <- split_spec3; auto; congruence.
+  setoid_replace x1 with y; auto.
+Qed.
+
+Lemma inter_spec : forall s1 s2 y `{Ok s1, Ok s2},
+ (InT y (inter s1 s2) <-> InT y s1 /\ InT y s2).
+Proof. intros; destruct (@inter_spec_ok s1 s2); auto. Qed.
+
+Instance inter_ok s1 s2 `(Ok s1, Ok s2) : Ok (inter s1 s2).
+Proof. intros; destruct (@inter_spec_ok s1 s2); auto. Qed.
+
+
+(** * Difference *)
+
+Lemma diff_spec_ok : forall s1 s2 `{Ok s1, Ok s2},
+ Ok (diff s1 s2) /\ (forall y, InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2).
+Proof.
+ intros s1 s2; functional induction diff s1 s2; intros B1 B2;
+ [intuition_in|intuition_in | | ];
+ factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv;
+ destruct IHt0 as (IHb1,IHi1), IHt1 as (IHb2,IHi2); auto with *;
+ split; intros.
+ (* Ok concat *)
+ apply concat_ok; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
+ (* InT concat *)
+ rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in.
+ absurd (InT x1 s2).
+  setoid_replace x1 with y; auto.
+  rewrite <- split_spec3; auto; congruence.
+ (* Ok join *)
+ apply join_ok; auto; intro y; rewrite ?IHi1, ?IHi2; intuition.
+ (* InT join *)
+ rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; auto with *.
+ intuition_in.
+ absurd (InT x1 s2); auto.
+  rewrite <- split_spec3; auto; congruence.
+  setoid_replace x1 with y; auto.
+Qed.
+
+Lemma diff_spec : forall s1 s2 y `{Ok s1, Ok s2},
+ (InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2).
+Proof. intros; destruct (@diff_spec_ok s1 s2); auto. Qed.
+
+Instance diff_ok s1 s2 `(Ok s1, Ok s2) : Ok (diff s1 s2).
+Proof. intros; destruct (@diff_spec_ok s1 s2); auto. Qed.
+
+
+(** * Union *)
+
+Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2},
+ (InT y (union s1 s2) <-> InT y s1 \/ InT y s2).
+Proof.
+ intros s1 s2; functional induction union s1 s2; intros y B1 B2.
+ intuition_in.
+ intuition_in.
+ factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
+ rewrite join_spec, IHt0, IHt1, split_spec1, split_spec2; auto with *.
+ elim_compare y x1; intuition_in.
+Qed.
+
+Instance union_ok s1 s2 : forall `(Ok s1, Ok s2), Ok (union s1 s2).
+Proof.
+ functional induction union s1 s2; intros B1 B2; auto.
+ factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
+ apply join_ok; auto with *.
+ intro y; rewrite union_spec, split_spec1; intuition_in.
+ intro y; rewrite union_spec, split_spec2; intuition_in.
+Qed.
+
+
+(** * Elements *)
+
+Lemma elements_spec1' : forall s acc x,
+ InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc.
+Proof.
+ induction s as [ | l Hl x r Hr h ]; simpl; auto.
+ intuition.
+ inversion H0.
+ intros.
+ rewrite Hl.
+ destruct (Hr acc x0); clear Hl Hr.
+ intuition; inversion_clear H3; intuition.
+Qed.
+
+Lemma elements_spec1 : forall s x, InA X.eq x (elements s) <-> InT x s.
+Proof.
+ intros; generalize (elements_spec1' s nil x); intuition.
+ inversion_clear H0.
+Qed.
+
+Lemma elements_spec2' : forall s acc `{Ok s}, sort X.lt acc ->
+ (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) ->
+ sort X.lt (elements_aux acc s).
+Proof.
+ induction s as [ | l Hl y r Hr h]; simpl; intuition.
+ inv.
+ apply Hl; auto.
+ constructor.
+ apply Hr; auto.
+ eapply InA_InfA; eauto with *.
+ intros.
+ destruct (elements_spec1' r acc y0); intuition.
+ intros.
+ inversion_clear H.
+ order.
+ destruct (elements_spec1' r acc x); intuition eauto.
+Qed.
+
+Lemma elements_spec2 : forall s `(Ok s), sort X.lt (elements s).
+Proof.
+ intros; unfold elements; apply elements_spec2'; auto.
+ intros; inversion H0.
+Qed.
+Local Hint Resolve elements_spec2.
+
+Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s).
+Proof.
+ intros. eapply SortA_NoDupA; eauto with *.
+Qed.
+
+Lemma elements_aux_cardinal :
+ forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s).
+Proof.
+ simple induction s; simpl in |- *; intuition.
+ rewrite <- H.
+ simpl in |- *.
+ rewrite <- H0; omega.
+Qed.
+
+Lemma elements_cardinal : forall s : tree, cardinal s = length (elements s).
+Proof.
+ exact (fun s => elements_aux_cardinal s nil).
+Qed.
+
+Definition cardinal_spec (s:t)(Hs:Ok s) := elements_cardinal s.
+
+Lemma elements_app :
+ forall s acc, elements_aux acc s = elements s ++ acc.
+Proof.
+ induction s; simpl; intros; auto.
+ rewrite IHs1, IHs2.
+ unfold elements; simpl.
+ rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto.
+Qed.
+
+Lemma elements_node :
+ forall l x r h acc,
+ elements l ++ x :: elements r ++ acc =
+ elements (Node l x r h) ++ acc.
+Proof.
+ unfold elements; simpl; intros; auto.
+ rewrite !elements_app, <- !app_nil_end, !app_ass; auto.
+Qed.
+
+
+(** * Filter *)
+
+Lemma filter_spec' : forall s x acc f,
+ Proper (X.eq==>eq) f ->
+ (InT x (filter_acc f acc s) <-> InT x acc \/ InT x s /\ f x = true).
+Proof.
+ induction s; simpl; intros.
+ intuition_in.
+ rewrite IHs2, IHs1 by (destruct (f t0); auto).
+ case_eq (f t0); intros.
+ rewrite add_spec'; auto.
+ intuition_in.
+ rewrite (H _ _ H2).
+ intuition.
+ intuition_in.
+ rewrite (H _ _ H2) in H3.
+ rewrite H0 in H3; discriminate.
+Qed.
+
+Instance filter_ok' : forall s acc f `(Ok s, Ok acc),
+ Ok (filter_acc f acc s).
+Proof.
+ induction s; simpl; auto.
+ intros. inv.
+ destruct (f t0); auto with *.
+Qed.
+
+Lemma filter_spec : forall s x f,
+ Proper (X.eq==>eq) f ->
+ (InT x (filter f s) <-> InT x s /\ f x = true).
+Proof.
+ unfold filter; intros; rewrite filter_spec'; intuition_in.
+Qed.
+
+Instance filter_ok s f `(Ok s) : Ok (filter f s).
+Proof.
+ unfold filter; intros; apply filter_ok'; auto.
+Qed.
+
+
+(** * Partition *)
+
+Lemma partition_spec1' : forall s acc f,
+ Proper (X.eq==>eq) f -> forall x : elt,
+ InT x (partition_acc f acc s)#1 <->
+ InT x acc#1 \/ InT x s /\ f x = true.
+Proof.
+ induction s; simpl; intros.
+ intuition_in.
+ destruct acc as [acct accf]; simpl in *.
+ rewrite IHs2 by
+  (destruct (f t0); auto; apply partition_acc_avl_1; simpl; auto).
+ rewrite IHs1 by (destruct (f t0); simpl; auto).
+ case_eq (f t0); simpl; intros.
+ rewrite add_spec'; auto.
+ intuition_in.
+ rewrite (H _ _ H2).
+ intuition.
+ intuition_in.
+ rewrite (H _ _ H2) in H3.
+ rewrite H0 in H3; discriminate.
+Qed.
+
+Lemma partition_spec2' : forall s acc f,
+ Proper (X.eq==>eq) f -> forall x : elt,
+ InT x (partition_acc f acc s)#2 <->
+ InT x acc#2 \/ InT x s /\ f x = false.
+Proof.
+ induction s; simpl; intros.
+ intuition_in.
+ destruct acc as [acct accf]; simpl in *.
+ rewrite IHs2 by
+  (destruct (f t0); auto; apply partition_acc_avl_2; simpl; auto).
+ rewrite IHs1 by (destruct (f t0); simpl; auto).
+ case_eq (f t0); simpl; intros.
+ intuition.
+ intuition_in.
+ rewrite (H _ _ H2) in H3.
+ rewrite H0 in H3; discriminate.
+ rewrite add_spec'; auto.
+ intuition_in.
+ rewrite (H _ _ H2).
+ intuition.
+Qed.
+
+Lemma partition_spec1 : forall s f,
+ Proper (X.eq==>eq) f ->
+ Equal (partition f s)#1 (filter f s).
+Proof.
+ unfold partition; intros s f P x.
+ rewrite partition_spec1', filter_spec; simpl; intuition_in.
+Qed.
+
+Lemma partition_spec2 : forall s f,
+ Proper (X.eq==>eq) f ->
+ Equal (partition f s)#2 (filter (fun x => negb (f x)) s).
+Proof.
+ unfold partition; intros s f P x.
+ rewrite partition_spec2', filter_spec; simpl; intuition_in.
+ rewrite H1; auto.
+ right; split; auto.
+ rewrite negb_true_iff in H1; auto.
+ intros u v H; rewrite H; auto.
+Qed.
+
+Instance partition_ok1' : forall s acc f `(Ok s, Ok acc#1),
+ Ok (partition_acc f acc s)#1.
+Proof.
+ induction s; simpl; auto.
+ destruct acc as [acct accf]; simpl in *.
+ intros. inv.
+ destruct (f t0); auto.
+ apply IHs2; simpl; auto.
+ apply IHs1; simpl; auto with *.
+Qed.
+
+Instance partition_ok2' : forall s acc f `(Ok s, Ok acc#2),
+ Ok (partition_acc f acc s)#2.
+Proof.
+ induction s; simpl; auto.
+ destruct acc as [acct accf]; simpl in *.
+ intros. inv.
+ destruct (f t0); auto.
+ apply IHs2; simpl; auto.
+ apply IHs1; simpl; auto with *.
+Qed.
+
+Instance partition_ok1 s f `(Ok s) : Ok (partition f s)#1.
+Proof. apply partition_ok1'; auto. Qed.
+
+Instance partition_ok2 s f `(Ok s) : Ok (partition f s)#2.
+Proof. apply partition_ok2'; auto. Qed.
+
+
+
+(** * [for_all] and [exists] *)
+
+Lemma for_all_spec : forall s f, Proper (X.eq==>eq) f ->
+ (for_all f s = true <-> For_all (fun x => f x = true) s).
+Proof.
+ split.
+ induction s; simpl; auto; intros; red; intros; inv.
+ destruct (andb_prop _ _ H0); auto.
+ destruct (andb_prop _ _ H1); eauto.
+ apply IHs1; auto.
+ destruct (andb_prop _ _ H0); auto.
+ destruct (andb_prop _ _ H1); auto.
+ apply IHs2; auto.
+ destruct (andb_prop _ _ H0); auto.
+ (* <- *)
+ induction s; simpl; auto.
+ intros. red in H0.
+ rewrite IHs1; try red; auto.
+ rewrite IHs2; try red; auto.
+ generalize (H0 t0).
+ destruct (f t0); simpl; auto.
+Qed.
+
+Lemma exists_spec : forall s f, Proper (X.eq==>eq) f ->
+ (exists_ f s = true <-> Exists (fun x => f x = true) s).
+Proof.
+ split.
+ induction s; simpl; intros; rewrite <- ?orb_lazy_alt in *.
+ discriminate.
+ destruct (orb_true_elim _ _ H0) as [H1|H1].
+ destruct (orb_true_elim _ _ H1) as [H2|H2].
+ exists t0; auto.
+ destruct (IHs1 H2); auto; exists x; intuition.
+ destruct (IHs2 H1); auto; exists x; intuition.
+ (* <- *)
+ induction s; simpl; destruct 1 as (x,(U,V)); inv; rewrite <- ?orb_lazy_alt.
+ rewrite (H _ _ (MX.eq_sym H0)); rewrite V; auto.
+ apply orb_true_intro; left.
+ apply orb_true_intro; right; apply IHs1; auto; exists x; auto.
+ apply orb_true_intro; right; apply IHs2; auto; exists x; auto.
+Qed.
+
+
+(** * Fold *)
+
+Lemma fold_spec' :
+ forall (A : Type) (f : elt -> A -> A) (s : tree) (i : A) (acc : list elt),
+ fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i).
+Proof.
+ induction s as [|l IHl x r IHr h]; simpl; intros; auto.
+ rewrite IHl.
+ simpl. unfold flip at 2.
+ apply IHr.
+Qed.
+
+Lemma fold_spec :
+ forall (s:t) (A : Type) (i : A) (f : elt -> A -> A),
+ fold f s i = fold_left (flip f) (elements s) i.
+Proof.
+ unfold elements.
+ induction s as [|l IHl x r IHr h]; simpl; intros; auto.
+ rewrite fold_spec'.
+ rewrite IHr.
+ simpl; auto.
+Qed.
+
+
+(** * Subset *)
+
+Lemma subsetl_spec : forall subset_l1 l1 x1 h1 s2
+ `{Ok (Node l1 x1 Leaf h1), Ok s2},
+ (forall s `{Ok s}, (subset_l1 s = true <-> Subset l1 s)) ->
+ (subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ).
+Proof.
+ induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
+ unfold Subset; intuition; try discriminate.
+ assert (H': InT x1 Leaf) by auto; inversion H'.
+ specialize (IHl2 H).
+ specialize (IHr2 H).
+ inv.
+ elim_compare x1 x2.
+
+ rewrite H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite IHl2 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ constructor 3. setoid_replace a with x1; auto. rewrite <- mem_spec; auto.
+ rewrite mem_spec; auto.
+ assert (InT x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+Qed.
+
+
+Lemma subsetr_spec : 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.
+ induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
+ unfold Subset; intuition; try discriminate.
+ assert (H': InT x1 Leaf) by auto; inversion H'.
+ specialize (IHl2 H).
+ specialize (IHr2 H).
+ inv.
+ elim_compare x1 x2.
+
+ rewrite H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto;  clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ constructor 2. setoid_replace a with x1; auto. rewrite <- mem_spec; auto.
+ rewrite mem_spec; auto.
+ assert (InT x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite IHr2 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+Qed.
+
+Lemma subset_spec : forall s1 s2 `{Ok s1, Ok 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': InT x1 Leaf) by auto; inversion H'.
+ inv.
+ elim_compare x1 x2.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto.
+ clear IHl1 IHr1.
+ unfold Subset; intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto.
+ rewrite (@subsetl_spec (subset l1) l1 x1 h1) by auto.
+ clear IHl1 IHr1.
+ unfold Subset; intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto.
+ rewrite (@subsetr_spec (subset r1) r1 x1 h1) by auto.
+ clear IHl1 IHr1.
+ unfold Subset; intuition_in.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+ assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
+Qed.
+
+
+(** * Comparison *)
+
+(** ** Relations [eq] and [lt] over trees *)
+
+Module L := MakeListOrdering X.
+
+Definition eq := Equal.
+Instance eq_equiv : Equivalence eq.
+Proof. firstorder. Qed.
+
+Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
+Proof.
+ unfold eq, Equal, L.eq; intros.
+ setoid_rewrite elements_spec1; firstorder.
+Qed.
+
+Definition lt (s1 s2 : t) : Prop :=
+ exists s1', exists s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
+   /\ L.lt (elements s1') (elements s2').
+
+Instance lt_strorder : StrictOrder lt.
+Proof.
+ split.
+ intros s (s1 & s2 & B1 & B2 & E1 & E2 & L).
+ assert (eqlistA X.eq (elements s1) (elements s2)).
+  apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
+  rewrite <- eq_Leq. transitivity s; auto. symmetry; auto.
+ rewrite H in L.
+ apply (StrictOrder_Irreflexive (elements s2)); auto.
+ intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
+                 (s2'' & s3' & B2' & B3 & E2' & E3 & L23).
+ exists s1', s3'; do 4 (split; trivial).
+ assert (eqlistA X.eq (elements s2') (elements s2'')).
+  apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
+  rewrite <- eq_Leq. transitivity s2; auto. symmetry; auto.
+ transitivity (elements s2'); auto.
+ rewrite H; auto.
+Qed.
+
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Proof.
+ intros s1 s2 E12 s3 s4 E34. split.
+ intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
+ exists s1', s3'; do 2 (split; trivial).
+  split. transitivity s1; auto. symmetry; auto.
+  split; auto. transitivity s3; auto. symmetry; auto.
+ intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
+ exists s1', s3'; do 2 (split; trivial).
+  split. transitivity s2; auto.
+  split; auto. transitivity s4; auto.
+Qed.
+
+
+(** * Proof of the comparison algorithm *)
+
+(** [flatten_e e] returns the list of elements of [e] i.e. the list
+    of elements actually compared *)
+
+Fixpoint flatten_e (e : enumeration) : list elt := match e with
+  | End => nil
+  | More x t r => x :: elements t ++ flatten_e r
+ end.
+
+Lemma flatten_e_elements :
+ 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 elements_node.
+Qed.
+
+Lemma cons_1 : forall s e,
+  flatten_e (cons s e) = elements s ++ flatten_e e.
+Proof.
+ induction s; simpl; auto; intros.
+ rewrite IHs1; apply flatten_e_elements.
+Qed.
+
+(** Correctness of this comparison *)
+
+Definition Cmp c x y := CompSpec L.eq L.lt x y c.
+
+Local Hint Unfold Cmp flip.
+
+Lemma compare_end_Cmp :
+ forall e2, Cmp (compare_end e2) nil (flatten_e e2).
+Proof.
+ destruct e2; simpl; constructor; auto. reflexivity.
+Qed.
+
+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.
+ simpl; intros; elim_compare x1 x2; simpl; auto.
+Qed.
+
+Lemma compare_cont_Cmp : forall s1 cont e2 l,
+ (forall e, Cmp (cont e) l (flatten_e e)) ->
+ Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
+Proof.
+ induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto.
+ rewrite <- elements_node; simpl.
+ apply Hl1; auto. clear e2. intros [|x2 r2 e2].
+ simpl; auto.
+ apply compare_more_Cmp.
+ rewrite <- cons_1; auto.
+Qed.
+
+Lemma compare_Cmp : forall s1 s2,
+ Cmp (compare s1 s2) (elements s1) (elements s2).
+Proof.
+ intros; unfold compare.
+ rewrite (app_nil_end (elements s1)).
+ replace (elements s2) with (flatten_e (cons s2 End)) by
+  (rewrite cons_1; simpl; rewrite <- app_nil_end; auto).
+ apply compare_cont_Cmp; auto.
+ intros.
+ apply compare_end_Cmp; auto.
+Qed.
+
+Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
+ CompSpec eq lt s1 s2 (compare s1 s2).
+Proof.
+ intros.
+ destruct (compare_Cmp s1 s2); constructor.
+ rewrite eq_Leq; auto.
+ intros; exists s1, s2; repeat split; auto.
+ intros; exists s2, s1; repeat split; auto.
+Qed.
+
+
+(** * Equality test *)
+
+Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2},
+ equal s1 s2 = true <-> eq s1 s2.
+Proof.
+unfold equal; intros s1 s2 B1 B2.
+destruct (@compare_spec s1 s2 B1 B2) as [H|H|H];
+ split; intros H'; auto; try discriminate.
+rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
+rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
+Qed.
+
+End MakeRaw.
+
+
+
+(** * Encapsulation
+
+   Now, in order to really provide a functor implementing [S], we
+   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 [MSetFullAVL] if you need more than just the MSet interface.
+*)
+
+Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
+ Module Raw := MakeRaw I X.
+ Include Raw2Sets X Raw.
+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).