improve zero_bounds tactic

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.