diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-21 15:38:17 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-21 15:38:17 -0400 |
| commit | e72acba808ef9a0620b9d2d5275af85dfa96c3ad (patch) | |
| tree | 4dda82bc1968ac9b76be7fb16554d2a9a5b249a5 /src/ModularArithmetic | |
| parent | 92cebb5b7c7b588467cdf4c07115aaaeafea2360 (diff) | |
| parent | d95a25365f600305bfcc374fbc24322e66c7c896 (diff) | |
Merge.
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 5923a7279..0ce214bbd 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -1205,6 +1205,8 @@ Section Conversion. let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in convert' inp (i + Z.to_nat dist)%nat (update_nth digitB (update_by_concat_bits indexB bitsA) out). Proof. + generalize limb_widthsA_nonneg; intros _. (* don't drop this from the proof in 8.4 *) + generalize limb_widthsB_nonneg; intros _. (* don't drop this from the proof in 8.4 *) repeat match goal with | |- _ => progress intros | |- appcontext [bit_index (Z.of_nat ?i)] => @@ -1212,7 +1214,7 @@ Section Conversion. | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] => unique pose proof (bit_index_not_done lw i) | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] => - unique pose proof (rem_bits_in_digit_le_rem_bits lw H i) + unique assert (0 <= i < bitsIn lw -> i + (lw # digit_index lw i - bit_index lw i) <= bitsIn lw) by auto using rem_bits_in_digit_le_rem_bits | |- _ => rewrite Z2Nat.id | |- _ => rewrite Nat2Z.inj_add | |- (Z.to_nat _ < Z.to_nat _)%nat => apply Z2Nat.inj_lt |