diff options
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 |