Split off pull_Zmod, push_Zmod from ZUtil

6 files changed, 221 insertions, 205 deletions

diff --git a/_CoqProject b/_CoqProject
index 7d440951a..d62d571b6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -312,6 +312,7 @@ src/Util/ZUtil/Hints/Core.v
 src/Util/ZUtil/Hints/PullPush.v
 src/Util/ZUtil/Hints/ZArith.v
 src/Util/ZUtil/Hints/Ztestbit.v
+src/Util/ZUtil/Modulo/PullPush.v
 src/Util/ZUtil/Tactics/CompareToSgn.v
 src/Util/ZUtil/Tactics/DivModToQuotRem.v
 src/Util/ZUtil/Tactics/DivideExistsMul.v
@@ -319,11 +320,13 @@ src/Util/ZUtil/Tactics/LinearSubstitute.v
 src/Util/ZUtil/Tactics/LtbToLt.v
 src/Util/ZUtil/Tactics/PeelLe.v
 src/Util/ZUtil/Tactics/PrimeBound.v
+src/Util/ZUtil/Tactics/PullPush.v
 src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
 src/Util/ZUtil/Tactics/RewriteModSmall.v
 src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
 src/Util/ZUtil/Tactics/ZeroBounds.v
 src/Util/ZUtil/Tactics/Ztestbit.v
+src/Util/ZUtil/Tactics/PullPush/Modulo.v
 src/Util/ZUtil/ZSimplify/Autogenerated.v
 src/Util/ZUtil/ZSimplify/Core.v
 src/Util/ZUtil/ZSimplify/Simple.v
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 91e42598e..936b4ce76 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -17,6 +17,7 @@ Require Export Crypto.Util.ZUtil.EquivModulo.
 Require Export Crypto.Util.ZUtil.Hints.
 Require Export Crypto.Util.ZUtil.Land.
 Require Export Crypto.Util.ZUtil.Modulo.
+Require Export Crypto.Util.ZUtil.Modulo.PullPush.
 Require Export Crypto.Util.ZUtil.Morphisms.
 Require Export Crypto.Util.ZUtil.Notations.
 Require Export Crypto.Util.ZUtil.Pow2Mod.
@@ -924,16 +925,6 @@ Module Z.
   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 div_add_exact x y d : d <> 0 -> x mod d = 0 -> (x + y) / d = x / d + y / d.
   Proof.
     intros; rewrite (Z_div_exact_full_2 x d) at 1 by assumption.
@@ -941,121 +932,6 @@ Module Z.
   Qed.
   Hint Rewrite div_add_exact using zutil_arith : zsimplify.
 
