Merge branch 'experimental/master'

1 files changed, 73 insertions, 79 deletions

diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index c0123ca8..99ecd150 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: Int.v 12363 2009-09-28 15:04:07Z letouzey $ *)
-
 (** * An light axiomatization of integers (used in FSetAVL). *)
 
 (** We define a signature for an integer datatype based on [Z].
@@ -18,28 +16,26 @@
 
 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 int : Set.
+  Parameter t : Set.
+  Bind Scope Int_scope with t.
 
-  Parameter i2z : int -> Z.
-  Arguments Scope i2z [ Int_scope ].
+  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.
@@ -56,10 +52,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.
@@ -67,41 +63,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 ... *)
@@ -110,13 +104,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 *)
 
@@ -126,14 +121,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
@@ -203,11 +198,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.
@@ -222,10 +217,10 @@ Module MoreInt (I:Int).
       | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey)
       | (~ ?x) => let ex := p2ep x in constr:(EPneg ex)
       | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey)
-      | (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey)
-      | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey)
-      | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey)
-      | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey)
+      | (?x < ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey)
+      | (?x <= ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey)
+      | (?x > ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey)
+      | (?x >= ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey)
       | ?x =>  constr:(EPraw x)
     end.
 
@@ -252,7 +247,7 @@ Module MoreInt (I:Int).
       | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z
       | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z
       | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z
-      | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2)
+      | EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2)
       | EZopp e => (-(ez2z e))%Z
       | EZofI e => i2z (ei2i e)
       | EZraw z => z
@@ -362,30 +357,29 @@ 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 _0 := 0.
   Definition _1 := 1.
   Definition _2 := 2.
   Definition _3 := 3.
-  Definition plus := Zplus.
-  Definition opp := Zopp.
-  Definition minus := Zminus.
-  Definition mult := Zmult.
-  Definition max := Zmax.
+  Definition plus := Z.add.
+  Definition opp := Z.opp.
+  Definition minus := Z.sub.
+  Definition mult := Z.mul.
+  Definition max := Z.max.
   Definition gt_le_dec := Z_gt_le_dec.
   Definition ge_lt_dec := Z_ge_lt_dec.
-  Definition eq_dec := Z_eq_dec.
-  Definition i2z : int -> Z := fun n => n.
+  Definition eq_dec := Z.eq_dec.
+  Definition i2z : t -> Z := fun n => n.
   Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed.
   Lemma i2z_0 : i2z _0 = 0.  Proof. auto. Qed.
   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) = Z.max (i2z n) (i2z p). Proof. auto. Qed.
 End Z_as_Int.
-