From a0bf587c8223ae237a475bb523784502a7a7dd68 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 29 Oct 2016 16:17:10 -0400 Subject: prove testbit_sub_pow2 --- src/ModularArithmetic/ModularBaseSystemListProofs.v | 8 +------- src/Util/ZUtil.v | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+), 7 deletions(-) (limited to 'src') 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) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c5a2ae99d..5417c3407 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -891,6 +891,26 @@ Module Z. Qed. Hint Rewrite shiftr_spec_full : Ztestbit_full. + Lemma lnot_sub1 x : Z.lnot (x-1) = (-x). + Proof. + replace (-x) with (- (1) - (x - 1)) by omega. + rewrite <-(Z.add_lnot_diag (x-1)); omega. + Qed. + + Lemma lnot_opp x : Z.lnot (- x) = x-1. + Proof. + rewrite <-Z.lnot_involutive, lnot_sub1; reflexivity. + Qed. + + Lemma testbit_sub_pow2 n i x (i_range:0 <= i < n) (x_range:0 < x < 2 ^ n) : + Z.testbit (2 ^ n - x) i = negb (Z.testbit (x - 1) i). + Proof. + rewrite <-Z.lnot_spec, lnot_sub1 by omega. + rewrite <-(Z.mod_pow2_bits_low (-x) _ _ (proj2 i_range)). + f_equal. + rewrite Z.mod_opp_l_nz; autorewrite with zsimplify; omega. + Qed. + (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) Ltac zero_bounds' := repeat match goal with -- cgit v1.2.3