Add some zutil lemmas

1 files changed, 61 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 03b9e0e56..87dec1cf9 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -2842,6 +2842,67 @@ Module Z.
     destruct (0 <=? x), (x <? 0); try omega.
   Qed.
 
+  Lemma quot_div_full a b : Z.quot a b = Z.sgn a * Z.sgn b * (Z.abs a / Z.abs b).
+  Proof.
+    destruct (Z_zerop b); [ subst | apply Z.quot_div; assumption ].
+    destruct a; simpl; reflexivity.
+  Qed.
+
+  Lemma div_abs_sgn_nonneg a b : 0 <= Z.sgn (Z.abs a / Z.abs b).
+  Proof.
+    generalize (Zdiv_sgn (Z.abs a) (Z.abs b)).
+    destruct a, b; simpl; omega.
+  Qed.
+  Hint Resolve div_abs_sgn_nonneg : zarith.
+
+  Local Arguments Z.mul !_ !_.
+
+  Lemma quot_sgn_nonneg a b : 0 <= Z.sgn (Z.quot a b) * Z.sgn a * Z.sgn b.
+  Proof.
+    rewrite quot_div_full, !Z.sgn_mul, !Z.sgn_sgn.
+    set (d := Z.abs a / Z.abs b).
+    destruct a, b; simpl; try (subst d; simpl; omega);
+      try rewrite (Z.mul_opp_l 1);
+      do 2 try rewrite (Z.mul_opp_r _ 1);
+      rewrite ?Z.mul_1_l, ?Z.mul_1_r, ?Z.opp_involutive;
+      apply div_abs_sgn_nonneg.
+  Qed.
+
+  Lemma quot_nonneg_same_sgn a b : Z.sgn a = Z.sgn b -> 0 <= Z.quot a b.
+  Proof.
+    intro H.
+    generalize (quot_sgn_nonneg a b); rewrite H.
+    rewrite <- Z.mul_assoc, <- Z.sgn_mul.
+    destruct (Z_zerop b); [ subst; destruct a; unfold Z.quot; simpl in *; congruence | ].
+    rewrite (Z.sgn_pos (_ * _)) by nia.
+    intro; apply Z.sgn_nonneg; omega.
+  Qed.
+
+  Lemma mul_quot_eq_full a m : m <> 0 -> m * (Z.quot a m) = a - a mod (Z.abs m * Z.sgn a).
+  Proof.
+    intro Hm.
+    assert (0 <> m * m) by (intro; apply Hm; nia).
+    assert (0 < m * m) by nia.
+    assert (0 <> Z.abs m) by (destruct m; simpl in *; try congruence).
+    rewrite quot_div_full.
+    rewrite <- (Z.abs_sgn m) at 1.
+    transitivity ((Z.sgn m * Z.sgn m) * Z.sgn a * (Z.abs m * (Z.abs a / Z.abs m))); [ nia | ].
+    rewrite <- Z.sgn_mul, Z.sgn_pos, Z.mul_1_l, Z.mul_div_eq_full by omega.
+    rewrite Z.mul_sub_distr_l.
+    rewrite Z.mul_comm, Z.abs_sgn.
+    destruct a; simpl Z.sgn; simpl Z.abs; autorewrite with zsimplify_const; [ reflexivity | reflexivity | ].
+    repeat match goal with |- context[-1 * ?x] => replace (-1 * x) with (-x) by omega end.
+    repeat match goal with |- context[?x * -1] => replace (x * -1) with (-x) by omega end.
+    rewrite <- Zmod_opp_opp; simpl Z.opp.
+    reflexivity.
+  Qed.
+
+  Lemma quot_sub_sgn a : Z.quot (a - Z.sgn a) a = 0.
+  Proof.
+    rewrite quot_div_full.
+    destruct (Z_zerop a); subst; [ lia | ].
+    rewrite Z.div_small; lia.
+  Qed.
 
   (* Naming Convention: [X] for thing being divided by, [p] for plus,
      [m] for minus, [d] for div, and [_] to separate parentheses and