From c92678ddbbbc0c2bcfe8ee211cbdf1908e6beeab Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 15 Feb 2016 14:31:06 -0500 Subject: tweaks to util files, including automation for proving positivity/nonnegativity in Z --- src/Util/ZUtil.v | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 3ebbbece1..1c3efbdac 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -154,6 +154,39 @@ Proof. pose proof (prime_ge_2 p prime_p); omega. Qed. +Lemma mul_div_eq : (forall a m, m > 0 -> m * (a / m) = (a - a mod m))%Z. +Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. +Qed. + Ltac prime_bound := match goal with | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega -end. \ No newline at end of file +end. + +Lemma Zlt_minus_lt_0 : forall n m, m < n -> 0 < n - m. +Proof. + intros; omega. +Qed. + +(* prove that known nonnegative numbers are nonnegative *) +Ltac zero_bounds' := + repeat match goal with + | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg + | [ |- 0 <= _ - _] => apply Zle_minus_le_0 + | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg + | [ |- 0 <= _ / _] => apply Z.div_pos + | [ |- 0 < _ + _] => apply Z.add_pos_nonneg + (* TODO : this apply is not good: it can make a true goal false. Actually, + * we would want this tactic to explore two branches: + * - apply Z.add_pos_nonneg and continue + * - apply Z.add_nonneg_pos and continue + * Keep whichever one solves all subgoals. If neither does, don't apply. *) + + | [ |- 0 < _ - _] => apply Zlt_minus_lt_0 + | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split + | [ |- 0 < _ / _] => apply Z.div_str_pos + end; try omega; try prime_bound; auto. + +Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. -- cgit v1.2.3