diff options
author | 2016-08-18 16:32:45 -0700 | |
---|---|---|
committer | 2016-08-18 16:39:08 -0700 | |
commit | a0a81235ccefc03ea44c56de6bbde6bbe2f33c72 (patch) | |
tree | b97a2de89cfe65de8c77fa00c479c395a17d7112 /src | |
parent | bb4c3f387ce5356fb7194708a4d641e1e67b837d (diff) |
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
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/ZUtil.v | 12 |
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. |