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/Util/ZUtil.v | |
parent | 8cc484392fe5a5b063b4dcce0a8464a7b849e9c6 (diff) |
prove testbit_sub_pow2
Diffstat (limited to 'src/Util/ZUtil.v')
-rw-r--r-- | src/Util/ZUtil.v | 20 |
1 files changed, 20 insertions, 0 deletions
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 |