From 4fe4323eddb4f9e0ff9d7f923921f1ae6967a668 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 1 Aug 2016 16:03:28 -0700
Subject: 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
---
 src/Util/ZUtil.v | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

(limited to 'src')

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 :=
-- 
cgit v1.2.3