diff options
author | jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
commit | cc920cf2a3aa859a93e8e990a19a960f78cd3b1b (patch) | |
tree | ed93d93f82578239ef2e0a6843e52e1d6968a5ef /src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | |
parent | 260b20cab885deae59a305492567dc0f0d88b3a8 (diff) | |
parent | 0cea3e2f80408a25954f820faebf5cd79d2e13ae (diff) |
Merged changes, including new ZUtil conventions.
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParamProofs.v')
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 50c1f3ea6..c07da850f 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -42,7 +42,7 @@ Section PseudoMersenneBaseParamProofs. rewrite (Z.mul_comm r). subst r. assert (i + j - length base < length base)%nat by omega. - rewrite mul_div_eq by (apply gt_lt_symmetry; apply Z.mul_pos_pos; + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos; [ | subst b; unfold base; rewrite nth_default_base; try assumption ]; zero_bounds; auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg). rewrite (Zminus_0_l_reverse (b i * b j)) at 1. @@ -51,7 +51,7 @@ Section PseudoMersenneBaseParamProofs. unfold base; repeat rewrite nth_default_base by auto. do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. symmetry. - apply mod_same_pow. + apply Z.mod_same_pow. split. + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg. + rewrite base_length, base_from_limb_widths_length in * by auto. @@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs. destruct In_b_base as [i nth_err_b]. apply nth_error_subst in nth_err_b; [ | auto ]. rewrite nth_err_b. - apply gt_lt_symmetry. + apply Z.gt_lt_iff. apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg. Qed. @@ -84,10 +84,10 @@ Section PseudoMersenneBaseParamProofs. unfold base in *. repeat rewrite nth_default_base by (omega || auto). rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). - rewrite mul_div_eq by (apply gt_lt_symmetry; zero_bounds; + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds; auto using sum_firstn_limb_widths_nonneg). rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. - rewrite mod_same_pow; try ring. + rewrite Z.mod_same_pow; try ring. split; [ auto using sum_firstn_limb_widths_nonneg | ]. apply limb_widths_good. rewrite <- base_length; assumption. |