More ZUtil

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m40.97s | Total                                           | 1m36.72s || +0m04.25s
----------------------------------------------------------------------------------
0m03.68s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m02.58s || +0m01.10s
0m16.27s | ModularArithmetic/ModularBaseSystemProofs       | 0m15.85s || +0m00.41s
0m14.15s | Specific/GF25519                                | 0m14.02s || +0m00.13s
0m13.88s | Experiments/SpecEd25519                         | 0m13.93s || -0m00.04s
0m04.66s | ModularArithmetic/Tutorial                      | 0m04.20s || +0m00.46s
0m04.51s | BaseSystemProofs                                | 0m03.99s || +0m00.51s
0m04.42s | ModularArithmetic/Pow2BaseProofs                | 0m05.20s || -0m00.78s
0m04.23s | ModularArithmetic/Montgomery/ZProofs            | 0m04.45s || -0m00.21s
0m03.31s | Util/ZUtil                                      | 0m03.43s || -0m00.12s
0m03.27s | Experiments/SpecificCurve25519                  | 0m03.31s || -0m00.04s
0m02.98s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.00s || +0m00.98s
0m02.06s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.02s || +0m00.04s
0m02.03s | ModularArithmetic/ModularArithmeticTheorems     | 0m01.94s || +0m00.08s
0m01.99s | Specific/GF1305                                 | 0m01.93s || +0m00.06s
0m01.81s | BaseSystem                                      | 0m01.21s || +0m00.60s
0m01.61s | Encoding/PointEncodingPre                       | 0m01.47s || +0m00.14s
0m01.33s | Util/NumTheoryUtil                              | 0m00.86s || +0m00.47s
0m01.29s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.06s || +0m00.23s
0m01.25s | ModularArithmetic/ExtendedBaseVector            | 0m01.68s || -0m00.42s
0m01.15s | ModularArithmetic/BarrettReduction/Z            | 0m01.19s || -0m00.04s
0m01.04s | ModularArithmetic/PrimeFieldTheorems            | 0m01.02s || +0m00.02s
0m00.94s | ModularArithmetic/ModularBaseSystemList         | 0m00.59s || +0m00.35s
0m00.93s | Encoding/ModularWordEncodingPre                 | 0m00.61s || +0m00.32s
0m00.89s | ModularArithmetic/ModularBaseSystemField        | 0m00.83s || +0m00.06s
0m00.85s | Encoding/ModularWordEncodingTheorems            | 0m00.96s || -0m00.10s
0m00.79s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.79s || +0m00.00s
0m00.74s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.65s || +0m00.08s
0m00.68s | Testbit                                         | 0m00.60s || +0m00.08s
0m00.64s | Spec/ModularWordEncoding                        | 0m00.62s || +0m00.02s
0m00.59s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.53s || +0m00.05s
0m00.58s | ModularArithmetic/ModularBaseSystem             | 0m00.53s || +0m00.04s
0m00.58s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.62s || -0m00.04s
0m00.53s | ModularArithmetic/Montgomery/Z                  | 0m00.55s || -0m00.02s
0m00.50s | ModularArithmetic/Pre                           | 0m00.71s || -0m00.20s
0m00.42s | ModularArithmetic/Pow2Base                      | 0m00.43s || -0m00.01s
0m00.39s | Spec/ModularArithmetic                          | 0m00.36s || +0m00.03s

1 files changed, 77 insertions, 2 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 7cde7c467..5113cb65f 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -39,6 +39,10 @@ Create HintDb push_Zmul discriminated.
 Create HintDb pull_Zmul discriminated.
 Create HintDb push_Zdiv discriminated.
 Create HintDb pull_Zdiv discriminated.
+Create HintDb push_Zadd discriminated.
+Create HintDb pull_Zadd discriminated.
+Create HintDb push_Zsub discriminated.
+Create HintDb pull_Zsub discriminated.
 Create HintDb pull_Zmod discriminated.
 Create HintDb push_Zmod discriminated.
 Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp.
@@ -47,6 +51,10 @@ Hint Extern 1 => autorewrite with push_Zpow in * : push_Zpow.
 Hint Extern 1 => autorewrite with pull_Zpow in * : pull_Zpow.
 Hint Extern 1 => autorewrite with push_Zmul in * : push_Zmul.
 Hint Extern 1 => autorewrite with pull_Zmul in * : pull_Zmul.
+Hint Extern 1 => autorewrite with push_Zadd in * : push_Zadd.
+Hint Extern 1 => autorewrite with pull_Zadd in * : pull_Zadd.
+Hint Extern 1 => autorewrite with push_Zsub in * : push_Zsub.
+Hint Extern 1 => autorewrite with pull_Zsub in * : pull_Zsub.
 Hint Extern 1 => autorewrite with push_Zdiv in * : push_Zmul.
 Hint Extern 1 => autorewrite with pull_Zdiv in * : pull_Zmul.
 Hint Extern 1 => autorewrite with pull_Zmod in * : pull_Zmod.
