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

1 files changed, 10 insertions, 12 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index a5f42d6d1..ff221f35e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -600,12 +600,12 @@ Fixpoint Zmod_POS (a : positive) (b : Z) : Z  :=
    | xI a' =>
       let r := Zmod_POS a' b in
       let r' := (2 * r + 1) in
-      if Zgt_bool b r' then r' else (r' - b)
+      if r' <? b then r' else (r' - b)
    | xO a' =>
       let r := Zmod_POS a' b in
       let r' := (2 * r) in
-      if Zgt_bool b r' then r' else (r' - b)
-   | xH => if Zge_bool b 2 then 1 else 0
+      if r' <? b then r' else (r' - b)
+   | xH => if 2 <=? b then 1 else 0
   end.
 
 Definition Zmod' a b :=
@@ -630,16 +630,14 @@ Definition Zmod' a b :=
   end.
 
 
-Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)).
+Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Zdiv_eucl_POS a b).
 Proof.
-  intros a b; elim a; simpl; auto.
-  intros p Rec; rewrite  Rec.
-  case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto.
-  match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto.
-  intros p Rec; rewrite  Rec.
-  case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto.
-  match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto.
-  case (Zge_bool b 2); auto.
+  induction a as [a IH|a IH| ]; simpl; rewrite ?IH.
+  destruct (Z.pos_div_eucl a b) as (p,q); simpl;
+   case Z.ltb_spec; reflexivity.
+  destruct (Z.pos_div_eucl a b) as (p,q); simpl;
+   case Z.ltb_spec; reflexivity.
+  case Z.leb_spec; trivial.
 Qed.
 
 Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b.