diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-17 19:18:43 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-17 19:18:43 -0400 |
| commit | 915e84a27e4828856eb1af84641224091a203a3f (patch) | |
| tree | 5626fe7cebd664b9dd8895f97f683252d76176b9 /src/Util | |
| parent | 74353376d2a9f69991300e6a0704f85bc642b1c4 (diff) | |
Handle Z.pow in push_Zmod tactic
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ZUtil/Tactics/PullPush/Modulo.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Tactics/PullPush/Modulo.v b/src/Util/ZUtil/Tactics/PullPush/Modulo.v index 4ff81f7ad..55889cbf0 100644 --- a/src/Util/ZUtil/Tactics/PullPush/Modulo.v +++ b/src/Util/ZUtil/Tactics/PullPush/Modulo.v @@ -20,6 +20,8 @@ Ltac push_Zmod := | 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 + | [ |- context[(?p^?q) mod ?z] ] + => rewrite (Z.pow_mod_push p q z) by Z.NoZMod end. Ltac push_Zmod_hyps := @@ -39,6 +41,8 @@ Ltac push_Zmod_hyps := | 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 + | [ H : context[(?p^?q) mod ?z] |- _ ] + => rewrite (Z.pow_mod_push p q z) in H by Z.NoZMod end. Ltac has_no_mod x z := |