ZArith/Int.v: some modernizations

2 files changed, 140 insertions, 71 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index e1fc454ae..cc023cc3f 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -31,7 +31,7 @@
     code after extraction.
 *)
 
-Require Import MSetInterface MSetGenTree ZArith Int.
+Require Import MSetInterface MSetGenTree BinInt Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -83,11 +83,11 @@ Definition assert_false := create.
 Definition bal l x r :=
   let hl := height l in
   let hr := height r in
-  if gt_le_dec hl (hr+2) then
+  if (hr+2) <? hl then
     match l with
      | Leaf => assert_false l x r
      | Node _ ll lx lr =>
-       if ge_lt_dec (height ll) (height lr) then
+       if (height lr) <=? (height ll) then
          create ll lx (create lr x r)
        else
          match lr with
@@ -97,11 +97,11 @@ Definition bal l x r :=
          end
     end
   else
-    if gt_le_dec hr (hl+2) then
+    if (hl+2) <? hr then
       match r with
        | Leaf => assert_false l x r
        | Node _ rl rx rr =>
-         if ge_lt_dec (height rr) (height rl) then
+         if (height rl) <=? (height rr) then
             create (create l x rl) rx rr
          else
            match rl with
@@ -138,8 +138,8 @@ Fixpoint join l : elt -> t -> t :=
        fix join_aux (r:t) : t := match r with
           | 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
+               if (rh+2) <? lh then bal ll lx (join lr x r)
+               else if (lh+2) <? rh then bal (join_aux rl) rx rr
                else create l x r
           end
   end.
@@ -419,12 +419,12 @@ Local Open Scope Int_scope.
 Ltac join_tac :=
  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];
