diff options
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/BarrettReduction/Z.v | 14 | ||||
| -rw-r--r-- | src/ModularArithmetic/BarrettReduction/ZBounded.v | 2 | ||||
| -rw-r--r-- | src/ModularArithmetic/BarrettReduction/ZGeneralized.v | 12 | ||||
| -rw-r--r-- | src/ModularArithmetic/BarrettReduction/ZHandbook.v | 20 | ||||
| -rw-r--r-- | src/ModularArithmetic/Conversion.v | 18 | ||||
| -rw-r--r-- | src/ModularArithmetic/ExtPow2BaseMulProofs.v | 2 | ||||
| -rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 22 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 82 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 2 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 68 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 12 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 134 | ||||
| -rw-r--r-- | src/ModularArithmetic/Montgomery/ZBounded.v | 6 | ||||
| -rw-r--r-- | src/ModularArithmetic/Montgomery/ZProofs.v | 64 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 198 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 36 | ||||
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 20 |
17 files changed, 360 insertions, 352 deletions
diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/ModularArithmetic/BarrettReduction/Z.v index 39f99c149..1f3fe0cdd 100644 --- a/src/ModularArithmetic/BarrettReduction/Z.v +++ b/src/ModularArithmetic/BarrettReduction/Z.v @@ -32,7 +32,7 @@ Section barrett. Theorem naive_barrett_reduction_correct : a mod n = a - ⌊am⌋ * n. - Proof. + Proof using n_reasonable. apply Zmod_eq_full; assumption. Qed. End general_idea. @@ -58,7 +58,7 @@ Section barrett. (a_nonneg : 0 <= a). Lemma k_nonnegative : 0 <= k. - Proof. + Proof using Type*. destruct (Z_lt_le_dec k 0); try assumption. rewrite !Z.pow_neg_r in * by lia; lia. Qed. @@ -70,7 +70,7 @@ Section barrett. truncated division), [q] is an integer and [r ≡ a mod n]. *) Theorem barrett_reduction_equivalent : r mod n = a mod n. - Proof. + Proof using m_good. subst r q m. rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption. reflexivity. @@ -78,7 +78,7 @@ Section barrett. Lemma qn_small : q * n <= a. - Proof. + Proof using a_nonneg k_good m_good n_pos n_reasonable. pose proof k_nonnegative; subst q r m. assert (0 <= 2^(k-1)) by zero_bounds. Z.simplify_fractions_le. @@ -88,7 +88,7 @@ Section barrett. (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *) Context (a_small : a < 4^k). Lemma q_nice : { b : bool | q = a / n + if b then -1 else 0 }. - Proof. + Proof using a_nonneg a_small k_good m_good n_pos n_reasonable. assert (0 <= (4 ^ k * a / n) mod 4 ^ k < 4 ^ k) by auto with zarith lia. assert (0 <= a * (4 ^ k mod n) / n < 4 ^ k) by (auto with zero_bounds zarith lia). subst q r m. @@ -99,7 +99,7 @@ Section barrett. Qed. Lemma r_small : r < 2 * n. - Proof. + Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q. Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. assert (a mod n < n) by auto with zarith lia. subst r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m. @@ -112,7 +112,7 @@ Section barrett. : a mod n = if r <? n then r else r - n. - Proof. + Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q. pose proof r_small. pose proof qn_small. destruct (r <? n) eqn:rlt; Z.ltb_to_lt. { symmetry; apply (Zmod_unique a n q); subst r; lia. } diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v index 60cd3df72..a6d968650 100644 --- a/src/ModularArithmetic/BarrettReduction/ZBounded.v +++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v @@ -53,7 +53,7 @@ Section barrett. : medium_valid x -> decode_small (barrett_reduce_function x) = (decode_large x) mod m /\ small_valid (barrett_reduce_function x). - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg μ'_eq μ'_good μ_good. exact (proj2_sig (barrett_reduce x)). Qed. End barrett. diff --git a/src/ModularArithmetic/BarrettReduction/ZGeneralized.v b/src/ModularArithmetic/BarrettReduction/ZGeneralized.v index aad0cf112..99543a45e 100644 --- a/src/ModularArithmetic/BarrettReduction/ZGeneralized.v +++ b/src/ModularArithmetic/BarrettReduction/ZGeneralized.v @@ -39,7 +39,7 @@ Section barrett. Theorem naive_barrett_reduction_correct : a mod n = a - ⌊am⌋ * n. - Proof. + Proof using n_reasonable. apply Zmod_eq_full; assumption. Qed. End general_idea. @@ -84,7 +84,7 @@ Section barrett. truncated division), [q] is an integer and [r ≡ a mod n]. *) Theorem barrett_reduction_equivalent : r mod n = a mod n. - Proof. + Proof using m_good offset. subst r q m. rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption. reflexivity. @@ -92,7 +92,7 @@ Section barrett. Lemma qn_small : q * n <= a. - Proof. + Proof using a_nonneg a_small base_good k_big_enough m_good n_pos n_reasonable offset_nonneg. subst q r m. assert (0 < b^(k-offset)). zero_bounds. assert (0 < b^(k+offset)) by zero_bounds. @@ -102,7 +102,7 @@ Section barrett. Qed. Lemma q_nice : { b : bool * bool | q = a / n + (if fst b then -1 else 0) + (if snd b then -1 else 0) }. - Proof. + Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg. assert (0 < b^(k+offset)) by zero_bounds. assert (0 < b^(k-offset)) by zero_bounds. assert (a / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia. @@ -116,7 +116,7 @@ Section barrett. Qed. Lemma r_small : r < 3 * n. - Proof. + Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg q. Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. assert (a mod n < n) by auto with zarith lia. subst r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m. @@ -129,7 +129,7 @@ Section barrett. : a mod n = let r := if r <? n then r else r-n in let r := if r <? n then r else r-n in r. - Proof. + Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg q. pose proof r_small. pose proof qn_small. cbv zeta. destruct (r <? n) eqn:Hr, (r-n <? n) eqn:?; try rewrite Hr; Z.ltb_to_lt; try lia. { symmetry; apply (Zmod_unique a n q); subst r; lia. } diff --git a/src/ModularArithmetic/BarrettReduction/ZHandbook.v b/src/ModularArithmetic/BarrettReduction/ZHandbook.v index b0d6480d8..8962a997f 100644 --- a/src/ModularArithmetic/BarrettReduction/ZHandbook.v +++ b/src/ModularArithmetic/BarrettReduction/ZHandbook.v @@ -54,7 +54,7 @@ Section barrett. if r <? 0 then r + b^(k+offset) else r. Lemma r_mod_3m_eq_orig : r_mod_3m = r_mod_3m_orig. - Proof. + Proof using base_pos k_big_enough m_pos m_small offset_nonneg r1 r2. assert (0 <= r1 < b^(k+offset)) by (subst r1; auto with zarith). assert (0 <= r2 < b^(k+offset)) by (subst r2; auto with zarith). subst r_mod_3m r_mod_3m_orig; cbv zeta. @@ -71,7 +71,7 @@ Section barrett. Let Q := x / m. Let R := x mod m. Lemma q3_nice : { b : bool * bool | q3 = Q + (if fst b then -1 else 0) + (if snd b then -1 else 0) }. - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg x_nonneg x_small μ_good. assert (0 < b^(k+offset)) by zero_bounds. assert (0 < b^(k-offset)) by zero_bounds. assert (x / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia. @@ -85,7 +85,7 @@ Section barrett. Qed. Fact q3_in_range : Q - 2 <= q3 <= Q. - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg q2 x_nonneg x_small μ_good. rewrite (proj2_sig q3_nice). break_match; lia. Qed. @@ -98,7 +98,7 @@ Section barrett. Fact 14.43 guarantees that [q₃] is never larger than the true quotient [Q], and is at most 2 smaller. *) Lemma x_minus_q3_m_in_range : 0 <= x - q3 * m < 3 * m. - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg q2 x_nonneg x_small μ_good. pose proof q3_in_range. assert (0 <= R < m) by (subst R; auto with zarith). assert (0 <= (Q - q3) * m + R < 3 * m) by nia. @@ -106,7 +106,7 @@ Section barrett. Qed. Lemma r_mod_3m_eq_alt : r_mod_3m = x - q3 * m. - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg q2 x_nonneg x_small μ_good. pose proof x_minus_q3_m_in_range. subst r_mod_3m r_mod_3m_orig r1 r2. autorewrite with pull_Zmod zsimplify; reflexivity. @@ -115,7 +115,7 @@ Section barrett. (** This version uses reduction modulo [b^(k+offset)]. *) Theorem barrett_reduction_equivalent : r_mod_3m mod m = x mod m. - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r1 r2 x_nonneg x_small μ_good. rewrite r_mod_3m_eq_alt. autorewrite with zsimplify push_Zmod; reflexivity. Qed. @@ -124,10 +124,10 @@ Section barrett. conditional addition of [b^(k+offset)]. *) Theorem barrett_reduction_orig_equivalent : r_mod_3m_orig mod m = x mod m. - Proof. rewrite <- r_mod_3m_eq_orig; apply barrett_reduction_equivalent. Qed. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r_mod_3m x_nonneg x_small μ_good. rewrite <- r_mod_3m_eq_orig; apply barrett_reduction_equivalent. Qed. Lemma r_small : 0 <= r_mod_3m < 3 * m. - Proof. + Proof using Q R base_pos k_big_enough m_large m_pos m_small offset_nonneg q3 x_nonneg x_small μ_good. pose proof x_minus_q3_m_in_range. subst Q R r_mod_3m r_mod_3m_orig r1 r2. autorewrite with pull_Zmod zsimplify; lia. @@ -139,7 +139,7 @@ Section barrett. : x mod m = let r := if r <? m then r else r-m in let r := if r <? m then r else r-m in r. - Proof. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r1 r2 x_nonneg x_small μ_good. pose proof r_small. cbv zeta. destruct (r <? m) eqn:Hr, (r-m <? m) eqn:?; subst r; rewrite !r_mod_3m_eq_alt, ?Hr in *; Z.ltb_to_lt; try lia. { symmetry; eapply (Zmod_unique x m q3); lia. } @@ -153,6 +153,6 @@ Section barrett. : x mod m = let r := if r <? m then r else r-m in let r := if r <? m then r else r-m in r. - Proof. subst r; rewrite <- r_mod_3m_eq_orig; apply barrett_reduction_small. Qed. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r_mod_3m x_nonneg x_small μ_good. subst r; rewrite <- r_mod_3m_eq_orig; apply barrett_reduction_small. Qed. End barrett_modular_reduction. End barrett. diff --git a/src/ModularArithmetic/Conversion.v b/src/ModularArithmetic/Conversion.v index 0fb07e26b..3e8436f43 100644 --- a/src/ModularArithmetic/Conversion.v +++ b/src/ModularArithmetic/Conversion.v @@ -103,7 +103,7 @@ Section Conversion. let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in 0 < dist -> bounded limb_widthsB (update_nth digitB (update_by_concat_bits indexB bitsA) out). - Proof. + Proof using limb_widthsB_nonneg. repeat match goal with | |- _ => progress intros | |- _ => progress autorewrite with Ztestbit @@ -134,7 +134,7 @@ Section Conversion. 0 < dist -> Z.of_nat i < bitsIn limb_widthsA -> Z.of_nat i + dist <= bitsIn limb_widthsA. - Proof. + Proof using limb_widthsA_nonneg. pose proof (rem_bits_in_digit_le_rem_bits limb_widthsA). pose proof (rem_bits_in_digit_le_rem_bits limb_widthsA). repeat match goal with @@ -167,7 +167,7 @@ Section Conversion. Z.of_nat i < bitsIn limb_widthsA -> convert'_invariant inp (i + Z.to_nat dist)%nat (update_nth digitB (update_by_concat_bits indexB bitsA) out). - Proof. + Proof using Type*. Time repeat match goal with | |- _ => progress intros; cbv [convert'_invariant] in * @@ -229,7 +229,7 @@ Section Conversion. bounded limb_widthsA inp -> convert'_invariant inp i out -> convert'_invariant inp (Z.to_nat (bitsIn limb_widthsA)) (convert' inp i out). - Proof. + Proof using Type. intros until 2; functional induction (convert' inp i out); repeat match goal with | |- _ => progress intros @@ -253,7 +253,7 @@ Section Conversion. Lemma convert_correct : forall us, length us = length limb_widthsA -> bounded limb_widthsA us -> decodeA us = decodeB (convert us). - Proof. + Proof using Type. repeat match goal with | |- _ => progress intros | |- _ => progress cbv [convert convert'_invariant] in * @@ -283,7 +283,7 @@ Section Conversion. Lemma convert'_bounded : forall inp i out, bounded limb_widthsB out -> bounded limb_widthsB (convert' inp i out). - Proof. + Proof using Type. intros; functional induction (convert' inp i out); auto. apply IHl. apply convert'_bounded_step; auto. @@ -295,7 +295,7 @@ Section Conversion. Qed. Lemma convert_bounded : forall us, bounded limb_widthsB (convert us). - Proof. + Proof using Type. intros; apply convert'_bounded. apply bounded_iff; intros. rewrite nth_default_zeros. @@ -305,12 +305,12 @@ Section Conversion. (* This is part of convert'_invariant, but proving it separately strips preconditions *) Lemma length_convert' : forall inp i out, length (convert' inp i out) = length out. - Proof. + Proof using Type. intros; functional induction (convert' inp i out); distr_length. Qed. Lemma length_convert : forall us, length (convert us) = length limb_widthsB. - Proof. + Proof using Type. cbv [convert]; intros. rewrite length_convert', length_zeros. reflexivity. diff --git a/src/ModularArithmetic/ExtPow2BaseMulProofs.v b/src/ModularArithmetic/ExtPow2BaseMulProofs.v index af2c1a679..38e9cf634 100644 --- a/src/ModularArithmetic/ExtPow2BaseMulProofs.v +++ b/src/ModularArithmetic/ExtPow2BaseMulProofs.v @@ -27,7 +27,7 @@ Section ext_mul. (length us <= length base)%nat -> (length vs <= length base)%nat -> (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs). - Proof. + Proof using Type*. intros; apply mul_rep_two_base; auto; distr_length. Qed. diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index b9d6ffe4c..2236461ce 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -41,7 +41,7 @@ Section ExtendedBaseVector. Definition ext_limb_widths := limb_widths ++ limb_widths. Definition ext_base := base_from_limb_widths ext_limb_widths. Lemma ext_base_alt : ext_base = base ++ (map (Z.mul (2^k)) base). - Proof. + Proof using Type*. unfold ext_base, ext_limb_widths. rewrite base_from_limb_widths_app by auto. rewrite two_p_equiv. @@ -49,13 +49,13 @@ Section ExtendedBaseVector. Qed. Lemma ext_base_positive : forall b, In b ext_base -> b > 0. - Proof. + Proof using Type*. apply base_positive; unfold ext_limb_widths. intros ? H. apply in_app_or in H; destruct H; auto. Qed. Lemma b0_1 : forall x, nth_default x base 0 = 1 -> nth_default x ext_base 0 = 1. - Proof. + Proof using Type*. intros. rewrite ext_base_alt, nth_default_app. destruct base; assumption. Qed. @@ -63,7 +63,7 @@ Section ExtendedBaseVector. Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> nth_default 0 (map (Z.mul (2 ^ k)) base) n = (2 ^ k) * (nth_default 0 base n). - Proof. + Proof using Type. intros. erewrite map_nth_default; auto. Qed. @@ -71,14 +71,14 @@ Section ExtendedBaseVector. Lemma ext_limb_widths_nonneg (limb_widths_nonneg : forall w : Z, In w limb_widths -> 0 <= w) : forall w : Z, In w ext_limb_widths -> 0 <= w. - Proof. + Proof using Type*. unfold ext_limb_widths; setoid_rewrite in_app_iff. intros ? [?|?]; auto. Qed. Lemma ext_limb_widths_upper_bound : upper_bound ext_limb_widths = upper_bound limb_widths * upper_bound limb_widths. - Proof. + Proof using Type*. unfold ext_limb_widths. autorewrite with push_upper_bound; reflexivity. Qed. @@ -105,7 +105,7 @@ Section ExtendedBaseVector. (2 ^ k * (nth_default 0 base i * nth_default 0 base j')) / (2 ^ k * nth_default 0 base (i + j')) * (2 ^ k * nth_default 0 base (i + j')). - Proof. + Proof using base_good two_k_nonzero. clear limb_widths_match_modulus. intros. remember (nth_default 0 base) as b. @@ -124,7 +124,7 @@ Section ExtendedBaseVector. let b := nth_default 0 ext_base in let r := (b i * b j) / b (i+j)%nat in b i * b j = r * b (i+j)%nat. - Proof. + Proof using Type*. intros. subst b. subst r. rewrite ext_base_alt in *. @@ -160,7 +160,7 @@ Section ExtendedBaseVector. Lemma extended_base_length: length ext_base = (length base + length base)%nat. - Proof. + Proof using Type. clear limb_widths_nonnegative. unfold ext_base, ext_limb_widths; autorewrite with distr_length; reflexivity. Qed. @@ -168,7 +168,7 @@ Section ExtendedBaseVector. Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), (length us <= length base)%nat -> firstn (length us) base = firstn (length us) ext_base. - Proof. + Proof using Type*. rewrite ext_base_alt; intros. rewrite firstn_app_inleft; auto; omega. Qed. @@ -176,7 +176,7 @@ Section ExtendedBaseVector. Lemma decode_short : forall (us : BaseSystem.digits), (length us <= length base)%nat -> BaseSystem.decode base us = BaseSystem.decode ext_base us. - Proof. auto using decode_short_initial, firstn_us_base_ext_base. Qed. + Proof using Type*. auto using decode_short_initial, firstn_us_base_ext_base. Qed. Section BaseVector. Context {bv : BaseSystem.BaseVector base} diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 863300dde..9cd211943 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -43,39 +43,39 @@ Module F. Local Open Scope F_scope. Theorem eq_to_Z_iff (x y : F m) : x = y <-> F.to_Z x = F.to_Z y. - Proof. destruct x, y; intuition; simpl in *; try apply (eqsig_eq _ _); congruence. Qed. + Proof using Type. destruct x, y; intuition; simpl in *; try apply (eqsig_eq _ _); congruence. Qed. Lemma eq_of_Z_iff : forall x y : Z, x mod m = y mod m <-> F.of_Z m x = F.of_Z m y. - Proof. split; unwrap_F; congruence. Qed. + Proof using Type. split; unwrap_F; congruence. Qed. Lemma to_Z_of_Z : forall z, F.to_Z (F.of_Z m z) = z mod m. - Proof. unwrap_F; trivial. Qed. + Proof using Type. unwrap_F; trivial. Qed. Lemma of_Z_to_Z x : F.of_Z m (F.to_Z x) = x :> F m. - Proof. unwrap_F; congruence. Qed. + Proof using Type. unwrap_F; congruence. Qed. Lemma of_Z_mod : forall x, F.of_Z m x = F.of_Z m (x mod m). - Proof. unwrap_F; trivial. Qed. + Proof using Type. unwrap_F; trivial. Qed. Lemma mod_to_Z : forall (x:F m), F.to_Z x mod m = F.to_Z x. - Proof. unwrap_F. congruence. Qed. + Proof using Type. unwrap_F. congruence. Qed. Lemma to_Z_0 : F.to_Z (0:F m) = 0%Z. - Proof. unwrap_F. apply Zmod_0_l. Qed. + Proof using Type. unwrap_F. apply Zmod_0_l. Qed. Lemma of_Z_small_nonzero z : (0 < z < m)%Z -> F.of_Z m z <> 0. - Proof. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed. + Proof using Type. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed. Lemma to_Z_nonzero (x:F m) : x <> 0 -> F.to_Z x <> 0%Z. - Proof. intros Hnz Hz. rewrite <- Hz, of_Z_to_Z in Hnz; auto. Qed. + Proof using Type. intros Hnz Hz. rewrite <- Hz, of_Z_to_Z in Hnz; auto. Qed. Lemma to_Z_range (x : F m) : 0 < m -> 0 <= F.to_Z x < m. - Proof. intros. rewrite <- mod_to_Z. apply Z.mod_pos_bound. trivial. Qed. + Proof using Type. intros. rewrite <- mod_to_Z. apply Z.mod_pos_bound. trivial. Qed. Lemma to_Z_nonzero_range (x : F m) : (x <> 0) -> 0 < m -> (1 <= F.to_Z x < m)%Z. - Proof. + Proof using Type. unfold not; intros Hnz Hlt. rewrite eq_to_Z_iff, to_Z_0 in Hnz; pose proof (to_Z_range x Hlt). omega. @@ -83,27 +83,27 @@ Module F. Lemma of_Z_add : forall (x y : Z), F.of_Z m (x + y) = F.of_Z m x + F.of_Z m y. - Proof. unwrap_F; trivial. Qed. + Proof using Type. unwrap_F; trivial. Qed. Lemma to_Z_add : forall x y : F m, F.to_Z (x + y) = ((F.to_Z x + F.to_Z y) mod m)%Z. - Proof. unwrap_F; trivial. Qed. + Proof using Type. unwrap_F; trivial. Qed. Lemma of_Z_mul x y : F.of_Z m (x * y) = F.of_Z _ x * F.of_Z _ y :> F m. - Proof. unwrap_F. trivial. Qed. + Proof using Type. unwrap_F. trivial. Qed. Lemma to_Z_mul : forall x y : F m, F.to_Z (x * y) = ((F.to_Z x * F.to_Z y) mod m)%Z. - Proof. unwrap_F; trivial. Qed. + Proof using Type. unwrap_F; trivial. Qed. Lemma of_Z_sub x y : F.of_Z _ (x - y) = F.of_Z _ x - F.of_Z _ y :> F m. - Proof. unwrap_F. trivial. Qed. + Proof using Type. unwrap_F. trivial. Qed. Lemma to_Z_opp : forall x : F m, F.to_Z (F.opp x) = (- F.to_Z x) mod m. - Proof. unwrap_F; trivial. Qed. + Proof using Type. unwrap_F; trivial. Qed. Lemma of_Z_pow x n : F.of_Z _ x ^ n = F.of_Z _ (x ^ (Z.of_N n) mod m) :> F m. - Proof. + Proof using Type. intros. induction n using N.peano_ind; destruct (pow_spec (F.of_Z m x)) as [pow_0 pow_succ] . { @@ -121,7 +121,7 @@ Module F. Lemma to_Z_pow : forall (x : F m) n, F.to_Z (x ^ n)%F = (F.to_Z x ^ Z.of_N n mod m)%Z. - Proof. + Proof using Type. intros. symmetry. induction n using N.peano_ind; @@ -140,7 +140,7 @@ Module F. Lemma square_iff (x:F m) : (exists y : F m, y * y = x) <-> (exists y : Z, y * y mod m = F.to_Z x)%Z. - Proof. + Proof using Type. setoid_rewrite eq_to_Z_iff; setoid_rewrite to_Z_mul; split; intro H; destruct H as [x' H]. - eauto. - exists (F.of_Z _ x'); rewrite !to_Z_of_Z; pull_Zmod; auto. @@ -155,7 +155,7 @@ Module F. Context {m:BinPos.positive}. Lemma to_nat_of_nat (n:nat) : F.to_nat (F.of_nat m n) = (n mod (Z.to_nat m))%nat. - Proof. + Proof using Type. unfold F.to_nat, F.of_nat. rewrite F.to_Z_of_Z. assert (Pos.to_nat m <> 0)%nat as HA by (pose proof Pos2Nat.is_pos m; omega). @@ -166,6 +166,8 @@ Module F. Qed. Lemma of_nat_to_nat x : F.of_nat m (F.to_nat x) = x. + Proof using Type. + unfold F.to_nat, F.of_nat. rewrite Z2Nat.id; [ eapply F.of_Z_to_Z | eapply F.to_Z_range; reflexivity]. Qed. @@ -174,7 +176,7 @@ Module F. Admitted. Lemma of_nat_mod (n:nat) : F.of_nat m (n mod (Z.to_nat m)) = F.of_nat m n. - Proof. + Proof using Type. unfold F.of_nat. rewrite (F.of_Z_mod (Z.of_nat n)), ?mod_Zmod, ?Z2Nat.id; [reflexivity|..]. { apply Pos2Z.is_nonneg. } @@ -182,6 +184,8 @@ Module F. Qed. Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x. + Proof using Type. + unfold F.to_nat. rewrite <-F.mod_to_Z at 2. apply Z.mod_to_nat; [assumption|]. @@ -190,11 +194,11 @@ Module F. Lemma of_nat_add x y : F.of_nat m (x + y) = (F.of_nat m x + F.of_nat m y)%F. - Proof. unfold F.of_nat; rewrite Nat2Z.inj_add, F.of_Z_add; reflexivity. Qed. + Proof using Type. unfold F.of_nat; rewrite Nat2Z.inj_add, F.of_Z_add; reflexivity. Qed. Lemma of_nat_mul x y : F.of_nat m (x * y) = (F.of_nat m x * F.of_nat m y)%F. - Proof. unfold F.of_nat; rewrite Nat2Z.inj_mul, F.of_Z_mul; reflexivity. Qed. + Proof using Type. unfold F.of_nat; rewrite Nat2Z.inj_mul, F.of_Z_mul; reflexivity. Qed. End FandNat. Section RingTacticGadgets. @@ -204,7 +208,7 @@ Module F. := Algebra.Ring.ring_theory_for_stdlib_tactic. Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F F.mul x n. - Proof. + Proof using Type. destruct (pow_spec x) as [HO HS]; intros. destruct n; auto; unfold id. rewrite Pre.N_pos_1plus at 1. @@ -218,13 +222,13 @@ Module F. Qed. Lemma power_theory : power_theory 1%F (@F.mul m) eq id (@F.pow m). - Proof. split; apply pow_pow_N. Qed. + Proof using Type. split; apply pow_pow_N. Qed. (***** Division Theory *****) Definition quotrem(a b: F m): F m * F m := let '(q, r) := (Z.quotrem (F.to_Z a) (F.to_Z b)) in (F.of_Z _ q , F.of_Z _ r). Lemma div_theory : div_theory eq (@F.add m) (@F.mul m) (@id _) quotrem. - Proof. + Proof using Type. constructor; intros; unfold quotrem, id. replace (Z.quotrem (F.to_Z a) (F.to_Z b)) with (Z.quot (F.to_Z a) (F.to_Z b), Z.rem (F.to_Z a) (F.to_Z b)) by @@ -241,12 +245,12 @@ Module F. * to inject the result afterward. *) Lemma ring_morph: ring_morph 0%F 1%F F.add F.mul F.sub F.opp eq 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb (F.of_Z m). - Proof. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed. + Proof using Type. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed. (* Redefine our division theory under the ring morphism *) Lemma morph_div_theory: Ring_theory.div_theory eq Zplus Zmult (F.of_Z m) Z.quotrem. - Proof. + Proof using Type. split; intros. replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). @@ -269,10 +273,10 @@ Module F. power_tac (power_theory m) [is_pow_constant]). Lemma mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0. - Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. + Proof using Type. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. Lemma mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0. - Proof. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. + Proof using Type. intros a b Hnz Hz. rewrite Hz in Hnz; apply Hnz; ring. Qed. End VariousModulo. Section Pow. @@ -287,7 +291,7 @@ Module F. Import Algebra.ScalarMult. Global Instance pow_is_scalarmult : is_scalarmult (G:=F m) (eq:=eq) (add:=F.mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)). - Proof. + Proof using Type. split; intros; rewrite ?Nat2N.inj_succ, <-?N.add_1_l; match goal with | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto] @@ -320,24 +324,24 @@ Module F. end). Lemma pow_0_r (x:F m) : x^0 = 1. - Proof. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed. + Proof using Type. pow_to_scalarmult_ref. apply scalarmult_0_l. Qed. Lemma pow_add_r (x:F m) (a b:N) : x^(a+b) = x^a * x^b. - Proof. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed. + Proof using Type. pow_to_scalarmult_ref; apply scalarmult_add_l. Qed. Lemma pow_0_l (n:N) : n <> 0%N -> 0^n = 0 :> F m. - Proof. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed. + Proof using Type. pow_to_scalarmult_ref; destruct n; simpl; intros; [congruence|ring]. Qed. Lemma pow_pow_l (x:F m) (a b:N) : (x^a)^b = x^(a*b). - Proof. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed. + Proof using Type. pow_to_scalarmult_ref. apply scalarmult_assoc. Qed. Lemma pow_1_r (x:F m) : x^1 = x. - Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. Lemma pow_2_r (x:F m) : x^2 = x*x. - Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. Lemma pow_3_r (x:F m) : x^3 = x*x*x. - Proof. pow_to_scalarmult_ref; simpl; ring. Qed. + Proof using Type. pow_to_scalarmult_ref; simpl; ring. Qed. End Pow. End F. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 9d7ce7c1f..0e09386f5 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -102,7 +102,7 @@ Section ModularBaseSystem. Import Morphisms. Global Instance eq_Equivalence : Equivalence eq. - Proof. + Proof using Type. split; cbv [eq]; repeat intro; congruence. Qed. diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 83db33dfe..8d749dfdd 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -26,7 +26,7 @@ Section LengthProofs. Local Notation base := (base_from_limb_widths limb_widths). Lemma length_encode {x} : length (encode x) = length limb_widths. - Proof. + Proof using Type. cbv [encode encodeZ]; intros. rewrite encode'_spec; auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length. @@ -35,7 +35,7 @@ Section LengthProofs. Lemma length_reduce : forall us, (length limb_widths <= length us <= length (ext_base limb_widths))%nat -> (length (reduce us) = length limb_widths)%nat. - Proof. + Proof using Type. rewrite extended_base_length. unfold reduce; intros. rewrite add_length_exact. @@ -48,7 +48,7 @@ Section LengthProofs. length u = length limb_widths -> length v = length limb_widths -> length (mul u v) = length limb_widths. - Proof. + Proof using Type. cbv [mul]; intros. apply length_reduce. destruct u; try congruence. @@ -75,7 +75,7 @@ Section LengthProofs. length u = length limb_widths -> length v = length limb_widths -> length (sub mm u v) = length limb_widths. - Proof. + Proof using Type*. cbv [sub]; intros. rewrite sub_length, add_length_exact. repeat rewrite Max.max_r; omega. @@ -83,19 +83,19 @@ Section LengthProofs. End Sub. Lemma length_carry_and_reduce {us}: forall i, length (carry_and_reduce i us) = length us. - Proof. intros; unfold carry_and_reduce; autorewrite with distr_length; reflexivity. Qed. + Proof using Type. intros; unfold carry_and_reduce; autorewrite with distr_length; reflexivity. Qed. Hint Rewrite @length_carry_and_reduce : distr_length. Lemma length_carry {u i} : length u = length limb_widths -> length (carry i u) = length limb_widths. - Proof. intros; unfold carry; break_if; autorewrite with distr_length; omega. Qed. + Proof using Type. intros; unfold carry; break_if; autorewrite with distr_length; omega. Qed. Hint Rewrite @length_carry : distr_length. Lemma length_carry_sequence {u i} : length u = length limb_widths -> length (carry_sequence i u) = length limb_widths. - Proof. + Proof using Type. induction i; intros; unfold carry_sequence; simpl; autorewrite with distr_length; auto. Qed. Hint Rewrite @length_carry_sequence : distr_length. @@ -103,11 +103,11 @@ Section LengthProofs. Lemma length_carry_full {u} : length u = length limb_widths -> length (carry_full u) = length limb_widths. - Proof. intros; unfold carry_full; autorewrite with distr_length; congruence. Qed. + Proof using Type. intros; unfold carry_full; autorewrite with distr_length; congruence. Qed. Hint Rewrite @length_carry_full : distr_length. Lemma length_modulus_digits : length modulus_digits = length limb_widths. - Proof. + Proof using Type. intros; unfold modulus_digits, encodeZ. rewrite encode'_spec, encode'_length; auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length. @@ -117,7 +117,7 @@ Section LengthProofs. Lemma length_conditional_subtract_modulus {int_width u cond} : length u = length limb_widths -> length (conditional_subtract_modulus int_width u cond) = length limb_widths. - Proof. + Proof using Type. intros; unfold conditional_subtract_modulus. rewrite map2_length, map_length, length_modulus_digits. apply Min.min_case; omega. @@ -127,7 +127,7 @@ Section LengthProofs. Lemma length_freeze {int_width u} : length u = length limb_widths -> length (freeze int_width u) = length limb_widths. - Proof. + Proof using Type. intros; unfold freeze; repeat autorewrite with distr_length; congruence. Qed. @@ -135,7 +135,7 @@ Section LengthProofs. {target_widths_nonneg : forall x, In x target_widths -> 0 <= x} {pf us}, length (pack target_widths_nonneg pf us) = length target_widths. - Proof. + Proof using Type. cbv [pack]; intros. apply length_convert. Qed. @@ -144,7 +144,7 @@ Section LengthProofs. {target_widths_nonneg : forall x, In x target_widths -> 0 <= x} {pf us}, length (unpack target_widths_nonneg pf us) = length limb_widths. - Proof. + Proof using Type. cbv [pack]; intros. apply length_convert. Qed. @@ -159,7 +159,7 @@ Section ModulusDigitsProofs. Local Hint Resolve limb_widths_nonneg. Lemma decode_modulus_digits : decode' base modulus_digits = modulus. - Proof. + Proof using Type. cbv [modulus_digits]. pose proof c_pos. pose proof modulus_pos. rewrite encodeZ_spec by eauto using limb_widths_nonnil, limb_widths_good. @@ -170,14 +170,14 @@ Section ModulusDigitsProofs. Qed. Lemma bounded_modulus_digits : bounded limb_widths modulus_digits. - Proof. + Proof using Type. apply bounded_encodeZ; auto using limb_widths_nonneg. pose proof modulus_pos; omega. Qed. Lemma modulus_digits_ones : forall i, (0 < i < length limb_widths)%nat -> nth_default 0 modulus_digits i = Z.ones (nth_default 0 limb_widths i). - Proof. + Proof using Type*. repeat match goal with | |- _ => progress (cbv [BaseSystem.decode]; intros) | |- _ => progress autorewrite with Ztestbit @@ -212,7 +212,7 @@ Section ModulusDigitsProofs. Lemma bounded_le_modulus_digits : forall us i, length us = length limb_widths -> bounded limb_widths us -> (0 < i < length limb_widths)%nat -> nth_default 0 us i <= nth_default 0 modulus_digits i. - Proof. + Proof using Type*. intros until 0; rewrite bounded_iff; intros. rewrite modulus_digits_ones by omega. specialize (H0 i). @@ -247,7 +247,7 @@ Section ModulusComparisonProofs. length vs = length limb_widths -> bounded limb_widths vs -> (Z.compare (decode' base (firstn i us)) (decode' base (firstn i vs)) = compare' us vs i). - Proof. + Proof using Type. induction i; repeat match goal with | |- _ => progress intros @@ -275,7 +275,7 @@ Section ModulusComparisonProofs. length vs = length limb_widths -> bounded limb_widths vs -> (Z.compare (decode' base us) (decode' base vs) = compare' us vs (length limb_widths)). - Proof. + Proof using Type. intros. rewrite <-decode_firstn_compare' by (auto || omega). rewrite !firstn_all by auto. @@ -284,14 +284,14 @@ Section ModulusComparisonProofs. Lemma ge_modulus'_0 : forall {A} f us i, ge_modulus' (A := A) f us 0 i = f 0. - Proof. + Proof using Type. induction i; intros; simpl; cbv [cmovne cmovl]; break_if; auto. Qed. Lemma ge_modulus'_01 : forall {A} f us i b, (b = 0 \/ b = 1) -> (ge_modulus' (A := A) f us b i = f 0 \/ ge_modulus' (A := A) f us b i = f 1). - Proof. + Proof using Type. induction i; intros; try intuition (subst; cbv [ge_modulus' LetIn.Let_In cmovl cmovne]; break_if; tauto). simpl; cbv [LetIn.Let_In cmovl cmovne]. @@ -300,7 +300,7 @@ Section ModulusComparisonProofs. Lemma ge_modulus_01 : forall us, (ge_modulus us = 0 \/ ge_modulus us = 1). - Proof. + Proof using Type. cbv [ge_modulus]; intros; apply ge_modulus'_01; tauto. Qed. @@ -309,7 +309,7 @@ Section ModulusComparisonProofs. forall i, (i < length us)%nat -> ge_modulus' id us 1 i = 1 -> forall j, (j <= i)%nat -> nth_default 0 modulus_digits j <= nth_default 0 us j. - Proof. + Proof using Type. induction i; repeat match goal with | |- _ => progress intros; simpl in * @@ -328,7 +328,7 @@ Section ModulusComparisonProofs. Lemma ge_modulus'_compare' : forall us, length us = length limb_widths -> bounded limb_widths us -> forall i, (i < length limb_widths)%nat -> (ge_modulus' id us 1 i = 0 <-> compare' us modulus_digits (S i) = Lt). - Proof. + Proof using Type*. induction i; repeat match goal with | |- _ => progress (intros; cbv [LetIn.Let_In id cmovne cmovl]) @@ -360,7 +360,7 @@ Section ModulusComparisonProofs. Lemma ge_modulus_spec : forall u, length u = length limb_widths -> bounded limb_widths u -> (ge_modulus u = 0 <-> 0 <= BaseSystem.decode base u < modulus). - Proof. + Proof using Type*. cbv [ge_modulus]; intros. assert (0 < length limb_widths)%nat by (pose proof limb_widths_nonnil; destruct limb_widths; @@ -391,14 +391,14 @@ Section ConditionalSubtractModulusProofs. Lemma map2_sub_eq : forall us vs, length us = length vs -> map2 (fun x y => x - y) us vs = BaseSystem.sub us vs. - Proof. + Proof using lt_1_length_limb_widths. induction us; destruct vs; boring; try omega. Qed. (* TODO : ListUtil *) Lemma map_id_strong : forall {A} f (xs : list A), (forall x, In x xs -> f x = x) -> map f xs = xs. - Proof. + Proof using Type. induction xs; intros; auto. simpl; f_equal; auto using in_eq, in_cons. Qed. @@ -406,7 +406,7 @@ Section ConditionalSubtractModulusProofs. Lemma bounded_digit_fits : forall us, length us = length limb_widths -> bounded limb_widths us -> forall x, In x us -> 0 <= x < 2 ^ B. - Proof. + Proof using B_compat c_upper_bound lt_1_length_limb_widths. intros. let i := fresh "i" in match goal with H : In ?x ?us, Hb : bounded _ _ |- _ => @@ -421,7 +421,7 @@ Section ConditionalSubtractModulusProofs. Lemma map_land_max_ones : forall us, length us = length limb_widths -> bounded limb_widths us -> map (Z.land (Z.ones B)) us = us. - Proof. + Proof using Type*. repeat match goal with | |- _ => progress intros | |- _ => apply map_id_strong @@ -433,7 +433,7 @@ Section ConditionalSubtractModulusProofs. Qed. Lemma map_land_zero : forall us, map (Z.land 0) us = zeros (length us). - Proof. + Proof using Type. induction us; boring. Qed. @@ -443,7 +443,7 @@ Section ConditionalSubtractModulusProofs. length u = length limb_widths -> BaseSystem.decode base (conditional_subtract_modulus B u cond) = BaseSystem.decode base u - cond * modulus. - Proof. + Proof using Type*. repeat match goal with | |- _ => progress (cbv [conditional_subtract_modulus neg]; intros) | |- _ => destruct cond_01; subst @@ -463,7 +463,7 @@ Section ConditionalSubtractModulusProofs. length u = length limb_widths -> bounded limb_widths u -> bounded limb_widths (conditional_subtract_modulus B u (ge_modulus u)). - Proof. + Proof using Type*. repeat match goal with | |- _ => progress (cbv [conditional_subtract_modulus neg]; intros) | |- _ => unique pose proof bounded_modulus_digits @@ -491,7 +491,7 @@ Section ConditionalSubtractModulusProofs. Lemma bounded_mul2_modulus : forall u, length u = length limb_widths -> bounded limb_widths u -> ge_modulus u = 1 -> modulus <= BaseSystem.decode base u < 2 * modulus. - Proof. + Proof using c_upper_bound lt_1_length_limb_widths. intros. pose proof (@decode_upper_bound _ limb_widths_nonneg u). specialize_by auto. @@ -525,7 +525,7 @@ Section ConditionalSubtractModulusProofs. length u = length limb_widths -> bounded limb_widths u -> ge_modulus (conditional_subtract_modulus B u (ge_modulus u)) = 0. - Proof. + Proof using Type*. intros. rewrite ge_modulus_spec by auto using length_conditional_subtract_modulus, conditional_subtract_modulus_preserves_bounded. pose proof (ge_modulus_01 u) as Hgm01. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 121e605a3..0a240568b 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -596,7 +596,7 @@ Section Multiplication. Definition mul_bi'_opt_correct (i : nat) (vsr : list Z) (bs : list Z) : mul_bi'_opt i vsr bs = mul_bi' bs i vsr. - Proof. + Proof using Type. revert i; induction vsr as [|vsr vsrs IHvsr]; intros. { reflexivity. } { simpl mul_bi'. @@ -621,7 +621,7 @@ Section Multiplication. Lemma map_zeros : forall a n l, List.map (Z.mul a) (zeros n ++ l) = zeros n ++ List.map (Z.mul a) l. - Proof. + Proof using prm. induction n; simpl; [ reflexivity | intros; apply f_equal2; [ omega | congruence ] ]. Qed. @@ -660,7 +660,7 @@ Section Multiplication. Definition mul'_opt_correct (usr vs : list Z) (bs : list Z) : mul'_opt usr vs bs = mul' bs usr vs. - Proof. + Proof using prm. revert vs; induction usr as [|usr usrs IHusr]; intros. { reflexivity. } { simpl. @@ -769,7 +769,7 @@ Section PowInv. Lemma fold_chain_opt_correct : forall {T} (id : T) op chain acc, fold_chain_opt id op chain acc = fold_chain id op chain acc. - Proof. + Proof using Type. reflexivity. Qed. @@ -940,7 +940,7 @@ Section Canonicalization. Lemma ge_modulus'_cps : forall {A} (f : Z -> A) (us : list Z) i b, f (ge_modulus' id us b i) = ge_modulus' f us b i. - Proof. + Proof using Type. induction i; intros; simpl; cbv [Let_In cmovl cmovne]; break_if; try reflexivity; apply IHi. Qed. @@ -1029,7 +1029,7 @@ Section SquareRoots. Lemma if_equiv : forall {A} (eqA : A -> A -> Prop) (x0 x1 : bool) y0 y1 z0 z1, x0 = x1 -> eqA y0 y1 -> eqA z0 z1 -> eqA (if x0 then y0 else z0) (if x1 then y1 else z1). - Proof. + Proof using Type. intros; repeat break_if; congruence. Qed. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 57ae4e10d..9b22187bd 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -61,25 +61,25 @@ Section FieldOperationProofs. Local Hint Unfold rep decode ModularBaseSystemList.decode. Lemma rep_decode : forall us x, us ~= x -> decode us = x. - Proof. + Proof using Type. autounfold; intuition. Qed. Lemma decode_rep : forall us, rep us (decode us). - Proof. + Proof using Type. cbv [rep]; auto. Qed. Lemma encode_eq : forall x : F modulus, ModularBaseSystemList.encode x = BaseSystem.encode base (F.to_Z x) (2 ^ k). - Proof. + Proof using Type. cbv [ModularBaseSystemList.encode BaseSystem.encode encodeZ]; intros. rewrite base_from_limb_widths_length. apply encode'_spec; auto using Nat.eq_le_incl. Qed. Lemma encode_rep : forall x : F modulus, encode x ~= x. - Proof. + Proof using Type. autounfold; cbv [encode]; intros. rewrite to_list_from_list; autounfold. rewrite encode_eq, encode_rep. @@ -94,7 +94,7 @@ Section FieldOperationProofs. Qed. Lemma bounded_encode : forall x, bounded limb_widths (to_list (encode x)). - Proof. + Proof using Type. intros. cbv [encode]; rewrite to_list_from_list. cbv [ModularBaseSystemList.encode]. @@ -118,7 +118,7 @@ Section FieldOperationProofs. Lemma add_rep : forall u v x y, u ~= x -> v ~= y -> add u v ~= (x+y)%F. - Proof. + Proof using Type. autounfold; cbv [add]; intros. rewrite to_list_from_list; autounfold. rewrite add_rep, F.of_Z_add. @@ -126,18 +126,18 @@ Section FieldOperationProofs. Qed. Lemma eq_rep_iff : forall u v, (eq u v <-> u ~= decode v). - Proof. + Proof using Type. reflexivity. Qed. Lemma eq_dec : forall x y, Decidable.Decidable (eq x y). - Proof. + Proof using Type. intros. destruct (F.eq_dec (decode x) (decode y)); [ left | right ]; congruence. Qed. Lemma modular_base_system_add_monoid : @monoid digits eq add zero. - Proof. + Proof using Type. repeat match goal with | |- _ => progress intro | |- _ => cbv [zero]; rewrite encode_rep @@ -171,7 +171,7 @@ Section FieldOperationProofs. Qed. Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%F. - Proof. + Proof using Type. autounfold in *; unfold ModularBaseSystem.mul in *. intuition idtac; subst. rewrite to_list_from_list. @@ -185,7 +185,7 @@ Section FieldOperationProofs. Qed. Lemma modular_base_system_mul_monoid : @monoid digits eq mul one. - Proof. + Proof using Type. repeat match goal with | |- _ => progress intro | |- _ => cbv [one]; rewrite encode_rep @@ -207,7 +207,7 @@ Section FieldOperationProofs. Lemma Fdecode_decode_mod : forall us x, decode us = x -> BaseSystem.decode base (to_list us) mod modulus = F.to_Z x. - Proof. + Proof using Type. autounfold; intros. rewrite <-H. apply F.to_Z_of_Z. @@ -227,7 +227,7 @@ Section FieldOperationProofs. Qed. Lemma opp_rep : forall mm pf u x, u ~= x -> opp mm pf u ~= F.opp x. - Proof. + Proof using Type. cbv [opp rep]; intros. rewrite sub_rep by (apply encode_rep || eassumption). apply F.eq_to_Z_iff. @@ -244,7 +244,7 @@ Section FieldOperationProofs. Lemma scalarmult_rep : forall u x n, u ~= x -> (@ScalarMult.scalarmult_ref digits mul one n u) ~= (x ^ (N.of_nat n))%F. - Proof. + Proof using Type. induction n; intros. + cbv [N.to_nat ScalarMult.scalarmult_ref]. rewrite F.pow_0_r. apply encode_rep. @@ -256,7 +256,7 @@ Section FieldOperationProofs. Lemma pow_rep : forall chain u x, u ~= x -> pow u chain ~= F.pow x (fold_chain 0%N N.add chain (1%N :: nil)). - Proof. + Proof using Type. cbv [pow rep]; intros. erewrite (@fold_chain_exp _ _ _ _ modular_base_system_mul_monoid) by (apply @ScalarMult.scalarmult_ref_is_scalarmult; apply modular_base_system_mul_monoid). @@ -267,7 +267,7 @@ Section FieldOperationProofs. Lemma inv_rep : forall chain pf u x, u ~= x -> inv chain pf u ~= F.inv x. - Proof. + Proof using modulus_gt_2. cbv [inv]; intros. rewrite (@F.Fq_inv_fermat _ prime_modulus modulus_gt_2). etransitivity; [ apply pow_rep; eassumption | ]. @@ -280,13 +280,13 @@ Section FieldOperationProofs. Import Morphisms. Global Instance encode_Proper : Proper (Logic.eq ==> eq) encode. - Proof. + Proof using Type. repeat intro; cbv [eq]. rewrite !encode_rep. assumption. Qed. Global Instance add_Proper : Proper (eq ==> eq ==> eq) add. - Proof. + Proof using Type. repeat intro. cbv beta delta [eq] in *. erewrite !add_rep; cbv [rep] in *; try reflexivity; assumption. @@ -294,7 +294,7 @@ Section FieldOperationProofs. Global Instance sub_Proper mm mm_correct : Proper (eq ==> eq ==> eq) (sub mm mm_correct). - Proof. + Proof using Type. repeat intro. cbv beta delta [eq] in *. erewrite !sub_rep; cbv [rep] in *; try reflexivity; assumption. @@ -302,20 +302,20 @@ Section FieldOperationProofs. Global Instance opp_Proper mm mm_correct : Proper (eq ==> eq) (opp mm mm_correct). - Proof. + Proof using Type. cbv [opp]; repeat intro. apply sub_Proper; assumption || reflexivity. Qed. Global Instance mul_Proper : Proper (eq ==> eq ==> eq) mul. - Proof. + Proof using Type. repeat intro. cbv beta delta [eq] in *. erewrite !mul_rep; cbv [rep] in *; try reflexivity; assumption. Qed. Global Instance pow_Proper : Proper (eq ==> Logic.eq ==> eq) pow. - Proof. + Proof using Type. repeat intro. cbv beta delta [eq] in *. erewrite !pow_rep; cbv [rep] in *; subst; try reflexivity. @@ -323,13 +323,13 @@ Section FieldOperationProofs. Qed. Global Instance inv_Proper chain chain_correct : Proper (eq ==> eq) (inv chain chain_correct). - Proof. + Proof using Type. cbv [inv]; repeat intro. apply pow_Proper; assumption || reflexivity. Qed. Global Instance div_Proper : Proper (eq ==> eq ==> eq) div. - Proof. + Proof using Type. cbv [div]; repeat intro; congruence. Qed. @@ -339,7 +339,7 @@ Section FieldOperationProofs. {ec : ExponentiationChain (modulus - 2)}. Lemma _zero_neq_one : not (eq zero one). - Proof. + Proof using Type. cbv [eq zero one]; erewrite !encode_rep. pose proof (@F.field_modulo modulus prime_modulus). apply zero_neq_one. @@ -347,7 +347,7 @@ Section FieldOperationProofs. Lemma modular_base_system_field : @field digits eq zero one (opp coeff coeff_mod) add (sub coeff coeff_mod) mul (inv chain chain_correct) div. - Proof. + Proof using modulus_gt_2. eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := @F.field_modulo modulus prime_modulus)). Grab Existential Variables. + intros; eapply encode_rep. @@ -375,7 +375,7 @@ Section CarryProofs. Local Hint Resolve log_cap_nonneg. Lemma base_length_lt_pred : (pred (length base) < length base)%nat. - Proof. + Proof using Type. pose proof limb_widths_nonnil; rewrite base_from_limb_widths_length. destruct limb_widths; congruence || distr_length. Qed. @@ -386,7 +386,7 @@ Section CarryProofs. Lemma carry_done_bounds : forall us, (length us = length base) -> (carry_done us <-> forall i, 0 <= nth_default 0 us i < 2 ^ log_cap i). - Proof. + Proof using Type. intros ? ?; unfold carry_done; split; [ intros Hcarry_done i | intros Hbounds i i_lt ]. + destruct (lt_dec i (length base)) as [i_lt | i_nlt]. - specialize (Hcarry_done i i_lt). @@ -410,7 +410,7 @@ Section CarryProofs. (length us = length limb_widths) -> BaseSystem.decode base (carry_and_reduce (pred (length limb_widths)) us) mod modulus = BaseSystem.decode base us mod modulus. - Proof. + Proof using Type. cbv [carry_and_reduce]; intros. rewrite carry_gen_decode_eq; auto. distr_length. @@ -443,7 +443,7 @@ Section CarryProofs. (i < length limb_widths)%nat -> forall pf1 pf2, from_list _ us pf1 ~= x -> from_list _ (carry i us) pf2 ~= x. - Proof. + Proof using Type. cbv [carry rep decode]; intros. rewrite to_list_from_list. pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths). @@ -462,7 +462,7 @@ Section CarryProofs. Lemma decode_mod_Fdecode : forall u, length u = length limb_widths -> BaseSystem.decode base u mod modulus= F.to_Z (decode (from_list_default 0 _ u)). - Proof. + Proof using Type. intros. rewrite <-(to_list_from_list _ u) with (pf := H). erewrite Fdecode_decode_mod by reflexivity. @@ -474,7 +474,7 @@ Section CarryProofs. Lemma carry_sequence_rep : forall is us x, (forall i, In i is -> (i < length limb_widths)%nat) -> us ~= x -> forall pf, from_list _ (carry_sequence is (to_list _ us)) pf ~= x. - Proof. + Proof using Type. induction is; intros. + cbv [carry_sequence fold_right]. rewrite from_list_to_list. assumption. + simpl. apply carry_rep with (pf1 := length_carry_sequence (length_to_list us)); @@ -486,7 +486,7 @@ Section CarryProofs. Lemma carry_mul_rep : forall us vs x y, rep us x -> rep vs y -> rep (carry_mul carry_chain us vs) (x * y)%F. - Proof. + Proof using Type. cbv [carry_mul]; intros; apply carry_sequence_rep; auto using carry_chain_valid, mul_rep. Qed. @@ -495,7 +495,7 @@ Section CarryProofs. eq (carry_sub carry_chain coeff coeff_mod a b) (sub coeff coeff_mod a b). - Proof. + Proof using Type. cbv [carry_sub carry_]; intros. eapply carry_sequence_rep; auto using carry_chain_valid. reflexivity. @@ -503,7 +503,7 @@ Section CarryProofs. Lemma carry_add_rep : forall a b, eq (carry_add carry_chain a b) (add a b). - Proof. + Proof using Type. cbv [carry_add carry_]; intros. eapply carry_sequence_rep; auto using carry_chain_valid. reflexivity. @@ -513,7 +513,7 @@ Section CarryProofs. eq (carry_opp carry_chain coeff coeff_mod a) (opp coeff coeff_mod a). - Proof. + Proof using Type. cbv [carry_opp opp]; intros. apply carry_sub_rep. Qed. @@ -556,7 +556,7 @@ Section CanonicalizationProofs. then c * (us [i mod length limb_widths]) >> (limb_widths [i mod length limb_widths]) else 0 else 0. - Proof. + Proof using Type. cbv [carry_and_reduce]; intros. autorewrite with push_nth_default. reflexivity. @@ -582,7 +582,7 @@ Section CanonicalizationProofs. then (us [i]) >> (limb_widths [i]) else 0 else 0. - Proof. + Proof using Type*. intros. cbv [carry]. break_innermost_match_step. @@ -622,7 +622,7 @@ Section CanonicalizationProofs. else 0) else Z.pow2_mod (us {{ pred i }} [n]) (limb_widths [n]) else 0. - Proof. + Proof using Type*. induction i; intros; cbv [carry_sequence]. + cbv [pred make_chain fold_right]. break_match; subst; omega || reflexivity || auto using Z.add_0_r. @@ -641,14 +641,14 @@ Section CanonicalizationProofs. (i < length us)%nat -> nth_default 0 (carry i us) i = Z.pow2_mod (us [i]) (limb_widths [i]). - Proof. + Proof using Type*. intros; pose proof lt_1_length_limb_widths; autorewrite with push_nth_default natsimplify; break_match; omega. Qed. Hint Rewrite @nth_default_carry using (omega || distr_length; omega) : push_nth_default. Lemma pow_limb_widths_gt_1 : forall i, (i < length limb_widths)%nat -> 1 < 2 ^ limb_widths [i]. - Proof. + Proof using Type. intros. apply Z.pow_gt_1; try omega. apply nth_default_preserves_properties_length_dep; intros; try omega. @@ -656,7 +656,7 @@ Section CanonicalizationProofs. Qed. Lemma carry_sequence_nil_l : forall us, carry_sequence nil us = us. - Proof. + Proof using Type. reflexivity. Qed. @@ -719,7 +719,7 @@ Section CanonicalizationProofs. if eq_nat_dec n 0 then 2 * 2 ^ limb_widths [n] else 2 ^ limb_widths [n]. - Proof. + Proof using Type*. induction i; bound_during_loop. Qed. @@ -738,7 +738,7 @@ Section CanonicalizationProofs. length (f us) = length limb_widths -> (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound us n) -> forall n, (n < length limb_widths)%nat -> 0 <= (carry_full (f us)) [n] < bound'' (f us) n. - Proof. + Proof using Type*. pose proof lt_1_length_limb_widths. cbv [carry_full full_carry_chain]; intros ? ? ? ? ? ? ? ? Hloop Hfbound Hflength Hbound n. specialize (Hfbound Hbound). @@ -762,7 +762,7 @@ Section CanonicalizationProofs. -> length (f us) = length limb_widths -> (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound us n) -> forall n, 0 <= (carry_full (f us)) [n] < bound'' (f us) n. - Proof. + Proof using Type*. pose proof lt_1_length_limb_widths. cbv [carry_full full_carry_chain]; intros ? ? ? ? ? ? ? ? Hloop Hfbound Hflength Hbound n. specialize (Hfbound Hbound). @@ -779,7 +779,7 @@ Section CanonicalizationProofs. if eq_nat_dec n 0 then 2 * 2 ^ limb_widths [n] else 2 ^ limb_widths [n]. - Proof. + Proof using Type*. intros ? ?. apply (bound_after_loop_length_preconditions us H id bound_during_first_loop); auto. Qed. @@ -792,7 +792,7 @@ Section CanonicalizationProofs. if eq_nat_dec n 0 then 2 * 2 ^ limb_widths [n] else 2 ^ limb_widths [n]. - Proof. + Proof using Type*. intros. destruct (lt_dec n (length limb_widths)); auto using bound_after_first_loop_pre. @@ -819,7 +819,7 @@ Section CanonicalizationProofs. if eq_nat_dec n 0 then 2 ^ limb_widths [n] + c else 2 ^ limb_widths [n]. - Proof. + Proof using Type*. induction i; bound_during_loop. Qed. @@ -831,7 +831,7 @@ Section CanonicalizationProofs. if eq_nat_dec n 0 then 2 ^ limb_widths [n] + c else 2 ^ limb_widths [n]. - Proof. + Proof using Type*. intros ? ?; apply (bound_after_loop us H carry_full bound_during_second_loop); auto using length_carry_full, bound_after_first_loop. Qed. @@ -858,7 +858,7 @@ Section CanonicalizationProofs. else us[n] + 1 else 2 ^ limb_widths [n]. - Proof. + Proof using Type*. induction i; bound_during_loop. Qed. @@ -867,7 +867,7 @@ Section CanonicalizationProofs. (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> forall n, 0 <= (carry_full (carry_full (carry_full us))) [n] < 2 ^ limb_widths [n]. - Proof. + Proof using Type*. intros ? ?. apply (bound_after_loop us H (fun x => carry_full (carry_full x)) bound_during_third_loop); auto using length_carry_full, bound_after_second_loop. @@ -886,7 +886,7 @@ Section CanonicalizationProofs. Lemma decode_bitwise_eq_iff : forall u v, minimal_rep u -> minimal_rep v -> (fieldwise Logic.eq u v <-> decode_bitwise limb_widths (to_list _ u) = decode_bitwise limb_widths (to_list _ v)). - Proof. + Proof using Type. intros. rewrite !decode_bitwise_spec by (tauto || auto using length_to_list). rewrite fieldwise_to_list_iff. @@ -899,14 +899,14 @@ Section CanonicalizationProofs. Qed. Lemma c_upper_bound : c - 1 < 2 ^ limb_widths[0]. - Proof. + Proof using Type*. pose proof c_reduce2. pose proof c_pos. omega. Qed. Hint Resolve c_upper_bound. Lemma minimal_rep_encode : forall x, minimal_rep (encode x). - Proof. + Proof using Type*. split; intros; auto using bounded_encode. apply ge_modulus_spec; auto using bounded_encode, length_to_list. apply encode_range. @@ -914,7 +914,7 @@ Section CanonicalizationProofs. Lemma encode_minimal_rep : forall u x, rep u x -> minimal_rep u -> fieldwise Logic.eq u (encode x). - Proof. + Proof using Type*. intros. apply decode_bitwise_eq_iff; auto using minimal_rep_encode. rewrite !decode_bitwise_spec by (intuition auto; distr_length; try apply minimal_rep_encode). @@ -928,7 +928,7 @@ Section CanonicalizationProofs. Lemma bounded_canonical : forall u v x y, rep u x -> rep v y -> minimal_rep u -> minimal_rep v -> (x = y <-> fieldwise Logic.eq u v). - Proof. + Proof using Type*. intros. eapply encode_minimal_rep in H1; eauto. eapply encode_minimal_rep in H2; eauto. @@ -944,14 +944,14 @@ Section CanonicalizationProofs. Qed. Lemma int_width_compat : forall x, In x limb_widths -> x < int_width. - Proof. + Proof using Type*. intros. apply B_compat in H. eapply Z.lt_le_trans; eauto using B_le_int_width. Qed. Lemma minimal_rep_freeze : forall u, initial_bounds u -> minimal_rep (freeze int_width u). - Proof. + Proof using Type*. repeat match goal with | |- _ => progress (cbv [freeze ModularBaseSystemList.freeze]) | |- _ => progress intros @@ -968,7 +968,7 @@ Section CanonicalizationProofs. Lemma freeze_decode : forall u, BaseSystem.decode base (to_list _ (freeze int_width u)) mod modulus = BaseSystem.decode base (to_list _ u) mod modulus. - Proof. + Proof using Type*. repeat match goal with | |- _ => progress cbv [freeze ModularBaseSystemList.freeze] | |- _ => progress intros @@ -996,7 +996,7 @@ Section CanonicalizationProofs. Qed. Lemma freeze_rep : forall u x, rep u x -> rep (freeze int_width u) x. - Proof. + Proof using Type*. cbv [rep]; intros. apply F.eq_to_Z_iff. erewrite <-!Fdecode_decode_mod by eauto. @@ -1007,7 +1007,7 @@ Section CanonicalizationProofs. initial_bounds u -> initial_bounds v -> (x = y <-> fieldwise Logic.eq (freeze int_width u) (freeze int_width v)). - Proof. + Proof using Type*. intros; apply bounded_canonical; auto using freeze_rep, minimal_rep_freeze. Qed. @@ -1032,7 +1032,7 @@ Section SquareRootProofs. Lemma eqb_true_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> u ~= x -> v ~= y -> (x = y <-> eqb int_width u v = true). - Proof. + Proof using Type*. cbv [eqb freeze_input_bounds]. intros. rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq). eauto using freeze_canonical. @@ -1041,7 +1041,7 @@ Section SquareRootProofs. Lemma eqb_false_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> u ~= x -> v ~= y -> (x <> y <-> eqb int_width u v = false). - Proof. + Proof using Type*. intros. case_eq (eqb int_width u v). + rewrite <-eqb_true_iff by eassumption; split; intros; @@ -1058,7 +1058,7 @@ Section SquareRootProofs. Lemma sqrt_3mod4_correct : forall u x, u ~= x -> (sqrt_3mod4 chain chain_correct u) ~= F.sqrt_3mod4 x. - Proof. + Proof using Type. repeat match goal with | |- _ => progress (cbv [sqrt_3mod4 F.sqrt_3mod4]; intros) | |- _ => rewrite @F.pow_2_r in * @@ -1079,7 +1079,7 @@ Section SquareRootProofs. ModularBaseSystem.eq powx (pow u chain) -> ModularBaseSystem.eq powx_squared (mul powx powx) -> (sqrt_5mod8 int_width powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. - Proof. + Proof using freeze_pre. cbv [sqrt_5mod8 F.sqrt_5mod8]. intros. repeat match goal with @@ -1120,7 +1120,7 @@ Section ConversionProofs. (BaseSystem.decode target_base (to_list _ (pack target_widths_nonneg bits_eq w)))). - Proof. + Proof using Type. intros; cbv [pack ModularBaseSystemList.pack rep]. rewrite Tuple.to_list_from_list. apply F.eq_to_Z_iff. @@ -1132,7 +1132,7 @@ Section ConversionProofs. bounded target_widths (to_list _ w) -> rep (unpack target_widths_nonneg bits_eq w) (F.of_Z modulus (BaseSystem.decode target_base (to_list _ w))). - Proof. + Proof using Type. intros; cbv [unpack ModularBaseSystemList.unpack rep]. apply F.eq_to_Z_iff. rewrite <-from_list_default_eq with (d := 0). diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v index 2e9f3b3cc..2c5936d30 100644 --- a/src/ModularArithmetic/Montgomery/ZBounded.v +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -90,7 +90,7 @@ Section montgomery. (decode_small (proj1_sig (reduce_via_partial v))) (decode_large v * R') /\ Z.min 0 (small_bound - modulus) <= (decode_small (proj1_sig (reduce_via_partial v))) < modulus. - Proof. + Proof using H Hmod Hmod' Hv. rewrite (proj1 (proj2_sig (reduce_via_partial v) H)). eauto 6 using reduce_via_partial_correct, reduce_via_partial_in_range, decode_small_valid. Qed. @@ -100,7 +100,7 @@ Section montgomery. (decode_small (proj1_sig (reduce_via_partial v))) (decode_large v * R') /\ 0 <= (decode_small (proj1_sig (reduce_via_partial v))) < modulus. - Proof. + Proof using H Hmod Hmod' Hv. pose proof (proj2 (proj2_sig (reduce_via_partial v) H)) as H'. apply decode_small_valid in H'. destruct reduce_via_partial_correct'; split; eauto; omega. @@ -108,7 +108,7 @@ Section montgomery. Theorem reduce_via_partial_correct : decode_small (proj1_sig (reduce_via_partial v)) = (decode_large v * R') mod modulus. - Proof. + Proof using H Hmod Hmod' Hv. rewrite <- (proj1 reduce_via_partial_correct''). rewrite Z.mod_small by apply reduce_via_partial_correct''. reflexivity. diff --git a/src/ModularArithmetic/Montgomery/ZProofs.v b/src/ModularArithmetic/Montgomery/ZProofs.v index 9a7ee1e3d..2d8f6155d 100644 --- a/src/ModularArithmetic/Montgomery/ZProofs.v +++ b/src/ModularArithmetic/Montgomery/ZProofs.v @@ -27,19 +27,19 @@ Section montgomery. (R'_good : R * R' ≡ 1). Lemma R'_good' : R' * R ≡ 1. - Proof. rewrite <- R'_good; apply f_equal2; lia. Qed. + Proof using R'_good. rewrite <- R'_good; apply f_equal2; lia. Qed. Local Notation to_montgomery_naive := (to_montgomery_naive R) (only parsing). Local Notation from_montgomery_naive := (from_montgomery_naive R') (only parsing). Lemma to_from_montgomery_naive x : to_montgomery_naive (from_montgomery_naive x) ≡ x. - Proof. + Proof using R'_good. unfold Z.to_montgomery_naive, Z.from_montgomery_naive. rewrite <- Z.mul_assoc, R'_good'. autorewrite with zsimplify; reflexivity. Qed. Lemma from_to_montgomery_naive x : from_montgomery_naive (to_montgomery_naive x) ≡ x. - Proof. + Proof using R'_good. unfold Z.to_montgomery_naive, Z.from_montgomery_naive. rewrite <- Z.mul_assoc, R'_good. autorewrite with zsimplify; reflexivity. @@ -52,18 +52,18 @@ Section montgomery. Local Infix "*" := (mul_naive R') : montgomery_scope. Lemma add_correct_naive x y : from_montgomery_naive (x + y) = from_montgomery_naive x + from_montgomery_naive y. - Proof. unfold Z.from_montgomery_naive, add; lia. Qed. + Proof using Type. unfold Z.from_montgomery_naive, add; lia. Qed. Lemma add_correct_naive_to x y : to_montgomery_naive (x + y) = (to_montgomery_naive x + to_montgomery_naive y)%montgomery. - Proof. unfold Z.to_montgomery_naive, add; autorewrite with push_Zmul; reflexivity. Qed. + Proof using Type. unfold Z.to_montgomery_naive, add; autorewrite with push_Zmul; reflexivity. Qed. Lemma sub_correct_naive x y : from_montgomery_naive (x - y) = from_montgomery_naive x - from_montgomery_naive y. - Proof. unfold Z.from_montgomery_naive, sub; lia. Qed. + Proof using Type. unfold Z.from_montgomery_naive, sub; lia. Qed. Lemma sub_correct_naive_to x y : to_montgomery_naive (x - y) = (to_montgomery_naive x - to_montgomery_naive y)%montgomery. - Proof. unfold Z.to_montgomery_naive, sub; autorewrite with push_Zmul; reflexivity. Qed. + Proof using Type. unfold Z.to_montgomery_naive, sub; autorewrite with push_Zmul; reflexivity. Qed. Theorem mul_correct_naive x y : from_montgomery_naive (x * y) = from_montgomery_naive x * from_montgomery_naive y. - Proof. unfold Z.from_montgomery_naive, mul_naive; lia. Qed. + Proof using Type. unfold Z.from_montgomery_naive, mul_naive; lia. Qed. Theorem mul_correct_naive_to x y : to_montgomery_naive (x * y) ≡ (to_montgomery_naive x * to_montgomery_naive y)%montgomery. - Proof. + Proof using R'_good. unfold Z.to_montgomery_naive, mul_naive. rewrite <- !Z.mul_assoc, R'_good. autorewrite with zsimplify; apply (f_equal2 Z.modulo); lia. @@ -77,10 +77,10 @@ Section montgomery. (N'_good : N * N' ≡ᵣ -1). Lemma N'_good' : N' * N ≡ᵣ -1. - Proof. rewrite <- N'_good; apply f_equal2; lia. Qed. + Proof using N'_good. rewrite <- N'_good; apply f_equal2; lia. Qed. Lemma N'_good'_alt x : (((x mod R) * (N' mod R)) mod R) * (N mod R) ≡ᵣ x * -1. - Proof. + Proof using N'_good. rewrite <- N'_good', Z.mul_assoc. unfold Z.equiv_modulo; push_Zmod. reflexivity. @@ -96,7 +96,7 @@ Section montgomery. unfold Z.equiv_modulo; push_Zmod; autorewrite with zsimplify; reflexivity. Lemma prereduce_correct : prereduce T ≡ T * R'. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. transitivity ((T + m * N) * R'). { unfold Z.prereduce. autorewrite with zstrip_div; push_Zmod. @@ -107,19 +107,19 @@ Section montgomery. Qed. Lemma reduce_correct : reduce N R N' T ≡ T * R'. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold reduce. break_match; rewrite prereduce_correct; t_fin_correct. Qed. Lemma partial_reduce_correct : partial_reduce N R N' T ≡ T * R'. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold partial_reduce. break_match; rewrite prereduce_correct; t_fin_correct. Qed. Lemma reduce_via_partial_correct : reduce_via_partial N R N' T ≡ T * R'. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold reduce_via_partial. break_match; rewrite partial_reduce_correct; t_fin_correct. Qed. @@ -131,7 +131,7 @@ Section montgomery. : 0 <= N -> 0 <= T <= R * B -> 0 <= prereduce T < B + N. - Proof. unfold Z.prereduce; auto with zarith nia. Qed. + Proof using N_reasonable m_small. unfold Z.prereduce; auto with zarith nia. Qed. End generic. Section N_very_small. @@ -140,7 +140,7 @@ Section montgomery. Lemma prereduce_in_range_very_small : 0 <= T <= (2 * N - 1) * (2 * N - 1) -> 0 <= prereduce T < 2 * N. - Proof. pose proof (prereduce_in_range_gen N); nia. Qed. + Proof using N_reasonable N_very_small m_small. pose proof (prereduce_in_range_gen N); nia. Qed. End N_very_small. Section N_small. @@ -149,12 +149,12 @@ Section montgomery. Lemma prereduce_in_range_small : 0 <= T <= (2 * N - 1) * (N - 1) -> 0 <= prereduce T < 2 * N. - Proof. pose proof (prereduce_in_range_gen N); nia. Qed. + Proof using N_reasonable N_small m_small. pose proof (prereduce_in_range_gen N); nia. Qed. Lemma prereduce_in_range_small_fully_reduced : 0 <= T <= 2 * N -> 0 <= prereduce T <= N. - Proof. pose proof (prereduce_in_range_gen 1); nia. Qed. + Proof using N_reasonable N_small m_small. pose proof (prereduce_in_range_gen 1); nia. Qed. End N_small. Section N_small_enough. @@ -163,12 +163,12 @@ Section montgomery. Lemma prereduce_in_range_small_enough : 0 <= T <= R * R -> 0 <= prereduce T < R + N. - Proof. pose proof (prereduce_in_range_gen R); nia. Qed. + Proof using N_reasonable N_small_enough m_small. pose proof (prereduce_in_range_gen R); nia. Qed. Lemma reduce_in_range_R : 0 <= T <= R * R -> 0 <= reduce N R N' T < R. - Proof. + Proof using N_reasonable N_small_enough m_small. intro H; pose proof (prereduce_in_range_small_enough H). unfold reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia. Qed. @@ -176,7 +176,7 @@ Section montgomery. Lemma partial_reduce_in_range_R : 0 <= T <= R * R -> 0 <= partial_reduce N R N' T < R. - Proof. + Proof using N_reasonable N_small_enough m_small. intro H; pose proof (prereduce_in_range_small_enough H). unfold partial_reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia. Qed. @@ -184,7 +184,7 @@ Section montgomery. Lemma reduce_via_partial_in_range_R : 0 <= T <= R * R -> 0 <= reduce_via_partial N R N' T < R. - Proof. + Proof using N_reasonable N_small_enough m_small. intro H; pose proof (prereduce_in_range_small_enough H). unfold reduce_via_partial, partial_reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia. Qed. @@ -194,12 +194,12 @@ Section montgomery. Lemma prereduce_in_range : 0 <= T <= R * N -> 0 <= prereduce T < 2 * N. - Proof. pose proof (prereduce_in_range_gen N); nia. Qed. + Proof using N_reasonable m_small. pose proof (prereduce_in_range_gen N); nia. Qed. Lemma reduce_in_range : 0 <= T <= R * N -> 0 <= reduce N R N' T < N. - Proof. + Proof using N_reasonable m_small. intro H; pose proof (prereduce_in_range H). unfold reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia. Qed. @@ -207,7 +207,7 @@ Section montgomery. Lemma partial_reduce_in_range : 0 <= T <= R * N -> Z.min 0 (R - N) <= partial_reduce N R N' T < 2 * N. - Proof. + Proof using N_reasonable m_small. intro H; pose proof (prereduce_in_range H). unfold partial_reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; apply Z.min_case_strong; nia. @@ -216,7 +216,7 @@ Section montgomery. Lemma reduce_via_partial_in_range : 0 <= T <= R * N -> Z.min 0 (R - N) <= reduce_via_partial N R N' T < N. - Proof. + Proof using N_reasonable m_small. intro H; pose proof (partial_reduce_in_range H). unfold reduce_via_partial in *; break_match; Z.ltb_to_lt; lia. Qed. @@ -226,7 +226,7 @@ Section montgomery. Context (N_in_range : 0 <= N < R) (T_representable : 0 <= T < R * R). Lemma partial_reduce_alt_eq : partial_reduce_alt N R N' T = partial_reduce N R N' T. - Proof. + Proof using N_in_range N_reasonable T_representable m_small. assert (0 <= T + m * N < 2 * (R * R)) by nia. assert (0 <= T + m * N < R * (R + N)) by nia. assert (0 <= (T + m * N) / R < R + N) by auto with zarith. @@ -252,7 +252,7 @@ Section montgomery. Local Notation to_montgomery := (to_montgomery N R N'). Local Notation from_montgomery := (from_montgomery N R N'). Lemma to_from_montgomery a : to_montgomery (from_montgomery a) ≡ a. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold Z.to_montgomery, Z.from_montgomery. transitivity ((a * 1) * 1); [ | apply f_equal2; lia ]. rewrite <- !R'_good, !reduce_correct. @@ -260,7 +260,7 @@ Section montgomery. apply f_equal2; lia. Qed. Lemma from_to_montgomery a : from_montgomery (to_montgomery a) ≡ a. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold Z.to_montgomery, Z.from_montgomery. rewrite !reduce_correct. transitivity (a * ((R * (R * R' mod N) * R') mod N)). @@ -273,12 +273,12 @@ Section montgomery. Qed. Theorem mul_correct x y : from_montgomery (x * y) ≡ from_montgomery x * from_montgomery y. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold Z.from_montgomery, mul. rewrite !reduce_correct; apply f_equal2; lia. Qed. Theorem mul_correct_to x y : to_montgomery (x * y) ≡ (to_montgomery x * to_montgomery y)%montgomery. - Proof. + Proof using N'_good N'_in_range N_reasonable R'_good. unfold Z.to_montgomery, mul. rewrite !reduce_correct. transitivity (x * y * R * 1 * 1 * 1); diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 914b19c11..7a5bb4255 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -31,7 +31,7 @@ Section Pow2BaseProofs. Local Notation base := (base_from_limb_widths limb_widths). Lemma base_from_limb_widths_length ls : length (base_from_limb_widths ls) = length ls. - Proof. + Proof using Type. clear limb_widths limb_widths_nonneg. induction ls; [ reflexivity | simpl in * ]. autorewrite with distr_length; auto. @@ -40,16 +40,16 @@ Section Pow2BaseProofs. Lemma base_from_limb_widths_cons : forall l0 l, base_from_limb_widths (l0 :: l) = 1 :: map (Z.mul (two_p l0)) (base_from_limb_widths l). - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Hint Rewrite base_from_limb_widths_cons : push_base_from_limb_widths. Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths. Lemma base_from_limb_widths_nil : base_from_limb_widths nil = nil. - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Hint Rewrite base_from_limb_widths_nil : push_base_from_limb_widths. Lemma firstn_base_from_limb_widths : forall n, firstn n (base_from_limb_widths limb_widths) = base_from_limb_widths (firstn n limb_widths). - Proof. + Proof using Type. clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) induction limb_widths as [|l ls IHls]; intros [|n]; try reflexivity. autorewrite with push_base_from_limb_widths push_firstn; boring. @@ -60,23 +60,23 @@ Section Pow2BaseProofs. Hint Rewrite @firstn_base_from_limb_widths : push_firstn. Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. - Proof. + Proof using Type*. unfold sum_firstn; intros. apply fold_right_invariant; try omega. eauto using Z.add_nonneg_nonneg, limb_widths_nonneg, In_firstn. Qed. Hint Resolve sum_firstn_limb_widths_nonneg. Lemma two_sum_firstn_limb_widths_pos n : 0 < 2^sum_firstn limb_widths n. - Proof. auto with zarith. Qed. + Proof using Type*. auto with zarith. Qed. Lemma two_sum_firstn_limb_widths_nonzero n : 2^sum_firstn limb_widths n <> 0. - Proof. pose proof (two_sum_firstn_limb_widths_pos n); omega. Qed. + Proof using Type*. pose proof (two_sum_firstn_limb_widths_pos n); omega. Qed. Lemma base_from_limb_widths_step : forall i b w, (S i < length limb_widths)%nat -> nth_error base i = Some b -> nth_error limb_widths i = Some w -> nth_error base (S i) = Some (two_p w * b). - Proof. + Proof using Type. clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; unfold base_from_limb_widths in *; fold base_from_limb_widths in *; @@ -101,7 +101,7 @@ Section Pow2BaseProofs. Lemma nth_error_base : forall i, (i < length limb_widths)%nat -> nth_error base i = Some (two_p (sum_firstn limb_widths i)). - Proof. + Proof using Type*. induction i; intros. + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. @@ -126,7 +126,7 @@ Section Pow2BaseProofs. Lemma nth_default_base : forall d i, (i < length limb_widths)%nat -> nth_default d base i = 2 ^ (sum_firstn limb_widths i). - Proof. + Proof using Type*. intros ? ? i_lt_length. apply nth_error_value_eq_nth_default. rewrite nth_error_base, two_p_correct by assumption. @@ -135,7 +135,7 @@ Section Pow2BaseProofs. Lemma base_succ : forall i, ((S i) < length limb_widths)%nat -> nth_default 0 base (S i) mod nth_default 0 base i = 0. - Proof. + Proof using Type*. intros. repeat rewrite nth_default_base by omega. apply Z.mod_same_pow. @@ -157,7 +157,7 @@ Section Pow2BaseProofs. Lemma nth_error_subst : forall i b, nth_error base i = Some b -> b = 2 ^ (sum_firstn limb_widths i). - Proof. + Proof using Type*. intros i b nth_err_b. pose proof (nth_error_value_length _ _ _ _ nth_err_b). rewrite base_from_limb_widths_length in *. @@ -167,7 +167,7 @@ Section Pow2BaseProofs. Qed. Lemma base_positive : forall b : Z, In b base -> b > 0. - Proof. + Proof using Type*. intros b In_b_base. apply In_nth_error_value in In_b_base. destruct In_b_base as [i nth_err_b]. @@ -178,7 +178,7 @@ Section Pow2BaseProofs. Qed. Lemma b0_1 : forall x : Z, limb_widths <> nil -> nth_default x base 0 = 1. - Proof. + Proof using Type. case_eq limb_widths; intros; [congruence | reflexivity]. Qed. @@ -187,7 +187,7 @@ Section Pow2BaseProofs. (l_nonneg : forall x, In x l -> 0 <= x), base_from_limb_widths (l0 ++ l) = base_from_limb_widths l0 ++ map (Z.mul (two_p (sum_firstn l0 (length l0)))) (base_from_limb_widths l). - Proof. + Proof using Type. induction l0 as [|?? IHl0]. { simpl; intros; rewrite <- map_id at 1; apply map_ext; intros; omega. } { simpl; intros; rewrite !IHl0, !map_app, map_map, sum_firstn_succ_cons, two_p_is_exp by auto with znonzero. @@ -195,7 +195,7 @@ Section Pow2BaseProofs. Qed. Lemma skipn_base_from_limb_widths : forall n, skipn n (base_from_limb_widths limb_widths) = map (Z.mul (two_p (sum_firstn limb_widths n))) (base_from_limb_widths (skipn n limb_widths)). - Proof. + Proof using Type*. intro n; pose proof (base_from_limb_widths_app (firstn n limb_widths) (skipn n limb_widths)) as H. specialize_by eauto using In_firstn, In_skipn. autorewrite with simpl_firstn simpl_skipn in *. @@ -212,7 +212,7 @@ Section Pow2BaseProofs. Lemma pow2_mod_bounded :forall lw us i, (forall w, In w lw -> 0 <= w) -> bounded lw us -> Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i. - Proof. + Proof using Type. clear. repeat match goal with | |- _ => progress (cbv [bounded]; intros) @@ -231,7 +231,7 @@ Section Pow2BaseProofs. Lemma pow2_mod_bounded_iff :forall lw us, (forall w, In w lw -> 0 <= w) -> (bounded lw us <-> (forall i, Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i)). - Proof. + Proof using Type. clear. split; intros; auto using pow2_mod_bounded. cbv [bounded]; intros. @@ -251,7 +251,7 @@ Section Pow2BaseProofs. Qed. Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0). - Proof. + Proof using Type. clear. split; cbv [bounded]; intros. + edestruct (In_nth_error_value us u); try assumption. @@ -267,7 +267,7 @@ Section Pow2BaseProofs. Qed. Lemma bounded_iff : forall lw us, bounded lw us <-> forall i, 0 <= nth_default 0 us i < 2 ^ nth_default 0 lw i. - Proof. + Proof using Type. clear. cbv [bounded]; intros. reflexivity. @@ -275,7 +275,7 @@ Section Pow2BaseProofs. Lemma digit_select : forall us i, bounded limb_widths us -> nth_default 0 us i = Z.pow2_mod (BaseSystem.decode base us >> sum_firstn limb_widths i) (nth_default 0 limb_widths i). - Proof. + Proof using Type*. intro; revert limb_widths limb_widths_nonneg; induction us; intros. + rewrite nth_default_nil, decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by (try (apply Z.pow_nonzero; try omega); apply nth_default_preserves_properties; auto; omega). @@ -330,7 +330,7 @@ Section Pow2BaseProofs. Qed. Lemma nth_default_limb_widths_nonneg : forall i, 0 <= nth_default 0 limb_widths i. - Proof. + Proof using Type*. intros; apply nth_default_preserves_properties; auto; omega. Qed. Hint Resolve nth_default_limb_widths_nonneg. @@ -338,7 +338,7 @@ Section Pow2BaseProofs. (0 < nth_default 0 limb_widths 0) -> length x = length limb_widths -> Z.odd (BaseSystem.decode base x) = Z.odd (nth_default 0 x 0). - Proof. + Proof using Type*. intros. destruct limb_widths, x; simpl in *; try discriminate; try reflexivity. rewrite peel_decode, nth_default_cons. @@ -355,7 +355,7 @@ Section Pow2BaseProofs. length us = length limb_widths -> bounded limb_widths us -> BaseSystem.decode' base (firstn i us) = Z.pow2_mod (BaseSystem.decode' base us) (sum_firstn limb_widths i). - Proof. + Proof using Type*. intros; induction i; repeat match goal with | |- _ => rewrite sum_firstn_0, decode_nil, Z.pow2_mod_0_r; reflexivity @@ -392,7 +392,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> sum_firstn limb_widths i <= n -> Z.testbit (BaseSystem.decode base (firstn i us)) n = false. - Proof. + Proof using Type*. repeat match goal with | |- _ => progress intros | |- _ => progress autorewrite with Ztestbit @@ -410,7 +410,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> sum_firstn limb_widths (length us) <= n -> Z.testbit (BaseSystem.decode base us) n = false. - Proof. + Proof using Type*. intros. erewrite <-(firstn_all _ us) by reflexivity. auto using testbit_decode_firstn_high. @@ -421,7 +421,7 @@ Section Pow2BaseProofs. length us = length limb_widths -> bounded limb_widths us -> 0 <= BaseSystem.decode base us. - Proof. + Proof using Type*. intros. unfold bounded, BaseSystem.decode, BaseSystem.decode' in *; simpl in *. pose 0 as zero. @@ -450,7 +450,7 @@ Section Pow2BaseProofs. length us = length limb_widths -> bounded limb_widths us -> 0 <= BaseSystem.decode base us < upper_bound limb_widths. - Proof. + Proof using Type*. cbv [upper_bound]; intros. split. { apply decode_nonneg; auto. } @@ -465,7 +465,7 @@ Section Pow2BaseProofs. length us = length limb_widths -> BaseSystem.decode base (firstn (S i) us) = Z.lor (BaseSystem.decode base (firstn i us)) (nth_default 0 us i << sum_firstn limb_widths i). - Proof. + Proof using Type*. repeat match goal with | |- _ => progress intros | |- _ => progress autorewrite with Ztestbit @@ -498,7 +498,7 @@ Section Pow2BaseProofs. bounded limb_widths us -> sum_firstn limb_widths i <= n < sum_firstn limb_widths (S i) -> Z.testbit (BaseSystem.decode base us) n = Z.testbit (nth_default 0 us i) (n - sum_firstn limb_widths i). - Proof. + Proof using Type*. repeat match goal with | |- _ => progress intros | |- _ => erewrite digit_select by eauto @@ -513,7 +513,7 @@ Section Pow2BaseProofs. Lemma testbit_bounded_high : forall i n us, bounded limb_widths us -> nth_default 0 limb_widths i <= n -> Z.testbit (nth_default 0 us i) n = false. - Proof. + Proof using Type*. repeat match goal with | |- _ => progress intros | |- _ => break_if @@ -528,7 +528,7 @@ Section Pow2BaseProofs. Lemma decode_shift_app : forall us0 us1, (length (us0 ++ us1) <= length limb_widths)%nat -> BaseSystem.decode base (us0 ++ us1) = (BaseSystem.decode (base_from_limb_widths (firstn (length us0) limb_widths)) us0) + ((BaseSystem.decode (base_from_limb_widths (skipn (length us0) limb_widths)) us1) << sum_firstn limb_widths (length us0)). - Proof. + Proof using Type*. unfold BaseSystem.decode; intros us0 us1 ?. assert (0 <= sum_firstn limb_widths (length us0)) by auto using sum_firstn_nonnegative. rewrite decode'_splice; autorewrite with push_firstn. @@ -539,17 +539,17 @@ Section Pow2BaseProofs. Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0)). - Proof. + Proof using Type*. intros; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. transitivity (u0 * 1 + 0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0 + 0))); [ | autorewrite with zsimplify; reflexivity ]. destruct limb_widths; distr_length; reflexivity. Qed. Lemma upper_bound_nil : upper_bound nil = 1. - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Lemma upper_bound_cons x xs : 0 <= x -> 0 <= sum_firstn xs (length xs) -> upper_bound (x::xs) = 2^x * upper_bound xs. - Proof. + Proof using Type. intros Hx Hxs. unfold upper_bound; simpl. autorewrite with simpl_sum_firstn pull_Zpow. @@ -557,7 +557,7 @@ Section Pow2BaseProofs. Qed. Lemma upper_bound_app xs ys : 0 <= sum_firstn xs (length xs) -> 0 <= sum_firstn ys (length ys) -> upper_bound (xs ++ ys) = upper_bound xs * upper_bound ys. - Proof. + Proof using Type. intros Hxs Hys. unfold upper_bound; simpl. autorewrite with distr_length simpl_sum_firstn pull_Zpow. @@ -565,7 +565,7 @@ Section Pow2BaseProofs. Qed. Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil. - Proof. + Proof using Type. cbv [bounded]; intros. rewrite nth_default_nil. apply nth_default_preserves_properties; intros; split; zero_bounds. @@ -590,7 +590,7 @@ Section Pow2BaseProofs. let b := nth_default 0 base in let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in b i * b j = r * (2^k * b (i+j-length base)%nat). - Proof. + Proof using limb_widths_match_modulus limb_widths_nonneg. intros. rewrite (Z.mul_comm r). subst r. @@ -615,7 +615,7 @@ Section Pow2BaseProofs. let b := nth_default 0 base in let r := b i * b j / b (i + j)%nat in b i * b j = r * b (i + j)%nat. - Proof. + Proof using limb_widths_good limb_widths_nonneg. intros; subst b r. clear limb_widths_match_modulus. rewrite base_from_limb_widths_length in *. @@ -662,7 +662,7 @@ Section BitwiseDecodeEncode. Lemma encode'_spec : forall x i, (i <= length limb_widths)%nat -> encode' limb_widths x i = BaseSystem.encode' base x upper_bound i. - Proof. + Proof using limb_widths_nonneg. induction i; intros. + rewrite encode'_zero. reflexivity. + rewrite encode'_succ, <-IHi by omega. @@ -678,14 +678,14 @@ Section BitwiseDecodeEncode. Qed. Lemma length_encode' : forall lw z i, length (encode' lw z i) = i. - Proof. + Proof using Type. induction i; intros; simpl encode'; distr_length. Qed. Hint Rewrite length_encode' : distr_length. Lemma bounded_encode' : forall z i, (0 <= z) -> bounded (firstn i limb_widths) (encode' limb_widths z i). - Proof. + Proof using limb_widths_nonneg. intros; induction i; simpl encode'; repeat match goal with | |- _ => progress intros @@ -715,14 +715,14 @@ Section BitwiseDecodeEncode. Lemma bounded_encodeZ : forall z, (0 <= z) -> bounded limb_widths (encodeZ limb_widths z). - Proof. + Proof using limb_widths_nonneg. cbv [encodeZ]; intros. pose proof (bounded_encode' z (length limb_widths)) as Hencode'. rewrite firstn_all in Hencode'; auto. Qed. Lemma base_upper_bound_compatible : @base_max_succ_divide base upper_bound. - Proof. + Proof using limb_widths_nonneg. unfold base_max_succ_divide; intros i lt_Si_length. rewrite base_from_limb_widths_length in lt_Si_length. rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length; @@ -757,7 +757,7 @@ Section BitwiseDecodeEncode. Qed. Lemma encodeZ_length : forall x, length (encodeZ limb_widths x) = length limb_widths. - Proof. + Proof using limb_widths_nonneg. cbv [encodeZ]; intros. rewrite encode'_spec by omega. apply encode'_length. @@ -771,7 +771,7 @@ Section BitwiseDecodeEncode. bounded limb_widths us -> forall i acc, decode_bitwise'_invariant us (S i) acc -> decode_bitwise'_invariant us i (Z.lor (nth_default 0 us i) (acc << nth_default 0 limb_widths i)). - Proof. + Proof using limb_widths_nonneg. repeat match goal with | |- _ => progress cbv [decode_bitwise'_invariant]; intros | |- _ => erewrite testbit_bounded_high by (omega || eauto) @@ -793,7 +793,7 @@ Section BitwiseDecodeEncode. bounded limb_widths us -> decode_bitwise'_invariant us i acc -> decode_bitwise'_invariant us 0 (decode_bitwise' limb_widths us i acc). - Proof. + Proof using limb_widths_nonneg. repeat match goal with | |- _ => progress intros | |- _ => solve [auto using decode_bitwise'_invariant_step] @@ -805,7 +805,7 @@ Section BitwiseDecodeEncode. Lemma decode_bitwise_spec : forall us, bounded limb_widths us -> length us = length limb_widths -> decode_bitwise limb_widths us = BaseSystem.decode base us. - Proof. + Proof using limb_widths_nonneg. repeat match goal with | |- _ => progress cbv [decode_bitwise decode_bitwise'_invariant] in * | |- _ => progress intros @@ -833,7 +833,7 @@ Section UniformBase. Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat -> (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)). - Proof. + Proof using Type*. cbv [bounded]; split; intro A; intros. + let G := fresh "G" in match goal with H : In _ us |- _ => @@ -853,7 +853,7 @@ Section UniformBase. Qed. Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. - Proof. + Proof using Type*. intros. replace w with width by (symmetry; auto). assumption. @@ -866,14 +866,14 @@ Section UniformBase. Lemma nth_default_uniform_base : forall i, (i < length limb_widths)%nat -> nth_default 0 limb_widths i = width. - Proof. + Proof using Type*. intros; rewrite nth_default_uniform_base_full. edestruct lt_dec; omega. Qed. Lemma sum_firstn_uniform_base : forall i, (i <= length limb_widths)%nat -> sum_firstn limb_widths i = Z.of_nat i * width. - Proof. + Proof using limb_widths_uniform. clear limb_width_nonneg. (* clear this before induction so we don't depend on this *) induction limb_widths as [|x xs IHxs]; (intros [|i] ?); simpl @length in *; @@ -886,18 +886,18 @@ Section UniformBase. Lemma sum_firstn_uniform_base_strong : forall i, (length limb_widths <= i)%nat -> sum_firstn limb_widths i = Z.of_nat (length limb_widths) * width. - Proof. + Proof using limb_widths_uniform. intros; rewrite sum_firstn_all, sum_firstn_uniform_base by omega; reflexivity. Qed. Lemma upper_bound_uniform : upper_bound limb_widths = 2^(Z.of_nat (length limb_widths) * width). - Proof. + Proof using limb_widths_uniform. unfold upper_bound; rewrite sum_firstn_uniform_base_strong by omega; reflexivity. Qed. (* TODO : move *) Lemma decode_truncate_base : forall us bs, BaseSystem.decode bs us = BaseSystem.decode (firstn (length us) bs) us. - Proof. + Proof using Type. clear. induction us; intros. + rewrite !decode_nil; reflexivity. @@ -913,7 +913,7 @@ Section UniformBase. Lemma tl_repeat : forall {A} xs n (x : A), (forall y, In y xs -> y = x) -> (n < length xs)%nat -> firstn n xs = firstn n (tl xs). - Proof. + Proof using Type. intros. erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ]. rewrite ListUtil.tl_repeat. @@ -923,7 +923,7 @@ Section UniformBase. Lemma decode_tl_base : forall us, (length us < length limb_widths)%nat -> BaseSystem.decode base us = BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us. - Proof. + Proof using limb_widths_uniform. intros. match goal with |- BaseSystem.decode ?b1 _ = BaseSystem.decode ?b2 _ => rewrite (decode_truncate_base _ b1), (decode_truncate_base _ b2) end. @@ -934,7 +934,7 @@ Section UniformBase. Lemma decode_shift_uniform_tl : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << width). - Proof. + Proof using Type*. intros. rewrite <- (nth_default_uniform_base 0) by distr_length. rewrite decode_shift by auto using uniform_limb_widths_nonneg. @@ -943,7 +943,7 @@ Section UniformBase. Lemma decode_shift_uniform_app : forall us0 us1, (length (us0 ++ us1) <= length limb_widths)%nat -> BaseSystem.decode base (us0 ++ us1) = (BaseSystem.decode (base_from_limb_widths (firstn (length us0) limb_widths)) us0) + ((BaseSystem.decode (base_from_limb_widths (skipn (length us0) limb_widths)) us1) << (Z.of_nat (length us0) * width)). - Proof. + Proof using Type*. intros. rewrite <- sum_firstn_uniform_base by (distr_length; omega). rewrite decode_shift_app by auto using uniform_limb_widths_nonneg. @@ -952,7 +952,7 @@ Section UniformBase. Lemma decode_shift_uniform : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode base us) << width). - Proof. + Proof using Type*. intros. rewrite decode_tl_base with (us := us) by distr_length. apply decode_shift_uniform_tl; assumption. @@ -1074,7 +1074,7 @@ Section SplitIndex. length us = length limb_widths -> bounded limb_widths us -> Z.testbit (BaseSystem.decode base us) n = Z.testbit (us # digit_index n) (bit_index n). - Proof. + Proof using Type*. cbv [digit_index bit_index split_index]; intros. pose proof (split_index'_correct n 0 limb_widths). pose proof (snd_split_index'_nonneg 0 limb_widths n). @@ -1108,7 +1108,7 @@ Section SplitIndex. then Z.testbit (us # digit_index n) (bit_index n) else false) else false. - Proof. + Proof using Type*. repeat match goal with | |- _ => progress intros | |- _ => break_if @@ -1120,13 +1120,13 @@ Section SplitIndex. Qed. Lemma bit_index_nonneg : forall i, 0 <= i -> 0 <= bit_index i. - Proof. + Proof using Type. apply snd_split_index'_nonneg. Qed. Lemma digit_index_lt_length : forall i, 0 <= i < bitsIn limb_widths -> (digit_index i < length limb_widths)%nat. - Proof. + Proof using Type*. cbv [bit_index digit_index split_index]; intros. pose proof (split_index'_done_case i 0 limb_widths). specialize_by lia. specialize_by eauto. @@ -1135,6 +1135,8 @@ Section SplitIndex. Lemma bit_index_not_done : forall i, 0 <= i < bitsIn limb_widths -> (bit_index i < limb_widths # digit_index i). + Proof using Type. + cbv [bit_index digit_index split_index]; intros. eapply Z.lt_le_trans; try apply (snd_split_index'_small i 0 limb_widths); try assumption. rewrite Nat.sub_0_r; lia. @@ -1142,7 +1144,7 @@ Section SplitIndex. Lemma split_index_eqn : forall i, 0 <= i < bitsIn limb_widths -> sum_firstn limb_widths (digit_index i) + bit_index i = i. - Proof. + Proof using Type. cbv [bit_index digit_index split_index]; intros. etransitivity;[ | apply (split_index'_correct i 0 limb_widths) ]. repeat f_equal; omega. @@ -1150,7 +1152,7 @@ Section SplitIndex. Lemma rem_bits_in_digit_pos : forall i, 0 <= i < bitsIn limb_widths -> 0 < (limb_widths # digit_index i) - bit_index i. - Proof. + Proof using Type. repeat match goal with | |- _ => progress intros | |- 0 < ?a - ?b => destruct (Z_lt_dec b a); [ lia | exfalso ] @@ -1162,7 +1164,7 @@ Section SplitIndex. Lemma rem_bits_in_digit_le_rem_bits : forall i, 0 <= i < bitsIn limb_widths -> i + ((limb_widths # digit_index i) - bit_index i) <= bitsIn limb_widths. - Proof. + Proof using Type*. intros. rewrite <-(split_index_eqn i) at 1 by lia. match goal with @@ -1178,7 +1180,7 @@ Section SplitIndex. j < bitsIn limb_widths -> j < i + ((limb_widths # (digit_index i)) - bit_index i) -> (digit_index i = digit_index j)%nat. - Proof. + Proof using Type*. intros. pose proof (split_index_eqn i). pose proof (split_index_eqn j). @@ -1206,7 +1208,7 @@ Section SplitIndex. Lemma same_digit_bit_index_sub : forall i j, 0 <= i <= j -> j < bitsIn limb_widths -> digit_index i = digit_index j -> bit_index j - bit_index i = j - i. - Proof. + Proof using Type. intros. pose proof (split_index_eqn i). pose proof (split_index_eqn j). @@ -1225,7 +1227,7 @@ Section carrying_helper. Lemma update_nth_sum : forall n f us, (n < length us \/ n >= length limb_widths)%nat -> BaseSystem.decode base (update_nth n f us) = (let v := nth_default 0 us n in f v - v) * nth_default 0 base n + BaseSystem.decode base us. - Proof. + Proof using Type. intros. unfold BaseSystem.decode. destruct H as [H|H]. @@ -1272,7 +1274,7 @@ Section carrying_helper. | x'::xs' => x'::add_to_nth n' x xs' end end. - Proof. + Proof using Type. induction n; destruct xs; reflexivity. Qed. @@ -1283,7 +1285,7 @@ Section carrying_helper. | nil => nil | x'::xs' => x + x'::xs' end. - Proof. intro; rewrite unfold_add_to_nth; reflexivity. Qed. + Proof using Type. intro; rewrite unfold_add_to_nth; reflexivity. Qed. Lemma simpl_add_to_nth_S x n : forall xs, @@ -1292,25 +1294,25 @@ Section carrying_helper. | nil => nil | x'::xs' => x'::add_to_nth n x xs' end. - Proof. intro; rewrite unfold_add_to_nth; reflexivity. Qed. + Proof using Type. intro; rewrite unfold_add_to_nth; reflexivity. Qed. Hint Rewrite @simpl_set_nth_S @simpl_set_nth_0 : simpl_add_to_nth. Lemma add_to_nth_cons : forall x u0 us, add_to_nth 0 x (u0 :: us) = x + u0 :: us. - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Hint Rewrite @add_to_nth_cons : simpl_add_to_nth. Lemma cons_add_to_nth : forall n f y us, y :: add_to_nth n f us = add_to_nth (S n) f (y :: us). - Proof. + Proof using Type. induction n; boring. Qed. Hint Rewrite <- @cons_add_to_nth : simpl_add_to_nth. Lemma add_to_nth_nil : forall n f, add_to_nth n f nil = nil. - Proof. + Proof using Type. induction n; boring. Qed. @@ -1319,7 +1321,7 @@ Section carrying_helper. Lemma add_to_nth_set_nth n x xs : add_to_nth n x xs = set_nth n (x + nth_default 0 xs n) xs. - Proof. + Proof using Type. revert xs; induction n; destruct xs; autorewrite with simpl_set_nth simpl_add_to_nth; try rewrite IHn; @@ -1328,7 +1330,7 @@ Section carrying_helper. Lemma add_to_nth_update_nth n x xs : add_to_nth n x xs = update_nth n (fun y => x + y) xs. - Proof. + Proof using Type. revert xs; induction n; destruct xs; autorewrite with simpl_update_nth simpl_add_to_nth; try rewrite IHn; @@ -1336,19 +1338,19 @@ Section carrying_helper. Qed. Lemma length_add_to_nth i x xs : length (add_to_nth i x xs) = length xs. - Proof. unfold add_to_nth; distr_length; reflexivity. Qed. + Proof using Type. unfold add_to_nth; distr_length; reflexivity. Qed. Hint Rewrite @length_add_to_nth : distr_length. Lemma set_nth_sum : forall n x us, (n < length us \/ n >= length limb_widths)%nat -> BaseSystem.decode base (set_nth n x us) = (x - nth_default 0 us n) * nth_default 0 base n + BaseSystem.decode base us. - Proof. intros; unfold set_nth; rewrite update_nth_sum by assumption; reflexivity. Qed. + Proof using Type. intros; unfold set_nth; rewrite update_nth_sum by assumption; reflexivity. Qed. Lemma add_to_nth_sum : forall n x us, (n < length us \/ n >= length limb_widths)%nat -> BaseSystem.decode base (add_to_nth n x us) = x * nth_default 0 base n + BaseSystem.decode base us. - Proof. intros; rewrite add_to_nth_set_nth, set_nth_sum; try ring_simplify; auto. Qed. + Proof using Type. intros; rewrite add_to_nth_set_nth, set_nth_sum; try ring_simplify; auto. Qed. Lemma add_to_nth_nth_default_full : forall n x l i d, nth_default d (add_to_nth n x l) i = @@ -1356,17 +1358,17 @@ Section carrying_helper. if (eq_nat_dec i n) then x + nth_default d l i else nth_default d l i else d. - Proof. intros; rewrite add_to_nth_update_nth; apply update_nth_nth_default_full; assumption. Qed. + Proof using Type. intros; rewrite add_to_nth_update_nth; apply update_nth_nth_default_full; assumption. Qed. Hint Rewrite @add_to_nth_nth_default_full : push_nth_default. Lemma add_to_nth_nth_default : forall n x l i, (0 <= i < length l)%nat -> nth_default 0 (add_to_nth n x l) i = if (eq_nat_dec i n) then x + nth_default 0 l i else nth_default 0 l i. - Proof. intros; rewrite add_to_nth_update_nth; apply update_nth_nth_default; assumption. Qed. + Proof using Type. intros; rewrite add_to_nth_update_nth; apply update_nth_nth_default; assumption. Qed. Hint Rewrite @add_to_nth_nth_default using omega : push_nth_default. Lemma log_cap_nonneg : forall i, 0 <= log_cap i. - Proof. + Proof using Type*. unfold nth_default; intros. case_eq (nth_error limb_widths i); intros; try omega. apply limb_widths_nonneg. @@ -1389,17 +1391,17 @@ Section carrying. Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. Lemma length_carry_gen : forall fc fi i us, length (carry_gen limb_widths fc fi i us) = length us. - Proof. intros; unfold carry_gen, carry_single; distr_length; reflexivity. Qed. + Proof using Type. intros; unfold carry_gen, carry_single; distr_length; reflexivity. Qed. Hint Rewrite @length_carry_gen : distr_length. Lemma length_carry_simple : forall i us, length (carry_simple limb_widths i us) = length us. - Proof. intros; unfold carry_simple; distr_length; reflexivity. Qed. + Proof using Type. intros; unfold carry_simple; distr_length; reflexivity. Qed. Hint Rewrite @length_carry_simple : distr_length. Lemma nth_default_base_succ : forall i, (S i < length limb_widths)%nat -> nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i. - Proof. + Proof using Type*. intros. rewrite !nth_default_base, <- Z.pow_add_r by (omega || eauto using log_cap_nonneg). autorewrite with simpl_sum_firstn; reflexivity. @@ -1418,7 +1420,7 @@ Section carrying. else nth_default 0 base Si) - 2 ^ log_cap i * (nth_default 0 us i / 2 ^ log_cap i) * nth_default 0 base i) + BaseSystem.decode base us. - Proof. + Proof using Type*. intros fc fi i' us i Si H; intros. destruct (eq_nat_dec 0 (length limb_widths)); [ destruct limb_widths, us, i; simpl in *; try congruence; @@ -1454,7 +1456,7 @@ Section carrying. (length us = length limb_widths) -> (i < (pred (length limb_widths)))%nat -> BaseSystem.decode base (carry_simple limb_widths i us) = BaseSystem.decode base us. - Proof. + Proof using Type*. unfold carry_simple; intros; rewrite carry_gen_decode_eq by assumption. autorewrite with natsimplify. break_match; try lia; autorewrite with zsimplify; lia. @@ -1462,7 +1464,7 @@ Section carrying. Lemma length_carry_simple_sequence : forall is us, length (carry_simple_sequence limb_widths is us) = length us. - Proof. + Proof using Type. unfold carry_simple_sequence. induction is; [ reflexivity | simpl; intros ]. distr_length. @@ -1471,20 +1473,20 @@ Section carrying. Hint Rewrite @length_carry_simple_sequence : distr_length. Lemma length_make_chain : forall i, length (make_chain i) = i. - Proof. induction i; simpl; congruence. Qed. + Proof using Type. induction i; simpl; congruence. Qed. Hint Rewrite @length_make_chain : distr_length. Lemma length_full_carry_chain : length (full_carry_chain limb_widths) = length limb_widths. - Proof. unfold full_carry_chain; distr_length; reflexivity. Qed. + Proof using Type. unfold full_carry_chain; distr_length; reflexivity. Qed. Hint Rewrite @length_full_carry_chain : distr_length. Lemma length_carry_simple_full us : length (carry_simple_full limb_widths us) = length us. - Proof. unfold carry_simple_full; distr_length; reflexivity. Qed. + Proof using Type. unfold carry_simple_full; distr_length; reflexivity. Qed. Hint Rewrite @length_carry_simple_full : distr_length. (* TODO : move? *) Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. - Proof. + Proof using Type. induction x; simpl; intuition auto with arith lia. Qed. @@ -1498,7 +1500,7 @@ Section carrying. then fc (nth_default 0 us (fi i) >> log_cap (fi i)) else 0 else d. - Proof. + Proof using Type. unfold carry_gen, carry_single. intros; autorewrite with push_nth_default natsimplify distr_length. edestruct (lt_dec n (length us)) as [H|H]; [ | reflexivity ]. @@ -1516,7 +1518,7 @@ Section carrying. else nth_default 0 us n + if eq_nat_dec n (S i) then nth_default 0 us i >> log_cap i else 0 else d. - Proof. + Proof using Type. intros; unfold carry_simple; autorewrite with push_nth_default. repeat break_match; try omega; try reflexivity. Qed. @@ -1533,7 +1535,7 @@ Section carrying. if eq_nat_dec i (fi (S (fi i))) then fc (nth_default 0 us (fi i) >> log_cap (fi i)) else 0. - Proof. + Proof using Type. intros; autorewrite with push_nth_default natsimplify; break_match; omega. Qed. Hint Rewrite @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. @@ -1543,7 +1545,7 @@ Section carrying. (0 <= i < length us)%nat -> nth_default 0 (carry_simple limb_widths i us) i = Z.pow2_mod (nth_default 0 us i) (log_cap i). - Proof. + Proof using Type. intros; autorewrite with push_nth_default natsimplify; break_match; omega. Qed. Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index d48aab36e..eba1af740 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -22,13 +22,13 @@ Module F. Context (q:positive) {prime_q:prime q}. Lemma inv_spec : F.inv 0%F = (0%F : F q) /\ (prime q -> forall x : F q, x <> 0%F -> (F.inv x * x)%F = 1%F). - Proof. change (@F.inv q) with (proj1_sig (@F.inv_with_spec q)); destruct (@F.inv_with_spec q); eauto. Qed. + Proof using Type. change (@F.inv q) with (proj1_sig (@F.inv_with_spec q)); destruct (@F.inv_with_spec q); eauto. Qed. - Lemma inv_0 : F.inv 0%F = F.of_Z q 0. Proof. destruct inv_spec; auto. Qed. - Lemma inv_nonzero (x:F q) : (x <> 0 -> F.inv x * x%F = 1)%F. Proof. destruct inv_spec; auto. Qed. + Lemma inv_0 : F.inv 0%F = F.of_Z q 0. Proof using Type. destruct inv_spec; auto. Qed. + Lemma inv_nonzero (x:F q) : (x <> 0 -> F.inv x * x%F = 1)%F. Proof using Type*. destruct inv_spec; auto. Qed. Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul F.inv F.div. - Proof. + Proof using Type*. repeat match goal with | _ => solve [ solve_proper | apply F.commutative_ring_modulo @@ -45,10 +45,10 @@ Module F. (* TODO: move to PrimeFieldTheorems *) Lemma to_Z_1 : @F.to_Z q 1 = 1%Z. - Proof. simpl. rewrite Zmod_small; omega. Qed. + Proof using two_lt_q. simpl. rewrite Zmod_small; omega. Qed. Lemma Fq_inv_fermat (x:F q) : F.inv x = x ^ Z.to_N (q - 2)%Z. - Proof. + Proof using Type*. destruct (dec (x = 0%F)) as [?|Hnz]. { subst x; rewrite inv_0, F.pow_0_l; trivial. change (0%N) with (Z.to_N 0%Z); rewrite Z2N.inj_iff; omega. } @@ -59,7 +59,7 @@ Module F. Lemma euler_criterion (a : F q) (a_nonzero : a <> 0) : (a ^ (Z.to_N (q / 2)) = 1) <-> (exists b, b*b = a). - Proof. + Proof using Type*. pose proof F.to_Z_nonzero_range a; pose proof (odd_as_div q). specialize_by (destruct (Z.prime_odd_or_2 _ prime_q); try omega; trivial). rewrite F.eq_to_Z_iff, !F.to_Z_pow, !to_Z_1, !Z2N.id by omega. @@ -86,10 +86,10 @@ Module F. Definition sqrt_3mod4 (a : F q) : F q := a ^ Z.to_N (q / 4 + 1). Global Instance Proper_sqrt_3mod4 : Proper (eq ==> eq ) sqrt_3mod4. - Proof. repeat intro; subst; reflexivity. Qed. + Proof using Type. repeat intro; subst; reflexivity. Qed. Lemma two_lt_q_3mod4 : 2 < q. - Proof. + Proof using Type*. pose proof (prime_ge_2 q _) as two_le_q. destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|]. rewrite <-H in q_3mod4; discriminate. @@ -98,7 +98,7 @@ Module F. Lemma sqrt_3mod4_correct (x:F q) : ((exists y, y*y = x) <-> (sqrt_3mod4 x)*(sqrt_3mod4 x) = x)%F. - Proof. + Proof using Type*. cbv [sqrt_3mod4]; intros. destruct (F.eq_dec x 0); repeat match goal with @@ -136,7 +136,7 @@ Module F. Context (sqrt_minus1 : F q) (sqrt_minus1_valid : sqrt_minus1 * sqrt_minus1 = F.opp 1). Lemma two_lt_q_5mod8 : 2 < q. - Proof. + Proof using prime_q q_5mod8. pose proof (prime_ge_2 q _) as two_le_q. destruct (Zle_lt_or_eq _ _ two_le_q) as [H|H]; [exact H|]. rewrite <-H in *. discriminate. @@ -150,11 +150,11 @@ Module F. else sqrt_minus1 * b. Global Instance Proper_sqrt_5mod8 : Proper (eq ==> eq ) sqrt_5mod8. - Proof. repeat intro; subst; reflexivity. Qed. + Proof using Type. repeat intro; subst; reflexivity. Qed. Lemma eq_b4_a2 (x : F q) (Hex:exists y, y*y = x) : ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2. - Proof. + Proof using prime_q q_5mod8. pose proof two_lt_q_5mod8. assert (0 <= q/8)%Z by (apply Z.div_le_lower_bound; rewrite ?Z.mul_0_r; omega). assert (Z.to_N (q / 8 + 1) <> 0%N) by @@ -185,7 +185,7 @@ Module F. Qed. Lemma mul_square_sqrt_minus1 : forall x, sqrt_minus1 * x * (sqrt_minus1 * x) = F.opp (x * x). - Proof. + Proof using prime_q sqrt_minus1_valid. intros. transitivity (F.opp 1 * (x * x)); [ | field]. rewrite <-sqrt_minus1_valid. @@ -194,7 +194,7 @@ Module F. Lemma eq_b4_a2_iff (x : F q) : x <> 0 -> ((exists y, y*y = x) <-> ((x ^ Z.to_N (q / 8 + 1)) ^ 2) ^ 2 = x ^ 2). - Proof. + Proof using Type*. split; try apply eq_b4_a2. intro Hyy. rewrite !@F.pow_2_r in *. @@ -207,7 +207,7 @@ Module F. Lemma sqrt_5mod8_correct : forall x, ((exists y, y*y = x) <-> (sqrt_5mod8 x)*(sqrt_5mod8 x) = x). - Proof. + Proof using Type*. cbv [sqrt_5mod8]; intros. destruct (F.eq_dec x 0). { @@ -261,7 +261,7 @@ Module F. @Algebra.ring H eq zero one opp add sub mul /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'. - Proof. eapply @Ring.ring_by_isomorphism; assumption || exact _. Qed. + Proof using phi'_add phi'_iff phi'_mul phi'_one phi'_opp phi'_phi phi'_sub phi'_zero. eapply @Ring.ring_by_isomorphism; assumption || exact _. Qed. Local Instance _iso_ring : Algebra.ring := proj1 ring. Local Instance _iso_hom1 : Ring.is_homomorphism := proj1 (proj2 ring). Local Instance _iso_hom2 : Ring.is_homomorphism := proj2 (proj2 ring). @@ -287,7 +287,7 @@ Module F. @Algebra.field H eq zero one opp add sub mul inv div /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'. - Proof. eapply @Field.field_and_homomorphism_from_redundant_representation; + Proof using Type*. eapply @Field.field_and_homomorphism_from_redundant_representation; assumption || exact _ || exact inv_proof || exact div_proof. Qed. End IsomorphicRings. End Iso. 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. |