MSetRBT : implementation of MSets via Red-Black trees

 Initial contribution by Andrew Appel, many ulterior modifications
 by myself.

 Interest: red-black trees maintain logarithmic depths as AVL,
 but they do not rely on integer height annotations as AVL,
 allowing interesting performance when computing in Coq or after
 standard extraction. More on this topic in the article by A. Appel.

 The common parts of MSetAVL and MSetRBT are shared in a new file
 MSetGenTree which include the definition of tree and functions
 such as mem fold elements compare subset.

 Note that the height of AVL trees is now the first arg of the
 Node constructor instead of the last one.

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

1 files changed, 64 insertions, 64 deletions

diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index bac50fc45..7c840c563 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.
-