From bc6311b1c912522e1babf593c5eb85a284cf564c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 16 Aug 2016 18:25:54 -0700 Subject: Add a faster zsimplify database --- src/Util/ZUtil.v | 13 +++++++++---- 1 file 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. -- cgit v1.2.3