diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-04 20:12:36 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-04 20:12:36 -0400 |
| commit | 4cd73fac4f8f68bf390f8c87f27fa4cba3e68cef (patch) | |
| tree | 6070a58cab538f70c3abf2de8ba631a8d157e77e /src/Util/ZUtil.v | |
| parent | a63e54ca057d61c4ffa9d1d1f240bb95e432fbc7 (diff) | |
Handle ?x mod ?x in push_Zmod
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 0de3d2ca0..624e953f9 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -100,6 +100,7 @@ Hint Rewrite <- Z.div_div using zutil_arith : push_Zdiv. Hint Rewrite <- Z.mul_mod Z.add_mod Zminus_mod using zutil_arith : pull_Zmod. Hint Rewrite Zminus_mod_idemp_l Zminus_mod_idemp_r : pull_Zmod. Hint Rewrite Z_mod_nz_opp_full using zutil_arith : push_Zmod. +Hint Rewrite Z_mod_same_full : push_Zmod. Hint Rewrite Nat2Z.id : zsimplify. Hint Rewrite Nat2Z.id : push_Zof_nat. Hint Rewrite Nat2Z.inj_0 Nat2Z.inj_succ Nat2Z.inj_abs_nat Nat2Z.inj_add Nat2Z.inj_mul Nat2Z.inj_sub_max Nat2Z.inj_pred_max Nat2Z.inj_min Nat2Z.inj_max Zabs2Nat.id_abs Zabs2Nat.id : push_Zof_nat. @@ -2491,6 +2492,8 @@ End BoundsTactics. Ltac push_Zmod := repeat match goal with | _ => progress autorewrite with push_Zmod + | [ |- context[?x mod ?x] ] + => rewrite (Z_mod_same_full x) | [ |- 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 @@ -2510,6 +2513,8 @@ Ltac push_Zmod := Ltac push_Zmod_hyps := repeat match goal with | _ => progress autorewrite with push_Zmod in * |- + | [ H : context[?x mod ?x] |- _ ] + => rewrite (Z_mod_same_full x) in H | [ 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 |