+     [ | destruct ((rh+2) <? lh) eqn:LT;
        [ match goal with |- context b [ bal ?a ?b ?c] =>
            replace (bal a b c)
            with (bal ll lx (join lr x (Node rh rl rx rr))); [ | auto]
          end
-       | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
+       | destruct ((lh+2) <? rh) eqn:LT';
          [ match goal with |- context b [ bal ?a ?b ?c] =>
              replace (bal a b c)
              with (bal (join (Node lh ll lx lr) x rl) rx rr); [ | auto]
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 99ecd150b..d210792f9 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(** * An light axiomatization of integers (used in FSetAVL). *)
+(** * An light axiomatization of integers (used in MSetAVL). *)
 
 (** We define a signature for an integer datatype based on [Z].
     The goal is to allow a switch after extraction to ocaml's
@@ -14,11 +14,11 @@
     (typically : when mesuring the height of an AVL tree).
 *)
 
-Require Import ZArith.
+Require Import BinInt.
 Delimit Scope Int_scope with I.
 Local Open Scope Int_scope.
 
-(** * a specification of integers *)
+(** * A specification of integers *)
 
 Module Type Int.
 
@@ -31,19 +31,19 @@ Module Type Int.
   Parameter _1 : t.
   Parameter _2 : t.
   Parameter _3 : t.
-  Parameter plus : t -> t -> t.
+  Parameter add : t -> t -> t.
   Parameter opp : t -> t.
-  Parameter minus : t -> t -> t.
-  Parameter mult : t -> t -> t.
+  Parameter sub : t -> t -> t.
+  Parameter mul : t -> t -> t.
   Parameter max : t -> t -> t.
 
   Notation "0" := _0 : Int_scope.
   Notation "1" := _1 : Int_scope.
   Notation "2" := _2 : Int_scope.
   Notation "3" := _3 : Int_scope.
-  Infix "+" := plus : Int_scope.
-  Infix "-" := minus : Int_scope.
-  Infix "*" := mult : Int_scope.
+  Infix "+" := add : Int_scope.
+  Infix "-" := sub : Int_scope.
+  Infix "*" := mul : Int_scope.
   Notation "- x" := (opp x) : Int_scope.
 
   (** For logical relations, we can rely on their counterparts in Z,
@@ -61,7 +61,17 @@ Module Type Int.
   Notation "x < y < z" := (x < y /\ y < z) : Int_scope.
   Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope.
 
-  (** Some decidability fonctions (informative). *)
+  (** Informative comparisons. *)
+
+  Axiom eqb : t -> t -> bool.
+  Axiom ltb : t -> t -> bool.
+  Axiom leb : t -> t -> bool.
+
+  Infix "=?" := eqb.
+  Infix "<?" := ltb.
+  Infix "<=?" := leb.
+
+  (** For compatibility, some decidability fonctions (informative). *)
 
   Axiom gt_le_dec : forall x y : t, {x > y} + {x <= y}.
   Axiom ge_lt_dec :  forall x y : t, {x >= y} + {x < y}.
@@ -83,11 +93,14 @@ Module Type Int.
   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_add : 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_sub : forall n p, i2z (n - p) = (i2z n - i2z p)%Z.
+  Axiom i2z_mul : 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).
+  Axiom i2z_eqb : forall n p, eqb n p = Z.eqb (i2z n) (i2z p).
+  Axiom i2z_ltb : forall n p, ltb n p = Z.ltb (i2z n) (i2z p).
+  Axiom i2z_leb : forall n p, leb n p = Z.leb (i2z n) (i2z p).
 
 End Int.
 
@@ -97,11 +110,42 @@ End Int.
 Module MoreInt (Import I:Int).
   Local Notation int := I.t.
 
+  Lemma eqb_eq n p : (n =? p) = true <-> n == p.
+  Proof.
+   now rewrite i2z_eqb, Z.eqb_eq.
+  Qed.
+
+  Lemma eqb_neq n p : (n =? p) = false <-> ~(n == p).
+  Proof.
+   rewrite <- eqb_eq. destruct (n =? p); intuition.
+  Qed.
+
+  Lemma ltb_lt n p : (n <? p) = true <-> n < p.
+  Proof.
+   now rewrite i2z_ltb, Z.ltb_lt.
+  Qed.
+
+  Lemma ltb_nlt n p : (n <? p) = false <-> ~(n < p).
+  Proof.
+   rewrite <- ltb_lt. destruct (n <? p); intuition.
+  Qed.
+
+  Lemma leb_le n p : (n <=? p) = true <-> n <= p.
+  Proof.
+   now rewrite i2z_leb, Z.leb_le.
+  Qed.
+
+  Lemma leb_nle n p : (n <=? p) = false <-> ~(n <= p).
+  Proof.
+   rewrite <- leb_le. destruct (n <=? p); intuition.
+  Qed.
+
   (** A magic (but costly) tactic that goes from [int] back to the [Z]
       friendly world ... *)
 
   Hint Rewrite ->
-    i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z.
+    i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max
+    i2z_eqb i2z_ltb i2z_leb : i2z.
 
   Ltac i2z := match goal with
     | H : ?a = ?b |- _ =>
@@ -149,18 +193,18 @@ Module MoreInt (Import I:Int).
     | EI1 : ExprI
     | EI2 : ExprI
     | EI3 : ExprI
-    | EIplus : ExprI -> ExprI -> ExprI
+    | EIadd : ExprI -> ExprI -> ExprI
     | EIopp : ExprI -> ExprI
-    | EIminus : ExprI -> ExprI -> ExprI
-    | EImult : ExprI -> ExprI -> ExprI
+    | EIsub : ExprI -> ExprI -> ExprI
+    | EImul : ExprI -> ExprI -> ExprI
     | EImax : ExprI -> ExprI -> ExprI
     | EIraw : int -> ExprI.
 
   Inductive ExprZ : Set :=
-    | EZplus : ExprZ -> ExprZ -> ExprZ
+    | EZadd : ExprZ -> ExprZ -> ExprZ
     | EZopp : ExprZ -> ExprZ
-    | EZminus : ExprZ -> ExprZ -> ExprZ
-    | EZmult : ExprZ -> ExprZ -> ExprZ
+    | EZsub : ExprZ -> ExprZ -> ExprZ
+    | EZmul : ExprZ -> ExprZ -> ExprZ
     | EZmax : ExprZ -> ExprZ -> ExprZ
     | EZofI : ExprI -> ExprZ
     | EZraw : Z -> ExprZ.
@@ -186,9 +230,9 @@ Module MoreInt (Import I:Int).
       | 1 => constr:EI1
       | 2 => constr:EI2
       | 3 => constr:EI3
-      | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey)
-      | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey)
-      | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey)
+      | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey)
+      | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey)
+      | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey)
       | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey)
       | - ?x => let ex := i2ei x in constr:(EIopp ex)
       | ?x => constr:(EIraw x)
