diff options
Diffstat (limited to 'theories/Numbers')
22 files changed, 1342 insertions, 429 deletions
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 |