diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 18:46:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 18:46:55 -0400 |
| commit | 00965588b4e14e34cd0f864fb32a780ad8bae89d (patch) | |
| tree | c43e5c4da8ed254bc93c4f917a499f6ff483cbbe /src/Util/ZUtil.v | |
| parent | 7361ecd49ae13cff49467e67a6533a557e77139c (diff) | |
Add {push,pull}_Zof_N hint db to ZUtil
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 8257c429f..852803638 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -75,6 +75,8 @@ Create HintDb pull_Zof_nat discriminated. Create HintDb push_Zof_nat discriminated. Create HintDb pull_Zshift discriminated. Create HintDb push_Zshift discriminated. +Create HintDb pull_Zof_N discriminated. +Create HintDb push_Zof_N discriminated. Create HintDb Zshift_to_pow discriminated. Create HintDb Zpow_to_shift discriminated. Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp. @@ -97,6 +99,8 @@ Hint Extern 1 => autorewrite with pull_Zshift in * : pull_Zshift. Hint Extern 1 => autorewrite with push_Zshift in * : push_Zshift. Hint Extern 1 => autorewrite with Zshift_to_pow in * : Zshift_to_pow. Hint Extern 1 => autorewrite with Zpow_to_shift in * : Zpow_to_shift. +Hint Extern 1 => autorewrite with pull_Zof_N in * : pull_Zof_N. +Hint Extern 1 => autorewrite with push_Zof_N in * : push_Zof_N. Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using zutil_arith : pull_Zopp. Hint Rewrite Z.mul_opp_l : pull_Zopp. Hint Rewrite <- Z.opp_add_distr : pull_Zopp. @@ -113,8 +117,12 @@ 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 N2Z.id : zsimplify. Hint Rewrite Nat2Z.id : push_Zof_nat. +Hint Rewrite N2Z.id : pull_Zof_N. +Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 : push_Zof_N. +Hint Rewrite N2Z.inj_compare N2Z.inj_testbit : pull_Zof_N. +Hint Rewrite <- N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow : pull_Zof_N. 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. 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 : pull_Zof_nat. Hint Rewrite Z.shiftr_shiftl_l Z.shiftr_shiftl_r Z.shiftr_shiftr Z.shiftl_shiftl using zutil_arith : pull_Zshift. |