Integer division: quot and rem (trunc convention) in addition to div and mod

(floor convention).

We follow Haskell naming convention: quot and rem are for
Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf.
the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom
(a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷
for quot, and infix rem for rem (which is actually remainder in
full). This way, both conventions can be used at the same time.

Definitions (and proofs of specifications) for div mod quot rem are
migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With
this new organisation, no need for functor application in Zdiv and
Zquot.

On the abstract side, ZAxiomsSig now provides div mod quot rem.
Zproperties now contains properties of them. In NZDiv, we stop
splitting specifications in Common vs. Specific parts. Instead,
the NZ specification is be extended later, even if this leads to
a useless mod_bound_pos, subsumed by more precise axioms.

A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff).

A few proofs in Nnat, Znat, Zabs are reworked (no more dependency
to Zmin, Zmax).

A lcm (least common multiple) is derived abstractly from gcd and
division (and hence available for nat N BigN Z BigZ :-).
In these new files NLcm and ZLcm, we also provide some combined
properties of div mod quot rem gcd.

We also provide a new file Zeuclid implementing a third division
convention, where the remainder is always positive. This file
instanciate the abstract one ZDivEucl. Operation names are
ZEuclid.div and ZEuclid.modulo.

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

1 files changed, 18 insertions, 14 deletions

diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 8443325ef..8543652c6 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -11,8 +11,8 @@
 Require Import Arith_base.
 Require Import BinPos.
 Require Import BinInt.
+Require Import Zcompare.
 Require Import Zorder.
-Require Import Zmax.
 Require Import Znat.
 Require Import ZArith_dec.
 
@@ -149,33 +149,37 @@ Proof.
   apply Zplus_le_0_compat; auto.
 Qed.
 
-Lemma Zabs_nat_Zminus:
- forall x y, 0 <= x <= y ->  Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
+Lemma Zabs_nat_compare :
+ forall x y, 0<=x -> 0<=y -> nat_compare (Zabs_nat x) (Zabs_nat y) = (x?=y).
 Proof.
-  intros x y (H,H').
-  assert (0 <= y) by (apply Zle_trans with x; auto).
-  assert (0 <= y-x) by (apply Zle_minus_le_0; auto).
-  apply inj_eq_rev.
-  rewrite inj_minus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
-  rewrite Zmax_right; auto.
+ intros. rewrite <- inj_compare, 2 inj_Zabs_nat, 2 Zabs_eq; trivial.
 Qed.
 
 Lemma Zabs_nat_le :
   forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
 Proof.
-  intros n m (H,H'); apply inj_le_rev.
-  repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
-  apply Zle_trans with n; auto.
+ intros n m (H,H'). apply nat_compare_le. rewrite Zabs_nat_compare; trivial.
+ apply Zle_trans with n; auto.
 Qed.
 
 Lemma Zabs_nat_lt :
   forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
 Proof.
-  intros n m (H,H'); apply inj_lt_rev.
-  repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
+  intros n m (H,H'). apply nat_compare_lt. rewrite Zabs_nat_compare; trivial.
   apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
 Qed.
 
+Lemma Zabs_nat_Zminus:
+ forall x y, 0 <= x <= y ->  Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
+Proof.
+  intros x y (H,H').
+  assert (0 <= y) by (apply Zle_trans with x; auto).
+  assert (0 <= y-x) by (apply Zle_minus_le_0; auto).
+  apply inj_eq_rev.
+  rewrite inj_minus1. rewrite !inj_Zabs_nat, !Zabs_eq; auto.
+  apply Zabs_nat_le. now split.
+Qed.
+
 (** * Some results about the sign function. *)
 
 Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.