diff options
| -rw-r--r-- | src/Util/ZUtil.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5fc97ce63..ea027bdee 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -27,6 +27,11 @@ Ltac zutil_arith := solve [ omega | lia ]. which can reasonably be said to "simplify" the goal, should go in this database. *) Create HintDb zsimplify discriminated. +(** Only hints that are always safe to apply, and "simplify" the goal, + and don't require any side conditions, should go in this + database. *) +Create HintDb zsimplify_fast discriminated. +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 : 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 : 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.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify. @@ -213,7 +218,7 @@ Module Z. unfold Z.pow2_mod. rewrite Z.land_ones; auto. Qed. - + Lemma ones_spec : forall n m, 0 <= n -> 0 <= m -> Z.testbit (Z.ones n) m = if Z_lt_dec m n then true else false. Proof. intros. @@ -236,12 +241,12 @@ Module Z. end. Qed. Hint Rewrite testbit_pow2_mod using omega : Ztestbit. - + Lemma pow2_mod_0_r : forall a, Z.pow2_mod a 0 = 0. Proof. - intros; rewrite Z.pow2_mod_spec, Z.mod_1_r; reflexivity. + intros; rewrite Z.pow2_mod_spec, Z.mod_1_r; reflexivity. Qed. - + Lemma pow2_mod_0_l : forall n, 0 <= n -> Z.pow2_mod 0 n = 0. Proof. intros; rewrite Z.pow2_mod_spec, Z.mod_0_l; try reflexivity; try apply Z.pow_nonzero; omega. |