diff options
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParamProofs.v')
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 3a530c377..85ed920a2 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -17,29 +17,31 @@ Section PseudoMersenneBaseParamProofs. Local Notation base := (base_from_limb_widths limb_widths). Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. - Proof. auto using Z.lt_le_incl, limb_widths_pos. Qed. + Proof using Type. auto using Z.lt_le_incl, limb_widths_pos. Qed. Lemma k_nonneg : 0 <= k. - Proof. apply sum_firstn_limb_widths_nonneg, limb_widths_nonneg. Qed. + Proof using Type. apply sum_firstn_limb_widths_nonneg, limb_widths_nonneg. Qed. Lemma lt_modulus_2k : modulus < 2 ^ k. - Proof. + Proof using Type. replace (2 ^ k) with (modulus + c) by (unfold c; ring). pose proof c_pos; omega. Qed. Hint Resolve lt_modulus_2k. Lemma modulus_pos : 0 < modulus. - Proof. + Proof using Type*. pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega. Qed. Hint Resolve modulus_pos. Lemma modulus_nonzero : Z.pos modulus <> 0. + Proof using Type*. + pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega. Qed. (* a = r + s(2^k) = r + s(2^k - c + c) = r + s(2^k - c) + cs = r + cs *) Lemma pseudomersenne_add: forall x y, (x + ((2^k) * y)) mod modulus = (x + (c * y)) mod modulus. - Proof. + Proof using Type. intros. replace (2^k) with ((2^k - c) + c) by ring. rewrite Z.mul_add_distr_r, Zplus_mod. @@ -50,7 +52,7 @@ Section PseudoMersenneBaseParamProofs. Qed. Lemma pseudomersenne_add': forall x y0 y1 z, (z - x + ((2^k) * y0 * y1)) mod modulus = (c * y0 * y1 - x + z) mod modulus. - Proof. + Proof using Type. intros; rewrite <- !Z.add_opp_r, <- !Z.mul_assoc, pseudomersenne_add; apply f_equal2; omega. Qed. @@ -58,7 +60,7 @@ Section PseudoMersenneBaseParamProofs. decode (ext_base limb_widths) us = decode base (firstn (length base) us) + (2 ^ k * decode base (skipn (length base) us)). - Proof. + Proof using Type. intros. unfold decode; rewrite <- mul_each_rep. rewrite ext_base_alt by apply limb_widths_nonneg. @@ -75,7 +77,7 @@ Section PseudoMersenneBaseParamProofs. Lemma nth_default_base_positive : forall i, (i < length base)%nat -> nth_default 0 base i > 0. - Proof. + Proof using Type. intros. pose proof (nth_error_length_exists_value _ _ H). destruct H0. @@ -88,7 +90,7 @@ Section PseudoMersenneBaseParamProofs. Lemma base_succ_div_mult : forall i, ((S i) < length base)%nat -> nth_default 0 base (S i) = nth_default 0 base i * (nth_default 0 base (S i) / nth_default 0 base i). - Proof. + Proof using Type. intros. apply Z_div_exact_2; try (apply nth_default_base_positive; omega). apply base_succ; distr_length; eauto using limb_widths_nonneg. |