Split off ZUtil initial hint databases

1 files changed, 55 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Tactics/PeelLe.v b/src/Util/ZUtil/Tactics/PeelLe.v
new file mode 100644
index 000000000..f299e0acd
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/PeelLe.v
@@ -0,0 +1,55 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+
+Local Open Scope Z.
+
+Module Z.
+  Ltac peel_le_step :=
+    match goal with
+    | [ |- ?x + _ <= ?x + _ ]
+      => apply Z.add_le_mono_l
+    | [ |- _ + ?x <= _ + ?x ]
+      => apply Z.add_le_mono_r
+    | [ |- ?x - _ <= ?x - _ ]
+      => apply Z.sub_le_mono_l
+    | [ |- _ - ?x <= _ - ?x ]
+      => apply Z.sub_le_mono_r
+    | [ |- ?x^_ <= ?x^_ ]
+      => apply Z.pow_le_mono_r; [ zutil_arith | ]
+    | [ |- _^?x <= _^?x ]
+      => apply Z.pow_le_mono_l; split; [ zutil_arith | ]
+    | [ |- Z.log2_up _ <= Z.log2_up _ ]
+      => apply Z.log2_up_le_mono
+    | [ |- Z.log2 _ <= Z.log2 _ ]
+      => apply Z.log2_le_mono
+    | [ |- Z.succ _ <= Z.succ _ ]
+      => apply Zsucc_le_compat
+    | [ |- Z.pred _ <= Z.pred _ ]
+      => apply Z.pred_le_mono
+    | [ |- ?x * _ <= ?x * _ ]
+      => first [ apply Z.mul_le_mono_nonneg_l; [ zutil_arith | ]
+               | apply Z.mul_le_mono_nonpos_l; [ zutil_arith | ] ]
+    | [ |- _ * ?x <= _ * ?x ]
+      => first [ apply Z.mul_le_mono_nonneg_r; [ zutil_arith | ]
+               | apply Z.mul_le_mono_nonpos_r; [ zutil_arith | ] ]
+    | [ |- -_ <= -_ ]
+      => apply Z.opp_le_mono
+    | [ |- _ / ?x <= _ / ?x ]
+      => apply Z.div_le_mono; [ zutil_arith | ]
+    | [ |- ?x / _ <= ?x / _ ]
+      => apply Z.div_le_compat_l; [ zutil_arith | split; [ zutil_arith | ] ]
+    | [ |- Z.quot _ ?x <= Z.quot _ ?x ]
+      => apply Z.quot_le_mono; [ zutil_arith | ]
+    | [ |- Z.quot ?x _ <= Z.quot ?x _ ]
+      => apply Z.quot_le_compat_l; [ zutil_arith | split; [ zutil_arith | ] ]
+    | [ |- Z.max ?x _ <= Z.max ?x _ ]
+      => apply Z.max_le_compat_l
+    | [ |- Z.max _ ?x <= Z.max _ ?x ]
+      => apply Z.max_le_compat_r
+    | [ |- Z.min ?x _ <= Z.min ?x _ ]
+      => apply Z.min_le_compat_l
+    | [ |- Z.min _ ?x <= Z.min _ ?x ]
+      => apply Z.min_le_compat_r
+    end.
+  Ltac peel_le := repeat peel_le_step.
+End Z.