-  (** Version without the [n <> 0] assumption *)
-  Lemma mul_mod_full a b n : (a * b) mod n = ((a mod n) * (b mod n)) mod n.
-  Proof. auto using Zmult_mod. Qed.
-  Hint Rewrite <- mul_mod_full : pull_Zmod.
-  Hint Resolve mul_mod_full : zarith.
-
-  Lemma mul_mod_l a b n : (a * b) mod n = ((a mod n) * b) mod n.
-  Proof.
-    intros; rewrite (mul_mod_full a b), (mul_mod_full (a mod n) b).
-    autorewrite with zsimplify; reflexivity.
-  Qed.
-  Hint Rewrite <- mul_mod_l : pull_Zmod.
-  Hint Resolve mul_mod_l : zarith.
-
-  Lemma mul_mod_r a b n : (a * b) mod n = (a * (b mod n)) mod n.
-  Proof.
-    intros; rewrite (mul_mod_full a b), (mul_mod_full a (b mod n)).
-    autorewrite with zsimplify; reflexivity.
-  Qed.
-  Hint Rewrite <- mul_mod_r : pull_Zmod.
-  Hint Resolve mul_mod_r : zarith.
-
-  Lemma add_mod_full a b n : (a + b) mod n = ((a mod n) + (b mod n)) mod n.
-  Proof. auto using Zplus_mod. Qed.
-  Hint Rewrite <- add_mod_full : pull_Zmod.
-  Hint Resolve add_mod_full : zarith.
-
-  Lemma add_mod_l a b n : (a + b) mod n = ((a mod n) + b) mod n.
-  Proof.
-    intros; rewrite (add_mod_full a b), (add_mod_full (a mod n) b).
-    autorewrite with zsimplify; reflexivity.
-  Qed.
-  Hint Rewrite <- add_mod_l : pull_Zmod.
-  Hint Resolve add_mod_l : zarith.
-
-  Lemma add_mod_r a b n : (a + b) mod n = (a + (b mod n)) mod n.
-  Proof.
-    intros; rewrite (add_mod_full a b), (add_mod_full a (b mod n)).
-    autorewrite with zsimplify; reflexivity.
-  Qed.
-  Hint Rewrite <- add_mod_r : pull_Zmod.
-  Hint Resolve add_mod_r : zarith.
-
-  Lemma opp_mod_mod a n : (-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 : pull_Zmod.
-  Hint Resolve opp_mod_mod : zarith.
-
-  (** Give alternate names for the next three lemmas, for consistency *)
-  Lemma sub_mod_full a b n : (a - b) mod n = ((a mod n) - (b mod n)) mod n.
-  Proof. auto using Zminus_mod. Qed.
-  Hint Rewrite <- sub_mod_full : pull_Zmod.
-  Hint Resolve sub_mod_full : zarith.
-
-  Lemma sub_mod_l a b n : (a - b) mod n = ((a mod n) - b) mod n.
-  Proof. auto using Zminus_mod_idemp_l. Qed.
-  Hint Rewrite <- sub_mod_l : pull_Zmod.
-  Hint Resolve sub_mod_l : zarith.
-
-  Lemma sub_mod_r a b n : (a - b) mod n = (a - (b mod n)) mod n.
-  Proof. auto using Zminus_mod_idemp_r. Qed.
-  Hint Rewrite <- sub_mod_r : pull_Zmod.
-  Hint Resolve sub_mod_r : zarith.
-
-  Definition NoZMod (x : Z) := True.
-  Ltac NoZMod :=
-    lazymatch goal with
-    | [ |- NoZMod (?x mod ?y) ] => fail 0 "Goal has" x "mod" y
-    | [ |- NoZMod _ ] => constructor
-    end.
-
-  Lemma mul_mod_push a b n : NoZMod a -> NoZMod b -> (a * b) mod n = ((a mod n) * (b mod n)) mod n.
-  Proof. intros; apply mul_mod_full; assumption. Qed.
-  Hint Rewrite mul_mod_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma add_mod_push a b n : NoZMod a -> NoZMod b -> (a + b) mod n = ((a mod n) + (b mod n)) mod n.
-  Proof. intros; apply add_mod_full; assumption. Qed.
-  Hint Rewrite add_mod_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma mul_mod_l_push a b n : NoZMod a -> (a * b) mod n = ((a mod n) * b) mod n.
-  Proof. intros; apply mul_mod_l; assumption. Qed.
-  Hint Rewrite mul_mod_l_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma mul_mod_r_push a b n : NoZMod b -> (a * b) mod n = (a * (b mod n)) mod n.
-  Proof. intros; apply mul_mod_r; assumption. Qed.
-  Hint Rewrite mul_mod_r_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma add_mod_l_push a b n : NoZMod a -> (a + b) mod n = ((a mod n) + b) mod n.
-  Proof. intros; apply add_mod_l; assumption. Qed.
-  Hint Rewrite add_mod_l_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma add_mod_r_push a b n : NoZMod b -> (a + b) mod n = (a + (b mod n)) mod n.
-  Proof. intros; apply add_mod_r; assumption. Qed.
-  Hint Rewrite add_mod_r_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma sub_mod_push a b n : NoZMod a -> NoZMod b -> (a - b) mod n = ((a mod n) - (b mod n)) mod n.
-  Proof. intros; apply Zminus_mod; assumption. Qed.
-  Hint Rewrite sub_mod_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma sub_mod_l_push a b n : NoZMod a -> (a - b) mod n = ((a mod n) - b) mod n.
-  Proof. intros; symmetry; apply Zminus_mod_idemp_l; assumption. Qed.
-  Hint Rewrite sub_mod_l_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma sub_mod_r_push a b n : NoZMod b -> (a - b) mod n = (a - (b mod n)) mod n.
-  Proof. intros; symmetry; apply Zminus_mod_idemp_r; assumption. Qed.
-  Hint Rewrite sub_mod_r_push using solve [ NoZMod ] : push_Zmod.
-
-  Lemma opp_mod_mod_push a n : 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 ] : 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.
@@ -1703,83 +1579,3 @@ Module Export BoundsTactics.
   Ltac prime_bound := Z.prime_bound.
   Ltac zero_bounds := Z.zero_bounds.
 End BoundsTactics.
