From 2c9ff3c36a3891b6b4f809b3a44fa1b7bed78803 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 11:38:36 -0700 Subject: Add ZUtil lemmas --- src/Util/ZUtil.v | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 9b487a773..9bd134f10 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -603,7 +603,7 @@ Module Z. Z.compare_to_sgn; rewrite Z.sgn_opp; simpl. pose proof (Zdiv_sgn n m) as H. pose proof (Z.sgn_spec (n / m)) as H'. - repeat first [ progress intuition + repeat first [ progress intuition auto | progress simpl in * | congruence | lia @@ -627,12 +627,12 @@ Module Z. apply Z_div_le; nia. Qed. - Lemma div_mul_diff a b c + Hint Resolve mul_div_le : zarith. + + Lemma div_mul_diff_exact a b c (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : c * a / b - c * (a / b) <= c. + : c * a / b = c * (a / b) + (c * (a mod b)) / b. Proof. - pose proof (Z.mod_pos_bound a b). - etransitivity; [ | apply (mul_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. @@ -640,6 +640,21 @@ Module Z. lia. Qed. + Lemma div_mul_diff_exact' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * (a / b) = c * a / b - (c * (a mod b)) / b. + Proof. + rewrite div_mul_diff_exact by assumption; lia. + Qed. + + Lemma div_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. + Proof. + rewrite div_mul_diff_exact by assumption. + ring_simplify; auto with zarith. + Qed. + Lemma div_mul_le_le a b c : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. Proof. -- cgit v1.2.3