@@ -198,9 +242,9 @@ Module MoreInt (Import 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)
+      | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey)
+      | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey)
+      | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul 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)
@@ -232,9 +276,9 @@ Module MoreInt (Import I:Int).
       | EI1 => 1
       | EI2 => 2
       | EI3 => 3
-      | EIplus e1 e2 => (ei2i e1)+(ei2i e2)
-      | EIminus e1 e2 => (ei2i e1)-(ei2i e2)
-      | EImult e1 e2 => (ei2i e1)*(ei2i e2)
+      | EIadd e1 e2 => (ei2i e1)+(ei2i e2)
+      | EIsub e1 e2 => (ei2i e1)-(ei2i e2)
+      | EImul e1 e2 => (ei2i e1)*(ei2i e2)
       | EImax e1 e2 => max (ei2i e1) (ei2i e2)
       | EIopp e => -(ei2i e)
       | EIraw i => i
@@ -244,9 +288,9 @@ Module MoreInt (Import I:Int).
 
   Fixpoint ez2z (e:ExprZ) : Z :=
     match e with
-      | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z
-      | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z
-      | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z
+      | EZadd e1 e2 => ((ez2z e1)+(ez2z e2))%Z
+      | EZsub e1 e2 => ((ez2z e1)-(ez2z e2))%Z
+      | EZmul e1 e2 => ((ez2z e1)*(ez2z e2))%Z
       | EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2)
       | EZopp e => (-(ez2z e))%Z
       | EZofI e => i2z (ei2i e)
@@ -278,9 +322,9 @@ Module MoreInt (Import I:Int).
       | EI1 => EZraw (1%Z)
       | EI2 => EZraw (2%Z)
       | EI3 => EZraw (3%Z)
-      | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2)
-      | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2)
-      | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2)
+      | EIadd e1 e2 => EZadd (norm_ei e1) (norm_ei e2)
+      | EIsub e1 e2 => EZsub (norm_ei e1) (norm_ei e2)
+      | EImul e1 e2 => EZmul (norm_ei e1) (norm_ei e2)
       | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2)
       | EIopp e => EZopp (norm_ei e)
       | EIraw i => EZofI (EIraw i)
@@ -290,9 +334,9 @@ Module MoreInt (Import I:Int).
 
   Fixpoint norm_ez (e:ExprZ) : ExprZ :=
     match e with
-      | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2)
-      | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2)
-      | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2)
+      | EZadd e1 e2 => EZadd (norm_ez e1) (norm_ez e2)
+      | EZsub e1 e2 => EZsub (norm_ez e1) (norm_ez e2)
+      | EZmul e1 e2 => EZmul (norm_ez e1) (norm_ez e2)
       | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2)
       | EZopp e => EZopp (norm_ez e)
       | EZofI e =>  norm_ei e
@@ -316,24 +360,22 @@ Module MoreInt (Import I:Int).
       | EPraw p => EPraw p
     end.
 
-  Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e).
+  Lemma norm_ei_correct (e:ExprI) : ez2z (norm_ei e) = i2z (ei2i e).
   Proof.
