From 76e6aecf3d4491b5d6f6bbda3f71e5aa5e8e4da1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 6 Jul 2018 15:46:42 -0400 Subject: Shuffle some ZUtil lemmas around --- src/Util/ZUtil/Div.v | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/Util/ZUtil/Le.v | 9 +++++++ 2 files changed, 80 insertions(+) create mode 100644 src/Util/ZUtil/Le.v (limited to 'src/Util/ZUtil') diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index afa22e5b6..4616a6090 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -1,5 +1,8 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.ZArith.Znumtheory. Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Le. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.ZArith. Require Import Crypto.Util.ZUtil.Hints.PullPush. @@ -187,4 +190,72 @@ Module Z. intros; rewrite !Z.div_div by omega. f_equal; ring. Qed. + + Lemma div_lt_upper_bound' a b q : 0 < b -> a < q * b -> a / b < q. + Proof. intros; apply Z.div_lt_upper_bound; nia. Qed. + Hint Resolve div_lt_upper_bound' : zarith. + + Lemma div_cross_le_abs a b c' d : c' <> 0 -> d <> 0 -> a * Z.sgn c' * Z.abs d <= b * Z.sgn d * Z.abs c' -> a / c' <= b / d. + Proof. + clear. + destruct c', d; cbn [Z.abs Z.sgn]; + rewrite ?Zdiv_0_r, ?Z.mul_0_r, ?Z.mul_0_l, ?Z.mul_1_l, ?Z.mul_1_r; + try lia; intros ?? H; + Z.div_mod_to_quot_rem; + subst. + all: repeat match goal with + | [ H : context[_ * -1] |- _ ] => rewrite (Z.mul_add_distr_r _ _ (-1)), <- ?(Z.mul_comm (-1)), ?Z.mul_assoc in H + | [ H : context[-1 * _] |- _ ] => rewrite (Z.mul_add_distr_l (-1)), <- ?(Z.mul_comm (-1)), ?Z.mul_assoc in H + | [ H : context[-1 * Z.neg ?x] |- _ ] => rewrite (Z.mul_comm (-1) (Z.neg x)), <- Z.opp_eq_mul_m1 in H + | [ H : context[-1 * ?x] |- _ ] => rewrite (Z.mul_comm (-1) x), <- Z.opp_eq_mul_m1 in H + | [ H : context[-Z.neg _] |- _ ] => cbn [Z.opp] in H + end. + all:lazymatch goal with + | [ H : (Z.pos ?p * ?q + ?r) * Z.pos ?p' <= (Z.pos ?p' * ?q' + ?r') * Z.pos ?p |- _ ] + => let H' := fresh in + assert (H' : q <= q' + (r' * Z.pos p - r * Z.pos p') / (Z.pos p * Z.pos p')) by (Z.div_mod_to_quot_rem; nia); + revert H' + end. + all:Z.div_mod_to_quot_rem; nia. + Qed. + + Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 -> + a / b > 0. + Proof. + intros; rewrite Z.gt_lt_iff. + apply Z.div_str_pos. + split; intuition auto with omega. + apply Z.divide_pos_le; try (apply Zmod_divide); omega. + Qed. + + Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1). + Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity. + Qed. + + Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1). + Proof. + destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia. + Qed. + + Hint Rewrite Z.div_opp_l_complete using zutil_arith : pull_Zopp. + Hint Rewrite Z.div_opp_l_complete' using zutil_arith : push_Zopp. + + Lemma div_opp a : a <> 0 -> -a / a = -1. + Proof. + intros; autorewrite with pull_Zopp zsimplify; lia. + Qed. + + Hint Rewrite Z.div_opp using zutil_arith : zsimplify. + + Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0. + Proof. auto with zarith lia. Qed. + + Hint Rewrite div_sub_1_0 using zutil_arith : zsimplify. + + Lemma div_same' a b : b <> 0 -> a = b -> a / b = 1. + Proof. + intros; subst; auto with zarith. + Qed. + Hint Resolve div_same' : zarith. End Z. diff --git a/src/Util/ZUtil/Le.v b/src/Util/ZUtil/Le.v new file mode 100644 index 000000000..ab7767de7 --- /dev/null +++ b/src/Util/ZUtil/Le.v @@ -0,0 +1,9 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. + Proof. intros; omega. Qed. + Hint Resolve positive_is_nonzero : zarith. +End Z. -- cgit v1.2.3