Handle [((-_) mod n) mod n] in {push,pull}_Zmod

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m59.43s | Total                                           | 1m52.16s || +0m07.26s
----------------------------------------------------------------------------------
0m37.54s | Specific/GF25519                                | 0m32.80s || +0m04.74s
0m12.08s | Specific/GF1305                                 | 0m07.23s || +0m04.84s
0m15.68s | ModularArithmetic/ModularBaseSystemProofs       | 0m15.82s || -0m00.14s
0m11.97s | Experiments/SpecEd25519                         | 0m12.35s || -0m00.37s
0m04.08s | ModularArithmetic/Pow2BaseProofs                | 0m04.86s || -0m00.78s
0m03.85s | BaseSystemProofs                                | 0m03.90s || -0m00.04s
0m03.76s | ModularArithmetic/Tutorial                      | 0m04.07s || -0m00.31s
0m03.30s | ModularArithmetic/ModularBaseSystemOpt          | 0m03.28s || +0m00.02s
0m03.14s | Util/ZUtil                                      | 0m02.96s || +0m00.18s
0m02.43s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m02.48s || -0m00.04s
0m01.91s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m01.87s || +0m00.03s
0m01.66s | Encoding/PointEncodingPre                       | 0m02.19s || -0m00.53s
0m01.62s | ModularArithmetic/ModularArithmeticTheorems     | 0m01.77s || -0m00.14s
0m01.57s | ModularArithmetic/PrimeFieldTheorems            | 0m01.59s || -0m00.02s
0m01.23s | ModularArithmetic/ExtendedBaseVector            | 0m01.18s || +0m00.05s
0m01.16s | BaseSystem                                      | 0m01.18s || -0m00.02s
0m01.04s | ModularArithmetic/BarrettReduction/Z            | 0m01.07s || -0m00.03s
0m00.96s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.00s || -0m00.04s
0m00.91s | ModularArithmetic/ModularBaseSystemList         | 0m00.59s || +0m00.32s
0m00.88s | ModularArithmetic/ModularBaseSystemField        | 0m00.94s || -0m00.05s
0m00.88s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.83s || +0m00.05s
0m00.87s | Util/NumTheoryUtil                              | 0m00.89s || -0m00.02s
0m00.79s | ModularArithmetic/ModularBaseSystem             | 0m00.55s || +0m00.24s
0m00.70s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.61s || +0m00.08s
0m00.69s | Experiments/SpecificCurve25519                  | 0m00.67s || +0m00.01s
0m00.68s | Testbit                                         | 0m00.69s || -0m00.00s
0m00.62s | Encoding/ModularWordEncodingTheorems            | 0m00.72s || -0m00.09s
0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.63s || -0m00.02s
0m00.60s | Encoding/ModularWordEncodingPre                 | 0m00.97s || -0m00.37s
0m00.59s | Spec/ModularWordEncoding                        | 0m00.89s || -0m00.30s
0m00.46s | ModularArithmetic/Pre                           | 0m00.42s || +0m00.04s
0m00.43s | ModularArithmetic/Pow2Base                      | 0m00.42s || +0m00.01s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.40s || +0m00.00s
0m00.33s | Spec/ModularArithmetic                          | 0m00.35s || -0m00.01s

1 files changed, 21 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 585841719..6c979c3e1 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -25,7 +25,7 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z
     this database. *)
 Create HintDb zsimplify discriminated.
 Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r Z_mod_same_full Z.sub_simpl_r Z.sub_simpl_l Z.add_opp_diag_r Z.add_opp_diag_l Zmod_0_l Z.add_simpl_r Z.add_simpl_l Z.opp_0 Zmod_0_r : zsimplify.
-Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small using lia : zsimplify.
+Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l Z.mod_mod Z.mod_small Z_mod_zero_opp_full using lia : zsimplify.
 Hint Rewrite <- Z.opp_eq_mul_m1 : zsimplify.
 
 (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *)
@@ -63,6 +63,7 @@ Hint Rewrite Z.div_div using lia : pull_Zdiv.
 Hint Rewrite <- Z.div_div using lia : push_Zdiv.
 Hint Rewrite <- Z.mul_mod Z.add_mod Zminus_mod using lia : pull_Zmod.
 Hint Rewrite Zminus_mod_idemp_l Zminus_mod_idemp_r : pull_Zmod.
+Hint Rewrite Z_mod_nz_opp_full using lia : push_Zmod.
 
 (** For the occasional lemma that can remove the use of [Z.div] *)
 Create HintDb zstrip_div.
@@ -1223,6 +1224,14 @@ Module Z.
   Qed.
   Hint Rewrite <- add_mod_r using lia : pull_Zmod.
 
+  Lemma opp_mod_mod a n : n <> 0 -> (-a) mod n = (-(a mod n)) mod n.
+  Proof.
+    intros; destruct (Z_zerop (a mod n)) as [H'|H']; [ rewrite H' | ];
+      [ | rewrite !Z_mod_nz_opp_full ];
+      autorewrite with zsimplify; lia.
+  Qed.
+  Hint Rewrite <- opp_mod_mod 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.
@@ -1276,6 +1285,10 @@ Module Z.
   Proof. intros; symmetry; apply Zminus_mod_idemp_r; assumption. Qed.
   Hint Rewrite sub_mod_r_push using solve [ NoZMod | lia ] : push_Zmod.
 
+  Lemma opp_mod_mod_push a n : n <> 0 -> NoZMod a -> (-a) mod n = (-(a mod n)) mod n.
+  Proof. intros; apply opp_mod_mod; assumption. Qed.
+  Hint Rewrite opp_mod_mod using solve [ NoZMod | lia ] : push_Zmod.
+
   Lemma sub_mod_mod_0 x d : (x - x mod d) mod d = 0.
   Proof.
     destruct (Z_zerop d); subst; autorewrite with push_Zmod zsimplify; reflexivity.
@@ -1494,6 +1507,8 @@ Ltac push_Zmod :=
            => 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) ]
+         | [ |- context[(-?y) mod ?z] ]
+           => rewrite (Z.opp_mod_mod_push y z) by (Z.NoZMod || lia)
          end.
 
 Ltac push_Zmod_hyps :=
@@ -1511,6 +1526,8 @@ Ltac push_Zmod_hyps :=
            => 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) ]
+         | [ H : context[(-?y) mod ?z] |- _ ]
+           => rewrite (Z.opp_mod_mod_push y z) in H by (Z.NoZMod || lia)
          end.
 
 Ltac has_no_mod x z :=
@@ -1547,5 +1564,8 @@ Ltac pull_Zmod :=
          | [ |- 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
+         | [ |- context[(((-?y) mod ?z)) mod ?z] ]
+           => has_no_mod y z;
+              rewrite <- (Z.opp_mod_mod y z) by lia
          | _ => progress autorewrite with pull_Zmod
          end.