Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

21 files changed, 3512 insertions, 1316 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 24cbc3f9..da1d9e98 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -11,7 +11,7 @@ Require Import Plus.
 Require Import Compare_dec.
 Require Import Even.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Type n : nat.
 
@@ -69,24 +69,24 @@ Proof.
     (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
 Qed.
 
-Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
-with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Lemma div2_even n : div2 n = div2 (S n) -> even n
+with div2_odd n : S (div2 n) = div2 (S n) -> odd n.
 Proof.
-  destruct n; intro H.
-    (* 0 *) constructor.
-    (* S n *) constructor. apply div2_odd. rewrite H. trivial.
-  destruct n; intro H.
-    (* 0 *) discriminate.
-    (* S n *) constructor. apply div2_even. injection H as <-. trivial.
+{ destruct n; intro H.
+  - constructor.
+  - constructor. apply div2_odd. rewrite H. trivial. }
+{ destruct n; intro H.
+  - discriminate.
+  - constructor. apply div2_even. injection H as <-. trivial. }
 Qed.
 
 Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
-Lemma even_odd_div2 :
-  forall n,
-    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Lemma even_odd_div2 n :
+ (even n <-> div2 n = div2 (S n)) /\
+ (odd n <-> S (div2 n) = div2 (S n)).
 Proof.
-  auto decomp using div2_odd, div2_even, odd_div2, even_div2.
+ split; split; auto using div2_odd, div2_even, odd_div2, even_div2.
 Qed.
 
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d1eabcab..9cd0b31b 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -221,7 +221,7 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
 
 Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
   (at level 200, x binder, right associativity,
-   format "'[' 'exists'  '/  ' x .. y ,  '/  ' p ']'")
+   format "'[' 'exists'  '/  ' x  ..  y ,  '/  ' p ']'")
   : type_scope.
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
@@ -404,7 +404,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
 Notation "'exists' ! x .. y , p" :=
   (ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
   (at level 200, x binder, right associativity,
-   format "'[' 'exists'  !  '/  ' x .. y ,  '/  ' p ']'")
+   format "'[' 'exists'  !  '/  ' x  ..  y ,  '/  ' p ']'")
   : type_scope.
 
 Lemma unique_existence : forall (A:Type) (P:A->Prop),
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e929c561..d85f5363 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,7 +19,6 @@ Declare ML Module "extraction_plugin".
 Declare ML Module "decl_mode_plugin".
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
-Declare ML Module "dp_plugin".
 Declare ML Module "recdef_plugin".
 Declare ML Module "subtac_plugin".
 Declare ML Module "xml_plugin".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 637994b2..5b7afc99 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -60,7 +60,7 @@ Add Printing Let sigT2.
 
 (** Projections of [sig]
 
-    An element [y] of a subset [{x:A & (P x)}] is the pair of an [a]
+    An element [y] of a subset [{x:A | (P x)}] is the pair of an [a]
     of type [A] and of a proof [h] that [a] satisfies [P].  Then
     [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
     proof of [(P a)] *)
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index e849967c..d372de8e 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -14,7 +14,7 @@ This library includes the following files:
   sets, implemented as lists.
 
 \item {\tt Streams.v} defines the type of infinite lists (streams). It is a
-  coinductive type. Basic facts are stated and proved. The streams are
+  co-inductive type. Basic facts are stated and proved. The streams are
   also polymorphic.
 
 \end{itemize}
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 8d82bc8e..fb7898c6 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -385,7 +385,7 @@ Qed.
 Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice :
   ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice).
 Proof.
-  auto decomp using
+  intuition auto using
     guarded_rel_choice_imp_rel_choice,
     rel_choice_and_proof_irrel_imp_guarded_rel_choice.
 Qed.
@@ -439,7 +439,7 @@ Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice :
   FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises
   <-> GuardedFunctionalChoice.
 Proof.
-  auto decomp using
+  intuition auto using
     guarded_fun_choice_imp_indep_of_general_premises,
     guarded_fun_choice_imp_fun_choice,
     fun_choice_and_indep_general_prem_imp_guarded_fun_choice.
@@ -480,7 +480,7 @@ Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice :
   FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox
   <-> OmniscientFunctionalChoice.
 Proof.
-  auto decomp using
+  intuition auto using
     omniscient_fun_choice_imp_small_drinker,
     omniscient_fun_choice_imp_fun_choice,
     fun_choice_and_small_drinker_imp_omniscient_fun_choice.
@@ -547,7 +547,7 @@ Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon :
   (EpsilonStatement ->
    SmallDrinker'sParadox * ConstructiveIndefiniteDescription).
 Proof.
-  auto decomp using
+  intuition auto using
     epsilon_imp_constructive_indefinite_description,
     constructive_indefinite_description_and_small_drinker_imp_epsilon,
     epsilon_imp_small_drinker.
@@ -689,7 +689,7 @@ Qed.
 Corollary dep_iff_non_dep_functional_rel_reification :
   FunctionalRelReification <-> DependentFunctionalRelReification.
 Proof.
-  auto decomp using
+  intuition auto using
     non_dep_dep_functional_rel_reification,
     dep_non_dep_functional_rel_reification.
 Qed.
@@ -814,9 +814,9 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
   (forall P:Prop, P \/ ~ P) ->
   forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-  intros FunReify EM C; auto decomp using
-    constructive_definite_descr_excluded_middle,
-    (relative_non_contradiction_of_definite_descr (C:=C)).
+  intros FunReify EM C H.
+  apply relative_non_contradiction_of_definite_descr; trivial.
+  auto using constructive_definite_descr_excluded_middle.
 Qed.
 
 (**********************************************************************)
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index bdada486..1e66e2b5 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -13,7 +13,7 @@
     It follows the implementation from Ocaml's standard library,
 
     All operations given here expect and produce well-balanced trees
-    (in the ocaml sense: heigths of subtrees shouldn't differ by more
+    (in the ocaml sense: heights of subtrees shouldn't differ by more
     than 2), and hence has low complexities (e.g. add is logarithmic
     in the size of the set). But proving these balancing preservations
     is in fact not necessary for ensuring correct operational behavior
@@ -31,74 +31,41 @@
     code after extraction.
 *)
 
-Require Import MSetInterface ZArith Int.
+Require Import MSetInterface MSetGenTree ZArith Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
-(* for nicer extraction, we create only logical inductive principles *)
+(* for nicer extraction, we create inductive principles
+   only when needed *)
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
 
 (** * Ops : the pure functions *)
 
-Module Ops (Import I:Int)(X:OrderedType) <: WOps X.
+Module Ops (Import I:Int)(X:OrderedType) <: MSetInterface.Ops X.
 Local Open Scope Int_scope.
-Local Open Scope lazy_bool_scope.
 
-Definition elt := X.t.
-Hint Transparent elt.
+(** ** Generic trees instantiated with integer height *)
 
-(** ** Trees
+(** We reuse a generic definition of trees where the information
+    parameter is a [Int.t]. Functions like mem or fold are also
+    provided by this generic functor. *)
 
-   The fourth field of [Node] is the height of the tree *)
-
-Inductive tree :=
-  | Leaf : tree
-  | Node : tree -> X.t -> tree -> int -> tree.
+Include MSetGenTree.Ops X I.
 
 Definition t := tree.
 
-(** ** Basic functions on trees: height and cardinal *)
+(** ** Height of trees *)
 
 Definition height (s : t) : int :=
   match s with
   | Leaf => 0
-  | Node _ _ _ h => h
-  end.
-
-Fixpoint cardinal (s : t) : nat :=
-  match s with
-   | Leaf => 0%nat
-   | Node l _ r _ => S (cardinal l + cardinal r)
+  | Node h _ _ _ => h
   end.
 
-(** ** Empty Set *)
-
-Definition empty := Leaf.
-
-(** ** Emptyness test *)
-
-Definition is_empty s :=
-  match s with Leaf => true | _ => false end.
-
-(** ** Membership *)
-
-(** The [mem] function is deciding membership. It exploits the
-    binary search tree invariant to achieve logarithmic complexity. *)
-
-Fixpoint mem x s :=
-   match s with
-     |  Leaf => false
-     |  Node l y r _ => match X.compare x y with
-             | Lt => mem x l
-             | Eq => true
-             | Gt => mem x r
-         end
-   end.
-
 (** ** Singleton set *)
 
-Definition singleton x := Node Leaf x Leaf 1.
+Definition singleton x := Node 1 Leaf x Leaf.
 
 (** ** Helper functions *)
 
@@ -106,7 +73,7 @@ Definition singleton x := Node Leaf x Leaf 1.
     to be balanced and [|height l - height r| <= 2]. *)
 
 Definition create l x r :=
-   Node l x r (max (height l) (height r) + 1).
+   Node (max (height l) (height r) + 1) l x r.
 
 (** [bal l x r] acts as [create], but performs one step of
     rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *)
@@ -119,13 +86,13 @@ Definition bal l x r :=
   if gt_le_dec hl (hr+2) then
     match l with
      | Leaf => assert_false l x r
-     | Node ll lx lr _ =>
+     | Node _ ll lx lr =>
        if ge_lt_dec (height ll) (height lr) then
          create ll lx (create lr x r)
        else
          match lr with
           | Leaf => assert_false l x r
-          | Node lrl lrx lrr _ =>
+          | Node _ lrl lrx lrr =>
               create (create ll lx lrl) lrx (create lrr x r)
          end
     end
@@ -133,13 +100,13 @@ Definition bal l x r :=
     if gt_le_dec hr (hl+2) then
       match r with
        | Leaf => assert_false l x r
-       | Node rl rx rr _ =>
+       | Node _ rl rx rr =>
          if ge_lt_dec (height rr) (height rl) then
             create (create l x rl) rx rr
          else
            match rl with
             | Leaf => assert_false l x r
-            | Node rll rlx rlr _ =>
+            | Node _ rll rlx rlr =>
                 create (create l x rll) rlx (create rlr rx rr)
            end
       end
@@ -149,11 +116,11 @@ Definition bal l x r :=
 (** ** Insertion *)
 
 Fixpoint add x s := match s with
-   | Leaf => Node Leaf x Leaf 1
-   | Node l y r h =>
+   | Leaf => Node 1 Leaf x Leaf
+   | Node h l y r =>
       match X.compare x y with
          | Lt => bal (add x l) y r
-         | Eq => Node l y r h
+         | Eq => Node h l y r
          | Gt => bal l y (add x r)
       end
   end.
@@ -167,10 +134,10 @@ Fixpoint add x s := match s with
 Fixpoint join l : elt -> t -> t :=
   match l with
     | Leaf => add
-    | Node ll lx lr lh => fun x =>
+    | Node lh ll lx lr => fun x =>
        fix join_aux (r:t) : t := match r with
-          | Leaf =>  add x l
-          | Node rl rx rr rh =>
+          | Leaf => add x l
+          | Node rh rl rx rr =>
                if gt_le_dec lh (rh+2) then bal ll lx (join lr x r)
                else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr
                else create l x r
@@ -180,14 +147,14 @@ Fixpoint join l : elt -> t -> t :=
 (** ** Extraction of minimum element
 
   Morally, [remove_min] is to be applied to a non-empty tree
-  [t = Node l x r h]. Since we can't deal here with [assert false]
+  [t = Node h l x r]. Since we can't deal here with [assert false]
   for [t=Leaf], we pre-unpack [t] (and forget about [h]).
 *)
 
 Fixpoint remove_min l x r : t*elt :=
   match l with
     | Leaf => (r,x)
-    | Node ll lx lr lh =>
+    | Node lh ll lx lr =>
        let (l',m) := remove_min ll lx lr in (bal l' x r, m)
   end.
 
@@ -201,7 +168,7 @@ Fixpoint remove_min l x r : t*elt :=
 Definition merge s1 s2 :=  match s1,s2 with
   | Leaf, _ => s2
   | _, Leaf => s1
-  | _, Node l2 x2 r2 h2 =>
+  | _, Node _ l2 x2 r2 =>
         let (s2',m) := remove_min l2 x2 r2 in bal s1 m s2'
 end.
 
@@ -209,34 +176,14 @@ end.
 
 Fixpoint remove x s := match s with
   | Leaf => Leaf
-  | Node l y r h =>
+  | Node _ l y r =>
       match X.compare x y with
          | Lt => bal (remove x l) y r
          | Eq => merge l r
-         | Gt => bal l  y (remove x r)
+         | Gt => bal l y (remove x r)
       end
    end.
 
-(** ** Minimum element *)
-
-Fixpoint min_elt s := match s with
-   | Leaf => None
-   | Node Leaf y _  _ => Some y
-   | Node l _ _ _ => min_elt l
-end.
-
-(** ** Maximum element *)
-
-Fixpoint max_elt s := match s with
-   | Leaf => None
-   | Node _ y Leaf  _ => Some y
-   | Node _ _ r _ => max_elt r
-end.
-
-(** ** Any element *)
-
-Definition choose := min_elt.
-
 (** ** Concatenation
 
     Same as [merge] but does not assume anything about heights.
@@ -246,7 +193,7 @@ Definition concat s1 s2 :=
    match s1, s2 with
       | Leaf, _ => s2
       | _, Leaf => s1
-      | _, Node l2 x2 r2 _ =>
+      | _, Node _ l2 x2 r2 =>
             let (s2',m) := remove_min l2 x2 r2 in
             join s1 m s2'
    end.
@@ -264,7 +211,7 @@ Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 
 Fixpoint split x s : triple := match s with
   | Leaf => << Leaf, false, Leaf >>
-  | Node l y r h =>
+  | Node _ l y r =>
      match X.compare x y with
       | Lt => let (ll,b,rl) := split x l in << ll, b, join rl y r >>
       | Eq => << l, true, r >>
@@ -277,7 +224,7 @@ Fixpoint split x s : triple := match s with
 Fixpoint inter s1 s2 := match s1, s2 with
     | Leaf, _ => Leaf
     | _, Leaf => Leaf
-    | Node l1 x1 r1 h1, _ =>
+    | Node _ l1 x1 r1, _ =>
             let (l2',pres,r2') := split x1 s2 in
             if pres then join (inter l1 l2') x1 (inter r1 r2')
             else concat (inter l1 l2') (inter r1 r2')
@@ -288,7 +235,7 @@ Fixpoint inter s1 s2 := match s1, s2 with
 Fixpoint diff s1 s2 := match s1, s2 with
  | Leaf, _ => Leaf
  | _, Leaf => s1
- | Node l1 x1 r1 h1, _ =>
+ | Node _ l1 x1 r1, _ =>
     let (l2',pres,r2') := split x1 s2 in
     if pres then concat (diff l1 l2') (diff r1 r2')
     else join (diff l1 l2') x1 (diff r1 r2')
@@ -311,187 +258,36 @@ Fixpoint union s1 s2 :=
  match s1, s2 with
   | Leaf, _ => s2
   | _, Leaf => s1
-  | Node l1 x1 r1 h1, _ =>
+  | Node _ l1 x1 r1, _ =>
      let (l2',_,r2') := split x1 s2 in
      join (union l1 l2') x1 (union r1 r2')
  end.
 
-(** ** Elements *)
-
-(** [elements_tree_aux acc t] catenates the elements of [t] in infix
-    order to the list [acc] *)
-
-Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t :=
-  match s with
-   | Leaf => acc
-   | Node l x r _ => elements_aux (x :: elements_aux acc r) l
-  end.
-
-(** then [elements] is an instanciation with an empty [acc] *)
-
-Definition elements := elements_aux nil.
-
 (** ** Filter *)
 
-Fixpoint filter_acc (f:elt->bool) acc s := match s with
-  | Leaf => acc
-  | Node l x r h =>
-     filter_acc f (filter_acc f (if f x then add x acc else acc) l) r
+Fixpoint filter (f:elt->bool) s := match s with
+  | Leaf => Leaf
+  | Node _ l x r =>
+    let l' := filter f l in
+    let r' := filter f r in
+    if f x then join l' x r' else concat l' r'
  end.
 
-Definition filter f := filter_acc f Leaf.
-
-
 (** ** Partition *)
 
-Fixpoint partition_acc (f:elt->bool)(acc : t*t)(s : t) : t*t :=
+Fixpoint partition (f:elt->bool)(s : t) : t*t :=
   match s with
-   | Leaf => acc
-   | Node l x r _ =>
-      let (acct,accf) := acc in
-      partition_acc f
-        (partition_acc f
-           (if f x then (add x acct, accf) else (acct, add x accf)) l) r
+   | Leaf => (Leaf, Leaf)
+   | Node _ l x r =>
+      let (l1,l2) := partition f l in
+      let (r1,r2) := partition f r in
+      if f x then (join l1 x r1, concat l2 r2)
+      else (concat l1 r1, join l2 x r2)
   end.
 
-Definition partition f := partition_acc f (Leaf,Leaf).
-
-(** ** [for_all] and [exists] *)
-
-Fixpoint for_all (f:elt->bool) s := match s with
-  | Leaf => true
-  | Node l x r _ => f x &&& for_all f l &&& for_all f r
-end.
-
-Fixpoint exists_ (f:elt->bool) s := match s with
-  | Leaf => false
-  | Node l x r _ => f x ||| exists_ f l ||| exists_ f r
-end.
-
-(** ** Fold *)
-
-Fixpoint fold (A : Type) (f : elt -> A -> A)(s : t) : A -> A :=
- fun a => match s with
-  | Leaf => a
-  | Node l x r _ => fold f r (f x (fold f l a))
- end.
-Arguments fold [A] f s _.
-
-
-(** ** Subset *)
-
-(** In ocaml, recursive calls are made on "half-trees" such as
-   (Node l1 x1 Leaf _) and (Node Leaf x1 r1 _). Instead of these
-   non-structural calls, we propose here two specialized functions for
-   these situations. This version should be almost as efficient as
-   the one of ocaml (closures as arguments may slow things a bit),
-   it is simply less compact. The exact ocaml version has also been
-   formalized (thanks to Function+measure), see [ocaml_subset] in
-   [MSetFullAVL].
- *)
-
-Fixpoint subsetl (subset_l1:t->bool) x1 s2 : bool :=
- match s2 with
-  | Leaf => false
-  | Node l2 x2 r2 h2 =>
-     match X.compare x1 x2 with
-      | Eq => subset_l1 l2
-      | Lt => subsetl subset_l1 x1 l2
-      | Gt => mem x1 r2 &&& subset_l1 s2
-     end
- end.
-
-Fixpoint subsetr (subset_r1:t->bool) x1 s2 : bool :=
- match s2 with
-  | Leaf => false
-  | Node l2 x2 r2 h2 =>
-     match X.compare x1 x2 with
-      | Eq => subset_r1 r2
-      | Lt => mem x1 l2 &&& subset_r1 s2
-      | Gt => subsetr subset_r1 x1 r2
-     end
- end.
-
-Fixpoint subset s1 s2 : bool := match s1, s2 with
-  | Leaf, _ => true
-  | Node _ _ _ _, Leaf => false
-  | Node l1 x1 r1 h1, Node l2 x2 r2 h2 =>
-     match X.compare x1 x2 with
-      | Eq => subset l1 l2 &&& subset r1 r2
-      | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2
-      | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2
-     end
- end.
-
-(** ** A new comparison algorithm suggested by Xavier Leroy
-
-    Transformation in C.P.S. suggested by Benjamin Grégoire.
-    The original ocaml code (with non-structural recursive calls)
-    has also been formalized (thanks to Function+measure), see
-    [ocaml_compare] in [MSetFullAVL]. The following code with
-    continuations computes dramatically faster in Coq, and
-    should be almost as efficient after extraction.
-*)
-
-(** Enumeration of the elements of a tree *)
-
-Inductive enumeration :=
- | End : enumeration
- | More : elt -> t -> enumeration -> enumeration.
-
-
-(** [cons t e] adds the elements of tree [t] on the head of
-    enumeration [e]. *)
-
-Fixpoint cons s e : enumeration :=
- match s with
-  | Leaf => e
-  | Node l x r h => cons l (More x r e)
- end.
-
-(** One step of comparison of elements *)
-
-Definition compare_more x1 (cont:enumeration->comparison) e2 :=
- match e2 with
- | End => Gt
- | More x2 r2 e2 =>
-     match X.compare x1 x2 with
-      | Eq => cont (cons r2 e2)
-      | Lt => Lt
-      | Gt => Gt
-     end
- end.
-
-(** Comparison of left tree, middle element, then right tree *)
-
-Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
- match s1 with
-  | Leaf => cont e2
-  | Node l1 x1 r1 _ =>
-     compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
-  end.
-
-(** Initial continuation *)
-
-Definition compare_end e2 :=
- match e2 with End => Eq | _ => Lt end.
-
-(** The complete comparison *)
-
-Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End).
-
-(** ** Equality test *)
-
-Definition equal s1 s2 : bool :=
- match compare s1 s2 with
-  | Eq => true
-  | _ => false
- end.
-
 End Ops.
 
 
-
 (** * MakeRaw
 
    Functor of pure functions + a posteriori proofs of invariant
@@ -500,265 +296,47 @@ End Ops.
 Module MakeRaw (Import I:Int)(X:OrderedType) <: RawSets X.
 Include Ops I X.
 
-(** * Invariants *)
-
-(** ** Occurrence in a tree *)
-
-Inductive InT (x : elt) : tree -> Prop :=
-  | IsRoot : forall l r h y, X.eq x y -> InT x (Node l y r h)
-  | InLeft : forall l r h y, InT x l -> InT x (Node l y r h)
-  | InRight : forall l r h y, InT x r -> InT x (Node l y r h).
-
-Definition In := InT.
-
-(** ** Some shortcuts *)
-
-Definition Equal s s' := forall a : elt, InT a s <-> InT a s'.
-Definition Subset s s' := forall a : elt, InT a s -> InT a s'.
-Definition Empty s := forall a : elt, ~ InT a s.
-Definition For_all (P : elt -> Prop) s := forall x, InT x s -> P x.
-Definition Exists (P : elt -> Prop) s := exists x, InT x s /\ P x.
-
-(** ** Binary search trees *)
-
-(** [lt_tree x s]: all elements in [s] are smaller than [x]
-   (resp. greater for [gt_tree]) *)
-
-Definition lt_tree x s := forall y, InT y s -> X.lt y x.
-Definition gt_tree x s := forall y, InT y s -> X.lt x y.
-
-(** [bst t] : [t] is a binary search tree *)
-
-Inductive bst : tree -> Prop :=
-  | BSLeaf : bst Leaf
-  | BSNode : forall x l r h, bst l -> bst r ->
-     lt_tree x l -> gt_tree x r -> bst (Node l x r h).
-
-(** [bst] is the (decidable) invariant our trees will have to satisfy. *)
-
-Definition IsOk := bst.
-
-Class Ok (s:t) : Prop := ok : bst s.
-
-Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }.
-
-Fixpoint ltb_tree x s :=
- match s with
-  | Leaf => true
-  | Node l y r _ =>
-     match X.compare x y with
-      | Gt => ltb_tree x l && ltb_tree x r
-      | _ => false
-     end
- end.
-
-Fixpoint gtb_tree x s :=
- match s with
-  | Leaf => true
-  | Node l y r _ =>
-     match X.compare x y with
-      | Lt => gtb_tree x l && gtb_tree x r
-      | _ => false
-     end
- end.
-
-Fixpoint isok s :=
- match s with
-  | Leaf => true
-  | Node l x r _ => isok l && isok r && ltb_tree x l && gtb_tree x r
- end.
-
-
-(** * Correctness proofs *)
+(** Generic definition of binary-search-trees and proofs of
+    specifications for generic functions such as mem or fold. *)
 
-Module Import MX := OrderedTypeFacts X.
+Include MSetGenTree.Props X I.
 
-(** * Automation and dedicated tactics *)
+(** Automation and dedicated tactics *)
 
-Scheme tree_ind := Induction for tree Sort Prop.
-
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
 Local Hint Immediate MX.eq_sym.
-Local Hint Unfold In lt_tree gt_tree.
+Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Unfold Ok.
-
-Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
- "as" ident(s) :=
- set (s:=Node l x r h) in *; clearbody s; clear l x r h.
-
-(** Automatic treatment of [Ok] hypothesis *)
-
-Ltac inv_ok := match goal with
- | H:Ok (Node _ _ _ _) |- _ => inversion_clear H; inv_ok
- | H:Ok Leaf |- _ => clear H; inv_ok
- | H:bst ?x |- _ => change (Ok x) in H; inv_ok
- | _ => idtac
-end.
-
-(** A tactic to repeat [inversion_clear] on all hyps of the
-    form [(f (Node _ _ _ _))] *)
-
-Ltac is_tree_constr c :=
-  match c with
-   | Leaf => idtac
-   | Node _ _ _ _ => idtac
-   | _ => fail
-  end.
-
-Ltac invtree f :=
-  match goal with
-     | H:f ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
-     | H:f _ ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
-     | H:f _ _ ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
-     | _ => idtac
-  end.
-
-Ltac inv := inv_ok; invtree InT.
-
-Ltac intuition_in := repeat progress (intuition; inv).
-
-(** Helper tactic concerning order of elements. *)
-
-Ltac order := match goal with
- | U: lt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
- | U: gt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
- | _ => MX.order
-end.
-
-
-(** [isok] is indeed a decision procedure for [Ok] *)
-
-Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true.
-Proof.
- induction s as [|l IHl y r IHr h]; simpl.
- unfold lt_tree; intuition_in.
- elim_compare x y.
- split; intros; try discriminate. assert (X.lt y x) by auto. order.
- split; intros; try discriminate. assert (X.lt y x) by auto. order.
- rewrite !andb_true_iff, <-IHl, <-IHr.
-  unfold lt_tree; intuition_in; order.
-Qed.
-
-Lemma gtb_tree_iff : forall x s, gt_tree x s <-> gtb_tree x s = true.
-Proof.
- induction s as [|l IHl y r IHr h]; simpl.
- unfold gt_tree; intuition_in.
- elim_compare x y.
- split; intros; try discriminate. assert (X.lt x y) by auto. order.
- rewrite !andb_true_iff, <-IHl, <-IHr.
-  unfold gt_tree; intuition_in; order.
- split; intros; try discriminate. assert (X.lt x y) by auto. order.
-Qed.
-
-Lemma isok_iff : forall s, Ok s <-> isok s = true.
-Proof.
- induction s as [|l IHl y r IHr h]; simpl.
- intuition_in.
- rewrite !andb_true_iff, <- IHl, <-IHr, <- ltb_tree_iff, <- gtb_tree_iff.
- intuition_in.
-Qed.
-
-Instance isok_Ok s : isok s = true -> Ok s | 10.
-Proof. intros; apply <- isok_iff; auto. Qed.
-
-
-(** * Basic results about [In], [lt_tree], [gt_tree], [height] *)
-
-(** [In] is compatible with [X.eq] *)
-
-Lemma In_1 :
- forall s x y, X.eq x y -> InT x s -> InT y s.
-Proof.
- induction s; simpl; intuition_in; eauto.
-Qed.
-Local Hint Immediate In_1.
-
-Instance In_compat : Proper (X.eq==>eq==>iff) InT.
-Proof.
-apply proper_sym_impl_iff_2; auto with *.
-repeat red; intros; subst. apply In_1 with x; auto.
-Qed.
-
-Lemma In_node_iff :
- forall l x r h y,
-  InT y (Node l x r h) <-> InT y l \/ X.eq y x \/ InT y r.
-Proof.
- intuition_in.
-Qed.
-
-(** Results about [lt_tree] and [gt_tree] *)
-
-Lemma lt_leaf : forall x : elt, lt_tree x Leaf.
-Proof.
- red; inversion 1.
-Qed.
-
-Lemma gt_leaf : forall x : elt, gt_tree x Leaf.
-Proof.
- red; inversion 1.
-Qed.
-
-Lemma lt_tree_node :
- forall (x y : elt) (l r : tree) (h : int),
- lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y r h).
-Proof.
- unfold lt_tree; intuition_in; order.
-Qed.
-
-Lemma gt_tree_node :
- forall (x y : elt) (l r : tree) (h : int),
- gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y r h).
-Proof.
- unfold gt_tree; intuition_in; order.
-Qed.
-
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+Local Hint Resolve elements_spec2.
 
