diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-10 12:58:38 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-10 12:58:38 +0000 |
| commit | f1da4e3df5abd1daa5bfee184512f1e363bc9688 (patch) | |
| tree | 4dc54964cdf6cf05b9d060fb6ed0f5898a2bad41 | |
| parent | 51f5f4d37fdc3db1e7da951db11119bdb5a7554b (diff) | |
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
36 files changed, 2342 insertions, 1419 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 43761b0ab..02c1e928d 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -184,7 +184,10 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpower.v + theories/ZArith/Zdiv_def.v theories/ZArith/Zdiv.v + theories/ZArith/Zquot.v + theories/ZArith/Zeuclid.v theories/ZArith/Zlog_def.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) @@ -193,8 +196,6 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zwf.v theories/ZArith/Znumtheory.v theories/ZArith/Int.v - theories/ZArith/ZOdiv_def.v - theories/ZArith/ZOdiv.v theories/ZArith/Zpow_facts.v theories/ZArith/Zdigits.v </dd> @@ -289,6 +290,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/Abstract/NSqrt.v theories/Numbers/Natural/Abstract/NLog.v theories/Numbers/Natural/Abstract/NGcd.v + theories/Numbers/Natural/Abstract/NLcm.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v @@ -316,6 +318,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Abstract/ZParity.v theories/Numbers/Integer/Abstract/ZPow.v theories/Numbers/Integer/Abstract/ZGcd.v + theories/Numbers/Integer/Abstract/ZLcm.v theories/Numbers/Integer/Abstract/ZProperties.v theories/Numbers/Integer/Abstract/ZDivEucl.v theories/Numbers/Integer/Abstract/ZDivFloor.v diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 67bb93092..cd59b7cb6 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -13,7 +13,7 @@ Require Import BinNat. Require Import Setoid. Require Import Ring_theory. Require Import Ring_polynom. -Require Import Ndiv_def ZOdiv_def. +Require Import Ndiv_def Zdiv_def. Import List. Set Implicit Arguments. @@ -630,10 +630,10 @@ Qed. Variable zphi : Z -> R. - Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi ZOdiv_eucl. + Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi Zquotrem. Proof. constructor. - intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_eucl; intros; subst. + intros; generalize (Zquotrem_eq a b); case Zquotrem; intros; subst. rewrite Zmult_comm; rsimpl. Qed. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index e950021f0..93fdfff7a 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -16,8 +16,6 @@ Require Import BinPos. Require Import BinNat. Require Import BinInt. Require Import Pnat. -Require Import Zmax. -Require Import Zmin. Require Import Znat. (** Translation from [N] to [nat] and back. *) diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 754c0b3d1..89fa8e170 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export NZAxioms. -Require Import NZPow NZSqrt NZLog NZGcd. +Require Import NZPow NZSqrt NZLog NZGcd NZDiv. (** We obtain integers by postulating that successor of predecessor is identity. *) @@ -70,16 +70,56 @@ Module Type Parity (Import Z : ZAxiomsMiniSig'). Axiom odd_spec : forall n, odd n = true <-> Odd n. End Parity. +(** Divisions *) + +(** First, the usual Coq convention of Truncated-Toward-Bottom + (a.k.a Floor). We simply extend the NZ signature. *) + +Module Type ZDivSpecific (Import A:ZAxiomsMiniSig')(Import B : DivMod' A). + Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b. + Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0. +End ZDivSpecific. + +Module Type ZDiv (Z:ZAxiomsMiniSig) := NZDiv.NZDiv Z <+ ZDivSpecific Z. +Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z. + +(** Then, the Truncated-Toward-Zero convention. + For not colliding with Floor operations, we use different names +*) + +Module Type QuotRem (Import A : Typ). + Parameters Inline quot remainder : t -> t -> t. +End QuotRem. + +Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A). + Infix "÷" := quot (at level 40, left associativity). + Infix "rem" := remainder (at level 40, no associativity). +End QuotRemNotation. + +Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A. + +Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A). + Declare Instance quot_wd : Proper (eq==>eq==>eq) quot. + Declare Instance rem_wd : Proper (eq==>eq==>eq) remainder. + Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b). + Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b. + Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b). + Axiom rem_opp_r : forall a b, b ~= 0 -> a rem (-b) == a rem b. +End QuotRemSpec. + +Module Type ZQuot (Z:ZAxiomsMiniSig) := QuotRem Z <+ QuotRemSpec Z. +Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z. + (** For pow sqrt log2 gcd, the NZ axiomatizations are enough. *) (** Let's group everything *) Module Type ZAxiomsSig := ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd. + <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd + <+ ZDiv <+ ZQuot. + Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'. - - -(** Division is left apart, since many different flavours are available *) + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' + <+ ZDiv' <+ ZQuot'. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 129785bad..070003972 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. + (** * Euclidean Division for integers, Euclid convention We use here the "usual" formulation of the Euclid Theorem @@ -19,37 +21,29 @@ Vol. 14, No.2, pp. 127-144, April 1992. See files [ZDivTrunc] and [ZDivFloor] for others conventions. -*) - -Require Import ZAxioms ZProperties NZDiv. - -Module Type ZDivSpecific (Import Z : ZAxiomsSig')(Import DM : DivMod' Z). - Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b. -End ZDivSpecific. -Module Type ZDiv (Z:ZAxiomsSig) - := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. + We simply extend NZDiv with a bound for modulo that holds + regardless of the sign of a and b. This new specification + subsume mod_bound_pos, which nonetheless stays there for + subtyping. Note also that ZAxiomSig now already contain + a div and a modulo (that follow the Floor convention). + We just ignore them here. +*) -Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +End EuclidSpec. -Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). +Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. +Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. -(** We benefit from what already exists for NZ *) +Module ZEuclidProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B) + (Import D : ZEuclid' A). - Module ZD <: NZDiv Z. - Definition div := div. - Definition modulo := modulo. - Definition div_wd := div_wd. - Definition mod_wd := mod_wd. - Definition div_mod := div_mod. - Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Proof. - intros. rewrite <- (abs_eq b) at 3 by now apply lt_le_incl. - apply mod_always_pos. - Qed. - End ZD. - Module Import NZDivP := Nop <+ NZDivProp Z ZD ZP. + Module Import NZDivP := Nop <+ NZDivProp A D B. (** Another formulation of the main equation *) @@ -117,7 +111,7 @@ Lemma div_opp_r : forall a b, b~=0 -> a/(-b) == -(a/b). Proof. intros. symmetry. apply div_unique with (a mod b). -rewrite abs_opp; apply mod_always_pos. +rewrite abs_opp; now apply mod_always_pos. rewrite mul_opp_opp; now apply div_mod. Qed. @@ -125,7 +119,7 @@ Lemma mod_opp_r : forall a b, b~=0 -> a mod (-b) == a mod b. Proof. intros. symmetry. apply mod_unique with (-(a/b)). -rewrite abs_opp; apply mod_always_pos. +rewrite abs_opp; now apply mod_always_pos. rewrite mul_opp_opp; now apply div_mod. Qed. @@ -296,7 +290,7 @@ intros a b Hb. split. intros EQ. rewrite (div_mod a b Hb), EQ; nzsimpl. -apply mod_always_pos. +now apply mod_always_pos. intros. pos_or_neg b. apply div_small. now rewrite <- (abs_eq b). @@ -365,7 +359,7 @@ intros. nzsimpl. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. -destruct (mod_always_pos a b). +destruct (mod_always_pos a b). order. rewrite abs_eq in *; order. Qed. @@ -375,7 +369,7 @@ intros a b Hb. rewrite mul_pred_r, <- add_opp_r. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. -destruct (mod_always_pos a b). +destruct (mod_always_pos a b). order. rewrite <- opp_pos_neg in Hb. rewrite abs_neq' in *; order. Qed. @@ -469,7 +463,7 @@ apply div_unique with ((a mod b)*c). (* ineqs *) rewrite abs_mul, (abs_eq c) by order. rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial. -apply mod_always_pos. +now apply mod_always_pos. (* equation *) rewrite (div_mod a b) at 1 by order. rewrite mul_add_distr_r. @@ -566,7 +560,7 @@ Proof. apply div_unique with (b*((a/b) mod c) + a mod b). (* begin 0<= ... <abs(b*c) *) rewrite abs_mul. - destruct (mod_always_pos (a/b) c), (mod_always_pos a b). + destruct (mod_always_pos (a/b) c), (mod_always_pos a b); try order. split. apply add_nonneg_nonneg; trivial. apply mul_nonneg_nonneg; order. @@ -590,16 +584,15 @@ Proof. exact div_mul_le. Qed. (** mod is related to divisibility *) Lemma mod_divides : forall a b, b~=0 -> - (a mod b == 0 <-> exists c, a == b*c). + (a mod b == 0 <-> (b|a)). Proof. intros a b Hb. split. -intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1. +intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2. rewrite Hab; now nzsimpl. intros (c,Hc). -rewrite Hc, mul_comm. +rewrite <- Hc, mul_comm. now apply mod_mul. Qed. - -End ZDivProp. +End ZEuclidProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index fd962024c..5f52f046f 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. + (** * Euclidean Division for integers (Floor convention) We use here the convention known as Floor, or Round-Toward-Bottom, @@ -24,33 +26,13 @@ See files [ZDivTrunc] and [ZDivEucl] for others conventions. *) -Require Import ZAxioms ZProperties NZDiv. - -Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z). - Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b. - Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0. -End ZDivSpecific. - -Module Type ZDiv (Z:ZAxiomsSig) - := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. - -Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. - -Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). +Module Type ZDivProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B). (** We benefit from what already exists for NZ *) - - Module ZD <: NZDiv Z. - Definition div := div. - Definition modulo := modulo. - Definition div_wd := div_wd. - Definition mod_wd := mod_wd. - Definition div_mod := div_mod. - Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Proof. intros. now apply mod_pos_bound. Qed. - End ZD. - Module Import NZDivP := Nop <+ NZDivProp Z ZD ZP. +Module Import NZDivP := Nop <+ NZDivProp A A B. (** Another formulation of the main equation *) @@ -62,6 +44,18 @@ rewrite <- add_move_l. symmetry. now apply div_mod. Qed. +(** We have a general bound for absolute values *) + +Lemma mod_bound_abs : + forall a b, b~=0 -> abs (a mod b) < abs b. +Proof. +intros. +destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ. +destruct (mod_pos_bound a b). order. now rewrite abs_eq. +destruct (mod_neg_bound a b). order. rewrite abs_neq; trivial. +now rewrite <- opp_lt_mono. +Qed. + (** Uniqueness theorems *) Theorem div_mod_unique : forall b q1 q2 r1 r2 : t, @@ -230,11 +224,26 @@ rewrite mod_opp_opp, mod_opp_l_nz by trivial. now rewrite opp_sub_distr, add_comm, add_opp_r. Qed. -(** The sign of [a mod b] is the one of [b] *) +(** The sign of [a mod b] is the one of [b] (when it isn't null) *) -(* TODO: a proper sgn function and theory *) +Lemma mod_sign_nz : forall a b, b~=0 -> a mod b ~= 0 -> + sgn (a mod b) == sgn b. +Proof. +intros a b Hb H. destruct (lt_ge_cases 0 b) as [Hb'|Hb']. +destruct (mod_pos_bound a b Hb'). rewrite 2 sgn_pos; order. +destruct (mod_neg_bound a b). order. rewrite 2 sgn_neg; order. +Qed. + +Lemma mod_sign : forall a b, b~=0 -> sgn (a mod b) ~= -sgn b. +Proof. +intros a b Hb H. +destruct (eq_decidable (a mod b) 0) as [EQ|NEQ]. +apply Hb, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0. +apply Hb, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'. +apply add_move_0_l. rewrite <- H. symmetry. now apply mod_sign_nz. +Qed. -Lemma mod_sign : forall a b, b~=0 -> (0 <= (a mod b) * b). +Lemma mod_sign_mul : forall a b, b~=0 -> 0 <= (a mod b) * b. Proof. intros. destruct (lt_ge_cases 0 b). apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order. @@ -615,18 +624,5 @@ Theorem div_mul_le: forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. exact div_mul_le. Qed. -(** mod is related to divisibility *) - -Lemma mod_divides : forall a b, b~=0 -> - (a mod b == 0 <-> exists c, a == b*c). -Proof. -intros a b Hb. split. -intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1. - rewrite Hab. now nzsimpl. -intros (c,Hc). -rewrite Hc, mul_comm. -now apply mod_mul. -Qed. - End ZDivProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 4ca692d00..37a0057ed 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. + (** * Euclidean Division for integers (Trunc convention) We use here the convention known as Trunc, or Round-Toward-Zero, @@ -24,25 +26,23 @@ See files [ZDivFloor] and [ZDivEucl] for others conventions. *) -Require Import ZAxioms ZProperties NZDiv. - -Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z). - Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Axiom mod_opp_l : forall a b, b ~= 0 -> (-a) mod b == - (a mod b). - Axiom mod_opp_r : forall a b, b ~= 0 -> a mod (-b) == a mod b. -End ZDivSpecific. - -Module Type ZDiv (Z:ZAxiomsSig) - := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. - -Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. - -Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). +Module Type ZQuotProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B). (** We benefit from what already exists for NZ *) - Module Import NZDivP := Nop <+ NZDivProp Z Z ZP. + Module Quot2Div <: NZDiv A. + Definition div := quot. + Definition modulo := remainder. + Definition div_wd := quot_wd. + Definition mod_wd := rem_wd. + Definition div_mod := quot_rem. + Definition mod_bound_pos := rem_bound_pos. + End Quot2Div. + + Module NZQuot := Nop <+ NZDivProp A Quot2Div B. Ltac pos_or_neg a := let LT := fresh "LT" in @@ -51,175 +51,269 @@ Ltac pos_or_neg a := (** Another formulation of the main equation *) -Lemma mod_eq : - forall a b, b~=0 -> a mod b == a - b*(a/b). +Lemma rem_eq : + forall a b, b~=0 -> a rem b == a - b*(a÷b). Proof. intros. rewrite <- add_move_l. -symmetry. now apply div_mod. +symmetry. now apply quot_rem. Qed. (** A few sign rules (simple ones) *) -Lemma mod_opp_opp : forall a b, b ~= 0 -> (-a) mod (-b) == - (a mod b). -Proof. intros. now rewrite mod_opp_r, mod_opp_l. Qed. +Lemma rem_opp_opp : forall a b, b ~= 0 -> (-a) rem (-b) == - (a rem b). +Proof. intros. now rewrite rem_opp_r, rem_opp_l. Qed. -Lemma div_opp_l : forall a b, b ~= 0 -> (-a)/b == -(a/b). +Lemma quot_opp_l : forall a b, b ~= 0 -> (-a)÷b == -(a÷b). Proof. intros. rewrite <- (mul_cancel_l _ _ b) by trivial. -rewrite <- (add_cancel_r _ _ ((-a) mod b)). -now rewrite <- div_mod, mod_opp_l, mul_opp_r, <- opp_add_distr, <- div_mod. +rewrite <- (add_cancel_r _ _ ((-a) rem b)). +now rewrite <- quot_rem, rem_opp_l, mul_opp_r, <- opp_add_distr, <- quot_rem. Qed. -Lemma div_opp_r : forall a b, b ~= 0 -> a/(-b) == -(a/b). +Lemma quot_opp_r : forall a b, b ~= 0 -> a÷(-b) == -(a÷b). Proof. intros. assert (-b ~= 0) by (now rewrite eq_opp_l, opp_0). rewrite <- (mul_cancel_l _ _ (-b)) by trivial. -rewrite <- (add_cancel_r _ _ (a mod (-b))). -now rewrite <- div_mod, mod_opp_r, mul_opp_opp, <- div_mod. -Qed. - -Lemma div_opp_opp : forall a b, b ~= 0 -> (-a)/(-b) == a/b. -Proof. intros. now rewrite div_opp_r, div_opp_l, opp_involutive. Qed. - -(** The sign of [a mod b] is the one of [a] *) - -(* TODO: a proper sgn function and theory *) - -Lemma mod_sign : forall a b, b~=0 -> 0 <= (a mod b) * a. -Proof. -assert (Aux : forall a b, 0<b -> 0 <= (a mod b) * a). - intros. pos_or_neg a. - apply mul_nonneg_nonneg; trivial. now destruct (mod_bound a b). - rewrite <- mul_opp_opp, <- mod_opp_l by order. - apply mul_nonneg_nonneg; try order. destruct (mod_bound (-a) b); order. -intros. pos_or_neg b. apply Aux; order. -rewrite <- mod_opp_r by order. apply Aux; order. +rewrite <- (add_cancel_r _ _ (a rem (-b))). +now rewrite <- quot_rem, rem_opp_r, mul_opp_opp, <- quot_rem. Qed. +Lemma quot_opp_opp : forall a b, b ~= 0 -> (-a)÷(-b) == a÷b. +Proof. intros. now rewrite quot_opp_r, quot_opp_l, opp_involutive. Qed. (** Uniqueness theorems *) -Theorem div_mod_unique : forall b q1 q2 r1 r2 : t, +Theorem quot_rem_unique : forall b q1 q2 r1 r2 : t, (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2. Proof. intros b q1 q2 r1 r2 Hr1 Hr2 EQ. destruct Hr1; destruct Hr2; try (intuition; order). -apply div_mod_unique with b; trivial. +apply NZQuot.div_mod_unique with b; trivial. rewrite <- (opp_inj_wd r1 r2). -apply div_mod_unique with (-b); trivial. +apply NZQuot.div_mod_unique with (-b); trivial. rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. now rewrite 2 mul_opp_l, <- 2 opp_add_distr, opp_inj_wd. Qed. -Theorem div_unique: - forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a/b. -Proof. intros; now apply div_unique with r. Qed. +Theorem quot_unique: + forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a÷b. +Proof. intros; now apply NZQuot.div_unique with r. Qed. -Theorem mod_unique: - forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a mod b. -Proof. intros; now apply mod_unique with q. Qed. +Theorem rem_unique: + forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a rem b. +Proof. intros; now apply NZQuot.mod_unique with q. Qed. (** A division by itself returns 1 *) -Lemma div_same : forall a, a~=0 -> a/a == 1. +Lemma quot_same : forall a, a~=0 -> a÷a == 1. Proof. -intros. pos_or_neg a. apply div_same; order. -rewrite <- div_opp_opp by trivial. now apply div_same. +intros. pos_or_neg a. apply NZQuot.div_same; order. +rewrite <- quot_opp_opp by trivial. now apply NZQuot.div_same. Qed. -Lemma mod_same : forall a, a~=0 -> a mod a == 0. +Lemma rem_same : forall a, a~=0 -> a rem a == 0. Proof. -intros. rewrite mod_eq, div_same by trivial. nzsimpl. apply sub_diag. +intros. rewrite rem_eq, quot_same by trivial. nzsimpl. apply sub_diag. Qed. (** A division of a small number by a bigger one yields zero. *) -Theorem div_small: forall a b, 0<=a<b -> a/b == 0. -Proof. exact div_small. Qed. +Theorem quot_small: forall a b, 0<=a<b -> a÷b == 0. +Proof. exact NZQuot.div_small. Qed. -(** Same situation, in term of modulo: *) +(** Same situation, in term of remulo: *) -Theorem mod_small: forall a b, 0<=a<b -> a mod b == a. -Proof. exact mod_small. Qed. +Theorem rem_small: forall a b, 0<=a<b -> a rem b == a. +Proof. exact NZQuot.mod_small. Qed. (** * Basic values of divisions and modulo. *) -Lemma div_0_l: forall a, a~=0 -> 0/a == 0. +Lemma quot_0_l: forall a, a~=0 -> 0÷a == 0. Proof. -intros. pos_or_neg a. apply div_0_l; order. -rewrite <- div_opp_opp, opp_0 by trivial. now apply div_0_l. +intros. pos_or_neg a. apply NZQuot.div_0_l; order. +rewrite <- quot_opp_opp, opp_0 by trivial. now apply NZQuot.div_0_l. Qed. -Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0. +Lemma rem_0_l: forall a, a~=0 -> 0 rem a == 0. Proof. -intros; rewrite mod_eq, div_0_l; now nzsimpl. +intros; rewrite rem_eq, quot_0_l; now nzsimpl. Qed. -Lemma div_1_r: forall a, a/1 == a. +Lemma quot_1_r: forall a, a÷1 == a. Proof. -intros. pos_or_neg a. now apply div_1_r. -apply opp_inj. rewrite <- div_opp_l. apply div_1_r; order. +intros. pos_or_neg a. now apply NZQuot.div_1_r. +apply opp_inj. rewrite <- quot_opp_l. apply NZQuot.div_1_r; order. intro EQ; symmetry in EQ; revert EQ; apply lt_neq, lt_0_1. Qed. -Lemma mod_1_r: forall a, a mod 1 == 0. +Lemma rem_1_r: forall a, a rem 1 == 0. Proof. -intros. rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag. +intros. rewrite rem_eq, quot_1_r; nzsimpl; auto using sub_diag. intro EQ; symmetry in EQ; revert EQ; apply lt_neq; apply lt_0_1. Qed. -Lemma div_1_l: forall a, 1<a -> 1/a == 0. -Proof. exact div_1_l. Qed. +Lemma quot_1_l: forall a, 1<a -> 1÷a == 0. +Proof. exact NZQuot.div_1_l. Qed. + +Lemma rem_1_l: forall a, 1<a -> 1 rem a == 1. +Proof. exact NZQuot.mod_1_l. Qed. + +Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a. +Proof. +intros. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order. +rewrite <- quot_opp_opp, <- mul_opp_r by order. apply NZQuot.div_mul; order. +rewrite <- opp_inj_wd, <- quot_opp_l, <- mul_opp_l by order. +apply NZQuot.div_mul; order. +rewrite <- opp_inj_wd, <- quot_opp_r, <- mul_opp_opp by order. +apply NZQuot.div_mul; order. +Qed. + +Lemma rem_mul : forall a b, b~=0 -> (a*b) rem b == 0. +Proof. +intros. rewrite rem_eq, quot_mul by trivial. rewrite mul_comm; apply sub_diag. +Qed. + +(** The sign of [a rem b] is the one of [a] (when it's not null) *) + +Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b. +Proof. + intros. pos_or_neg b. destruct (rem_bound_pos a b); order. + rewrite <- rem_opp_r; trivial. + destruct (rem_bound_pos a (-b)); trivial. +Qed. + +Lemma rem_nonpos : forall a b, b~=0 -> a <= 0 -> a rem b <= 0. +Proof. + intros a b Hb Ha. + apply opp_nonneg_nonpos. apply opp_nonneg_nonpos in Ha. + rewrite <- rem_opp_l by trivial. now apply rem_nonneg. +Qed. -Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1. -Proof. exact mod_1_l. Qed. +Lemma rem_sign_mul : forall a b, b~=0 -> 0 <= (a rem b) * a. +Proof. +intros a b Hb. destruct (le_ge_cases 0 a). + apply mul_nonneg_nonneg; trivial. now apply rem_nonneg. + apply mul_nonpos_nonpos; trivial. now apply rem_nonpos. +Qed. -Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a. +Lemma rem_sign_nz : forall a b, b~=0 -> a rem b ~= 0 -> + sgn (a rem b) == sgn a. Proof. -intros. pos_or_neg a; pos_or_neg b. apply div_mul; order. -rewrite <- div_opp_opp, <- mul_opp_r by order. apply div_mul; order. -rewrite <- opp_inj_wd, <- div_opp_l, <- mul_opp_l by order. apply div_mul; order. -rewrite <- opp_inj_wd, <- div_opp_r, <- mul_opp_opp by order. apply div_mul; order. +intros a b Hb H. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. +rewrite 2 sgn_pos; try easy. + generalize (rem_nonneg a b Hb (lt_le_incl _ _ LT)). order. +now rewrite <- EQ, rem_0_l, sgn_0. +rewrite 2 sgn_neg; try easy. + generalize (rem_nonpos a b Hb (lt_le_incl _ _ LT)). order. Qed. -Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0. +Lemma rem_sign : forall a b, a~=0 -> b~=0 -> sgn (a rem b) ~= -sgn a. Proof. -intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag. +intros a b Ha Hb H. +destruct (eq_decidable (a rem b) 0) as [EQ|NEQ]. +apply Ha, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0. +apply Ha, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'. +apply add_move_0_l. rewrite <- H. symmetry. now apply rem_sign_nz. Qed. -(** * Order results about mod and div *) +(** Operations and absolute value *) + +Lemma rem_abs_l : forall a b, b ~= 0 -> (abs a) rem b == abs (a rem b). +Proof. +intros a b Hb. destruct (le_ge_cases 0 a) as [LE|LE]. +rewrite 2 abs_eq; try easy. now apply rem_nonneg. +rewrite 2 abs_neq, rem_opp_l; try easy. now apply rem_nonpos. +Qed. + +Lemma rem_abs_r : forall a b, b ~= 0 -> a rem (abs b) == a rem b. +Proof. +intros a b Hb. destruct (le_ge_cases 0 b). +now rewrite abs_eq. now rewrite abs_neq, ?rem_opp_r. +Qed. + +Lemma rem_abs : forall a b, b ~= 0 -> (abs a) rem (abs b) == abs (a rem b). +Proof. +intros. now rewrite rem_abs_r, rem_abs_l. +Qed. + +Lemma quot_abs_l : forall a b, b ~= 0 -> (abs a)÷b == (sgn a)*(a÷b). +Proof. +intros a b Hb. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. +rewrite abs_eq, sgn_pos by order. now nzsimpl. +rewrite <- EQ, abs_0, quot_0_l; trivial. now nzsimpl. +rewrite abs_neq, quot_opp_l, sgn_neg by order. + rewrite mul_opp_l. now nzsimpl. +Qed. + +Lemma quot_abs_r : forall a b, b ~= 0 -> a÷(abs b) == (sgn b)*(a÷b). +Proof. +intros a b Hb. destruct (lt_trichotomy 0 b) as [LT|[EQ|LT]]. +rewrite abs_eq, sgn_pos by order. now nzsimpl. +order. +rewrite abs_neq, quot_opp_r, sgn_neg by order. + rewrite mul_opp_l. now nzsimpl. +Qed. + +Lemma quot_abs : forall a b, b ~= 0 -> (abs a)÷(abs b) == abs (a÷b). +Proof. +intros a b Hb. +pos_or_neg a; [rewrite (abs_eq a)|rewrite (abs_neq a)]; + try apply opp_nonneg_nonpos; try order. +pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)]; + try apply opp_nonneg_nonpos; try order. +rewrite abs_eq; try easy. apply NZQuot.div_pos; order. +rewrite <- abs_opp, <- quot_opp_r, abs_eq; try easy. + apply NZQuot.div_pos; order. +pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)]; + try apply opp_nonneg_nonpos; try order. +rewrite <- (abs_opp (_÷_)), <- quot_opp_l, abs_eq; try easy. + apply NZQuot.div_pos; order. +rewrite <- (quot_opp_opp a b), abs_eq; try easy. + apply NZQuot.div_pos; order. +Qed. + +(** We have a general bound for absolute values *) + +Lemma rem_bound_abs : + forall a b, b~=0 -> abs (a rem b) < abs b. +Proof. +intros. rewrite <- rem_abs; trivial. +apply rem_bound_pos. apply abs_nonneg. now apply abs_pos. +Qed. + +(** * Order results about rem and quot *) (** A modulo cannot grow beyond its starting point. *) -Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. -Proof. exact mod_le. Qed. +Theorem rem_le: forall a b, 0<=a -> 0<b -> a rem b <= a. +Proof. exact NZQuot.mod_le. Qed. -Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b. -Proof. exact div_pos. Qed. +Theorem quot_pos : forall a b, 0<=a -> 0<b -> 0<= a÷b. +Proof. exact NZQuot.div_pos. Qed. -Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b. -Proof. exact div_str_pos. Qed. +Lemma quot_str_pos : forall a b, 0<b<=a -> 0 < a÷b. +Proof. exact NZQuot.div_str_pos. Qed. -Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> abs a < abs b). +Lemma quot_small_iff : forall a b, b~=0 -> (a÷b==0 <-> abs a < abs b). Proof. intros. pos_or_neg a; pos_or_neg b. -rewrite div_small_iff; try order. rewrite 2 abs_eq; intuition; order. -rewrite <- opp_inj_wd, opp_0, <- div_opp_r, div_small_iff by order. +rewrite NZQuot.div_small_iff; try order. rewrite 2 abs_eq; intuition; order. +rewrite <- opp_inj_wd, opp_0, <- quot_opp_r, NZQuot.div_small_iff by order. rewrite (abs_eq a), (abs_neq' b); intuition; order. -rewrite <- opp_inj_wd, opp_0, <- div_opp_l, div_small_iff by order. +rewrite <- opp_inj_wd, opp_0, <- quot_opp_l, NZQuot.div_small_iff by order. rewrite (abs_neq' a), (abs_eq b); intuition; order. -rewrite <- div_opp_opp, div_small_iff by order. +rewrite <- quot_opp_opp, NZQuot.div_small_iff by order. rewrite (abs_neq' a), (abs_neq' b); intuition; order. Qed. -Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> abs a < abs b). +Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b). Proof. -intros. rewrite mod_eq, <- div_small_iff by order. +intros. rewrite rem_eq, <- quot_small_iff by order. rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l. rewrite eq_sym_iff, eq_mul_0. tauto. Qed. @@ -227,306 +321,295 @@ Qed. (** As soon as the divisor is strictly greater than 1, the division is strictly decreasing. *) -Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a. -Proof. exact div_lt. Qed. +Lemma quot_lt : forall a b, 0<a -> 1<b -> a÷b < a. +Proof. exact NZQuot.div_lt. Qed. (** [le] is compatible with a positive division. *) -Lemma div_le_mono : forall a b c, 0<c -> a<=b -> a/c <= b/c. +Lemma quot_le_mono : forall a b c, 0<c -> a<=b -> a÷c <= b÷c. Proof. -intros. pos_or_neg a. apply div_le_mono; auto. +intros. pos_or_neg a. apply NZQuot.div_le_mono; auto. pos_or_neg b. apply le_trans with 0. - rewrite <- opp_nonneg_nonpos, <- div_opp_l by order. - apply div_pos; order. - apply div_pos; order. -rewrite opp_le_mono in *. rewrite <- 2 div_opp_l by order. - apply div_le_mono; intuition; order. + rewrite <- opp_nonneg_nonpos, <- quot_opp_l by order. + apply quot_pos; order. + apply quot_pos; order. +rewrite opp_le_mono in *. rewrite <- 2 quot_opp_l by order. + apply NZQuot.div_le_mono; intuition; order. Qed. (** With this choice of division, - rounding of div is always done toward zero: *) + rounding of quot is always done toward zero: *) -Lemma mul_div_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a/b) <= a. +Lemma mul_quot_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a÷b) <= a. Proof. intros. pos_or_neg b. split. -apply mul_nonneg_nonneg; [|apply div_pos]; order. -apply mul_div_le; order. -rewrite <- mul_opp_opp, <- div_opp_r by order. +apply mul_nonneg_nonneg; [|apply quot_pos]; order. +apply NZQuot.mul_div_le; order. +rewrite <- mul_opp_opp, <- quot_opp_r by order. split. -apply mul_nonneg_nonneg; [|apply div_pos]; order. -apply mul_div_le; order. +apply mul_nonneg_nonneg; [|apply quot_pos]; order. +apply NZQuot.mul_div_le; order. Qed. -Lemma mul_div_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a/b) <= 0. +Lemma mul_quot_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a÷b) <= 0. Proof. intros. -rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-div_opp_l by order. +rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. -destruct (mul_div_le (-a) b); tauto. +destruct (mul_quot_le (-a) b); tauto. Qed. -(** For positive numbers, considering [S (a/b)] leads to an upper bound for [a] *) +(** For positive numbers, considering [S (a÷b)] leads to an upper bound for [a] *) -Lemma mul_succ_div_gt: forall a b, 0<=a -> 0<b -> a < b*(S (a/b)). -Proof. exact mul_succ_div_gt. Qed. +Lemma mul_succ_quot_gt: forall a b, 0<=a -> 0<b -> a < b*(S (a÷b)). +Proof. exact NZQuot.mul_succ_div_gt. Qed. (** Similar results with negative numbers *) -Lemma mul_pred_div_lt: forall a b, a<=0 -> 0<b -> b*(P (a/b)) < a. +Lemma mul_pred_quot_lt: forall a b, a<=0 -> 0<b -> b*(P (a÷b)) < a. Proof. intros. -rewrite opp_lt_mono, <- mul_opp_r, opp_pred, <- div_opp_l by order. +rewrite opp_lt_mono, <- mul_opp_r, opp_pred, <- quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. -now apply mul_succ_div_gt. +now apply mul_succ_quot_gt. Qed. -Lemma mul_pred_div_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a/b)). +Lemma mul_pred_quot_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a÷b)). Proof. intros. -rewrite <- mul_opp_opp, opp_pred, <- div_opp_r by order. +rewrite <- mul_opp_opp, opp_pred, <- quot_opp_r by order. rewrite <- opp_pos_neg in *. -now apply mul_succ_div_gt. +now apply mul_succ_quot_gt. Qed. -Lemma mul_succ_div_lt: forall a b, a<=0 -> b<0 -> b*(S (a/b)) < a. +Lemma mul_succ_quot_lt: forall a b, a<=0 -> b<0 -> b*(S (a÷b)) < a. Proof. intros. -rewrite opp_lt_mono, <- mul_opp_l, <- div_opp_opp by order. +rewrite opp_lt_mono, <- mul_opp_l, <- quot_opp_opp by order. rewrite <- opp_nonneg_nonpos, <- opp_pos_neg in *. -now apply mul_succ_div_gt. +now apply mul_succ_quot_gt. Qed. -(** Inequality [mul_div_le] is exact iff the modulo is zero. *) +(** Inequality [mul_quot_le] is exact iff the modulo is zero. *) -Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). +Lemma quot_exact : forall a b, b~=0 -> (a == b*(a÷b) <-> a rem b == 0). Proof. -intros. rewrite mod_eq by order. rewrite sub_move_r; nzsimpl; tauto. +intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto. Qed. -(** Some additionnal inequalities about div. *) +(** Some additionnal inequalities about quot. *) -Theorem div_lt_upper_bound: - forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q. -Proof. exact div_lt_upper_bound. Qed. +Theorem quot_lt_upper_bound: + forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q. +Proof. exact NZQuot.div_lt_upper_bound. Qed. -Theorem div_le_upper_bound: - forall a b q, 0<b -> a <= b*q -> a/b <= q. +Theorem quot_le_upper_bound: + forall a b q, 0<b -> a <= b*q -> a÷b <= q. Proof. intros. -rewrite <- (div_mul q b) by order. -apply div_le_mono; trivial. now rewrite mul_comm. +rewrite <- (quot_mul q b) by order. +apply quot_le_mono; trivial. now rewrite mul_comm. Qed. -Theorem div_le_lower_bound: - forall a b q, 0<b -> b*q <= a -> q <= a/b. +Theorem quot_le_lower_bound: + forall a b q, 0<b -> b*q <= a -> q <= a÷b. Proof. intros. -rewrite <- (div_mul q b) by order. -apply div_le_mono; trivial. now rewrite mul_comm. +rewrite <- (quot_mul q b) by order. +apply quot_le_mono; trivial. now rewrite mul_comm. Qed. (** A division respects opposite monotonicity for the divisor *) -Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p/r <= p/q. -Proof. exact div_le_compat_l. Qed. +Lemma quot_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p÷r <= p÷q. +Proof. exact NZQuot.div_le_compat_l. Qed. -(** * Relations between usual operations and mod and div *) +(** * Relations between usual operations and rem and quot *) (** Unlike with other division conventions, some results here aren't always valid, and need to be restricted. For instance - [(a+b*c) mod c <> a mod c] for [a=9,b=-5,c=2] *) + [(a+b*c) rem c <> a rem c] for [a=9,b=-5,c=2] *) -Lemma mod_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> - (a + b * c) mod c == a mod c. +Lemma rem_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> + (a + b * c) rem c == a rem c. Proof. -assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) mod c == a mod c). - intros. pos_or_neg c. apply mod_add; order. - rewrite <- (mod_opp_r a), <- (mod_opp_r (a+b*c)) by order. +assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) rem c == a rem c). + intros. pos_or_neg c. apply NZQuot.mod_add; order. + rewrite <- (rem_opp_r a), <- (rem_opp_r (a+b*c)) by order. rewrite <- mul_opp_opp in *. - apply mod_add; order. + apply NZQuot.mod_add; order. intros a b c Hc Habc. destruct (le_0_mul _ _ Habc) as [(Habc',Ha)|(Habc',Ha)]. auto. apply opp_inj. revert Ha Habc'. rewrite <- 2 opp_nonneg_nonpos. -rewrite <- 2 mod_opp_l, opp_add_distr, <- mul_opp_l by order. auto. +rewrite <- 2 rem_opp_l, opp_add_distr, <- mul_opp_l by order. auto. Qed. -Lemma div_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> - (a + b * c) / c == a / c + b. +Lemma quot_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> + (a + b * c) ÷ c == a ÷ c + b. Proof. intros. rewrite <- (mul_cancel_l _ _ c) by trivial. -rewrite <- (add_cancel_r _ _ ((a+b*c) mod c)). -rewrite <- div_mod, mod_add by trivial. -now rewrite mul_add_distr_l, add_shuffle0, <-div_mod, mul_comm. +rewrite <- (add_cancel_r _ _ ((a+b*c) rem c)). +rewrite <- quot_rem, rem_add by trivial. +now rewrite mul_add_distr_l, add_shuffle0, <-quot_rem, mul_comm. Qed. -Lemma div_add_l: forall a b c, b~=0 -> 0 <= (a*b+c)*c -> - (a * b + c) / b == a + c / b. +Lemma quot_add_l: forall a b c, b~=0 -> 0 <= (a*b+c)*c -> + (a * b + c) ÷ b == a + c ÷ b. Proof. - intros a b c. rewrite add_comm, (add_comm a). now apply div_add. + intros a b c. rewrite add_comm, (add_comm a). now apply quot_add. Qed. (** Cancellations. *) -Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> - (a*c)/(b*c) == a/b. +Lemma quot_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> + (a*c)÷(b*c) == a÷b. Proof. -assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)/(b*c) == a/b). - intros. pos_or_neg c. apply div_mul_cancel_r; order. - rewrite <- div_opp_opp, <- 2 mul_opp_r. apply div_mul_cancel_r; order. +assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)÷(b*c) == a÷b). + intros. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order. + rewrite <- quot_opp_opp, <- 2 mul_opp_r. apply NZQuot.div_mul_cancel_r; order. rewrite <- neq_mul_0; intuition order. -assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)/(b*c) == a/b). +assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b). intros. pos_or_neg b. apply Aux1; order. - apply opp_inj. rewrite <- 2 div_opp_r, <- mul_opp_l; try order. apply Aux1; order. + apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_l; try order. apply Aux1; order. rewrite <- neq_mul_0; intuition order. intros. pos_or_neg a. apply Aux2; order. -apply opp_inj. rewrite <- 2 div_opp_l, <- mul_opp_l; try order. apply Aux2; order. +apply opp_inj. rewrite <- 2 quot_opp_l, <- mul_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0; intuition order. Qed. -Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> - (c*a)/(c*b) == a/b. +Lemma quot_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> + (c*a)÷(c*b) == a÷b. Proof. -intros. rewrite !(mul_comm c); now apply div_mul_cancel_r. +intros. rewrite !(mul_comm c); now apply quot_mul_cancel_r. Qed. -Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 -> - (a*c) mod (b*c) == (a mod b) * c. +Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 -> + (a*c) rem (b*c) == (a rem b) * c. Proof. intros. assert (b*c ~= 0) by (rewrite <- neq_mul_0; tauto). -rewrite ! mod_eq by trivial. -rewrite div_mul_cancel_r by order. -now rewrite mul_sub_distr_r, <- !mul_assoc, (mul_comm (a/b) c). +rewrite ! rem_eq by trivial. +rewrite quot_mul_cancel_r by order. +now rewrite mul_sub_distr_r, <- !mul_assoc, (mul_comm (a÷b) c). Qed. -Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 -> - (c*a) mod (c*b) == c * (a mod b). +Lemma mul_rem_distr_l: forall a b c, b~=0 -> c~=0 -> + (c*a) rem (c*b) == c * (a rem b). Proof. -intros; rewrite !(mul_comm c); now apply mul_mod_distr_r. +intros; rewrite !(mul_comm c); now apply mul_rem_distr_r. Qed. (** Operations modulo. *) -Theorem mod_mod: forall a n, n~=0 -> - (a mod n) mod n == a mod n. +Theorem rem_rem: forall a n, n~=0 -> + (a rem n) rem n == a rem n. Proof. -intros. pos_or_neg a; pos_or_neg n. apply mod_mod; order. -rewrite <- ! (mod_opp_r _ n) by trivial. apply mod_mod; order. -apply opp_inj. rewrite <- !mod_opp_l by order. apply mod_mod; order. -apply opp_inj. rewrite <- !mod_opp_opp by order. apply mod_mod; order. +intros. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order. +rewrite <- ! (rem_opp_r _ n) by trivial. apply NZQuot.mod_mod; order. +apply opp_inj. rewrite <- !rem_opp_l by order. apply NZQuot.mod_mod; order. +apply opp_inj. rewrite <- !rem_opp_opp by order. apply NZQuot.mod_mod; order. Qed. -Lemma mul_mod_idemp_l : forall a b n, n~=0 -> - ((a mod n)*b) mod n == (a*b) mod n. +Lemma mul_rem_idemp_l : forall a b n, n~=0 -> + ((a rem n)*b) rem n == (a*b) rem n. Proof. assert (Aux1 : forall a b n, 0<=a -> 0<=b -> n~=0 -> - ((a mod n)*b) mod n == (a*b) mod n). - intros. pos_or_neg n. apply mul_mod_idemp_l; order. - rewrite <- ! (mod_opp_r _ n) by order. apply mul_mod_idemp_l; order. + ((a rem n)*b) rem n == (a*b) rem n). + intros. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order. + rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.mul_mod_idemp_l; order. assert (Aux2 : forall a b n, 0<=a -> n~=0 -> - ((a mod n)*b) mod n == (a*b) mod n). + ((a rem n)*b) rem n == (a*b) rem n). intros. pos_or_neg b. now apply Aux1. - apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_r by order. + apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_r by order. apply Aux1; order. intros a b n Hn. pos_or_neg a. now apply Aux2. -apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_l, <-mod_opp_l by order. +apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_l, <-rem_opp_l by order. apply Aux2; order. Qed. -Lemma mul_mod_idemp_r : forall a b n, n~=0 -> - (a*(b mod n)) mod n == (a*b) mod n. +Lemma mul_rem_idemp_r : forall a b n, n~=0 -> + (a*(b rem n)) rem n == (a*b) rem n. Proof. -intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l. +intros. rewrite !(mul_comm a). now apply mul_rem_idemp_l. Qed. -Theorem mul_mod: forall a b n, n~=0 -> - (a * b) mod n == ((a mod n) * (b mod n)) mod n. +Theorem mul_rem: forall a b n, n~=0 -> + (a * b) rem n == ((a rem n) * (b rem n)) rem n. Proof. -intros. now rewrite mul_mod_idemp_l, mul_mod_idemp_r. +intros. now rewrite mul_rem_idemp_l, mul_rem_idemp_r. Qed. (** addition and modulo Generally speaking, unlike with other conventions, we don't have - [(a+b) mod n = (a mod n + b mod n) mod n] + [(a+b) rem n = (a rem n + b rem n) rem n] for any a and b. - For instance, take (8 + (-10)) mod 3 = -2 whereas - (8 mod 3 + (-10 mod 3)) mod 3 = 1. + For instance, take (8 + (-10)) rem 3 = -2 whereas + (8 rem 3 + (-10 rem 3)) rem 3 = 1. *) -Lemma add_mod_idemp_l : forall a b n, n~=0 -> 0 <= a*b -> - ((a mod n)+b) mod n == (a+b) mod n. +Lemma add_rem_idemp_l : forall a b n, n~=0 -> 0 <= a*b -> + ((a rem n)+b) rem n == (a+b) rem n. Proof. assert (Aux : forall a b n, 0<=a -> 0<=b -> n~=0 -> - ((a mod n)+b) mod n == (a+b) mod n). - intros. pos_or_neg n. apply add_mod_idemp_l; order. - rewrite <- ! (mod_opp_r _ n) by order. apply add_mod_idemp_l; order. + ((a rem n)+b) rem n == (a+b) rem n). + intros. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order. + rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.add_mod_idemp_l; order. intros a b n Hn Hab. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]. now apply Aux. -apply opp_inj. rewrite <-2 mod_opp_l, 2 opp_add_distr, <-mod_opp_l by order. +apply opp_inj. rewrite <-2 rem_opp_l, 2 opp_add_distr, <-rem_opp_l by order. rewrite <- opp_nonneg_nonpos in *. now apply Aux. Qed. -Lemma add_mod_idemp_r : forall a b n, n~=0 -> 0 <= a*b -> - (a+(b mod n)) mod n == (a+b) mod n. +Lemma add_rem_idemp_r : forall a b n, n~=0 -> 0 <= a*b -> + (a+(b rem n)) rem n == (a+b) rem n. Proof. -intros. rewrite !(add_comm a). apply add_mod_idemp_l; trivial. +intros. rewrite !(add_comm a). apply add_rem_idemp_l; trivial. now rewrite mul_comm. Qed. -Theorem add_mod: forall a b n, n~=0 -> 0 <= a*b -> - (a+b) mod n == (a mod n + b mod n) mod n. +Theorem add_rem: forall a b n, n~=0 -> 0 <= a*b -> + (a+b) rem n == (a rem n + b rem n) rem n. Proof. -intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. +intros a b n Hn Hab. rewrite add_rem_idemp_l, add_rem_idemp_r; trivial. reflexivity. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]; - destruct (le_0_mul _ _ (mod_sign b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; + destruct (le_0_mul _ _ (rem_sign_mul b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; auto using mul_nonneg_nonneg, mul_nonpos_nonpos. - setoid_replace b with 0 by order. rewrite mod_0_l by order. nzsimpl; order. - setoid_replace b with 0 by order. rewrite mod_0_l by order. nzsimpl; order. + setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. + setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. Qed. (** Conversely, the following result needs less restrictions here. *) -Lemma div_div : forall a b c, b~=0 -> c~=0 -> - (a/b)/c == a/(b*c). +Lemma quot_quot : forall a b c, b~=0 -> c~=0 -> + (a÷b)÷c == a÷(b*c). Proof. -assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a/b)/c == a/(b*c)). - intros. pos_or_neg c. apply div_div; order. - apply opp_inj. rewrite <- 2 div_opp_r, <- mul_opp_r; trivial. - apply div_div; order. +assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a÷b)÷c == a÷(b*c)). + intros. pos_or_neg c. apply NZQuot.div_div; order. + apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_r; trivial. + apply NZQuot.div_div; order. rewrite <- neq_mul_0; intuition order. -assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a/b)/c == a/(b*c)). +assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a÷b)÷c == a÷(b*c)). intros. pos_or_neg b. apply Aux1; order. - apply opp_inj. rewrite <- div_opp_l, <- 2 div_opp_r, <- mul_opp_l; trivial. + apply opp_inj. rewrite <- quot_opp_l, <- 2 quot_opp_r, <- mul_opp_l; trivial. apply Aux1; trivial. rewrite <- neq_mul_0; intuition order. intros. pos_or_neg a. apply Aux2; order. -apply opp_inj. rewrite <- 3 div_opp_l; try order. apply Aux2; order. +apply opp_inj. rewrite <- 3 quot_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0. tauto. Qed. (** A last inequality: *) -Theorem div_mul_le: - forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. -Proof. exact div_mul_le. Qed. - -(** mod is related to divisibility *) - -Lemma mod_divides : forall a b, b~=0 -> - (a mod b == 0 <-> exists c, a == b*c). -Proof. - intros a b Hb. split. - intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1. - rewrite Hab; now nzsimpl. - intros (c,Hc). rewrite Hc, mul_comm. now apply mod_mul. -Qed. +Theorem quot_mul_le: + forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a÷b) <= (c*a)÷b. +Proof. exact NZQuot.div_mul_le. Qed. -End ZDivProp. +End ZQuotProp. diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index d58d1f1e2..6b1d4675e 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -10,10 +10,10 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZGcd. -Module ZGcdProp +Module Type ZGcdProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) - (Import D : ZSgnAbsProp A B). + (Import C : ZSgnAbsProp A B). Include NZGcdProp A A B. @@ -269,8 +269,6 @@ Proof. symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. Qed. -(** TODO : relation between gcd and division and modulo *) - (** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *) End ZGcdProp. diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v new file mode 100644 index 000000000..27bd5962c --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -0,0 +1,436 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor. + +(** * Least Common Multiple *) + +(** Unlike other functions around, we will define lcm below instead of + axiomatizing it. Indeed, there is no "prior art" about lcm in the + standard library to be compliant with, and the generic definition + of lcm via gcd is quite reasonable. + + By the way, we also state here some combined properties of div/mod + and quot/rem and gcd. +*) + +Module Type ZLcmProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B) + (Import D : ZDivProp A B C) + (Import E : ZQuotProp A B C) + (Import F : ZGcdProp A B C). + +(** The two notions of division are equal on non-negative numbers *) + +Lemma quot_div_nonneg : forall a b, 0<=a -> 0<b -> a÷b == a/b. +Proof. + intros. apply div_unique_pos with (a rem b). + now apply rem_bound_pos. + apply quot_rem. order. +Qed. + +Lemma rem_mod_nonneg : forall a b, 0<=a -> 0<b -> a rem b == a mod b. +Proof. + intros. apply mod_unique_pos with (a÷b). + now apply rem_bound_pos. + apply quot_rem. order. +Qed. + +(** Modulo and remainder are null at the same place, + and this correspond to the divisibility relation. *) + +Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)). +Proof. + intros a b Hb. split. + intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2. + rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite <- Hc, mul_comm. now apply mod_mul. +Qed. + +Lemma rem_divide : forall a b, b~=0 -> (a rem b == 0 <-> (b|a)). +Proof. + intros a b Hb. split. + intros Hab. exists (a÷b). rewrite (quot_rem a b Hb) at 2. + rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite <- Hc, mul_comm. now apply rem_mul. +Qed. + +Lemma rem_mod_eq_0 : forall a b, b~=0 -> (a rem b == 0 <-> a mod b == 0). +Proof. + intros a b Hb. now rewrite mod_divide, rem_divide. +Qed. + +(** When division is exact, div and quot agree *) + +Lemma quot_div_exact : forall a b, b~=0 -> (b|a) -> a÷b == a/b. +Proof. + intros a b Hb H. + apply mul_cancel_l with b; trivial. + assert (H':=H). + apply rem_divide, quot_exact in H; trivial. + apply mod_divide, div_exact in H'; trivial. + now rewrite <-H,<-H'. +Qed. + +Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) -> + (c*a)/b == c*(a/b). +Proof. + intros a b c Hb H. + apply mul_cancel_l with b; trivial. + rewrite mul_assoc, mul_shuffle0. + assert (H':=H). apply mod_divide, div_exact in H'; trivial. + rewrite <- H', (mul_comm a c). + symmetry. apply div_exact; trivial. + apply mod_divide; trivial. + now apply divide_mul_r. +Qed. + +Lemma divide_quot_mul_exact : forall a b c, b~=0 -> (b|a) -> + (c*a)÷b == c*(a÷b). +Proof. + intros a b c Hb H. + rewrite 2 quot_div_exact; trivial. + apply divide_div_mul_exact; trivial. + now apply divide_mul_r. +Qed. + +(** Gcd of divided elements, for exact divisions *) + +Lemma gcd_div_factor : forall a b c, 0<c -> (c|a) -> (c|b) -> + gcd (a/c) (b/c) == (gcd a b)/c. +Proof. + intros a b c Hc Ha Hb. + apply mul_cancel_l with c; try order. + assert (H:=gcd_greatest _ _ _ Ha Hb). + apply mod_divide, div_exact in H; try order. + rewrite <- H. + rewrite <- gcd_mul_mono_l_nonneg; try order. + apply gcd_wd; symmetry; apply div_exact; try order; + apply mod_divide; trivial; try order. +Qed. + +Lemma gcd_quot_factor : forall a b c, 0<c -> (c|a) -> (c|b) -> + gcd (a÷c) (b÷c) == (gcd a b)÷c. +Proof. + intros a b c Hc Ha Hb. rewrite !quot_div_exact; trivial; try order. + now apply gcd_div_factor. now apply gcd_greatest. +Qed. + +Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b -> + gcd (a/g) (b/g) == 1. +Proof. + intros a b g NZ EQ. rewrite gcd_div_factor. + now rewrite <- EQ, div_same. + generalize (gcd_nonneg a b); order. + rewrite EQ; apply gcd_divide_l. + rewrite EQ; apply gcd_divide_r. +Qed. + +Lemma gcd_quot_gcd : forall a b g, g~=0 -> g == gcd a b -> + gcd (a÷g) (b÷g) == 1. +Proof. + intros a b g NZ EQ. rewrite !quot_div_exact; trivial. + now apply gcd_div_gcd. + rewrite EQ; apply gcd_divide_r. + rewrite EQ; apply gcd_divide_l. +Qed. + +(** The following equality is crucial for Euclid algorithm *) + +Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a. +Proof. + intros a b Hb. rewrite mod_eq; trivial. + rewrite <- add_opp_r, mul_comm, <- mul_opp_l. + rewrite (gcd_comm _ b). + apply gcd_add_mult_diag_r. +Qed. + +Lemma gcd_rem : forall a b, b~=0 -> gcd (a rem b) b == gcd b a. +Proof. + intros a b Hb. rewrite rem_eq; trivial. + rewrite <- add_opp_r, mul_comm, <- mul_opp_l. + rewrite (gcd_comm _ b). + apply gcd_add_mult_diag_r. +Qed. + +(** We now define lcm thanks to gcd: + + lcm a b = a * (b / gcd a b) + = (a / gcd a b) * b + = (a*b) / gcd a b + + We had an abs in order to have an always-nonnegative lcm, + in the spirit of gcd. Nota: [lcm 0 0] should be 0, which + isn't garantee with the third equation above. +*) + +Definition lcm a b := abs (a*(b/gcd a b)). + +Instance lcm_wd : Proper (eq==>eq==>eq) lcm. +Proof. + unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy. +Qed. + +Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 -> + a * (b / gcd a b) == (a*b)/gcd a b. +Proof. + intros a b H. rewrite divide_div_mul_exact; try easy. apply gcd_divide_r. +Qed. + +Lemma lcm_equiv2 : forall a b, gcd a b ~= 0 -> + (a / gcd a b) * b == (a*b)/gcd a b. +Proof. + intros a b H. rewrite 2 (mul_comm _ b). + rewrite divide_div_mul_exact; try easy. apply gcd_divide_l. +Qed. + +Lemma gcd_div_swap : forall a b, + (a / gcd a b) * b == a * (b / gcd a b). +Proof. + intros a b. destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. + apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ, EQ'. now nzsimpl. + now rewrite lcm_equiv1, <-lcm_equiv2. +Qed. + +Lemma divide_lcm_l : forall a b, (a | lcm a b). +Proof. + unfold lcm. intros a b. apply divide_abs_r, divide_factor_l. +Qed. + +Lemma divide_lcm_r : forall a b, (b | lcm a b). +Proof. + unfold lcm. intros a b. apply divide_abs_r. rewrite <- gcd_div_swap. + apply divide_factor_r. +Qed. + +Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a). +Proof. + intros a b c Ha Hb (c',Hc). exists c'. + now rewrite mul_comm, <- divide_div_mul_exact, mul_comm, Hc. +Qed. + +Lemma lcm_least : forall a b c, + (a | c) -> (b | c) -> (lcm a b | c). +Proof. + intros a b c Ha Hb. unfold lcm. apply divide_abs_l. + destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. + apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ in *. now nzsimpl. + assert (Ga := gcd_divide_l a b). + assert (Gb := gcd_divide_r a b). + set (g:=gcd a b) in *. + assert (Ha' := divide_div g a c NEQ Ga Ha). + assert (Hb' := divide_div g b c NEQ Gb Hb). + destruct Ha' as (a',Ha'). rewrite <- Ha' in Hb'. + apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm]. + destruct Hb' as (b',Hb'). + exists b'. + rewrite <- mul_assoc, Hb'. + rewrite (proj2 (div_exact c g NEQ)). + rewrite <- Ha', mul_assoc. apply mul_wd; try easy. + apply div_exact; trivial. + apply mod_divide; trivial. + apply mod_divide; trivial. transitivity a; trivial. +Qed. + +Lemma lcm_nonneg : forall a b, 0 <= lcm a b. +Proof. + intros a b. unfold lcm. apply abs_nonneg. +Qed. + +Lemma lcm_comm : forall a b, lcm a b == lcm b a. +Proof. + intros a b. unfold lcm. rewrite (gcd_comm b), (mul_comm b). + now rewrite <- gcd_div_swap. +Qed. + +Lemma lcm_divide_iff : forall n m p, + (lcm n m | p) <-> (n | p) /\ (m | p). +Proof. + intros. split. split. + transitivity (lcm n m); trivial using divide_lcm_l. + transitivity (lcm n m); trivial using divide_lcm_r. + intros (H,H'). now apply lcm_least. +Qed. + +Lemma lcm_unique : forall n m p, + 0<=p -> (n|p) -> (m|p) -> + (forall q, (n|q) -> (m|q) -> (p|q)) -> + lcm n m == p. +Proof. + intros n m p Hp Hn Hm H. + apply divide_antisym_nonneg; trivial. apply lcm_nonneg. + now apply lcm_least. + apply H. apply divide_lcm_l. apply divide_lcm_r. +Qed. + +Lemma lcm_unique_alt : forall n m p, 0<=p -> + (forall q, (p|q) <-> (n|q) /\ (m|q)) -> + lcm n m == p. +Proof. + intros n m p Hp H. + apply lcm_unique; trivial. + apply -> H. apply divide_refl. + apply -> H. apply divide_refl. + intros. apply H. now split. +Qed. + +Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p. +Proof. + intros. apply lcm_unique_alt; try apply lcm_nonneg. + intros. now rewrite !lcm_divide_iff, and_assoc. +Qed. + +Lemma lcm_0_l : forall n, lcm 0 n == 0. +Proof. + intros. apply lcm_unique; trivial. order. + apply divide_refl. + apply divide_0_r. +Qed. + +Lemma lcm_0_r : forall n, lcm n 0 == 0. +Proof. + intros. now rewrite lcm_comm, lcm_0_l. +Qed. + +Lemma lcm_1_l_nonneg : forall n, 0<=n -> lcm 1 n == n. +Proof. + intros. apply lcm_unique; trivial using divide_1_l, le_0_1, divide_refl. +Qed. + +Lemma lcm_1_r_nonneg : forall n, 0<=n -> lcm n 1 == n. +Proof. + intros. now rewrite lcm_comm, lcm_1_l_nonneg. +Qed. + +Lemma lcm_diag_nonneg : forall n, 0<=n -> lcm n n == n. +Proof. + intros. apply lcm_unique; trivial using divide_refl. +Qed. + +Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0. +Proof. + intros. split. + intros EQ. + apply eq_mul_0. + apply divide_0_l. rewrite <- EQ. apply lcm_least. + apply divide_factor_l. apply divide_factor_r. + destruct 1 as [EQ|EQ]; rewrite EQ. apply lcm_0_l. apply lcm_0_r. +Qed. + +Lemma divide_lcm_eq_r : forall n m, 0<=m -> (n|m) -> lcm n m == m. +Proof. + intros n m Hm H. apply lcm_unique_alt; trivial. + intros q. split. split; trivial. now transitivity m. + now destruct 1. +Qed. + +Lemma divide_lcm_iff : forall n m, 0<=m -> ((n|m) <-> lcm n m == m). +Proof. + intros n m Hn. split. now apply divide_lcm_eq_r. + intros EQ. rewrite <- EQ. apply divide_lcm_l. +Qed. + +Lemma lcm_opp_l : forall n m, lcm (-n) m == lcm n m. +Proof. + intros. apply lcm_unique_alt; try apply lcm_nonneg. + intros. rewrite divide_opp_l. apply lcm_divide_iff. +Qed. + +Lemma lcm_opp_r : forall n m, lcm n (-m) == lcm n m. +Proof. + intros. now rewrite lcm_comm, lcm_opp_l, lcm_comm. +Qed. + +Lemma lcm_abs_l : forall n m, lcm (abs n) m == lcm n m. +Proof. + intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + easy. apply lcm_opp_l. +Qed. + +Lemma lcm_abs_r : forall n m, lcm n (abs m) == lcm n m. +Proof. + intros. now rewrite lcm_comm, lcm_abs_l, lcm_comm. +Qed. + +Lemma lcm_1_l : forall n, lcm 1 n == abs n. +Proof. + intros. rewrite <- lcm_abs_r. apply lcm_1_l_nonneg, abs_nonneg. +Qed. + +Lemma lcm_1_r : forall n, lcm n 1 == abs n. +Proof. + intros. now rewrite lcm_comm, lcm_1_l. +Qed. + +Lemma lcm_diag : forall n, lcm n n == abs n. +Proof. + intros. rewrite <- lcm_abs_l, <- lcm_abs_r. + apply lcm_diag_nonneg, abs_nonneg. +Qed. + +Lemma lcm_mul_mono_l : + forall n m p, lcm (p * n) (p * m) == abs p * lcm n m. +Proof. + intros n m p. + destruct (eq_decidable p 0) as [Hp|Hp]. + rewrite Hp. nzsimpl. rewrite lcm_0_l, abs_0. now nzsimpl. + destruct (eq_decidable (gcd n m) 0) as [Hg|Hg]. + apply gcd_eq_0 in Hg. destruct Hg as (Hn,Hm); rewrite Hn, Hm. + nzsimpl. rewrite lcm_0_l. now nzsimpl. + unfold lcm. + rewrite gcd_mul_mono_l. + rewrite !abs_mul, mul_assoc. apply mul_wd; try easy. + rewrite <- (abs_sgn p) at 1. rewrite <- mul_assoc. + rewrite div_mul_cancel_l; trivial. + rewrite divide_div_mul_exact; trivial. rewrite abs_mul. + rewrite <- (sgn_abs (sgn p)), sgn_sgn. + destruct (sgn_spec p) as [(_,EQ)|[(EQ,_)|(_,EQ)]]. + rewrite EQ. now nzsimpl. order. + rewrite EQ. rewrite mul_opp_l, mul_opp_r, opp_involutive. now nzsimpl. + apply gcd_divide_r. + contradict Hp. now apply abs_0_iff. +Qed. + +Lemma lcm_mul_mono_l_nonneg : + forall n m p, 0<=p -> lcm (p*n) (p*m) == p * lcm n m. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l. +Qed. + +Lemma lcm_mul_mono_r : + forall n m p, lcm (n * p) (m * p) == lcm n m * abs p. +Proof. + intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm. +Qed. + +Lemma lcm_mul_mono_r_nonneg : + forall n m p, 0<=p -> lcm (n*p) (m*p) == lcm n m * p. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r. +Qed. + +Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> + (gcd n m == 1 <-> lcm n m == abs (n*m)). +Proof. + intros n m Hn Hm. split; intros H. + unfold lcm. rewrite H. now rewrite div_1_r. + unfold lcm in *. + rewrite !abs_mul in H. apply mul_cancel_l in H; [|now rewrite abs_0_iff]. + assert (H' := gcd_divide_r n m). + assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order). + apply mod_divide in H'; trivial. apply div_exact in H'; trivial. + assert (m / gcd n m ~=0) by (contradict Hm; rewrite H', Hm; now nzsimpl). + rewrite <- (mul_1_l (abs (_/_))) in H. + rewrite H' in H at 3. rewrite abs_mul in H. + apply mul_cancel_r in H; [|now rewrite abs_0_iff]. + rewrite abs_eq in H. order. apply gcd_nonneg. +Qed. + +End ZLcmProp. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 6fbf0f23d..2e747782c 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -6,10 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZGcd. +Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor + ZGcd ZLcm. (** This functor summarizes all known facts about Z. *) Module Type ZProp (Z:ZAxiomsSig) := ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z - <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z <+ ZGcdProp Z. + <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z + <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index b2bf8703e..72137eccf 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 b341b3209..f4baf32bc 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) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 01d36854b..f68aa0dbe 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -10,7 +10,7 @@ Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec - Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def. + Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def Zdiv_def. Local Open Scope Z_scope. @@ -170,6 +170,27 @@ Definition gcd_nonneg := Zgcd_nonneg. Definition divide := Zdivide'. Definition gcd := Zgcd. +(** Div / Mod / Quot / Rem *) + +Program Instance div_wd : Proper (eq==>eq==>eq) Zdiv. +Program Instance mod_wd : Proper (eq==>eq==>eq) Zmod. +Program Instance quot_wd : Proper (eq==>eq==>eq) Zquot. +Program Instance rem_wd : Proper (eq==>eq==>eq) Zrem. + +Definition div_mod := Z_div_mod_eq_full. +Definition mod_pos_bound := Zmod_pos_bound. +Definition mod_neg_bound := Zmod_neg_bound. +Definition mod_bound_pos := fun a b (_:0<=a) => Zmod_pos_bound a b. +Definition div := Zdiv. +Definition modulo := Zmod. + +Definition quot_rem := fun a b (_:b<>0) => Z_quot_rem_eq a b. +Definition rem_bound_pos := Zrem_bound. +Definition rem_opp_l := fun a b (_:b<>0) => Zrem_opp_l a b. +Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b. +Definition quot := Zquot. +Definition remainder := Zrem. + (** We define [eq] only here to avoid refering to this [eq] above. *) Definition eq := (@eq Z). @@ -212,18 +233,3 @@ exact Zadd_opp_r. Qed. Add Ring ZR : Zring.*) - - - -(* -Theorem eq_equiv_e : forall x y : Z, E x y <-> e x y. -Proof. -intros x y; unfold E, e, Zeq_bool; split; intro H. -rewrite H; now rewrite Zcompare_refl. -rewrite eq_true_unfold_pos in H. -assert (H1 : (x ?= y) = Eq). -case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H; -[reflexivity | discriminate H | discriminate H]. -now apply Zcompare_Eq_eq. -Qed. -*) diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index b5c761a6f..c2a173e22 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 999e7cd03..6a823a732 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. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index aaf6bfc22..0807013eb 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -23,26 +23,19 @@ End DivModNotation. Module Type DivMod' (A : Typ) := DivMod A <+ DivModNotation A. -Module Type NZDivCommon (Import A : NZAxiomsSig')(Import B : DivMod' A). +Module Type NZDivSpec (Import A : NZOrdAxiomsSig')(Import B : DivMod' A). Declare Instance div_wd : Proper (eq==>eq==>eq) div. Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo. Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b). -End NZDivCommon. + Axiom mod_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. +End NZDivSpec. (** The different divisions will only differ in the conditions - they impose on [modulo]. For NZ, we only describe behavior - on positive numbers. - - NB: This axiom would also be true for N and Z, but redundant. + they impose on [modulo]. For NZ, we have only described the + behavior on positive numbers. *) -Module Type NZDivSpecific (Import A : NZOrdAxiomsSig')(Import B : DivMod' A). - Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. -End NZDivSpecific. - -Module Type NZDiv (A : NZOrdAxiomsSig) - := DivMod A <+ NZDivCommon A <+ NZDivSpecific A. - +Module Type NZDiv (A : NZOrdAxiomsSig) := DivMod A <+ NZDivSpec A. Module Type NZDiv' (A : NZOrdAxiomsSig) := NZDiv A <+ DivModNotation A. Module Type NZDivProp @@ -83,7 +76,7 @@ Theorem div_unique: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. -apply mod_bound; order. +apply mod_bound_pos; order. rewrite <- div_mod; order. Qed. @@ -93,7 +86,7 @@ Theorem mod_unique: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. -apply mod_bound; order. +apply mod_bound_pos; order. rewrite <- div_mod; order. Qed. @@ -193,7 +186,7 @@ Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. Proof. intros. destruct (le_gt_cases b a). apply le_trans with b; auto. -apply lt_le_incl. destruct (mod_bound a b); auto. +apply lt_le_incl. destruct (mod_bound_pos a b); auto. rewrite lt_eq_cases; right. apply mod_small; auto. Qed. @@ -215,7 +208,7 @@ Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b. Proof. intros a b (Hb,Hab). assert (LE : 0 <= a/b) by (apply div_pos; order). -assert (MOD : a mod b < b) by (destruct (mod_bound a b); order). +assert (MOD : a mod b < b) by (destruct (mod_bound_pos a b); order). rewrite lt_eq_cases in LE; destruct LE as [LT|EQ]; auto. exfalso; revert Hab. rewrite (div_mod a b), <-EQ; nzsimpl; order. @@ -262,7 +255,7 @@ rewrite <- (mul_1_l (a/b)) at 1. rewrite <- mul_lt_mono_pos_r; auto. apply div_str_pos; auto. rewrite <- (add_0_r (b*(a/b))) at 1. -rewrite <- add_le_mono_l. destruct (mod_bound a b); order. +rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed. (** [le] is compatible with a positive division. *) @@ -281,8 +274,8 @@ apply lt_le_trans with b; auto. rewrite (div_mod b c) at 1 by order. rewrite <- add_assoc, <- add_le_mono_l. apply le_trans with (c+0). -nzsimpl; destruct (mod_bound b c); order. -rewrite <- add_le_mono_l. destruct (mod_bound a c); order. +nzsimpl; destruct (mod_bound_pos b c); order. +rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order. Qed. (** The following two properties could be used as specification of div *) @@ -292,7 +285,7 @@ Proof. intros. rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order. rewrite <- (add_0_r a) at 1. -rewrite <- add_le_mono_l. destruct (mod_bound a b); order. +rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed. Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)). @@ -301,7 +294,7 @@ intros. rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. -destruct (mod_bound a b); auto. +destruct (mod_bound_pos a b); auto. Qed. @@ -358,7 +351,7 @@ Proof. apply mul_le_mono_nonneg_r; try order. apply div_pos; order. rewrite <- (add_0_r (r*(p/r))) at 1. - rewrite <- add_le_mono_l. destruct (mod_bound p r); order. + rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order. Qed. @@ -370,7 +363,7 @@ Proof. intros. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound; auto. + apply mod_bound_pos; auto. rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. now rewrite mul_comm. Qed. @@ -403,8 +396,8 @@ Proof. apply div_unique with ((a mod b)*c). apply mul_nonneg_nonneg; order. split. - apply mul_nonneg_nonneg; destruct (mod_bound a b); order. - rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound a b); auto. + apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order. + rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto. rewrite (div_mod a b) at 1 by order. rewrite mul_add_distr_r. rewrite add_cancel_r. @@ -440,7 +433,7 @@ Qed. Theorem mod_mod: forall a n, 0<=a -> 0<n -> (a mod n) mod n == a mod n. Proof. - intros. destruct (mod_bound a n); auto. now rewrite mod_small_iff. + intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. Qed. Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -453,7 +446,7 @@ Proof. rewrite mul_add_distr_l, mul_assoc. intros. rewrite mod_add; auto. now rewrite mul_comm. - apply mul_nonneg_nonneg; destruct (mod_bound a n); auto. + apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto. Qed. Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -466,7 +459,7 @@ Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity. - now destruct (mod_bound b n). + now destruct (mod_bound_pos b n). Qed. Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -477,7 +470,7 @@ Proof. rewrite (div_mod a n) at 1 2 by order. rewrite <- add_assoc, add_comm, mul_comm. intros. rewrite mod_add; trivial. reflexivity. - apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto. + apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto. Qed. Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -490,7 +483,7 @@ Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity. - now destruct (mod_bound b n). + now destruct (mod_bound_pos b n). Qed. Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -499,7 +492,7 @@ Proof. intros a b c Ha Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b); trivial. (* begin 0<= ... <b*c *) - destruct (mod_bound (a/b) c), (mod_bound a b); auto using div_pos. + destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos. split. apply add_nonneg_nonneg; auto. apply mul_nonneg_nonneg; order. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index ee2a92e84..82f072746 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -39,17 +39,17 @@ Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N). Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. End NDivSpecific. -(** For gcd pow sqrt log2, the NZ axiomatizations are enough. *) +(** For div mod gcd pow sqrt log2, the NZ axiomatizations are enough. *) (** We now group everything together. *) Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd - <+ DivMod <+ NZDivCommon <+ NDivSpecific. + <+ NZDiv.NZDiv. Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' - <+ DivMod' <+ NZDivCommon <+ NDivSpecific. + <+ NZDiv.NZDiv'. (** It could also be interesting to have a constructive recursor function. *) diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 0bb66ab2f..9110ec036 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -6,29 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Properties of Euclidean Division *) - Require Import NAxioms NSub NZDiv. -Module NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N). +(** Properties of Euclidean Division *) -(** We benefit from what already exists for NZ *) +Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N). - Module ND <: NZDiv N. - Definition div := div. - Definition modulo := modulo. - Definition div_wd := div_wd. - Definition mod_wd := mod_wd. - Definition div_mod := div_mod. - Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Proof. split. apply le_0_l. apply mod_upper_bound. order. Qed. - End ND. - Module Import NZDivP := Nop <+ NZDivProp N ND NP. +(** We benefit from what already exists for NZ *) +Module Import NZDivP := Nop <+ NZDivProp N N NP. - Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. +Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. (** Let's now state again theorems, but without useless hypothesis. *) +Lemma mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. +Proof. intros. apply mod_bound_pos; auto'. Qed. + +(** Another formulation of the main equation *) + +Lemma mod_eq : + forall a b, b~=0 -> a mod b == a - b*(a/b). +Proof. +intros. +symmetry. apply add_sub_eq_l. symmetry. +now apply div_mod. +Qed. + (** Uniqueness theorems *) Theorem div_mod_unique : diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index 5bf33d4d2..77f23a02b 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -10,7 +10,7 @@ Require Import NAxioms NSub NZGcd. -Module NGcdProp +Module Type NGcdProp (Import A : NAxiomsSig') (Import B : NSubProp A). diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v new file mode 100644 index 000000000..f3b45e308 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -0,0 +1,292 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import NAxioms NSub NDiv NGcd. + +(** * Least Common Multiple *) + +(** Unlike other functions around, we will define lcm below instead of + axiomatizing it. Indeed, there is no "prior art" about lcm in the + standard library to be compliant with, and the generic definition + of lcm via gcd is quite reasonable. + + By the way, we also state here some combined properties of div/mod + and gcd. +*) + +Module Type NLcmProp + (Import A : NAxiomsSig') + (Import B : NSubProp A) + (Import C : NDivProp A B) + (Import D : NGcdProp A B). + +(** Divibility and modulo *) + +Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)). +Proof. + intros a b Hb. split. + intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2. + rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite <- Hc, mul_comm. now apply mod_mul. +Qed. + +Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) -> + (c*a)/b == c*(a/b). +Proof. + intros a b c Hb H. + apply mul_cancel_l with b; trivial. + rewrite mul_assoc, mul_shuffle0. + assert (H':=H). apply mod_divide, div_exact in H'; trivial. + rewrite <- H', (mul_comm a c). + symmetry. apply div_exact; trivial. + apply mod_divide; trivial. + now apply divide_mul_r. +Qed. + +(** Gcd of divided elements, for exact divisions *) + +Lemma gcd_div_factor : forall a b c, c~=0 -> (c|a) -> (c|b) -> + gcd (a/c) (b/c) == (gcd a b)/c. +Proof. + intros a b c Hc Ha Hb. + apply mul_cancel_l with c; try order. + assert (H:=gcd_greatest _ _ _ Ha Hb). + apply mod_divide, div_exact in H; try order. + rewrite <- H. + rewrite <- gcd_mul_mono_l; try order. + apply gcd_wd; symmetry; apply div_exact; try order; + apply mod_divide; trivial; try order. +Qed. + +Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b -> + gcd (a/g) (b/g) == 1. +Proof. + intros a b g NZ EQ. rewrite gcd_div_factor. + now rewrite <- EQ, div_same. + generalize (gcd_nonneg a b); order. + rewrite EQ; apply gcd_divide_l. + rewrite EQ; apply gcd_divide_r. +Qed. + +(** The following equality is crucial for Euclid algorithm *) + +Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a. +Proof. + intros a b Hb. rewrite (gcd_comm _ b). + rewrite <- (gcd_add_mult_diag_r b (a mod b) (a/b)). + now rewrite add_comm, mul_comm, <- div_mod. +Qed. + +(** We now define lcm thanks to gcd: + + lcm a b = a * (b / gcd a b) + = (a / gcd a b) * b + = (a*b) / gcd a b + + Nota: [lcm 0 0] should be 0, which isn't garantee with the third + equation above. +*) + +Definition lcm a b := a*(b/gcd a b). + +Instance lcm_wd : Proper (eq==>eq==>eq) lcm. +Proof. + unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy. +Qed. + +Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 -> + a * (b / gcd a b) == (a*b)/gcd a b. +Proof. + intros a b H. rewrite divide_div_mul_exact; try easy. apply gcd_divide_r. +Qed. + +Lemma lcm_equiv2 : forall a b, gcd a b ~= 0 -> + (a / gcd a b) * b == (a*b)/gcd a b. +Proof. + intros a b H. rewrite 2 (mul_comm _ b). + rewrite divide_div_mul_exact; try easy. apply gcd_divide_l. +Qed. + +Lemma gcd_div_swap : forall a b, + (a / gcd a b) * b == a * (b / gcd a b). +Proof. + intros a b. destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. + apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ, EQ'. now nzsimpl. + now rewrite lcm_equiv1, <-lcm_equiv2. +Qed. + +Lemma divide_lcm_l : forall a b, (a | lcm a b). +Proof. + unfold lcm. intros a b. apply divide_factor_l. +Qed. + +Lemma divide_lcm_r : forall a b, (b | lcm a b). +Proof. + unfold lcm. intros a b. rewrite <- gcd_div_swap. + apply divide_factor_r. +Qed. + +Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a). +Proof. + intros a b c Ha Hb (c',Hc). exists c'. + now rewrite mul_comm, <- divide_div_mul_exact, mul_comm, Hc. +Qed. + +Lemma lcm_least : forall a b c, + (a | c) -> (b | c) -> (lcm a b | c). +Proof. + intros a b c Ha Hb. unfold lcm. + destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. + apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ in *. now nzsimpl. + assert (Ga := gcd_divide_l a b). + assert (Gb := gcd_divide_r a b). + set (g:=gcd a b) in *. + assert (Ha' := divide_div g a c NEQ Ga Ha). + assert (Hb' := divide_div g b c NEQ Gb Hb). + destruct Ha' as (a',Ha'). rewrite <- Ha' in Hb'. + apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm]. + destruct Hb' as (b',Hb'). + exists b'. + rewrite <- mul_assoc, Hb'. + rewrite (proj2 (div_exact c g NEQ)). + rewrite <- Ha', mul_assoc. apply mul_wd; try easy. + apply div_exact; trivial. + apply mod_divide; trivial. + apply mod_divide; trivial. transitivity a; trivial. +Qed. + +Lemma lcm_comm : forall a b, lcm a b == lcm b a. +Proof. + intros a b. unfold lcm. rewrite (gcd_comm b), (mul_comm b). + now rewrite <- gcd_div_swap. +Qed. + +Lemma lcm_divide_iff : forall n m p, + (lcm n m | p) <-> (n | p) /\ (m | p). +Proof. + intros. split. split. + transitivity (lcm n m); trivial using divide_lcm_l. + transitivity (lcm n m); trivial using divide_lcm_r. + intros (H,H'). now apply lcm_least. +Qed. + +Lemma lcm_unique : forall n m p, + 0<=p -> (n|p) -> (m|p) -> + (forall q, (n|q) -> (m|q) -> (p|q)) -> + lcm n m == p. +Proof. + intros n m p Hp Hn Hm H. + apply divide_antisym; trivial. + now apply lcm_least. + apply H. apply divide_lcm_l. apply divide_lcm_r. +Qed. + +Lemma lcm_unique_alt : forall n m p, 0<=p -> + (forall q, (p|q) <-> (n|q) /\ (m|q)) -> + lcm n m == p. +Proof. + intros n m p Hp H. + apply lcm_unique; trivial. + apply -> H. apply divide_refl. + apply -> H. apply divide_refl. + intros. apply H. now split. +Qed. + +Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p. +Proof. + intros. apply lcm_unique_alt. apply le_0_l. + intros. now rewrite !lcm_divide_iff, and_assoc. +Qed. + +Lemma lcm_0_l : forall n, lcm 0 n == 0. +Proof. + intros. apply lcm_unique; trivial. order. + apply divide_refl. + apply divide_0_r. +Qed. + +Lemma lcm_0_r : forall n, lcm n 0 == 0. +Proof. + intros. now rewrite lcm_comm, lcm_0_l. +Qed. + +Lemma lcm_1_l : forall n, lcm 1 n == n. +Proof. + intros. apply lcm_unique; trivial using divide_1_l, le_0_l, divide_refl. +Qed. + +Lemma lcm_1_r : forall n, lcm n 1 == n. +Proof. + intros. now rewrite lcm_comm, lcm_1_l. +Qed. + +Lemma lcm_diag : forall n, lcm n n == n. +Proof. + intros. apply lcm_unique; trivial using divide_refl, le_0_l. +Qed. + +Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0. +Proof. + intros. split. + intros EQ. + apply eq_mul_0. + apply divide_0_l. rewrite <- EQ. apply lcm_least. + apply divide_factor_l. apply divide_factor_r. + destruct 1 as [EQ|EQ]; rewrite EQ. apply lcm_0_l. apply lcm_0_r. +Qed. + +Lemma divide_lcm_eq_r : forall n m, (n|m) -> lcm n m == m. +Proof. + intros n m H. apply lcm_unique_alt; trivial using le_0_l. + intros q. split. split; trivial. now transitivity m. + now destruct 1. +Qed. + +Lemma divide_lcm_iff : forall n m, (n|m) <-> lcm n m == m. +Proof. + intros n m. split. now apply divide_lcm_eq_r. + intros EQ. rewrite <- EQ. apply divide_lcm_l. +Qed. + +Lemma lcm_mul_mono_l : + forall n m p, lcm (p * n) (p * m) == p * lcm n m. +Proof. + intros n m p. + destruct (eq_decidable p 0) as [Hp|Hp]. + rewrite Hp. nzsimpl. rewrite lcm_0_l. now nzsimpl. + destruct (eq_decidable (gcd n m) 0) as [Hg|Hg]. + apply gcd_eq_0 in Hg. destruct Hg as (Hn,Hm); rewrite Hn, Hm. + nzsimpl. rewrite lcm_0_l. now nzsimpl. + unfold lcm. + rewrite gcd_mul_mono_l. + rewrite mul_assoc. apply mul_wd; try easy. + now rewrite div_mul_cancel_l. +Qed. + +Lemma lcm_mul_mono_r : + forall n m p, lcm (n * p) (m * p) == lcm n m * p. +Proof. + intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm. +Qed. + +Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> + (gcd n m == 1 <-> lcm n m == n*m). +Proof. + intros n m Hn Hm. split; intros H. + unfold lcm. rewrite H. now rewrite div_1_r. + unfold lcm in *. + apply mul_cancel_l in H; trivial. + assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order). + assert (H' := gcd_divide_r n m). + apply mod_divide in H'; trivial. apply div_exact in H'; trivial. + rewrite H in H'. + rewrite <- (mul_1_l m) in H' at 1. + now apply mul_cancel_r in H'. +Qed. + +End NLcmProp. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 3fc44124f..58e3afe78 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -7,10 +7,10 @@ (************************************************************************) Require Export NAxioms. -Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd. +Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm. (** This functor summarizes all known facts about N. *) Module Type NProp (N:NAxiomsSig) := NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N - <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N. + <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 73ed4e814..1b5d382a3 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -141,7 +141,8 @@ Program Instance div_wd : Proper (eq==>eq==>eq) Ndiv. Program Instance mod_wd : Proper (eq==>eq==>eq) Nmod. Definition div_mod := fun x y (_:y<>0) => Ndiv_mod_eq x y. -Definition mod_upper_bound := Nmod_lt. +Definition mod_bound_pos : forall a b, 0<=a -> 0<b -> 0<= a mod b < b. +Proof. split. now destruct (a mod b). apply Nmod_lt. now destruct b. Qed. (** Odd and Even *) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index ce8e03a5a..60c59b323 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -127,9 +127,9 @@ Proof. now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U. Qed. -Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y. +Lemma mod_bound_pos : forall x y, 0<=x -> 0<y -> 0 <= x mod y < y. Proof. - intros x y Hy. + intros x y Hx Hy. split. auto with arith. destruct y; [ now elim Hy | clear Hy ]. unfold modulo. apply le_n_S, le_minus. @@ -515,7 +515,7 @@ Definition modulo := modulo. Program Instance div_wd : Proper (eq==>eq==>eq) div. Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. Definition div_mod := div_mod. -Definition mod_upper_bound := mod_upper_bound. +Definition mod_bound_pos := mod_bound_pos. Definition divide := divide. Definition gcd := gcd. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 7b90aa09e..6760cfc81 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -292,11 +292,10 @@ Proof. intros a b. zify. intros. apply Z_div_mod_eq_full; auto. Qed. -Theorem mod_upper_bound : forall a b, ~b==0 -> modulo a b < b. +Theorem mod_bound_pos : forall a b, 0<=a -> 0<b -> + 0 <= modulo a b /\ modulo a b < b. Proof. -intros a b. zify. intros. -destruct (Z_mod_lt [a] [b]); auto. -generalize (spec_pos b); auto with zarith. +intros a b. zify. apply Z.mod_bound_pos. Qed. (** Gcd *) diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index e380d835e..408d8e59b 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -23,7 +23,6 @@ Integer/Abstract/ZLt.vo Integer/Abstract/ZMulOrder.vo Integer/Abstract/ZMul.vo Integer/Abstract/ZSgnAbs.vo -Integer/Abstract/ZProperties.vo Integer/Abstract/ZDivFloor.vo Integer/Abstract/ZDivTrunc.vo Integer/Abstract/ZDivEucl.vo @@ -31,6 +30,8 @@ Integer/Abstract/ZMaxMin.vo Integer/Abstract/ZParity.vo Integer/Abstract/ZPow.vo Integer/Abstract/ZGcd.vo +Integer/Abstract/ZLcm.vo +Integer/Abstract/ZProperties.vo Integer/BigZ/BigZ.vo Integer/BigZ/ZMake.vo Integer/Binary/ZBinary.vo diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index f8a08bf4e..ffc5b91bc 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -22,7 +22,7 @@ Require Import Orders NPeano POrderedType NArith Module Nat_as_OT := NPeano.Nat. Module Positive_as_OT := POrderedType.Positive_as_OT. Module N_as_OT := NArith.N. -Module Z_as_OT := ZArith.Z. +Module Z_as_OT := ZBinary.Z. (** An OrderedType can now directly be seen as a DecidableType *) diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 3956e9160..26d700773 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -12,7 +12,7 @@ Require Export ZArith_base. (** Extra definitions *) -Require Export Zpow_def Zsqrt_def Zlog_def Zgcd_def. +Require Export Zpow_def Zsqrt_def Zlog_def Zgcd_def Zdiv_def. (** Extra modules using [Omega] or [Ring]. *) @@ -22,7 +22,3 @@ Require Export Zdiv. Require Export Zlogarithm. Export ZArithRing. - -(** Final Z module, cumulating ZBinary.Z and Zdiv.Z *) - -Module Z := Zdiv.Z. diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v deleted file mode 100644 index df81fa9a6..000000000 --- a/theories/ZArith/ZOdiv.v +++ /dev/null @@ -1,563 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - - -Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms. -Require Export Ndiv_def ZOdiv_def. -Require Zdiv ZBinary ZDivTrunc. - -Open Scope Z_scope. - -(** This file provides results about the Round-Toward-Zero Euclidean - division [ZOdiv_eucl], whose projections are [ZOdiv] and [ZOmod]. - Definition of this division can be found in file [ZOdiv_def]. - - This division and the one defined in Zdiv agree only on positive - numbers. Otherwise, Zdiv performs Round-Toward-Bottom. - - The current approach is compatible with the division of usual - programming languages such as Ocaml. In addition, it has nicer - properties with respect to opposite and other usual operations. -*) - -(** Since ZOdiv and Zdiv are not meant to be used concurrently, - we reuse the same notation. *) - -Infix "/" := ZOdiv : Z_scope. -Infix "mod" := ZOmod (at level 40, no associativity) : Z_scope. - -(* -(** Auxiliary results on the ad-hoc comparison [NPgeb]. *) - -Lemma NPgeb_Zge : forall (n:N)(p:positive), - NPgeb n p = true -> Z_of_N n >= Zpos p. -Proof. - destruct n as [|n]; simpl; intros. - discriminate. - red; simpl; destruct Pcompare; now auto. -Qed. - -Lemma NPgeb_Zlt : forall (n:N)(p:positive), - NPgeb n p = false -> Z_of_N n < Zpos p. -Proof. - destruct n as [|n]; simpl; intros. - red; auto. - red; simpl; destruct Pcompare; now auto. -Qed. -*) - -(** * Relation between division on N and on Z. *) - -Lemma Ndiv_Z0div : forall a b:N, - Z_of_N (a/b) = (Z_of_N a / Z_of_N b). -Proof. - intros. - destruct a; destruct b; simpl; auto. - unfold Ndiv, ZOdiv; simpl; destruct Pdiv_eucl; auto. -Qed. - -Lemma Nmod_Z0mod : forall a b:N, - Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b). -Proof. - intros. - destruct a; destruct b; simpl; auto. - unfold Nmod, ZOmod; simpl; destruct Pdiv_eucl; auto. -Qed. - -(** * Characterization of this euclidean division. *) - -(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] - has been chosen to be [a], so this equation holds even for [b=0]. -*) - -Theorem ZO_div_mod_eq : forall a b, - a = b * (ZOdiv a b) + (ZOmod a b). -Proof. - intros; generalize (ZOdiv_eucl_correct a b). - unfold ZOdiv, ZOmod; destruct ZOdiv_eucl; simpl. - intro H; rewrite H; rewrite Zmult_comm; auto. -Qed. - -(** Then, the inequalities constraining the remainder: - The remainder is bounded by the divisor, in term of absolute values *) - -Theorem ZOmod_lt : forall a b:Z, b<>0 -> - Zabs (a mod b) < Zabs b. -Proof. - destruct b as [ |b|b]; intro H; try solve [elim H;auto]; - destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl; - generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; - try rewrite Zabs_Zopp; rewrite Zabs_eq; auto using Z_of_N_le_0; - intros LT; apply (Z_of_N_lt _ _ LT). -Qed. - -(** The sign of the remainder is the one of [a]. Due to the possible - nullity of [a], a general result is to be stated in the following form: -*) - -Theorem ZOmod_sgn : forall a b:Z, - 0 <= Zsgn (a mod b) * Zsgn a. -Proof. - destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith; - unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; - simpl; destruct n0; simpl; auto with zarith. -Qed. - -(** This can also be said in a simplier way: *) - -Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z. -Proof. - destruct z; simpl; intuition auto with zarith. -Qed. - -Theorem ZOmod_sgn2 : forall a b:Z, - 0 <= (a mod b) * a. -Proof. - intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply ZOmod_sgn. -Qed. - -(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2 - then 4 particular cases. *) - -Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 -> - 0 <= a mod b < Zabs b. -Proof. - intros. - assert (0 <= a mod b). - generalize (ZOmod_sgn a b). - destruct (Zle_lt_or_eq 0 a H). - rewrite <- Zsgn_pos in H1; rewrite H1; romega with *. - subst a; simpl; auto. - generalize (ZOmod_lt a b H0); romega with *. -Qed. - -Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 -> - -Zabs b < a mod b <= 0. -Proof. - intros. - assert (a mod b <= 0). - generalize (ZOmod_sgn a b). - destruct (Zle_lt_or_eq a 0 H). - rewrite <- Zsgn_neg in H1; rewrite H1; romega with *. - subst a; simpl; auto. - generalize (ZOmod_lt a b H0); romega with *. -Qed. - -Theorem ZOmod_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a mod b < b. -Proof. - intros; generalize (ZOmod_lt_pos a b); romega with *. -Qed. - -Theorem ZOmod_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a mod b < -b. -Proof. - intros; generalize (ZOmod_lt_pos a b); romega with *. -Qed. - -Theorem ZOmod_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a mod b <= 0. -Proof. - intros; generalize (ZOmod_lt_neg a b); romega with *. -Qed. - -Theorem ZOmod_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a mod b <= 0. -Proof. - intros; generalize (ZOmod_lt_neg a b); romega with *. -Qed. - -(** * Division and Opposite *) - -(* The precise equalities that are invalid with "historic" Zdiv. *) - -Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b). -Proof. - destruct a; destruct b; simpl; auto; - unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. -Qed. - -Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b). -Proof. - destruct a; destruct b; simpl; auto; - unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. -Qed. - -Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b). -Proof. - destruct a; destruct b; simpl; auto; - unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. -Qed. - -Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b. -Proof. - destruct a; destruct b; simpl; auto; - unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. -Qed. - -Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. -Proof. - destruct a; destruct b; simpl; auto; - unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. -Qed. - -Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b). -Proof. - destruct a; destruct b; simpl; auto; - unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. -Qed. - -(** We know enough to prove that [ZOdiv] and [ZOmod] are instances of - one of the abstract Euclidean divisions of Numbers. *) - -Module ZODiv <: ZDivTrunc.ZDiv ZBinary.Z. - Definition div := ZOdiv. - Definition modulo := ZOmod. - Local Obligation Tactic := simpl_relation. - Program Instance div_wd : Proper (eq==>eq==>eq) div. - Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. - - Definition div_mod := fun a b (_:b<>0) => ZO_div_mod_eq a b. - Definition mod_bound := ZOmod_lt_pos_pos. - Definition mod_opp_l := fun a b (_:b<>0) => ZOmod_opp_l a b. - Definition mod_opp_r := fun a b (_:b<>0) => ZOmod_opp_r a b. -End ZODiv. - -Module ZODivMod := ZBinary.Z <+ ZODiv. - -(** We hence benefit from generic results about this abstract division. *) - -Module Z := ZDivTrunc.ZDivProp ZODivMod ZBinary.Z. - -(** * Unicity results *) - -Definition Remainder a b r := - (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0). - -Definition Remainder_alt a b r := - Zabs r < Zabs b /\ 0 <= r * a. - -Lemma Remainder_equiv : forall a b r, - Remainder a b r <-> Remainder_alt a b r. -Proof. - unfold Remainder, Remainder_alt; intuition. - romega with *. - romega with *. - rewrite <-(Zmult_opp_opp). - apply Zmult_le_0_compat; romega. - assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto). - destruct r; simpl Zsgn in *; romega with *. -Qed. - -Theorem ZOdiv_mod_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> q = a/b /\ r = a mod b. -Proof. - destruct 1 as [(H,H0)|(H,H0)]; intros. - apply Zdiv.Zdiv_mod_unique with b; auto. - apply ZOmod_lt_pos; auto. - romega with *. - rewrite <- H1; apply ZO_div_mod_eq. - - rewrite <- (Zopp_involutive a). - rewrite ZOdiv_opp_l, ZOmod_opp_l. - generalize (Zdiv.Zdiv_mod_unique b (-q) (-a/b) (-r) (-a mod b)). - generalize (ZOmod_lt_pos (-a) b). - rewrite <-ZO_div_mod_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1. - romega with *. -Qed. - -Theorem ZOdiv_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> q = a/b. -Proof. - intros; destruct (ZOdiv_mod_unique_full a b q r); auto. -Qed. - -Theorem ZOdiv_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> - a = b*q + r -> q = a/b. -Proof. exact Z.div_unique. Qed. - -Theorem ZOmod_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> r = a mod b. -Proof. - intros; destruct (ZOdiv_mod_unique_full a b q r); auto. -Qed. - -Theorem ZOmod_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> - a = b*q + r -> r = a mod b. -Proof. exact Z.mod_unique. Qed. - -(** * Basic values of divisions and modulo. *) - -Lemma ZOmod_0_l: forall a, 0 mod a = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma ZOmod_0_r: forall a, a mod 0 = a. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma ZOdiv_0_l: forall a, 0/a = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma ZOdiv_0_r: forall a, a/0 = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma ZOmod_1_r: forall a, a mod 1 = 0. -Proof. exact Z.mod_1_r. Qed. - -Lemma ZOdiv_1_r: forall a, a/1 = a. -Proof. exact Z.div_1_r. Qed. - -Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r - : zarith. - -Lemma ZOdiv_1_l: forall a, 1 < a -> 1/a = 0. -Proof. exact Z.div_1_l. Qed. - -Lemma ZOmod_1_l: forall a, 1 < a -> 1 mod a = 1. -Proof. exact Z.mod_1_l. Qed. - -Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1. -Proof. exact Z.div_same. Qed. - -Ltac zero_or_not a := - destruct (Z_eq_dec a 0); - [subst; rewrite ?ZOmod_0_l, ?ZOdiv_0_l, ?ZOmod_0_r, ?ZOdiv_0_r; - auto with zarith|]. - -Lemma ZO_mod_same : forall a, a mod a = 0. -Proof. intros. zero_or_not a. apply Z.mod_same; auto. Qed. - -Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0. -Proof. intros. zero_or_not b. apply Z.mod_mul; auto. Qed. - -Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a. -Proof. exact Z.div_mul. Qed. - -(** * Order results about ZOmod and ZOdiv *) - -(* Division of positive numbers is positive. *) - -Lemma ZO_div_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a/b. -Proof. intros. zero_or_not b. apply Z.div_pos; auto with zarith. Qed. - -(** As soon as the divisor is greater or equal than 2, - the division is strictly decreasing. *) - -Lemma ZO_div_lt : forall a b:Z, 0 < a -> 2 <= b -> a/b < a. -Proof. intros. apply Z.div_lt; auto with zarith. Qed. - -(** A division of a small number by a bigger one yields zero. *) - -Theorem ZOdiv_small: forall a b, 0 <= a < b -> a/b = 0. -Proof. exact Z.div_small. Qed. - -(** Same situation, in term of modulo: *) - -Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a. -Proof. exact Z.mod_small. Qed. - -(** [Zge] is compatible with a positive division. *) - -Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c. -Proof. intros. zero_or_not c. apply Z.div_le_mono; auto with zarith. Qed. - -(** With our choice of division, rounding of (a/b) is always done toward zero: *) - -Lemma ZO_mult_div_le : forall a b:Z, 0 <= a -> 0 <= b*(a/b) <= a. -Proof. intros. zero_or_not b. apply Z.mul_div_le; auto with zarith. Qed. - -Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0. -Proof. intros. zero_or_not b. apply Z.mul_div_ge; auto with zarith. Qed. - -(** The previous inequalities between [b*(a/b)] and [a] are exact - iff the modulo is zero. *) - -Lemma ZO_div_exact_full : forall a b:Z, a = b*(a/b) <-> a mod b = 0. -Proof. intros. zero_or_not b. intuition. apply Z.div_exact; auto. Qed. - -(** A modulo cannot grow beyond its starting point. *) - -Theorem ZOmod_le: forall a b, 0 <= a -> 0 <= b -> a mod b <= a. -Proof. intros. zero_or_not b. apply Z.mod_le; auto with zarith. Qed. - -(** Some additionnal inequalities about Zdiv. *) - -Theorem ZOdiv_le_upper_bound: - forall a b q, 0 < b -> a <= q*b -> a/b <= q. -Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_upper_bound. Qed. - -Theorem ZOdiv_lt_upper_bound: - forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. -Proof. intros a b q; rewrite Zmult_comm; apply Z.div_lt_upper_bound. Qed. - -Theorem ZOdiv_le_lower_bound: - forall a b q, 0 < b -> q*b <= a -> q <= a/b. -Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_lower_bound. Qed. - -Theorem ZOdiv_sgn: forall a b, - 0 <= Zsgn (a/b) * Zsgn a * Zsgn b. -Proof. - destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; - unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith. -Qed. - -(** * Relations between usual operations and Zmod and Zdiv *) - -(** First, a result that used to be always valid with Zdiv, - but must be restricted here. - For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2 *) - -Lemma ZO_mod_plus : forall a b c:Z, - 0 <= (a+b*c) * a -> - (a + b * c) mod c = a mod c. -Proof. intros. zero_or_not c. apply Z.mod_add; auto with zarith. Qed. - -Lemma ZO_div_plus : forall a b c:Z, - 0 <= (a+b*c) * a -> c<>0 -> - (a + b * c) / c = a / c + b. -Proof. intros. apply Z.div_add; auto with zarith. Qed. - -Theorem ZO_div_plus_l: forall a b c : Z, - 0 <= (a*b+c)*c -> b<>0 -> - b<>0 -> (a * b + c) / b = a + c / b. -Proof. intros. apply Z.div_add_l; auto with zarith. Qed. - -(** Cancellations. *) - -Lemma ZOdiv_mult_cancel_r : forall a b c:Z, - c<>0 -> (a*c)/(b*c) = a/b. -Proof. intros. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed. - -Lemma ZOdiv_mult_cancel_l : forall a b c:Z, - c<>0 -> (c*a)/(c*b) = a/b. -Proof. - intros. rewrite (Zmult_comm c b). zero_or_not b. - rewrite (Zmult_comm b c). apply Z.div_mul_cancel_l; auto. -Qed. - -Lemma ZOmult_mod_distr_l: forall a b c, - (c*a) mod (c*b) = c * (a mod b). -Proof. - intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b. - rewrite (Zmult_comm b c). apply Z.mul_mod_distr_l; auto. -Qed. - -Lemma ZOmult_mod_distr_r: forall a b c, - (a*c) mod (b*c) = (a mod b) * c. -Proof. - intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c. - rewrite (Zmult_comm c b). apply Z.mul_mod_distr_r; auto. -Qed. - -(** Operations modulo. *) - -Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n. -Proof. intros. zero_or_not n. apply Z.mod_mod; auto. Qed. - -Theorem ZOmult_mod: forall a b n, - (a * b) mod n = ((a mod n) * (b mod n)) mod n. -Proof. intros. zero_or_not n. apply Z.mul_mod; auto. Qed. - -(** addition and modulo - - Generally speaking, unlike with Zdiv, we don't have - (a+b) mod n = (a mod n + b mod n) mod n - for any a and b. - For instance, take (8 + (-10)) mod 3 = -2 whereas - (8 mod 3 + (-10 mod 3)) mod 3 = 1. *) - -Theorem ZOplus_mod: forall a b n, - 0 <= a * b -> - (a + b) mod n = (a mod n + b mod n) mod n. -Proof. intros. zero_or_not n. apply Z.add_mod; auto. Qed. - -Lemma ZOplus_mod_idemp_l: forall a b n, - 0 <= a * b -> - (a mod n + b) mod n = (a + b) mod n. -Proof. intros. zero_or_not n. apply Z.add_mod_idemp_l; auto. Qed. - -Lemma ZOplus_mod_idemp_r: forall a b n, - 0 <= a*b -> - (b + a mod n) mod n = (b + a) mod n. -Proof. - intros. zero_or_not n. apply Z.add_mod_idemp_r; auto. - rewrite Zmult_comm; auto. Qed. - -Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n. -Proof. intros. zero_or_not n. apply Z.mul_mod_idemp_l; auto. Qed. - -Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n. -Proof. intros. zero_or_not n. apply Z.mul_mod_idemp_r; auto. Qed. - -(** Unlike with Zdiv, the following result is true without restrictions. *) - -Lemma ZOdiv_ZOdiv : forall a b c, (a/b)/c = a/(b*c). -Proof. - intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c. - rewrite Zmult_comm. apply Z.div_div; auto. -Qed. - -(** A last inequality: *) - -Theorem ZOdiv_mult_le: - forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. -Proof. intros. zero_or_not b. apply Z.div_mul_le; auto with zarith. Qed. - -(** ZOmod is related to divisibility (see more in Znumtheory) *) - -Lemma ZOmod_divides : forall a b, - a mod b = 0 <-> exists c, a = b*c. -Proof. intros. zero_or_not b. firstorder. apply Z.mod_divides; auto. Qed. - -(** * Interaction with "historic" Zdiv *) - -(** They agree at least on positive numbers: *) - -Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> - a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b. -Proof. - intros. - apply Zdiv.Zdiv_mod_unique with b. - apply ZOmod_lt_pos; auto with zarith. - rewrite Zabs_eq; auto with *; apply Zdiv.Z_mod_lt; auto with *. - rewrite <- Zdiv.Z_div_mod_eq; auto with *. - symmetry; apply ZO_div_mod_eq; auto with *. -Qed. - -Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> - a/b = Zdiv.Zdiv a b. -Proof. - intros a b Ha Hb. - destruct (Zle_lt_or_eq _ _ Hb). - generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha H); intuition. - subst; rewrite ZOdiv_0_r, Zdiv.Zdiv_0_r; reflexivity. -Qed. - -Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b -> - a mod b = Zdiv.Zmod a b. -Proof. - intros a b Ha Hb; generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha Hb); - intuition. -Qed. - -(** Modulos are null at the same places *) - -Theorem ZOmod_Zmod_zero : forall a b, b<>0 -> - (a mod b = 0 <-> Zdiv.Zmod a b = 0). -Proof. - intros. - rewrite ZOmod_divides, Zdiv.Zmod_divides; intuition. -Qed. diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v deleted file mode 100644 index 1fb238f2b..000000000 --- a/theories/ZArith/ZOdiv_def.v +++ /dev/null @@ -1,56 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - - -Require Import BinPos BinNat Nnat ZArith_base Ndiv_def. - -Open Scope Z_scope. - -Definition ZOdiv_eucl (a b:Z) : Z * Z := - match a, b with - | Z0, _ => (Z0, Z0) - | _, Z0 => (Z0, a) - | Zpos na, Zpos nb => - let (nq, nr) := Pdiv_eucl na nb in - (Z_of_N nq, Z_of_N nr) - | Zneg na, Zpos nb => - let (nq, nr) := Pdiv_eucl na nb in - (Zopp (Z_of_N nq), Zopp (Z_of_N nr)) - | Zpos na, Zneg nb => - let (nq, nr) := Pdiv_eucl na nb in - (Zopp (Z_of_N nq), Z_of_N nr) - | Zneg na, Zneg nb => - let (nq, nr) := Pdiv_eucl na nb in - (Z_of_N nq, Zopp (Z_of_N nr)) - end. - -Definition ZOdiv a b := fst (ZOdiv_eucl a b). -Definition ZOmod a b := snd (ZOdiv_eucl a b). - -(* Proofs of specifications for this euclidean division. *) - -Theorem ZOdiv_eucl_correct: forall a b, - let (q,r) := ZOdiv_eucl a b in a = q * b + r. -Proof. - destruct a; destruct b; simpl; auto; - generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros q r H. - - change (Zpos p) with (Z_of_N (Npos p)). rewrite H. - rewrite Z_of_N_plus, Z_of_N_mult. reflexivity. - - change (Zpos p) with (Z_of_N (Npos p)). rewrite H. - rewrite Z_of_N_plus, Z_of_N_mult. rewrite Zmult_opp_comm. reflexivity. - - change (Zneg p) with (-(Z_of_N (Npos p))); rewrite H. - rewrite Z_of_N_plus, Z_of_N_mult. - rewrite Zopp_plus_distr, Zopp_mult_distr_l; trivial. - - change (Zneg p) with (-(Z_of_N (Npos p))); rewrite H. - rewrite Z_of_N_plus, Z_of_N_mult. - rewrite Zopp_plus_distr, Zopp_mult_distr_r; trivial. -Qed. 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. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index fbedaa3d7..a14f29308 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -7,130 +7,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Contribution by Claude Marché and Xavier Urbain *) +(** * Euclidean Division *) -(** Euclidean Division +(** Initial Contribution by Claude Marché and Xavier Urbain *) - Defines first of function that allows Coq to normalize. - Then only after proves the main required property. -*) - -Require Export ZArith_base. +Require Export ZArith_base Zdiv_def. Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms. Require ZDivFloor. -Open Local Scope Z_scope. - -(** * Definitions of Euclidian operations *) - -(** Euclidean division of a positive by a integer - (that is supposed to be positive). - - Total function than returns an arbitrary value when - divisor is not positive - -*) - -Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z := - match a with - | xH => if Zge_bool b 2 then (0, 1) else (1, 0) - | xO a' => - let (q, r) := Zdiv_eucl_POS a' b in - let r' := 2 * r in - if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) - | xI a' => - let (q, r) := Zdiv_eucl_POS a' b in - let r' := 2 * r + 1 in - if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) - end. - - -(** Euclidean division of integers. - - Total function than returns (0,0) when dividing by 0. -*) - -(** - - The pseudo-code is: - - if b = 0 : (0,0) - - if b <> 0 and a = 0 : (0,0) - - if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in - if r = 0 then (-q,0) else (-(q+1),b-r) - - if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r) - - if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in - if r = 0 then (-q,0) else (-(q+1),b+r) - - In other word, when b is non-zero, q is chosen to be the greatest integer - smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when - r is not null). -*) - -(* Nota: At least two others conventions also exist for euclidean division. - They all satify the equation a=b*q+r, but differ on the choice of (q,r) - on negative numbers. - - * Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b). - Hence (-a) mod b = - (a mod b) - a mod (-b) = a mod b - And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). - - * Another solution is to always pick a non-negative remainder: - a=b*q+r with 0 <= r < |b| -*) - -Definition Zdiv_eucl (a b:Z) : Z * Z := - match a, b with - | Z0, _ => (0, 0) - | _, Z0 => (0, 0) - | Zpos a', Zpos _ => Zdiv_eucl_POS a' b - | Zneg a', Zpos _ => - let (q, r) := Zdiv_eucl_POS a' b in - match r with - | Z0 => (- q, 0) - | _ => (- (q + 1), b - r) - end - | Zneg a', Zneg b' => let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r) - | Zpos a', Zneg b' => - let (q, r) := Zdiv_eucl_POS a' (Zpos b') in - match r with - | Z0 => (- q, 0) - | _ => (- (q + 1), b + r) - end - end. - - -(** Division and modulo are projections of [Zdiv_eucl] *) - -Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q. - -Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. - -(** Syntax *) - -Infix "/" := Zdiv : Z_scope. -Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. - -(* Tests: - -Eval compute in (Zdiv_eucl 7 3). - -Eval compute in (Zdiv_eucl (-7) 3). - -Eval compute in (Zdiv_eucl 7 (-3)). - -Eval compute in (Zdiv_eucl (-7) (-3)). - -*) +Local Open Scope Z_scope. +(** The definition and initial properties are now in file [Zdiv_def] *) -(** * Main division theorem *) +(** * Main division theorems *) -(** First a lemma for two positive arguments *) +(** NB: many things are stated twice for compatibility reasons *) Lemma Z_div_mod_POS : forall b:Z, @@ -138,58 +28,19 @@ Lemma Z_div_mod_POS : forall a:positive, let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b. Proof. -simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *; - fold Zdiv_eucl_POS in |- *; cbv zeta. - -intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. -generalize (Zgt_cases b (2 * r + 1)). -case (Zgt_bool b (2 * r + 1)); - (rewrite BinInt.Zpos_xI; rewrite H0; split; [ ring | omega ]). - -intros p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. -generalize (Zgt_cases b (2 * r)). -case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO; - change (Zpos (xO p)) with (2 * Zpos p) in |- *; rewrite H0; - (split; [ ring | omega ]). - -generalize (Zge_cases b 2). -case (Zge_bool b 2); (intros; split; [ try ring | omega ]). -omega. + intros b Hb a. apply Zgt_lt in Hb. + generalize (Zdiv_eucl_POS_eq a b Hb) (Zmod_POS_bound a b Hb). + destruct Zdiv_eucl_POS. auto. Qed. -(** Then the usual situation of a positive [b] and no restriction on [a] *) - Theorem Z_div_mod : forall a b:Z, b > 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ 0 <= r < b. Proof. - intros a b; case a; case b; try (simpl in |- *; intros; omega). - unfold Zdiv_eucl in |- *; intros; apply Z_div_mod_POS; trivial. - - intros; discriminate. - - intros. - generalize (Z_div_mod_POS (Zpos p) H p0). - unfold Zdiv_eucl in |- *. - case (Zdiv_eucl_POS p0 (Zpos p)). - intros z z0. - case z0. - - intros [H1 H2]. - split; trivial. - change (Zneg p0) with (- Zpos p0); rewrite H1; ring. - - intros p1 [H1 H2]. - split; trivial. - change (Zneg p0) with (- Zpos p0); rewrite H1; ring. - generalize (Zorder.Zgt_pos_0 p1); omega. - - intros p1 [H1 H2]. - split; trivial. - change (Zneg p0) with (- Zpos p0); rewrite H1; ring. - generalize (Zorder.Zlt_neg_0 p1); omega. - - intros; discriminate. + intros a b Hb. apply Zgt_lt in Hb. + assert (Hb' : b<>0) by (now destruct b). + generalize (Zdiv_eucl_eq a b Hb') (Zmod_pos_bound a b Hb). + unfold Zmod. destruct Zdiv_eucl. auto. Qed. (** For stating the fully general result, let's give a short name @@ -217,37 +68,14 @@ Theorem Z_div_mod_full : forall a b:Z, b <> 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ Remainder r b. Proof. - destruct b as [|b|b]. - (* b = 0 *) - intro H; elim H; auto. - (* b > 0 *) - intros _. - assert (Zpos b > 0) by auto with zarith. - generalize (Z_div_mod a (Zpos b) H). - destruct Zdiv_eucl as (q,r); intuition; simpl; auto. - (* b < 0 *) - intros _. - assert (Zpos b > 0) by auto with zarith. - generalize (Z_div_mod a (Zpos b) H). - unfold Remainder. - destruct a as [|a|a]. - (* a = 0 *) - simpl; intuition. - (* a > 0 *) - unfold Zdiv_eucl; destruct Zdiv_eucl_POS as (q,r). - destruct r as [|r|r]; [ | | omega with *]. - rewrite <- Zmult_opp_comm; simpl Zopp; intuition. - rewrite <- Zmult_opp_comm; simpl Zopp. - rewrite Zmult_plus_distr_r; omega with *. - (* a < 0 *) - unfold Zdiv_eucl. - generalize (Z_div_mod_POS (Zpos b) H a). - destruct Zdiv_eucl_POS as (q,r). - destruct r as [|r|r]; change (Zneg b) with (-Zpos b). - rewrite Zmult_opp_comm; omega with *. - rewrite <- Zmult_opp_comm, Zmult_plus_distr_r; - repeat rewrite Zmult_opp_comm; omega. - rewrite Zmult_opp_comm; omega with *. + intros a b Hb. + generalize (Zdiv_eucl_eq a b Hb) + (Zmod_pos_bound a b) (Zmod_neg_bound a b). + unfold Zmod. destruct Zdiv_eucl as (q,r). + intros EQ POS NEG. + split; auto. + red; destruct b. + now destruct Hb. left; now apply POS. right; now apply NEG. Qed. (** The same results as before, stated separately in terms of Zdiv and Zmod *) @@ -258,26 +86,13 @@ Proof. destruct Zdiv_eucl; tauto. Qed. -Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= a mod b < b. -Proof. - unfold Zmod; intros a b Hb; generalize (Z_div_mod a b Hb). - destruct Zdiv_eucl; tauto. -Qed. +Definition Z_mod_lt : forall a b:Z, b > 0 -> 0 <= a mod b < b + := fun a b Hb => Zmod_pos_bound a b (Zgt_lt _ _ Hb). -Lemma Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0. -Proof. - unfold Zmod; intros a b Hb. - assert (Hb' : b<>0) by (auto with zarith). - generalize (Z_div_mod_full a b Hb'). - destruct Zdiv_eucl. - unfold Remainder; intuition. -Qed. +Definition Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0 + := Zmod_neg_bound. -Lemma Z_div_mod_eq_full : forall a b:Z, b <> 0 -> a = b*(a/b) + (a mod b). -Proof. - unfold Zdiv, Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb). - destruct Zdiv_eucl; tauto. -Qed. +Notation Z_div_mod_eq_full := Z_div_mod_eq_full (only parsing). Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b*(a/b) + (a mod b). Proof. @@ -285,39 +100,10 @@ Proof. Qed. Lemma Zmod_eq_full : forall a b:Z, b<>0 -> a mod b = a - (a/b)*b. -Proof. - intros. - rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry. - apply Z_div_mod_eq_full; auto. -Qed. +Proof. intros. rewrite Zmult_comm. now apply Z.mod_eq. Qed. Lemma Zmod_eq : forall a b:Z, b>0 -> a mod b = a - (a/b)*b. -Proof. - intros. - rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry. - apply Z_div_mod_eq; auto. -Qed. - -(** We know enough to prove that [Zdiv] and [Zmod] are instances of - one of the abstract Euclidean divisions of Numbers. - We hence benefit from generic results about this abstract division. *) - -Module Z. - - Definition div := Zdiv. - Definition modulo := Zmod. - Local Obligation Tactic := simpl_relation. - Program Instance div_wd : Proper (eq==>eq==>eq) div. - Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. - - Definition div_mod := Z_div_mod_eq_full. - Definition mod_pos_bound : forall a b:Z, 0<b -> 0<=a mod b<b. - Proof. intros; apply Z_mod_lt; auto with zarith. Qed. - Definition mod_neg_bound := Z_mod_neg. - - Include ZBinary.Z <+ ZDivFloor.ZDivProp. - -End Z. +Proof. intros. apply Zmod_eq_full. now destruct b. Qed. (** Existence theorem *) @@ -730,7 +516,10 @@ Proof. Lemma Zmod_divides : forall a b, b<>0 -> (a mod b = 0 <-> exists c, a = b*c). -Proof. exact Z.mod_divides. Qed. +Proof. + intros. rewrite Z.mod_divide; trivial. + split; intros (c,Hc); exists c; auto. +Qed. (** * Compatibility *) @@ -866,16 +655,6 @@ Qed. Implicit Arguments Zdiv_eucl_extended. -(** A third convention: Ocaml. - - See files ZOdiv_def.v and ZOdiv.v. - - Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b). - Hence (-a) mod b = - (a mod b) - a mod (-b) = a mod b - And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). -*) - (** * Division and modulo in Z agree with same in nat: *) Require Import NPeano. @@ -901,3 +680,10 @@ Proof. rewrite <- div_Zdiv, <- inj_mult, <- inj_plus by trivial. now apply inj_eq, Nat.div_mod. Qed. + + +(** For compatibility *) + +Notation Zdiv_eucl := Zdiv_eucl (only parsing). +Notation Zdiv := Zdiv (only parsing). +Notation Zmod := Zmod (only parsing). diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v new file mode 100644 index 000000000..a48170fd1 --- /dev/null +++ b/theories/ZArith/Zdiv_def.v @@ -0,0 +1,310 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Nnat Ndiv_def. +Local Open Scope Z_scope. + +(** * Definitions of divisions for binary integers *) + +(** Concerning the many possible variants of integer divisions, see: + + R. Boute, "The Euclidean definition of the functions div and mod", + ACM Transactions on Programming Languages and Systems, + Vol. 14, No.2, pp. 127-144, April 1992. + + We provide here two flavours: + + - convention Floor (F) : [Zdiv_eucl], [Zdiv], [Zmod] + - convention Trunc (T) : [Zquotrem], [Zquot], [Zrem] + + A third one, the Euclid (E) convention, can be found in file + Zeuclid.v + + For non-zero b, they all satisfy [a = b*(a/b) + (a mod b)] + and [ |a mod b| < |b| ], but the sign of the modulo will differ + when [a<0] and/or [b<0]. + +*) + +(** * Floor *) + +(** [Zdiv_eucl] provides a Truncated-Toward-Bottom (a.k.a Floor) + Euclidean division. Its projections are named [Zdiv] and [Zmod]. + These functions correspond to the `div` and `mod` of Haskell. + This is the historical convention of Coq. + + The main properties of this convention are : + - we have [sgn (a mod b) = sgn (b)] + - [div a b] is the greatest integer smaller or equal to the exact + fraction [a/b]. + - there is no easy sign rule. + + In addition, note that we arbitrary take [a/0 = 0] and [a mod 0 = 0]. +*) + +(** First, a division for positive numbers. Even if the second + argument is a Z, the answer is arbitrary is it isn't a Zpos. *) + +Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z := + match a with + | xH => if Zge_bool b 2 then (0, 1) else (1, 0) + | xO a' => + let (q, r) := Zdiv_eucl_POS a' b in + let r' := 2 * r in + if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) + | xI a' => + let (q, r) := Zdiv_eucl_POS a' b in + let r' := 2 * r + 1 in + if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) + end. + +(** Then the general euclidean division *) + +Definition Zdiv_eucl (a b:Z) : Z * Z := + match a, b with + | 0, _ => (0, 0) + | _, 0 => (0, 0) + | Zpos a', Zpos _ => Zdiv_eucl_POS a' b + | Zneg a', Zpos _ => + let (q, r) := Zdiv_eucl_POS a' b in + match r with + | 0 => (- q, 0) + | _ => (- (q + 1), b - r) + end + | Zneg a', Zneg b' => + let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r) + | Zpos a', Zneg b' => + let (q, r) := Zdiv_eucl_POS a' (Zpos b') in + match r with + | 0 => (- q, 0) + | _ => (- (q + 1), b + r) + end + end. + +Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q. +Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. + +Infix "/" := Zdiv : Z_scope. +Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. + + +(** * Trunc *) + +(** [Zquotrem] provides a Truncated-Toward-Zero Euclidean division. + Its projections are named [Zquot] and [Zrem]. These functions + correspond to the `quot` and `rem` of Haskell, and this division + convention is used in most programming languages, e.g. Ocaml. + + With this convention: + - we have [sgn(a rem b) = sgn(a)] + - sign rule for division: [quot (-a) b = quot a (-b) = -(quot a b)] + - and for modulo: [a rem (-b) = a rem b] and [(-a) rem b = -(a rem b)] + + Note that we arbitrary take here [quot a 0 = 0] and [a rem 0 = a]. +*) + +Definition Zquotrem (a b:Z) : Z * Z := + match a, b with + | 0, _ => (0, 0) + | _, 0 => (0, a) + | Zpos a, Zpos b => + let (q, r) := Pdiv_eucl a b in (Z_of_N q, Z_of_N r) + | Zneg a, Zpos b => + let (q, r) := Pdiv_eucl a b in (- Z_of_N q, - Z_of_N r) + | Zpos a, Zneg b => + let (q, r) := Pdiv_eucl a b in (- Z_of_N q, Z_of_N r) + | Zneg a, Zneg b => + let (q, r) := Pdiv_eucl a b in (Z_of_N q, - Z_of_N r) + end. + +Definition Zquot a b := fst (Zquotrem a b). +Definition Zrem a b := snd (Zquotrem a b). + +Infix "÷" := Zquot (at level 40, left associativity) : Z_scope. +Infix "rem" := Zrem (at level 40, no associativity) : Z_scope. + + + +(** * Euclid *) + +(** In this last convention, the remainder is always non-negative *) + +Definition Zeuclid_mod a b := Zmod a (Zabs b). +Definition Zeuclid_div a b := (Zsgn b) * (Zdiv a (Zabs b)). + + + +(** * Correctness proofs *) + +(** Correctness proofs for Trunc *) + +Lemma Zdiv_eucl_POS_eq : forall a b, 0 < b -> + let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r. +Proof. + intros a b Hb. + induction a; cbv beta iota delta [Zdiv_eucl_POS]; fold Zdiv_eucl_POS. + (* ~1 *) + destruct Zdiv_eucl_POS as (q,r); cbv zeta. + rewrite Zpos_xI, IHa, Zmult_plus_distr_r, Zmult_permute. + destruct Zgt_bool. + now rewrite Zplus_assoc. + now rewrite Zmult_plus_distr_r, Zmult_1_r, <- !Zplus_assoc, Zplus_minus. + (* ~0 *) + destruct Zdiv_eucl_POS as (q,r); cbv zeta. + rewrite (Zpos_xO a), IHa, Zmult_plus_distr_r, Zmult_permute. + destruct Zgt_bool; trivial. + now rewrite Zmult_plus_distr_r, Zmult_1_r, <- !Zplus_assoc, Zplus_minus. + (* ~1 *) + generalize (Zge_cases b 2); destruct Zge_bool; intros Hb'. + now rewrite Zmult_0_r. + replace b with 1. reflexivity. + apply Zle_antisym. now apply Zlt_le_succ in Hb. now apply Zlt_succ_le. +Qed. + +Lemma Zdiv_eucl_eq : forall a b, b<>0 -> + let (q, r) := Zdiv_eucl a b in a = b * q + r. +Proof. + intros [ |a|a] [ |b|b]; unfold Zdiv_eucl; trivial; + (now destruct 1) || intros _; + generalize (Zdiv_eucl_POS_eq a (Zpos b) (eq_refl _)); + destruct Zdiv_eucl_POS as (q,r); try change (Zneg a) with (-Zpos a); + intros ->. + (* Zpos Zpos *) + reflexivity. + (* Zpos Zneg *) + rewrite <- (Zopp_neg b), Zmult_opp_comm. + destruct r as [ |r|r]; trivial. + rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal. + now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l. + rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal. + now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l. + (* Zneg Zpos *) + rewrite (Zopp_plus_distr _ r), Zopp_mult_distr_r. + destruct r as [ |r|r]; trivial; unfold Zminus. + rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal. + now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l. + rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal. + now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l. + (* Zneg Zneg *) + now rewrite (Zopp_plus_distr _ r), Zopp_mult_distr_l. +Qed. + +Lemma Z_div_mod_eq_full : forall a b, b<>0 -> a = b*(a/b) + (a mod b). +Proof. + intros a b Hb. generalize (Zdiv_eucl_eq a b Hb). + unfold Zdiv, Zmod. now destruct Zdiv_eucl. +Qed. + +Lemma Zmod_POS_bound : forall a b, 0<b -> 0 <= snd (Zdiv_eucl_POS a b) < b. +Proof. + assert (AUX : forall a p, a < Zpos (p~0) -> a - Zpos p < Zpos p). + intros. unfold Zminus. apply Zlt_plus_swap. unfold Zminus. + now rewrite Zopp_involutive, Zplus_diag_eq_mult_2, Zmult_comm. + intros a [|b|b] Hb; discriminate Hb || clear Hb. + induction a; cbv beta iota delta [Zdiv_eucl_POS]; fold Zdiv_eucl_POS. + (* ~1 *) + destruct Zdiv_eucl_POS as (q,r). cbv zeta. + simpl in IHa; destruct IHa as (Hr,Hr'). + generalize (Zgt_cases (Zpos b) (2*r+1)). destruct Zgt_bool. + unfold snd in *. + split. apply Zplus_le_0_compat. now apply Zmult_le_0_compat. easy. + now apply Zgt_lt. + unfold snd in *. + split. now apply Zle_minus_le_0. + apply AUX. + destruct r as [|r|r]; try (now destruct Hr); try easy. + red. simpl. apply Pcompare_eq_Lt. exact Hr'. + (* ~0 *) + destruct Zdiv_eucl_POS as (q,r). cbv zeta. + simpl in IHa; destruct IHa as (Hr,Hr'). + generalize (Zgt_cases (Zpos b) (2*r)). destruct Zgt_bool. + unfold snd in *. + split. now apply Zmult_le_0_compat. + now apply Zgt_lt. + unfold snd in *. + split. now apply Zle_minus_le_0. + apply AUX. + destruct r as [|r|r]; try (now destruct Hr); try easy. + (* 1 *) + generalize (Zge_cases (Zpos b) 2). destruct Zge_bool; simpl. + split. easy. now apply Zle_succ_l, Zge_le. + now split. +Qed. + +Lemma Zmod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b. +Proof. + intros a [|b|b] Hb; discriminate Hb || clear Hb. + destruct a as [|a|a]; unfold Zmod, Zdiv_eucl. + now split. + now apply Zmod_POS_bound. + generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)). + destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr'). + destruct r as [|r|r]; (now destruct Hr) || clear Hr. + now split. + split. now apply Zlt_le_weak, Zlt_plus_swap. + now apply Zlt_minus_simpl_swap. +Qed. + +Lemma Zmod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0. +Proof. + intros a [|b|b] Hb; discriminate Hb || clear Hb. + destruct a as [|a|a]; unfold Zmod, Zdiv_eucl. + now split. + generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)). + destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr'). + destruct r as [|r|r]; (now destruct Hr) || clear Hr. + now split. + split. rewrite Zplus_comm. now apply (Zplus_lt_compat_r 0). + rewrite Zplus_comm. apply Zle_plus_swap. simpl. now apply Zlt_le_weak. + generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)). + destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr'). + split. red in Hr'. now rewrite Zcompare_opp in Hr'. now destruct r. +Qed. + +(** Correctness proofs for Floor *) + +Theorem Zquotrem_eq: forall a b, + let (q,r) := Zquotrem a b in a = q * b + r. +Proof. + destruct a, b; simpl; trivial; + generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; trivial; + intros q r H; try change (Zneg p) with (-Zpos p); + rewrite <- (Z_of_N_pos p), H, Z_of_N_plus, Z_of_N_mult; f_equal. + now rewrite Zmult_opp_comm. + now rewrite Zopp_plus_distr, Zopp_mult_distr_l. + now rewrite Zopp_plus_distr, Zopp_mult_distr_r. +Qed. + +Lemma Z_quot_rem_eq : forall a b, a = b*(a÷b) + a rem b. +Proof. + intros a b. rewrite Zmult_comm. generalize (Zquotrem_eq a b). + unfold Zquot, Zrem. now destruct Zquotrem. +Qed. + +Lemma Zrem_bound : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b. +Proof. + intros a [|b|b] Ha Hb; discriminate Hb || clear Hb. + destruct a as [|a|a]; (now destruct Ha) || clear Ha. + compute. now split. + unfold Zrem, Zquotrem. + generalize (Pdiv_eucl_remainder a b). destruct Pdiv_eucl as (q,r). + simpl. split. apply Z_of_N_le_0. + destruct r; red; simpl; trivial. +Qed. + +Lemma Zrem_opp_l : forall a b, (-a) rem b = - (a rem b). +Proof. + intros [|a|a] [|b|b]; trivial; unfold Zrem; + simpl; destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial. +Qed. + +Lemma Zrem_opp_r : forall a b, a rem (-b) = a rem b. +Proof. + intros [|a|a] [|b|b]; trivial; unfold Zrem; simpl; + destruct Pdiv_eucl; simpl; try rewrite Zopp_involutive; trivial. +Qed. diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v new file mode 100644 index 000000000..ece227e10 --- /dev/null +++ b/theories/ZArith/Zeuclid.v @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Morphisms BinInt Zdiv_def ZBinary ZDivEucl. +Local Open Scope Z_scope. + +(** * Definitions of division for binary integers, Euclid convention. *) + +(** In this convention, the remainder is always positive. + For other conventions, see file Zdiv_def. + To avoid collision with the other divisions, we place this one + under a module. +*) + +Module ZEuclid. + + Definition modulo a b := Zmod a (Zabs b). + Definition div a b := (Zsgn b) * (Zdiv a (Zabs b)). + + Instance mod_wd : Proper (eq==>eq==>eq) modulo. + Proof. congruence. Qed. + Instance div_wd : Proper (eq==>eq==>eq) div. + Proof. congruence. Qed. + + Theorem div_mod : forall a b, b<>0 -> + a = b*(div a b) + modulo a b. + Proof. + intros a b Hb. unfold div, modulo. + rewrite Zmult_assoc. rewrite Z.sgn_abs. apply Z.div_mod. + now destruct b. + Qed. + + Lemma mod_always_pos : forall a b, b<>0 -> + 0 <= modulo a b < Zabs b. + Proof. + intros a b Hb. unfold modulo. + apply Z.mod_pos_bound. + destruct b; compute; trivial. now destruct Hb. + Qed. + + Lemma mod_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= modulo a b < b. + Proof. + intros a b _ Hb. rewrite <- (Z.abs_eq b) at 3 by z_order. + apply mod_always_pos. z_order. + Qed. + + Include ZEuclidProp Z Z Z. + +End ZEuclid. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 2866a38fd..c7e6d5750 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -16,7 +16,7 @@ Require Import Zcompare. Require Import Zorder. Require Import Decidable. Require Import Peano_dec. -Require Import Min Max Zmin Zmax. +Require Import Min Max. Require Export Compare_dec. Open Local Scope Z_scope. @@ -76,96 +76,62 @@ Qed. (** Injection and order relations: *) -(** One way ... *) - -Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m. +Theorem inj_compare : forall n m:nat, + (Z_of_nat n ?= Z_of_nat m) = nat_compare n m. Proof. - intros x y; intros H; elim H; - [ unfold Zle in |- *; elim (Zcompare_Eq_iff_eq (Z_of_nat x) (Z_of_nat x)); - intros H1 H2; rewrite H2; [ discriminate | trivial with arith ] - | intros m H1 H2; apply Zle_trans with (Z_of_nat m); - [ assumption | rewrite inj_S; apply Zle_succ ] ]. + induction n; destruct m; trivial. + rewrite 2 inj_S, Zcompare_succ_compat. now simpl. Qed. -Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m. -Proof. - intros x y H; apply Zgt_lt; apply Zle_succ_gt; rewrite <- inj_S; apply inj_le; - exact H. -Qed. +(* Both ways ... *) -Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m. Proof. - intros x y H; apply Zle_ge; apply inj_le; apply H. + intros. unfold Zle. rewrite inj_compare. apply nat_compare_le. Qed. -Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m. +Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m. Proof. - intros x y H; apply Zlt_gt; apply inj_lt; exact H. + intros. unfold Zlt. rewrite inj_compare. apply nat_compare_lt. Qed. -(** The other way ... *) - -Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat. +Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m. Proof. - intros x y H. - destruct (le_lt_dec x y) as [H0|H0]; auto. - exfalso. - assert (H1:=inj_lt _ _ H0). - red in H; red in H1. - rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. + intros. unfold Zge. rewrite inj_compare. apply nat_compare_ge. Qed. -Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat. +Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m. Proof. - intros x y H. - destruct (le_lt_dec y x) as [H0|H0]; auto. - exfalso. - assert (H1:=inj_le _ _ H0). - red in H; red in H1. - rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. + intros. unfold Zgt. rewrite inj_compare. apply nat_compare_gt. Qed. -Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat. -Proof. - intros x y H. - destruct (le_lt_dec y x) as [H0|H0]; auto. - exfalso. - assert (H1:=inj_gt _ _ H0). - red in H; red in H1. - rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. -Qed. +(** One way ... *) -Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat. -Proof. - intros x y H. - destruct (le_lt_dec x y) as [H0|H0]; auto. - exfalso. - assert (H1:=inj_ge _ _ H0). - red in H; red in H1. - rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. -Qed. +Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m. +Proof. apply inj_le_iff. Qed. -(* Both ways ... *) +Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m. +Proof. apply inj_lt_iff. Qed. -Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m. -Proof. - split; [apply inj_le | apply inj_le_rev]. -Qed. +Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +Proof. apply inj_ge_iff. Qed. -Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m. -Proof. - split; [apply inj_lt | apply inj_lt_rev]. -Qed. +Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m. +Proof. apply inj_gt_iff. Qed. -Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m. -Proof. - split; [apply inj_ge | apply inj_ge_rev]. -Qed. +(** The other way ... *) -Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m. -Proof. - split; [apply inj_gt | apply inj_gt_rev]. -Qed. +Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat. +Proof. apply inj_le_iff. Qed. + +Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat. +Proof. apply inj_lt_iff. Qed. + +Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat. +Proof. apply inj_ge_iff. Qed. + +Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat. +Proof. apply inj_gt_iff. Qed. (** Injection and usual operations *) @@ -208,38 +174,38 @@ Theorem inj_minus : forall n m:nat, Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m). Proof. intros. - rewrite Zmax_comm. unfold Zmax. destruct (le_lt_dec m n) as [H|H]. - rewrite (inj_minus1 _ _ H). - assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)). - unfold Zle in H'. - rewrite <- Zcompare_antisym in H'. - destruct Zcompare; simpl in *; intuition. + rewrite inj_minus1; trivial. + apply inj_le, Zle_minus_le_0 in H. revert H. unfold Zle. + case Zcompare_spec; intuition. - rewrite (inj_minus2 _ _ H). - assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)). - rewrite Zplus_opp_r in H'. - unfold Zminus; rewrite H'; auto. + rewrite inj_minus2; trivial. + apply inj_lt, Zlt_gt in H. + apply (Zplus_gt_compat_r _ _ (- Z_of_nat m)) in H. + rewrite Zplus_opp_r in H. + unfold Zminus. rewrite H; auto. Qed. Theorem inj_min : forall n m:nat, Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m). Proof. - induction n; destruct m; try (compute; auto; fail). - simpl min. - do 3 rewrite inj_S. - rewrite <- Zsucc_min_distr; f_equal; auto. + intros n m. unfold Zmin. rewrite inj_compare. + case nat_compare_spec; intros; f_equal. + subst. apply min_idempotent. + apply min_l. auto with arith. + apply min_r. auto with arith. Qed. Theorem inj_max : forall n m:nat, Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m). Proof. - induction n; destruct m; try (compute; auto; fail). - simpl max. - do 3 rewrite inj_S. - rewrite <- Zsucc_max_distr; f_equal; auto. + intros n m. unfold Zmax. rewrite inj_compare. + case nat_compare_spec; intros; f_equal. + subst. apply max_idempotent. + apply max_r. auto with arith. + apply max_l. auto with arith. Qed. (** Composition of injections **) diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v new file mode 100644 index 000000000..307faccfe --- /dev/null +++ b/theories/ZArith/Zquot.v @@ -0,0 +1,511 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms Zdiv. +Require Export Ndiv_def Zdiv_def. +Require ZBinary ZDivTrunc. + +Local Open Scope Z_scope. + +(** This file provides results about the Round-Toward-Zero Euclidean + division [Zquotrem], whose projections are [Zquot] and [Zrem]. + Definition of this division can be found in file [Zdiv_def]. + + This division and the one defined in Zdiv agree only on positive + numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor). + + The current approach is compatible with the division of usual + programming languages such as Ocaml. In addition, it has nicer + properties with respect to opposite and other usual operations. +*) + +(** * Relation between division on N and on Z. *) + +Lemma Ndiv_Zquot : forall a b:N, + Z_of_N (a/b) = (Z_of_N a ÷ Z_of_N b). +Proof. + intros. + destruct a; destruct b; simpl; auto. + unfold Ndiv, Zquot; simpl; destruct Pdiv_eucl; auto. +Qed. + +Lemma Nmod_Zrem : forall a b:N, + Z_of_N (a mod b) = (Z_of_N a) rem (Z_of_N b). +Proof. + intros. + destruct a; destruct b; simpl; auto. + unfold Nmod, Zrem; simpl; destruct Pdiv_eucl; auto. +Qed. + +(** * Characterization of this euclidean division. *) + +(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] + has been chosen to be [a], so this equation holds even for [b=0]. +*) + +Notation Z_quot_rem_eq := Z_quot_rem_eq (only parsing). + +(** Then, the inequalities constraining the remainder: + The remainder is bounded by the divisor, in term of absolute values *) + +Theorem Zrem_lt : forall a b:Z, b<>0 -> + Zabs (a rem b) < Zabs b. +Proof. + destruct b as [ |b|b]; intro H; try solve [elim H;auto]; + destruct a as [ |a|a]; try solve [compute;auto]; unfold Zrem, Zquotrem; + generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; + try rewrite Zabs_Zopp; rewrite Zabs_eq; auto using Z_of_N_le_0; + intros LT; apply (Z_of_N_lt _ _ LT). +Qed. + +(** The sign of the remainder is the one of [a]. Due to the possible + nullity of [a], a general result is to be stated in the following form: +*) + +Theorem Zrem_sgn : forall a b:Z, + 0 <= Zsgn (a rem b) * Zsgn a. +Proof. + destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith; + unfold Zrem, Zquotrem; destruct Pdiv_eucl; + simpl; destruct n0; simpl; auto with zarith. +Qed. + +(** This can also be said in a simplier way: *) + +Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z. +Proof. + destruct z; simpl; intuition auto with zarith. +Qed. + +Theorem Zrem_sgn2 : forall a b:Z, + 0 <= (a rem b) * a. +Proof. + intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply Zrem_sgn. +Qed. + +(** Reformulation of [Zquot_lt] and [Zrem_sgn] in 2 + then 4 particular cases. *) + +Theorem Zrem_lt_pos : forall a b:Z, 0<=a -> b<>0 -> + 0 <= a rem b < Zabs b. +Proof. + intros. + assert (0 <= a rem b). + generalize (Zrem_sgn a b). + destruct (Zle_lt_or_eq 0 a H). + rewrite <- Zsgn_pos in H1; rewrite H1; romega with *. + subst a; simpl; auto. + generalize (Zrem_lt a b H0); romega with *. +Qed. + +Theorem Zrem_lt_neg : forall a b:Z, a<=0 -> b<>0 -> + -Zabs b < a rem b <= 0. +Proof. + intros. + assert (a rem b <= 0). + generalize (Zrem_sgn a b). + destruct (Zle_lt_or_eq a 0 H). + rewrite <- Zsgn_neg in H1; rewrite H1; romega with *. + subst a; simpl; auto. + generalize (Zrem_lt a b H0); romega with *. +Qed. + +Theorem Zrem_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a rem b < b. +Proof. + intros; generalize (Zrem_lt_pos a b); romega with *. +Qed. + +Theorem Zrem_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a rem b < -b. +Proof. + intros; generalize (Zrem_lt_pos a b); romega with *. +Qed. + +Theorem Zrem_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a rem b <= 0. +Proof. + intros; generalize (Zrem_lt_neg a b); romega with *. +Qed. + +Theorem Zrem_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a rem b <= 0. +Proof. + intros; generalize (Zrem_lt_neg a b); romega with *. +Qed. + +(** * Division and Opposite *) + +(* The precise equalities that are invalid with "historic" Zdiv. *) + +Theorem Zquot_opp_l : forall a b:Z, (-a)÷b = -(a÷b). +Proof. + destruct a; destruct b; simpl; auto; + unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem Zquot_opp_r : forall a b:Z, a÷(-b) = -(a÷b). +Proof. + destruct a; destruct b; simpl; auto; + unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem Zrem_opp_l : forall a b:Z, (-a) rem b = -(a rem b). +Proof. + destruct a; destruct b; simpl; auto; + unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem Zrem_opp_r : forall a b:Z, a rem (-b) = a rem b. +Proof. + destruct a; destruct b; simpl; auto; + unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem Zquot_opp_opp : forall a b:Z, (-a)÷(-b) = a÷b. +Proof. + destruct a; destruct b; simpl; auto; + unfold Zquot, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem Zrem_opp_opp : forall a b:Z, (-a) rem (-b) = -(a rem b). +Proof. + destruct a; destruct b; simpl; auto; + unfold Zrem, Zquotrem; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +(** * Unicity results *) + +Definition Remainder a b r := + (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0). + +Definition Remainder_alt a b r := + Zabs r < Zabs b /\ 0 <= r * a. + +Lemma Remainder_equiv : forall a b r, + Remainder a b r <-> Remainder_alt a b r. +Proof. + unfold Remainder, Remainder_alt; intuition. + romega with *. + romega with *. + rewrite <-(Zmult_opp_opp). + apply Zmult_le_0_compat; romega. + assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto). + destruct r; simpl Zsgn in *; romega with *. +Qed. + +Theorem Zquot_mod_unique_full: + forall a b q r, Remainder a b r -> + a = b*q + r -> q = a÷b /\ r = a rem b. +Proof. + destruct 1 as [(H,H0)|(H,H0)]; intros. + apply Zdiv_mod_unique with b; auto. + apply Zrem_lt_pos; auto. + romega with *. + rewrite <- H1; apply Z_quot_rem_eq. + + rewrite <- (Zopp_involutive a). + rewrite Zquot_opp_l, Zrem_opp_l. + generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (-a rem b)). + generalize (Zrem_lt_pos (-a) b). + rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1. + romega with *. +Qed. + +Theorem Zquot_unique_full: + forall a b q r, Remainder a b r -> + a = b*q + r -> q = a÷b. +Proof. + intros; destruct (Zquot_mod_unique_full a b q r); auto. +Qed. + +Theorem Zquot_unique: + forall a b q r, 0 <= a -> 0 <= r < b -> + a = b*q + r -> q = a÷b. +Proof. exact Z.quot_unique. Qed. + +Theorem Zrem_unique_full: + forall a b q r, Remainder a b r -> + a = b*q + r -> r = a rem b. +Proof. + intros; destruct (Zquot_mod_unique_full a b q r); auto. +Qed. + +Theorem Zrem_unique: + forall a b q r, 0 <= a -> 0 <= r < b -> + a = b*q + r -> r = a rem b. +Proof. exact Z.rem_unique. Qed. + +(** * Basic values of divisions and modulo. *) + +Lemma Zrem_0_l: forall a, 0 rem a = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zrem_0_r: forall a, a rem 0 = a. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zquot_0_l: forall a, 0÷a = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zquot_0_r: forall a, a÷0 = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zrem_1_r: forall a, a rem 1 = 0. +Proof. exact Z.rem_1_r. Qed. + +Lemma Zquot_1_r: forall a, a÷1 = a. +Proof. exact Z.quot_1_r. Qed. + +Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r + : zarith. + +Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0. +Proof. exact Z.quot_1_l. Qed. + +Lemma Zrem_1_l: forall a, 1 < a -> 1 rem a = 1. +Proof. exact Z.rem_1_l. Qed. + +Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1. +Proof. exact Z.quot_same. Qed. + +Ltac zero_or_not a := + destruct (Z_eq_dec a 0); + [subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r; + auto with zarith|]. + +Lemma Z_rem_same : forall a, a rem a = 0. +Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed. + +Lemma Z_rem_mult : forall a b, (a*b) rem b = 0. +Proof. intros. zero_or_not b. apply Z.rem_mul; auto. Qed. + +Lemma Z_quot_mult : forall a b:Z, b <> 0 -> (a*b)÷b = a. +Proof. exact Z.quot_mul. Qed. + +(** * Order results about Zrem and Zquot *) + +(* Division of positive numbers is positive. *) + +Lemma Z_quot_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a÷b. +Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed. + +(** As soon as the divisor is greater or equal than 2, + the division is strictly decreasing. *) + +Lemma Z_quot_lt : forall a b:Z, 0 < a -> 2 <= b -> a÷b < a. +Proof. intros. apply Z.quot_lt; auto with zarith. Qed. + +(** A division of a small number by a bigger one yields zero. *) + +Theorem Zquot_small: forall a b, 0 <= a < b -> a÷b = 0. +Proof. exact Z.quot_small. Qed. + +(** Same situation, in term of modulo: *) + +Theorem Zrem_small: forall a n, 0 <= a < n -> a rem n = a. +Proof. exact Z.rem_small. Qed. + +(** [Zge] is compatible with a positive division. *) + +Lemma Z_quot_monotone : forall a b c, 0<=c -> a<=b -> a÷c <= b÷c. +Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed. + +(** With our choice of division, rounding of (a÷b) is always done toward zero: *) + +Lemma Z_mult_quot_le : forall a b:Z, 0 <= a -> 0 <= b*(a÷b) <= a. +Proof. intros. zero_or_not b. apply Z.mul_quot_le; auto with zarith. Qed. + +Lemma Z_mult_quot_ge : forall a b:Z, a <= 0 -> a <= b*(a÷b) <= 0. +Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed. + +(** The previous inequalities between [b*(a÷b)] and [a] are exact + iff the modulo is zero. *) + +Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> a rem b = 0. +Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. + +(** A modulo cannot grow beyond its starting point. *) + +Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> a rem b <= a. +Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. + +(** Some additionnal inequalities about Zdiv. *) + +Theorem Zquot_le_upper_bound: + forall a b q, 0 < b -> a <= q*b -> a÷b <= q. +Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_upper_bound. Qed. + +Theorem Zquot_lt_upper_bound: + forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q. +Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_lt_upper_bound. Qed. + +Theorem Zquot_le_lower_bound: + forall a b q, 0 < b -> q*b <= a -> q <= a÷b. +Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_lower_bound. Qed. + +Theorem Zquot_sgn: forall a b, + 0 <= Zsgn (a÷b) * Zsgn a * Zsgn b. +Proof. + destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; + unfold Zquot; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith. +Qed. + +(** * Relations between usual operations and Zmod and Zdiv *) + +(** First, a result that used to be always valid with Zdiv, + but must be restricted here. + For instance, now (9+(-5)*2) rem 2 = -1 <> 1 = 9 rem 2 *) + +Lemma Z_rem_plus : forall a b c:Z, + 0 <= (a+b*c) * a -> + (a + b * c) rem c = a rem c. +Proof. intros. zero_or_not c. apply Z.rem_add; auto with zarith. Qed. + +Lemma Z_quot_plus : forall a b c:Z, + 0 <= (a+b*c) * a -> c<>0 -> + (a + b * c) ÷ c = a ÷ c + b. +Proof. intros. apply Z.quot_add; auto with zarith. Qed. + +Theorem Z_quot_plus_l: forall a b c : Z, + 0 <= (a*b+c)*c -> b<>0 -> + b<>0 -> (a * b + c) ÷ b = a + c ÷ b. +Proof. intros. apply Z.quot_add_l; auto with zarith. Qed. + +(** Cancellations. *) + +Lemma Zquot_mult_cancel_r : forall a b c:Z, + c<>0 -> (a*c)÷(b*c) = a÷b. +Proof. intros. zero_or_not b. apply Z.quot_mul_cancel_r; auto. Qed. + +Lemma Zquot_mult_cancel_l : forall a b c:Z, + c<>0 -> (c*a)÷(c*b) = a÷b. +Proof. + intros. rewrite (Zmult_comm c b). zero_or_not b. + rewrite (Zmult_comm b c). apply Z.quot_mul_cancel_l; auto. +Qed. + +Lemma Zmult_rem_distr_l: forall a b c, + (c*a) rem (c*b) = c * (a rem b). +Proof. + intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b. + rewrite (Zmult_comm b c). apply Z.mul_rem_distr_l; auto. +Qed. + +Lemma Zmult_rem_distr_r: forall a b c, + (a*c) rem (b*c) = (a rem b) * c. +Proof. + intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c. + rewrite (Zmult_comm c b). apply Z.mul_rem_distr_r; auto. +Qed. + +(** Operations modulo. *) + +Theorem Zrem_rem: forall a n, (a rem n) rem n = a rem n. +Proof. intros. zero_or_not n. apply Z.rem_rem; auto. Qed. + +Theorem Zmult_rem: forall a b n, + (a * b) rem n = ((a rem n) * (b rem n)) rem n. +Proof. intros. zero_or_not n. apply Z.mul_rem; auto. Qed. + +(** addition and modulo + + Generally speaking, unlike with Zdiv, we don't have + (a+b) rem n = (a rem n + b rem n) rem n + for any a and b. + For instance, take (8 + (-10)) rem 3 = -2 whereas + (8 rem 3 + (-10 rem 3)) rem 3 = 1. *) + +Theorem Zplus_rem: forall a b n, + 0 <= a * b -> + (a + b) rem n = (a rem n + b rem n) rem n. +Proof. intros. zero_or_not n. apply Z.add_rem; auto. Qed. + +Lemma Zplus_rem_idemp_l: forall a b n, + 0 <= a * b -> + (a rem n + b) rem n = (a + b) rem n. +Proof. intros. zero_or_not n. apply Z.add_rem_idemp_l; auto. Qed. + +Lemma Zplus_rem_idemp_r: forall a b n, + 0 <= a*b -> + (b + a rem n) rem n = (b + a) rem n. +Proof. + intros. zero_or_not n. apply Z.add_rem_idemp_r; auto. + rewrite Zmult_comm; auto. Qed. + +Lemma Zmult_rem_idemp_l: forall a b n, (a rem n * b) rem n = (a * b) rem n. +Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_l; auto. Qed. + +Lemma Zmult_rem_idemp_r: forall a b n, (b * (a rem n)) rem n = (b * a) rem n. +Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_r; auto. Qed. + +(** Unlike with Zdiv, the following result is true without restrictions. *) + +Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c). +Proof. + intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c. + rewrite Zmult_comm. apply Z.quot_quot; auto. +Qed. + +(** A last inequality: *) + +Theorem Zquot_mult_le: + forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b. +Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed. + +(** Zrem is related to divisibility (see more in Znumtheory) *) + +Lemma Zrem_divides : forall a b, + a rem b = 0 <-> exists c, a = b*c. +Proof. + intros. zero_or_not b. firstorder. + rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto. +Qed. + +(** * Interaction with "historic" Zdiv *) + +(** They agree at least on positive numbers: *) + +Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> + a÷b = a/b /\ a rem b = a mod b. +Proof. + intros. + apply Zdiv_mod_unique with b. + apply Zrem_lt_pos; auto with zarith. + rewrite Zabs_eq; auto with *; apply Z_mod_lt; auto with *. + rewrite <- Z_div_mod_eq; auto with *. + symmetry; apply Z_quot_rem_eq; auto with *. +Qed. + +Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> + a÷b = a/b. +Proof. + intros a b Ha Hb. + destruct (Zle_lt_or_eq _ _ Hb). + generalize (Zquotrem_Zdiv_eucl_pos a b Ha H); intuition. + subst; rewrite Zquot_0_r, Zdiv_0_r; reflexivity. +Qed. + +Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b -> + a rem b = a mod b. +Proof. + intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); + intuition. +Qed. + +(** Modulos are null at the same places *) + +Theorem Zrem_Zmod_zero : forall a b, b<>0 -> + (a rem b = 0 <-> a mod b = 0). +Proof. + intros. + rewrite Zrem_divides, Zmod_divides; intuition. +Qed. diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index bfc52d3e4..ef18d67c7 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -21,8 +21,8 @@ Zmin.vo Zmisc.vo Znat.vo Znumtheory.vo -ZOdiv_def.vo -ZOdiv.vo +Zdiv_def.vo +Zquot.vo Zorder.vo Zpow_def.vo Zpower.vo @@ -31,4 +31,5 @@ Zsqrt_compat.vo Zwf.vo Zsqrt_def.vo Zlog_def.vo -Zgcd_def.vo
\ No newline at end of file +Zgcd_def.vo +Zeuclid.vo |