From bcc95258fa71e0ea75811227e31a3d8ef6349688 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 11:58:24 -0700 Subject: Add some proofs about Z.div and Z.mul --- src/Util/ZUtil.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 095d418a8..c7671fae5 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -526,6 +526,40 @@ Qed. Lemma two_times_x_minus_x x : 2 * x - x = x. Proof. lia. Qed. +Lemma Zmul_div_le x y z + (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) + (Hyz : y <= z) + : x * y / z <= x. +Proof. + transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. + apply Z_div_le; nia. +Qed. + +Lemma Zdiv_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. +Proof. + pose proof (Z.mod_pos_bound a b). + etransitivity; [ | apply (Zmul_div_le c (a mod b) b); lia ]. + rewrite (Z_div_mod_eq a b) at 1 by lia. + rewrite Z.mul_add_distr_l. + replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. + rewrite Z.div_add_l by lia. + lia. +Qed. + +Lemma Zdiv_mul_le_le a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. +Proof. + pose proof (Zdiv_mul_diff a b c); split; try apply Z.div_mul_le; lia. +Qed. + +Lemma Zdiv_mul_le_le_offset a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). +Proof. + pose proof (Zdiv_mul_le_le a b c); lia. +Qed. + (** * [Zsimplify_fractions_le] *) (** The culmination of this series of tactics, [Zsimplify_fractions_le], will use the fact that [a * (b / c) <= -- cgit v1.2.3