Add Z.pow_mod_Proper

3 files changed, 37 insertions, 2 deletions

diff --git a/src/Util/ZUtil/EquivModulo.v b/src/Util/ZUtil/EquivModulo.v
index 93de3f267..3578a8223 100644
--- a/src/Util/ZUtil/EquivModulo.v
+++ b/src/Util/ZUtil/EquivModulo.v
@@ -29,6 +29,12 @@ Module Z.
     Local Instance opp_mod_Proper : Proper (equiv_modulo ==> equiv_modulo) Z.opp.
     Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed.
 
+    Local Instance pow_mod_Proper : Proper (equiv_modulo ==> eq ==> equiv_modulo) Z.pow.
+    Proof.
+      intros ?? H ???; subst; hnf in H |- *.
+      rewrite Z.power_mod_full, H, <- Z.power_mod_full; reflexivity.
+    Qed.
+
     Local Instance modulo_equiv_modulo_Proper
       : Proper (equiv_modulo ==> (fun x y => x = N /\ N = y) ==> Logic.eq) Z.modulo.
     Proof.
@@ -59,11 +65,12 @@ Module Z.
     Existing Instance add_mod_Proper.
     Existing Instance sub_mod_Proper.
     Existing Instance opp_mod_Proper.
+    Existing Instance pow_mod_Proper.
     Existing Instance modulo_equiv_modulo_Proper.
     Existing Instance eq_to_ProperProxy.
   End EquivModuloInstances.
   Module RemoveEquivModuloInstances (dummy : Nop).
-    Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances.
+    Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper pow_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances.
   End RemoveEquivModuloInstances.
 End Z.
 
diff --git a/src/Util/ZUtil/Hints/Core.v b/src/Util/ZUtil/Hints/Core.v
index dff4b7b26..1739e72af 100644
--- a/src/Util/ZUtil/Hints/Core.v
+++ b/src/Util/ZUtil/Hints/Core.v
@@ -1,6 +1,7 @@
 (** * Declaration of Hint Databases with lemmas about ℤ from the standard library *)
 Require Import Coq.micromega.Psatz Coq.omega.Omega.
 Require Import Coq.ZArith.ZArith.
+(* Should we [Require Import Coq.ZArith.Zhints.]? *)
 
 Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 4e14907e8..2146d119f 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.ZArith.Znumtheory.
+Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts.
 Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.ZSimplify.Core.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
@@ -149,6 +149,33 @@ Module Z.
   Qed.
   Hint Rewrite mod_div_eq0 using zutil_arith : zsimplify.
 
+  Lemma power_mod_full p q n : (p^q) mod n = ((p mod n)^q) mod n.
+  Proof.
+    destruct (Z_dec' n 0) as [ [H|H] | H]; subst;
+      [
+      | apply Zpower_mod; assumption
+      | rewrite !Zmod_0_r; reflexivity ].
+    { revert H.
+      rewrite <- (Z.opp_involutive (p^q)),
+      <- (Z.opp_involutive ((p mod n)^q)),
+      <- (Z.opp_involutive p),
+      <- (Z.opp_involutive n).
+      generalize (-n); clear n; intros n H.
+      rewrite !Zmod_opp_opp.
+      rewrite !Z.opp_involutive.
+      apply f_equal.
+      destruct (Z.Even_or_Odd q).
+      { rewrite !Z.pow_opp_even by (assumption || omega).
+        destruct (Z.eq_dec (p^q mod n) 0) as [H'|H'], (Z.eq_dec ((-p mod n)^q mod n) 0) as [H''|H''];
+          repeat first [ rewrite Z_mod_zero_opp_full by assumption
+                       | rewrite Z_mod_nz_opp_full by assumption
+                       | reflexivity
+                       | rewrite <- Zpower_mod, Z.pow_opp_even in H'' by (assumption || omega); omega
+                       | rewrite <- Zpower_mod, Z.pow_opp_even in H'' |- * by (assumption || omega); omega ]. }
+      { rewrite Z.pow_opp_odd, !Z.opp_involutive, <- Zpower_mod, Z.pow_opp_odd, ?Z.opp_involutive by (assumption || omega).
+        reflexivity. } }
+  Qed.
+
   Lemma mod_bound_min_max l x u d (H : l <= x <= u)
     : (if l / d =? u / d then Z.min (l mod d) (u mod d) else Z.min 0 (d + 1))
       <= x mod d