-Lemma lt_tree_not_in :
- forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t.
-Proof.
- intros; intro; order.
-Qed.
-
-Lemma lt_tree_trans :
- forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t.
-Proof.
- eauto.
-Qed.
+(* Sometimes functional induction will expose too much of
+   a tree structure. The following tactic allows to factor back
+   a Node whose internal parts occurs nowhere else. *)
 
-Lemma gt_tree_not_in :
- forall (x : elt) (t : tree), gt_tree x t -> ~ InT x t.
-Proof.
- intros; intro; order.
-Qed.
+(* TODO: why Ltac instead of Tactic Notation don't work ? why clear ? *)
 
-Lemma gt_tree_trans :
- forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t.
-Proof.
- eauto.
-Qed.
-
-Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+Tactic Notation "factornode" ident(s) :=
+ try clear s;
+ match goal with
+   | |- context [Node ?l ?x ?r ?h] =>
+       set (s:=Node l x r h) in *; clearbody s; clear l x r h
+   | _ : context [Node ?l ?x ?r ?h] |- _ =>
+       set (s:=Node l x r h) in *; clearbody s; clear l x r h
+ end.
 
-(** * Inductions principles for some of the set operators *)
+(** Inductions principles for some of the set operators *)
 
 Functional Scheme bal_ind := Induction for bal Sort Prop.
 Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
 Functional Scheme merge_ind := Induction for merge Sort Prop.
-Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
-Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.
 Functional Scheme concat_ind := Induction for concat Sort Prop.
 Functional Scheme inter_ind := Induction for inter Sort Prop.
 Functional Scheme diff_ind := Induction for diff Sort Prop.
 Functional Scheme union_ind := Induction for union Sort Prop.
 
-Ltac induct s x :=
- induction s as [|l IHl x' r IHr h]; simpl; intros;
- [|elim_compare x x'; intros; inv].
-
-
-(** * Notations and helper lemma about pairs and triples *)
+(** Notations and helper lemma about pairs and triples *)
 
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
@@ -766,42 +344,9 @@ Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope.
 Notation "t #b" := (t_in t) (at level 9, format "t '#b'") : pair_scope.
 Notation "t #r" := (t_right t) (at level 9, format "t '#r'") : pair_scope.
 
-Open Local Scope pair_scope.
-
-
-(** * Empty set *)
-
-Lemma empty_spec : Empty empty.
-Proof.
- intro; intro.
- inversion H.
-Qed.
-
-Instance empty_ok : Ok empty.
-Proof.
- auto.
-Qed.
-
-(** * Emptyness test *)
-
-Lemma is_empty_spec : forall s, is_empty s = true <-> Empty s.
-Proof.
- destruct s as [|r x l h]; simpl; auto.
- split; auto. red; red; intros; inv.
- split; auto. try discriminate. intro H; elim (H x); auto.
-Qed.
-
-(** * Membership *)
-
-Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
-Proof.
- split.
- induct s x; auto; try discriminate.
- induct s x; intuition_in; order.
-Qed.
-
+Local Open Scope pair_scope.
 
-(** * Singleton set *)
+(** ** Singleton set *)
 
 Lemma singleton_spec : forall x y, InT y (singleton x) <-> X.eq y x.
 Proof.
@@ -813,9 +358,7 @@ Proof.
  unfold singleton; auto.
 Qed.
 
-
-
-(** * Helper functions *)
+(** ** Helper functions *)
 
 Lemma create_spec :
  forall l x r y,  InT y (create l x r) <-> X.eq y x \/ InT y l \/ InT y r.
@@ -846,7 +389,7 @@ Proof.
 Qed.
 
 
-(** * Insertion *)
+(** ** Insertion *)
 
 Lemma add_spec' : forall s x y,
  InT y (add x s) <-> X.eq y x \/ InT y s.
@@ -866,25 +409,25 @@ Proof.
 Qed.
 
 
-Open Scope Int_scope.
+Local Open Scope Int_scope.
 
-(** * Join *)
+(** ** Join *)
 
-(* Function/Functional Scheme can't deal with internal fix.
-   Let's do its job by hand: *)
+(** Function/Functional Scheme can't deal with internal fix.
+    Let's do its job by hand: *)
 
 Ltac join_tac :=
- intro l; induction l as [| ll _ lx lr Hlr lh];
-   [ | intros x r; induction r as [| rl Hrl rx rr _ rh]; unfold join;
+ intro l; induction l as [| lh ll _ lx lr Hlr];
+   [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join;
      [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
        [ match goal with |- context b [ bal ?a ?b ?c] =>
            replace (bal a b c)
-           with (bal ll lx (join lr x (Node rl rx rr rh))); [ | auto]
+           with (bal ll lx (join lr x (Node rh rl rx rr))); [ | auto]
          end
        | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
          [ match goal with |- context b [ bal ?a ?b ?c] =>
              replace (bal a b c)
-             with (bal (join (Node ll lx lr lh) x rl) rx rr); [ | auto]
+             with (bal (join (Node lh ll lx lr) x rl) rx rr); [ | auto]
            end
          | ] ] ] ]; intros.
 
@@ -910,10 +453,10 @@ Proof.
 Qed.
 
 
-(** * Extraction of minimum element *)
+(** ** Extraction of minimum element *)
 
-Lemma remove_min_spec : forall l x r h y,
- InT y (Node l x r h) <->
+Lemma remove_min_spec : forall l x r y h,
+ InT y (Node h l x r) <->
   X.eq y (remove_min l x r)#2 \/ InT y (remove_min l x r)#1.
 Proof.
  intros l x r; functional induction (remove_min l x r); simpl in *; intros.
@@ -921,13 +464,13 @@ Proof.
  rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition.
 Qed.
 
-Instance remove_min_ok l x r : forall h `(Ok (Node l x r h)),
+Instance remove_min_ok l x r : forall h `(Ok (Node h l x r)),
  Ok (remove_min l x r)#1.
 Proof.
  functional induction (remove_min l x r); simpl; intros.
  inv; auto.
- assert (O : Ok (Node ll lx lr _x)) by (inv; auto).
- assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto).
+ assert (O : Ok (Node _x ll lx lr)) by (inv; auto).
+ assert (L : lt_tree x (Node _x ll lx lr)) by (inv; auto).
  specialize IHp with (1:=O); rewrite e0 in IHp; auto; simpl in *.
  apply bal_ok; auto.
  inv; auto.
@@ -936,13 +479,13 @@ Proof.
  inv; auto.
 Qed.
 
-Lemma remove_min_gt_tree : forall l x r h `{Ok (Node l x r h)},
+Lemma remove_min_gt_tree : forall l x r h `{Ok (Node h l x r)},
  gt_tree (remove_min l x r)#2 (remove_min l x r)#1.
 Proof.
  intros l x r; functional induction (remove_min l x r); simpl; intros.
  inv; auto.
- assert (O : Ok (Node ll lx lr _x)) by (inv; auto).
- assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto).
+ assert (O : Ok (Node _x ll lx lr)) by (inv; auto).
+ assert (L : lt_tree x (Node _x ll lx lr)) by (inv; auto).
  specialize IHp with (1:=O); rewrite e0 in IHp; simpl in IHp.
  intro y; rewrite bal_spec; intuition;
   specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L;
@@ -951,14 +494,13 @@ Qed.
 Local Hint Resolve remove_min_gt_tree.
 
 
-
-(** * Merging two trees *)
+(** ** Merging two trees *)
 
 Lemma merge_spec : forall s1 s2 y,
  InT y (merge s1 s2) <-> InT y s1 \/ InT y s2.
 Proof.
  intros s1 s2; functional induction (merge s1 s2); intros;
- try factornode _x _x0 _x1 _x2 as s1.
+  try factornode s1.
  intuition_in.
  intuition_in.
  rewrite bal_spec, remove_min_spec, e1; simpl; intuition.
@@ -969,7 +511,7 @@ Instance merge_ok s1 s2 : forall `(Ok s1, Ok s2)
  Ok (merge s1 s2).
 Proof.
  functional induction (merge s1 s2); intros; auto;
- try factornode _x _x0 _x1 _x2 as s1.
+  try factornode s1.
  apply bal_ok; auto.
  change s2' with ((s2',m)#1); rewrite <-e1; eauto with *.
  intros y Hy.
@@ -980,7 +522,7 @@ Qed.
 
 
 
-(** * Deletion *)
+(** ** Deletion *)
 
 Lemma remove_spec : forall s x y `{Ok s},
  (InT y (remove x s) <-> InT y s /\ ~ X.eq y x).
@@ -988,7 +530,7 @@ Proof.
  induct s x.
  intuition_in.
  rewrite merge_spec; intuition; [order|order|intuition_in].
- elim H6; eauto.
+ elim H2; eauto.
  rewrite bal_spec, IHl; clear IHl IHr; intuition; [order|order|intuition_in].
  rewrite bal_spec, IHr; clear IHl IHr; intuition; [order|order|intuition_in].
 Qed.
@@ -1008,109 +550,13 @@ Proof.
 Qed.
 
 
-(** * Minimum element *)
-
-Lemma min_elt_spec1 : forall s x, min_elt s = Some x -> InT x s.
-Proof.
- intro s; functional induction (min_elt s); auto; inversion 1; auto.
-Qed.
-
-Lemma min_elt_spec2 : forall s x y `{Ok s},
- min_elt s = Some x -> InT y s -> ~ X.lt y x.
-Proof.
- intro s; functional induction (min_elt s);
- try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1.
- discriminate.
- intros x y0 U V W.
- inversion V; clear V; subst.
- inv; order.
- intros; inv; auto.
- assert (X.lt x y) by (apply H4; apply min_elt_spec1; auto).
- order.
- assert (X.lt x1 y) by auto.
- assert (~X.lt x1 x) by auto.
- order.
-Qed.
-
-Lemma min_elt_spec3 : forall s, min_elt s = None -> Empty s.
-Proof.
- intro s; functional induction (min_elt s).
- red; red; inversion 2.
- inversion 1.
- intro H0.
- destruct (IHo H0 _x2); auto.
-Qed.
-
-
-
-(** * Maximum element *)
-
-Lemma max_elt_spec1 : forall s x, max_elt s = Some x -> InT x s.
-Proof.
- intro s; functional induction (max_elt s); auto; inversion 1; auto.
-Qed.
-
-Lemma max_elt_spec2 : forall s x y `{Ok s},
- max_elt s = Some x -> InT y s -> ~ X.lt x y.
-Proof.
- intro s; functional induction (max_elt s);
- try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1.
- discriminate.
- intros x y0 U V W.
- inversion V; clear V; subst.
- inv; order.
- intros; inv; auto.
- assert (X.lt y x1) by auto.
- assert (~ X.lt x x1) by auto.
- order.
- assert (X.lt y x) by (apply H5; apply max_elt_spec1; auto).
- order.
-Qed.
-
-Lemma max_elt_spec3 : forall s, max_elt s = None -> Empty s.
-Proof.
- intro s; functional induction (max_elt s).
- red; auto.
- inversion 1.
- intros H0; destruct (IHo H0 _x2); auto.
-Qed.
-
-
-
-(** * Any element *)
-
-Lemma choose_spec1 : forall s x, choose s = Some x -> InT x s.
-Proof.
- exact min_elt_spec1.
-Qed.
-
-Lemma choose_spec2 : forall s, choose s = None -> Empty s.
-Proof.
- exact min_elt_spec3.
-Qed.
-
-Lemma choose_spec3 : forall s s' x x' `{Ok s, Ok s'},
-  choose s = Some x -> choose s' = Some x' ->
-  Equal s s' -> X.eq x x'.
-Proof.
- unfold choose, Equal; intros s s' x x' Hb Hb' Hx Hx' H.
- assert (~X.lt x x').
-  apply min_elt_spec2 with s'; auto.
-  rewrite <-H; auto using min_elt_spec1.
- assert (~X.lt x' x).
-  apply min_elt_spec2 with s; auto.
-  rewrite H; auto using min_elt_spec1.
- elim_compare x x'; intuition.
-Qed.
-
-
-(** * Concatenation *)
+(** ** Concatenation *)
 
 Lemma concat_spec : forall s1 s2 y,
  InT y (concat s1 s2) <-> InT y s1 \/ InT y s2.
 Proof.
  intros s1 s2; functional induction (concat s1 s2); intros;
- try factornode _x _x0 _x1 _x2 as s1.
+  try factornode s1.
  intuition_in.
  intuition_in.
  rewrite join_spec, remove_min_spec, e1; simpl; intuition.
@@ -1121,7 +567,7 @@ Instance concat_ok s1 s2 : forall `(Ok s1, Ok s2)
  Ok (concat s1 s2).
 Proof.
  functional induction (concat s1 s2); intros; auto;
- try factornode _x _x0 _x1 _x2 as s1.
+  try factornode s1.
  apply join_ok; auto.
  change (Ok (s2',m)#1); rewrite <-e1; eauto with *.
  intros y Hy.
@@ -1132,7 +578,7 @@ Qed.
 
 
 
-(** * Splitting *)
+(** ** Splitting *)
 
 Lemma split_spec1 : forall s x y `{Ok s},
  (InT y (split x s)#l <-> InT y s /\ X.lt y x).
@@ -1174,11 +620,11 @@ Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r.
 Proof.
  induct s x; simpl; auto.
  specialize (IHl x).
- generalize (fun y => @split_spec2 _ x y H1).
+ generalize (fun y => @split_spec2 l x y _).
  destruct (split x l); simpl in *; intuition. apply join_ok; auto.
  intros y; rewrite H; intuition.
  specialize (IHr x).
- generalize (fun y => @split_spec1 _ x y H2).
+ generalize (fun y => @split_spec1 r x y _).
  destruct (split x r); simpl in *; intuition. apply join_ok; auto.
  intros y; rewrite H; intuition.
 Qed.
@@ -1190,7 +636,7 @@ Instance split_ok2 s x `(Ok s) : Ok (split x s)#r.
 Proof. intros; destruct (@split_ok s x); auto. Qed.
 
 
-(** * Intersection *)
+(** ** Intersection *)
 
 Ltac destruct_split := match goal with
  | H : split ?x ?s = << ?u, ?v, ?w >> |- _ =>
@@ -1204,23 +650,24 @@ Lemma inter_spec_ok : forall s1 s2 `{Ok s1, Ok s2},
  Ok (inter s1 s2) /\ (forall y, InT y (inter s1 s2) <-> InT y s1 /\ InT y s2).
 Proof.
  intros s1 s2; functional induction inter s1 s2; intros B1 B2;
- [intuition_in|intuition_in | | ];
- factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv;
+ [intuition_in|intuition_in | | ]; factornode s2;
+ destruct_split; inv;
  destruct IHt0 as (IHo1,IHi1), IHt1 as (IHo2,IHi2); auto with *;
  split; intros.
- (* Ok join *)
- apply join_ok; auto with *; intro y; rewrite ?IHi1, ?IHi2; intuition.
- (* InT join *)
- rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in.
- setoid_replace y with x1; auto. rewrite <- split_spec3; auto.
- (* Ok concat *)
- apply concat_ok; auto with *; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
- (* InT concat *)
- rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; auto.
- intuition_in.
- absurd (InT x1 s2).
-  rewrite <- split_spec3; auto; congruence.
-  setoid_replace x1 with y; auto.
+ - (* Ok join *)
+   apply join_ok; auto with *; intro y; rewrite ?IHi1, ?IHi2; intuition.
+ - (* InT join *)
+   rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in.
+   setoid_replace y with x1; auto. rewrite <- split_spec3; auto.
+ - (* Ok concat *)
+   apply concat_ok; auto with *; intros y1 y2; rewrite IHi1, IHi2;
+   intuition; order.
+ - (* InT concat *)
+   rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; auto.
+   intuition_in.
+   absurd (InT x1 s2).
+   rewrite <- split_spec3; auto; congruence.
+   setoid_replace x1 with y; auto.
 Qed.
 
 Lemma inter_spec : forall s1 s2 y `{Ok s1, Ok s2},
@@ -1231,31 +678,31 @@ Instance inter_ok s1 s2 `(Ok s1, Ok s2) : Ok (inter s1 s2).
 Proof. intros; destruct (@inter_spec_ok s1 s2); auto. Qed.
 
 
-(** * Difference *)
+(** ** Difference *)
 
 Lemma diff_spec_ok : forall s1 s2 `{Ok s1, Ok s2},
  Ok (diff s1 s2) /\ (forall y, InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2).
 Proof.
  intros s1 s2; functional induction diff s1 s2; intros B1 B2;
- [intuition_in|intuition_in | | ];
- factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv;
+ [intuition_in|intuition_in | | ]; factornode s2;
+ destruct_split; inv;
  destruct IHt0 as (IHb1,IHi1), IHt1 as (IHb2,IHi2); auto with *;
  split; intros.
- (* Ok concat *)
- apply concat_ok; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
- (* InT concat *)
- rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in.
- absurd (InT x1 s2).
-  setoid_replace x1 with y; auto.
-  rewrite <- split_spec3; auto; congruence.
- (* Ok join *)
- apply join_ok; auto; intro y; rewrite ?IHi1, ?IHi2; intuition.
- (* InT join *)
- rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; auto with *.
- intuition_in.
- absurd (InT x1 s2); auto.
-  rewrite <- split_spec3; auto; congruence.
-  setoid_replace x1 with y; auto.
+ - (* Ok concat *)
+   apply concat_ok; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
+ - (* InT concat *)
+   rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in.
+   absurd (InT x1 s2).
+   + setoid_replace x1 with y; auto.
+   + rewrite <- split_spec3; auto; congruence.
+ - (* Ok join *)
+   apply join_ok; auto; intro y; rewrite ?IHi1, ?IHi2; intuition.
+ - (* InT join *)
+   rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; auto with *.
+   intuition_in.
+   absurd (InT x1 s2); auto.
+   * rewrite <- split_spec3; auto; congruence.
+   * setoid_replace x1 with y; auto.
 Qed.
 
 Lemma diff_spec : forall s1 s2 y `{Ok s1, Ok s2},
@@ -1266,7 +713,7 @@ Instance diff_ok s1 s2 `(Ok s1, Ok s2) : Ok (diff s1 s2).
 Proof. intros; destruct (@diff_spec_ok s1 s2); auto. Qed.
 
 
-(** * Union *)
+(** ** Union *)
 
 Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2},
  (InT y (union s1 s2) <-> InT y s1 \/ InT y s2).
@@ -1274,548 +721,90 @@ Proof.
  intros s1 s2; functional induction union s1 s2; intros y B1 B2.
  intuition_in.
  intuition_in.
- factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
+ factornode s2; destruct_split; inv.
  rewrite join_spec, IHt0, IHt1, split_spec1, split_spec2; auto with *.
- elim_compare y x1; intuition_in.
+ destruct (X.compare_spec y x1); intuition_in.
 Qed.
 
 Instance union_ok s1 s2 : forall `(Ok s1, Ok s2), Ok (union s1 s2).
 Proof.
  functional induction union s1 s2; intros B1 B2; auto.
- factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
+ factornode s2; destruct_split; inv.
  apply join_ok; auto with *.
  intro y; rewrite union_spec, split_spec1; intuition_in.
  intro y; rewrite union_spec, split_spec2; intuition_in.
 Qed.
 
-
-(** * Elements *)
-
-Lemma elements_spec1' : forall s acc x,
- InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc.
-Proof.
- induction s as [ | l Hl x r Hr h ]; simpl; auto.
- intuition.
- inversion H0.
- intros.
- rewrite Hl.
- destruct (Hr acc x0); clear Hl Hr.
- intuition; inversion_clear H3; intuition.
-Qed.
-
-Lemma elements_spec1 : forall s x, InA X.eq x (elements s) <-> InT x s.
-Proof.
- intros; generalize (elements_spec1' s nil x); intuition.
- inversion_clear H0.
-Qed.
-
-Lemma elements_spec2' : forall s acc `{Ok s}, sort X.lt acc ->
- (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) ->
- sort X.lt (elements_aux acc s).
-Proof.
- induction s as [ | l Hl y r Hr h]; simpl; intuition.
- inv.
- apply Hl; auto.
- constructor.
- apply Hr; auto.
- eapply InA_InfA; eauto with *.
- intros.
- destruct (elements_spec1' r acc y0); intuition.
- intros.
- inversion_clear H.
- order.
- destruct (elements_spec1' r acc x); intuition eauto.
-Qed.
-
-Lemma elements_spec2 : forall s `(Ok s), sort X.lt (elements s).
-Proof.
- intros; unfold elements; apply elements_spec2'; auto.
- intros; inversion H0.
-Qed.
-Local Hint Resolve elements_spec2.
-
-Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s).
-Proof.
- intros. eapply SortA_NoDupA; eauto with *.
-Qed.
-
-Lemma elements_aux_cardinal :
- forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s).
-Proof.
- simple induction s; simpl in |- *; intuition.
- rewrite <- H.
- simpl in |- *.
- rewrite <- H0; omega.
-Qed.
-
-Lemma elements_cardinal : forall s : tree, cardinal s = length (elements s).
-Proof.
- exact (fun s => elements_aux_cardinal s nil).
-Qed.
-
-Definition cardinal_spec (s:t)(Hs:Ok s) := elements_cardinal s.
-
-Lemma elements_app :
- forall s acc, elements_aux acc s = elements s ++ acc.
-Proof.
- induction s; simpl; intros; auto.
- rewrite IHs1, IHs2.
- unfold elements; simpl.
- rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto.
-Qed.
-
-Lemma elements_node :
- forall l x r h acc,
- elements l ++ x :: elements r ++ acc =
- elements (Node l x r h) ++ acc.
-Proof.
- unfold elements; simpl; intros; auto.
- rewrite !elements_app, <- !app_nil_end, !app_ass; auto.
-Qed.
-
-
 (** * Filter *)
 
-Lemma filter_spec' : forall s x acc f,
- Proper (X.eq==>eq) f ->
- (InT x (filter_acc f acc s) <-> InT x acc \/ InT x s /\ f x = true).
-Proof.
- induction s; simpl; intros.
- intuition_in.
- rewrite IHs2, IHs1 by (destruct (f t0); auto).
- case_eq (f t0); intros.
- rewrite add_spec'; auto.
- intuition_in.
- rewrite (H _ _ H2).
- intuition.
- intuition_in.
- rewrite (H _ _ H2) in H3.
- rewrite H0 in H3; discriminate.
-Qed.
-
-Instance filter_ok' : forall s acc f `(Ok s, Ok acc),
- Ok (filter_acc f acc s).
+Lemma filter_spec : forall s x f,
+ Proper (X.eq==>Logic.eq) f ->
+ (InT x (filter f s) <-> InT x s /\ f x = true).
 Proof.
- induction s; simpl; auto.
- intros. inv.
- destruct (f t0); auto with *.
+ induction s as [ |h l Hl x0 r Hr]; intros x f Hf; simpl.
+ - intuition_in.
+ - case_eq (f x0); intros Hx0.
+   * rewrite join_spec, Hl, Hr; intuition_in.
+     now setoid_replace x with x0.
+   * rewrite concat_spec, Hl, Hr; intuition_in.
+     assert (f x = f x0) by auto. congruence.
 Qed.
 
-Lemma filter_spec : forall s x f,
- Proper (X.eq==>eq) f ->
- (InT x (filter f s) <-> InT x s /\ f x = true).
+Lemma filter_weak_spec : forall s x f,
+ InT x (filter f s) -> InT x s.
 Proof.
- unfold filter; intros; rewrite filter_spec'; intuition_in.
+ induction s as [ |h l Hl x0 r Hr]; intros x f; simpl.
+ - trivial.
+ - destruct (f x0).
+   * rewrite join_spec; intuition_in; eauto.
+   * rewrite concat_spec; intuition_in; eauto.
 Qed.
 
-Instance filter_ok s f `(Ok s) : Ok (filter f s).
+Instance filter_ok s f `(H : Ok s) : Ok (filter f s).
 Proof.
- unfold filter; intros; apply filter_ok'; auto.
+ induction H as [ | h x l r Hl Hfl Hr Hfr Hlt Hgt ].
+ - constructor.
+ - simpl.
+   assert (lt_tree x (filter f l)) by (eauto using filter_weak_spec).
+   assert (gt_tree x (filter f r)) by (eauto using filter_weak_spec).
+   destruct (f x); eauto using concat_ok, join_ok.
 Qed.
 
 
 (** * Partition *)
 
-Lemma partition_spec1' : forall s acc f,
- Proper (X.eq==>eq) f -> forall x : elt,
- InT x (partition_acc f acc s)#1 <->
- InT x acc#1 \/ InT x s /\ f x = true.
+Lemma partition_spec1' s f : (partition f s)#1 = filter f s.
 Proof.
- induction s; simpl; intros.
- intuition_in.
- destruct acc as [acct accf]; simpl in *.
- rewrite IHs2 by
-  (destruct (f t0); auto; apply partition_acc_avl_1; simpl; auto).
- rewrite IHs1 by (destruct (f t0); simpl; auto).
- case_eq (f t0); simpl; intros.
- rewrite add_spec'; auto.
- intuition_in.
- rewrite (H _ _ H2).
- intuition.
- intuition_in.
- rewrite (H _ _ H2) in H3.
- rewrite H0 in H3; discriminate.
+ induction s as [ | h l Hl x r Hr ]; simpl.
+ - trivial.
+ - rewrite <- Hl, <- Hr.
+   now destruct (partition f l), (partition f r), (f x).
 Qed.
 
-Lemma partition_spec2' : forall s acc f,
- Proper (X.eq==>eq) f -> forall x : elt,
- InT x (partition_acc f acc s)#2 <->
- InT x acc#2 \/ InT x s /\ f x = false.
+Lemma partition_spec2' s f :
+ (partition f s)#2 = filter (fun x => negb (f x)) s.
 Proof.
- induction s; simpl; intros.
- intuition_in.
- destruct acc as [acct accf]; simpl in *.
- rewrite IHs2 by
-  (destruct (f t0); auto; apply partition_acc_avl_2; simpl; auto).
- rewrite IHs1 by (destruct (f t0); simpl; auto).
- case_eq (f t0); simpl; intros.
- intuition.
- intuition_in.
- rewrite (H _ _ H2) in H3.
- rewrite H0 in H3; discriminate.
- rewrite add_spec'; auto.
- intuition_in.
- rewrite (H _ _ H2).
- intuition.
+ induction s as [ | h l Hl x r Hr ]; simpl.
+ - trivial.
+ - rewrite <- Hl, <- Hr.
+   now destruct (partition f l), (partition f r), (f x).
 Qed.
 
-Lemma partition_spec1 : forall s f,
- Proper (X.eq==>eq) f ->
+Lemma partition_spec1 s f :
+ Proper (X.eq==>Logic.eq) f ->
  Equal (partition f s)#1 (filter f s).
-Proof.
- unfold partition; intros s f P x.
- rewrite partition_spec1', filter_spec; simpl; intuition_in.
-Qed.
+Proof. now rewrite partition_spec1'. Qed.
 
-Lemma partition_spec2 : forall s f,
- Proper (X.eq==>eq) f ->
+Lemma partition_spec2 s f :
+ Proper (X.eq==>Logic.eq) f ->
  Equal (partition f s)#2 (filter (fun x => negb (f x)) s).
-Proof.
- unfold partition; intros s f P x.
- rewrite partition_spec2', filter_spec; simpl; intuition_in.
- rewrite H1; auto.
- right; split; auto.
- rewrite negb_true_iff in H1; auto.
- intros u v H; rewrite H; auto.
-Qed.
-
-Instance partition_ok1' : forall s acc f `(Ok s, Ok acc#1),
- Ok (partition_acc f acc s)#1.
-Proof.
- induction s; simpl; auto.
- destruct acc as [acct accf]; simpl in *.
- intros. inv.
- destruct (f t0); auto.
- apply IHs2; simpl; auto.
- apply IHs1; simpl; auto with *.
-Qed.
-
-Instance partition_ok2' : forall s acc f `(Ok s, Ok acc#2),
- Ok (partition_acc f acc s)#2.
-Proof.
- induction s; simpl; auto.
- destruct acc as [acct accf]; simpl in *.
- intros. inv.
- destruct (f t0); auto.
- apply IHs2; simpl; auto.
- apply IHs1; simpl; auto with *.
-Qed.
+Proof. now rewrite partition_spec2'. Qed.
 
 Instance partition_ok1 s f `(Ok s) : Ok (partition f s)#1.
-Proof. apply partition_ok1'; auto. Qed.
+Proof. rewrite partition_spec1'; now apply filter_ok. Qed.
 
 Instance partition_ok2 s f `(Ok s) : Ok (partition f s)#2.
-Proof. apply partition_ok2'; auto. Qed.
-
-
-
-(** * [for_all] and [exists] *)
-
-Lemma for_all_spec : forall s f, Proper (X.eq==>eq) f ->
- (for_all f s = true <-> For_all (fun x => f x = true) s).
-Proof.
- split.
- induction s; simpl; auto; intros; red; intros; inv.
- destruct (andb_prop _ _ H0); auto.
- destruct (andb_prop _ _ H1); eauto.
- apply IHs1; auto.
- destruct (andb_prop _ _ H0); auto.
- destruct (andb_prop _ _ H1); auto.
- apply IHs2; auto.
- destruct (andb_prop _ _ H0); auto.
- (* <- *)
- induction s; simpl; auto.
- intros. red in H0.
- rewrite IHs1; try red; auto.
- rewrite IHs2; try red; auto.
- generalize (H0 t0).
- destruct (f t0); simpl; auto.
-Qed.
-
-Lemma exists_spec : forall s f, Proper (X.eq==>eq) f ->
- (exists_ f s = true <-> Exists (fun x => f x = true) s).
-Proof.
- split.
- induction s; simpl; intros; rewrite <- ?orb_lazy_alt in *.
- discriminate.
- destruct (orb_true_elim _ _ H0) as [H1|H1].
- destruct (orb_true_elim _ _ H1) as [H2|H2].
- exists t0; auto.
- destruct (IHs1 H2); auto; exists x; intuition.
- destruct (IHs2 H1); auto; exists x; intuition.
- (* <- *)
- induction s; simpl; destruct 1 as (x,(U,V)); inv; rewrite <- ?orb_lazy_alt.
- rewrite (H _ _ (MX.eq_sym H0)); rewrite V; auto.
- apply orb_true_intro; left.
- apply orb_true_intro; right; apply IHs1; auto; exists x; auto.
- apply orb_true_intro; right; apply IHs2; auto; exists x; auto.
-Qed.
-
-
-(** * Fold *)
-
-Lemma fold_spec' :
- forall (A : Type) (f : elt -> A -> A) (s : tree) (i : A) (acc : list elt),
- fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i).
-Proof.
- induction s as [|l IHl x r IHr h]; simpl; intros; auto.
- rewrite IHl.
- simpl. unfold flip at 2.
- apply IHr.
-Qed.
-
-Lemma fold_spec :
- forall (s:t) (A : Type) (i : A) (f : elt -> A -> A),
- fold f s i = fold_left (flip f) (elements s) i.
-Proof.
- unfold elements.
- induction s as [|l IHl x r IHr h]; simpl; intros; auto.
- rewrite fold_spec'.
- rewrite IHr.
- simpl; auto.
-Qed.
-
-
-(** * Subset *)
-
-Lemma subsetl_spec : forall subset_l1 l1 x1 h1 s2
- `{Ok (Node l1 x1 Leaf h1), Ok s2},
- (forall s `{Ok s}, (subset_l1 s = true <-> Subset l1 s)) ->
- (subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ).
-Proof.
- induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
- unfold Subset; intuition; try discriminate.
- assert (H': InT x1 Leaf) by auto; inversion H'.
- specialize (IHl2 H).
- specialize (IHr2 H).
- inv.
- elim_compare x1 x2.
-
- rewrite H1 by auto; clear H1 IHl2 IHr2.
- unfold Subset. intuition_in.
- assert (X.eq a x2) by order; intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-
- rewrite IHl2 by auto; clear H1 IHl2 IHr2.
- unfold Subset. intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-
- rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
- unfold Subset. intuition_in.
- constructor 3. setoid_replace a with x1; auto. rewrite <- mem_spec; auto.
- rewrite mem_spec; auto.
- assert (InT x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-Qed.
-
-
-Lemma subsetr_spec : forall subset_r1 r1 x1 h1 s2,
- bst (Node Leaf x1 r1 h1) -> bst s2 ->
- (forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) ->
- (subsetr subset_r1 x1 s2 = true <-> Subset (Node Leaf x1 r1 h1) s2).
-Proof.
- induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros.
- unfold Subset; intuition; try discriminate.
- assert (H': InT x1 Leaf) by auto; inversion H'.
- specialize (IHl2 H).
- specialize (IHr2 H).
- inv.
- elim_compare x1 x2.
-
- rewrite H1 by auto; clear H1 IHl2 IHr2.
- unfold Subset. intuition_in.
- assert (X.eq a x2) by order; intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-
- rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto;  clear H1 IHl2 IHr2.
- unfold Subset. intuition_in.
- constructor 2. setoid_replace a with x1; auto. rewrite <- mem_spec; auto.
- rewrite mem_spec; auto.
- assert (InT x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-
- rewrite IHr2 by auto; clear H1 IHl2 IHr2.
- unfold Subset. intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-Qed.
-
-Lemma subset_spec : forall s1 s2 `{Ok s1, Ok s2},
- (subset s1 s2 = true <-> Subset s1 s2).
-Proof.
- induction s1 as [|l1 IHl1 x1 r1 IHr1 h1]; simpl; intros.
- unfold Subset; intuition_in.
- destruct s2 as [|l2 x2 r2 h2]; simpl; intros.
- unfold Subset; intuition_in; try discriminate.
- assert (H': InT x1 Leaf) by auto; inversion H'.
- inv.
- elim_compare x1 x2.
-
- rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto.
- clear IHl1 IHr1.
- unfold Subset; intuition_in.
- assert (X.eq a x2) by order; intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-
- rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto.
- rewrite (@subsetl_spec (subset l1) l1 x1 h1) by auto.
- clear IHl1 IHr1.
- unfold Subset; intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-
- rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto.
- rewrite (@subsetr_spec (subset r1) r1 x1 h1) by auto.
- clear IHl1 IHr1.
- unfold Subset; intuition_in.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
- assert (InT a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
-Qed.
-
-
-(** * Comparison *)
-
-(** ** Relations [eq] and [lt] over trees *)
-
-Module L := MakeListOrdering X.
-
-Definition eq := Equal.
-Instance eq_equiv : Equivalence eq.
-Proof. firstorder. Qed.
-
-Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
-Proof.
- unfold eq, Equal, L.eq; intros.
- setoid_rewrite elements_spec1; firstorder.
-Qed.
-
-Definition lt (s1 s2 : t) : Prop :=
- exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
-   /\ L.lt (elements s1') (elements s2').
-
-Instance lt_strorder : StrictOrder lt.
-Proof.
- split.
- intros s (s1 & s2 & B1 & B2 & E1 & E2 & L).
- assert (eqlistA X.eq (elements s1) (elements s2)).
-  apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
-  rewrite <- eq_Leq. transitivity s; auto. symmetry; auto.
- rewrite H in L.
- apply (StrictOrder_Irreflexive (elements s2)); auto.
- intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
-                 (s2'' & s3' & B2' & B3 & E2' & E3 & L23).
- exists s1', s3'; do 4 (split; trivial).
- assert (eqlistA X.eq (elements s2') (elements s2'')).
-  apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
-  rewrite <- eq_Leq. transitivity s2; auto. symmetry; auto.
- transitivity (elements s2'); auto.
- rewrite H; auto.
-Qed.
-
-Instance lt_compat : Proper (eq==>eq==>iff) lt.
-Proof.
- intros s1 s2 E12 s3 s4 E34. split.
- intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
- exists s1', s3'; do 2 (split; trivial).
-  split. transitivity s1; auto. symmetry; auto.
-  split; auto. transitivity s3; auto. symmetry; auto.
- intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
- exists s1', s3'; do 2 (split; trivial).
-  split. transitivity s2; auto.
-  split; auto. transitivity s4; auto.
-Qed.
-
-
-(** * Proof of the comparison algorithm *)
-
-(** [flatten_e e] returns the list of elements of [e] i.e. the list
-    of elements actually compared *)
-
-Fixpoint flatten_e (e : enumeration) : list elt := match e with
-  | End => nil
-  | More x t r => x :: elements t ++ flatten_e r
- end.
-
-Lemma flatten_e_elements :
- forall l x r h e,
- elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ flatten_e e.
-Proof.
- intros; simpl; apply elements_node.
-Qed.
-
-Lemma cons_1 : forall s e,
-  flatten_e (cons s e) = elements s ++ flatten_e e.
-Proof.
- induction s; simpl; auto; intros.
- rewrite IHs1; apply flatten_e_elements.
-Qed.
-
-(** Correctness of this comparison *)
-
-Definition Cmp c x y := CompSpec L.eq L.lt x y c.
-
-Local Hint Unfold Cmp flip.
-
-Lemma compare_end_Cmp :
- forall e2, Cmp (compare_end e2) nil (flatten_e e2).
-Proof.
- destruct e2; simpl; constructor; auto. reflexivity.
-Qed.
-
-Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
-  Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
-   Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
-      (flatten_e (More x2 r2 e2)).
-Proof.
- simpl; intros; elim_compare x1 x2; simpl; red; auto.
-Qed.
-
-Lemma compare_cont_Cmp : forall s1 cont e2 l,
- (forall e, Cmp (cont e) l (flatten_e e)) ->
- Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
-Proof.
- induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto.
- rewrite <- elements_node; simpl.
- apply Hl1; auto. clear e2. intros [|x2 r2 e2].
- simpl; auto.
- apply compare_more_Cmp.
- rewrite <- cons_1; auto.
-Qed.
-
-Lemma compare_Cmp : forall s1 s2,
- Cmp (compare s1 s2) (elements s1) (elements s2).
-Proof.
- intros; unfold compare.
- rewrite (app_nil_end (elements s1)).
- replace (elements s2) with (flatten_e (cons s2 End)) by
-  (rewrite cons_1; simpl; rewrite <- app_nil_end; auto).
- apply compare_cont_Cmp; auto.
- intros.
- apply compare_end_Cmp; auto.
-Qed.
-
-Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
- CompSpec eq lt s1 s2 (compare s1 s2).
-Proof.
- intros.
- destruct (compare_Cmp s1 s2); constructor.
- rewrite eq_Leq; auto.
- intros; exists s1, s2; repeat split; auto.
- intros; exists s2, s1; repeat split; auto.
-Qed.
-
-
-(** * Equality test *)
-
-Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2},
- equal s1 s2 = true <-> eq s1 s2.
-Proof.
-unfold equal; intros s1 s2 B1 B2.
-destruct (@compare_spec s1 s2 B1 B2) as [H|H|H];
- split; intros H'; auto; try discriminate.
-rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
-rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
-Qed.
+Proof. rewrite partition_spec2'; now apply filter_ok. Qed.
 
 End MakeRaw.
 
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
new file mode 100644
index 00000000..704ff31b
--- /dev/null
+++ b/theories/MSets/MSetGenTree.v
@@ -0,0 +1,1145 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * MSetGenTree : sets via generic trees
+
+    This module factorizes common parts in implementations
+    of finite sets as AVL trees and as Red-Black trees. The nodes
+    of the trees defined here include an generic information
+    parameter, that will be the heigth in AVL trees and the color
+    in Red-Black trees. Without more details here about these
+    information parameters, trees here are not known to be
+    well-balanced, but simply binary-search-trees.
+
+    The operations we could define and prove correct here are the
+    one that do not build non-empty trees, but only analyze them :
+
+     - empty is_empty
+     - mem
+     - compare equal subset
+     - fold cardinal elements
+     - for_all exists_
+     - min_elt max_elt choose
+*)
+
+Require Import Orders OrdersFacts MSetInterface NPeano.
+Local Open Scope list_scope.
+Local Open Scope lazy_bool_scope.
+
+(* For nicer extraction, we create induction principles
+   only when needed *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
+Module Type InfoTyp.
+ Parameter t : Set.
+End InfoTyp.
+
+(** * Ops : the pure functions *)
+
+Module Type Ops (X:OrderedType)(Info:InfoTyp).
+
+Definition elt := X.t.
+Hint Transparent elt.
+
+Inductive tree  : Type :=
+| Leaf : tree
+| Node : Info.t -> tree -> X.t -> tree -> tree.
+
+(** ** The empty set and emptyness test *)
+
+Definition empty := Leaf.
+
+Definition is_empty t :=
+ match t with
+ | Leaf => true
+ | _ => false
+ end.
+
+(** ** Membership test *)
+
+(** The [mem] function is deciding membership. It exploits the
+    binary search tree invariant to achieve logarithmic complexity. *)
+
+Fixpoint mem x t :=
+ match t with
+ | Leaf => false
+ | Node _ l k r =>
+   match X.compare x k with
+     | Lt => mem x l
+     | Eq => true
+     | Gt => mem x r
+   end
+ end.
+
+(** ** Minimal, maximal, arbitrary elements *)
+
+Fixpoint min_elt (t : tree) : option elt :=
+ match t with
+ | Leaf => None
+ | Node _ Leaf x r => Some x
+ | Node _ l x r => min_elt l
+ end.
+
+Fixpoint max_elt (t : tree) : option elt :=
+  match t with
+  | Leaf => None
+  | Node _ l x Leaf => Some x
+  | Node _ l x r => max_elt r
+  end.
+
+Definition choose := min_elt.
+
+(** ** Iteration on elements *)
+
+Fixpoint fold {A: Type} (f: elt -> A -> A) (t: tree) (base: A) : A :=
+  match t with
+  | Leaf => base
+  | Node _ l x r => fold f r (f x (fold f l base))
+ end.
+
+Fixpoint elements_aux acc s :=
+  match s with
+   | Leaf => acc
+   | Node _ l x r => elements_aux (x :: elements_aux acc r) l
+  end.
+
+Definition elements := elements_aux nil.
+
+Fixpoint rev_elements_aux acc s :=
+  match s with
+   | Leaf => acc
+   | Node _ l x r => rev_elements_aux (x :: rev_elements_aux acc l) r
+  end.
+
+Definition rev_elements := rev_elements_aux nil.
+
+Fixpoint cardinal (s : tree) : nat :=
+  match s with
+   | Leaf => 0
+   | Node _ l _ r => S (cardinal l + cardinal r)
+  end.
+
+Fixpoint maxdepth s :=
+ match s with
+ | Leaf => 0
+ | Node _ l _ r => S (max (maxdepth l) (maxdepth r))
+ end.
+
+Fixpoint mindepth s :=
+ match s with
+ | Leaf => 0
+ | Node _ l _ r => S (min (mindepth l) (mindepth r))
+ end.
+
+(** ** Testing universal or existential properties. *)
+
+(** We do not use the standard boolean operators of Coq,
+    but lazy ones. *)
+
+Fixpoint for_all (f:elt->bool) s := match s with
+  | Leaf => true
+  | Node _ l x r => f x &&& for_all f l &&& for_all f r
+end.
+
+Fixpoint exists_ (f:elt->bool) s := match s with
+  | Leaf => false
+  | Node _ l x r => f x ||| exists_ f l ||| exists_ f r
+end.
+
+(** ** Comparison of trees *)
+
+(** The algorithm here has been suggested by Xavier Leroy,
+    and transformed into c.p.s. by Benjamin Grégoire.
+    The original ocaml code (with non-structural recursive calls)
+    has also been formalized (thanks to Function+measure), see
+    [ocaml_compare] in [MSetFullAVL]. The following code with
+    continuations computes dramatically faster in Coq, and
+    should be almost as efficient after extraction.
+*)
+
+(** Enumeration of the elements of a tree. This corresponds
+    to the "samefringe" notion in the litterature. *)
+
+Inductive enumeration :=
+ | End : enumeration
+ | More : elt -> tree -> enumeration -> enumeration.
+
+
+(** [cons t e] adds the elements of tree [t] on the head of
+    enumeration [e]. *)
+
+Fixpoint cons s e : enumeration :=
+ match s with
+  | Leaf => e
+  | Node _ l x r => cons l (More x r e)
+ end.
+
+(** One step of comparison of elements *)
+
+Definition compare_more x1 (cont:enumeration->comparison) e2 :=
+ match e2 with
+ | End => Gt
+ | More x2 r2 e2 =>
+     match X.compare x1 x2 with
+      | Eq => cont (cons r2 e2)
+      | Lt => Lt
+      | Gt => Gt
+     end
+ end.
+
+(** Comparison of left tree, middle element, then right tree *)
+
+Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
+ match s1 with
+  | Leaf => cont e2
+  | Node _ l1 x1 r1 =>
+     compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
+  end.
+
+(** Initial continuation *)
+
+Definition compare_end e2 :=
+ match e2 with End => Eq | _ => Lt end.
+
+(** The complete comparison *)
+
+Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End).
+
+Definition equal s1 s2 :=
+ match compare s1 s2 with Eq => true | _ => false end.
+
+(** ** Subset test *)
+
+(** In ocaml, recursive calls are made on "half-trees" such as
+   (Node _ l1 x1 Leaf) and (Node _ Leaf x1 r1). Instead of these
+   non-structural calls, we propose here two specialized functions
+   for these situations. This version should be almost as efficient
+   as the one of ocaml (closures as arguments may slow things a bit),
+   it is simply less compact. The exact ocaml version has also been
+   formalized (thanks to Function+measure), see [ocaml_subset] in
+   [MSetFullAVL].
+*)
+
+Fixpoint subsetl (subset_l1 : tree -> bool) x1 s2 : bool :=
+ match s2 with
+  | Leaf => false
+  | Node _ l2 x2 r2 =>
+     match X.compare x1 x2 with
+      | Eq => subset_l1 l2
+      | Lt => subsetl subset_l1 x1 l2
+      | Gt => mem x1 r2 &&& subset_l1 s2
+     end
+ end.
+
+Fixpoint subsetr (subset_r1 : tree -> bool) x1 s2 : bool :=
+ match s2 with
+  | Leaf => false
+  | Node _ l2 x2 r2 =>
+     match X.compare x1 x2 with
+      | Eq => subset_r1 r2
+      | Lt => mem x1 l2 &&& subset_r1 s2
+      | Gt => subsetr subset_r1 x1 r2
+     end
+ end.
+
+Fixpoint subset s1 s2 : bool := match s1, s2 with
+  | Leaf, _ => true
+  | Node _ _ _ _, Leaf => false
+  | Node _ l1 x1 r1, Node _ l2 x2 r2 =>
+     match X.compare x1 x2 with
+      | Eq => subset l1 l2 &&& subset r1 r2
+      | Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2
+      | Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2
+     end
+ end.
+
+End Ops.
+
+(** * Props : correctness proofs of these generic operations *)
+
+Module Type Props (X:OrderedType)(Info:InfoTyp)(Import M:Ops X Info).
+
+(** ** Occurrence in a tree *)
+
+Inductive InT (x : elt) : tree -> Prop :=
+  | IsRoot : forall c l r y, X.eq x y -> InT x (Node c l y r)
+  | InLeft : forall c l r y, InT x l -> InT x (Node c l y r)
+  | InRight : forall c l r y, InT x r -> InT x (Node c l y r).
+
+Definition In := InT.
+
+(** ** Some shortcuts *)
+
+Definition Equal s s' := forall a : elt, InT a s <-> InT a s'.
+Definition Subset s s' := forall a : elt, InT a s -> InT a s'.
+Definition Empty s := forall a : elt, ~ InT a s.
+Definition For_all (P : elt -> Prop) s := forall x, InT x s -> P x.
+Definition Exists (P : elt -> Prop) s := exists x, InT x s /\ P x.
+
+(** ** Binary search trees *)
+
+(** [lt_tree x s]: all elements in [s] are smaller than [x]
+   (resp. greater for [gt_tree]) *)
+
+Definition lt_tree x s := forall y, InT y s -> X.lt y x.
+Definition gt_tree x s := forall y, InT y s -> X.lt x y.
+
+(** [bst t] : [t] is a binary search tree *)
+
+Inductive bst : tree -> Prop :=
+  | BSLeaf : bst Leaf
+  | BSNode : forall c x l r, bst l -> bst r ->
+     lt_tree x l -> gt_tree x r -> bst (Node c l x r).
+
+(** [bst] is the (decidable) invariant our trees will have to satisfy. *)
+
+Definition IsOk := bst.
+
+Class Ok (s:tree) : Prop := ok : bst s.
+
+Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }.
+
+Fixpoint ltb_tree x s :=
+ match s with
+  | Leaf => true
+  | Node _ l y r =>
+     match X.compare x y with
+      | Gt => ltb_tree x l && ltb_tree x r
+      | _ => false
+     end
+ end.
+
+Fixpoint gtb_tree x s :=
+ match s with
+  | Leaf => true
+  | Node _ l y r =>
+     match X.compare x y with
+      | Lt => gtb_tree x l && gtb_tree x r
+      | _ => false
+     end
+ end.
+
+Fixpoint isok s :=
+ match s with
+  | Leaf => true
+  | Node _  l x r => isok l && isok r && ltb_tree x l && gtb_tree x r
+ end.
+
+
+(** ** Known facts about ordered types *)
+
+Module Import MX := OrderedTypeFacts X.
+
+(** ** Automation and dedicated tactics *)
+
+Scheme tree_ind := Induction for tree Sort Prop.
+Scheme bst_ind := Induction for bst Sort Prop.
+
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Immediate MX.eq_sym.
+Local Hint Unfold In lt_tree gt_tree.
+Local Hint Constructors InT bst.
+Local Hint Unfold Ok.
+
+(** Automatic treatment of [Ok] hypothesis *)
+
+Ltac clear_inversion H := inversion H; clear H; subst.
+
+Ltac inv_ok := match goal with
+ | H:Ok (Node _ _ _ _) |- _ => clear_inversion H; inv_ok
+ | H:Ok Leaf |- _ => clear H; inv_ok
+ | H:bst ?x |- _ => change (Ok x) in H; inv_ok
+ | _ => idtac
+end.
+
+(** A tactic to repeat [inversion_clear] on all hyps of the
+    form [(f (Node _ _ _ _))] *)
+
+Ltac is_tree_constr c :=
+  match c with
+   | Leaf => idtac
+   | Node _ _ _ _ => idtac
+   | _ => fail
+  end.
+
+Ltac invtree f :=
+  match goal with
+     | H:f ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
+     | H:f _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
+     | H:f _ _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
+     | _ => idtac
+  end.
+
+Ltac inv := inv_ok; invtree InT.
+
+Ltac intuition_in := repeat progress (intuition; inv).
+
+(** Helper tactic concerning order of elements. *)
+
+Ltac order := match goal with
+ | U: lt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
+ | U: gt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
+ | _ => MX.order
+end.
+
+
+(** [isok] is indeed a decision procedure for [Ok] *)
+
+Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true.
+Proof.
+ induction s as [|c l IHl y r IHr]; simpl.
+ unfold lt_tree; intuition_in.
+ elim_compare x y.
+ split; intros; try discriminate. assert (X.lt y x) by auto. order.
+ split; intros; try discriminate. assert (X.lt y x) by auto. order.
+ rewrite !andb_true_iff, <-IHl, <-IHr.
+  unfold lt_tree; intuition_in; order.
+Qed.
+
+Lemma gtb_tree_iff : forall x s, gt_tree x s <-> gtb_tree x s = true.
+Proof.
+ induction s as [|c l IHl y r IHr]; simpl.
+ unfold gt_tree; intuition_in.
+ elim_compare x y.
+ split; intros; try discriminate. assert (X.lt x y) by auto. order.
+ rewrite !andb_true_iff, <-IHl, <-IHr.
+  unfold gt_tree; intuition_in; order.
+ split; intros; try discriminate. assert (X.lt x y) by auto. order.
+Qed.
+
+Lemma isok_iff : forall s, Ok s <-> isok s = true.
+Proof.
+ induction s as [|c l IHl y r IHr]; simpl.
+ intuition_in.
+ rewrite !andb_true_iff, <- IHl, <-IHr, <- ltb_tree_iff, <- gtb_tree_iff.
+ intuition_in.
+Qed.
+
+Instance isok_Ok s : isok s = true -> Ok s | 10.
+Proof. intros; apply <- isok_iff; auto. Qed.
+
+(** ** Basic results about [In] *)
+
+Lemma In_1 :
+ forall s x y, X.eq x y -> InT x s -> InT y s.
+Proof.
+ induction s; simpl; intuition_in; eauto.
+Qed.
+Local Hint Immediate In_1.
+
+Instance In_compat : Proper (X.eq==>eq==>iff) InT.
+Proof.
+apply proper_sym_impl_iff_2; auto with *.
+repeat red; intros; subst. apply In_1 with x; auto.
+Qed.
+
+Lemma In_node_iff :
+ forall c l x r y,
+  InT y (Node c l x r) <-> InT y l \/ X.eq y x \/ InT y r.
+Proof.
+ intuition_in.
+Qed.
+
+Lemma In_leaf_iff : forall x, InT x Leaf <-> False.
+Proof.
+ intuition_in.
+Qed.
+
+(** Results about [lt_tree] and [gt_tree] *)
+
+Lemma lt_leaf : forall x : elt, lt_tree x Leaf.
+Proof.
+ red; inversion 1.
+Qed.
+
+Lemma gt_leaf : forall x : elt, gt_tree x Leaf.
+Proof.
+ red; inversion 1.
+Qed.
+
+Lemma lt_tree_node :
+ forall (x y : elt) (l r : tree) (i : Info.t),
+ lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r).
+Proof.
+ unfold lt_tree; intuition_in; order.
+Qed.
+
+Lemma gt_tree_node :
+ forall (x y : elt) (l r : tree) (i : Info.t),
+ gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node i l y r).
+Proof.
+ unfold gt_tree; intuition_in; order.
+Qed.
+
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+
+Lemma lt_tree_not_in :
+ forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t.
+Proof.
+ intros; intro; order.
+Qed.
+
+Lemma lt_tree_trans :
+ forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t.
+Proof.
+ eauto.
+Qed.
+
+Lemma gt_tree_not_in :
+ forall (x : elt) (t : tree), gt_tree x t -> ~ InT x t.
+Proof.
+ intros; intro; order.
+Qed.
+
+Lemma gt_tree_trans :
+ forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t.
+Proof.
+ eauto.
+Qed.
+
+Instance lt_tree_compat : Proper (X.eq ==> Logic.eq ==> iff) lt_tree.
+Proof.
+ apply proper_sym_impl_iff_2; auto.
+ intros x x' Hx s s' Hs H y Hy. subst. setoid_rewrite <- Hx; auto.
+Qed.
+
+Instance gt_tree_compat : Proper (X.eq ==> Logic.eq ==> iff) gt_tree.
+Proof.
+ apply proper_sym_impl_iff_2; auto.
+ intros x x' Hx s s' Hs H y Hy. subst. setoid_rewrite <- Hx; auto.
+Qed.
+
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+
+Ltac induct s x :=
+ induction s as [|i l IHl x' r IHr]; simpl; intros;
+ [|elim_compare x x'; intros; inv].
+
+Ltac auto_tc := auto with typeclass_instances.
+
+Ltac ok :=
+ inv; change bst with Ok in *;
+ match goal with
+   | |- Ok (Node _ _ _ _) => constructor; auto_tc; ok
+   | |- lt_tree _ (Node _ _ _ _) => apply lt_tree_node; ok
+   | |- gt_tree _ (Node _ _ _ _) => apply gt_tree_node; ok
+   | _ => eauto with typeclass_instances
+ end.
+
+(** ** Empty set *)
+
+Lemma empty_spec : Empty empty.
+Proof.
+ intros x H. inversion H.
+Qed.
+
+Instance empty_ok : Ok empty.
+Proof.
+ auto.
+Qed.
+
+(** ** Emptyness test *)
+
+Lemma is_empty_spec : forall s, is_empty s = true <-> Empty s.
+Proof.
+ destruct s as [|c r x l]; simpl; auto.
+ - split; auto. intros _ x H. inv.
+ - split; auto. try discriminate. intro H; elim (H x); auto.
+Qed.
+
+(** ** Membership *)
+
+Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
+Proof.
+ split.
+ - induct s x; now auto.
+ - induct s x; intuition_in; order.
+Qed.
+
+(** ** Minimal and maximal elements *)
+
+Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
+Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.
+
+Lemma min_elt_spec1 s x : min_elt s = Some x -> InT x s.
+Proof.
+ functional induction (min_elt s); auto; inversion 1; auto.
+Qed.
+
+Lemma min_elt_spec2 s x y `{Ok s} :
+ min_elt s = Some x -> InT y s -> ~ X.lt y x.
+Proof.
+ revert y.
+ functional induction (min_elt s);
+ try rename _x0 into r; try rename _x2 into l1, _x3 into x1, _x4 into r1.
+ - discriminate.
+ - intros y V W.
+   inversion V; clear V; subst.
+   inv; order.
+ - intros; inv; auto.
+   * assert (X.lt x x0) by (apply H8; apply min_elt_spec1; auto).
+     order.
+   * assert (X.lt x1 x0) by auto.
+     assert (~X.lt x1 x) by auto.
+     order.
+Qed.
+
+Lemma min_elt_spec3 s : min_elt s = None -> Empty s.
+Proof.
+ functional induction (min_elt s).
+ red; red; inversion 2.
+ inversion 1.
+ intro H0.
+ destruct (IHo H0 _x3); auto.
+Qed.
+
+Lemma max_elt_spec1 s x : max_elt s = Some x -> InT x s.
+Proof.
+ functional induction (max_elt s); auto; inversion 1; auto.
+Qed.
+
+Lemma max_elt_spec2 s x y `{Ok s} :
+ max_elt s = Some x -> InT y s -> ~ X.lt x y.
+Proof.
+ revert y.
+ functional induction (max_elt s);
+ try rename _x0 into r; try rename _x2 into l1, _x3 into x1, _x4 into r1.
+ - discriminate.
+ - intros y V W.
+   inversion V; clear V; subst.
+   inv; order.
+ - intros; inv; auto.
+   * assert (X.lt x0 x) by (apply H9; apply max_elt_spec1; auto).
+     order.
+   * assert (X.lt x0 x1) by auto.
+     assert (~X.lt x x1) by auto.
+     order.
+Qed.
+
+Lemma max_elt_spec3 s : max_elt s = None -> Empty s.
+Proof.
+ functional induction (max_elt s).
+ red; red; inversion 2.
+ inversion 1.
+ intro H0.
+ destruct (IHo H0 _x3); auto.
+Qed.
+
+Lemma choose_spec1 : forall s x, choose s = Some x -> InT x s.
+Proof.
+ exact min_elt_spec1.
+Qed.
+
+Lemma choose_spec2 : forall s, choose s = None -> Empty s.
+Proof.
+ exact min_elt_spec3.
+Qed.
+
+Lemma choose_spec3 : forall s s' x x' `{Ok s, Ok s'},
+  choose s = Some x -> choose s' = Some x' ->
+  Equal s s' -> X.eq x x'.
+Proof.
+ unfold choose, Equal; intros s s' x x' Hb Hb' Hx Hx' H.
+ assert (~X.lt x x').
+  apply min_elt_spec2 with s'; auto.
+  rewrite <-H; auto using min_elt_spec1.
+ assert (~X.lt x' x).
+  apply min_elt_spec2 with s; auto.
+  rewrite H; auto using min_elt_spec1.
+ elim_compare x x'; intuition.
+Qed.
+
+(** ** Elements *)
+
+Lemma elements_spec1' : forall s acc x,
+ InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc.
+Proof.
+ induction s as [ | c l Hl x r Hr ]; simpl; auto.
+ intuition.
+ inversion H0.
+ intros.
+ rewrite Hl.
+ destruct (Hr acc x0); clear Hl Hr.
+ intuition; inversion_clear H3; intuition.
+Qed.
+
+Lemma elements_spec1 : forall s x, InA X.eq x (elements s) <-> InT x s.
+Proof.
+ intros; generalize (elements_spec1' s nil x); intuition.
+ inversion_clear H0.
+Qed.
+
+Lemma elements_spec2' : forall s acc `{Ok s}, sort X.lt acc ->
+ (forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) ->
+ sort X.lt (elements_aux acc s).
+Proof.
+ induction s as [ | c l Hl y r Hr]; simpl; intuition.
+ inv.
+ apply Hl; auto.
+ constructor.
+ apply Hr; auto.
+ eapply InA_InfA; eauto with *.
+ intros.
+ destruct (elements_spec1' r acc y0); intuition.
+ intros.
+ inversion_clear H.
+ order.
+ destruct (elements_spec1' r acc x); intuition eauto.
+Qed.
+
+Lemma elements_spec2 : forall s `(Ok s), sort X.lt (elements s).
+Proof.
+ intros; unfold elements; apply elements_spec2'; auto.
+ intros; inversion H0.
+Qed.
+Local Hint Resolve elements_spec2.
+
+Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s).
+Proof.
+ intros. eapply SortA_NoDupA; eauto with *.
+Qed.
+
+Lemma elements_aux_cardinal :
+ forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s).
+Proof.
+ simple induction s; simpl; intuition.
+ rewrite <- H.
+ simpl.
+ rewrite <- H0. rewrite (Nat.add_comm (cardinal t0)).
+ now rewrite <- Nat.add_succ_r, Nat.add_assoc.
+Qed.
+
+Lemma elements_cardinal : forall s : tree, cardinal s = length (elements s).
+Proof.
+ exact (fun s => elements_aux_cardinal s nil).
+Qed.
+
+Definition cardinal_spec (s:tree)(Hs:Ok s) := elements_cardinal s.
+
+Lemma elements_app :
+ forall s acc, elements_aux acc s = elements s ++ acc.
+Proof.
+ induction s; simpl; intros; auto.
+ rewrite IHs1, IHs2.
+ unfold elements; simpl.
+ rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto.
+Qed.
+
+Lemma elements_node c l x r :
+ elements (Node c l x r) = elements l ++ x :: elements r.
+Proof.
+ unfold elements; simpl.
+ now rewrite !elements_app, !app_nil_r.
+Qed.
+
+Lemma rev_elements_app :
+ forall s acc, rev_elements_aux acc s = rev_elements s ++ acc.
+Proof.
+ induction s; simpl; intros; auto.
+ rewrite IHs1, IHs2.
+ unfold rev_elements; simpl.
+ rewrite IHs1, 2 IHs2, !app_nil_r, !app_ass; auto.
+Qed.
+
+Lemma rev_elements_node c l x r :
+ rev_elements (Node c l x r) = rev_elements r ++ x :: rev_elements l.
+Proof.
+ unfold rev_elements; simpl.
+ now rewrite !rev_elements_app, !app_nil_r.
+Qed.
+
+Lemma rev_elements_rev s : rev_elements s = rev (elements s).
+Proof.
+ induction s as [|c l IHl x r IHr]; trivial.
+ rewrite elements_node, rev_elements_node, IHl, IHr, rev_app_distr.
+ simpl. now rewrite !app_ass.
+Qed.
+
+(** The converse of [elements_spec2], used in MSetRBT *)
+
+(* TODO: TO MIGRATE ELSEWHERE... *)
+
+Lemma sorted_app_inv l1 l2 :
+ sort X.lt (l1++l2) ->
+ sort X.lt l1 /\ sort X.lt l2 /\
+ forall x1 x2, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2.
+Proof.
+ induction l1 as [|a1 l1 IHl1].
+ - simpl; repeat split; auto.
+   intros. now rewrite InA_nil in *.
+ - simpl. inversion_clear 1 as [ | ? ? Hs Hhd ].
+   destruct (IHl1 Hs) as (H1 & H2 & H3).
+   repeat split.
+   * constructor; auto.
+     destruct l1; simpl in *; auto; inversion_clear Hhd; auto.
+   * trivial.
+   * intros x1 x2 Hx1 Hx2. rewrite InA_cons in Hx1. destruct Hx1.
+     + rewrite H.
+       apply SortA_InfA_InA with (eqA:=X.eq)(l:=l1++l2); auto_tc.
+       rewrite InA_app_iff; auto_tc.
+     + auto.
+Qed.
+
+Lemma elements_sort_ok s : sort X.lt (elements s) -> Ok s.
+Proof.
+ induction s as [|c l IHl x r IHr].
+ - auto.
+ - rewrite elements_node.
+   intros H. destruct (sorted_app_inv _ _ H) as (H1 & H2 & H3).
+   inversion_clear H2.
+   constructor; ok.
+   * intros y Hy. apply H3.
+     + now rewrite elements_spec1.
+     + rewrite InA_cons. now left.
+   * intros y Hy.
+     apply SortA_InfA_InA with (eqA:=X.eq)(l:=elements r); auto_tc.
+     now rewrite elements_spec1.
+Qed.
+
+(** ** [for_all] and [exists] *)
+
+Lemma for_all_spec s f : Proper (X.eq==>eq) f ->
+ (for_all f s = true <-> For_all (fun x => f x = true) s).
+Proof.
+ intros Hf; unfold For_all.
+ induction s as [|i l IHl x r IHr]; simpl; auto.
+ - split; intros; inv; auto.
+ - rewrite <- !andb_lazy_alt, !andb_true_iff, IHl, IHr. clear IHl IHr.
+   intuition_in. eauto.
+Qed.
+
+Lemma exists_spec s f : Proper (X.eq==>eq) f ->
+ (exists_ f s = true <-> Exists (fun x => f x = true) s).
+Proof.
+ intros Hf; unfold Exists.
+ induction s as [|i l IHl x r IHr]; simpl; auto.
+ - split.
+   * discriminate.
+   * intros (y,(H,_)); inv.
+ - rewrite <- !orb_lazy_alt, !orb_true_iff, IHl, IHr. clear IHl IHr.
+   split; [intros [[H|(y,(H,H'))]|(y,(H,H'))]|intros (y,(H,H'))].
+   * exists x; auto.
+   * exists y; auto.
+   * exists y; auto.
+   * inv; [left;left|left;right|right]; try (exists y); eauto.
+Qed.
+
+(** ** Fold *)
+
+Lemma fold_spec' {A} (f : elt -> A -> A) (s : tree) (i : A) (acc : list elt) :
+ fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i).
+Proof.
+ revert i acc.
+ induction s as [|c l IHl x r IHr]; simpl; intros; auto.
+ rewrite IHl.
+ simpl. unfold flip at 2.
+ apply IHr.
+Qed.
+
+Lemma fold_spec (s:tree) {A} (i : A) (f : elt -> A -> A) :
+ fold f s i = fold_left (flip f) (elements s) i.
+Proof.
+ revert i. unfold elements.
+ induction s as [|c l IHl x r IHr]; simpl; intros; auto.
+ rewrite fold_spec'.
+ rewrite IHr.
+ simpl; auto.
+Qed.
+
+
+(** ** Subset *)
+
+Lemma subsetl_spec : forall subset_l1 l1 x1 c1 s2
+ `{Ok (Node c1 l1 x1 Leaf), Ok s2},
+ (forall s `{Ok s}, (subset_l1 s = true <-> Subset l1 s)) ->
+ (subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2 ).
+Proof.
+ induction s2 as [|c2 l2 IHl2 x2 r2 IHr2]; simpl; intros.
+ unfold Subset; intuition; try discriminate.
+ assert (H': InT x1 Leaf) by auto; inversion H'.
+ specialize (IHl2 H).
+ specialize (IHr2 H).
+ inv.
+ elim_compare x1 x2.
+
+ rewrite H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+
+ rewrite IHl2 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ constructor 3. setoid_replace a with x1; auto. rewrite <- mem_spec; auto.
+ rewrite mem_spec; auto.
+ assert (InT x1 (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+Qed.
+
+
+Lemma subsetr_spec : forall subset_r1 r1 x1 c1 s2,
+ bst (Node c1 Leaf x1 r1) -> bst s2 ->
+ (forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) ->
+ (subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) s2).
+Proof.
+ induction s2 as [|c2 l2 IHl2 x2 r2 IHr2]; simpl; intros.
+ unfold Subset; intuition; try discriminate.
+ assert (H': InT x1 Leaf) by auto; inversion H'.
+ specialize (IHl2 H).
+ specialize (IHr2 H).
+ inv.
+ elim_compare x1 x2.
+
+ rewrite H1 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto;  clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ constructor 2. setoid_replace a with x1; auto. rewrite <- mem_spec; auto.
+ rewrite mem_spec; auto.
+ assert (InT x1 (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+
+ rewrite IHr2 by auto; clear H1 IHl2 IHr2.
+ unfold Subset. intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+Qed.
+
+Lemma subset_spec : forall s1 s2 `{Ok s1, Ok s2},
+ (subset s1 s2 = true <-> Subset s1 s2).
+Proof.
+ induction s1 as [|c1 l1 IHl1 x1 r1 IHr1]; simpl; intros.
+ unfold Subset; intuition_in.
+ destruct s2 as [|c2 l2 x2 r2]; simpl; intros.
+ unfold Subset; intuition_in; try discriminate.
+ assert (H': InT x1 Leaf) by auto; inversion H'.
+ inv.
+ elim_compare x1 x2.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto.
+ clear IHl1 IHr1.
+ unfold Subset; intuition_in.
+ assert (X.eq a x2) by order; intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto.
+ rewrite (@subsetl_spec (subset l1) l1 x1 c1) by auto.
+ clear IHl1 IHr1.
+ unfold Subset; intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+
+ rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto.
+ rewrite (@subsetr_spec (subset r1) r1 x1 c1) by auto.
+ clear IHl1 IHr1.
+ unfold Subset; intuition_in.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+ assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order.
+Qed.
+
+
+(** ** Comparison *)
+
+(** Relations [eq] and [lt] over trees *)
+
+Module L := MSetInterface.MakeListOrdering X.
+
+Definition eq := Equal.
+Instance eq_equiv : Equivalence eq.
+Proof. firstorder. Qed.
+
+Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
+Proof.
+ unfold eq, Equal, L.eq; intros.
+ setoid_rewrite elements_spec1; firstorder.
+Qed.
+
+Definition lt (s1 s2 : tree) : Prop :=
+ exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
+   /\ L.lt (elements s1') (elements s2').
+
+Instance lt_strorder : StrictOrder lt.
+Proof.
+ split.
+ intros s (s1 & s2 & B1 & B2 & E1 & E2 & L).
+ assert (eqlistA X.eq (elements s1) (elements s2)).
+  apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
+  rewrite <- eq_Leq. transitivity s; auto. symmetry; auto.
+ rewrite H in L.
+ apply (StrictOrder_Irreflexive (elements s2)); auto.
+ intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
+                 (s2'' & s3' & B2' & B3 & E2' & E3 & L23).
+ exists s1', s3'; do 4 (split; trivial).
+ assert (eqlistA X.eq (elements s2') (elements s2'')).
+  apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *.
+  rewrite <- eq_Leq. transitivity s2; auto. symmetry; auto.
+ transitivity (elements s2'); auto.
+ rewrite H; auto.
+Qed.
+
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Proof.
+ intros s1 s2 E12 s3 s4 E34. split.
+ intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
+ exists s1', s3'; do 2 (split; trivial).
+  split. transitivity s1; auto. symmetry; auto.
+  split; auto. transitivity s3; auto. symmetry; auto.
+ intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
+ exists s1', s3'; do 2 (split; trivial).
+  split. transitivity s2; auto.
+  split; auto. transitivity s4; auto.
+Qed.
+
+
+(** Proof of the comparison algorithm *)
+
+(** [flatten_e e] returns the list of elements of [e] i.e. the list
+    of elements actually compared *)
+
+Fixpoint flatten_e (e : enumeration) : list elt := match e with
+  | End => nil
+  | More x t r => x :: elements t ++ flatten_e r
+ end.
+
+Lemma flatten_e_elements :
+ forall l x r c e,
+ elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e.
+Proof.
+ intros; simpl. now rewrite elements_node, app_ass.
+Qed.
+
+Lemma cons_1 : forall s e,
+  flatten_e (cons s e) = elements s ++ flatten_e e.
+Proof.
+ induction s; simpl; auto; intros.
+ rewrite IHs1; apply flatten_e_elements.
+Qed.
+
+(** Correctness of this comparison *)
+
+Definition Cmp c x y := CompSpec L.eq L.lt x y c.
+
+Local Hint Unfold Cmp flip.
+
+Lemma compare_end_Cmp :
+ forall e2, Cmp (compare_end e2) nil (flatten_e e2).
+Proof.
+ destruct e2; simpl; constructor; auto. reflexivity.
+Qed.
+
+Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
+  Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
+   Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
+      (flatten_e (More x2 r2 e2)).
+Proof.
+ simpl; intros; elim_compare x1 x2; simpl; red; auto.
+Qed.
+
+Lemma compare_cont_Cmp : forall s1 cont e2 l,
+ (forall e, Cmp (cont e) l (flatten_e e)) ->
+ Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
+Proof.
+ induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; simpl; intros; auto.
+ rewrite elements_node, app_ass; simpl.
+ apply Hl1; auto. clear e2. intros [|x2 r2 e2].
+ simpl; auto.
+ apply compare_more_Cmp.
+ rewrite <- cons_1; auto.
+Qed.
+
+Lemma compare_Cmp : forall s1 s2,
+ Cmp (compare s1 s2) (elements s1) (elements s2).
+Proof.
+ intros; unfold compare.
+ rewrite (app_nil_end (elements s1)).
+ replace (elements s2) with (flatten_e (cons s2 End)) by
+  (rewrite cons_1; simpl; rewrite <- app_nil_end; auto).
+ apply compare_cont_Cmp; auto.
+ intros.
+ apply compare_end_Cmp; auto.
+Qed.
+
+Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
+ CompSpec eq lt s1 s2 (compare s1 s2).
+Proof.
+ intros.
+ destruct (compare_Cmp s1 s2); constructor.
+ rewrite eq_Leq; auto.
+ intros; exists s1, s2; repeat split; auto.
+ intros; exists s2, s1; repeat split; auto.
+Qed.
+
+
+(** ** Equality test *)
+
+Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2},
+ equal s1 s2 = true <-> eq s1 s2.
+Proof.
+unfold equal; intros s1 s2 B1 B2.
+destruct (@compare_spec s1 s2 B1 B2) as [H|H|H];
+ split; intros H'; auto; try discriminate.
+rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
+rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
+Qed.
+
+(** ** A few results about [mindepth] and [maxdepth] *)
+
+Lemma mindepth_maxdepth s : mindepth s <= maxdepth s.
+Proof.
+ induction s; simpl; auto.
+ rewrite <- Nat.succ_le_mono.
+ transitivity (mindepth s1). apply Nat.le_min_l.
+ transitivity (maxdepth s1). trivial. apply Nat.le_max_l.
+Qed.
+
+Lemma maxdepth_cardinal s : cardinal s < 2^(maxdepth s).
+Proof.
+ unfold Peano.lt.
+ induction s as [|c l IHl x r IHr].
+ - auto.
+ - simpl. rewrite <- Nat.add_succ_r, <- Nat.add_succ_l, Nat.add_0_r.
+   apply Nat.add_le_mono; etransitivity;
+   try apply IHl; try apply IHr; apply Nat.pow_le_mono; auto.
+   * apply Nat.le_max_l.
+   * apply Nat.le_max_r.
+Qed.
+
+Lemma mindepth_cardinal s : 2^(mindepth s) <= S (cardinal s).
+Proof.
+ unfold Peano.lt.
+ induction s as [|c l IHl x r IHr].
+ - auto.
+ - simpl. rewrite <- Nat.add_succ_r, <- Nat.add_succ_l, Nat.add_0_r.
+   apply Nat.add_le_mono; etransitivity;
+   try apply IHl; try apply IHr; apply Nat.pow_le_mono; auto.
+   * apply Nat.le_min_l.
+   * apply Nat.le_min_r.
+Qed.
+
+Lemma maxdepth_log_cardinal s : s <> Leaf ->
+ log2 (cardinal s) < maxdepth s.
+Proof.
+ intros H.
+ apply Nat.log2_lt_pow2. destruct s; simpl; intuition.
+ apply maxdepth_cardinal.
+Qed.
+
+Lemma mindepth_log_cardinal s : mindepth s <= log2 (S (cardinal s)).
+Proof.
+ apply Nat.log2_le_pow2. auto with arith.
+ apply mindepth_cardinal.
+Qed.
+
+End Props.
\ No newline at end of file
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
new file mode 100644
index 00000000..b53c0392
--- /dev/null
+++ b/theories/MSets/MSetRBT.v
@@ -0,0 +1,1931 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * MSetRBT : Implementation of MSetInterface via Red-Black trees *)
+
+(** Initial author: Andrew W. Appel, 2011.
+    Extra modifications by: Pierre Letouzey
+
+The design decisions behind this implementation are described here:
+
+ - Efficient Verified Red-Black Trees, by Andrew W. Appel, September 2011.
+   http://www.cs.princeton.edu/~appel/papers/redblack.pdf
+
+Additional suggested reading:
+
+ - Red-Black Trees in a Functional Setting by Chris Okasaki.
+   Journal of Functional Programming, 9(4):471-477, July 1999.
+   http://www.eecs.usma.edu/webs/people/okasaki/jfp99redblack.pdf
+
+ - Red-black trees with types, by Stefan Kahrs.
+   Journal of Functional Programming, 11(4), 425-432, 2001.
+
+ - Functors for Proofs and Programs, by J.-C. Filliatre and P. Letouzey.
+   ESOP'04: European Symposium on Programming, pp. 370-384, 2004.
+   http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz
+*)
+
+Require MSetGenTree.
+Require Import Bool List BinPos Pnat Setoid SetoidList NPeano Psatz.
+Local Open Scope list_scope.
+
+(* For nicer extraction, we create induction principles
+   only when needed *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
+(** An extra function not (yet?) in MSetInterface.S *)
+
+Module Type MSetRemoveMin (Import M:MSetInterface.S).
+
+ Parameter remove_min : t -> option (elt * t).
+
+ Axiom remove_min_spec1 : forall s k s',
+  remove_min s = Some (k,s') ->
+   min_elt s = Some k /\ remove k s [=] s'.
+
+ Axiom remove_min_spec2 : forall s, remove_min s = None -> Empty s.
+
+End MSetRemoveMin.
+
+(** The type of color annotation. *)
+
+Inductive color := Red | Black.
+
+Module Color.
+ Definition t := color.
+End Color.
+
+(** * Ops : the pure functions *)
+
+Module Ops (X:Orders.OrderedType) <: MSetInterface.Ops X.
+
+(** ** Generic trees instantiated with color *)
+
+(** We reuse a generic definition of trees where the information
+    parameter is a color. Functions like mem or fold are also
+    provided by this generic functor. *)
+
+Include MSetGenTree.Ops X Color.
+
+Definition t := tree.
+Local Notation Rd := (Node Red).
+Local Notation Bk := (Node Black).
+
+(** ** Basic tree *)
+
+Definition singleton (k: elt) : tree := Bk Leaf k Leaf.
+
+(** ** Changing root color *)
+
+Definition makeBlack t :=
+ match t with
+ | Leaf => Leaf
+ | Node _ a x b => Bk a x b
+ end.
+
+Definition makeRed t :=
+ match t with
+ | Leaf => Leaf
+ | Node _ a x b => Rd a x b
+ end.
+
+(** ** Balancing *)
+
+(** We adapt when one side is not a true red-black tree.
+    Both sides have the same black depth. *)
+
+Definition lbal l k r :=
+ match l with
+ | Rd (Rd a x b) y c => Rd (Bk a x b) y (Bk c k r)
+ | Rd a x (Rd b y c) => Rd (Bk a x b) y (Bk c k r)
+ | _ => Bk l k r
+ end.
+
+Definition rbal l k r :=
+ match r with
+ | Rd (Rd b y c) z d => Rd (Bk l k b) y (Bk c z d)
+ | Rd b y (Rd c z d) => Rd (Bk l k b) y (Bk c z d)
+ | _ => Bk l k r
+ end.
+
+(** A variant of [rbal], with reverse pattern order.
+    Is it really useful ? Should we always use it ? *)
+
+Definition rbal' l k r :=
+ match r with
+ | Rd b y (Rd c z d) => Rd (Bk l k b) y (Bk c z d)
+ | Rd (Rd b y c) z d => Rd (Bk l k b) y (Bk c z d)
+ | _ => Bk l k r
+ end.
+
+(** Balancing with different black depth.
+    One side is almost a red-black tree, while the other is
+    a true red-black tree, but with black depth + 1.
+    Used in deletion. *)
+
+Definition lbalS l k r :=
+ match l with
+ | Rd a x b => Rd (Bk a x b) k r
+ | _ =>
+   match r with
+   | Bk a y b => rbal' l k (Rd a y b)
+   | Rd (Bk a y b) z c => Rd (Bk l k a) y (rbal' b z (makeRed c))
+   | _ => Rd l k r (* impossible *)
+   end
+ end.
+
+Definition rbalS l k r :=
+ match r with
+ | Rd b y c => Rd l k (Bk b y c)
+ | _ =>
+   match l with
+   | Bk a x b => lbal (Rd a x b) k r
+   | Rd a x (Bk b y c) => Rd (lbal (makeRed a) x b) y (Bk c k r)
+   | _ => Rd l k r (* impossible *)
+   end
+ end.
+
+(** ** Insertion *)
+
+Fixpoint ins x s :=
+ match s with
+ | Leaf => Rd Leaf x Leaf
+ | Node c l y r =>
+   match X.compare x y with
+   | Eq => s
+   | Lt =>
+     match c with
+     | Red => Rd (ins x l) y r
+     | Black => lbal (ins x l) y r
+     end
+   | Gt =>
+     match c with
+     | Red => Rd l y (ins x r)
+     | Black => rbal l y (ins x r)
+     end
+   end
+ end.
+
+Definition add x s := makeBlack (ins x s).
+
+(** ** Deletion *)
+
+Fixpoint append (l:tree) : tree -> tree :=
+ match l with
+ | Leaf => fun r => r
+ | Node lc ll lx lr =>
+   fix append_l (r:tree) : tree :=
+   match r with
+   | Leaf => l
+   | Node rc rl rx rr =>
+     match lc, rc with
+     | Red, Red =>
+       let lrl := append lr rl in
+       match lrl with
+       | Rd lr' x rl' => Rd (Rd ll lx lr') x (Rd rl' rx rr)
+       | _ => Rd ll lx (Rd lrl rx rr)
+       end
+     | Black, Black =>
+       let lrl := append lr rl in
+       match lrl with
+       | Rd lr' x rl' => Rd (Bk ll lx lr') x (Bk rl' rx rr)
+       | _ => lbalS ll lx (Bk lrl rx rr)
+       end
+     | Black, Red => Rd (append_l rl) rx rr
+     | Red, Black => Rd ll lx (append lr r)
+     end
+   end
+ end.
+
+Fixpoint del x t :=
+ match t with
+ | Leaf => Leaf
+ | Node _ a y b =>
+   match X.compare x y with
+   | Eq => append a b
+   | Lt =>
+     match a with
+     | Bk _ _ _ => lbalS (del x a) y b
+     | _ => Rd (del x a) y b
+     end
+   | Gt =>
+     match b with
+     | Bk _ _ _ => rbalS a y (del x b)
+     | _ => Rd a y (del x b)
+     end
+   end
+ end.
+
+Definition remove x t := makeBlack (del x t).
+
+(** ** Removing minimal element *)
+
+Fixpoint delmin l x r : (elt * tree) :=
+ match l with
+ | Leaf => (x,r)
+ | Node lc ll lx lr =>
+   let (k,l') := delmin ll lx lr in
+   match lc with
+   | Black => (k, lbalS l' x r)
+   | Red => (k, Rd l' x r)
+   end
+ end.
+
+Definition remove_min t : option (elt * tree) :=
+ match t with
+ | Leaf => None
+ | Node _ l x r =>
+   let (k,t) := delmin l x r in
+   Some (k, makeBlack t)
+ end.
+
+(** ** Tree-ification
+
+    We rebuild a tree of size [if pred then n-1 else n] as soon
+    as the list [l] has enough elements *)
+
+Definition bogus : tree * list elt := (Leaf, nil).
+
+Notation treeify_t := (list elt -> tree * list elt).
+
+Definition treeify_zero : treeify_t :=
+ fun acc => (Leaf,acc).
+
+Definition treeify_one : treeify_t :=
+ fun acc => match acc with
+ | x::acc => (Rd Leaf x Leaf, acc)
+ | _ => bogus
+ end.
+
+Definition treeify_cont (f g : treeify_t) : treeify_t :=
+ fun acc =>
+ match f acc with
+ | (l, x::acc) =>
+   match g acc with
+   | (r, acc) => (Bk l x r, acc)
+   end
+ | _ => bogus
+ end.
+
+Fixpoint treeify_aux (pred:bool)(n: positive) : treeify_t :=
+ match n with
+ | xH => if pred then treeify_zero else treeify_one
+ | xO n => treeify_cont (treeify_aux pred n) (treeify_aux true n)
+ | xI n => treeify_cont (treeify_aux false n) (treeify_aux pred n)
+ end.
+
+Fixpoint plength (l:list elt) := match l with
+ | nil => 1%positive
+ | _::l => Psucc (plength l)
+end.
+
+Definition treeify (l:list elt) :=
+ fst (treeify_aux true (plength l) l).
+
+(** ** Filtering *)
+
+Fixpoint filter_aux (f: elt -> bool) s acc :=
+ match s with
+ | Leaf => acc
+ | Node _ l k r =>
+   let acc := filter_aux f r acc in
+   if f k then filter_aux f l (k::acc)
+   else filter_aux f l acc
+ end.
+
+Definition filter (f: elt -> bool) (s: t) : t :=
+ treeify (filter_aux f s nil).
+
+Fixpoint partition_aux (f: elt -> bool) s acc1 acc2 :=
+ match s with
+ | Leaf => (acc1,acc2)
+ | Node _ sl k sr =>
+   let (acc1, acc2) := partition_aux f sr acc1 acc2 in
+   if f k then partition_aux f sl (k::acc1) acc2
+   else partition_aux f sl acc1 (k::acc2)
+ end.
+
+Definition partition (f: elt -> bool) (s:t) : t*t :=
+  let (ok,ko) := partition_aux f s nil nil in
+  (treeify ok, treeify ko).
+
+(** ** Union, intersection, difference *)
+
+(** union of the elements of [l1] and [l2] into a third [acc] list. *)
+
+Fixpoint union_list l1 : list elt -> list elt -> list elt :=
+ match l1 with
+ | nil => @rev_append _
+ | x::l1' =>
+    fix union_l1 l2 acc :=
+    match l2 with
+    | nil => rev_append l1 acc
+    | y::l2' =>
+       match X.compare x y with
+       | Eq => union_list l1' l2' (x::acc)
+       | Lt => union_l1 l2' (y::acc)
+       | Gt => union_list l1' l2 (x::acc)
+       end
+    end
+ end.
+
+Definition linear_union s1 s2 :=
+  treeify (union_list (rev_elements s1) (rev_elements s2) nil).
+
+Fixpoint inter_list l1 : list elt -> list elt -> list elt :=
+ match l1 with
+ | nil => fun _ acc => acc
+ | x::l1' =>
+    fix inter_l1 l2 acc :=
+    match l2 with
+    | nil => acc
+    | y::l2' =>
+       match X.compare x y with
+       | Eq => inter_list l1' l2' (x::acc)
+       | Lt => inter_l1 l2' acc
+       | Gt => inter_list l1' l2 acc
+       end
+    end
+ end.
+
+Definition linear_inter s1 s2 :=
+  treeify (inter_list (rev_elements s1) (rev_elements s2) nil).
+
+Fixpoint diff_list l1 : list elt -> list elt -> list elt :=
+ match l1 with
+ | nil => fun _ acc => acc
+ | x::l1' =>
+    fix diff_l1 l2 acc :=
+    match l2 with
+    | nil => rev_append l1 acc
+    | y::l2' =>
+       match X.compare x y with
+       | Eq => diff_list l1' l2' acc
+       | Lt => diff_l1 l2' acc
+       | Gt => diff_list l1' l2 (x::acc)
+       end
+    end
+ end.
+
+Definition linear_diff s1 s2 :=
+  treeify (diff_list (rev_elements s1) (rev_elements s2) nil).
+
+(** [compare_height] returns:
+  - [Lt] if [height s2] is at least twice [height s1];
+  - [Gt] if [height s1] is at least twice [height s2];
+  - [Eq] if heights are approximately equal.
+  Warning: this is not an equivalence relation! but who cares.... *)
+
+Definition skip_red t :=
+ match t with
+ | Rd t' _ _ => t'
+ | _ => t
+ end.
+
+Definition skip_black t :=
+ match skip_red t with
+ | Bk t' _ _ => t'
+ | t' => t'
+ end.
+
+Fixpoint compare_height (s1x s1 s2 s2x: tree) : comparison :=
+ match skip_red s1x, skip_red s1, skip_red s2, skip_red s2x with
+ | Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Node _ s2x' _ _ =>
+   compare_height (skip_black s2x') s1' s2' (skip_black s2x')
+ | _, Leaf, _, Node _ _ _ _ => Lt
+ | Node _ _ _ _, _, Leaf, _ => Gt
+ | Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Leaf =>
+   compare_height (skip_black s1x') s1' s2' Leaf
+ | Leaf, Node _ s1' _ _, Node _ s2' _ _, Node _ s2x' _ _ =>
+   compare_height Leaf s1'  s2'  (skip_black s2x')
+ | _, _, _, _ => Eq
+ end.
+
+(** When one tree is quite smaller than the other, we simply
+    adds repeatively all its elements in the big one.
+    For trees of comparable height, we rather use [linear_union]. *)
+
+Definition union (t1 t2: t) : t :=
+ match compare_height t1 t1 t2 t2 with
+ | Lt => fold add t1 t2
+ | Gt => fold add t2 t1
+ | Eq => linear_union t1 t2
+ end.
+
+Definition diff (t1 t2: t) : t :=
+ match compare_height t1 t1 t2 t2 with
+ | Lt => filter (fun k => negb (mem k t2)) t1
+ | Gt => fold remove t2 t1
+ | Eq => linear_diff t1 t2
+ end.
+
+Definition inter (t1 t2: t) : t :=
+ match compare_height t1 t1 t2 t2 with
+ | Lt => filter (fun k => mem k t2) t1
+ | Gt => filter (fun k => mem k t1) t2
+ | Eq => linear_inter t1 t2
+ end.
+
+End Ops.
+
+(** * MakeRaw : the pure functions and their specifications *)
+
+Module Type MakeRaw (X:Orders.OrderedType) <: MSetInterface.RawSets X.
+Include Ops X.
+
+(** Generic definition of binary-search-trees and proofs of
+    specifications for generic functions such as mem or fold. *)
+
+Include MSetGenTree.Props X Color.
+
+Local Notation Rd := (Node Red).
+Local Notation Bk := (Node Black).
+
+Local Hint Immediate MX.eq_sym.
+Local Hint Unfold In lt_tree gt_tree Ok.
+Local Hint Constructors InT bst.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+Local Hint Resolve elements_spec2.
+
+(** ** Singleton set *)
+
+Lemma singleton_spec x y : InT y (singleton x) <-> X.eq y x.
+Proof.
+ unfold singleton; intuition_in.
+Qed.
+
+Instance singleton_ok x : Ok (singleton x).
+Proof.
+ unfold singleton; auto.
+Qed.
+
+(** ** makeBlack, MakeRed *)
+
+Lemma makeBlack_spec s x : InT x (makeBlack s) <-> InT x s.
+Proof.
+ destruct s; simpl; intuition_in.
+Qed.
+
+Lemma makeRed_spec s x : InT x (makeRed s) <-> InT x s.
+Proof.
+ destruct s; simpl; intuition_in.
+Qed.
+
+Instance makeBlack_ok s `{Ok s} : Ok (makeBlack s).
+Proof.
+ destruct s; simpl; ok.
+Qed.
+
+Instance makeRed_ok s `{Ok s} : Ok (makeRed s).
+Proof.
+ destruct s; simpl; ok.
+Qed.
+
+(** ** Generic handling for red-matching and red-red-matching *)
+
+Definition isblack t :=
+ match t with Bk _ _ _ => True | _ => False end.
+
+Definition notblack t :=
+ match t with Bk _ _ _ => False | _ => True end.
+
+Definition notred t :=
+ match t with Rd _ _ _ => False | _ => True end.
+
+Definition rcase {A} f g t : A :=
+ match t with
+ | Rd a x b => f a x b
+ | _ => g t
+ end.
+
+Inductive rspec {A} f g : tree -> A -> Prop :=
+ | rred a x b : rspec f g (Rd a x b) (f a x b)
+ | relse t : notred t -> rspec f g t (g t).
+
+Fact rmatch {A} f g t : rspec (A:=A) f g t (rcase f g t).
+Proof.
+destruct t as [|[|] l x r]; simpl; now constructor.
+Qed.
+
+Definition rrcase {A} f g t : A :=
+ match t with
+ | Rd (Rd a x b) y c => f a x b y c
+ | Rd a x (Rd b y c) => f a x b y c
+ | _ => g t
+ end.
+
+Notation notredred := (rrcase (fun _ _ _ _ _ => False) (fun _ => True)).
+
+Inductive rrspec {A} f g : tree -> A -> Prop :=
+ | rrleft a x b y c : rrspec f g (Rd (Rd a x b) y c) (f a x b y c)
+ | rrright a x b y c : rrspec f g (Rd a x (Rd b y c)) (f a x b y c)
+ | rrelse t : notredred t -> rrspec f g t (g t).
+
+Fact rrmatch {A} f g t : rrspec (A:=A) f g t (rrcase f g t).
+Proof.
+destruct t as [|[|] l x r]; simpl; try now constructor.
+destruct l as [|[|] ll lx lr], r as [|[|] rl rx rr]; now constructor.
+Qed.
+
+Definition rrcase' {A} f g t : A :=
+ match t with
+ | Rd a x (Rd b y c) => f a x b y c
+ | Rd (Rd a x b) y c => f a x b y c
+ | _ => g t
+ end.
+
+Fact rrmatch' {A} f g t : rrspec (A:=A) f g t (rrcase' f g t).
+Proof.
+destruct t as [|[|] l x r]; simpl; try now constructor.
+destruct l as [|[|] ll lx lr], r as [|[|] rl rx rr]; now constructor.
+Qed.
+
+(** Balancing operations are instances of generic match *)
+
+Fact lbal_match l k r :
+ rrspec
+   (fun a x b y c => Rd (Bk a x b) y (Bk c k r))
+   (fun l => Bk l k r)
+   l
+   (lbal l k r).
+Proof.
+ exact (rrmatch _ _ _).
+Qed.
+
+Fact rbal_match l k r :
+ rrspec
+   (fun a x b y c => Rd (Bk l k a) x (Bk b y c))
+   (fun r => Bk l k r)
+   r
+   (rbal l k r).
+Proof.
+ exact (rrmatch _ _ _).
+Qed.
+
+Fact rbal'_match l k r :
+ rrspec
+   (fun a x b y c => Rd (Bk l k a) x (Bk b y c))
+   (fun r => Bk l k r)
+   r
+   (rbal' l k r).
+Proof.
+ exact (rrmatch' _ _ _).
+Qed.
+
+Fact lbalS_match l x r :
+ rspec
+  (fun a y b => Rd (Bk a y b) x r)
+  (fun l =>
+    match r with
+    | Bk a y b => rbal' l x (Rd a y b)
+    | Rd (Bk a y b) z c => Rd (Bk l x a) y (rbal' b z (makeRed c))
+    | _ => Rd l x r
+    end)
+  l
+  (lbalS l x r).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+Fact rbalS_match l x r :
+ rspec
+  (fun a y b => Rd l x (Bk a y b))
+  (fun r =>
+    match l with
+    | Bk a y b => lbal (Rd a y b) x r
+    | Rd a y (Bk b z c) => Rd (lbal (makeRed a) y b) z (Bk c x r)
+    | _ => Rd l x r
+    end)
+  r
+  (rbalS l x r).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+(** ** Balancing for insertion *)
+
+Lemma lbal_spec l x r y :
+   InT y (lbal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case lbal_match; intuition_in.
+Qed.
+
+Instance lbal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (lbal l x r).
+Proof.
+ destruct (lbal_match l x r); ok.
+Qed.
+
+Lemma rbal_spec l x r y :
+   InT y (rbal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case rbal_match; intuition_in.
+Qed.
+
+Instance rbal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (rbal l x r).
+Proof.
+ destruct (rbal_match l x r); ok.
+Qed.
+
+Lemma rbal'_spec l x r y :
+   InT y (rbal' l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case rbal'_match; intuition_in.
+Qed.
+
+Instance rbal'_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (rbal' l x r).
+Proof.
+ destruct (rbal'_match l x r); ok.
+Qed.
+
+Hint Rewrite In_node_iff In_leaf_iff
+ makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb.
+
+Ltac descolor := destruct_all Color.t.
+Ltac destree t := destruct t as [|[|] ? ? ?].
+Ltac autorew := autorewrite with rb.
+Tactic Notation "autorew" "in" ident(H) := autorewrite with rb in H.
+
+(** ** Insertion *)
+
+Lemma ins_spec : forall s x y,
+ InT y (ins x s) <-> X.eq y x \/ InT y s.
+Proof.
+ induct s x.
+ - intuition_in.
+ - intuition_in. setoid_replace y with x; eauto.
+ - descolor; autorew; rewrite IHl; intuition_in.
+ - descolor; autorew; rewrite IHr; intuition_in.
+Qed.
+Hint Rewrite ins_spec : rb.
+
+Instance ins_ok s x `{Ok s} : Ok (ins x s).
+Proof.
+ induct s x; auto; descolor;
+ (apply lbal_ok || apply rbal_ok || ok); auto;
+ intros y; autorew; intuition; order.
+Qed.
+
+Lemma add_spec' s x y :
+ InT y (add x s) <-> X.eq y x \/ InT y s.
+Proof.
+ unfold add. now autorew.
+Qed.
+
+Hint Rewrite add_spec' : rb.
+
+Lemma add_spec s x y `{Ok s} :
+ InT y (add x s) <-> X.eq y x \/ InT y s.
+Proof.
+ apply add_spec'.
+Qed.
+
+Instance add_ok s x `{Ok s} : Ok (add x s).
+Proof.
+ unfold add; auto_tc.
+Qed.
+
+(** ** Balancing for deletion *)
+
+Lemma lbalS_spec l x r y :
+  InT y (lbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case lbalS_match.
+ - intros; autorew; intuition_in.
+ - clear l. intros l _.
+   destruct r as [|[|] rl rx rr].
+   * autorew. intuition_in.
+   * destree rl; autorew; intuition_in.
+   * autorew. intuition_in.
+Qed.
+
+Instance lbalS_ok l x r :
+ forall `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (lbalS l x r).
+Proof.
+ case lbalS_match; intros.
+ - ok.
+ - destruct r as [|[|] rl rx rr].
+   * ok.
+   * destruct rl as [|[|] rll rlx rlr]; intros; ok.
+     + apply rbal'_ok; ok.
+       intros w; autorew; auto.
+     + intros w; autorew.
+       destruct 1 as [Hw|[Hw|Hw]]; try rewrite Hw; eauto.
+   * ok. autorew. apply rbal'_ok; ok.
+Qed.
+
+Lemma rbalS_spec l x r y :
+  InT y (rbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case rbalS_match.
+ - intros; autorew; intuition_in.
+ - intros t _.
+   destruct l as [|[|] ll lx lr].
+   * autorew. intuition_in.
+   * destruct lr as [|[|] lrl lrx lrr]; autorew; intuition_in.
+   * autorew. intuition_in.
+Qed.
+
+Instance rbalS_ok l x r :
+ forall `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (rbalS l x r).
+Proof.
+ case rbalS_match; intros.
+ - ok.
+ - destruct l as [|[|] ll lx lr].
+   * ok.
+   * destruct lr as [|[|] lrl lrx lrr]; intros; ok.
+     + apply lbal_ok; ok.
+       intros w; autorew; auto.
+     + intros w; autorew.
+       destruct 1 as [Hw|[Hw|Hw]]; try rewrite Hw; eauto.
+   * ok. apply lbal_ok; ok.
+Qed.
+
+Hint Rewrite lbalS_spec rbalS_spec : rb.
+
+(** ** Append for deletion *)
+
+Ltac append_tac l r :=
+ induction l as [| lc ll _ lx lr IHlr];
+ [intro r; simpl
+ |induction r as [| rc rl IHrl rx rr _];
+   [simpl
+   |destruct lc, rc;
+     [specialize (IHlr rl); clear IHrl
+     |simpl;
+      assert (Hr:notred (Bk rl rx rr)) by (simpl; trivial);
+      set (r:=Bk rl rx rr) in *; clearbody r; clear IHrl rl rx rr;
+      specialize (IHlr r)
+     |change (append _ _) with (Rd (append (Bk ll lx lr) rl) rx rr);
+      assert (Hl:notred (Bk ll lx lr)) by (simpl; trivial);
+      set (l:=Bk ll lx lr) in *; clearbody l; clear IHlr ll lx lr
+     |specialize (IHlr rl); clear IHrl]]].
+
+Fact append_rr_match ll lx lr rl rx rr :
+ rspec
+  (fun a x b => Rd (Rd ll lx a) x (Rd b rx rr))
+  (fun t => Rd ll lx (Rd t rx rr))
+  (append lr rl)
+  (append (Rd ll lx lr) (Rd rl rx rr)).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+Fact append_bb_match ll lx lr rl rx rr :
+ rspec
+  (fun a x b => Rd (Bk ll lx a) x (Bk b rx rr))
+  (fun t => lbalS ll lx (Bk t rx rr))
+  (append lr rl)
+  (append (Bk ll lx lr) (Bk rl rx rr)).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+Lemma append_spec l r x :
+ InT x (append l r) <-> InT x l \/ InT x r.
+Proof.
+ revert r.
+ append_tac l r; autorew; try tauto.
+ - (* Red / Red *)
+   revert IHlr; case append_rr_match;
+    [intros a y b | intros t Ht]; autorew; tauto.
+ - (* Black / Black *)
+   revert IHlr; case append_bb_match;
+    [intros a y b | intros t Ht]; autorew; tauto.
+Qed.
+
+Hint Rewrite append_spec : rb.
+
+Lemma append_ok : forall x l r `{Ok l, Ok r},
+ lt_tree x l -> gt_tree x r -> Ok (append l r).
+Proof.
+ append_tac l r.
+ - (* Leaf / _ *)
+   trivial.
+ - (* _ / Leaf *)
+   trivial.
+ - (* Red / Red *)
+   intros; inv.
+   assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr.
+   assert (X.lt lx rx) by (transitivity x; eauto).
+   assert (G : gt_tree lx (append lr rl)).
+    { intros w. autorew. destruct 1; [|transitivity x]; eauto. }
+   assert (L : lt_tree rx (append lr rl)).
+    { intros w. autorew. destruct 1; [transitivity x|]; eauto. }
+   revert IH G L; case append_rr_match; intros; ok.
+ - (* Red / Black *)
+   intros; ok.
+   intros w; autorew; destruct 1; eauto.
+ - (* Black / Red *)
+   intros; ok.
+   intros w; autorew; destruct 1; eauto.
+ - (* Black / Black *)
+   intros; inv.
+   assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr.
+   assert (X.lt lx rx) by (transitivity x; eauto).
+   assert (G : gt_tree lx (append lr rl)).
+    { intros w. autorew. destruct 1; [|transitivity x]; eauto. }
+   assert (L : lt_tree rx (append lr rl)).
+    { intros w. autorew. destruct 1; [transitivity x|]; eauto. }
+   revert IH G L; case append_bb_match; intros; ok.
+    apply lbalS_ok; ok.
+Qed.
+
+(** ** Deletion *)
+
+Lemma del_spec : forall s x y `{Ok s},
+ InT y (del x s) <-> InT y s /\ ~X.eq y x.
+Proof.
+induct s x.
+- intuition_in.
+- autorew; intuition_in.
+  assert (X.lt y x') by eauto. order.
+  assert (X.lt x' y) by eauto. order.
+  order.
+- destruct l as [|[|] ll lx lr]; autorew;
+  rewrite ?IHl by trivial; intuition_in; order.
+- destruct r as [|[|] rl rx rr]; autorew;
+  rewrite ?IHr by trivial; intuition_in; order.
+Qed.
+
+Hint Rewrite del_spec : rb.
+
+Instance del_ok s x `{Ok s} : Ok (del x s).
+Proof.
+induct s x.
+- trivial.
+- eapply append_ok; eauto.
+- assert (lt_tree x' (del x l)).
+  { intro w. autorew; trivial. destruct 1. eauto. }
+  destruct l as [|[|] ll lx lr]; auto_tc.
+- assert (gt_tree x' (del x r)).
+  { intro w. autorew; trivial. destruct 1. eauto. }
+  destruct r as [|[|] rl rx rr]; auto_tc.
+Qed.
+
+Lemma remove_spec s x y `{Ok s} :
+ InT y (remove x s) <-> InT y s /\ ~X.eq y x.
+Proof.
+unfold remove. now autorew.
+Qed.
+
+Hint Rewrite remove_spec : rb.
+
+Instance remove_ok s x `{Ok s} : Ok (remove x s).
+Proof.
+unfold remove; auto_tc.
+Qed.
+
+(** ** Removing the minimal element *)
+
+Lemma delmin_spec l y r c x s' `{O : Ok (Node c l y r)} :
+ delmin l y r = (x,s') ->
+  min_elt (Node c l y r) = Some x /\ del x (Node c l y r) = s'.
+Proof.
+ revert y r c x s' O.
+ induction l as [|lc ll IH ly lr _].
+ - simpl. intros y r _ x s' _. injection 1; intros; subst.
+   now rewrite MX.compare_refl.
+ - intros y r c x s' O.
+   simpl delmin.
+   specialize (IH ly lr). destruct delmin as (x0,s0).
+   destruct (IH lc x0 s0); clear IH; [ok|trivial|].
+   remember (Node lc ll ly lr) as l.
+   simpl min_elt in *.
+   intros E.
+   replace x0 with x in * by (destruct lc; now injection E).
+   split.
+   * subst l; intuition.
+   * assert (X.lt x y).
+     { inversion_clear O.
+       assert (InT x l) by now apply min_elt_spec1. auto. }
+     simpl. case X.compare_spec; try order.
+     destruct lc; injection E; clear E; intros; subst l s0; auto.
+Qed.
+
+Lemma remove_min_spec1 s x s' `{Ok s}:
+ remove_min s = Some (x,s') ->
+  min_elt s = Some x /\ remove x s = s'.
+Proof.
+ unfold remove_min.
+ destruct s as [|c l y r]; try easy.
+ generalize (delmin_spec l y r c).
+ destruct delmin as (x0,s0). intros D.
+ destruct (D x0 s0) as (->,<-); auto.
+ fold (remove x0 (Node c l y r)).
+ inversion_clear 1; auto.
+Qed.
+
+Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
+Proof.
+ unfold remove_min.
+ destruct s as [|c l y r].
+ - easy.
+ - now destruct delmin.
+Qed.
+
+Lemma remove_min_ok (s:t) `{Ok s}:
+ match remove_min s with
+ | Some (_,s') => Ok s'
+ | None => True
+ end.
+Proof.
+ generalize (remove_min_spec1 s).
+ destruct remove_min as [(x0,s0)|]; auto.
+ intros R. destruct (R x0 s0); auto. subst s0. auto_tc.
+Qed.
+
+(** ** Treeify *)
+
+Notation ifpred p n := (if p then pred n else n%nat).
+
+Definition treeify_invariant size (f:treeify_t) :=
+ forall acc,
+ size <= length acc ->
+ let (t,acc') := f acc in
+ cardinal t = size /\ acc = elements t ++ acc'.
+
+Lemma treeify_zero_spec : treeify_invariant 0 treeify_zero.
+Proof.
+ intro. simpl. auto.
+Qed.
+
+Lemma treeify_one_spec : treeify_invariant 1 treeify_one.
+Proof.
+ intros [|x acc]; simpl; auto; inversion 1.
+Qed.
+
+Lemma treeify_cont_spec f g size1 size2 size :
+ treeify_invariant size1 f ->
+ treeify_invariant size2 g ->
+ size = S (size1 + size2) ->
+ treeify_invariant size (treeify_cont f g).
+Proof.
+ intros Hf Hg EQ acc LE. unfold treeify_cont.
+ specialize (Hf acc).
+ destruct (f acc) as (t1,acc1).
+ destruct Hf as (Hf1,Hf2).
+  { lia. }
+ destruct acc1 as [|x acc1].
+  { exfalso. subst acc.
+    rewrite <- app_nil_end, <- elements_cardinal in LE. lia. }
+ specialize (Hg acc1).
+ destruct (g acc1) as (t2,acc2).
+ destruct Hg as (Hg1,Hg2).
+  { subst acc. rewrite app_length, <- elements_cardinal in LE.
+    simpl in LE. unfold elt in *. lia. }
+ simpl. split.
+ * lia.
+ * rewrite elements_node, app_ass. simpl. unfold elt in *; congruence.
+Qed.
+
+Lemma treeify_aux_spec n (p:bool) :
+ treeify_invariant (ifpred p (Pos.to_nat n)) (treeify_aux p n).
+Proof.
+ revert p.
+ induction n as [n|n|]; intros p; simpl treeify_aux.
+ - eapply treeify_cont_spec; [ apply (IHn false) | apply (IHn p) | ].
+   rewrite Pos2Nat.inj_xI. generalize (Pos2Nat.is_pos n).
+   destruct p; simpl; lia.
+ - eapply treeify_cont_spec; [ apply (IHn p) | apply (IHn true) | ].
+   rewrite Pos2Nat.inj_xO. generalize (Pos2Nat.is_pos n).
+   destruct p; simpl; lia.
+ - destruct p; [ apply treeify_zero_spec | apply treeify_one_spec ].
+Qed.
+
+Lemma plength_spec l : Pos.to_nat (plength l) = S (length l).
+Proof.
+ induction l; simpl; now rewrite ?Pos2Nat.inj_succ, ?IHl.
+Qed.
+
+Lemma treeify_elements l : elements (treeify l) = l.
+Proof.
+ assert (H := treeify_aux_spec (plength l) true l).
+ unfold treeify. destruct treeify_aux as (t,acc); simpl in *.
+ destruct H as (H,H'). { now rewrite plength_spec. }
+ subst l. rewrite plength_spec, app_length, <- elements_cardinal in *.
+ destruct acc.
+ * now rewrite app_nil_r.
+ * simpl in H. lia.
+Qed.
+
+Lemma treeify_spec x l : InT x (treeify l) <-> InA X.eq x l.
+Proof.
+ intros. now rewrite <- elements_spec1, treeify_elements.
+Qed.
+
+Lemma treeify_ok l : sort X.lt l -> Ok (treeify l).
+Proof.
+ intros. apply elements_sort_ok. rewrite treeify_elements; auto.
+Qed.
+
+
+(** ** Filter *)
+
+Lemma filter_app A f (l l':list A) :
+ List.filter f (l ++ l') = List.filter f l ++ List.filter f l'.
+Proof.
+ induction l as [|x l IH]; simpl; trivial.
+ destruct (f x); simpl; now rewrite IH.
+Qed.
+
+Lemma filter_aux_elements s f acc :
+ filter_aux f s acc = List.filter f (elements s) ++ acc.
+Proof.
+ revert acc.
+ induction s as [|c l IHl x r IHr]; simpl; trivial.
+ intros acc.
+ rewrite elements_node, filter_app. simpl.
+ destruct (f x); now rewrite IHl, IHr, app_ass.
+Qed.
+
+Lemma filter_elements s f :
+ elements (filter f s) = List.filter f (elements s).
+Proof.
+ unfold filter.
+ now rewrite treeify_elements, filter_aux_elements, app_nil_r.
+Qed.
+
+Lemma filter_spec s x f :
+ Proper (X.eq==>Logic.eq) f ->
+ (InT x (filter f s) <-> InT x s /\ f x = true).
+Proof.
+ intros Hf.
+ rewrite <- elements_spec1, filter_elements, filter_InA, elements_spec1;
+  now auto_tc.
+Qed.
+
+Instance filter_ok s f `(Ok s) : Ok (filter f s).
+Proof.
+ apply elements_sort_ok.
+ rewrite filter_elements.
+ apply filter_sort with X.eq; auto_tc.
+Qed.
+
+(** ** Partition *)
+
+Lemma partition_aux_spec s f acc1 acc2 :
+ partition_aux f s acc1 acc2 =
+  (filter_aux f s acc1, filter_aux (fun x => negb (f x)) s acc2).
+Proof.
+ revert acc1 acc2.
+ induction s as [ | c l Hl x r Hr ]; simpl.
+ - trivial.
+ - intros acc1 acc2.
+   destruct (f x); simpl; now rewrite Hr, Hl.
+Qed.
+
+Lemma partition_spec s f :
+ partition f s = (filter f s, filter (fun x => negb (f x)) s).
+Proof.
+ unfold partition, filter. now rewrite partition_aux_spec.
+Qed.
+
+Lemma partition_spec1 s f :
+ Proper (X.eq==>Logic.eq) f ->
+ Equal (fst (partition f s)) (filter f s).
+Proof. now rewrite partition_spec. Qed.
+
+Lemma partition_spec2 s f :
+ Proper (X.eq==>Logic.eq) f ->
+ Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+Proof. now rewrite partition_spec. Qed.
+
+Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+Proof. rewrite partition_spec; now apply filter_ok. Qed.
+
+Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+Proof. rewrite partition_spec; now apply filter_ok. Qed.
+
+
+(** ** An invariant for binary list functions with accumulator. *)
+
+Ltac inA :=
+ rewrite ?InA_app_iff, ?InA_cons, ?InA_nil, ?InA_rev in *; auto_tc.
+
+Record INV l1 l2 acc : Prop := {
+ l1_sorted : sort X.lt (rev l1);
+ l2_sorted : sort X.lt (rev l2);
+ acc_sorted : sort X.lt acc;
+ l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y;
+ l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}.
+Local Hint Resolve l1_sorted l2_sorted acc_sorted.
+
+Lemma INV_init s1 s2 `(Ok s1, Ok s2) :
+ INV (rev_elements s1) (rev_elements s2) nil.
+Proof.
+ rewrite !rev_elements_rev.
+ split; rewrite ?rev_involutive; auto; intros; now inA.
+Qed.
+
+Lemma INV_sym l1 l2 acc : INV l1 l2 acc -> INV l2 l1 acc.
+Proof.
+ destruct 1; now split.
+Qed.
+
+Lemma INV_drop x1 l1 l2 acc :
+  INV (x1 :: l1) l2 acc -> INV l1 l2 acc.
+Proof.
+ intros (l1s,l2s,accs,l1a,l2a). simpl in *.
+ destruct (sorted_app_inv _ _ l1s) as (U & V & W); auto.
+ split; auto.
+Qed.
+
+Lemma INV_eq x1 x2 l1 l2 acc :
+  INV (x1 :: l1) (x2 :: l2) acc -> X.eq x1 x2 ->
+  INV l1 l2 (x1 :: acc).
+Proof.
+ intros (U,V,W,X,Y) EQ. simpl in *.
+ destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+ destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+ split; auto.
+ - constructor; auto. apply InA_InfA with X.eq; auto_tc.
+ - intros x y; inA; intros Hx [Hy|Hy].
+   + apply U3; inA.
+   + apply X; inA.
+ - intros x y; inA; intros Hx [Hy|Hy].
+   + rewrite Hy, EQ; apply V3; inA.
+   + apply Y; inA.
+Qed.
+
+Lemma INV_lt x1 x2 l1 l2 acc :
+  INV (x1 :: l1) (x2 :: l2) acc -> X.lt x1 x2 ->
+  INV (x1 :: l1) l2 (x2 :: acc).
+Proof.
+ intros (U,V,W,X,Y) EQ. simpl in *.
+ destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+ destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+ split; auto.
+ - constructor; auto. apply InA_InfA with X.eq; auto_tc.
+ - intros x y; inA; intros Hx [Hy|Hy].
+   + rewrite Hy; clear Hy. destruct Hx; [order|].
+     transitivity x1; auto. apply U3; inA.
+   + apply X; inA.
+ - intros x y; inA; intros Hx [Hy|Hy].
+   + rewrite Hy. apply V3; inA.
+   + apply Y; inA.
+Qed.
+
+Lemma INV_rev l1 l2 acc :
+ INV l1 l2 acc -> Sorted X.lt (rev_append l1 acc).
+Proof.
+ intros. rewrite rev_append_rev.
+ apply SortA_app with X.eq; eauto with *.
+ intros x y. inA. eapply l1_lt_acc; eauto.
+Qed.
+
+(** ** union *)
+
+Lemma union_list_ok l1 l2 acc :
+ INV l1 l2 acc -> sort X.lt (union_list l1 l2 acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1];
+  [intro l2|induction l2 as [|x2 l2 IH2]];
+   intros acc inv.
+ - eapply INV_rev, INV_sym; eauto.
+ - eapply INV_rev; eauto.
+ - simpl. case X.compare_spec; intro C.
+   * apply IH1. eapply INV_eq; eauto.
+   * apply (IH2 (x2::acc)). eapply INV_lt; eauto.
+   * apply IH1. eapply INV_sym, INV_lt; eauto. now apply INV_sym.
+Qed.
+
+Instance linear_union_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (linear_union s1 s2).
+Proof.
+ unfold linear_union. now apply treeify_ok, union_list_ok, INV_init.
+Qed.
+
+Instance fold_add_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (fold add s1 s2).
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2).
+Proof.
+ unfold union. destruct compare_height; auto_tc.
+Qed.
+
+Lemma union_list_spec x l1 l2 acc :
+ InA X.eq x (union_list l1 l2 acc) <->
+  InA X.eq x l1 \/ InA X.eq x l2 \/ InA X.eq x acc.
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1].
+ - intros l2 acc; simpl. rewrite rev_append_rev. inA. tauto.
+ - induction l2 as [|x2 l2 IH2]; intros acc; simpl.
+   * rewrite rev_append_rev. inA. tauto.
+   * case X.compare_spec; intro C.
+     + rewrite IH1, !InA_cons, C; tauto.
+     + rewrite (IH2 (x2::acc)), !InA_cons. tauto.
+     + rewrite IH1, !InA_cons; tauto.
+Qed.
+
+Lemma linear_union_spec s1 s2 x :
+ InT x (linear_union s1 s2) <-> InT x s1 \/ InT x s2.
+Proof.
+ unfold linear_union.
+ rewrite treeify_spec, union_list_spec, !rev_elements_rev.
+ rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc.
+ tauto.
+Qed.
+
+Lemma fold_add_spec s1 s2 x :
+ InT x (fold add s1 s2) <-> InT x s1 \/ InT x s2.
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl.
+ - rewrite InA_nil. tauto.
+ - unfold flip. rewrite add_spec', IHl, InA_cons. tauto.
+Qed.
+
+Lemma union_spec' s1 s2 x :
+ InT x (union s1 s2) <-> InT x s1 \/ InT x s2.
+Proof.
+ unfold union. destruct compare_height.
+ - apply linear_union_spec.
+ - apply fold_add_spec.
+ - rewrite fold_add_spec. tauto.
+Qed.
+
+Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2},
+ (InT y (union s1 s2) <-> InT y s1 \/ InT y s2).
+Proof.
+ intros; apply union_spec'.
+Qed.
+
+(** ** inter *)
+
+Lemma inter_list_ok l1 l2 acc :
+ INV l1 l2 acc -> sort X.lt (inter_list l1 l2 acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1]; [|induction l2 as [|x2 l2 IH2]]; simpl.
+ - eauto.
+ - eauto.
+ - intros acc inv.
+   case X.compare_spec; intro C.
+   * apply IH1. eapply INV_eq; eauto.
+   * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto.
+   * apply IH1. eapply INV_drop; eauto.
+Qed.
+
+Instance linear_inter_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (linear_inter s1 s2).
+Proof.
+ unfold linear_inter. now apply treeify_ok, inter_list_ok, INV_init.
+Qed.
+
+Instance inter_ok s1 s2 `(Ok s1, Ok s2) : Ok (inter s1 s2).
+Proof.
+ unfold inter. destruct compare_height; auto_tc.
+Qed.
+
+Lemma inter_list_spec x l1 l2 acc :
+ sort X.lt (rev l1) ->
+ sort X.lt (rev l2) ->
+ (InA X.eq x (inter_list l1 l2 acc) <->
+   (InA X.eq x l1 /\ InA X.eq x l2) \/ InA X.eq x acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1].
+ - intros l2 acc; simpl. inA. tauto.
+ - induction l2 as [|x2 l2 IH2]; intros acc.
+   * simpl. inA. tauto.
+   * simpl. intros U V.
+     destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+     destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+     case X.compare_spec; intro C.
+     + rewrite IH1, !InA_cons, C; tauto.
+     + rewrite (IH2 acc); auto. inA. intuition; try order.
+       assert (X.lt x x1) by (apply U3; inA). order.
+     + rewrite IH1; auto. inA. intuition; try order.
+       assert (X.lt x x2) by (apply V3; inA). order.
+Qed.
+
+Lemma linear_inter_spec s1 s2 x `(Ok s1, Ok s2) :
+ InT x (linear_inter s1 s2) <-> InT x s1 /\ InT x s2.
+Proof.
+ unfold linear_inter.
+ rewrite !rev_elements_rev, treeify_spec, inter_list_spec
+  by (rewrite rev_involutive; auto_tc).
+ rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.
+Qed.
+
+Local Instance mem_proper s `(Ok s) :
+ Proper (X.eq ==> Logic.eq) (fun k => mem k s).
+Proof.
+ intros x y EQ. apply Bool.eq_iff_eq_true; rewrite !mem_spec; auto.
+ now rewrite EQ.
+Qed.
+
+Lemma inter_spec s1 s2 y `{Ok s1, Ok s2} :
+ InT y (inter s1 s2) <-> InT y s1 /\ InT y s2.
+Proof.
+ unfold inter. destruct compare_height.
+ - now apply linear_inter_spec.
+ - rewrite filter_spec, mem_spec by auto_tc; tauto.
+ - rewrite filter_spec, mem_spec by auto_tc; tauto.
+Qed.
+
+(** ** difference *)
+
+Lemma diff_list_ok l1 l2 acc :
+ INV l1 l2 acc -> sort X.lt (diff_list l1 l2 acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1];
+  [intro l2|induction l2 as [|x2 l2 IH2]];
+    intros acc inv.
+ - eauto.
+ - unfold diff_list. eapply INV_rev; eauto.
+ - simpl. case X.compare_spec; intro C.
+   * apply IH1. eapply INV_drop, INV_sym, INV_drop, INV_sym; eauto.
+   * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto.
+   * apply IH1. eapply INV_sym, INV_lt; eauto. now apply INV_sym.
+Qed.
+
+Instance diff_inter_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (linear_diff s1 s2).
+Proof.
+ unfold linear_inter. now apply treeify_ok, diff_list_ok, INV_init.
+Qed.
+
+Instance fold_remove_ok s1 s2 `(Ok s2) :
+ Ok (fold remove s1 s2).
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Instance diff_ok s1 s2 `(Ok s1, Ok s2) : Ok (diff s1 s2).
+Proof.
+ unfold diff. destruct compare_height; auto_tc.
+Qed.
+
+Lemma diff_list_spec x l1 l2 acc :
+ sort X.lt (rev l1) ->
+ sort X.lt (rev l2) ->
+ (InA X.eq x (diff_list l1 l2 acc) <->
+   (InA X.eq x l1 /\ ~InA X.eq x l2) \/ InA X.eq x acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1].
+ - intros l2 acc; simpl. inA. tauto.
+ - induction l2 as [|x2 l2 IH2]; intros acc.
+   * intros; simpl. rewrite rev_append_rev. inA. tauto.
+   * simpl. intros U V.
+     destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+     destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+     case X.compare_spec; intro C.
+     + rewrite IH1; auto. f_equiv. inA. intuition; try order.
+       assert (X.lt x x1) by (apply U3; inA). order.
+     + rewrite (IH2 acc); auto. f_equiv. inA. intuition; try order.
+       assert (X.lt x x1) by (apply U3; inA). order.
+     + rewrite IH1; auto. inA. intuition; try order.
+       left; split; auto. destruct 1. order.
+       assert (X.lt x x2) by (apply V3; inA). order.
+Qed.
+
+Lemma linear_diff_spec s1 s2 x `(Ok s1, Ok s2) :
+ InT x (linear_diff s1 s2) <-> InT x s1 /\ ~InT x s2.
+Proof.
+ unfold linear_diff.
+ rewrite !rev_elements_rev, treeify_spec, diff_list_spec
+  by (rewrite rev_involutive; auto_tc).
+ rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.
+Qed.
+
+Lemma fold_remove_spec s1 s2 x `(Ok s2) :
+  InT x (fold remove s1 s2) <-> InT x s2 /\ ~InT x s1.
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl; intros.
+ - rewrite InA_nil. intuition.
+ - unfold flip in *. rewrite remove_spec, IHl, InA_cons. tauto.
+   clear IHl. induction l; simpl; auto_tc.
+Qed.
+
+Lemma diff_spec s1 s2 y `{Ok s1, Ok s2} :
+ InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2.
+Proof.
+ unfold diff. destruct compare_height.
+ - now apply linear_diff_spec.
+ - rewrite filter_spec, Bool.negb_true_iff,
+     <- Bool.not_true_iff_false, mem_spec;
+    intuition.
+    intros x1 x2 EQ. f_equal. now apply mem_proper.
+ - now apply fold_remove_spec.
+Qed.
+
+End MakeRaw.
+
+(** * Balancing properties
+
+    We now prove that all operations preserve a red-black invariant,
+    and that trees have hence a logarithmic depth.
+*)
+
+Module BalanceProps(X:Orders.OrderedType)(Import M : MakeRaw X).
+
+Local Notation Rd := (Node Red).
+Local Notation Bk := (Node Black).
+Import M.MX.
+
+(** ** Red-Black invariants *)
+
+(** In a red-black tree :
+    - a red node has no red children
+    - the black depth at each node is the same along all paths.
+    The black depth is here an argument of the predicate. *)
+
+Inductive rbt : nat -> tree -> Prop :=
+ | RB_Leaf : rbt 0 Leaf
+ | RB_Rd n l k r :
+   notred l -> notred r -> rbt n l -> rbt n r -> rbt n (Rd l k r)
+ | RB_Bk n l k r : rbt n l -> rbt n r -> rbt (S n) (Bk l k r).
+
+(** A red-red tree is almost a red-black tree, except that it has
+    a _red_ root node which _may_ have red children. Note that a
+    red-red tree is hence non-empty, and all its strict subtrees
+    are red-black. *)
+
+Inductive rrt (n:nat) : tree -> Prop :=
+ | RR_Rd l k r : rbt n l -> rbt n r -> rrt n (Rd l k r).
+
+(** An almost-red-black tree is almost a red-black tree, except that
+    it's permitted to have two red nodes in a row at the very root (only).
+    We implement this notion by saying that a quasi-red-black tree
+    is either a red-black tree or a red-red tree. *)
+
+Inductive arbt (n:nat)(t:tree) : Prop :=
+ | ARB_RB : rbt n t -> arbt n t
+ | ARB_RR : rrt n t -> arbt n t.
+
+(** The main exported invariant : being a red-black tree for some
+    black depth. *)
+
+Class Rbt (t:tree) :=  RBT : exists d, rbt d t.
+
+(** ** Basic tactics and results about red-black *)
+
+Scheme rbt_ind := Induction for rbt Sort Prop.
+Local Hint Constructors rbt rrt arbt.
+Local Hint Extern 0 (notred _) => (exact I).
+Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction.
+Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end.
+Ltac nonzero n := destruct n as [|n]; [try split; invrb|].
+
+Lemma rr_nrr_rb n t :
+ rrt n t -> notredred t -> rbt n t.
+Proof.
+ destruct 1 as [l x r Hl Hr].
+ destruct l, r; descolor; invrb; auto.
+Qed.
+
+Local Hint Resolve rr_nrr_rb.
+
+Lemma arb_nrr_rb n t :
+ arbt n t -> notredred t -> rbt n t.
+Proof.
+ destruct 1; auto.
+Qed.
+
+Lemma arb_nr_rb n t :
+ arbt n t -> notred t -> rbt n t.
+Proof.
+ destruct 1; destruct t; descolor; invrb; auto.
+Qed.
+
+Local Hint Resolve arb_nrr_rb arb_nr_rb.
+
+(** ** A Red-Black tree has indeed a logarithmic depth *)
+
+Definition redcarac s := rcase (fun _ _ _ => 1) (fun _ => 0) s.
+
+Lemma rb_maxdepth s n : rbt n s -> maxdepth s <= 2*n + redcarac s.
+Proof.
+ induction 1.
+ - simpl; auto.
+ - replace (redcarac l) with 0 in * by now destree l.
+   replace (redcarac r) with 0 in * by now destree r.
+   simpl maxdepth. simpl redcarac.
+   rewrite Nat.add_succ_r, <- Nat.succ_le_mono.
+   now apply Nat.max_lub.
+ - simpl. Nat.nzsimpl. rewrite <- Nat.succ_le_mono.
+   apply Nat.max_lub; eapply Nat.le_trans; eauto.
+   destree l; simpl; lia.
+   destree r; simpl; lia.
+Qed.
+
+Lemma rb_mindepth s n : rbt n s -> n + redcarac s <= mindepth s.
+Proof.
+ induction 1; simpl.
+ - trivial.
+ - rewrite Nat.add_succ_r.
+   apply -> Nat.succ_le_mono.
+   replace (redcarac l) with 0 in * by now destree l.
+   replace (redcarac r) with 0 in * by now destree r.
+   now apply Nat.min_glb.
+ - apply -> Nat.succ_le_mono. apply Nat.min_glb; lia.
+Qed.
+
+Lemma maxdepth_upperbound s : Rbt s ->
+ maxdepth s <= 2 * log2 (S (cardinal s)).
+Proof.
+ intros (n,H).
+ eapply Nat.le_trans; [eapply rb_maxdepth; eauto|].
+ generalize (rb_mindepth s n H).
+ generalize (mindepth_log_cardinal s). lia.
+Qed.
+
+Lemma maxdepth_lowerbound s : s<>Leaf ->
+ log2 (cardinal s) < maxdepth s.
+Proof.
+ apply maxdepth_log_cardinal.
+Qed.
+
+
+(** ** Singleton *)
+
+Lemma singleton_rb x : Rbt (singleton x).
+Proof.
+ unfold singleton. exists 1; auto.
+Qed.
+
+(** ** [makeBlack] and [makeRed] *)
+
+Lemma makeBlack_rb n t : arbt n t -> Rbt (makeBlack t).
+Proof.
+ destruct t as [|[|] l x r].
+ - exists 0; auto.
+ - destruct 1; invrb; exists (S n); simpl; auto.
+ - exists n; auto.
+Qed.
+
+Lemma makeRed_rr t n :
+ rbt (S n) t -> notred t -> rrt n (makeRed t).
+Proof.
+ destruct t as [|[|] l x r]; invrb; simpl; auto.
+Qed.
+
+(** ** Balancing *)
+
+Lemma lbal_rb n l k r :
+ arbt n l -> rbt n r -> rbt (S n) (lbal l k r).
+Proof.
+case lbal_match; intros; desarb; invrb; auto.
+Qed.
+
+Lemma rbal_rb n l k r :
+ rbt n l -> arbt n r -> rbt (S n) (rbal l k r).
+Proof.
+case rbal_match; intros; desarb; invrb; auto.
+Qed.
+
+Lemma rbal'_rb n l k r :
+ rbt n l -> arbt n r -> rbt (S n) (rbal' l k r).
+Proof.
+case rbal'_match; intros; desarb; invrb; auto.
+Qed.
+
+Lemma lbalS_rb n l x r :
+ arbt n l -> rbt (S n) r -> notred r -> rbt (S n) (lbalS l x r).
+Proof.
+ intros Hl Hr Hr'.
+ destruct r as [|[|] rl rx rr]; invrb. clear Hr'.
+ revert Hl.
+ case lbalS_match.
+ - destruct 1; invrb; auto.
+ - intros. apply rbal'_rb; auto.
+Qed.
+
+Lemma lbalS_arb n l x r :
+ arbt n l -> rbt (S n) r -> arbt (S n) (lbalS l x r).
+Proof.
+ case lbalS_match.
+ - destruct 1; invrb; auto.
+ - clear l. intros l Hl Hl' Hr.
+   destruct r as [|[|] rl rx rr]; invrb.
+   * destruct rl as [|[|] rll rlx rlr]; invrb.
+     right; auto using rbal'_rb, makeRed_rr.
+   * left; apply rbal'_rb; auto.
+Qed.
+
+Lemma rbalS_rb n l x r :
+ rbt (S n) l -> notred l -> arbt n r -> rbt (S n) (rbalS l x r).
+Proof.
+ intros Hl Hl' Hr.
+ destruct l as [|[|] ll lx lr]; invrb. clear Hl'.
+ revert Hr.
+ case rbalS_match.
+ - destruct 1; invrb; auto.
+ - intros. apply lbal_rb; auto.
+Qed.
+
+Lemma rbalS_arb n l x r :
+ rbt (S n) l -> arbt n r -> arbt (S n) (rbalS l x r).
+Proof.
+ case rbalS_match.
+ - destruct 2; invrb; auto.
+ - clear r. intros r Hr Hr' Hl.
+   destruct l as [|[|] ll lx lr]; invrb.
+   * destruct lr as [|[|] lrl lrx lrr]; invrb.
+     right; auto using lbal_rb, makeRed_rr.
+   * left; apply lbal_rb; auto.
+Qed.
+
+
+(** ** Insertion *)
+
+(** The next lemmas combine simultaneous results about rbt and arbt.
+    A first solution here: statement with [if ... then ... else] *)
+
+Definition ifred s (A B:Prop) := rcase (fun _ _ _ => A) (fun _ => B) s.
+
+Lemma ifred_notred s A B : notred s -> (ifred s A B <-> B).
+Proof.
+ destruct s; descolor; simpl; intuition.
+Qed.
+
+Lemma ifred_or s A B : ifred s A B -> A\/B.
+Proof.
+ destruct s; descolor; simpl; intuition.
+Qed.
+
+Lemma ins_rr_rb x s n : rbt n s ->
+ ifred s (rrt n (ins x s)) (rbt n (ins x s)).
+Proof.
+induction 1 as [ | n l k r | n l k r Hl IHl Hr IHr ].
+- simpl; auto.
+- simpl. rewrite ifred_notred in * by trivial.
+  elim_compare x k; auto.
+- rewrite ifred_notred by trivial.
+  unfold ins; fold ins. (* simpl is too much here ... *)
+  elim_compare x k.
+  * auto.
+  * apply lbal_rb; trivial. apply ifred_or in IHl; intuition.
+  * apply rbal_rb; trivial. apply ifred_or in IHr; intuition.
+Qed.
+
+Lemma ins_arb x s n : rbt n s -> arbt n (ins x s).
+Proof.
+ intros H. apply (ins_rr_rb x), ifred_or in H. intuition.
+Qed.
+
+Instance add_rb x s : Rbt s -> Rbt (add x s).
+Proof.
+ intros (n,H). unfold add. now apply (makeBlack_rb n), ins_arb.
+Qed.
+
+(** ** Deletion *)
+
+(** A second approach here: statement with ... /\ ... *)
+
+Lemma append_arb_rb n l r : rbt n l -> rbt n r ->
+ (arbt n (append l r)) /\
+ (notred l -> notred r -> rbt n (append l r)).
+Proof.
+revert r n.
+append_tac l r.
+- split; auto.
+- split; auto.
+- (* Red / Red *)
+  intros n. invrb.
+  case (IHlr n); auto; clear IHlr.
+  case append_rr_match.
+  + intros a x b _ H; split; invrb.
+    assert (rbt n (Rd a x b)) by auto. invrb. auto.
+  + split; invrb; auto.
+- (* Red / Black *)
+  split; invrb. destruct (IHlr n) as (_,IH); auto.
+- (* Black / Red *)
+  split; invrb. destruct (IHrl n) as (_,IH); auto.
+- (* Black / Black *)
+  nonzero n.
+  invrb.
+  destruct (IHlr n) as (IH,_); auto; clear IHlr.
+  revert IH.
+  case append_bb_match.
+  + intros a x b IH; split; destruct IH; invrb; auto.
+  + split; [left | invrb]; auto using lbalS_rb.
+Qed.
+
+(** A third approach : Lemma ... with ... *)
+
+Lemma del_arb s x n : rbt (S n) s -> isblack s -> arbt n (del x s)
+with del_rb s x n : rbt n s -> notblack s -> rbt n (del x s).
+Proof.
+{ revert n.
+  induct s x; try destruct c; try contradiction; invrb.
+  - apply append_arb_rb; assumption.
+  - assert (IHl' := del_rb l x). clear IHr del_arb del_rb.
+    destruct l as [|[|] ll lx lr]; auto.
+    nonzero n. apply lbalS_arb; auto.
+  - assert (IHr' := del_rb r x). clear IHl del_arb del_rb.
+    destruct r as [|[|] rl rx rr]; auto.
+    nonzero n. apply rbalS_arb; auto. }
+{ revert n.
+  induct s x; try assumption; try destruct c; try contradiction; invrb.
+  - apply append_arb_rb; assumption.
+  - assert (IHl' := del_arb l x). clear IHr del_arb del_rb.
+    destruct l as [|[|] ll lx lr]; auto.
+    nonzero n. destruct n as [|n]; [invrb|]; apply lbalS_rb; auto.
+  - assert (IHr' := del_arb r x). clear IHl del_arb del_rb.
+    destruct r as [|[|] rl rx rr]; auto.
+    nonzero n. apply rbalS_rb; auto. }
+Qed.
+
+Instance remove_rb s x : Rbt s -> Rbt (remove x s).
+Proof.
+ intros (n,H). unfold remove.
+ destruct s as [|[|] l y r].
+ - apply (makeBlack_rb n). auto.
+ - apply (makeBlack_rb n). left. apply del_rb; simpl; auto.
+ - nonzero n. apply (makeBlack_rb n). apply del_arb; simpl; auto.
+Qed.
+
+(** ** Treeify *)
+
+Definition treeify_rb_invariant size depth (f:treeify_t) :=
+ forall acc,
+ size <= length acc ->
+  rbt depth (fst (f acc)) /\
+  size + length (snd (f acc)) = length acc.
+
+Lemma treeify_zero_rb : treeify_rb_invariant 0 0 treeify_zero.
+Proof.
+ intros acc _; simpl; auto.
+Qed.
+
+Lemma treeify_one_rb : treeify_rb_invariant 1 0 treeify_one.
+Proof.
+ intros [|x acc]; simpl; auto; inversion 1.
+Qed.
+
+Lemma treeify_cont_rb f g size1 size2 size d :
+ treeify_rb_invariant size1 d f ->
+ treeify_rb_invariant size2 d g ->
+ size = S (size1 + size2) ->
+ treeify_rb_invariant size (S d) (treeify_cont f g).
+Proof.
+ intros Hf Hg H acc Hacc.
+ unfold treeify_cont.
+ specialize (Hf acc).
+ destruct (f acc) as (l, acc1). simpl in *.
+ destruct Hf as (Hf1, Hf2). { lia. }
+ destruct acc1 as [|x acc2]; simpl in *. { lia. }
+ specialize (Hg acc2).
+ destruct (g acc2) as (r, acc3). simpl in *.
+ destruct Hg as (Hg1, Hg2). { lia. }
+ split; [auto | lia].
+Qed.
+
+Lemma treeify_aux_rb n :
+ exists d, forall (b:bool),
+  treeify_rb_invariant (ifpred b (Pos.to_nat n)) d (treeify_aux b n).
+Proof.
+ induction n as [n (d,IHn)|n (d,IHn)| ].
+ - exists (S d). intros b.
+   eapply treeify_cont_rb; [ apply (IHn false) | apply (IHn b) | ].
+   rewrite Pos2Nat.inj_xI. generalize (Pos2Nat.is_pos n).
+   destruct b; simpl; lia.
+ - exists (S d). intros b.
+   eapply treeify_cont_rb; [ apply (IHn b) | apply (IHn true) | ].
+   rewrite Pos2Nat.inj_xO. generalize (Pos2Nat.is_pos n).
+   destruct b; simpl; lia.
+ - exists 0; destruct b;
+    [ apply treeify_zero_rb | apply treeify_one_rb ].
+Qed.
+
+(** The black depth of [treeify l] is actually a log2, but
+    we don't need to mention that. *)
+
+Instance treeify_rb l : Rbt (treeify l).
+Proof.
+ unfold treeify.
+ destruct (treeify_aux_rb (plength l)) as (d,H).
+ exists d.
+ apply H.
+ now rewrite plength_spec.
+Qed.
+
+(** ** Filtering *)
+
+Instance filter_rb f s : Rbt (filter f s).
+Proof.
+ unfold filter; auto_tc.
+Qed.
+
+Instance partition_rb1 f s : Rbt (fst (partition f s)).
+Proof.
+ unfold partition. destruct partition_aux. simpl. auto_tc.
+Qed.
+
+Instance partition_rb2 f s : Rbt (snd (partition f s)).
+Proof.
+ unfold partition. destruct partition_aux. simpl. auto_tc.
+Qed.
+
+(** ** Union, intersection, difference *)
+
+Instance fold_add_rb s1 s2 : Rbt s2 -> Rbt (fold add s1 s2).
+Proof.
+ intros. rewrite fold_spec, <- fold_left_rev_right. unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Instance fold_remove_rb s1 s2 : Rbt s2 -> Rbt (fold remove s1 s2).
+Proof.
+ intros. rewrite fold_spec, <- fold_left_rev_right. unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Lemma union_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (union s1 s2).
+Proof.
+ intros. unfold union, linear_union. destruct compare_height; auto_tc.
+Qed.
+
+Lemma inter_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (inter s1 s2).
+Proof.
+ intros. unfold inter, linear_inter. destruct compare_height; auto_tc.
+Qed.
+
+Lemma diff_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (diff s1 s2).
+Proof.
+ intros. unfold diff, linear_diff. destruct compare_height; auto_tc.
+Qed.
+
+End BalanceProps.
+
+(** * Final Encapsulation
+
+   Now, in order to really provide a functor implementing [S], we
+   need to encapsulate everything into a type of binary search trees.
+   They also happen to be well-balanced, but this has no influence
+   on the correctness of operations, so we won't state this here,
+   see [BalanceProps] if you need more than just the MSet interface.
+*)
+
+Module Type MSetInterface_S_Ext := MSetInterface.S <+ MSetRemoveMin.
+
+Module Make (X: Orders.OrderedType) <:
+ MSetInterface_S_Ext with Module E := X.
+ Module Raw. Include MakeRaw X. End Raw.
+ Include MSetInterface.Raw2Sets X Raw.
+
+ Definition opt_ok (x:option (elt * Raw.t)) :=
+  match x with Some (_,s) => Raw.Ok s | None => True end.
+
+ Definition mk_opt_t (x: option (elt * Raw.t))(P: opt_ok x) :
+   option (elt * t) :=
+ match x as o return opt_ok o -> option (elt * t) with
+ | Some (k,s') => fun P : Raw.Ok s' => Some (k, Mkt s')
+ | None => fun _ => None
+ end P.
+
+ Definition remove_min s : option (elt * t) :=
+  mk_opt_t (Raw.remove_min (this s)) (Raw.remove_min_ok s).
+
+ Lemma remove_min_spec1 s x s' :
+  remove_min s = Some (x,s') ->
+   min_elt s = Some x /\ Equal (remove x s) s'.
+ Proof.
+ destruct s as (s,Hs).
+ unfold remove_min, mk_opt_t, min_elt, remove, Equal, In; simpl.
+ generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs).
+ set (P := Raw.remove_min_ok s). clearbody P.
+ destruct (Raw.remove_min s) as [(x0,s0)|]; try easy.
+ intros H U. injection U. clear U; intros; subst. simpl.
+ destruct (H x s0); auto. subst; intuition.
+ Qed.
+
+ Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
+ Proof.
+ destruct s as (s,Hs).
+ unfold remove_min, mk_opt_t, Empty, In; simpl.
+ generalize (Raw.remove_min_spec2 s).
+ set (P := Raw.remove_min_ok s). clearbody P.
+ destruct (Raw.remove_min s) as [(x0,s0)|]; now intuition.
+ Qed.
+
+End Make.
diff --git a/theories/MSets/vo.itarget b/theories/MSets/vo.itarget
index 14429b81..7c5b6899 100644
--- a/theories/MSets/vo.itarget
+++ b/theories/MSets/vo.itarget
@@ -1,4 +1,6 @@
+MSetGenTree.vo
 MSetAVL.vo
+MSetRBT.vo
 MSetDecide.vo
 MSetEqProperties.vo
 MSetFacts.vo
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 06ff7cd1..d408845e 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -28,7 +28,7 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
 Definition block {A : Type} (a : A) := a.
 
 Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
-Ltac unblock_goal := cbv beta delta [block]. 
+Ltac unblock_goal := unfold block in *.
 
 (** Notation for heterogenous equality. *)
 
@@ -214,7 +214,8 @@ Ltac simplify_eqs :=
 
 Ltac simplify_IH_hyps := repeat
   match goal with
-    | [ hyp : _ |- _ ] => specialize_eqs hyp
+    | [ hyp : context [ block _ ] |- _ ] => 
+      specialize_eqs hyp
   end.
 
 (** We split substitution tactics in the two directions depending on which 
@@ -377,14 +378,23 @@ Ltac is_introduced H :=
   end.
 
 Tactic Notation "intro_block" hyp(H) :=
-  (is_introduced H ; block_goal ; revert_until H) ||
+  (is_introduced H ; block_goal ; revert_until H ; block_goal) ||
     (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
 
 Tactic Notation "intro_block_id" ident(H) :=
-  (is_introduced H ; block_goal ; revert_until H) ||
+  (is_introduced H ; block_goal ; revert_until H; block_goal) ||
     (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
 
-Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
+Ltac unblock_dep_elim :=
+  match goal with
+    | |- block ?T => 
+      match T with context [ block _ ] => 
+        change T ; intros ; unblock_goal
+      end
+    | _ => unblock_goal
+  end.
+
+Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_dep_elim.
 
 Ltac do_intros H :=
   (try intros until H) ; (intro_block_id H || intro_block H).
@@ -395,7 +405,7 @@ Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim.
 
 Ltac do_depind tac H := 
   (try intros until H) ; intro_block H ;
-  generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
+  generalize_eqs_vars H ; tac H ; simpl_dep_elim.
 
 (** To dependent elimination on some hyp. *)
 
@@ -412,8 +422,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
 (** A variant where generalized variables should be given by the user. *)
 
 Ltac do_depelim' rev tac H :=
-  (try intros until H) ; block_goal ; rev H ; generalize_eqs H ; tac H ; simplify_dep_elim ; 
-    simplify_IH_hyps ; unblock_goal.
+  (try intros until H) ; block_goal ; rev H ;
+  (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v
index 31724b3c..13387f30 100644
--- a/theories/Unicode/Utf8_core.v
+++ b/theories/Unicode/Utf8_core.v
@@ -17,7 +17,9 @@ Notation "∃  x .. y , P" := (exists x, .. (exists y, P) ..)
 
 Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
 Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
-Notation "x → y" := (x -> y) (at level 90, right associativity): type_scope.
+Notation "x → y" := (x -> y)
+  (at level 90, y at level 200, right associativity): type_scope.
+
 Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope.
 Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope.
 Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 28e355fb..a5e37f34 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -14,7 +14,7 @@ Require Arith_base.
 the n-uplet and [FS] set (n-1)-uplet of all the element but the first.
 
    Author: Pierre Boutillier
-   Institution: PPS, INRIA 12/2010
+   Institution: PPS, INRIA 12/2010-01/2012
 *)
 
 Inductive t : nat -> Set :=
@@ -69,6 +69,13 @@ match a with
 end.
 End SCHEMES.
 
+Definition FS_inj {n} (x y: t n) (eq: FS x = FS y): x = y :=
+match eq in _ = a return
+  match a as a' in t m return match m with |0 => Prop |S n' => t n' -> Prop end
+  with @F1 _ =>  fun _ => True |@FS _ y => fun x' => x' = y end x with
+  eq_refl => eq_refl
+end.
+
 (** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
 Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
   match n in t k return {i | i< k} with
@@ -167,6 +174,7 @@ end.
 
 Lemma depair_sanity {m n} (o : t m) (p : t n) :
   proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
+Proof.
 induction o ; simpl.
   rewrite L_sanity. now rewrite Mult.mult_0_r.
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 0fee50ff..30c0d4c0 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,17 +40,17 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
  fix rectS_fix {n} (v: t A (S n)) : P v :=
  match v with
- |nil => @id
+ |nil => fun devil => False_rect (@ID) devil
  |cons a 0 v =>
    match v as vnn in t _ nn
        return
          match nn,vnn with
          |0,vm =>  P (a :: vm)
-         |S _,_ => ID
+         |S _,_ => _
          end
      with
      |nil => bas a
-     |_ :: _ => @id
+     |_ :: _ => fun devil => False_rect (@ID) devil
      end
  |cons a (S nn') v => rect a v (rectS_fix v)
  end.
@@ -66,11 +66,11 @@ match v1 as v1' in t _ n1
   |[] => fun v2 =>
      match v2 with
        |[] => bas
-       |_ :: _ => @id
+       |_ :: _ => fun devil => False_rect (@ID) devil
      end
   |h1 :: t1 => fun v2 =>
     match v2 with
-      |[] => @id
+      |[] => fun devil => False_rect (@ID) devil
       |h2 :: t2 => fun t1' =>
         rect (rect2_fix t1' t2) h1 h2
     end t1
@@ -83,10 +83,10 @@ match v with
 end.
 
 (** A vector of length [S _] is [cons] *)
-Definition caseS {A} (P : forall n, t A (S n) -> Type)
-  (H : forall h {n} t, @P n (h :: t)) {n} v : P n v :=
-match v with
-  |[] => @id (* Why needed ? *)
+Definition caseS {A} (P : forall {n}, t A (S n) -> Type)
+  (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v :=
+match v as v' in t _ m return match m, v' with |0, _ => False -> True |S _, v0 => P v' end with
+  |[] => fun devil => False_rect _ devil (* subterm !!! *)
   |h :: t => H h t
 end.
 End SCHEMES.
@@ -111,11 +111,12 @@ Fixpoint const {A} (a:A) (n:nat) :=
 
 Computational behavior of this function should be the same as
 ocaml function. *)
-Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : A :=
+Definition nth {A} := 
+fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
 match p in Fin.t m' return t A m' -> A with
  |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v
  |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
-   (fun h n t p0 => nth t p0) v) p'
+   (fun h n t p0 => nth_fix t p0) v) p'
 end v'.
 
 (** An equivalent definition of [nth]. *)
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index a576315e..2f4086e5 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -16,6 +16,12 @@ Require Fin.
 Require Import VectorDef.
 Import VectorNotations.
 
+Definition cons_inj A a1 a2 n (v1 v2 : t A n)
+ (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 :=
+   match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1
+   with | eq_refl => conj eq_refl eq_refl
+   end.
+
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
 is true for the one that use [lt] *)
 
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index ce0fee71..0e096100 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -54,7 +54,7 @@ Section WfLexicographic_Product.
     subst x1.
     apply IHAcc0.
     elim inj_pair2 with A B x y' x0; assumption.
-  Qed.
+  Defined.
 
   Theorem wf_lexprod :
     well_founded leA ->
@@ -65,7 +65,7 @@ Section WfLexicographic_Product.
     apply acc_A_B_lexprod; auto with sets; intros.
     red in wfB.
     auto with sets.
-  Qed.
+  Defined.
 
 
 End WfLexicographic_Product.
@@ -88,7 +88,7 @@ Section Wf_Symmetric_Product.
     inversion_clear H5; auto with sets.
     apply IHAcc; auto.
     apply Acc_intro; trivial.
-  Qed.
+  Defined.
 
 
   Lemma wf_symprod :
@@ -97,7 +97,7 @@ Section Wf_Symmetric_Product.
     red in |- *.
     destruct a.
     apply Acc_symprod; auto with sets.
-  Qed.
+  Defined.
 
 End Wf_Symmetric_Product.
 
@@ -128,7 +128,7 @@ Section Swap.
 
     apply sp_noswap.
     apply left_sym; auto with sets.
-  Qed.
+  Defined.
 
 
   Lemma Acc_swapprod :
@@ -156,7 +156,7 @@ Section Swap.
     apply right_sym; auto with sets.
 
     auto with sets.
-  Qed.
+  Defined.
 
 
   Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
@@ -164,6 +164,6 @@ Section Swap.
     red in |- *.
     destruct a; intros.
     apply Acc_swapprod; auto with sets.
-  Qed.
+  Defined.
 
 End Swap.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index bac50fc4..7c840c56 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -16,28 +16,29 @@
 
 Require Import ZArith.
 Delimit Scope Int_scope with I.
-
+Local Open Scope Int_scope.
 
 (** * a specification of integers *)
 
 Module Type Int.
 
-  Open Scope Int_scope.
+  Parameter t : Set.
+  Bind Scope Int_scope with t.
 
-  Parameter int : Set.
+  (** For compatibility *)
+  Definition int := t.
 
-  Parameter i2z : int -> Z.
-  Arguments i2z _%I.
+  Parameter i2z : t -> Z.
 
-  Parameter _0 : int.
-  Parameter _1 : int.
-  Parameter _2 : int.
-  Parameter _3 : int.
-  Parameter plus : int -> int -> int.
-  Parameter opp : int -> int.
-  Parameter minus : int -> int -> int.
-  Parameter mult : int -> int -> int.
-  Parameter max : int -> int -> int.
+  Parameter _0 : t.
+  Parameter _1 : t.
+  Parameter _2 : t.
+  Parameter _3 : t.
+  Parameter plus : t -> t -> t.
+  Parameter opp : t -> t.
+  Parameter minus : t -> t -> t.
+  Parameter mult : t -> t -> t.
+  Parameter max : t -> t -> t.
 
   Notation "0" := _0 : Int_scope.
   Notation "1" := _1 : Int_scope.
@@ -54,10 +55,10 @@ Module Type Int.
 
   Notation "x == y" := (i2z x = i2z y)
     (at level 70, y at next level, no associativity) : Int_scope.
-  Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope.
-  Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope.
-  Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope.
-  Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope.
+  Notation "x <= y" := (i2z x <= i2z y)%Z : Int_scope.
+  Notation "x < y" := (i2z x < i2z y)%Z : Int_scope.
+  Notation "x >= y" := (i2z x >= i2z y)%Z : Int_scope.
+  Notation "x > y" := (i2z x > i2z y)%Z : Int_scope.
   Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope.
   Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope.
   Notation "x < y < z" := (x < y /\ y < z) : Int_scope.
@@ -65,41 +66,39 @@ Module Type Int.
 
   (** Some decidability fonctions (informative). *)
 
-  Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}.
-  Axiom ge_lt_dec :  forall x y : int, {x >= y} + {x < y}.
-  Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }.
+  Axiom gt_le_dec : forall x y : t, {x > y} + {x <= y}.
+  Axiom ge_lt_dec :  forall x y : t, {x >= y} + {x < y}.
+  Axiom eq_dec : forall x y : t, { x == y } + {~ x==y }.
 
   (** Specifications *)
 
   (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality
       [==] and the generic [=] are in fact equivalent. We define [==]
-      nonetheless since the translation to [Z] for using automatic tactic is easier. *)
+      nonetheless since the translation to [Z] for using automatic tactic
+      is easier. *)
 
-  Axiom i2z_eq : forall n p : int, n == p -> n = p.
+  Axiom i2z_eq : forall n p : t, n == p -> n = p.
 
    (** Then, we express the specifications of the above parameters using their
        Z counterparts. *)
 
-  Open Scope Z_scope.
-  Axiom i2z_0 : i2z _0 = 0.
-  Axiom i2z_1 : i2z _1 = 1.
-  Axiom i2z_2 : i2z _2 = 2.
-  Axiom i2z_3 : i2z _3 = 3.
-  Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p.
-  Axiom i2z_opp : forall n, i2z (-n) = -i2z n.
-  Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p.
-  Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p.
-  Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p).
+  Axiom i2z_0 : i2z _0 = 0%Z.
+  Axiom i2z_1 : i2z _1 = 1%Z.
+  Axiom i2z_2 : i2z _2 = 2%Z.
+  Axiom i2z_3 : i2z _3 = 3%Z.
+  Axiom i2z_plus : forall n p, i2z (n + p) = (i2z n + i2z p)%Z.
+  Axiom i2z_opp : forall n, i2z (-n) = (-i2z n)%Z.
+  Axiom i2z_minus : forall n p, i2z (n - p) = (i2z n - i2z p)%Z.
+  Axiom i2z_mult : forall n p, i2z (n * p) = (i2z n * i2z p)%Z.
+  Axiom i2z_max : forall n p, i2z (max n p) = Z.max (i2z n) (i2z p).
 
 End Int.
 
 
 (** * Facts and  tactics using [Int] *)
 
-Module MoreInt (I:Int).
-  Import I.
-
-  Open Scope Int_scope.
+Module MoreInt (Import I:Int).
+  Local Notation int := I.t.
 
   (** A magic (but costly) tactic that goes from [int] back to the [Z]
       friendly world ... *)
@@ -108,13 +107,14 @@ Module MoreInt (I:Int).
     i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z.
 
   Ltac i2z := match goal with
-		| H : (eq (A:=int) ?a ?b) |- _ =>
-		  generalize (f_equal i2z H);
-		    try autorewrite with i2z; clear H; intro H; i2z
-		| |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z
-		| H : _ |- _ => progress autorewrite with i2z in H; i2z
-		| _ => try autorewrite with i2z
-	      end.
+    | H : ?a = ?b |- _ =>
+      generalize (f_equal i2z H);
+	try autorewrite with i2z; clear H; intro H; i2z
+    | |- ?a = ?b =>
+      apply (i2z_eq a b); try autorewrite with i2z; i2z
+    | H : _ |- _ => progress autorewrite with i2z in H; i2z
+    | _ => try autorewrite with i2z
+  end.
 
   (** A reflexive version of the [i2z] tactic *)
 
@@ -124,14 +124,14 @@ Module MoreInt (I:Int).
       Anyhow, [i2z_refl] is enough for applying [romega]. *)
 
   Ltac i2z_gen := match goal with
-    | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen
-    | H : (eq (A:=int) ?a ?b) |- _ =>
+    | |- ?a = ?b => apply (i2z_eq a b); i2z_gen
+    | H : ?a = ?b |- _ =>
        generalize (f_equal i2z H); clear H; i2z_gen
-    | H : (eq (A:=Z) ?a ?b) |- _ => revert H; i2z_gen
-    | H : (Zlt ?a ?b) |- _ => revert H; i2z_gen
-    | H : (Zle ?a ?b) |- _ => revert H; i2z_gen
-    | H : (Zgt ?a ?b) |- _ => revert H; i2z_gen
-    | H : (Zge ?a ?b) |- _ => revert H; i2z_gen
+    | H : eq (A:=Z) ?a ?b |- _ => revert H; i2z_gen
+    | H : Z.lt ?a ?b |- _ => revert H; i2z_gen
+    | H : Z.le ?a ?b |- _ => revert H; i2z_gen
+    | H : Z.gt ?a ?b |- _ => revert H; i2z_gen
+    | H : Z.ge ?a ?b |- _ => revert H; i2z_gen
     | H : _ -> ?X |- _ =>
       (* A [Set] or [Type] part cannot be dealt with easily
          using the [ExprP] datatype. So we forget it, leaving
@@ -201,11 +201,11 @@ Module MoreInt (I:Int).
 
     with z2ez trm :=
     match constr:trm with
-      | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey)
-      | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey)
-      | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey)
-      | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey)
-      | (-?x)%Z =>  let ex := z2ez x in constr:(EZopp ex)
+      | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey)
+      | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey)
+      | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey)
+      | (Z.max ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey)
+      | (- ?x)%Z =>  let ex := z2ez x in constr:(EZopp ex)
       | i2z ?x => let ex := i2ei x in constr:(EZofI ex)
       | ?x => constr:(EZraw x)
     end.
@@ -360,8 +360,9 @@ End MoreInt.
 (** It's always nice to know that our [Int] interface is realizable :-) *)
 
 Module Z_as_Int <: Int.
-  Open Scope Z_scope.
-  Definition int := Z.
+  Local Open Scope Z_scope.
+  Definition t := Z.
+  Definition int := t.
   Definition _0 := 0.
   Definition _1 := 1.
   Definition _2 := 2.
@@ -380,10 +381,9 @@ Module Z_as_Int <: Int.
   Lemma i2z_1 : i2z _1 = 1.  Proof. auto. Qed.
   Lemma i2z_2 : i2z _2 = 2.  Proof. auto. Qed.
   Lemma i2z_3 : i2z _3 = 3.  Proof. auto. Qed.
-  Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p.  Proof. auto. Qed.
-  Lemma i2z_opp : forall n, i2z (- n)  = - i2z n.  Proof. auto. Qed.
-  Lemma i2z_minus : forall n p, i2z (n - p)  = i2z n - i2z p.  Proof. auto. Qed.
-  Lemma i2z_mult : forall n p, i2z (n * p)  = i2z n * i2z p.  Proof. auto. Qed.
-  Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed.
+  Lemma i2z_plus n p : i2z (n + p) = i2z n + i2z p.  Proof. auto. Qed.
+  Lemma i2z_opp n : i2z (- n) = - i2z n.  Proof. auto. Qed.
+  Lemma i2z_minus n p : i2z (n - p) = i2z n - i2z p.  Proof. auto. Qed.
+  Lemma i2z_mult n p : i2z (n * p) = i2z n * i2z p.  Proof. auto. Qed.
+  Lemma i2z_max n p : i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed.
 End Z_as_Int.
-
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
new file mode 100644
index 00000000..17c5bae3
--- /dev/null
+++ b/theories/ZArith/ZOdiv.v
@@ -0,0 +1,88 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Export ZOdiv_def.
+Require Import BinInt Zquot.
+
+Notation ZO_div_mod_eq := Z.quot_rem' (only parsing).
+Notation ZOmod_lt := Zrem_lt (only parsing).
+Notation ZOmod_sgn := Zrem_sgn (only parsing).
+Notation ZOmod_sgn2 := Zrem_sgn2 (only parsing).
+Notation ZOmod_lt_pos := Zrem_lt_pos (only parsing).
+Notation ZOmod_lt_neg := Zrem_lt_neg (only parsing).
+Notation ZOmod_lt_pos_pos := Zrem_lt_pos_pos (only parsing).
+Notation ZOmod_lt_pos_neg := Zrem_lt_pos_neg (only parsing).
+Notation ZOmod_lt_neg_pos := Zrem_lt_neg_pos (only parsing).
+Notation ZOmod_lt_neg_neg := Zrem_lt_neg_neg (only parsing).
+
+Notation ZOdiv_opp_l := Zquot_opp_l (only parsing).
+Notation ZOdiv_opp_r := Zquot_opp_r (only parsing).
+Notation ZOmod_opp_l := Zrem_opp_l (only parsing).
+Notation ZOmod_opp_r := Zrem_opp_r (only parsing).
+Notation ZOdiv_opp_opp := Zquot_opp_opp (only parsing).
+Notation ZOmod_opp_opp := Zrem_opp_opp (only parsing).
+
+Notation Remainder := Remainder (only parsing).
+Notation Remainder_alt := Remainder_alt (only parsing).
+Notation Remainder_equiv := Remainder_equiv (only parsing).
+Notation ZOdiv_mod_unique_full := Zquot_mod_unique_full (only parsing).
+Notation ZOdiv_unique_full := Zquot_unique_full (only parsing).
+Notation ZOdiv_unique := Zquot_unique (only parsing).
+Notation ZOmod_unique_full := Zrem_unique_full (only parsing).
+Notation ZOmod_unique := Zrem_unique (only parsing).
+
+Notation ZOmod_0_l := Zrem_0_l (only parsing).
+Notation ZOmod_0_r := Zrem_0_r (only parsing).
+Notation ZOdiv_0_l := Zquot_0_l (only parsing).
+Notation ZOdiv_0_r := Zquot_0_r (only parsing).
+Notation ZOmod_1_r := Zrem_1_r (only parsing).
+Notation ZOdiv_1_r := Zquot_1_r (only parsing).
+Notation ZOdiv_1_l := Zquot_1_l (only parsing).
+Notation ZOmod_1_l := Zrem_1_l (only parsing).
+Notation ZO_div_same := Z_quot_same (only parsing).
+Notation ZO_mod_same := Z_rem_same (only parsing).
+Notation ZO_mod_mult := Z_rem_mult (only parsing).
+Notation ZO_div_mult := Z_quot_mult (only parsing).
+
+Notation ZO_div_pos := Z_quot_pos (only parsing).
+Notation ZO_div_lt := Z_quot_lt (only parsing).
+Notation ZOdiv_small := Zquot_small (only parsing).
+Notation ZOmod_small := Zrem_small (only parsing).
+Notation ZO_div_monotone := Z_quot_monotone (only parsing).
+Notation ZO_mult_div_le := Z_mult_quot_le (only parsing).
+Notation ZO_mult_div_ge := Z_mult_quot_ge (only parsing).
+Definition ZO_div_exact_full_1 a b := proj1 (Z_quot_exact_full a b).
+Definition ZO_div_exact_full_2 a b := proj2 (Z_quot_exact_full a b).
+Notation ZOmod_le := Zrem_le (only parsing).
+Notation ZOdiv_le_upper_bound := Zquot_le_upper_bound (only parsing).
+Notation ZOdiv_lt_upper_bound := Zquot_lt_upper_bound (only parsing).
+Notation ZOdiv_le_lower_bound := Zquot_le_lower_bound (only parsing).
+Notation ZOdiv_sgn := Zquot_sgn (only parsing).
+
+Notation ZO_mod_plus := Z_rem_plus (only parsing).
+Notation ZO_div_plus := Z_quot_plus (only parsing).
+Notation ZO_div_plus_l := Z_quot_plus_l (only parsing).
+Notation ZOdiv_mult_cancel_r := Zquot_mult_cancel_r (only parsing).
+Notation ZOdiv_mult_cancel_l := Zquot_mult_cancel_l (only parsing).
+Notation ZOmult_mod_distr_l := Zmult_rem_distr_l (only parsing).
+Notation ZOmult_mod_distr_r := Zmult_rem_distr_r (only parsing).
+Notation ZOmod_mod := Zrem_rem (only parsing).
+Notation ZOmult_mod := Zmult_rem (only parsing).
+Notation ZOplus_mod := Zplus_rem (only parsing).
+Notation ZOplus_mod_idemp_l := Zplus_rem_idemp_l (only parsing).
+Notation ZOplus_mod_idemp_r := Zplus_rem_idemp_r (only parsing).
+Notation ZOmult_mod_idemp_l := Zmult_rem_idemp_l (only parsing).
+Notation ZOmult_mod_idemp_r := Zmult_rem_idemp_r (only parsing).
+Notation ZOdiv_ZOdiv := Zquot_Zquot (only parsing).
+Notation ZOdiv_mult_le := Zquot_mult_le (only parsing).
+Notation ZOmod_divides := Zrem_divides (only parsing).
+
+Notation ZOdiv_eucl_Zdiv_eucl_pos := Zquotrem_Zdiv_eucl_pos (only parsing).
+Notation ZOdiv_Zdiv_pos := Zquot_Zdiv_pos (only parsing).
+Notation ZOmod_Zmod_pos := Zrem_Zmod_pos (only parsing).
+Notation ZOmod_Zmod_zero := Zrem_Zmod_zero (only parsing).
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v
new file mode 100644
index 00000000..38d25797
--- /dev/null
+++ b/theories/ZArith/ZOdiv_def.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import BinInt.
+
+Notation ZOdiv_eucl := Z.quotrem (only parsing).
+Notation ZOdiv := Z.quot (only parsing).
+Notation ZOmod := Z.rem (only parsing).
+
+Notation ZOdiv_eucl_correct := Z.quotrem_eq.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 550b66f7..f4d702b2 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -197,14 +197,12 @@ Qed.
 Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.
 Proof.
  assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2).
-  BeginSubproof.
-   intros m Hm.
+ { intros m Hm.
    apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0).
    now apply Z.lt_le_incl.
    rewrite Z.sgn_pos by trivial.
    destruct (Z.odd m); now split.
-   apply Zquot2_odd_eqn.
-  EndSubproof.
+   apply Zquot2_odd_eqn. }
  destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]].
  - now apply AUX.
  - now subst.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 178111cd..88751cc0 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -23,6 +23,8 @@ Zmin.vo
 Zmisc.vo
 Znat.vo
 Znumtheory.vo
+ZOdiv_def.vo
+ZOdiv.vo
 Zquot.vo
 Zorder.vo
 Zpow_def.vo