-
-Ltac push_Zmod :=
-  repeat match goal with
-         | _ => progress autorewrite with push_Zmod
-         | [ |- context[(?x * ?y) mod ?z] ]
-           => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod
-                    | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod
-                    | rewrite (Z.mul_mod_r_push x y z) by Z.NoZMod ]
-         | [ |- context[(?x + ?y) mod ?z] ]
-           => first [ rewrite (Z.add_mod_push x y z) by Z.NoZMod
-                    | rewrite (Z.add_mod_l_push x y z) by Z.NoZMod
-                    | rewrite (Z.add_mod_r_push x y z) by Z.NoZMod ]
-         | [ |- context[(?x - ?y) mod ?z] ]
-           => first [ rewrite (Z.sub_mod_push x y z) by Z.NoZMod
-                    | rewrite (Z.sub_mod_l_push x y z) by Z.NoZMod
-                    | rewrite (Z.sub_mod_r_push x y z) by Z.NoZMod ]
-         | [ |- context[(-?y) mod ?z] ]
-           => rewrite (Z.opp_mod_mod_push y z) by Z.NoZMod
-         end.
-
-Ltac push_Zmod_hyps :=
-  repeat match goal with
-         | _ => progress autorewrite with push_Zmod in * |-
-         | [ H : context[(?x * ?y) mod ?z] |- _ ]
-           => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod
-                    | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod
-                    | rewrite (Z.mul_mod_r_push x y z) in H by Z.NoZMod ]
-         | [ H : context[(?x + ?y) mod ?z] |- _ ]
-           => first [ rewrite (Z.add_mod_push x y z) in H by Z.NoZMod
-                    | rewrite (Z.add_mod_l_push x y z) in H by Z.NoZMod
-                    | rewrite (Z.add_mod_r_push x y z) in H by Z.NoZMod ]
-         | [ H : context[(?x - ?y) mod ?z] |- _ ]
-           => first [ rewrite (Z.sub_mod_push x y z) in H by Z.NoZMod
-                    | rewrite (Z.sub_mod_l_push x y z) in H by Z.NoZMod
-                    | rewrite (Z.sub_mod_r_push x y z) in H by Z.NoZMod ]
-         | [ H : context[(-?y) mod ?z] |- _ ]
-           => rewrite (Z.opp_mod_mod_push y z) in H by Z.NoZMod
-         end.
-
-Ltac has_no_mod x z :=
-  lazymatch x with
-  | context[_ mod z] => fail
-  | _ => idtac
-  end.
-Ltac pull_Zmod :=
-  repeat match goal with
-         | [ |- context[((?x mod ?z) * (?y mod ?z)) mod ?z] ]
-           => has_no_mod x z; has_no_mod y z;
-              rewrite <- (Z.mul_mod_full x y z)
-         | [ |- context[((?x mod ?z) * ?y) mod ?z] ]
-           => has_no_mod x z; has_no_mod y z;
-              rewrite <- (Z.mul_mod_l x y z)
-         | [ |- 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)
-         | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ]
-           => has_no_mod x z; has_no_mod y z;
-              rewrite <- (Z.add_mod_full x y z)
-         | [ |- 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)
-         | [ |- 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)
-         | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ]
-           => has_no_mod x z; has_no_mod y z;
-              rewrite <- (Z.sub_mod_full x y z)
-         | [ |- 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)
-         | [ |- 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)
-         | [ |- context[(((-?y) mod ?z)) mod ?z] ]
-           => has_no_mod y z;
-              rewrite <- (Z.opp_mod_mod y z)
-         | [ |- context[(?x mod ?z) mod ?z] ]
-           => rewrite (Zmod_mod x z)
-         | _ => progress autorewrite with pull_Zmod
-         end.
diff --git a/src/Util/ZUtil/Modulo/PullPush.v b/src/Util/ZUtil/Modulo/PullPush.v
new file mode 100644
index 000000000..7e3a9b46a
--- /dev/null
+++ b/src/Util/ZUtil/Modulo/PullPush.v
@@ -0,0 +1,131 @@
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.ZSimplify.Core.
+Local Open Scope Z_scope.
+
+Module Z.
+  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.
+
+  (** Version without the [n <> 0] assumption *)
+  Lemma mul_mod_full a b n : (a * b) mod n = ((a mod n) * (b mod n)) mod n.
+  Proof. auto using Zmult_mod. Qed.
+  Hint Rewrite <- mul_mod_full : pull_Zmod.
+  Hint Resolve mul_mod_full : zarith.
+
+  Lemma mul_mod_l a b n : (a * b) mod n = ((a mod n) * b) mod n.
+  Proof.
+    intros; rewrite (mul_mod_full a b), (mul_mod_full (a mod n) b).
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+  Hint Rewrite <- mul_mod_l : pull_Zmod.
+  Hint Resolve mul_mod_l : zarith.
+
+  Lemma mul_mod_r a b n : (a * b) mod n = (a * (b mod n)) mod n.
+  Proof.
+    intros; rewrite (mul_mod_full a b), (mul_mod_full a (b mod n)).
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+  Hint Rewrite <- mul_mod_r : pull_Zmod.
+  Hint Resolve mul_mod_r : zarith.
+
+  Lemma add_mod_full a b n : (a + b) mod n = ((a mod n) + (b mod n)) mod n.
+  Proof. auto using Zplus_mod. Qed.
+  Hint Rewrite <- add_mod_full : pull_Zmod.
+  Hint Resolve add_mod_full : zarith.
+
+  Lemma add_mod_l a b n : (a + b) mod n = ((a mod n) + b) mod n.
+  Proof.
+    intros; rewrite (add_mod_full a b), (add_mod_full (a mod n) b).
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+  Hint Rewrite <- add_mod_l : pull_Zmod.
+  Hint Resolve add_mod_l : zarith.
+
+  Lemma add_mod_r a b n : (a + b) mod n = (a + (b mod n)) mod n.
+  Proof.
+    intros; rewrite (add_mod_full a b), (add_mod_full a (b mod n)).
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+  Hint Rewrite <- add_mod_r : pull_Zmod.
+  Hint Resolve add_mod_r : zarith.
+
+  Lemma opp_mod_mod a n : (-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 : pull_Zmod.
+  Hint Resolve opp_mod_mod : zarith.
+
+  (** Give alternate names for the next three lemmas, for consistency *)
+  Lemma sub_mod_full a b n : (a - b) mod n = ((a mod n) - (b mod n)) mod n.
+  Proof. auto using Zminus_mod. Qed.
+  Hint Rewrite <- sub_mod_full : pull_Zmod.
+  Hint Resolve sub_mod_full : zarith.
+
+  Lemma sub_mod_l a b n : (a - b) mod n = ((a mod n) - b) mod n.
+  Proof. auto using Zminus_mod_idemp_l. Qed.
+  Hint Rewrite <- sub_mod_l : pull_Zmod.
+  Hint Resolve sub_mod_l : zarith.
+
+  Lemma sub_mod_r a b n : (a - b) mod n = (a - (b mod n)) mod n.
+  Proof. auto using Zminus_mod_idemp_r. Qed.
+  Hint Rewrite <- sub_mod_r : pull_Zmod.
+  Hint Resolve sub_mod_r : zarith.
+
+  Definition NoZMod (x : Z) := True.
+  Ltac NoZMod :=
+    lazymatch goal with
+    | [ |- NoZMod (?x mod ?y) ] => fail 0 "Goal has" x "mod" y
+    | [ |- NoZMod _ ] => constructor
+    end.
+
+  Lemma mul_mod_push a b n : NoZMod a -> NoZMod b -> (a * b) mod n = ((a mod n) * (b mod n)) mod n.
+  Proof. intros; apply mul_mod_full; assumption. Qed.
+  Hint Rewrite mul_mod_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma add_mod_push a b n : NoZMod a -> NoZMod b -> (a + b) mod n = ((a mod n) + (b mod n)) mod n.
+  Proof. intros; apply add_mod_full; assumption. Qed.
+  Hint Rewrite add_mod_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma mul_mod_l_push a b n : NoZMod a -> (a * b) mod n = ((a mod n) * b) mod n.
+  Proof. intros; apply mul_mod_l; assumption. Qed.
+  Hint Rewrite mul_mod_l_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma mul_mod_r_push a b n : NoZMod b -> (a * b) mod n = (a * (b mod n)) mod n.
+  Proof. intros; apply mul_mod_r; assumption. Qed.
+  Hint Rewrite mul_mod_r_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma add_mod_l_push a b n : NoZMod a -> (a + b) mod n = ((a mod n) + b) mod n.
+  Proof. intros; apply add_mod_l; assumption. Qed.
+  Hint Rewrite add_mod_l_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma add_mod_r_push a b n : NoZMod b -> (a + b) mod n = (a + (b mod n)) mod n.
+  Proof. intros; apply add_mod_r; assumption. Qed.
+  Hint Rewrite add_mod_r_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma sub_mod_push a b n : NoZMod a -> NoZMod b -> (a - b) mod n = ((a mod n) - (b mod n)) mod n.
+  Proof. intros; apply Zminus_mod; assumption. Qed.
+  Hint Rewrite sub_mod_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma sub_mod_l_push a b n : NoZMod a -> (a - b) mod n = ((a mod n) - b) mod n.
+  Proof. intros; symmetry; apply Zminus_mod_idemp_l; assumption. Qed.
+  Hint Rewrite sub_mod_l_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma sub_mod_r_push a b n : NoZMod b -> (a - b) mod n = (a - (b mod n)) mod n.
+  Proof. intros; symmetry; apply Zminus_mod_idemp_r; assumption. Qed.
+  Hint Rewrite sub_mod_r_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma opp_mod_mod_push a n : 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 ] : push_Zmod.
+End Z.
diff --git a/src/Util/ZUtil/Tactics.v b/src/Util/ZUtil/Tactics.v
index 7dfb8ff46..38808e6c7 100644
--- a/src/Util/ZUtil/Tactics.v
+++ b/src/Util/ZUtil/Tactics.v
@@ -5,6 +5,7 @@ Require Export Crypto.Util.ZUtil.Tactics.LinearSubstitute.
 Require Export Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Export Crypto.Util.ZUtil.Tactics.PeelLe.
 Require Export Crypto.Util.ZUtil.Tactics.PrimeBound.
