Better Zmod manipulation

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m45.47s | Total                                           | 1m47.54s || -0m02.07s
----------------------------------------------------------------------------------
0m34.35s | Specific/GF25519                                | 0m32.34s || +0m02.00s
0m08.95s | Specific/GF1305                                 | 0m07.13s || +0m01.81s
0m15.04s | ModularArithmetic/ModularBaseSystemProofs       | 0m15.57s || -0m00.53s
0m11.29s | Experiments/SpecEd25519                         | 0m12.15s || -0m00.86s
0m04.02s | ModularArithmetic/Pow2BaseProofs                | 0m04.32s || -0m00.30s
0m03.76s | ModularArithmetic/Tutorial                      | 0m04.01s || -0m00.25s
0m03.68s | BaseSystemProofs                                | 0m03.81s || -0m00.12s
0m03.15s | ModularArithmetic/ModularBaseSystemOpt          | 0m03.17s || -0m00.02s
0m02.89s | Util/ZUtil                                      | 0m03.01s || -0m00.11s
0m01.51s | ModularArithmetic/PrimeFieldTheorems            | 0m01.64s || -0m00.12s
0m01.51s | ModularArithmetic/ModularArithmeticTheorems     | 0m01.64s || -0m00.12s
0m01.47s | Encoding/PointEncodingPre                       | 0m02.23s || -0m00.76s
0m01.15s | BaseSystem                                      | 0m01.66s || -0m00.51s
0m01.09s | ModularArithmetic/ExtendedBaseVector            | 0m01.19s || -0m00.09s
0m00.99s | ModularArithmetic/BarrettReduction/Z            | 0m01.05s || -0m00.06s
0m00.94s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.04s || -0m00.10s
0m00.88s | Util/NumTheoryUtil                              | 0m01.37s || -0m00.49s
0m00.87s | ModularArithmetic/ModularBaseSystemField        | 0m00.84s || +0m00.03s
0m00.77s | ModularArithmetic/ModularBaseSystemListProofs   | 0m01.21s || -0m00.43s
0m00.71s | Experiments/SpecificCurve25519                  | 0m00.69s || +0m00.02s
0m00.66s | Encoding/ModularWordEncodingTheorems            | 0m00.75s || -0m00.08s
0m00.62s | ModularArithmetic/ModularBaseSystemList         | 0m00.93s || -0m00.31s
0m00.61s | Encoding/ModularWordEncodingPre                 | 0m00.67s || -0m00.06s
0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.99s || -0m00.39s
0m00.60s | Testbit                                         | 0m00.62s || -0m00.02s
0m00.59s | Spec/ModularWordEncoding                        | 0m00.73s || -0m00.14s
0m00.58s | ModularArithmetic/ModularBaseSystem             | 0m00.59s || -0m00.01s
0m00.55s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.56s || -0m00.01s
0m00.45s | ModularArithmetic/Pre                           | 0m00.44s || +0m00.01s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.39s || +0m00.02s
0m00.40s | ModularArithmetic/Pow2Base                      | 0m00.42s || -0m00.01s
0m00.37s | Spec/ModularArithmetic                          | 0m00.38s || -0m00.01s

1 files changed, 50 insertions, 10 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index aa55f373c..f484a86c7 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1223,6 +1223,16 @@ Module Z.
   Qed.
   Hint Rewrite <- add_mod_r using lia : pull_Zmod.
 
+  (** Give alternate names for the next three lemmas, for consistency *)
+  Lemma sub_mod a b n : n <> 0 -> (a - b) mod n = ((a mod n) - (b mod n)) mod n.
+  Proof. auto using Zminus_mod. Qed.
+
+  Lemma sub_mod_l a b n : n <> 0 -> (a - b) mod n = ((a mod n) - b) mod n.
+  Proof. auto using Zminus_mod_idemp_l. Qed.
+
+  Lemma sub_mod_r a b n : n <> 0 -> (a - b) mod n = (a - (b mod n)) mod n.
+  Proof. auto using Zminus_mod_idemp_r. Qed.
+
   Definition NoZMod (x : Z) := True.
   Ltac NoZMod :=
     lazymatch goal with
