Add lnot mod pull/push lemmas

1 files changed, 11 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Modulo/PullPush.v b/src/Util/ZUtil/Modulo/PullPush.v
index a284e61c9..dbbe98975 100644
--- a/src/Util/ZUtil/Modulo/PullPush.v
+++ b/src/Util/ZUtil/Modulo/PullPush.v
@@ -82,6 +82,13 @@ Module Z.
   Hint Rewrite <- sub_mod_r : pull_Zmod.
   Hint Resolve sub_mod_r : zarith.
 
+  Lemma lnot_mod_mod v m : (Z.lnot (v mod m) mod m) = (Z.lnot v) mod m.
+  Proof.
+    cbv [Z.lnot]; etransitivity; rewrite <- !Z.sub_1_r, Z.sub_mod_full, Z.opp_mod_mod, ?Zmod_mod; reflexivity.
+  Qed.
+  Hint Rewrite lnot_mod_mod : pull_Zmod.
+  Hint Resolve lnot_mod_mod : zarith.
+
   Definition NoZMod (x : Z) := True.
   Ltac NoZMod :=
     lazymatch goal with
@@ -128,4 +135,8 @@ Module Z.
   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_push using solve [ NoZMod ] : push_Zmod.
+
+  Lemma lnot_mod_mod_push v m : NoZMod v -> (Z.lnot v) mod m = (Z.lnot (v mod m) mod m).
+  Proof. intros; symmetry; apply lnot_mod_mod. Qed.
+  Hint Rewrite lnot_mod_mod_push using solve [ NoZMod ] : push_Zmod.
 End Z.