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, 39 insertions, 8 deletions

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b5c761a6f2..c2a173e22a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -55,6 +55,8 @@ Module Type ZType.
  Parameter div_eucl : t -> t -> t * t.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
+ Parameter quot : t -> t -> t.
+ Parameter remainder : t -> t -> t.
  Parameter gcd : t -> t -> t.
  Parameter sgn : t -> t.
  Parameter abs : t -> t.
@@ -85,6 +87,8 @@ Module Type ZType.
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_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_quot: forall x y, [quot x y] = [x] ÷ [y].
+ Parameter spec_remainder: forall x y, [remainder x y] = [x] rem [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 999e7cd03e..6a823a7324 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,13 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
-
-(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig]
-
-    It also provides [sgn], [abs], [div], [mod]
-*)
+Require Import ZArith Nnat ZAxioms ZSig.
 
+(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
 Module ZTypeIsZAxioms (Import Z : ZType').
 
@@ -20,7 +16,8 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd
+ spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot
+ spec_remainder
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -349,6 +346,36 @@ Proof.
 intros a b. zify. intros. apply Z_mod_neg; auto with zarith.
 Qed.
 
+Definition mod_bound_pos :
+ forall a b, 0<=a -> 0<b -> 0 <= modulo a b /\ modulo a b < b :=
+ fun a b _ H => mod_pos_bound a b H.
+
+(** Quot / Rem *)
+
+Program Instance quot_wd : Proper (eq==>eq==>eq) quot.
+Program Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+
+Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + (remainder a b).
+Proof.
+intros a b _. zify. apply Z_quot_rem_eq.
+Qed.
+
+Theorem rem_bound_pos :
+ forall a b, 0<=a -> 0<b -> 0 <= remainder a b /\ remainder a b < b.
+Proof.
+intros a b. zify. intros. now apply Zrem_bound.
+Qed.
+
+Theorem rem_opp_l : forall a b, ~b==0 -> remainder (-a) b == -(remainder a b).
+Proof.
+intros a b _. zify. apply Zrem_opp_l.
+Qed.
+
+Theorem rem_opp_r : forall a b, ~b==0 -> remainder a (-b) == remainder a b.
+Proof.
+intros a b _. zify. apply Zrem_opp_r.
+Qed.
+
 (** Gcd *)
 
 Definition divide n m := exists p, n*p == m.
@@ -384,5 +411,5 @@ Qed.
 End ZTypeIsZAxioms.
 
 Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
+ <: ZAxiomsSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
  := Z <+ ZTypeIsZAxioms.