prove testbit_sub_pow2

2 files changed, 21 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)
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