Split off more ZUtil things

1 files changed, 65 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v
index 325818a2c..b054ec8e5 100644
--- a/src/Util/ZUtil/Div.v
+++ b/src/Util/ZUtil/Div.v
@@ -1,6 +1,9 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
 Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn.
 Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Hints.ZArith.
+Require Import Crypto.Util.ZUtil.Hints.PullPush.
+Require Import Crypto.Util.ZUtil.ZSimplify.Core.
 Local Open Scope Z_scope.
 
 Module Z.
@@ -33,4 +36,66 @@ Module Z.
                    | [ x : Z |- _ ] => destruct x
                    end ].
   Qed.
+
+  Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b.
+  Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed.
+
+  Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b.
+  Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed.
+
+  Hint Rewrite div_add_l' div_add' using zutil_arith : zsimplify.
+
+  Lemma div_sub a b c : c <> 0 -> (a - b * c) / c = a / c - b.
+  Proof. intros; rewrite <- !Z.add_opp_r, <- Z.div_add by lia; apply f_equal2; lia. Qed.
+
+  Lemma div_sub' a b c : c <> 0 -> (a - c * b) / c = a / c - b.
+  Proof. intro; rewrite <- div_sub, (Z.mul_comm c); try lia. Qed.
+
+  Hint Rewrite div_sub div_sub' using zutil_arith : zsimplify.
+
+  Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b.
+  Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed.
+
+  Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b.
+  Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed.
+
+  Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b.
+  Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed.
+
+  Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b.
+  Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed.
+
+  Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using zutil_arith : zsimplify.
+
+  Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
+    autorewrite with zsimplify. reflexivity.
+  Qed.
+
+  Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
+    autorewrite with zsimplify; reflexivity.
+  Qed.
+
+  Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using zutil_arith : zsimplify.
+
+  Lemma div_mul_skip_pow base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> x * base^e0 / y / base^e1 = x * base^(e0 - e1) / y.
+  Proof.
+    intros.
+    assert (0 < base^e1) by auto with zarith.
+    replace (base^e0) with (base^(e0 - e1) * base^e1) by (autorewrite with pull_Zpow zsimplify; reflexivity).
+    rewrite !Z.mul_assoc.
+    autorewrite with zsimplify; lia.
+  Qed.
+  Hint Rewrite div_mul_skip_pow using zutil_arith : zsimplify.
+
+  Lemma div_mul_skip_pow' base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> base^e0 * x / y / base^e1 = base^(e0 - e1) * x / y.
+  Proof.
+    intros.
+    rewrite (Z.mul_comm (base^e0) x), div_mul_skip_pow by lia.
+    auto using f_equal2 with lia.
+  Qed.
+  Hint Rewrite div_mul_skip_pow' using zutil_arith : zsimplify.
 End Z.