Rework of FMapAVL inspired by recent changes of FSetAVL:

 * pure functions comes first, proofs are isolated in a sub-module
 * lazy (&&&) = if ... then ... else true instead of strict (&&) = andb
 * equal and compare done via continuations
 * a more clever map2_opt suggested by B. Gregoire: no more 
    intermediate conversion to lists, some sub-functions can handle 
    trivial situations, etc.
 * map2 is now done via map2_opt and another new iterator: map_option.
   By the way, this map_option allows to define easily an efficient
   filter function. Both map2_opt and map_option are currently not 
   available through FMapInterface.S, but they can be used by direct
   reference to the underlying Raw module.



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

1 files changed, 1318 insertions, 841 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 556d6225a..31c3baca4 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -11,34 +11,34 @@
 
 (* $Id$ *)
 
-(** This module implements map using AVL trees.
-    It follows the implementation from Ocaml's standard library. *)
+(** * FMapAVL *)
 
-Require Import Recdef FMapInterface FMapList ZArith Int.
+(** This module implements maps using AVL trees.
+    It follows the implementation from Ocaml's standard library. 
+    
+    See the comments at the beginning of FSetAVL for more details.
+*)
+
+Require Import FMapInterface FMapList ZArith Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (Import I:Int)(X: OrderedType).
-Module Import II:=MoreInt(I).
-Open Local Scope Int_scope.
-Module MX := OrderedTypeFacts X.
-Module PX := KeyOrderedType X.
-Module L := FMapList.Raw X.
-
-Definition key := X.t.
-
 (** Notations and helper lemma about pairs *)
 
-Notation "s #1" := (fst s) (at level 9, format "s '#1'").
-Notation "s #2" := (snd s) (at level 9, format "s '#2'").
+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.
 
-Lemma distr_pair : forall (A B:Type)(s:A*B)(a:A)(b:B), s = (a,b) -> 
- s#1 = a /\ s#2 = b.
-Proof.
- destruct s; simpl; injection 1; auto.
-Qed.
+(** * The Raw functor
+   
+   Functor of pure functions + separate proofs of invariant 
+   preservation *)
 
+Module Raw (Import I:Int)(X: OrderedType).
+Open Local Scope pair_scope.
+Open Local Scope Int_scope.
+
+Definition key := X.t.
 
 (** * Trees *)
 
@@ -58,21 +58,377 @@ Notation t := tree.
 
 (** * Basic functions on trees: height and cardinal *)
 
-Definition height (s : tree) : int :=
-  match s with
+Definition height (m : t) : int :=
+  match m with
   | Leaf => 0
   | Node _ _ _ _ h => h
   end.
 
-Fixpoint cardinal (s : tree) : nat :=
-  match s with
+Fixpoint cardinal (m : t) : nat :=
+  match m with
    | Leaf => 0%nat
    | Node l _ _ r _ => S (cardinal l + cardinal r)
   end.
 
-(** * Occurrence in a tree *)
+(** * Empty Map *)
+
+Definition empty := Leaf.
+
+(** * Emptyness test *)
+
+Definition is_empty m := match m with Leaf => true | _ => false end.
+
+(** * Appartness *)
+
+(** The [mem] function is deciding appartness. It exploits the [bst] property
+    to achieve logarithmic complexity. *)
+
+Fixpoint mem x m : bool :=
+   match m 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.
+
+Fixpoint find x m : option elt := 
+   match m with 
+     |  Leaf => None 
+     |  Node l y d r _ => match X.compare x y with 
+             | LT _ => find x l 
+             | EQ _ => Some d
+             | GT _ => find x r
+         end
+   end.
+
+(** * 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 e r := 
+   Node l x e r (max (height l) (height r) + 1).
+
+(** [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.
+
+Fixpoint bal l x d 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 d r
+     | Node ll lx ld lr _ => 
+       if ge_lt_dec (height ll) (height lr) then 
+         create ll lx ld (create lr x d r)
+       else 
+         match lr with 
+          | Leaf => assert_false l x d r
+          | Node lrl lrx lrd lrr _ => 
+              create (create ll lx ld lrl) lrx lrd (create lrr x d r)
+         end
+    end
+  else 
+    if gt_le_dec hr (hl+2) then 
+      match r with
+       | Leaf => assert_false l x d r
+       | Node rl rx rd rr _ =>
+         if ge_lt_dec (height rr) (height rl) then 
+            create (create l x d rl) rx rd rr
+         else 
+           match rl with
+            | Leaf => assert_false l x d r
+            | Node rll rlx rld rlr _ => 
+                create (create l x d rll) rlx rld (create rlr rx rd rr) 
+           end
+      end
+    else 
+      create l x d r.
+
+(** * Insertion *)
+
+Fixpoint add x d m := 
+  match m with 
+   | Leaf => Node Leaf x d Leaf 1
+   | Node l y d' r h => 
+      match X.compare x y with
+         | LT _ => bal (add x d l) y d' r
+         | EQ _ => Node l y d r h
+         | GT _ => bal l y d' (add x d r)
+      end
+  end.
+
+(** * Extraction of minimum binding
+
+  Morally, [remove_min] is to be applied to a non-empty tree 
+  [t = Node l x e 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 d r : t*(key*elt) := 
+  match l with
+    | Leaf => (r,(x,d))
+    | Node ll lx ld lr lh => 
+       let (l',m) := remove_min ll lx ld lr in 
+       (bal l' x d 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].
+*)
+
+Fixpoint merge s1 s2 :=  match s1,s2 with 
+  | Leaf, _ => s2 
+  | _, Leaf => s1
+  | _, Node l2 x2 d2 r2 h2 => 
+    match remove_min l2 x2 d2 r2 with 
+      (s2',(x,d)) => bal s1 x d s2'
+    end
+end.
+
+(** * Deletion *)
+
+Fixpoint remove x m := match m with 
+  | Leaf => Leaf
+  | Node l y d r h =>
+      match X.compare x y with
+         | LT _ => bal (remove x l) y d r
+         | EQ _ => merge l r
+         | GT _ => bal l y d (remove x r)
+      end
+   end.
+
+(** * join 
+    
+    Same as [bal] but does not assume anything regarding heights of [l] 
+    and [r].
+*)
+
+Fixpoint join l : key -> elt -> t -> t :=
+  match l with
+    | Leaf => add
+    | Node ll lx ld lr lh => fun x d => 
+       fix join_aux (r:t) : t := match r with 
+          | Leaf =>  add x d l
+          | Node rl rx rd rr rh =>  
+               if gt_le_dec lh (rh+2) then bal ll lx ld (join lr x d r)
+               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr 
+               else create l x d r
+          end
+  end.
+
+(** * Splitting 
+
+    [split x m] returns a triple [(l, o, r)] where
+    - [l] is the set of elements of [m] that are [< x]
+    - [r] is the set of elements of [m] that are [> x]
+    - [o] is the result of [find x m].
+*)
+
+Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }.
+Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
+
+Fixpoint split x m : triple := match m with 
+  | Leaf => << Leaf, None, Leaf >>
+  | Node l y d r h => 
+     match X.compare x y with 
+      | LT _ => let (ll,o,rl) := split x l in << ll, o, join rl y d r >>
+      | EQ _ => << l, Some d, r >>
+      | GT _ => let (rl,o,rr) := split x r in << join l y d rl, o, rr >>
+     end
+ end.
+
+(** * Concatenation 
+
+   Same as [merge] but does not assume anything about heights.
+*)
+
+Definition concat m1 m2 :=
+   match m1, m2 with
+      | Leaf, _ => m2
+      | _ , Leaf => m1
+      | _, Node l2 x2 d2 r2 _ =>
+            let (m2',xd) := remove_min l2 x2 d2 r2 in 
+            join m1 xd#1 xd#2 m2'
+   end.
+
+(** * Elements *)
+
+(** [elements_tree_aux acc t] catenates the elements of [t] in infix
+    order to the list [acc] *)
+
+Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) :=
+  match m with
+   | Leaf => acc
+   | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l
+  end.
+
+(** then [elements] is an instanciation with an empty [acc] *)
+
+Definition elements := elements_aux nil.
+
+(** * Fold *)
+
+Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A := 
+ fun a => match m with
+  | Leaf => a
+  | Node l x d r _ => fold f r (f x d (fold f l a))
+ end.
+
+(** * Comparison *)
+
+Variable cmp : elt->elt->bool.
+
+(** ** Enumeration of the elements of a tree *)
+
+Inductive enumeration :=
+ | End : enumeration
+ | More : key -> elt -> t -> enumeration -> enumeration.
+
+(** [cons m e] adds the elements of tree [m] on the head of 
+    enumeration [e]. *)
+
+Fixpoint cons m e : enumeration := 
+ match m with 
+  | Leaf => e
+  | Node l x d r h => cons l (More x d r e)
+ end.
+
+(** One step of comparison of elements *)
+
+Definition equal_more x1 d1 (cont:enumeration->bool) e2 :=
+ match e2 with
+ | End => false
+ | More x2 d2 r2 e2 =>
+     match X.compare x1 x2 with
+      | EQ _ => cmp d1 d2 &&& cont (cons r2 e2)
+      | _ => false
+     end
+ end.
+
+(** Comparison of left tree, middle element, then right tree *)
+
+Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := 
+ match m1 with
+  | Leaf => cont e2
+  | Node l1 x1 d1 r1 _ =>
+     equal_cont l1 (equal_more x1 d1 (equal_cont r1 cont)) e2
+  end.
+
+(** Initial continuation *)
+
+Definition equal_end e2 := match e2 with End => true | _ => false end.
+
+(** The complete comparison *)
+
+Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End).
+
+End Elt.
+Notation t := tree.
+Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
+Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
+Notation "t #o" := (t_opt t) (at level 9, format "t '#o'").
+Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
+
+
+(** * Map *)
+
+Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := 
+  match m with 
+   | Leaf   => Leaf _
+   | Node l x d r h => Node (map f l) x (f d) (map f r) h
+  end.
+
+(* * Mapi *)
+
+Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
+  match m with 
+   | Leaf   => Leaf _
+   | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
+  end.
+
+(** * Map with removal *)
+
+Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
+  : t elt' := 
+  match m with 
+   | Leaf => Leaf _
+   | Node l x d r h => 
+      match f x d with 
+       | Some d' => join (map_option f l) x d' (map_option f r)
+       | None => concat (map_option f l) (map_option f r)
+      end
+  end.
+
+(** * Optimized map2
+  
+  Suggestion by B. Gregoire: a [map2] function with specialized 
+  arguments allowing to bypass some tree traversal. Instead of one 
+  [f0] of type [key -> option elt -> option elt' -> option elt''], 
+  we ask here for: 
+  - [f] which is a specialisation of [f0] when first option isn't [None]
+  - [mapl] treats a [tree elt] with [f0] when second option is [None]
+  - [mapr] treats a [tree elt'] with [f0] when first option is [None]
+
+  The idea is that [mapl] and [mapr] can be instantaneous (e.g. 
+  the identity or some constant function). 
+*)
+
+Section Map2_opt.
+Variable elt elt' elt'' : Type.
+Variable f : key -> elt -> option elt' -> option elt''.
+Variable mapl : t elt -> t elt''.
+Variable mapr : t elt' -> t elt''.
+
+Fixpoint map2_opt m1 m2 := 
+ match m1, m2 with 
+  | Leaf, _ => mapr m2 
+  | _, Leaf => mapl m1
+  | Node l1 x1 d1 r1 h1, _ => 
+     let (l2',o2,r2') := split x1 m2 in
+     match f x1 d1 o2 with 
+      | Some e => join (map2_opt l1 l2') x1 e (map2_opt r1 r2')
+      | None => concat (map2_opt l1 l2') (map2_opt r1 r2')
+     end
+ end.
+
+End Map2_opt.
+
+(** * Map2
+    
+    The [map2] function of the Map interface can be implemented 
+    via [map2_opt] and [map_option].
+*)
+
+Section Map2.
+Variable elt elt' elt'' : Type.
+Variable f : option elt -> option elt' -> option elt''.
+
+Definition map2 : t elt -> t elt' -> t elt'' := 
+ map2_opt 
+   (fun _ d o => f (Some d) o)
+   (map_option (fun _ d => f (Some d) None))
+   (map_option (fun _ d' => f None (Some d'))).
+
+End Map2.
+
+
 
-Inductive MapsTo (x : key)(e : elt) : tree -> Prop :=
+(** * Invariants *)
+
+Section Invariants.
+Variable elt : Type.
+
+(** ** Occurrence in a tree *)
+
+Inductive MapsTo (x : key)(e : elt) : t elt -> Prop :=
   | MapsRoot : forall l r h y,
       X.eq x y -> MapsTo x e (Node l y e r h)
   | MapsLeft : forall l r h y e', 
@@ -80,7 +436,7 @@ Inductive MapsTo (x : key)(e : elt) : tree -> Prop :=
   | MapsRight : forall l r h y e', 
       MapsTo x e r -> MapsTo x e (Node l y e' r h).
 
-Inductive In (x : key) : tree -> Prop :=
+Inductive In (x : key) : t elt -> Prop :=
   | InRoot : forall l r h y e,
       X.eq x y -> In x (Node l y e r h)
   | InLeft : forall l r h y e', 
@@ -88,36 +444,54 @@ Inductive In (x : key) : tree -> Prop :=
   | InRight : forall l r h y e', 
       In x r -> In x (Node l y e' r h).
 
-Definition In0 (k:key)(m:t) : Prop := exists e:elt, MapsTo k e m.
+Definition In0 k m := exists e:elt, MapsTo k e m.
 
-(** * Binary search trees *)
+(** ** 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:key, In y s -> X.lt y x.
-Definition gt_tree x s := forall y:key, In y s -> X.lt x y.
+Definition lt_tree x m := forall y, In y m -> X.lt y x.
+Definition gt_tree x m := forall y, In y m -> X.lt x y.
 
 (** [bst t] : [t] is a binary search tree *)
 
-Inductive bst : tree -> Prop :=
-  | BSLeaf : bst Leaf
+Inductive bst : t elt -> Prop :=
+  | BSLeaf : bst (Leaf _)
   | 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).
 
-(* We should end this section before the big proofs that follows, 
-    otherwise the discharge takes a lot of time. *)
-End Elt. 
+End Invariants.
 
-Notation t := tree.
 
+(** * Correctness proofs, isolated in a sub-module *)
+
+Module Proofs.
+ Module MX := OrderedTypeFacts X.
+ Module PX := KeyOrderedType X.
+ Module L := FMapList.Raw X.
 
+Functional Scheme mem_ind := Induction for mem Sort Prop.
+Functional Scheme find_ind := Induction for find Sort Prop.
+Functional Scheme bal_ind := Induction for bal Sort Prop. 
+Functional Scheme add_ind := Induction for add Sort Prop.
+Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
+Functional Scheme merge_ind := Induction for merge Sort Prop. 
+Functional Scheme remove_ind := Induction for remove Sort Prop.
+Functional Scheme concat_ind := Induction for concat Sort Prop.
+Functional Scheme split_ind := Induction for split Sort Prop.
+Functional Scheme map_option_ind := Induction for map_option Sort Prop.
+Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop.
 
 (** * Automation and dedicated tactics. *)
 
 Hint Constructors tree MapsTo In bst.
 Hint Unfold lt_tree gt_tree.
 
+Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) 
+ "as" ident(s) :=  
+ set (s:=Node l x d r h) in *; clearbody s; clear l x d r h.
+
 (** A tactic for cleaning hypothesis after use of functional induction. *)
 
 Ltac clearf :=
@@ -162,23 +536,26 @@ end.
 
 Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo).
 
+Section Elt.
+Variable elt:Type.
+Implicit Types m r : t elt.
 
 (** * Basic results about [MapsTo], [In], [lt_tree], [gt_tree], [height] *)
 
 (** Facts about [MapsTo] and [In]. *)
 
-Lemma MapsTo_In : forall elt k e (m:t elt), MapsTo k e m -> In k m.
+Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m.
 Proof.
  induction 1; auto.
 Qed.
 Hint Resolve MapsTo_In.
 
-Lemma In_MapsTo : forall elt k (m:t elt), In k m -> exists e, MapsTo k e m.
+Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m.
 Proof.
  induction 1; try destruct IHIn as (e,He); exists e; auto.
 Qed.
 
-Lemma In_alt : forall elt k (m:t elt), In0 k m <-> In k m.
+Lemma In_alt : forall k m, In0 k m <-> In k m.
 Proof. 
  split.
  intros (e,H); eauto.
@@ -186,20 +563,20 @@ Proof.
 Qed.
 
 Lemma MapsTo_1 :
- forall elt (m:t elt) x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m.
+ forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m.
 Proof.
  induction m; simpl; intuition_in; eauto.
 Qed.
 Hint Immediate MapsTo_1.
 
 Lemma In_1 : 
- forall elt (m:t elt) x y, X.eq x y -> In x m -> In y m.
+ forall m x y, X.eq x y -> In x m -> In y m.
 Proof.
- intros elt m x y; induction m; simpl; intuition_in; eauto.
+ intros m x y; induction m; simpl; intuition_in; eauto.
 Qed.
 
 Lemma In_node_iff : 
- forall elt (l:t elt) x e r h y, 
+ forall l 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.
@@ -207,23 +584,23 @@ Qed.
 
 (** Results about [lt_tree] and [gt_tree] *)
 
-Lemma lt_leaf : forall elt x, lt_tree x (Leaf elt).
+Lemma lt_leaf : forall x, lt_tree x (Leaf elt).
 Proof.
  unfold lt_tree in |- *; intros; intuition_in.
 Qed.
 
-Lemma gt_leaf : forall elt x, gt_tree x (Leaf elt).
+Lemma gt_leaf : forall x, gt_tree x (Leaf elt).
 Proof.
   unfold gt_tree in |- *; intros; intuition_in.
 Qed.
 
-Lemma lt_tree_node : forall elt x y (l:t elt) r e h, 
+Lemma lt_tree_node : forall x y l r e h, 
  lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h).
 Proof.
  unfold lt_tree in *; intuition_in; order.
 Qed.
 
-Lemma gt_tree_node : forall elt x y (l:t elt) r e h,
+Lemma gt_tree_node : forall x y l r e h,
  gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y e r h).
 Proof.
  unfold gt_tree in *; intuition_in; order.
@@ -231,25 +608,25 @@ Qed.
 
 Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 
-Lemma lt_left : forall elt x y (l: t elt) r e h, 
+Lemma lt_left : forall x y l r e h, 
  lt_tree x (Node l y e r h) -> lt_tree x l.
 Proof.
  intuition_in.
 Qed.
 
-Lemma lt_right : forall elt x y (l:t elt) r e h, 
+Lemma lt_right : forall x y l r e h, 
  lt_tree x (Node l y e r h) -> lt_tree x r.
 Proof.
  intuition_in.
 Qed.
 
-Lemma gt_left : forall elt x y (l:t elt) r e h, 
+Lemma gt_left : forall x y l r e h, 
  gt_tree x (Node l y e r h) -> gt_tree x l.
 Proof.
  intuition_in.
 Qed.
 
-Lemma gt_right : forall elt x y (l:t elt) r e h, 
+Lemma gt_right : forall x y l r e h, 
  gt_tree x (Node l y e r h) -> gt_tree x r.
 Proof.
  intuition_in.
@@ -258,43 +635,157 @@ Qed.
 Hint Resolve lt_left lt_right gt_left gt_right.
 
 Lemma lt_tree_not_in :
- forall elt x (t : t elt), lt_tree x t -> ~ In x t.
+ forall x m, lt_tree x m -> ~ In x m.
 Proof.
  intros; intro; generalize (H _ H0); order.
 Qed.
 
 Lemma lt_tree_trans :
- forall elt x y, X.lt x y -> forall (t:t elt), lt_tree x t -> lt_tree y t.
+ forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m.
 Proof.
  eauto.
 Qed.
 
 Lemma gt_tree_not_in :
- forall elt x (t : t elt), gt_tree x t -> ~ In x t.
+ forall x m, gt_tree x m -> ~ In x m.
 Proof.
  intros; intro; generalize (H _ H0); order.
 Qed.
 
 Lemma gt_tree_trans :
- forall elt x y, X.lt y x -> forall (t:t elt), gt_tree x t -> gt_tree y t.
+ forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m.
 Proof.
  eauto.
 Qed.
 
 Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 
+(** * Empty map *)
 
+Definition Empty m := forall (a:key)(e:elt) , ~ MapsTo a e m.
 
-(** * Helper functions *)
+Lemma empty_bst : bst (empty elt).
+Proof.
+ unfold empty; auto.
+Qed.
 
-(** [create l x r] creates a node, assuming [l] and [r]
-    to be balanced and [|height l - height r| <= 2]. *)
+Lemma empty_1 : Empty (empty elt).
+Proof.
+ unfold empty, Empty; intuition_in.
+Qed.
 
-Definition create elt (l:t elt) x e r := 
-   Node l x e r (max (height l) (height r) + 1).
+(** * Emptyness test *)
+
+Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. 
+Proof.
+ destruct m as [|r x e l h]; simpl; auto.
+ intro H; elim (H x e); auto.
+Qed.
+
+Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
+Proof. 
+ destruct m; simpl; intros; try discriminate; red; intuition_in.
+Qed.
+
+(** * Appartness *)
+
+Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
+Proof. 
+ intros m x; functional induction (mem x m); auto; intros; clearf;
+  inv bst; intuition_in; order.
+Qed.
+
+Lemma mem_2 : forall m x, mem x m = true -> In x m. 
+Proof. 
+ intros m x; functional induction (mem x m); auto; intros; discriminate.
+Qed.
+
+Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
+Proof. 
+ intros m x; functional induction (find x m); auto; intros; clearf;
+  inv bst; intuition_in; simpl; auto; 
+ try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto].
+Qed.
+
+Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
+Proof. 
+ intros m x; functional induction (find x m); subst; intros; clearf;
+  try discriminate.
+ constructor 2; auto.
+ inversion H; auto.
+ constructor 3; auto.
+Qed.
+
+Lemma find_iff : forall m x e, bst m -> 
+ (find x m = Some e <-> MapsTo x e m).
+Proof.
+ split; auto using find_1, find_2.
+Qed.
+
+Lemma find_in : forall m x, find x m <> None -> In x m.
+Proof.
+ intros.
+ case_eq (find x m); [intros|congruence].
+ apply MapsTo_In with e; apply find_2; auto. 
+Qed.
+
+Lemma in_find : forall m x, bst m -> In x m -> find x m <> None.
+Proof.
+ intros.
+ destruct (In_MapsTo H0) as (d,Hd).
+ rewrite (find_1 H Hd); discriminate.
+Qed.
+
+Lemma find_in_iff : forall m x, bst m -> 
+ (find x m <> None <-> In x m).
+Proof.
+ split; auto using find_in, in_find.
+Qed.
+
+Lemma not_find_iff : forall m x, bst m ->
+ (find x m = None <-> ~In x m).
+Proof.
+ split; intros.
+ red; intros.
+ elim (in_find H H1 H0).
+ case_eq (find x m); [ intros | auto ].
+ elim H0; apply find_in; congruence.
+Qed.
+
+Lemma find_find : forall m m' x, 
+ find x m = find x m' <-> 
+ (forall d, find x m = Some d <-> find x m' = Some d).
+Proof.
+ intros; destruct (find x m); destruct (find x m'); split; intros; 
+  try split; try congruence.
+ rewrite H; auto.
+ symmetry; rewrite <- H; auto.
+ rewrite H; auto.
+Qed.
+
+Lemma find_mapsto_equiv : forall m m' x, bst m -> bst m' ->
+ (find x m = find x m' <-> 
+  (forall d, MapsTo x d m <-> MapsTo x d m')).
+Proof.
+ intros m m' x Hm Hm'.
+ rewrite find_find.
+ split; intros H d; specialize H with d.
+ rewrite <- 2 find_iff; auto.
+ rewrite 2 find_iff; auto.
+Qed.
+
+Lemma find_in_equiv : forall m m' x, bst m -> bst m' -> 
+ find x m = find x m' -> 
+ (In x m <-> In x m').
+Proof.
+ split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ];
+  apply in_find; auto.
+Qed.
+
+(** * Helper functions *)
 
 Lemma create_bst : 
- forall elt (l:t elt) x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> 
+ forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> 
  bst (create l x e r).
 Proof.
  unfold create; auto.
@@ -302,309 +793,245 @@ Qed.
 Hint Resolve create_bst.
 
 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.
+ forall l x e r y,  
+  In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
  unfold create; split; [ inversion_clear 1 | ]; intuition.
 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 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 l x e r
-          | Node lrl lrx lre lrr _ => 
-              create (create ll lx le lrl) lrx lre (create lrr x e r)
-         end
-    end
-  else 
-    if gt_le_dec hr (hl+2) then 
-      match r with
-       | 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 l x e r
-            | Node rll rlx rle rlr _ => 
-                create (create l x e rll) rlx rle (create rlr rx re rr) 
-           end
-      end
-    else 
-      create l x e r. 
-
-Lemma bal_bst : forall elt (l:t elt) x e r, bst l -> bst r -> 
+Lemma bal_bst : forall l x e r, bst l -> bst r -> 
  lt_tree x l -> gt_tree x r -> bst (bal l x e r).
 Proof.
- intros elt l x e r; functional induction (bal l x e r); intros; clearf;
+ intros l x e r; functional induction (bal l x e r); intros; clearf;
  inv bst; repeat apply create_bst; auto; unfold create; try constructor;
  (apply lt_tree_node || apply gt_tree_node); auto; 
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
 Qed.
+Hint Resolve bal_bst.
 
-Lemma bal_in : forall elt (l:t elt) x e r y,
+Lemma bal_in : forall l 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;
+ intros l x e r; functional induction (bal l x e r); intros; clearf;
  rewrite !create_in; intuition_in.
 Qed.
 
-Lemma bal_mapsto : forall elt (l:t elt) x e r y e',
+Lemma bal_mapsto : forall l 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;
+ intros l x e r; functional induction (bal l x e r); intros; clearf;
  unfold assert_false, create; intuition_in.
 Qed.
 
+Lemma bal_find : forall l x e r y, 
+ bst l -> bst r -> lt_tree x l -> gt_tree x r ->
+ find y (bal l x e r) = find y (create l x e r).
+Proof.
+ intros; rewrite find_mapsto_equiv; auto; intros; apply bal_mapsto.
+Qed.
 
 (** * Insertion *)
 
-Function add (elt:Type)(x:key)(e:elt)(s:t elt) { struct s } : t elt := 
-  match s with 
-   | Leaf => Node (Leaf _) x e (Leaf _) 1
-   | Node l y e' r h => 
-      match X.compare x y with
-         | LT _ => bal (add x e l) y e' r
-         | EQ _ => Node l y e r h
-         | GT _ => bal l y e' (add x e r)
-      end
-  end.
-
-Lemma add_in : forall elt (m:t elt) x y e,
+Lemma add_in : forall m 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 *)
- rewrite bal_in, IHt; intuition_in.
- (* EQ *)  
- intuition_in.
- apply InRoot; apply X.eq_sym; eauto.
- (* GT *)
- rewrite bal_in, IHt; intuition_in.
+ intros m x y e; functional induction (add x e m); auto; intros;
+ try (rewrite bal_in, IHt); intuition_in.
+ apply In_1 with x; auto.
 Qed.
 
-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; auto; apply bal_bst; auto.
- (* lt_tree -> lt_tree (add ...) *)
- intro z; rewrite add_in; intuition.
- eauto.
- (* gt_tree -> gt_tree (add ...) *)
- intro z; rewrite add_in; intuition.
+Lemma add_bst : forall m x e, bst m -> bst (add x e m).
+Proof.
+ intros m x e; functional induction (add x e m); intros;
+  inv bst; try apply bal_bst; auto;
+  intro z; rewrite add_in; intuition.
+ apply MX.eq_lt with x; auto.
  apply MX.lt_eq with x; auto.
 Qed.
+Hint Resolve add_bst.
 
-Lemma add_1 : forall elt (m:t elt) x y e, X.eq x y -> MapsTo y e (add x e m).
+Lemma add_1 : forall m 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 m x y e; functional induction (add x e m); 
    intros; inv bst; try rewrite bal_mapsto; unfold create; eauto.
 Qed.
 
-Lemma add_2 : forall elt (m:t elt) x y e e', ~X.eq x y -> 
+Lemma add_2 : forall m 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.
+ intros m x y e e'; induction m; simpl; auto.
  destruct (X.compare x k);
  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', ~X.eq x y -> 
+Lemma add_3 : forall m 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 m x y e e'; induction m; simpl; auto. 
  intros; inv MapsTo; auto; order.
  destruct (X.compare x k); intro; 
   try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; 
   order.
 Qed.
 
+Lemma add_find : forall m x y e, bst m -> 
+ find y (add x e m) = 
+  match X.compare y x with EQ _ => Some e | _ => find y m end.
+Proof.
+ intros.
+ assert (~X.eq x y -> find y (add x e m) = find y m).
+  intros; rewrite find_mapsto_equiv; auto.
+  split; eauto using add_2, add_3.
+ destruct X.compare; try (apply H0; order).
+ auto using find_1, add_1.
+Qed.
 
+(** * Extraction of minimum binding *)
 
-(** * Extraction of minimum binding
-
-  morally, [remove_min] is to be applied to a non-empty tree 
-  [t = Node l x e r h]. Since we can't deal here with [assert false] 
-  for [t=Leaf], we pre-unpack [t] (and forget about [h]). 
-*)
- 
-Function remove_min (elt:Type)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := 
-  match l with 
-    | Leaf => (r,(x,e))
-    | 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_in : forall elt (l:t elt) x e r h y,
+Lemma remove_min_in : forall l 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.
+ intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in.
- rewrite e1 in *; simpl; intros.
+ rewrite e0 in *; simpl; intros.
  rewrite bal_in, In_node_iff, IHp; intuition.
 Qed.
 
-Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e',
+Lemma remove_min_mapsto : forall l 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.
 Proof.
- intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
+ intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in; subst; auto.
- rewrite e1 in *; simpl; intros.
+ rewrite e0 in *; simpl; intros.
  rewrite bal_mapsto; auto; unfold create.
- simpl in *;destruct (IHp lh y e').
+ simpl in *;destruct (IHp _x y e').
  intuition.
  inversion_clear H1; intuition.
  inversion_clear H3; intuition.
 Qed.
 
-Lemma remove_min_bst : forall elt (l:t elt) x e r h, 
+Lemma remove_min_bst : forall l x e r h, 
  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.
+ intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
  inversion_clear H; inversion_clear H0.
  apply bal_bst; auto.
- rewrite e1 in *; simpl in *; apply (IHp lh); auto.
+ rewrite e0 in *; simpl in *; apply (IHp _x); auto.
  intro; intros.
- generalize (remove_min_in ll lx le lr lh y).
- rewrite e1; simpl in *.
+ generalize (remove_min_in ll lx ld lr _x y).
+ rewrite e0; simpl in *.
  destruct 1.
  apply H2; intuition.
 Qed.
+Hint Resolve remove_min_bst.
 
-Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, 
+Lemma remove_min_gt_tree : forall 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.
+ intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
  inversion_clear H.
  intro; intro.
- rewrite e1 in *;simpl in *.
- generalize (IHp lh H0).
- generalize (remove_min_in ll lx le lr lh m#1).
- rewrite e1; simpl; intros.
- 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.
+ rewrite e0 in *;simpl in *.
+ generalize (IHp _x H0).
+ generalize (remove_min_in ll lx ld lr _x m#1).
+ rewrite e0; simpl; intros.
+ rewrite (bal_in l' x d r y) in H.
+ assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto); clear H4.
  assert (X.lt m#1 x) by order.
  decompose [or] H; order.
 Qed.
+Hint Resolve remove_min_gt_tree.
 
+Lemma remove_min_find : forall l x e r h y, 
+ bst (Node l x e r h) -> 
+ find y (Node l x e r h) = 
+   match X.compare y (remove_min l x e r)#2#1 with 
+    | LT _ => None
+    | EQ _ => Some (remove_min l x e r)#2#2
+    | GT _ => find y (remove_min l x e r)#1
+   end.
+Proof.
+ intros.
+ destruct X.compare.
+ rewrite not_find_iff; auto.
+ rewrite remove_min_in; red; destruct 1 as [H'|H']; [ order | ].
+ generalize (remove_min_gt_tree H H'); order.
+ apply find_1; auto.
+ rewrite remove_min_mapsto; auto.
+ rewrite find_mapsto_equiv; eauto; intros.
+ rewrite remove_min_mapsto; intuition; order.
+Qed.
 
+(** * Merging two trees *)
 
-(** * 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].
-*)
-
-Function merge (elt:Type) (s1 s2 : t elt) : tree elt :=  match s1,s2 with 
-  | Leaf, _ => s2 
-  | _, Leaf => s1
-  | _, Node l2 x2 e2 r2 h2 => 
-    match remove_min l2 x2 e2 r2 with 
-      (s2',(x,e)) => bal s1 x e s2'
-    end
-end.
-
-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).
+Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 -> 
+ (In y (merge m1 m2) <-> In y m1 \/ In y m2).
 Proof. 
- intros elt s1 s2; functional induction (merge s1 s2);intros.
+ intros m1 m2; functional induction (merge m1 m2);intros;
+  try factornode _x _x0 _x1 _x2 _x3 as m1.
  intuition_in.
  intuition_in.
- destruct s1;try contradiction;clear y.
- replace s2' with ((remove_min l2 x2 e2 r2)#1) by (rewrite e3; auto).
- rewrite bal_in; auto.
- generalize (remove_min_in l2 x2 e2 r2 h2 y0); rewrite e3; simpl; intro.
- rewrite H1; intuition.
+ rewrite bal_in, remove_min_in, e1; simpl; intuition.
 Qed.
 
-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).
+Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 -> 
+  (MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2).
 Proof.
- intros elt s1 s2; functional induction (@merge elt s1 s2); intros.
+ intros m1 m2; functional induction (merge m1 m2); intros; 
+  try factornode _x _x0 _x1 _x2 _x3 as m1.
  intuition_in.
  intuition_in.
- 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 l2 x2 e2 r2 h2 y0 e); rewrite e3; simpl; intro.
- rewrite H1; intuition (try subst; auto).
+ rewrite bal_mapsto, remove_min_mapsto, e1; simpl; auto.
+ unfold create.
+ intuition; subst; auto.
  inversion_clear H1; intuition.
 Qed.
 
-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). 
+Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 -> 
+ (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> 
+ bst (merge m1 m2). 
 Proof.
- intros elt s1 s2; functional induction (@merge elt s1 s2); intros; auto.
-
+ intros m1 m2; functional induction (merge m1 m2); intros; auto;
+ try factornode _x _x0 _x1 _x2 _x3 as m1. 
  apply bal_bst; auto.
- destruct s1;try contradiction.
- generalize (remove_min_bst H0); rewrite e3; simpl in *; auto.
- destruct s1;try contradiction.
+ generalize (remove_min_bst H0); rewrite e1; simpl in *; auto.
  intro; intro.
  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 H0); rewrite e3; simpl; auto.
+ generalize (remove_min_in l2 x2 d2 r2 _x4 x); rewrite e1; simpl; intuition.
+ generalize (remove_min_gt_tree H0); rewrite e1; simpl; auto.
 Qed.
 
-
-
 (** * Deletion *)
 
-Function remove (elt:Type)(x:key)(s:t elt) { struct s } : t elt := match s with 
-  | Leaf => Leaf _
-  | Node l y e r h =>
-      match X.compare x y with
-         | LT _ => bal (remove x l) y e r
-         | EQ _ => merge l r
-         | GT _ => bal l y e (remove x r)
-      end
-   end.
-
-Lemma remove_in : forall elt (s:t elt) x y, bst s -> 
- (In y (remove x s) <-> ~ X.eq y x /\ In y s).
+Lemma remove_in : forall m x y, bst m -> 
+ (In y (remove x m) <-> ~ X.eq y x /\ In y m).
 Proof.
- intros elt s x; functional induction (@remove elt x s); simpl; intros.
+ intros m x; functional induction (remove x m); simpl; intros.
  intuition_in.
  (* LT *)
- inv bst; clear e1.
+ inv bst; clear e0.
  rewrite bal_in; auto.
  generalize (IHt y0 H0); intuition; [ order | order | intuition_in ].
  (* EQ *)
- inv bst; clear e1.
+ inv bst; clear e0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
  elim H4; eauto.
  (* GT *)
- inv bst; clear e1.
+ inv bst; clear e0.
  rewrite bal_in; auto.
  generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
 Qed.
 
-Lemma remove_bst : forall elt (s:t elt) x, bst s -> bst (remove x s).
+Lemma remove_bst : forall m x, bst m -> bst (remove x m).
 Proof. 
- intros elt s x; functional induction (@remove elt x s); simpl; intros.
+ intros m x; functional induction (remove x m); simpl; intros.
  auto.
  (* LT *)
  inv bst.
@@ -623,26 +1050,26 @@ Proof.
  destruct H; eauto.
 Qed.
 
-Lemma remove_1 : forall elt (m:t elt) x y, bst m -> X.eq x y -> ~ In y (remove x m).
+Lemma remove_1 : forall m x y, bst m -> X.eq x y -> ~ In y (remove x m).
 Proof. 
  intros; rewrite remove_in; intuition.
-Qed. 
+Qed.
 
-Lemma remove_2 : forall elt (m:t elt) x y e, bst m -> ~X.eq x y -> 
+Lemma remove_2 : forall m 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.
+ intros m x y 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; 
    try solve [inv MapsTo; auto].
  rewrite merge_mapsto; auto.
  inv MapsTo; auto; order.
 Qed.
 
-Lemma remove_3 : forall elt (m:t elt) x y e, bst m ->
+Lemma remove_3 : forall m 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.
+ intros m x y e; induction m; simpl; auto.
  destruct (X.compare x k); intros Bs; inv bst; 
   try rewrite bal_mapsto; auto; unfold create.
   intros; inv MapsTo; auto.
@@ -650,141 +1077,215 @@ Proof.
   intros; inv MapsTo; auto.
 Qed.
 
-Section Elt2.
-
-Variable elt:Type.
-
-Notation eqk := (PX.eqk (elt:= elt)).
-Notation eqke := (PX.eqke (elt:= elt)).
-Notation ltk := (PX.ltk (elt:= elt)).
+(** * join *)
 
-(** * Empty map *)
+(* Function/Functional Scheme can't deal with internal fix. 
+   Let's do its job by hand: *)
 
-Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.
-
-Definition empty := (Leaf elt).
+Ltac join_tac := 
+ intros l; induction l as [| ll _ lx ld lr Hlr lh]; 
+   [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
+     [ | destruct (gt_le_dec lh (rh+2)); 
+       [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
+           replace (bal u v w z) 
+           with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
+         end 
+       | destruct (gt_le_dec rh (lh+2)); 
+         [ match goal with |- context [ bal ?u ?v ?w ?z ] => 
+             replace (bal u v w z) 
+             with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] 
+           end
+         | ] ] ] ]; intros.
 
-Lemma empty_bst : bst empty.
+Lemma join_in : forall l x d r y, 
+ In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
- unfold empty; auto.
+ join_tac.
+ simpl.
+ rewrite add_in; intuition_in.
+ rewrite add_in; 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 empty_1 : Empty empty.
+Lemma join_bst : forall l x d r, bst l -> bst r -> 
+ lt_tree x l -> gt_tree x r -> bst (join l x d r).
 Proof.
- unfold empty, Empty; intuition_in.
+ join_tac; auto; try (simpl; auto; fail); 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.
 
-(** * Emptyness test *)
-
-Definition is_empty (s:t elt) := match s with Leaf => true | _ => false end.
-
-Lemma is_empty_1 : forall s, Empty s -> is_empty s = true. 
+Lemma join_find : forall l x d r y, 
+ bst l -> bst r -> lt_tree x l -> gt_tree x r -> 
+ find y (join l x d r) = find y (create l x d r).
 Proof.
- destruct s as [|r x e l h]; simpl; auto.
- intro H; elim (H x e); auto.
-Qed.
+ join_tac; auto; inv bst;
+  simpl (join (Leaf elt)); 
+  try (assert (X.lt lx x) by auto); 
+  try (assert (X.lt x rx) by auto);
+  rewrite ?add_find, ?bal_find; auto.
 
-Lemma is_empty_2 : forall s, is_empty s = true -> Empty s.
-Proof. 
- destruct s; simpl; intros; try discriminate; red; intuition_in.
-Qed.
+ simpl; destruct X.compare; auto.
+ rewrite not_find_iff; auto; intro; order.
 
+ simpl; repeat (destruct X.compare; auto); try (order; fail).
+ rewrite not_find_iff by auto; intro.
+ assert (X.lt y x) by auto; order.
 
+ simpl; rewrite Hlr; simpl; auto.
+ repeat (destruct X.compare; auto); order.
+ intros u Hu; rewrite join_in in Hu.
+  destruct Hu as [Hu|[Hu|Hu]]; try generalize (H2 _ Hu); order.
 
-(** * Appartness *)
+ simpl; rewrite Hrl; simpl; auto.
+ repeat (destruct X.compare; auto); order.
+ intros u Hu; rewrite join_in in Hu.
+  destruct Hu as [Hu|[Hu|Hu]]; order.
+Qed.
 
-(** The [mem] function is deciding appartness. It exploits the [bst] property
-    to achieve logarithmic complexity. *)
+(** * split *)
 
-Function mem (x:key)(m:t elt) { struct m } : bool := 
-   match m with 
-     |  Leaf => false 
-     |  Node l y e r _ => match X.compare x y with 
-             | LT _ => mem x l 
-             | EQ _ => true
-             | GT _ => mem x r
-         end
-   end.
-Implicit Arguments mem. 
+Lemma split_in_1 : forall m x, bst m -> forall y, 
+ (In y (split x m)#l <-> In y m /\ X.lt y x).
+Proof.
+ intros m x; functional induction (split x m); simpl; intros; 
+  inv bst; try clear e0.
+ intuition_in.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
+ intuition_in; order.
+ rewrite join_in.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
+Qed.
 
-Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true.
+Lemma split_in_2 : forall m x, bst m -> forall y, 
+ (In y (split x m)#r <-> In y m /\ X.lt x y).
 Proof. 
- intros s x; functional induction mem x s; auto; intros; clearf;
-  inv bst; intuition_in; order.
+ intros m x; functional induction (split x m); subst; simpl; intros; 
+  inv bst; try clear e0.
+ intuition_in.
+ rewrite join_in.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
+ intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
+Qed.
+
+Lemma split_in_3 : forall m x, bst m -> 
+ (split x m)#o = find x m.
+Proof.
+ intros m x; functional induction (split x m); subst; simpl; auto;
+  intros; inv bst; try clear e0; 
+  destruct X.compare; try (order;fail); rewrite <-IHt, e1; auto.
 Qed.
 
-Lemma mem_2 : forall s x, mem x s = true -> In x s. 
+Lemma split_bst : forall m x, bst m -> 
+ bst (split x m)#l /\ bst (split x m)#r.
 Proof. 
- intros s x; functional induction mem x s; auto; intros; discriminate.
+ intros m x; functional induction (split x m); 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 H0 y0); rewrite e1; simpl; intuition.
+ intros y0.
+ generalize (split_in_1 x H1 y0); rewrite e1; simpl; intuition.
 Qed.
 
-Function find (x:key)(m:t elt) { struct m } : option elt := 
-   match m with 
-     |  Leaf => None 
-     |  Node l y e r _ => match X.compare x y with 
-             | LT _ => find x l 
-             | EQ _ => Some e
-             | GT _ => find x r
-         end
-   end.
+Lemma split_lt_tree : forall m x, bst m -> lt_tree x (split x m)#l.
+Proof.
+ intros m x B y Hy; rewrite split_in_1 in Hy; intuition.
+Qed.
 
-Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
-Proof. 
- intros s x; functional induction find x s; auto; intros; clearf;
-  inv bst; intuition_in; simpl; auto; 
- try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto].
+Lemma split_gt_tree : forall m x, bst m -> gt_tree x (split x m)#r.
+Proof.
+ intros m x B y Hy; rewrite split_in_2 in Hy; intuition.
 Qed.
 
-Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
-Proof. 
- intros m x; functional induction find x m; subst; intros; clearf;
-  try discriminate.
- constructor 2; auto.
- inversion H; auto.
- constructor 3; auto.
+Lemma split_find : forall m x y, bst m -> 
+ find y m = match X.compare y x with 
+              | LT _ => find y (split x m)#l
+              | EQ _ => (split x m)#o
+              | GT _ => find y (split x m)#r
+            end.
+Proof.
+ intros m x; functional induction (split x m); subst; simpl; intros; 
+  inv bst; try clear e0; try rewrite e1 in *; simpl in *; 
+  [ destruct X.compare; auto | .. ];
+  try match goal with E:split ?x ?t = _, B:bst ?t |- _ => 
+      generalize (split_in_1 x B)(split_in_2 x B)(split_bst x B);
+       rewrite E; simpl; destruct 3 end.
+
+ rewrite join_find, IHt; auto; clear IHt; simpl.
+ repeat (destruct X.compare; auto); order.
+ intro y1; rewrite H4; intuition.
+
+ repeat (destruct X.compare; auto); order.
+
+ rewrite join_find, IHt; auto; clear IHt; simpl.
+ repeat (destruct X.compare; auto); order.
+ intros y1; rewrite H; intuition.
 Qed.
 
-(** An all-in-one spec for [add] used later in the naive [map2] *)
+(** * Concatenation *)
 
-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.
+Lemma concat_in : forall m1 m2 y, 
+ In y (concat m1 m2) <-> In y m1 \/ In y m2.
 Proof.
-intros.
-destruct (MX.eq_dec x y).
-apply find_1.
-apply add_bst; auto.
-eapply MapsTo_1 with y; eauto.
-apply add_1; auto.
-case_eq (find x m); intros.
-apply find_1.
-apply add_bst; auto.
-apply add_2; auto.
-apply find_2; auto.
-case_eq (find x (add y e m)); auto; intros.
-rewrite <- H0; symmetry.
-apply find_1; auto.
-eapply add_3; eauto.
-apply find_2; eauto.
+ intros m1 m2; functional induction (concat m1 m2); intros;
+  try factornode _x _x0 _x1 _x2 _x3 as m1.
+ intuition_in.
+ intuition_in.
+ rewrite join_in, remove_min_in, e1; simpl; intuition.
 Qed.
 
+Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 -> 
+ (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> 
+ bst (concat m1 m2).
+Proof.
+ intros m1 m2; functional induction (concat m1 m2); intros; auto; 
+ try factornode _x _x0 _x1 _x2 _x3 as m1.
+ apply join_bst; auto.
+ change (bst (m2',xd)#1); rewrite <-e1; eauto.
+ intros y Hy.
+ apply H1; auto.
+ rewrite remove_min_in, e1; simpl; auto.
+ change (gt_tree (m2',xd)#2#1 (m2',xd)#1); rewrite <-e1; eauto.
+Qed.
+Hint Resolve concat_bst.
 
+Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> 
+ (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> 
+ find y (concat m1 m2) = 
+  match find y m2 with Some d => Some d | None => find y m1 end.
+Proof.
+ intros m1 m2; functional induction (concat m1 m2); intros; auto; 
+ try factornode _x _x0 _x1 _x2 _x3 as m1.
+ simpl; destruct (find y m2); auto.
 
-(** * Elements *)
+ generalize (remove_min_find y H0)(remove_min_in l2 x2 d2 r2 _x4)
+  (remove_min_bst H0)(remove_min_gt_tree H0); 
+  rewrite e1; simpl fst; simpl snd; intros.
+ 
+ inv bst.
+ rewrite H2, join_find; auto; clear H2.
+ simpl; destruct X.compare; simpl; auto.
+ destruct (find y m2'); auto.
+ symmetry; rewrite not_find_iff; auto; intro.
+ apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto.
 
-(** [elements_tree_aux acc t] catenates the elements of [t] in infix
-    order to the list [acc] *)
+ intros z Hz; apply H1; auto; rewrite H3; auto.
+Qed.
 
-Fixpoint elements_aux (acc : list (key*elt)) (t : t elt) {struct t} : list (key*elt) :=
-  match t with
-   | Leaf => acc
-   | Node l x e r _ => elements_aux ((x,e) :: elements_aux acc r) l
-  end.
 
-(** then [elements] is an instanciation with an empty [acc] *)
+(** * Elements *)
 
-Definition elements := elements_aux nil.
+Notation eqk := (PX.eqk (elt:= elt)).
+Notation eqke := (PX.eqke (elt:= elt)).
+Notation ltk := (PX.ltk (elt:= elt)).
 
-Lemma elements_aux_mapsto : forall s acc x e, 
+Lemma elements_aux_mapsto : forall (s:t elt) acc x e, 
  InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc.
 Proof.
  induction s as [ | l Hl x e r Hr h ]; simpl; auto.
@@ -797,13 +1298,13 @@ Proof.
  destruct H0; simpl in *; subst; intuition.
 Qed.
 
-Lemma elements_mapsto : forall s x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. 
+Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. 
 Proof. 
  intros; generalize (elements_aux_mapsto s nil x e); intuition.
  inversion_clear H0.
 Qed.
 
-Lemma elements_in : forall s x, L.PX.In x (elements s) <-> In x s.
+Lemma elements_in : forall (s:t elt) x, L.PX.In x (elements s) <-> In x s.
 Proof.
  intros.
  unfold L.PX.In.
@@ -815,7 +1316,7 @@ Proof.
  unfold L.PX.MapsTo; rewrite elements_mapsto; auto.
 Qed.
 
-Lemma elements_aux_sort : forall s acc, bst s -> sort ltk acc ->
+Lemma elements_aux_sort : forall (s:t elt) acc, bst s -> sort ltk acc ->
  (forall x e y, InA eqke (x,e) acc -> In y s -> X.lt y x) ->
  sort ltk (elements_aux acc s).
 Proof.
@@ -848,28 +1349,38 @@ Proof.
 Qed.
 
 Lemma elements_aux_cardinal :
- forall m acc, (length acc + cardinal m)%nat = length (elements_aux acc m).
+ forall (m:t elt) acc, (length acc + cardinal m)%nat = length (elements_aux acc m).
 Proof.
  simple induction m; simpl; intuition.
  rewrite <- H; simpl.
  rewrite <- H0; omega.
 Qed.
 
-Lemma elements_cardinal : forall m, cardinal m = length (elements m).
+Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m).
 Proof.
  exact (fun m => elements_aux_cardinal m nil).
 Qed.
 
+Lemma elements_app :
+ forall (s:t elt) 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 (t1 t2:t elt) x e z l,
+ elements t1 ++ (x,e) :: elements t2 ++ l =
+ elements (Node t1 x e t2 z) ++ l.
+Proof.
+ unfold elements; simpl; intros.
+ rewrite !elements_app, <- !app_nil_end, !app_ass; auto.
+Qed.
 
 (** * Fold *)
 
-Fixpoint fold (A : Type) (f : key -> elt -> A -> A)(s : t elt) {struct s} : A -> A := 
- fun a => match s with
-  | Leaf => a
-  | Node l x e r _ => fold f r (f x e (fold f l a))
- end.
-
 Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) := 
   L.fold f (elements s).
 
@@ -907,197 +1418,93 @@ Proof.
  unfold L.elements; auto.
 Qed.
 
-
-
 (** * Comparison *)
 
-Definition Equivb (cmp:elt->elt->bool) m m' := 
-  (forall k, In k m <-> In k m') /\ 
-  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
-
-(** ** Enumeration of the elements of a tree *)
-
-Inductive enumeration :=
- | End : enumeration
- | More : key -> elt -> t elt -> enumeration -> enumeration.
-
-(** [flatten_e e] returns the list of elements of [e] i.e. the list
-    of elements actually compared *)
+(** [flatten_e e] returns the list of elements of the enumeration [e] 
+    i.e. the list of elements actually compared *)
  
-Fixpoint flatten_e (e : enumeration) : list (key*elt) := match e with
+Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
   | End => nil
   | More x e t r => (x,e) :: elements t ++ flatten_e r
  end.
 
-(** [sorted_e e] expresses that elements in the enumeration [e] are
-    sorted, and that all trees in [e] are binary search trees. *)
-
-Inductive In_e (p:key*elt) : enumeration -> Prop :=
-  | InEHd1 : forall y d s e, eqke p (y,d) -> In_e p (More y d s e)
-  | InEHd2 : forall y d s e, MapsTo p#1 p#2 s -> In_e p (More y d s e)
-  | InETl : forall y d s e, In_e p e -> In_e p (More y d s e).
-
-Hint Constructors In_e.
-
-Inductive sorted_e : enumeration -> Prop :=
-  | SortedEEnd : sorted_e End
-  | SortedEMore :
-      forall x d s e, bst s -> gt_tree x s -> sorted_e e ->
-      (forall p, In_e p e -> ltk (x,d) p) ->
-      (forall p, MapsTo p#1 p#2 s -> forall q, In_e q e -> ltk p q) ->
-      sorted_e (More x d s e).
-
-Hint Constructors sorted_e.
-
-Lemma in_flatten_e :
- forall p e, InA eqke p (flatten_e e) -> In_e p e.
+Lemma flatten_e_elements :
+ forall (l:t elt) r x d z e,
+ elements l ++ flatten_e (More x d r e) = 
+ elements (Node l x d r z) ++ flatten_e e.
 Proof.
- simple induction e; simpl in |- *; intuition.
- inversion_clear H.
- inversion_clear H0; auto.
- elim (InA_app H1); auto.
- destruct (elements_mapsto t a b); auto.
+ intros; simpl; apply elements_node.
 Qed.
 
-Lemma sorted_flatten_e :
- forall e : enumeration, sorted_e e -> sort ltk (flatten_e e).
+Lemma cons_1 : forall (s:t elt) e, 
+  flatten_e (cons s e) = elements s ++ flatten_e e.
 Proof.
- simple induction e; simpl in |- *; intuition.
- apply cons_sort.
- apply (SortA_app (PX.eqke_refl (elt:=elt))); inversion_clear H0; auto.
- intros; apply H5; auto.
- rewrite <- elements_mapsto; auto; destruct x; auto.
- apply in_flatten_e; auto.
- inversion_clear H0.
- apply In_InfA; intros.
- intros; elim (in_app_or _ _ _ H0); intuition.
- generalize (In_InA (PX.eqke_refl (elt:=elt)) H6).
- destruct y; rewrite elements_mapsto; eauto.
- apply H4; apply in_flatten_e; auto.
- apply In_InA; auto.
+  induction s; simpl; auto; intros.
+  rewrite IHs1; apply flatten_e_elements; auto.
 Qed.
 
-Lemma elements_app :
- forall s acc, elements_aux acc s = elements s ++ acc.
-Proof.
- simple induction s; simpl in |- *; intuition.
- rewrite H0.
- rewrite H.
- unfold elements; simpl.
- do 2 rewrite H.
- rewrite H0.
- repeat rewrite <- app_nil_end.
- repeat rewrite app_ass; auto.
-Qed.
+(** Proof of correction for the comparison *)
 
-Lemma compare_flatten_1 :
- forall t1 t2 x e z l,
- elements t1 ++ (x,e) :: elements t2 ++ l =
- elements (Node t1 x e t2 z) ++ l.
-Proof.
- simpl in |- *; unfold elements in |- *; simpl in |- *; intuition.
- repeat rewrite elements_app.
- repeat rewrite <- app_nil_end.
- repeat rewrite app_ass; auto.
-Qed.
+Variable cmp : elt->elt->bool.
 
-(** key lemma for correctness *)
+Definition IfEq b l1 l2 := L.equal cmp l1 l2 = b.
 
-Lemma flatten_e_elements :
- forall l r x d z e,
- elements l ++ flatten_e (More x d r e) = 
- elements (Node l x d r z) ++ flatten_e e.
+Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2, 
+  X.eq x1 x2 -> cmp d1 d2 = true -> 
+  IfEq b l1 l2 -> 
+    IfEq b ((x1,d1)::l1) ((x2,d2)::l2).
 Proof.
- intros; simpl.
- apply compare_flatten_1.
+ unfold IfEq; destruct b; simpl; intros; destruct X.compare; simpl; 
+  try rewrite H0; auto; order.
 Qed.
 
-(** termination of [compare_aux] *)
-
-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 
-    enumeration [e]. *)
-
-Fixpoint cons s e {struct s} : enumeration := 
- match s with 
-  | Leaf => e
-  | Node l x d r h => cons l (More x d r e)
- end.
-
-Lemma cons_cardinal_e : forall s e, 
- cardinal_e (cons s e) = (cardinal s + cardinal_e e)%nat.
+Lemma equal_end_IfEq : forall e2, 
+  IfEq (equal_end e2) nil (flatten_e e2).
 Proof.
- induction s; simpl; intros; auto.
- rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith.
+ destruct e2; red; auto.
 Qed.
 
-Lemma cons_1 : forall s e, 
-  bst s -> sorted_e e ->
-  (forall x y, MapsTo x#1 x#2 s -> In_e y e -> ltk x y) ->
-  sorted_e (cons s e) /\ 
-  flatten_e (cons s e) = elements s ++ flatten_e e.
+Lemma equal_more_IfEq : 
+ forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, 
+  IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> 
+    IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l)
+       (flatten_e (More x2 d2 r2 e2)).
 Proof.
- induction s; simpl; auto.
- clear IHs2; intros.
- inv bst.
- destruct (IHs1 (More k e s2 e0)); clear IHs1; intuition.
- inversion_clear H6; subst; auto; clear H1.
- destruct y; red in H7; simpl in *; destruct H7; subst.
- red; simpl; auto.
- assert (In a s1) by eauto.
- order.
- destruct y; simpl in *; auto.
- red; simpl; auto.
- assert (In a s1) by eauto.
- assert (In k0 s2) by eauto.
- order.
- rewrite H6.
- apply flatten_e_elements.
-Qed.
-
-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 cardinal_e_2 e } : bool := 
- match e with 
- | (End,End) => true
- | (End,More _ _ _ _) => false
- | (More _ _ _ _, End) => false
- | (More x1 d1 r1 e1, More x2 d2 r2 e2) => 
-       match X.compare x1 x2 with 
-        | EQ _ => cmp d1 d2 && equal_aux cmp (cons r1 e1, cons r2 e2)
-        | LT _ => false
-        | GT _ => false
-       end
- end.
-Proof.
-intros; unfold cardinal_e_2; simpl; 
-abstract (do 2 rewrite cons_cardinal_e; romega with *).
-Defined.
+ unfold IfEq; simpl; intros; destruct X.compare; simpl; auto.
+ rewrite <-andb_lazy_alt; f_equal; auto.
+Qed.
 
-Definition equal (cmp: elt -> elt -> bool) s s' := 
- equal_aux cmp (cons s End, cons s' End).
+Lemma equal_cont_IfEq : forall m1 cont e2 l, 
+  (forall e, IfEq (cont e) l (flatten_e e)) ->
+  IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2).
+Proof.
+ induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto.
+ rewrite <- elements_node; simpl.
+ apply Hl1; auto.
+ clear e2; intros [|x2 d2 r2 e2].
+ simpl; red; auto.
+ apply equal_more_IfEq.
+ rewrite <- cons_1; auto.
+Qed.
 
-Lemma equal_aux_Equivb : forall cmp e, sorted_e e#1 -> sorted_e e#2 ->
- (equal_aux cmp e = L.equal cmp (flatten_e e#1) (flatten_e e#2)).
+Lemma equal_IfEq : forall (m1 m2:t elt),
+  IfEq (equal cmp m1 m2) (elements m1) (elements m2).
 Proof.
- intros cmp e; functional induction equal_aux cmp e; intros; clearf;
-  simpl in *; auto; MX.elim_comp; auto.
- f_equal; auto.
- inversion_clear H.
- inversion_clear H0.
- destruct (@cons_1 r1 e1); auto.
- destruct (@cons_1 r2 e2); auto.
- rewrite <- H11, <- H13; auto.
+ intros; unfold equal.
+ rewrite (app_nil_end (elements m1)).
+ replace (elements m2) with (flatten_e (cons m2 (End _))) 
+  by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto).
+ apply equal_cont_IfEq.
+ intros.
+ apply equal_end_IfEq; auto.
 Qed.
 
-Lemma Equivb_elements : forall cmp s s', 
- Equivb cmp s s' <-> L.Equivb cmp (elements s) (elements s').
+Definition Equivb m m' := 
+  (forall k, In k m <-> In k m') /\ 
+  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).
+
+Lemma Equivb_elements : forall s s', 
+ Equivb s s' <-> L.Equivb cmp (elements s) (elements s').
 Proof.
 unfold Equivb, L.Equivb; split; split; intros.
 do 2 rewrite elements_in; firstorder.
@@ -1108,78 +1515,46 @@ destruct H.
 apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto.
 Qed.
 
-Lemma equal_Equivb : forall cmp s s', bst s -> bst s' -> 
- (equal cmp s s' = true <-> Equivb cmp s s').
+Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' -> 
+  (equal cmp s s' = true <-> Equivb s s').
 Proof.
- intros; unfold equal.
- destruct (@cons_1 s End); auto.
- inversion 2.
- destruct (@cons_1 s' End); auto.
- inversion 2.
- rewrite equal_aux_Equivb; simpl; auto.
- rewrite Equivb_elements.
- rewrite H2, H4.
- simpl; do 2 rewrite <- app_nil_end.
+ intros s s' B B'.
+ rewrite Equivb_elements, <- equal_IfEq.
  split; [apply L.equal_2|apply L.equal_1]; auto.
 Qed.
 
-End Elt2.
-
-Section Elts. 
-
-Variable elt elt' elt'' : Type.
+End Elt.
 
 Section Map. 
+Variable elt elt' : Type.
 Variable f : elt -> elt'. 
 
-Fixpoint map (m:t elt) {struct m} : t elt' := 
-  match m with 
-   | Leaf   => Leaf _
-   | Node l v d r h => Node (map l) v  (f d) (map r) h
-  end.
-
-Lemma map_height : forall m, height (map m) = height m.
-Proof. 
-destruct m; simpl; auto.
-Qed.
-
-Lemma map_1 : forall (m: tree elt)(x:key)(e:elt), 
-    MapsTo x e m -> MapsTo x (f e) (map m).
+Lemma map_1 : forall (m: t elt)(x:key)(e:elt), 
+    MapsTo x e m -> MapsTo x (f e) (map f m).
 Proof.
 induction m; simpl; inversion_clear 1; auto.
 Qed.
 
 Lemma map_2 : forall (m: t elt)(x:key), 
-    In x (map m) -> In x m.
+    In x (map f m) -> In x m.
 Proof.
 induction m; simpl; inversion_clear 1; auto.
 Qed.
 
-Lemma map_bst : forall m, bst m -> bst (map m).
+Lemma map_bst : forall m, bst m -> bst (map f m).
 Proof.
 induction m; simpl; auto.
-inversion_clear 1; constructor; auto.
-red; intros; apply H2; apply map_2; auto.
-red; intros; apply H3; apply map_2; auto.
+inversion_clear 1; constructor; auto; 
+ red; auto using map_2.
 Qed.
 
 End Map.
-Section Mapi. 
-Variable f : key -> elt -> elt'. 
-
-Fixpoint mapi (m:t elt) {struct m} : t elt' := 
-  match m with 
-   | Leaf   => Leaf _
-   | Node l v d r h => Node (mapi l) v  (f v d) (mapi r) h
-  end.
-
-Lemma mapi_height : forall m, height (mapi m) = height m.
-Proof. 
-destruct m; simpl; auto.
-Qed.
+Section Mapi.
+Variable elt elt' : Type.
+Variable f : key -> elt -> elt'.
 
 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).
+    MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).
 Proof.
 induction m; simpl; inversion_clear 1; auto.
 exists k; auto.
@@ -1190,172 +1565,242 @@ exists x0; intuition.
 Qed.
 
 Lemma mapi_2 : forall (m: t elt)(x:key), 
-    In x (mapi m) -> In x m.
+    In x (mapi f m) -> In x m.
 Proof.
 induction m; simpl; inversion_clear 1; auto.
 Qed.
 
-Lemma mapi_bst : forall m, bst m -> bst (mapi m).
+Lemma mapi_bst : forall m, bst m -> bst (mapi f m).
 Proof.
 induction m; simpl; auto.
-inversion_clear 1; constructor; auto.
-red; intros; apply H2; apply mapi_2; auto.
-red; intros; apply H3; apply mapi_2; auto.
+inversion_clear 1; constructor; auto; 
+ red; auto using mapi_2.
 Qed.
 
 End Mapi.
 
-Section Map2.
-Variable f : option elt -> option elt' -> option elt''.
-
-(* Not exactly pretty nor perfect, but should suffice as a first naive implem. 
-    Anyway, map2 isn't in Ocaml...
-*)
-
-Definition anti_elements (l:list (key*elt'')) := L.fold (@add _) l (empty _).
+Section Map_option.
+Variable elt elt' : Type.
+Variable f : key -> elt -> option elt'.
+Hypothesis f_compat : forall x x' d, X.eq x x' -> f x d = f x' d.
 
-Definition map2 (m:t elt)(m':t elt') : t elt'' := 
-  anti_elements (L.map2 f (elements m) (elements m')).
-
-Lemma anti_elements_bst_aux : forall (l:list (key*elt''))(m:t elt''), 
-  bst m -> bst (L.fold (@add _) l m).
+Lemma map_option_2 : forall (m:t elt)(x:key), 
+ In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None.
 Proof.
-induction l.
-simpl; auto.
-simpl; destruct a; intros.
-apply IHl.
-apply add_bst; auto.
+intros m; functional induction (map_option f m); simpl; auto; intros.
+inversion H.
+rewrite join_in in H; destruct H as [H|[H|H]].
+exists d; split; auto; rewrite (f_compat d H), e0; discriminate.
+destruct (IHt _ H) as {d0,?,?}; exists d0; auto.
+destruct (IHt0 _ H) as {d0,?,?}; exists d0; auto.
+rewrite concat_in in H; destruct H as [H|H].
+destruct (IHt _ H) as {d0,?,?}; exists d0; auto.
+destruct (IHt0 _ H) as {d0,?,?}; exists d0; auto.
 Qed.
 
-Lemma anti_elements_bst : forall l, bst (anti_elements l).
+Lemma map_option_bst : forall m, bst m -> bst (map_option f m).
 Proof.
-unfold anti_elements, empty; intros; apply anti_elements_bst_aux; auto.
-Qed.
+intros m; functional induction (map_option f m); simpl; auto; intros; 
+ inv bst.
+apply join_bst; auto; intros y H; 
+ destruct (map_option_2 H) as {d0,?,?}; eauto using MapsTo_In.
+apply concat_bst; auto; intros y y' H H'.
+destruct (map_option_2 H) as {d0,?,?}.
+destruct (map_option_2 H') as {d0',?,?}.
+eapply X.lt_trans with x; eauto using MapsTo_In.
+Qed.
+Hint Resolve map_option_bst.
+
+Ltac nonify e := 
+ replace e with (@None elt) by 
+  (symmetry; rewrite not_find_iff; auto; intro; order).
+
+Lemma map_option_find : forall (m:t elt)(x:key), 
+ bst m -> 
+ find x (map_option f m) = 
+  match (find x m) with Some d => f x d | None => None end.
+Proof.
+intros m; functional induction (map_option f m); simpl; auto; intros;
+ inv bst; rewrite join_find || rewrite concat_find; auto; simpl; 
+ try destruct X.compare; simpl; auto.
+rewrite (f_compat d e); auto.
+intros y H;
+ destruct (map_option_2 H) as {?,?,?}; eauto using MapsTo_In.
+intros y H; 
+ destruct (map_option_2 H) as {?,?,?}; eauto using MapsTo_In.
+
+rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto.
+rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto.
+rewrite (f_compat d e); auto.
+rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto.
+ destruct (find x0 (map_option f r)); auto.
+
+intros y y' H H'.
+destruct (map_option_2 H) as {?,?,?}.
+destruct (map_option_2 H') as {?,?,?}.
+eapply X.lt_trans with x; eauto using MapsTo_In.
+Qed.
+
+End Map_option.
+
+Section Map2_opt.
+Variable elt elt' elt'' : Type.
+Variable f0 : key -> option elt -> option elt' -> option elt''.
+Variable f : key -> elt -> option elt' -> option elt''.
+Variable mapl : t elt -> t elt''.
+Variable mapr : t elt' -> t elt''.
+Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o.
+Hypothesis mapl_bst : forall m, bst m -> bst (mapl m).
+Hypothesis mapr_bst : forall m', bst m' -> bst (mapr m').
+Hypothesis mapl_f0 : forall x m, bst m -> 
+ find x (mapl m) = 
+  match find x m with Some d => f0 x (Some d) None | None => None end.
+Hypothesis mapr_f0 : forall x m', bst m' -> 
+ find x (mapr m') = 
+  match find x m' with Some d' => f0 x None (Some d') | None => None end.
+Hypothesis f0_compat : forall x x' o o', X.eq x x' -> f0 x o o' = f0 x' o o'.
+
+Notation map2_opt := (map2_opt f mapl mapr).
+
+Lemma map2_opt_2 : forall m m' y, bst m -> bst m' -> 
+  In y (map2_opt m m') -> In y m \/ In y m'.
+Proof.
+intros m m'; functional induction (map2_opt m m'); intros;
+ auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; 
+ try (generalize (split_in_1 x1 H0 y)(split_in_2 x1 H0 y)
+      (split_bst x1 H0); rewrite e1; simpl; destruct 3; inv bst).
+
+right; apply find_in.
+generalize (in_find (mapr_bst H0) H1); rewrite mapr_f0; auto.
+destruct (find y m2); auto; intros; discriminate.
+
+factornode l1 x1 d1 r1 _x as m1.
+left; apply find_in.
+generalize (in_find (mapl_bst H) H1); rewrite mapl_f0; auto.
+destruct (find y m1); auto; intros; discriminate.
+
+rewrite join_in in H1; destruct H1 as [H'|[H'|H']]; auto.
+destruct (IHt1 y H6 H4 H'); intuition.
+destruct (IHt0 y H7 H5 H'); intuition.
+
+rewrite concat_in in H1; destruct H1 as [H'|H']; auto.
+destruct (IHt1 y H6 H4 H'); intuition.
+destruct (IHt0 y H7 H5 H'); intuition.
+Qed.
+
+Lemma map2_opt_bst : forall m m', bst m -> bst m' -> 
+ bst (map2_opt m m').
+Proof.
+intros m m'; functional induction (map2_opt m m'); intros;
+ auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst; 
+ generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0); 
+  rewrite e1; simpl in *; destruct 3.
+
+apply join_bst; auto.
+intros y Hy; specialize H with y.
+destruct (map2_opt_2 H1 H6 Hy); intuition.
+intros y Hy; specialize H5 with y.
+destruct (map2_opt_2 H2 H7 Hy); intuition.
+
+apply concat_bst; auto.
+intros y y' Hy Hy'; specialize H with y; specialize H5 with y'.
+apply X.lt_trans with x1.
+destruct (map2_opt_2 H1 H6 Hy); intuition.
+destruct (map2_opt_2 H2 H7 Hy'); intuition.
+Qed.
+Hint Resolve map2_opt_bst.
+
+Ltac map2_aux := 
+ match goal with
+  | H : In ?x _ \/ In ?x ?m, 
+    H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ => 
+    destruct H; [ intuition_in; order | 
+                  rewrite <-(find_in_equiv B B' H'); auto ]
+ end.
 
-Lemma anti_elements_mapsto_aux : forall (l:list (key*elt'')) m k e,
-  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 H3.
-simpl; destruct a; intros.
-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 H3.
-rewrite add_spec in H2; auto.
-destruct (MX.eq_dec k0 k).
-inversion_clear H2; subst; auto.
-right; apply find_2; auto.
-inversion_clear H3; auto.
-compute in H2; destruct H2.
-subst; right; apply add_1; auto.
-inversion_clear H0.
-destruct (MX.eq_dec k0 k).
-destruct (H1 k); eauto.
-right; apply add_2; auto.
-inversion H0; auto.
-intros.
-inversion_clear H0.
-assert (~X.eq x k).
- contradict H4.
- destruct H2.
- apply InA_eqA with (x,x0); eauto.
-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.
-
-Lemma anti_elements_mapsto : forall l k e, NoDupA (PX.eqk (elt:=elt'')) l ->
-  (MapsTo k e (anti_elements l) <-> L.PX.MapsTo k e l).
-Proof. 
-intros. 
-unfold anti_elements.
-rewrite anti_elements_mapsto_aux; auto; unfold empty; auto.
-intuition.
-inversion H1.
-inversion 2.
-Qed.
+Ltac nonify t := 
+ match t with (find ?y (map2_opt ?m ?m')) => 
+ replace t with (@None elt'');
+ [ | symmetry; rewrite not_find_iff; auto; intro;
+     destruct (@map2_opt_2 m m' y); auto; order ]
+ end.
+
+Lemma map2_opt_1 : forall m m' y, bst m -> bst m' -> 
+ In y m \/ In y m' ->
+ find y (map2_opt m m') = f0 y (find y m) (find y m').
+Proof.
+intros m m'; functional induction (map2_opt m m'); intros;
+ auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; 
+ try (generalize (split_in_1 x1 H0)(split_in_2 x1 H0)
+       (split_in_3 x1 H0)(split_bst x1 H0)(split_find x1 y H0)
+       (split_lt_tree (x:=x1) H0)(split_gt_tree (x:=x1) H0);
+       rewrite e1; simpl in *; destruct 4; intros; inv bst; 
+      subst o2; rewrite H7, ?join_find, ?concat_find; auto).
+
+simpl; destruct H1; [ inversion_clear H1 | ].
+rewrite mapr_f0; auto.
+generalize (in_find H0 H1); destruct (find y m2); intuition.
+
+factornode l1 x1 d1 r1 _x as m1.
+destruct H1; [ | inversion_clear H1 ].
+rewrite mapl_f0; auto.
+generalize (in_find H H1); destruct (find y m1); intuition.
+
+simpl; destruct X.compare; auto.
+apply IHt1; auto; map2_aux.
+rewrite (@f0_compat y x1), <- f0_f; auto.
+apply IHt0; auto; map2_aux.
+intros z Hz; destruct (@map2_opt_2 l1 l2' z); auto.
+intros z Hz; destruct (@map2_opt_2 r1 r2' z); auto.
+
+destruct X.compare.
+nonify (find y (map2_opt r1 r2')).
+apply IHt1; auto; map2_aux.
+nonify (find y (map2_opt r1 r2')).
+nonify (find y (map2_opt l1 l2')).
+rewrite (@f0_compat y x1), <- f0_f; auto.
+nonify (find y (map2_opt l1 l2')).
+rewrite IHt0; auto; [ | map2_aux ].
+destruct (f0 y (find y r1) (find y r2')); auto.
+intros y1 y2 Hy1 Hy2; apply X.lt_trans with x1.
+ destruct (@map2_opt_2 l1 l2' y1); auto.
+ destruct (@map2_opt_2 r1 r2' y2); auto.
+Qed.
+
+End Map2_opt.
+
+Section Map2.
+Variable elt elt' elt'' : Type.
+Variable f : option elt -> option elt' -> option elt''.
 
-Lemma map2_bst : forall (m: t elt)(m': t elt'), bst (map2 m m').
+Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m').
 Proof.
-unfold map2; intros; apply anti_elements_bst; auto.
+unfold map2; intros.
+apply map2_opt_bst with (fun _ => f); auto using map_option_bst; 
+ intros; rewrite map_option_find; auto.
 Qed.
 
-Lemma find_elements : forall (elt:Type)(m: t elt) x, bst m -> 
-  L.find x (elements m) = find x m.
-Proof. 
-intros.
-case_eq (find x m); intros.
-apply L.find_1.
-apply elements_sort; auto.
-red; rewrite elements_mapsto.
-apply find_2; auto.
-case_eq (L.find x (elements m)); auto; intros.
-rewrite <- H0; symmetry.
-apply find_1; auto.
-rewrite <- elements_mapsto.
-apply L.find_2; auto.
-Qed.
-
-Lemma find_anti_elements : forall (l: list (key*elt'')) x, 
- sort (@PX.ltk _) l -> 
- find x (anti_elements l) = L.find x l.
-Proof.
-intros.
-case_eq (L.find x l); intros.
-apply find_1.
-apply anti_elements_bst; auto.
-rewrite anti_elements_mapsto; auto using L.PX.Sort_NoDupA, L.find_2.
-case_eq (find x (anti_elements l)); auto; intros.
-rewrite <- H0; symmetry.
-apply L.find_1; auto.
-rewrite <- anti_elements_mapsto; auto using L.PX.Sort_NoDupA, find_2.
-Qed.
-
-Lemma map2_1 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> 
-  In x m \/ In x m' -> find x (map2 m m') = f (find x m) (find x m').       
-Proof. 
+Lemma map2_1 : forall m m' y, bst m -> bst m' -> 
+  In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y m').
+Proof.
 unfold map2; intros.
-rewrite find_anti_elements; auto.
-rewrite <- find_elements; auto.
-rewrite <- find_elements; auto.
-apply L.map2_1; auto.
-apply elements_sort; auto.
-apply elements_sort; auto.
-do 2 rewrite elements_in; auto.
-apply L.map2_sorted; auto.
-apply elements_sort; auto.
-apply elements_sort; auto.
+rewrite (map2_opt_1 (f0:=fun _ => f)); 
+ auto using map_option_bst; intros; rewrite map_option_find; auto.
 Qed.
 
-Lemma map2_2 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> 
-  In x (map2 m m') -> In x m \/ In x m'.
+Lemma map2_2 : forall m m' y, bst m -> bst m' -> 
+  In y (map2 f m m') -> In y m \/ In y m'.
 Proof.
 unfold map2; intros.
-do 2 rewrite <- elements_in.
-apply L.map2_2 with (f:=f); auto.
-apply elements_sort; auto.
-apply elements_sort; auto.
-revert H1.
-rewrite <- In_alt.
-destruct 1.
-exists x0.
-rewrite <- anti_elements_mapsto; auto.
-apply L.PX.Sort_NoDupA; auto.
-apply L.map2_sorted; auto.
-apply elements_sort; auto.
-apply elements_sort; auto.
+eapply map2_opt_2 with (f0:=fun _ => f); eauto; intros.
+ apply map_option_bst; auto.
+ apply map_option_bst; auto.
+ rewrite map_option_find; auto.
+ rewrite map_option_find; auto.
 Qed.
 
 End Map2.
-End Elts.
+End Proofs.
 End Raw.
 
 (** * Encapsulation
@@ -1367,6 +1812,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Module E := X.
  Module Raw := Raw I X. 
+ Import Raw.Proofs.
 
  Record bst (elt:Type) := 
   Bst {this :> Raw.tree elt; is_bst : Raw.bst this}.
@@ -1381,17 +1827,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 := Bst (Raw.empty_bst elt).
+ Definition empty : t elt := Bst (empty_bst elt).
  Definition is_empty m : bool := Raw.is_empty m.(this).
- 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 add x e m : t elt := Bst (add_bst x e m.(is_bst)).
+ Definition remove x m : t elt := Bst (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' := Bst (Raw.map_bst f m.(is_bst)).
+ Definition map f m : t elt' := Bst (map_bst f m.(is_bst)).
  Definition mapi (f:key->elt->elt') m : t elt' := 
-  Bst (Raw.mapi_bst f m.(is_bst)).
+  Bst (mapi_bst f m.(is_bst)).
  Definition map2 f m (m':t elt') : t elt'' := 
-  Bst (Raw.map2_bst f m m').
+  Bst (map2_bst f m.(is_bst) m'.(is_bst)).
  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.
@@ -1399,81 +1845,81 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this).
  Definition In x m : Prop := Raw.In0 x m.(this).
- Definition Empty m : Prop := Raw.Empty m.(this).
+ Definition Empty m : Prop := Empty m.(this).
 
- Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt.
- Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqke elt.
- Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.ltk elt.
+ Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
+ Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
+ Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.
 
  Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
- Proof. intros m; exact (@Raw.MapsTo_1 _ m.(this)). Qed.
+ Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed.
  
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
  Proof.
- unfold In, mem; intros m x; rewrite Raw.In_alt; simpl; apply Raw.mem_1; auto.
+ unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.
  apply m.(is_bst).
  Qed.
  
  Lemma mem_2 : forall m x, mem x m = true -> In x m. 
  Proof.
- unfold In, mem; intros m x; rewrite Raw.In_alt; simpl; apply Raw.mem_2; auto.
+ unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto.
  Qed.
 
  Lemma empty_1 : Empty empty.
- Proof. exact (@Raw.empty_1 elt). Qed.
+ Proof. exact (@empty_1 elt). Qed.
 
  Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
- Proof. intros m; exact (@Raw.is_empty_1 _ m.(this)). Qed.
+ Proof. intros m; exact (@is_empty_1 _ m.(this)). Qed.
  Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
- Proof. intros m; exact (@Raw.is_empty_2 _ m.(this)). Qed.
+ Proof. intros m; exact (@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). Qed.
+ Proof. intros m x y e; exact (@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'). Qed.
+ Proof. intros m x y e e'; exact (@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'). Qed.
+ Proof. intros m x y e e'; exact (@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.
+ unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto.
  apply m.(is_bst).
  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)). Qed.
+ Proof. intros m x y e; exact (@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)). Qed.
+ Proof. intros m x y e; exact (@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. 
- Proof. intros m x e; exact (@Raw.find_1 elt _ x e m.(is_bst)). Qed.
+ Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
- Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@find_2 elt m.(this)). Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
- Proof. intros m; exact (@Raw.fold_1 elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed.
 
  Lemma elements_1 : forall m x e,       
    MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
  Proof.
- intros; unfold elements, MapsTo, eq_key_elt; rewrite Raw.elements_mapsto; auto.
+ intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto.
  Qed.
 
  Lemma elements_2 : forall m x e,   
    InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
  Proof.
- intros; unfold elements, MapsTo, eq_key_elt; rewrite <- Raw.elements_mapsto; auto.
+ intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto.
  Qed.
 
  Lemma elements_3 : forall m, sort lt_key (elements m).  
- Proof. intros m; exact (@Raw.elements_sort elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed.
 
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
- Proof. intros m; exact (@Raw.elements_nodup elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed.
 
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
- Proof. intro m; exact (@Raw.elements_cardinal elt m.(this)). Qed.
+ Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed.
 
  Definition Equal m m' := forall y, find y m = find y m'.
  Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
@@ -1481,50 +1927,51 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
  Definition Equivb cmp := Equiv (Cmp cmp).
 
- Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Equivb cmp m m'.
+ Lemma Equivb_Equivb : forall cmp m m', 
+  Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
  Proof. 
- intros; unfold Equivb, Equiv, Raw.Equivb, In; intuition.
- generalize (H0 k); do 2 rewrite Raw.In_alt; intuition.
- generalize (H0 k); do 2 rewrite Raw.In_alt; intuition.
- generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition.
- generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition.
+ intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.
+ generalize (H0 k); do 2 rewrite In_alt; intuition.
+ generalize (H0 k); do 2 rewrite In_alt; intuition.
+ generalize (H0 k); do 2 rewrite <- In_alt; intuition.
+ generalize (H0 k); do 2 rewrite <- In_alt; intuition.
  Qed.
 
  Lemma equal_1 : forall m m' cmp, 
    Equivb cmp m m' -> equal cmp m m' = true. 
  Proof. 
  unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; 
-  intros; simpl in *; rewrite Raw.equal_Equivb; auto.
+  intros; simpl in *; rewrite 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) (m',b') cmp; rewrite Equivb_Equivb; 
-  intros; simpl in *; rewrite <-Raw.equal_Equivb; auto.
+  intros; simpl in *; rewrite <-equal_Equivb; auto.
  Qed.
 
  End Elt.
 
  Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
         MapsTo x e m -> MapsTo x (f e) (map f m).
- Proof. intros elt elt' m x e f; exact (@Raw.map_1 elt elt' f m.(this) x e). Qed.
+ Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed.
 
  Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
  Proof.
- intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite Raw.In_alt; simpl.
- apply Raw.map_2; auto.
+ intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl.
+ apply map_2; auto.
  Qed. 
 
  Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
         (f:key->elt->elt'), MapsTo x e m -> 
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
- Proof. intros elt elt' m x e f; exact (@Raw.mapi_1 elt elt' f m.(this) x e). Qed.
+ Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed.
  Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
         (f:key->elt->elt'), In x (mapi f m) -> In x m.
  Proof.
- intros elt elt' m x f; unfold In in *; do 2 rewrite Raw.In_alt; simpl; apply Raw.mapi_2; auto.
- Qed. 
+ intros elt elt' m x f; unfold In in *; do 2 rewrite In_alt; simpl; apply mapi_2; auto.
+ Qed.
 
  Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
     (x:key)(f:option elt->option elt'->option elt''), 
@@ -1532,7 +1979,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
     find x (map2 f m m') = f (find x m) (find x m'). 
  Proof. 
  unfold find, map2, In; intros elt elt' elt'' m m' x f.
- do 2 rewrite Raw.In_alt; intros; simpl; apply Raw.map2_1; auto.
+ do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.
  apply m.(is_bst).
  apply m'.(is_bst).
  Qed.
@@ -1542,7 +1989,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
      In x (map2 f m m') -> In x m \/ In x m'.
  Proof. 
  unfold In, map2; intros elt elt' elt'' m m' x f.
- do 3 rewrite Raw.In_alt; intros; simpl in *; eapply Raw.map2_2; eauto.
+ do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.
  apply m.(is_bst).
  apply m'.(is_bst).
  Qed.
@@ -1552,128 +1999,154 @@ End IntMake.
 
 Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: 
     Sord with Module Data := D 
-            with Module MapS.E := X.
+         with Module MapS.E := X.
 
   Module Data := D.
   Module Import MapS := IntMake(I)(X). 
-  Module Import MD := OrderedTypeFacts(D).
   Module LO := FMapList.Make_ord(X)(D).
+  Module R := Raw.
+  Module P := Raw.Proofs.
 
-  Definition t := MapS.t D.t. 
+  Definition t := MapS.t D.t.
 
   Definition cmp e e' := 
    match D.compare e e' with EQ _ => true | _ => false end.
 
-  Definition elements (m:t) := 
-    LO.MapS.Build_slist (Raw.elements_sort m.(is_bst)).
-
-  Function compare_aux (e:Raw.enumeration D.t * Raw.enumeration D.t) 
-   { measure Raw.cardinal_e_2 e } : comparison := 
-  match e with 
-  | (Raw.End, Raw.End) => Eq
-  | (Raw.End, Raw.More _ _ _ _) => Lt
-  | (Raw.More _ _ _ _, Raw.End) => Gt
-  | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
-      match X.compare x1 x2 with
-      | EQ _ => match D.compare d1 d2 with 
-                | EQ _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2)
-                | LT _ => Lt
-                | GT _ => Gt
-                end
-      | LT _ => Lt
-      | GT _ => Gt
-      end
-  end.
+  (** One step of comparison of elements *)
+
+  Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
+   match e2 with
+    | R.End => Gt
+    | R.More x2 d2 r2 e2 =>
+       match X.compare x1 x2 with
+        | EQ _ => match D.compare d1 d2 with 
+                   | EQ _ => cont (R.cons r2 e2)
+                   | LT _ => Lt 
+                   | GT _ => Gt
+                  end
+        | LT _ => Lt
+        | GT _ => Gt
+       end
+   end.
+
+  (** Comparison of left tree, middle element, then right tree *)
+
+  Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 :=
+   match s1 with
+    | R.Leaf => cont e2
+    | R.Node l1 x1 d1 r1 _ =>
+       compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2
+   end.
+
+  (** Initial continuation *)
+
+  Definition compare_end (e2:R.enumeration D.t) :=
+   match e2 with R.End => Eq | _ => Lt end.
+
+  (** The complete comparison *)
+
+  Definition compare_pure s1 s2 := 
+   compare_cont s1 compare_end (R.cons s2 (Raw.End _)).
+
+  (** Correctness of this comparison *)
+
+  Definition Cmp c :=
+   match c with
+    | Eq => LO.eq_list
+    | Lt => LO.lt_list
+    | Gt => (fun l1 l2 => LO.lt_list l2 l1)
+   end.
+
+  Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, 
+   X.eq x1 x2 -> D.eq d1 d2 ->
+   Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
   Proof.
-  intros; unfold Raw.cardinal_e_2; simpl; 
-  abstract (do 2 rewrite Raw.cons_cardinal_e; romega with *).
-  Defined.
+   destruct c; simpl; intros; P.MX.elim_comp; auto.
+  Qed.
+  Hint Resolve cons_Cmp.
 
-  Lemma compare_aux_Eq : 
-   forall e, Raw.sorted_e (fst e) -> Raw.sorted_e (snd e) -> 
-   compare_aux e = Eq -> 
-   LO.eq_list (Raw.flatten_e (fst e)) (Raw.flatten_e (snd e)).
+  Lemma compare_end_Cmp :
+   forall e2, Cmp (compare_end e2) nil (P.flatten_e e2).
   Proof.
-  intros e; functional induction compare_aux e; simpl in *; intros; 
-   try discriminate; simpl; auto; try clear e3 e4; 
-   Raw.MX.elim_comp; split; auto.
-  inversion_clear H.
-  inversion_clear H0.
-  destruct (@Raw.cons_1 _ r1 e1); auto.
-  destruct (@Raw.cons_1 _ r2 e2); auto.
-  rewrite <- H12, <- H14; auto.
+   destruct e2; simpl; auto.
   Qed.
 
-  Lemma compare_aux_Lt : 
-   forall e,  Raw.sorted_e (fst e) -> Raw.sorted_e (snd e) -> 
-   compare_aux e = Lt -> 
-   LO.lt_list (Raw.flatten_e (fst e)) (Raw.flatten_e (snd e)).
+  Lemma compare_more_Cmp : forall x1 d1 cont x2 d2 r2 e2 l,
+    Cmp (cont (R.cons r2 e2)) l (R.elements r2 ++ P.flatten_e e2) ->
+     Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l)
+       (P.flatten_e (R.More x2 d2 r2 e2)).
   Proof.
-  intros e; functional induction compare_aux e; simpl in *; intros; 
-   try discriminate; simpl; auto; clear e3; try clear e4; 
-   Raw.MX.elim_comp; auto.
-  right; split; auto.
-  inversion_clear H.
-  inversion_clear H0.
-  destruct (@Raw.cons_1 _ r1 e1); auto.
-  destruct (@Raw.cons_1 _ r2 e2); auto.
-  rewrite <- H12, <- H14; auto.
+   simpl; intros; destruct X.compare; simpl; 
+    try destruct D.compare; simpl; auto; P.MX.elim_comp; auto.
+  Qed.
+  
+  Lemma compare_cont_Cmp : forall s1 cont e2 l,
+   (forall e, Cmp (cont e) l (P.flatten_e e)) ->
+   Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2).
+  Proof.
+   induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto.
+   rewrite <- P.elements_node; simpl.
+   apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2].
+   simpl; auto.
+   apply compare_more_Cmp.
+   rewrite <- P.cons_1; auto.
   Qed.
 
-  Lemma compare_aux_Gt : 
-   forall e,  Raw.sorted_e (fst e) -> Raw.sorted_e (snd e) -> 
-   compare_aux e = Gt -> 
-   LO.lt_list (Raw.flatten_e (snd e)) (Raw.flatten_e (fst e)).
+  Lemma compare_Cmp : forall s1 s2,
+   Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2).
   Proof.
-  intros e; functional induction compare_aux e; simpl in *; intros; 
-   try discriminate; simpl; auto; clear e3; try clear e4; 
-   Raw.MX.elim_comp; auto.
-  right; split; auto.
-  inversion_clear H.
-  inversion_clear H0.
-  destruct (@Raw.cons_1 _ r1 e1); auto.
-  destruct (@Raw.cons_1 _ r2 e2); auto.
-  rewrite <- H12, <- H14; auto.
+   intros; unfold compare_pure.
+   rewrite (app_nil_end (R.elements s1)).
+   replace (R.elements s2) with (P.flatten_e (R.cons s2 (R.End _))) by
+    (rewrite P.cons_1; simpl; rewrite <- app_nil_end; auto).
+   auto using compare_cont_Cmp, compare_end_Cmp.
   Qed.
 
-  Definition eq (m1 m2 : t) := LO.eq (elements m1) (elements m2).
+  (** The dependent-style [compare] *)
 
-  Definition lt (m1 m2 : t) := LO.lt (elements m1) (elements m2).
+  Definition eq (m1 m2 : t) := LO.eq_list (elements m1) (elements m2).
+  Definition lt (m1 m2 : t) := LO.lt_list (elements m1) (elements m2).
 
-  Definition compare (m1 m2 : t) : Compare lt eq m1 m2.
+  Definition compare (s s':t) : Compare lt eq s s'.
   Proof.
-   intros.
-   destruct (@Raw.cons_1 _ _ (Raw.End _) m1.(is_bst)).
-    constructor.
-    inversion 2.
-   destruct (@Raw.cons_1 _ _ (Raw.End _) m2.(is_bst)).
-    constructor.
-    inversion 2.
-   set (e:= (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))).
-   generalize (@compare_aux_Eq e H H1)(@compare_aux_Lt e H H1)
-     (@compare_aux_Gt e H H1).
-   destruct (compare_aux e); intros; [ apply EQ | apply LT | apply GT ]; 
-    unfold eq, LO.eq, lt, LO.lt in *; simpl in *; 
-    rewrite H0, H2, <-app_nil_end, <-app_nil_end in *; auto.
+   intros (s,b) (s',b').
+   generalize (compare_Cmp s s').
+   destruct compare_pure; intros; [apply EQ|apply LT|apply GT]; red; auto.
   Defined.
+  
+  (* Proofs about [eq] and [lt] *)
+
+  Definition selements (m1 : t) := 
+   LO.MapS.Build_slist (P.elements_sort m1.(is_bst)).
+
+  Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
+  Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).
 
-  Lemma eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
+  Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2.
+  Proof.
+   unfold eq, seq, selements, elements, LO.eq; intuition.
+  Qed.
+
+  Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2.
+  Proof.
+   unfold lt, slt, selements, elements, LO.lt; intuition.
+  Qed.
+
+  Lemma eq_1 : forall (m m' : t), Equivb cmp m m' -> eq m m'.
   Proof.
   intros m m'.
-  unfold eq.
+  rewrite eq_seq; unfold seq.
   rewrite Equivb_Equivb.
-  rewrite Raw.Equivb_elements.
-  intros.
-  apply LO.eq_1.
-  auto.
+  rewrite P.Equivb_elements.
+  auto using LO.eq_1.
   Qed.
 
   Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
   Proof.
   intros m m'.
-  unfold eq.
+  rewrite eq_seq; unfold seq.
   rewrite Equivb_Equivb.
-  rewrite Raw.Equivb_elements.
+  rewrite P.Equivb_elements.
   intros.
   generalize (LO.eq_2 H).
   auto.
@@ -1681,27 +2154,30 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Lemma eq_refl : forall m : t, eq m m.
   Proof. 
-  unfold eq; intros; apply LO.eq_refl.
+  intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl.
   Qed.
 
   Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
   Proof.
-  unfold eq; intros; apply LO.eq_sym; auto.
+  intros m1 m2; rewrite 2 eq_seq; unfold seq; intros; apply LO.eq_sym; auto.
   Qed.
 
   Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
   Proof.
-  unfold eq; intros; eapply LO.eq_trans; eauto.
+  intros m1 m2 M3; rewrite 3 eq_seq; unfold seq.
+   intros; eapply LO.eq_trans; eauto.
   Qed.
 
   Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
   Proof.
-  unfold lt; intros; eapply LO.lt_trans; eauto.
+  intros m1 m2 m3; rewrite 3 lt_slt; unfold slt;  
+   intros; eapply LO.lt_trans; eauto.
   Qed.
 
   Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
   Proof.
-  unfold lt, eq; intros; apply LO.lt_not_eq; auto.
+  intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; 
+   intros; apply LO.lt_not_eq; auto.
   Qed.
 
 End IntMake_ord.
@@ -1715,3 +2191,4 @@ Module Make_ord (X: OrderedType)(D: OrderedType)
  <: Sord with Module Data := D 
             with Module MapS.E := X
  :=IntMake_ord(Z_as_Int)(X)(D).
+