Arithemtic: more concerning compare, eqb, leb, ltb

 Start of a uniform treatment of compare, eqb, leb, ltb:
 - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
 - Some generic properties are derived in OrdersFacts.BoolOrderFacts

 In BinPos, more work about sub_mask with nice implications
 on compare (e.g. simplier proof of lt_trans).

 In BinNat/BinPos, for uniformity, compare_antisym is now
 (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.

 In BigN / BigZ, eq_bool is now eqb

 In BinIntDef, gtb and geb are kept for the moment, but
 a comment advise to rather use ltb and leb. Z.div now uses
 Z.ltb and Z.leb.

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

2 files changed, 72 insertions, 38 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index f186c55b44..6626484321 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Znumtheory.
+Require Import BinInt.
 
 Open Scope Z_scope.
 
@@ -35,7 +35,9 @@ Module Type NType.
  Definition le n m := [n] <= [m].
 
  Parameter compare : t -> t -> comparison.
- Parameter eq_bool : t -> t -> bool.
+ Parameter eqb : t -> t -> bool.
+ Parameter ltb : t -> t -> bool.
+ Parameter leb : t -> t -> bool.
  Parameter max : t -> t -> t.
  Parameter min : t -> t -> t.
  Parameter zero : t.
@@ -67,39 +69,41 @@ Module Type NType.
  Parameter lxor : t -> t -> t.
  Parameter div2 : t -> t.
 
- Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
- Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
- Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
+ Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]).
+ Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]).
+ Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]).
+ Parameter spec_max : forall x y, [max x y] = Z.max [x] [y].
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
  Parameter spec_2: [two] = 2.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
- Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
- Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
+ Parameter spec_pred: forall x, [pred x] = Z.max 0 ([x] - 1).
+ Parameter spec_sub: forall x y, [sub x y] = Z.max 0 ([x] - [y]).
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
  Parameter spec_square: forall x, [square x] = [x] *  [x].
  Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
+ Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Z.log2 [x].
  Parameter spec_div_eucl: forall x y,
-  let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+  let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_even: forall x, even x = Zeven_bool [x].
- Parameter spec_odd: forall x, odd x = Zodd_bool [x].
- Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
- Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
- Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
- Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
- Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
- Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
- Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ Parameter spec_even: forall x, even x = Z.even [x].
+ Parameter spec_odd: forall x, odd x = Z.odd [x].
+ Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Z.div2 [x].
 
 End NType.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 84682820db..878e46fea5 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith Nnat Ndigits NAxioms NDiv NSig.
+Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
@@ -15,8 +15,8 @@ Module NTypeIsNAxioms (Import N : NType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
- spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt
- spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
+ spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
+ spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
  spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
  spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
  : nsimpl.
@@ -126,36 +126,66 @@ Qed.
 
 (** Order *)
 
-Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
+Lemma eqb_eq x y : eqb x y = true <-> x == y.
 Proof.
- intros. zify. destruct (Zcompare_spec [x] [y]); auto.
+ zify. apply Z.eqb_eq.
 Qed.
 
-Definition eqb := eq_bool.
+Lemma leb_le x y : leb x y = true <-> x <= y.
+Proof.
+ zify. apply Z.leb_le.
+Qed.
+
+Lemma ltb_lt x y : ltb x y = true <-> x < y.
+Proof.
+ zify. apply Z.ltb_lt.
+Qed.
+
+Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
+Proof.
+ intros. zify. apply Z.compare_eq_iff.
+Qed.
+
+Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
+
+Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
 
-Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
 Proof.
- intros. zify. symmetry. apply Zeq_is_eq_bool.
+ intros. zify. apply Z.compare_antisym.
 Qed.
 
+Include BoolOrderFacts N N N [no inline].
+
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
-intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
 Proof.
-intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
 Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Theorem lt_irrefl : forall n, ~ n < n.
+Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
 Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
+Qed.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Proof.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
 Qed.
 
 Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
@@ -474,5 +504,5 @@ Qed.
 End NTypeIsNAxioms.
 
 Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: HasCompare N <: HasEqBool N <: HasMinMax N
+ <: NAxiomsSig <: OrderFunctions N <: HasMinMax N
  := N <+ NTypeIsNAxioms.