diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-10-29 16:17:10 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-10-29 16:17:10 -0400 |
| commit | a0bf587c8223ae237a475bb523784502a7a7dd68 (patch) | |
| tree | fbe8526631fb2c84d77e467fd61ea719adbca03a /src/ModularArithmetic | |
| parent | 8cc484392fe5a5b063b4dcce0a8464a7b849e9c6 (diff) | |
prove testbit_sub_pow2
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 9cb65bd19..fd9483182 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -157,12 +157,6 @@ Section ModulusDigitsProofs. Local Hint Resolve sum_firstn_limb_widths_nonneg. Local Hint Resolve limb_widths_nonneg. - (* TODO : ZUtil *) - Lemma testbit_sub_pow2 : forall n i x, 0 <= i < n -> 0 < x < 2 ^ n -> - Z.testbit (2 ^ n - x) i = negb (Z.testbit (x - 1) i). - Proof. - Admitted. - Lemma decode_modulus_digits : decode' base modulus_digits = modulus. Proof. cbv [modulus_digits]. @@ -197,7 +191,7 @@ Section ModulusDigitsProofs. | |- _ => erewrite digit_select by (eauto; apply bounded_encodeZ; eauto; omega) | |- Z.testbit (2 ^ k - c) _ = _ => - rewrite testbit_sub_pow2 by (try omega; cbv [k]; + rewrite Z.testbit_sub_pow2 by (try omega; cbv [k]; pose proof (sum_firstn_prefix_le limb_widths (S i) (length limb_widths)); specialize_by (eauto || omega); rewrite sum_firstn_succ_default in *; split; zero_bounds; eauto) |