Add some ZUtil lemmas and hints

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
2m45.95s | Total                                           | 2m39.20s || +0m06.74s
----------------------------------------------------------------------------------
0m17.76s | ModularArithmetic/ModularBaseSystemProofs       | 0m20.55s || -0m02.78s
0m14.41s | Util/ZUtil                                      | 0m11.79s || +0m02.62s
0m12.45s | Specific/GF25519                                | 0m10.16s || +0m02.28s
0m09.20s | Specific/GF1305                                 | 0m07.08s || +0m02.11s
0m11.29s | ModularArithmetic/Montgomery/ZProofs            | 0m10.07s || +0m01.21s
0m05.36s | ModularArithmetic/Tutorial                      | 0m03.87s || +0m01.49s
0m02.73s | ModularArithmetic/ModularArithmeticTheorems     | 0m03.91s || -0m01.18s
0m24.05s | ModularArithmetic/Pow2BaseProofs                | 0m23.30s || +0m00.75s
0m15.10s | Experiments/SpecEd25519                         | 0m14.69s || +0m00.41s
0m10.42s | Testbit                                         | 0m10.86s || -0m00.43s
0m04.40s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m04.26s || +0m00.14s
0m04.29s | BaseSystemProofs                                | 0m04.96s || -0m00.67s
0m04.11s | Experiments/SpecificCurve25519                  | 0m03.28s || +0m00.83s
0m03.66s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m04.01s || -0m00.34s
0m02.80s | ModularArithmetic/BarrettReduction/ZBounded     | 0m03.50s || -0m00.70s
0m02.26s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.24s || +0m00.01s
0m02.12s | Encoding/PointEncodingPre                       | 0m01.81s || +0m00.31s
0m02.04s | ModularArithmetic/BarrettReduction/Z            | 0m01.52s || +0m00.52s
0m01.71s | ModularArithmetic/ExtendedBaseVector            | 0m01.29s || +0m00.41s
0m01.62s | BaseSystem                                      | 0m01.22s || +0m00.40s
0m01.28s | ModularArithmetic/Montgomery/ZBounded           | 0m01.20s || +0m00.08s
0m01.05s | ModularArithmetic/PrimeFieldTheorems            | 0m01.22s || -0m00.16s
0m00.96s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.01s || -0m00.05s
0m00.94s | Util/NumTheoryUtil                              | 0m00.93s || +0m00.00s
0m00.93s | ModularArithmetic/ModularBaseSystem             | 0m00.78s || +0m00.15s
0m00.93s | ModularArithmetic/ModularBaseSystemListProofs   | 0m01.06s || -0m00.13s
0m00.92s | ModularArithmetic/ModularBaseSystemList         | 0m00.87s || +0m00.05s
0m00.90s | ModularArithmetic/ModularBaseSystemField        | 0m00.89s || +0m00.01s
0m00.72s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.80s || -0m00.08s
0m00.72s | Encoding/ModularWordEncodingTheorems            | 0m00.79s || -0m00.07s
0m00.72s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.88s || -0m00.16s
0m00.65s | Encoding/ModularWordEncodingPre                 | 0m00.82s || -0m00.16s
0m00.59s | Spec/ModularWordEncoding                        | 0m00.65s || -0m00.06s
0m00.56s | ModularArithmetic/Pre                           | 0m00.53s || +0m00.03s
0m00.53s | Spec/ModularArithmetic                          | 0m00.39s || +0m00.14s
0m00.49s | ModularArithmetic/ZBounded                      | 0m00.59s || -0m00.09s
0m00.44s | ModularArithmetic/Pow2Base                      | 0m00.50s || -0m00.06s
0m00.43s | ModularArithmetic/Montgomery/Z                  | 0m00.42s || +0m00.01s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.51s || -0m00.10s

1 files changed, 11 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 9a6080cda..bf3907e1c 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -22,7 +22,7 @@ Hint Extern 1 => omega : omega.
 Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r : zarith.
 Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith.
 
-Ltac zutil_arith := solve [ omega | lia ].
+Ltac zutil_arith := solve [ omega | lia | auto with nocore ].
 
 (** Only hints that are always safe to apply (i.e., reversible), and
     which can reasonably be said to "simplify" the goal, should go in
@@ -111,6 +111,8 @@ Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_d
 Create HintDb zstrip_div.
 Hint Rewrite Z.div_small_iff using zutil_arith : zstrip_div.
 
+Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_div_pow2 using zutil_arith : convert_to_Ztestbit.
+
 (** It's not clear that [mod] is much easier for [lia] than [Z.div],
     so we separate out the transformations between [mod] and [div].
     We'll put, e.g., [mul_div_eq] into it below. *)
@@ -219,6 +221,7 @@ Module Z.
     unfold Z.pow2_mod.
     rewrite Z.land_ones; auto.
   Qed.
+  Hint Rewrite <- Z.pow2_mod_spec using zutil_arith : convert_to_Ztestbit.
 
   Lemma ones_spec : forall n m, 0 <= n -> 0 <= m -> Z.testbit (Z.ones n) m = if Z_lt_dec m n then true else false.
   Proof.
@@ -272,6 +275,13 @@ Module Z.
     apply Z.min_case_strong; intros; repeat progress (try break_if; autorewrite with Ztestbit zsimplify; try reflexivity).
   Qed.
 
+  Lemma pow2_mod_pos_bound a b : 0 < b -> 0 <= Z.pow2_mod a b < 2^b.
+  Proof.
+    intros; rewrite Z.pow2_mod_spec by omega.
+    auto with zarith.
+  Qed.
+  Hint Resolve pow2_mod_pos_bound : zarith.
+
   Lemma land_same_r : forall a b, (a & b) & b = a & b.
   Proof.
   intros; apply Z.bits_inj'; intros.