+Require Export Crypto.Util.ZUtil.Tactics.PullPush.
 Require Export Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
 Require Export Crypto.Util.ZUtil.Tactics.RewriteModSmall.
 Require Export Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
diff --git a/src/Util/ZUtil/Tactics/PullPush.v b/src/Util/ZUtil/Tactics/PullPush.v
new file mode 100644
index 000000000..4f40ea9e9
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/PullPush.v
@@ -0,0 +1 @@
+Require Export Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
diff --git a/src/Util/ZUtil/Tactics/PullPush/Modulo.v b/src/Util/ZUtil/Tactics/PullPush/Modulo.v
new file mode 100644
index 000000000..a2502aeea
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/PullPush/Modulo.v
@@ -0,0 +1,84 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Modulo.PullPush.
+Local Open Scope Z_scope.
+
+Ltac push_Zmod :=
+  repeat match goal with
+         | _ => progress autorewrite with push_Zmod
+         | [ |- context[(?x * ?y) mod ?z] ]
+           => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod
+                    | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod
+                    | rewrite (Z.mul_mod_r_push x y z) by Z.NoZMod ]
+         | [ |- context[(?x + ?y) mod ?z] ]
+           => first [ rewrite (Z.add_mod_push x y z) by Z.NoZMod
+                    | rewrite (Z.add_mod_l_push x y z) by Z.NoZMod
+                    | rewrite (Z.add_mod_r_push x y z) by Z.NoZMod ]
+         | [ |- context[(?x - ?y) mod ?z] ]
+           => first [ rewrite (Z.sub_mod_push x y z) by Z.NoZMod
+                    | rewrite (Z.sub_mod_l_push x y z) by Z.NoZMod
+                    | rewrite (Z.sub_mod_r_push x y z) by Z.NoZMod ]
+         | [ |- context[(-?y) mod ?z] ]
+           => rewrite (Z.opp_mod_mod_push y z) by Z.NoZMod
+         end.
+
+Ltac push_Zmod_hyps :=
+  repeat match goal with
+         | _ => progress autorewrite with push_Zmod in * |-
+         | [ H : context[(?x * ?y) mod ?z] |- _ ]
+           => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod
+                    | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod
+                    | rewrite (Z.mul_mod_r_push x y z) in H by Z.NoZMod ]
+         | [ H : context[(?x + ?y) mod ?z] |- _ ]
+           => first [ rewrite (Z.add_mod_push x y z) in H by Z.NoZMod
+                    | rewrite (Z.add_mod_l_push x y z) in H by Z.NoZMod
+                    | rewrite (Z.add_mod_r_push x y z) in H by Z.NoZMod ]
+         | [ H : context[(?x - ?y) mod ?z] |- _ ]
+           => first [ rewrite (Z.sub_mod_push x y z) in H by Z.NoZMod
+                    | rewrite (Z.sub_mod_l_push x y z) in H by Z.NoZMod
+                    | rewrite (Z.sub_mod_r_push x y z) in H by Z.NoZMod ]
+         | [ H : context[(-?y) mod ?z] |- _ ]
+           => rewrite (Z.opp_mod_mod_push y z) in H by Z.NoZMod
+         end.
+
+Ltac has_no_mod x z :=
+  lazymatch x with
+  | context[_ mod z] => fail
+  | _ => idtac
+  end.
+Ltac pull_Zmod :=
+  repeat match goal with
+         | [ |- context[((?x mod ?z) * (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.mul_mod_full x y z)
+         | [ |- context[((?x mod ?z) * ?y) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.mul_mod_l x y z)
+         | [ |- 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)
+         | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.add_mod_full x y z)
+         | [ |- 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)
+         | [ |- 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)
+         | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ]
+           => has_no_mod x z; has_no_mod y z;
+              rewrite <- (Z.sub_mod_full x y z)
+         | [ |- 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)
+         | [ |- 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)
+         | [ |- context[(((-?y) mod ?z)) mod ?z] ]
+           => has_no_mod y z;
+              rewrite <- (Z.opp_mod_mod y z)
+         | [ |- context[(?x mod ?z) mod ?z] ]
+           => rewrite (Zmod_mod x z)
+         | _ => progress autorewrite with pull_Zmod
+         end.