diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-01 16:03:28 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-01 16:09:13 -0700 |
| commit | 4fe4323eddb4f9e0ff9d7f923921f1ae6967a668 (patch) | |
| tree | 29eab5bc6b8742d0fa01a2528b1963f827eb6592 /src | |
| parent | 997d95a9c402aff7a13898a396c68b3d620a165e (diff) | |
Make Z.ltb_to_lt more powerful
Now it handles <=?, >?, >=?, not just <?.
After | File Name | Before || Change
----------------------------------------------------------------------------------
1m57.90s | Total | 1m58.48s || -0m00.57s
----------------------------------------------------------------------------------
0m15.49s | ModularArithmetic/ModularBaseSystemProofs | 0m21.82s || -0m06.33s
0m37.86s | Specific/GF25519 | 0m33.76s || +0m04.10s
0m11.93s | Specific/GF1305 | 0m07.46s || +0m04.46s
0m04.09s | ModularArithmetic/Pow2BaseProofs | 0m05.29s || -0m01.20s
0m11.54s | Experiments/SpecEd25519 | 0m11.71s || -0m00.17s
0m04.99s | ModularArithmetic/Tutorial | 0m04.03s || +0m00.96s
0m03.87s | BaseSystemProofs | 0m03.99s || -0m00.12s
0m03.30s | ModularArithmetic/ModularBaseSystemOpt | 0m03.27s || +0m00.02s
0m02.96s | Util/ZUtil | 0m03.03s || -0m00.06s
0m01.71s | Encoding/PointEncodingPre | 0m01.74s || -0m00.03s
0m01.70s | ModularArithmetic/ExtendedBaseVector | 0m01.13s || +0m00.57s
0m01.68s | ModularArithmetic/PrimeFieldTheorems | 0m01.64s || +0m00.04s
0m01.58s | ModularArithmetic/ModularArithmeticTheorems | 0m01.79s || -0m00.20s
0m01.39s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.39s || +0m00.00s
0m01.21s | BaseSystem | 0m01.84s || -0m00.63s
0m01.00s | ModularArithmetic/BarrettReduction/Z | 0m01.44s || -0m00.43s
0m00.97s | Testbit | 0m00.96s || +0m00.01s
0m00.96s | ModularArithmetic/ModularBaseSystemField | 0m00.94s || +0m00.02s
0m00.95s | Encoding/ModularWordEncodingPre | 0m00.97s || -0m00.02s
0m00.94s | Util/NumTheoryUtil | 0m01.39s || -0m00.44s
0m00.84s | Spec/ModularWordEncoding | 0m00.88s || -0m00.04s
0m00.84s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.92s || -0m00.08s
0m00.76s | Encoding/ModularWordEncodingTheorems | 0m00.96s || -0m00.19s
0m00.73s | Experiments/SpecificCurve25519 | 0m01.02s || -0m00.29s
0m00.69s | ModularArithmetic/ModularBaseSystemList | 0m00.58s || +0m00.10s
0m00.67s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.90s || -0m00.23s
0m00.59s | ModularArithmetic/Pre | 0m00.49s || +0m00.09s
0m00.59s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.86s || -0m00.27s
0m00.58s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.60s || -0m00.02s
0m00.57s | ModularArithmetic/ModularBaseSystem | 0m00.66s || -0m00.09s
0m00.52s | Spec/ModularArithmetic | 0m00.41s || +0m00.11s
0m00.41s | ModularArithmetic/Pow2Base | 0m00.62s || -0m00.21s
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZUtil.v | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 64dfce99b..3ab0b25f7 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -620,14 +620,23 @@ Module Z. etransitivity; [ apply IHl | apply Z.le_max_r ]. Qed. + Ltac ltb_to_lt_with_hyp H lem := + let H' := fresh in + rename H into H'; + pose proof lem as H; + rewrite H' in H; + clear H'. + Ltac ltb_to_lt := repeat match goal with | [ H : (?x <? ?y) = ?b |- _ ] - => let H' := fresh in - rename H into H'; - pose proof (Zlt_cases x y) as H; - rewrite H' in H; - clear H' + => ltb_to_lt_with_hyp H (Zlt_cases x y) + | [ H : (?x <=? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zle_cases x y) + | [ H : (?x >? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zgt_cases x y) + | [ H : (?x >=? ?y) = ?b |- _ ] + => ltb_to_lt_with_hyp H (Zge_cases x y) end. Ltac compare_to_sgn := |