diff options
author | Jason Gross <jagro@google.com> | 2018-07-17 18:51:25 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-07-17 18:51:25 -0400 |
commit | 10d1d4825c00d432b76420bb24f1b9df732ec4b3 (patch) | |
tree | f2ce97f2bce6e0b0b14cdbd109005fcef56240c1 /src/Util/ZUtil/ZSimplify | |
parent | abdd602e89c4d6f9073baab523a880b473f241af (diff) |
Handle Z.pow in {push,pull}_Zmod
Diffstat (limited to 'src/Util/ZUtil/ZSimplify')
-rw-r--r-- | src/Util/ZUtil/ZSimplify/Core.v | 8 | ||||
-rw-r--r-- | src/Util/ZUtil/ZSimplify/Simple.v | 13 |
2 files changed, 16 insertions, 5 deletions
diff --git a/src/Util/ZUtil/ZSimplify/Core.v b/src/Util/ZUtil/ZSimplify/Core.v index 6717a5a01..958c44f74 100644 --- a/src/Util/ZUtil/ZSimplify/Core.v +++ b/src/Util/ZUtil/ZSimplify/Core.v @@ -1,14 +1,14 @@ Require Import Coq.ZArith.ZArith. Require Export Crypto.Util.ZUtil.Hints.Core. -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 Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.pow_1_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 Z.sub_diag Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : 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 Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.pow_1_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.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 Zplus_minus Z.add_diag Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Zdiv_0_r Zdiv_0_l Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : 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 Z.pow_1_l using zutil_arith : zsimplify. Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify. Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify. Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify. -Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r Z.pow_1_l : zsimplify_const. +Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 Z.abs_0 Z.sgn_0 Nat2Z.inj_0 Z2Nat.inj_0 Z.land_0_l Z.land_0_r Z.lor_0_l Z.lor_0_r Z.lnot_0 Z.land_lnot_diag Z.lnot_involutive Z.lxor_lnot_lnot Z.lnot_m1 Z.lxor_m1_l Z.lxor_m1_r Z.add_lnot_diag Z.lor_lnot_diag Z.pow_0_r Z.pow_0_l Z.pow_1_r : zsimplify_const. Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const. diff --git a/src/Util/ZUtil/ZSimplify/Simple.v b/src/Util/ZUtil/ZSimplify/Simple.v index 9b5e0e9c8..94fa05e1a 100644 --- a/src/Util/ZUtil/ZSimplify/Simple.v +++ b/src/Util/ZUtil/ZSimplify/Simple.v @@ -3,6 +3,17 @@ Require Import Crypto.Util.ZUtil.Hints.Core. Local Open Scope Z_scope. Module Z. + Lemma pow_1_l_Zpos a : 1^Zpos a = 1. + Proof. apply Z.pow_1_l; lia. Qed. + Hint Rewrite pow_1_l_Zpos : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_1_l_0 : 1^Z0 = 1. Proof. reflexivity. Qed. + Hint Rewrite pow_1_l_0 : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_r_Zneg a b : a^Zneg b = 0. Proof. reflexivity. Qed. + Hint Rewrite pow_r_Zneg : zsimplify_fast zsimplify_const zsimplify. + Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1. + Proof. apply Z.pow_1_l; lia. Qed. + Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify. + Lemma sub_same_minus (x y : Z) : x - (x - y) = y. Proof. lia. Qed. Hint Rewrite sub_same_minus : zsimplify. @@ -78,5 +89,5 @@ Module Z. Lemma minus_minus_one : - -1 = 1. Proof. reflexivity. Qed. - Hint Rewrite minus_minus_one : zsimplify. + Hint Rewrite minus_minus_one : zsimplify zsimplify_fast zsimplify_const. End Z. |