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

2 files changed, 46 insertions, 7 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index b2bf8703ea..72137eccf7 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -19,17 +19,14 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
     - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith
     - [ZTypeIsZAxioms] shows (mainly) that these operations implement
       the interface [ZAxioms]
-    - [ZPropSig] adds all generic properties derived from [ZAxioms]
-    - [ZDivPropFunct] provides generic properties of [div] and [mod]
-      ("Floor" variant)
+    - [ZProp] adds all generic properties derived from [ZAxioms]
     - [MinMax*Properties] provides properties of [min] and [max]
 
 *)
 
 
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
- ZMake.Make BigN <+ ZTypeIsZAxioms
- <+ !ZProp <+ !ZDivProp <+ HasEqBool2Dec
+ ZMake.Make BigN <+ ZTypeIsZAxioms <+ !ZProp <+ HasEqBool2Dec
  <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 
 (** Notations about [BigZ] *)
@@ -67,6 +64,8 @@ Arguments Scope BigZ.log2 [bigZ_scope].
 Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.remainder [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.even [bigZ_scope].
 Arguments Scope BigZ.odd [bigZ_scope].
@@ -92,7 +91,9 @@ Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope.
 Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
-Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope.
+Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
+Infix "rem" := BigZ.remainder (at level 40, no associativity) : bigZ_scope.
+Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
 Local Open Scope bigZ_scope.
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index b341b32095..f4baf32bc4 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith.
+Require Import ZArith Zquot.
 Require Import BigNumPrelude.
 Require Import NSig.
 Require Import ZSig.
@@ -453,6 +453,44 @@ Module Make (N:NType) <: ZType.
  intros q r q11 r1 H; injection H; auto.
  Qed.
 
+ Definition quot x y :=
+  match x, y with
+  | Pos nx, Pos ny => Pos (N.div nx ny)
+  | Pos nx, Neg ny => Neg (N.div nx ny)
+  | Neg nx, Pos ny => Neg (N.div nx ny)
+  | Neg nx, Neg ny => Pos (N.div nx ny)
+  end.
+
+ Definition remainder x y :=
+  if eq_bool y zero then x
+  else
+    match x, y with
+      | Pos nx, Pos ny => Pos (N.modulo nx ny)
+      | Pos nx, Neg ny => Pos (N.modulo nx ny)
+      | Neg nx, Pos ny => Neg (N.modulo nx ny)
+      | Neg nx, Neg ny => Neg (N.modulo nx ny)
+    end.
+
+ Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
+ Proof.
+  intros [x|x] [y|y]; simpl; symmetry;
+   rewrite N.spec_div, ?Zquot_opp_r, ?Zquot_opp_l, ?Zopp_involutive;
+   rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
+ Qed.
+
+ Lemma spec_remainder : forall x y,
+   to_Z (remainder x y) = (to_Z x) rem (to_Z y).
+ Proof.
+  intros x y. unfold remainder. rewrite spec_eq_bool, spec_0.
+  assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
+  now rewrite Hy, Zrem_0_r.
+  destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
+   rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
+   try rewrite Z.eq_opp_l, Z.opp_0 in Hy;
+   rewrite Zrem_Zmod_pos; generalize (N.spec_pos x) (N.spec_pos y);
+   z_order.
+ Qed.
+
  Definition gcd x y :=
   match x, y with
   | Pos nx, Pos ny => Pos (N.gcd nx ny)