From b1bdefa45c0fa9786a8f916981a67ac5a4961eb0 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 13:06:56 -0400 Subject: Move some lemmas to appropriate places --- src/Arithmetic.v | 68 +++++++------------------------------------------ src/Util/ZUtil/Divide.v | 7 +++++ src/Util/ZUtil/Pow.v | 24 +++++++++++++++++ 3 files changed, 40 insertions(+), 59 deletions(-) (limited to 'src') diff --git a/src/Arithmetic.v b/src/Arithmetic.v index 75e93deaf..7a9babf1a 100644 --- a/src/Arithmetic.v +++ b/src/Arithmetic.v @@ -3656,6 +3656,13 @@ Module UniformWeight. push_Zmod. autorewrite with zsimplify. reflexivity. } { f_equal; lia. } Qed. + + Lemma mod_mod_uweight lgr (Hr : 0 < lgr) a i j : + (i <= j)%nat -> (a mod (uweight lgr j)) mod (uweight lgr i) = a mod (uweight lgr i). + Proof. + intros. rewrite <-Znumtheory.Zmod_div_mod; auto using uwprops; [ ]. + rewrite !uweight_eq_alt'. apply Divide.Z.divide_pow_le. nia. + Qed. End UniformWeight. Module WordByWordMontgomery. @@ -5088,23 +5095,6 @@ Module BarrettReduction. Section Proofs. - (* TODO: move *) - Lemma divides_pow_le b n m : 0 <= n <= m -> (b ^ n | b ^ m). - Proof. - intros. replace m with (n + (m - n)) by ring. - rewrite Z.pow_add_r by lia. - apply Z.divide_factor_l. - Qed. - - (* TODO: move to UW or Weight *) - Lemma mod_mod_weight a i j : - (i <= j)%nat -> (a mod (w j)) mod (w i) = a mod (w i). - Proof. - intros. rewrite <-Znumtheory.Zmod_div_mod; auto; [ ]. - rewrite !UniformWeight.uweight_eq_alt'. - apply divides_pow_le. nia. - Qed. - Lemma shiftr'_correct m n : forall t tn, (m <= tn)%nat -> 0 <= t < w tn -> 0 <= n < width -> @@ -5135,7 +5125,7 @@ Module BarrettReduction. rewrite <-Znumtheory.Zmod_div_mod by (try solve [Z.zero_bounds]; rewrite <-!Z.pow_add_r by auto with zarith; - auto using Z.mul_divide_mono_r, divides_pow_le with zarith). + auto using Z.mul_divide_mono_r, Divide.Z.divide_pow_le with zarith). rewrite Z.div_div_comm by auto with zarith. repeat (f_equal; try ring). } Qed. @@ -5258,35 +5248,6 @@ Module BarrettReduction. end. Qed. - (* TODO: move *) - Lemma pow_pos_le a b : 0 < a -> 0 < b -> a <= a ^ b. - Proof. - intros; transitivity (a ^ 1). - { rewrite Z.pow_1_r; reflexivity. } - { apply Z.pow_le_mono; auto with zarith. } - Qed. - Hint Resolve pow_pos_le : zarith. - - (* TODO: move *) - Lemma pow_pos_lt a b : 1 < a -> 1 < b -> a < a ^ b. - Proof. - intros; eapply Z.le_lt_trans with (m:=a ^ 1). - { rewrite Z.pow_1_r; reflexivity. } - { apply Z.pow_lt_mono_r; auto with zarith. } - Qed. - Hint Resolve pow_pos_lt : zarith. - - (* TODO: move *) - Lemma pow_div_base a b : a <> 0 -> 0 < b -> a ^ b / a = a ^ (b - 1). - Proof. intros; rewrite Z.pow_sub_r, Z.pow_1_r; lia. Qed. - Hint Rewrite pow_div_base using zutil_arith : pull_Zpow. - - (* TODO: move *) - Lemma pow_mul_base a b : 0 <= b -> a * a ^ b = a ^ (b + 1). - Proof. intros; rewrite <-Z.pow_succ_r, <-Z.add_1_r by lia; reflexivity. Qed. - Hint Rewrite pow_mul_base using zutil_arith : pull_Zpow. - - (* improved! *) Ltac zero_bounds' := repeat match goal with @@ -5406,7 +5367,6 @@ Module BarrettReduction. Qed. Hint Rewrite cond_subM_correct : pull_partition. - (* TODO: unused?*) Lemma w_eq_22k : w (sz * 2) = 2 ^ (2 * k). Proof. replace (sz * 2)%nat with (sz + sz)%nat by lia. @@ -5414,16 +5374,6 @@ Module BarrettReduction. f_equal; lia. Qed. - (* TODO: unused?*) - Lemma q3M_eq x q3 (b:bool) : - 0 <= x < M * 2 ^ k -> - q3 = x / M + (if b then -1 else 0) -> - q3 * M = x - x mod M - (if b then M else 0). - Proof. - intros. assert (0 < 2^(k-1)) by Z.zero_bounds. rewrite Z.mod_eq by lia. - subst q3. break_innermost_match; ring. - Qed. - (* TODO: move *) Hint Resolve Z.positive_is_nonzero Z.lt_gt : zarith. @@ -5538,7 +5488,7 @@ Module BarrettReduction. rewrite <-Z.mod_pull_div by Z.zero_bounds. autorewrite with zsimplify. reflexivity. } cbv [fancy_reduce' reduce q1 q3 shiftr r cond_subM]. - autorewrite with natsimplify. (* TODO: maybe need to get rid of hd 0? *) + autorewrite with natsimplify. cbv [shiftr' seq]. autorewrite with push_map push_nth_default. subst fancy_reduce; reflexivity. Qed. diff --git a/src/Util/ZUtil/Divide.v b/src/Util/ZUtil/Divide.v index 8609db5ad..b49530194 100644 --- a/src/Util/ZUtil/Divide.v +++ b/src/Util/ZUtil/Divide.v @@ -33,4 +33,11 @@ Module Z. apply Zmod_divide; omega || auto. } Qed. + + Lemma divide_pow_le b n m : 0 <= n <= m -> (b ^ n | b ^ m). + Proof. + intros. replace m with (n + (m - n)) by ring. + rewrite Z.pow_add_r by lia. + apply Z.divide_factor_l. + Qed. End Z. diff --git a/src/Util/ZUtil/Pow.v b/src/Util/ZUtil/Pow.v index 06ce2187b..f07709614 100644 --- a/src/Util/ZUtil/Pow.v +++ b/src/Util/ZUtil/Pow.v @@ -41,4 +41,28 @@ Module Z. Lemma two_p_two_eq_four : 2^(2) = 4. Proof. reflexivity. Qed. Hint Rewrite <- two_p_two_eq_four : push_Zpow. + + Lemma pow_pos_le a b : 0 < a -> 0 < b -> a <= a ^ b. + Proof. + intros; transitivity (a ^ 1). + { rewrite Z.pow_1_r; reflexivity. } + { apply Z.pow_le_mono; auto with zarith. } + Qed. + Hint Resolve pow_pos_le : zarith. + + Lemma pow_pos_lt a b : 1 < a -> 1 < b -> a < a ^ b. + Proof. + intros; eapply Z.le_lt_trans with (m:=a ^ 1). + { rewrite Z.pow_1_r; reflexivity. } + { apply Z.pow_lt_mono_r; auto with zarith. } + Qed. + Hint Resolve pow_pos_lt : zarith. + + Lemma pow_div_base a b : a <> 0 -> 0 < b -> a ^ b / a = a ^ (b - 1). + Proof. intros; rewrite Z.pow_sub_r, Z.pow_1_r; lia. Qed. + Hint Rewrite pow_div_base using zutil_arith : pull_Zpow. + + Lemma pow_mul_base a b : 0 <= b -> a * a ^ b = a ^ (b + 1). + Proof. intros; rewrite <-Z.pow_succ_r, <-Z.add_1_r by lia; reflexivity. Qed. + Hint Rewrite pow_mul_base using zutil_arith : pull_Zpow. End Z. -- cgit v1.2.3