-    induction e; simpl; intros; i2z; auto; try congruence.
+    induction e; simpl; i2z; auto; try congruence.
   Qed.
 
-  Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e.
+  Lemma norm_ez_correct (e:ExprZ) : ez2z (norm_ez e) = ez2z e.
   Proof.
-    induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct.
+    induction e; simpl; i2z; auto; try congruence; apply norm_ei_correct.
   Qed.
 
-  Lemma norm_ep_correct :
-    forall e:ExprP, ep2p (norm_ep e) <-> ep2p e.
+  Lemma norm_ep_correct (e:ExprP) : ep2p (norm_ep e) <-> ep2p e.
   Proof.
-    induction e; simpl; repeat (rewrite norm_ez_correct); intuition.
+    induction e; simpl; rewrite ?norm_ez_correct; intuition.
   Qed.
 
-  Lemma norm_ep_correct2 :
-    forall e:ExprP, ep2p (norm_ep e) -> ep2p e.
+  Lemma norm_ep_correct2 (e:ExprP) : ep2p (norm_ep e) -> ep2p e.
   Proof.
     intros; destruct (norm_ep_correct e); auto.
   Qed.
@@ -363,23 +405,50 @@ Module Z_as_Int <: Int.
   Definition _1 := 1.
   Definition _2 := 2.
   Definition _3 := 3.
-  Definition plus := Z.add.
+  Definition add := Z.add.
   Definition opp := Z.opp.
-  Definition minus := Z.sub.
-  Definition mult := Z.mul.
+  Definition sub := Z.sub.
+  Definition mul := Z.mul.
   Definition max := Z.max.
-  Definition gt_le_dec := Z_gt_le_dec.
-  Definition ge_lt_dec := Z_ge_lt_dec.
+  Definition eqb := Z.eqb.
+  Definition ltb := Z.ltb.
+  Definition leb := Z.leb.
+
   Definition eq_dec := Z.eq_dec.
+  Definition gt_le_dec i j : {i > j} + { i <= j }.
+  Proof.
+    generalize (Z.ltb_spec j i).
+    destruct (j <? i); [left|right]; inversion H; trivial.
+    now apply Z.lt_gt.
+  Defined.
+  Definition ge_lt_dec i j : {i >= j} + { i < j }.
+  Proof.
+    generalize (Z.ltb_spec i j).
+    destruct (i <? j); [right|left]; inversion H; trivial.
+    now apply Z.le_ge.
+  Defined.
+
   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 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.
+  Lemma i2z_eq n p : i2z n = i2z p -> n = p. Proof. trivial. Qed.
+  Lemma i2z_0 : i2z _0 = 0.  Proof. reflexivity. Qed.
+  Lemma i2z_1 : i2z _1 = 1.  Proof. reflexivity. Qed.
+  Lemma i2z_2 : i2z _2 = 2.  Proof. reflexivity. Qed.
+  Lemma i2z_3 : i2z _3 = 3.  Proof. reflexivity. Qed.
+  Lemma i2z_add n p : i2z (n + p) = i2z n + i2z p.
+  Proof. reflexivity. Qed.
+  Lemma i2z_opp n : i2z (- n) = - i2z n.
+  Proof. reflexivity. Qed.
+  Lemma i2z_sub n p : i2z (n - p) = i2z n - i2z p.
+  Proof. reflexivity. Qed.
+  Lemma i2z_mul n p : i2z (n * p) = i2z n * i2z p.
+  Proof. reflexivity. Qed.
+  Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p).
+  Proof. reflexivity. Qed.
+  Lemma i2z_eqb n p : eqb n p = Z.eqb (i2z n) (i2z p).
+  Proof. reflexivity. Qed.
+  Lemma i2z_leb n p : leb n p = Z.leb (i2z n) (i2z p).
+  Proof. reflexivity. Qed.
+  Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p).
+  Proof. reflexivity. Qed.
+
 End Z_as_Int.