diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-13 13:09:48 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-13 13:09:48 -0400 |
commit | a680811dcbd532f3bdc55bc1ac3437e761359469 (patch) | |
tree | e67057d588bfc830ab1d3517debedc149f24710b /src/Util | |
parent | 401058d999a6eaa38ce31b2ee9356a65b63498d2 (diff) |
Split off pull_Zmod, push_Zmod from ZUtil
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/ZUtil.v | 206 | ||||
-rw-r--r-- | src/Util/ZUtil/Modulo/PullPush.v | 131 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics.v | 1 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/PullPush.v | 1 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/PullPush/Modulo.v | 84 |
5 files changed, 218 insertions, 205 deletions
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. |