diff options
author | jadep <jade.philipoom@gmail.com> | 2016-08-16 18:28:13 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-08-16 18:28:13 -0400 |
commit | 82defeaac51f1b76217fcb548a8115449946e432 (patch) | |
tree | ee253f108337609a75d04d823ee48b79796f63b8 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
parent | 071ef883b070577d1bf57292db7fc981732c3df4 (diff) |
Instantiated conversion both to (pack) and from (unpack) another set of limb widths in ModularBaseSystem
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 2331a0435..5b01a0f6c 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -97,7 +97,11 @@ Section PseudoMersenneProofs. rewrite encode_eq, encode_rep. + apply F.of_Z_to_Z. + apply bv. - + split; [ | etransitivity]; try (apply F.to_Z_range; auto using modulus_pos); auto. + + rewrite <-F.mod_to_Z. + match goal with |- appcontext [?a mod modulus] => + pose proof (Z.mod_pos_bound a modulus modulus_pos) end. + pose proof lt_modulus_2k. + omega. + eauto using base_upper_bound_compatible, limb_widths_nonneg. Qed. @@ -167,7 +171,7 @@ Section PseudoMersenneProofs. cbv [ModularBaseSystemList.mul ModularBaseSystemList.decode]. rewrite F.of_Z_mod, reduce_rep, <-F.of_Z_mod. pose proof (@base_from_limb_widths_length limb_widths). - rewrite mul_rep by (auto using ExtBaseVector || rewrite extended_base_length, !length_to_list; omega). + rewrite @mul_rep by (eauto using ExtBaseVector || rewrite extended_base_length, !length_to_list; omega). rewrite 2decode_short by (rewrite ?base_from_limb_widths_length; auto using Nat.eq_le_incl, length_to_list with omega). apply F.of_Z_mul. |