From 6ee6d5242d8caab769bd60ee4d44efe41add8bda Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 10 Jun 2017 15:04:32 -0400 Subject: Add Z.pow_mod_Proper --- src/Util/ZUtil/EquivModulo.v | 9 ++++++++- src/Util/ZUtil/Hints/Core.v | 1 + src/Util/ZUtil/Modulo.v | 29 ++++++++++++++++++++++++++++- 3 files changed, 37 insertions(+), 2 deletions(-) (limited to 'src/Util') 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 -- cgit v1.2.3