diff options
Diffstat (limited to 'theories/ZArith/ZOdiv.v')
| -rw-r--r-- | theories/ZArith/ZOdiv.v | 947 |
1 files changed, 0 insertions, 947 deletions
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v deleted file mode 100644 index 70f6866e..00000000 --- a/theories/ZArith/ZOdiv.v +++ /dev/null @@ -1,947 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \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. -Require Export ZOdiv_def. -Require Zdiv. - -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. - -Infix "/" := Ndiv : N_scope. -Infix "mod" := Nmod (at level 40, no associativity) : N_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 N_div_mod_eq : forall a b, - a = (b * (Ndiv a b) + (Nmod a b))%N. -Proof. - intros; generalize (Ndiv_eucl_correct a b). - unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl. - intro H; rewrite H; rewrite Nmult_comm; auto. -Qed. - -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. *) - -Theorem Pdiv_eucl_remainder : forall a b:positive, - Z_of_N (snd (Pdiv_eucl a b)) < Zpos b. -Proof. - induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hr1; simpl in Hr1. - case_eq (NPgeb (2*r1+1) b); intros; unfold snd. - romega with *. - apply NPgeb_Zlt; auto. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hr1; simpl in Hr1. - case_eq (NPgeb (2*r1) b); intros; unfold snd. - romega with *. - apply NPgeb_Zlt; auto. - destruct b; simpl; romega with *. -Qed. - -Theorem Nmod_lt : forall (a b:N), b<>0%N -> - (a mod b < b)%N. -Proof. - destruct b as [ |b]; intro H; try solve [elim H;auto]. - destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl. - generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl. - romega with *. -Qed. - -(** 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; apply Z_of_N_le_0. -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. - -(** * 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. - intros; eapply ZOdiv_unique_full; eauto. - red; romega with *. -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. - intros; eapply ZOmod_unique_full; eauto. - red; romega with *. -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. - intros; symmetry; apply ZOmod_unique_full with a; auto with zarith. - rewrite Remainder_equiv; red; simpl; auto with zarith. -Qed. - -Lemma ZOdiv_1_r: forall a, a/1 = a. -Proof. - intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith. - rewrite Remainder_equiv; red; simpl; auto with zarith. -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. - intros; symmetry; apply ZOdiv_unique with 1; auto with zarith. -Qed. - -Lemma ZOmod_1_l: forall a, 1 < a -> 1 mod a = 1. -Proof. - intros; symmetry; apply ZOmod_unique with 0; auto with zarith. -Qed. - -Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1. -Proof. - intros; symmetry; apply ZOdiv_unique_full with 0; auto with *. - rewrite Remainder_equiv; red; simpl; romega with *. -Qed. - -Lemma ZO_mod_same : forall a, a mod a = 0. -Proof. - destruct a; intros; symmetry. - compute; auto. - apply ZOmod_unique with 1; auto with *; romega with *. - apply ZOmod_unique_full with 1; auto with *; red; romega with *. -Qed. - -Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0. -Proof. - intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb]. - subst; simpl; rewrite ZOmod_0_r; auto with zarith. - symmetry; apply ZOmod_unique_full with a; [ red; romega with * | ring ]. -Qed. - -Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a. -Proof. - intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith; - [ red; romega with * | ring]. -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. - destruct (Zle_lt_or_eq 0 b H0). - assert (H2:=ZOmod_lt_pos_pos a b H H1). - rewrite (ZO_div_mod_eq a b) in H. - destruct (Z_lt_le_dec (a/b) 0); auto. - assert (b*(a/b) <= -b). - replace (-b) with (b*-1); [ | ring]. - apply Zmult_le_compat_l; auto with zarith. - romega. - subst b; rewrite ZOdiv_0_r; auto. -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. - assert (Hb : 0 < b) by romega. - assert (H1 : 0 <= a/b) by (apply ZO_div_pos; auto with zarith). - assert (H2 : 0 <= a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith). - destruct (Zle_lt_or_eq 0 (a/b) H1) as [H3|H3]; [ | rewrite <- H3; auto]. - pattern a at 2; rewrite (ZO_div_mod_eq a b). - apply Zlt_le_trans with (2*(a/b)). - romega. - apply Zle_trans with (b*(a/b)). - apply Zmult_le_compat_r; auto. - romega. -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. - intros a b H; apply sym_equal; apply ZOdiv_unique with a; auto with zarith. -Qed. - -(** Same situation, in term of modulo: *) - -Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a. -Proof. - intros a b H; apply sym_equal; apply ZOmod_unique with 0; auto with zarith. -Qed. - -(** [Zge] is compatible with a positive division. *) - -Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c. -Proof. - intros. - destruct H0. - destruct (Zle_lt_or_eq 0 c H); - [ clear H | subst c; do 2 rewrite ZOdiv_0_r; auto]. - generalize (ZO_div_mod_eq a c). - generalize (ZOmod_lt_pos_pos a c H0 H2). - generalize (ZO_div_mod_eq b c). - generalize (ZOmod_lt_pos_pos b c (Zle_trans _ _ _ H0 H1) H2). - intros. - elim (Z_le_gt_dec (a / c) (b / c)); auto with zarith. - intro. - absurd (a - b >= 1). - omega. - replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by - (symmetry; pattern a at 1; rewrite H5; pattern b at 1; rewrite H3; ring). - assert (c * (a / c - b / c) >= c * 1). - apply Zmult_ge_compat_l. - omega. - omega. - assert (c * 1 = c). - ring. - omega. -Qed. - -Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c. -Proof. - intros. - destruct (Z_le_gt_dec 0 a). - apply ZO_div_monotone_pos; auto with zarith. - destruct (Z_le_gt_dec 0 b). - apply Zle_trans with 0. - apply Zle_left_rev. - simpl. - rewrite <- ZOdiv_opp_l. - apply ZO_div_pos; auto with zarith. - apply ZO_div_pos; auto with zarith. - rewrite <-(Zopp_involutive a), (ZOdiv_opp_l (-a)). - rewrite <-(Zopp_involutive b), (ZOdiv_opp_l (-b)). - generalize (ZO_div_monotone_pos (-b) (-a) c H). - romega. -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 a b Ha. - destruct b as [ |b|b]. - simpl; auto with zarith. - split. - apply Zmult_le_0_compat; auto with zarith. - apply ZO_div_pos; auto with zarith. - generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *. - change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp. - split. - apply Zmult_le_0_compat; auto with zarith. - apply ZO_div_pos; auto with zarith. - generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *. -Qed. - -Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0. -Proof. - intros a b Ha. - destruct b as [ |b|b]. - simpl; auto with zarith. - split. - generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *. - apply Zle_left_rev; unfold Zplus. - rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l. - apply Zmult_le_0_compat; auto with zarith. - apply ZO_div_pos; auto with zarith. - change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp. - split. - generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *. - apply Zle_left_rev; unfold Zplus. - rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l. - apply Zmult_le_0_compat; auto with zarith. - apply ZO_div_pos; 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_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0. -Proof. - intros; generalize (ZO_div_mod_eq a b); romega. -Qed. - -Lemma ZO_div_exact_full_2 : forall a b:Z, a mod b = 0 -> a = b*(a/b). -Proof. - intros; generalize (ZO_div_mod_eq a b); romega. -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 a b H1 H2. - destruct (Zle_lt_or_eq _ _ H2). - case (Zle_or_lt b a); intros H3. - case (ZOmod_lt_pos_pos a b); auto with zarith. - rewrite ZOmod_small; auto with zarith. - subst; rewrite ZOmod_0_r; 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. - rewrite <- (ZO_div_mult q b); auto with zarith. - apply ZO_div_monotone; auto with zarith. -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 H1 H2 H3. - apply Zmult_lt_reg_r with b; auto with zarith. - apply Zle_lt_trans with (2 := H3). - pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith. - rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith. -Qed. - -Theorem ZOdiv_le_lower_bound: - forall a b q, 0 < b -> q*b <= a -> q <= a/b. -Proof. - intros. - rewrite <- (ZO_div_mult q b); auto with zarith. - apply ZO_div_monotone; auto with zarith. -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; destruct (Z_eq_dec a 0) as [Ha|Ha]. - subst; simpl; rewrite ZOmod_0_l; apply ZO_mod_mult. - intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. - subst; do 2 rewrite ZOmod_0_r; romega. - symmetry; apply ZOmod_unique_full with (a/c+b); auto with zarith. - rewrite Remainder_equiv; split. - apply ZOmod_lt; auto. - apply Zmult_le_0_reg_r with (a*a); eauto. - destruct a; simpl; auto with zarith. - replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring. - apply Zmult_le_0_compat; auto. - apply ZOmod_sgn2. - rewrite Zmult_plus_distr_r, Zmult_comm. - generalize (ZO_div_mod_eq a c); romega. -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; destruct (Z_eq_dec a 0) as [Ha|Ha]. - subst; simpl; apply ZO_div_mult; auto. - symmetry. - apply ZOdiv_unique_full with (a mod c); auto with zarith. - rewrite Remainder_equiv; split. - apply ZOmod_lt; auto. - apply Zmult_le_0_reg_r with (a*a); eauto. - destruct a; simpl; auto with zarith. - replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring. - apply Zmult_le_0_compat; auto. - apply ZOmod_sgn2. - rewrite Zmult_plus_distr_r, Zmult_comm. - generalize (ZO_div_mod_eq a c); romega. -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 a b c; rewrite Zplus_comm; intros; rewrite ZO_div_plus; - try apply Zplus_comm; 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 a b c Hc. - destruct (Z_eq_dec b 0). - subst; simpl; do 2 rewrite ZOdiv_0_r; auto. - symmetry. - apply ZOdiv_unique_full with ((a mod b)*c); auto with zarith. - rewrite Remainder_equiv. - split. - do 2 rewrite Zabs_Zmult. - apply Zmult_lt_compat_r. - romega with *. - apply ZOmod_lt; auto. - replace ((a mod b)*c*(a*c)) with (((a mod b)*a)*(c*c)) by ring. - apply Zmult_le_0_compat. - apply ZOmod_sgn2. - destruct c; simpl; auto with zarith. - pattern a at 1; rewrite (ZO_div_mod_eq a b); ring. -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 a); rewrite (Zmult_comm c b). - apply ZOdiv_mult_cancel_r; auto. -Qed. - -Lemma ZOmult_mod_distr_l: forall a b c, - (c*a) mod (c*b) = c * (a mod b). -Proof. - intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. - subst; simpl; rewrite ZOmod_0_r; auto. - destruct (Z_eq_dec b 0) as [Hb|Hb]. - subst; repeat rewrite Zmult_0_r || rewrite ZOmod_0_r; auto. - assert (c*b <> 0). - contradict Hc; eapply Zmult_integral_l; eauto. - rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq (c*a) (c*b))). - rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq a b)). - rewrite ZOdiv_mult_cancel_l; auto with zarith. - ring. -Qed. - -Lemma ZOmult_mod_distr_r: forall a b c, - (a*c) mod (b*c) = (a mod b) * c. -Proof. - intros; repeat rewrite (fun x => (Zmult_comm x c)). - apply ZOmult_mod_distr_l; auto. -Qed. - -(** Operations modulo. *) - -Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n. -Proof. - intros. - generalize (ZOmod_sgn2 a n). - pattern a at 2 4; rewrite (ZO_div_mod_eq a n); auto with zarith. - rewrite Zplus_comm; rewrite (Zmult_comm n). - intros. - apply sym_equal; apply ZO_mod_plus; auto with zarith. - rewrite Zmult_comm; auto. -Qed. - -Theorem ZOmult_mod: forall a b n, - (a * b) mod n = ((a mod n) * (b mod n)) mod n. -Proof. - intros. - generalize (Zmult_le_0_compat _ _ (ZOmod_sgn2 a n) (ZOmod_sgn2 b n)). - pattern a at 2 3; rewrite (ZO_div_mod_eq a n); auto with zarith. - pattern b at 2 3; rewrite (ZO_div_mod_eq b n); auto with zarith. - set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n). - replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B)) - by ring. - replace ((n*A' + A) * (n*B' + B)) - with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring. - intros. - apply ZO_mod_plus; auto with zarith. -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. - assert (forall a b n, 0<a -> 0<b -> - (a + b) mod n = (a mod n + b mod n) mod n). - intros a b n Ha Hb. - assert (H : 0<=a+b) by (romega with * ); revert H. - pattern a at 1 2; rewrite (ZO_div_mod_eq a n); auto with zarith. - pattern b at 1 2; rewrite (ZO_div_mod_eq b n); auto with zarith. - replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n)) - with ((a mod n + b mod n) + (a / n + b / n) * n) by ring. - intros. - apply ZO_mod_plus; auto with zarith. - apply Zmult_le_0_compat; auto with zarith. - apply Zplus_le_0_compat. - apply Zmult_le_reg_r with a; auto with zarith. - simpl; apply ZOmod_sgn2; auto. - apply Zmult_le_reg_r with b; auto with zarith. - simpl; apply ZOmod_sgn2; auto. - (* general situation *) - intros a b n Hab. - destruct (Z_eq_dec a 0). - subst; simpl; symmetry; apply ZOmod_mod. - destruct (Z_eq_dec b 0). - subst; simpl; do 2 rewrite Zplus_0_r; symmetry; apply ZOmod_mod. - assert (0<a /\ 0<b \/ a<0 /\ b<0). - destruct a; destruct b; simpl in *; intuition; romega with *. - destruct H0. - apply H; intuition. - rewrite <-(Zopp_involutive a), <-(Zopp_involutive b). - rewrite <- Zopp_plus_distr; rewrite ZOmod_opp_l. - rewrite (ZOmod_opp_l (-a)),(ZOmod_opp_l (-b)). - match goal with |- _ = (-?x+-?y) mod n => - rewrite <-(Zopp_plus_distr x y), ZOmod_opp_l end. - f_equal; apply H; auto with zarith. -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. - rewrite ZOplus_mod. - rewrite ZOmod_mod. - symmetry. - apply ZOplus_mod; auto. - destruct (Z_eq_dec a 0). - subst; rewrite ZOmod_0_l; auto. - destruct (Z_eq_dec b 0). - subst; rewrite Zmult_0_r; auto with zarith. - apply Zmult_le_reg_r with (a*b). - assert (a*b <> 0). - intro Hab. - rewrite (Zmult_integral_l _ _ n1 Hab) in n0; auto with zarith. - auto with zarith. - simpl. - replace (a mod n * b * (a*b)) with ((a mod n * a)*(b*b)) by ring. - apply Zmult_le_0_compat. - apply ZOmod_sgn2. - destruct b; simpl; auto with zarith. -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. - rewrite Zplus_comm, (Zplus_comm b a). - apply ZOplus_mod_idemp_l; auto. -Qed. - -Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n. -Proof. - intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto. -Qed. - -Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n. -Proof. - intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; 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. - (* particular case: a, b, c positive *) - assert (forall a b c, a>0 -> b>0 -> c>0 -> (a/b)/c = a/(b*c)). - intros a b c H H0 H1. - pattern a at 2;rewrite (ZO_div_mod_eq a b). - pattern (a/b) at 2;rewrite (ZO_div_mod_eq (a/b) c). - replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with - ((a / b / c)*(b * c) + (b * ((a / b) mod c) + a mod b)) by ring. - assert (b*c<>0). - intro H2; - assert (H3: c <> 0) by auto with zarith; - rewrite (Zmult_integral_l _ _ H3 H2) in H0; auto with zarith. - assert (0<=a/b) by (apply (ZO_div_pos a b); auto with zarith). - assert (0<=a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith). - assert (0<=(a/b) mod c < c) by - (apply ZOmod_lt_pos_pos; auto with zarith). - rewrite ZO_div_plus_l; auto with zarith. - rewrite (ZOdiv_small (b * ((a / b) mod c) + a mod b)). - ring. - split. - apply Zplus_le_0_compat;auto with zarith. - apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)). - apply Zplus_le_compat;auto with zarith. - apply Zle_lt_trans with (b * (c-1) + (b - 1)). - apply Zplus_le_compat;auto with zarith. - replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith. - repeat (apply Zmult_le_0_compat || apply Zplus_le_0_compat); auto with zarith. - apply (ZO_div_pos (a/b) c); auto with zarith. - (* b c positive, a general *) - assert (forall a b c, b>0 -> c>0 -> (a/b)/c = a/(b*c)). - intros; destruct a as [ |a|a]; try reflexivity. - apply H; auto with zarith. - change (Zneg a) with (-Zpos a); repeat rewrite ZOdiv_opp_l. - f_equal; apply H; auto with zarith. - (* c positive, a b general *) - assert (forall a b c, c>0 -> (a/b)/c = a/(b*c)). - intros; destruct b as [ |b|b]. - repeat rewrite ZOdiv_0_r; reflexivity. - apply H0; auto with zarith. - change (Zneg b) with (-Zpos b); - repeat (rewrite ZOdiv_opp_r || rewrite ZOdiv_opp_l || rewrite <- Zopp_mult_distr_l). - f_equal; apply H0; auto with zarith. - (* a b c general *) - intros; destruct c as [ |c|c]. - rewrite Zmult_0_r; repeat rewrite ZOdiv_0_r; reflexivity. - apply H1; auto with zarith. - change (Zneg c) with (-Zpos c); - rewrite <- Zopp_mult_distr_r; do 2 rewrite ZOdiv_opp_r. - f_equal; apply H1; auto with zarith. -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 a b c Ha Hb Hc. - destruct (Zle_lt_or_eq _ _ Ha); - [ | subst; rewrite ZOdiv_0_l, Zmult_0_r, ZOdiv_0_l; auto]. - destruct (Zle_lt_or_eq _ _ Hb); - [ | subst; rewrite ZOdiv_0_r, ZOdiv_0_r, Zmult_0_r; auto]. - destruct (Zle_lt_or_eq _ _ Hc); - [ | subst; rewrite ZOdiv_0_l; auto]. - case (ZOmod_lt_pos_pos a b); auto with zarith; intros Hu1 Hu2. - case (ZOmod_lt_pos_pos c b); auto with zarith; intros Hv1 Hv2. - apply Zmult_le_reg_r with b; auto with zarith. - rewrite <- Zmult_assoc. - replace (a / b * b) with (a - a mod b). - replace (c * a / b * b) with (c * a - (c * a) mod b). - rewrite Zmult_minus_distr_l. - unfold Zminus; apply Zplus_le_compat_l. - match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end. - apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith. - rewrite ZOmult_mod; auto with zarith. - apply (ZOmod_le ((c mod b) * (a mod b)) b); auto with zarith. - apply Zmult_le_compat_r; auto with zarith. - apply (ZOmod_le c b); auto. - pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring; - auto with zarith. - pattern a at 1; rewrite (ZO_div_mod_eq a b); try ring; 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. - split; intros. - exists (a/b). - pattern a at 1; rewrite (ZO_div_mod_eq a b). - rewrite H; auto with zarith. - destruct H as [c Hc]. - destruct (Z_eq_dec b 0). - subst b; simpl in *; subst a; auto. - symmetry. - apply ZOmod_unique_full with c; auto with zarith. - red; romega with *. -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. |