@@ -1183,9 +1191,60 @@ Module Z.
     reflexivity.
   Qed.
 
-  Lemma minus_distr_if (b : bool) x y : -(if b then x else y) = if b then -x else -y.
+  Definition opp_distr_if (b : bool) x y : -(if b then x else y) = if b then -x else -y.
   Proof. destruct b; reflexivity. Qed.
-  Hint Rewrite minus_distr_if : push_Zopp.
+  Hint Rewrite opp_distr_if : push_Zopp.
+  Hint Rewrite <- opp_distr_if : pull_Zopp.
+
+  Lemma mul_r_distr_if (b : bool) x y z : z * (if b then x else y) = if b then z * x else z * y.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite mul_r_distr_if : push_Zmul.
+  Hint Rewrite <- mul_r_distr_if : pull_Zmul.
+
+  Lemma mul_l_distr_if (b : bool) x y z : (if b then x else y) * z = if b then x * z else y * z.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite mul_l_distr_if : push_Zmul.
+  Hint Rewrite <- mul_l_distr_if : pull_Zmul.
+
+  Lemma add_r_distr_if (b : bool) x y z : z + (if b then x else y) = if b then z + x else z + y.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite add_r_distr_if : push_Zadd.
+  Hint Rewrite <- add_r_distr_if : pull_Zadd.
+
+  Lemma add_l_distr_if (b : bool) x y z : (if b then x else y) + z = if b then x + z else y + z.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite add_l_distr_if : push_Zadd.
+  Hint Rewrite <- add_l_distr_if : pull_Zadd.
+
+  Lemma sub_r_distr_if (b : bool) x y z : z - (if b then x else y) = if b then z - x else z - y.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite sub_r_distr_if : push_Zsub.
+  Hint Rewrite <- sub_r_distr_if : pull_Zsub.
+
+  Lemma sub_l_distr_if (b : bool) x y z : (if b then x else y) - z = if b then x - z else y - z.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite sub_l_distr_if : push_Zsub.
+  Hint Rewrite <- sub_l_distr_if : pull_Zsub.
+
+  Lemma div_r_distr_if (b : bool) x y z : z / (if b then x else y) = if b then z / x else z / y.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite div_r_distr_if : push_Zdiv.
+  Hint Rewrite <- div_r_distr_if : pull_Zdiv.
+
+  Lemma div_l_distr_if (b : bool) x y z : (if b then x else y) / z = if b then x / z else y / z.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite div_l_distr_if : push_Zdiv.
+  Hint Rewrite <- div_l_distr_if : pull_Zdiv.
+
+  Lemma mod_r_distr_if (b : bool) x y z : z mod (if b then x else y) = if b then z mod x else z mod y.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite mod_r_distr_if : push_Zmod.
+  Hint Rewrite <- mod_r_distr_if : pull_Zmod.
+
+  Lemma mod_l_distr_if (b : bool) x y z : (if b then x else y) mod z = if b then x mod z else y mod z.
+  Proof. destruct b; reflexivity. Qed.
+  Hint Rewrite mod_l_distr_if : push_Zmod.
+  Hint Rewrite <- mod_l_distr_if : pull_Zmod.
 
   Lemma minus_minus_one : - -1 = 1.
   Proof. reflexivity. Qed.
@@ -1344,6 +1403,22 @@ Module Z.
   Proof. intros; rewrite (div_between 1) by lia; reflexivity. Qed.
   Hint Rewrite div_between_1 using zutil_arith : zsimplify.
 
+  Lemma leb_add_same x y : (x <=? y + x) = (0 <=? y).
+  Proof. destruct (x <=? y + x) eqn:?, (0 <=? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed.
+  Hint Rewrite leb_add_same : zsimplify.
+
+  Lemma ltb_add_same x y : (x <? y + x) = (0 <? y).
+  Proof. destruct (x <? y + x) eqn:?, (0 <? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed.
+  Hint Rewrite ltb_add_same : zsimplify.
+
+  Lemma geb_add_same x y : (x >=? y + x) = (0 >=? y).
+  Proof. destruct (x >=? y + x) eqn:?, (0 >=? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed.
+  Hint Rewrite geb_add_same : zsimplify.
+
+  Lemma gtb_add_same x y : (x >? y + x) = (0 >? y).
+  Proof. destruct (x >? y + x) eqn:?, (0 >? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed.
+  Hint Rewrite gtb_add_same : zsimplify.
+
   Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y.
   Proof. lia. Qed.
   Hint Rewrite simplify_twice_sub_sub : zsimplify.