diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/ZArith.v | 6 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv.v | 563 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv_def.v | 56 | ||||
| -rw-r--r-- | theories/ZArith/Zabs.v | 32 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 294 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv_def.v | 310 | ||||
| -rw-r--r-- | theories/ZArith/Zeuclid.v | 54 | ||||
| -rw-r--r-- | theories/ZArith/Znat.v | 140 | ||||
| -rw-r--r-- | theories/ZArith/Zquot.v | 511 | ||||
| -rw-r--r-- | theories/ZArith/vo.itarget | 7 |
10 files changed, 991 insertions, 982 deletions
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 |