@@ -1386,22 +1396,34 @@ Ltac push_Zmod :=
   repeat match goal with
          | _ => progress autorewrite with push_Zmod
          | [ |- context[(?x * ?y) mod ?z] ]
-           => rewrite (Z.mul_mod_push x y z) by (Z.NoZMod || lia)
-         | [ |- context[(?x * ?y) mod ?z] ]
-           => rewrite (Z.mul_mod_l_push x y z) by (Z.NoZMod || lia)
-         | [ |- context[(?x * ?y) mod ?z] ]
-           => rewrite (Z.mul_mod_r_push x y z) by (Z.NoZMod || lia)
+           => first [ rewrite (Z.mul_mod_push x y z) by (Z.NoZMod || lia)
+                    | rewrite (Z.mul_mod_l_push x y z) by (Z.NoZMod || lia)
+                    | rewrite (Z.mul_mod_r_push x y z) by (Z.NoZMod || lia) ]
+         | [ |- context[(?x + ?y) mod ?z] ]
+           => first [ rewrite (Z.add_mod_push x y z) by (Z.NoZMod || lia)
+                    | rewrite (Z.add_mod_l_push x y z) by (Z.NoZMod || lia)
+                    | rewrite (Z.add_mod_r_push x y z) by (Z.NoZMod || lia) ]
+         | [ |- context[(?x - ?y) mod ?z] ]
+           => first [ rewrite (Z.sub_mod_push x y z) by (Z.NoZMod || lia)
+                    | rewrite (Z.sub_mod_l_push x y z) by (Z.NoZMod || lia)
+                    | rewrite (Z.sub_mod_r_push x y z) by (Z.NoZMod || lia) ]
          end.
 
 Ltac push_Zmod_hyps :=
   repeat match goal with
          | _ => progress autorewrite with push_Zmod in * |-
          | [ H : context[(?x * ?y) mod ?z] |- _ ]
-           => rewrite (Z.mul_mod_push x y z) in H by (Z.NoZMod || lia)
-         | [ H : context[(?x * ?y) mod ?z] |- _ ]
-           => rewrite (Z.mul_mod_l_push x y z) in H by (Z.NoZMod || lia)
-         | [ H : context[(?x * ?y) mod ?z] |- _ ]
-           => rewrite (Z.mul_mod_r_push x y z) in H by (Z.NoZMod || lia)
+           => first [ rewrite (Z.mul_mod_push x y z) in H by (Z.NoZMod || lia)
+                    | rewrite (Z.mul_mod_l_push x y z) in H by (Z.NoZMod || lia)
+                    | rewrite (Z.mul_mod_r_push x y z) in H by (Z.NoZMod || lia) ]
+         | [ H : context[(?x + ?y) mod ?z] |- _ ]
+           => first [ rewrite (Z.add_mod_push x y z) in H by (Z.NoZMod || lia)
+                    | rewrite (Z.add_mod_l_push x y z) in H by (Z.NoZMod || lia)
+                    | rewrite (Z.add_mod_r_push x y z) in H by (Z.NoZMod || lia) ]
+         | [ H : context[(?x - ?y) mod ?z] |- _ ]
+           => first [ rewrite (Z.sub_mod_push x y z) in H by (Z.NoZMod || lia)
+                    | rewrite (Z.sub_mod_l_push x y z) in H by (Z.NoZMod || lia)
+                    | rewrite (Z.sub_mod_r_push x y z) in H by (Z.NoZMod || lia) ]
          end.
 
 Ltac has_no_mod x z :=
@@ -1420,5 +1442,23 @@ Ltac pull_Zmod :=
          | [ |- context[(?x * (?y mod ?z)) mod ?z] ]
            => has_no_mod x z; has_no_mod y z;
               rewrite <- (Z.mul_mod_r x y z) by lia
+         | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.add_mod x y z) by lia
+         | [ |- context[((?x mod ?z) + ?y) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.add_mod_l x y z) by lia
+         | [ |- context[(?x + (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.add_mod_r x y z) by lia
+         | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.sub_mod x y z) by lia
+         | [ |- context[((?x mod ?z) - ?y) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.sub_mod_l x y z) by lia
+         | [ |- context[(?x - (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.sub_mod_r x y z) by lia
          | _ => progress autorewrite with pull_Zmod
          end.