From 10d1d4825c00d432b76420bb24f1b9df732ec4b3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Jul 2018 18:51:25 -0400 Subject: Handle Z.pow in {push,pull}_Zmod --- src/Util/ZUtil/EquivModulo.v | 2 ++ src/Util/ZUtil/Modulo.v | 27 ------------------------ src/Util/ZUtil/Modulo/PullPush.v | 35 ++++++++++++++++++++++++++++++++ src/Util/ZUtil/Tactics/PullPush/Modulo.v | 3 +++ src/Util/ZUtil/ZSimplify/Core.v | 8 ++++---- src/Util/ZUtil/ZSimplify/Simple.v | 13 +++++++++++- 6 files changed, 56 insertions(+), 32 deletions(-) (limited to 'src/Util/ZUtil') diff --git a/src/Util/ZUtil/EquivModulo.v b/src/Util/ZUtil/EquivModulo.v index a67174629..2d8f5aefc 100644 --- a/src/Util/ZUtil/EquivModulo.v +++ b/src/Util/ZUtil/EquivModulo.v @@ -5,6 +5,8 @@ Require Import Crypto.Util.Notations. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.ZArith. Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. + Local Open Scope Z_scope. Module Z. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index be513eb3c..8dea71870 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -225,33 +225,6 @@ Module Z. Lemma small_mod_eq a b n: a mod n = b mod n -> 0 <= a < n -> a = b mod n. Proof. intros; rewrite <-(Z.mod_small a n); auto. Qed. - Lemma mod_pow_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 diff --git a/src/Util/ZUtil/Modulo/PullPush.v b/src/Util/ZUtil/Modulo/PullPush.v index dbbe98975..13f8bd24f 100644 --- a/src/Util/ZUtil/Modulo/PullPush.v +++ b/src/Util/ZUtil/Modulo/PullPush.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.ZSimplify.Core. Local Open Scope Z_scope. @@ -89,6 +90,36 @@ Module Z. Hint Rewrite lnot_mod_mod : pull_Zmod. Hint Resolve lnot_mod_mod : zarith. + Lemma mod_pow_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. + Hint Rewrite <- mod_pow_full : pull_Zmod. + Hint Resolve mod_pow_full : zarith. + Notation pow_mod_full := mod_pow_full. + Definition NoZMod (x : Z) := True. Ltac NoZMod := lazymatch goal with @@ -139,4 +170,8 @@ Module Z. 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. + + Lemma pow_mod_push p q n : NoZMod p -> (p^q) mod n = ((p mod n)^q) mod n. + Proof. intros; apply pow_mod_full. Qed. + Hint Rewrite pow_mod_push using solve [ NoZMod ] : push_Zmod. End Z. diff --git a/src/Util/ZUtil/Tactics/PullPush/Modulo.v b/src/Util/ZUtil/Tactics/PullPush/Modulo.v index a2502aeea..4ff81f7ad 100644 --- a/src/Util/ZUtil/Tactics/PullPush/Modulo.v +++ b/src/Util/ZUtil/Tactics/PullPush/Modulo.v @@ -78,6 +78,9 @@ Ltac pull_Zmod := | [ |- context[(((-?y) mod ?z)) mod ?z] ] => has_no_mod y z; rewrite <- (Z.opp_mod_mod y z) + | [ |- context[((?x mod ?z)^?y) mod ?z] ] + => has_no_mod x z; + rewrite <- (Z.pow_mod_full x y z) | [ |- context[(?x mod ?z) mod ?z] ] => rewrite (Zmod_mod x z) | _ => progress autorewrite with pull_Zmod diff --git a/src/Util/ZUtil/ZSimplify/Core.v b/src/Util/ZUtil/ZSimplify/Core.v index 6717a5a01..958c44f74 100644 --- a/src/Util/ZUtil/ZSimplify/Core.v +++ b/src/Util/ZUtil/ZSimplify/Core.v @@ -1,14 +1,14 @@ Require Import Coq.ZArith.ZArith. Require Export Crypto.Util.ZUtil.Hints.Core. -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 Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.pow_1_l : zsimplify_fast. +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 Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_fast. -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 Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.pow_1_l : 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 Z.mod_1_l using zutil_arith : zsimplify. +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 Zmod_mod Z.mul_succ_l Z.mul_succ_r Z.shiftr_0_r Z.shiftr_0_l Z.mod_1_r Zmod_0_l Zmod_0_r Z.shiftl_0_r Z.shiftl_0_l Z.shiftr_0_r Z.shiftr_0_l Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_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 Z_mod_zero_opp_full Z.mod_1_l Z.pow_1_l using zutil_arith : zsimplify. Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify. Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify. Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify. -Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.pow_1_l : zsimplify_const. +Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_const. Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const. diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v index 9b5e0e9c8..94fa05e1a 100644 --- a/src/Util/ZUtil/ZSimplify/Simple.v +++ b/src/Util/ZUtil/ZSimplify/Simple.v @@ -3,6 +3,17 @@ Require Import Crypto.Util.ZUtil.Hints.Core. Local Open Scope Z_scope. Module Z. + Lemma pow_1_l_Zpos a : 1^Zpos a = 1. + Proof. apply Z.pow_1_l; lia. Qed. + Hint Rewrite pow_1_l_Zpos : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_1_l_0 : 1^Z0 = 1. Proof. reflexivity. Qed. + Hint Rewrite pow_1_l_0 : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_r_Zneg a b : a^Zneg b = 0. Proof. reflexivity. Qed. + Hint Rewrite pow_r_Zneg : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1. + Proof. apply Z.pow_1_l; lia. Qed. + Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify. + Lemma sub_same_minus (x y : Z) : x - (x - y) = y. Proof. lia. Qed. Hint Rewrite sub_same_minus : zsimplify. @@ -78,5 +89,5 @@ Module Z. Lemma minus_minus_one : - -1 = 1. Proof. reflexivity. Qed. - Hint Rewrite minus_minus_one : zsimplify. + Hint Rewrite minus_minus_one : zsimplify zsimplify_fast zsimplify_const. End Z. -- cgit v1.2.3