From b18cfd89e1e8760185d9f50dd777c1c8096cf807 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 15:53:08 -0400 Subject: improve zero_bounds tactic --- src/Arithmetic.v | 20 ++++---------------- src/Util/ZUtil/Tactics/ZeroBounds.v | 18 +++++++++++++++--- 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/Arithmetic.v b/src/Arithmetic.v index 5cd751551..b2f1eb428 100644 --- a/src/Arithmetic.v +++ b/src/Arithmetic.v @@ -5243,20 +5243,6 @@ Module BarrettReduction. end. Qed. - (* improved! *) - Ltac zero_bounds' := - repeat match goal with - | |- ?a <> 0 => apply Z.positive_is_nonzero - | |- ?a > 0 => apply Z.lt_gt - | |- ?a >= 0 => apply Z.le_ge - end; - try match goal with - | |- 0 < ?a => Z.zero_bounds - | |- 0 <= ?a => Z.zero_bounds - end. - - Ltac zutil_arith ::= solve [ omega | Psatz.lia | auto with nocore | solve [zero_bounds'] ]. - Hint Rewrite UniformWeight.uweight_S UniformWeight.uweight_eq_alt' using lia : weight_to_pow. Hint Rewrite <-UniformWeight.uweight_S UniformWeight.uweight_eq_alt' using lia : pow_to_weight. @@ -5271,6 +5257,9 @@ Module BarrettReduction. apply Z.pow_le_mono_r; lia. Qed. + (* use zero_bounds in zutil_arith *) + Local Ltac zutil_arith ::= solve [ omega | Psatz.lia | auto with nocore | solve [Z.zero_bounds] ]. + Lemma muSelect_correct x : 0 <= x < w (sz * 2) -> muSelect (partition w (sz*2) x) = partition w sz (mu mod (w sz) * (x / 2 ^ (k - 1) / (w sz))). @@ -5286,8 +5275,7 @@ Module BarrettReduction. end. replace (x / (w (sz * 2 - 1)) / (2 ^ width / 2)) with (x / (2 ^ (k - 1)) / w sz) by (autorewrite with weight_to_pow pull_Zpow pull_Zdiv; do 2 f_equal; nia). - - rewrite Z.div_between_0_if with (a:=x / 2^(k-1)) by (zero_bounds'; auto using q1_range). + rewrite Z.div_between_0_if with (a:=x / 2^(k-1)) by (Z.zero_bounds; auto using q1_range). break_innermost_match; try lia; autorewrite with zsimplify_fast; [ | ]. { apply partition_eq_mod; auto with zarith. } { rewrite partition_0; reflexivity. } diff --git a/src/Util/ZUtil/Tactics/ZeroBounds.v b/src/Util/ZUtil/Tactics/ZeroBounds.v index 86501d84b..c81343b55 100644 --- a/src/Util/ZUtil/Tactics/ZeroBounds.v +++ b/src/Util/ZUtil/Tactics/ZeroBounds.v @@ -1,11 +1,12 @@ Require Import Coq.ZArith.ZArith Coq.omega.Omega. Require Import Crypto.Util.ZUtil.Tactics.PrimeBound. Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Le. Local Open Scope Z_scope. Module Z. (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) - Ltac zero_bounds' := + Ltac zero_bounds'' := repeat match goal with | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg | [ |- 0 <= _ - _] => apply Z.le_0_sub @@ -14,14 +15,25 @@ Module Z. | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg | [ |- 0 <= _ mod _] => apply Z.mod_pos_bound - | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds']; - try solve [apply Z.add_nonneg_pos; zero_bounds'] + | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'']; + try solve [apply Z.add_nonneg_pos; zero_bounds''] | [ |- 0 < _ - _] => apply Z.lt_0_sub | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split | [ |- 0 < _ / _] => apply Z.div_str_pos | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg end; try omega; try Z.prime_bound; auto. + Ltac zero_bounds' := + repeat match goal with + | |- ?a <> 0 => apply Z.positive_is_nonzero + | |- ?a > 0 => apply Z.lt_gt + | |- ?a >= 0 => apply Z.le_ge + end; + try match goal with + | |- 0 < ?a => zero_bounds'' + | |- 0 <= ?a => zero_bounds'' + end. + Ltac zero_bounds := try omega; try Z.prime_bound; zero_bounds'. Hint Extern 1 => progress zero_bounds : zero_bounds. -- cgit v1.2.3