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 --- _CoqProject | 1 + src/Experiments/NewPipeline/Arithmetic.v | 2 +- src/Experiments/SimplyTypedArithmetic.v | 2 +- src/Util/ZUtil.v | 51 +---------------------- src/Util/ZUtil/Div.v | 71 ++++++++++++++++++++++++++++++++ src/Util/ZUtil/Le.v | 9 ++++ 6 files changed, 85 insertions(+), 51 deletions(-) create mode 100644 src/Util/ZUtil/Le.v diff --git a/_CoqProject b/_CoqProject index b3d46f06a..bbfffaabc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6597,6 +6597,7 @@ src/Util/ZUtil/EquivModulo.v src/Util/ZUtil/Ge.v src/Util/ZUtil/Hints.v src/Util/ZUtil/Land.v +src/Util/ZUtil/Le.v src/Util/ZUtil/ModInv.v src/Util/ZUtil/Modulo.v src/Util/ZUtil/Morphisms.v diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 21570c6b0..6dbce1a55 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -2247,7 +2247,7 @@ Module BaseConversion. eval dw dn (convert_bases sn dn p) = eval sw sn p. Proof using dwprops. cbv [convert_bases]; intros. - rewrite eval_chained_carries_no_reduce; auto using ZUtil.Z.positive_is_nonzero. + rewrite eval_chained_carries_no_reduce; auto using Z.positive_is_nonzero. rewrite eval_from_associational; auto. Qed. diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 7d314bfce..4c8830795 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -1759,7 +1759,7 @@ Module BaseConversion. eval dw dn (convert_bases sn dn p) = eval sw sn p. Proof. cbv [convert_bases]; intros. - rewrite eval_chained_carries_no_reduce; auto using ZUtil.Z.positive_is_nonzero. + rewrite eval_chained_carries_no_reduce; auto using Z.positive_is_nonzero. rewrite eval_from_associational; auto. Qed. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index eab5fda1b..2abfa7398 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -13,6 +13,7 @@ Require Import Coq.Lists.List. Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.ZUtil.Definitions. Require Export Crypto.Util.ZUtil.Div. +Require Export Crypto.Util.ZUtil.Le. Require Export Crypto.Util.ZUtil.EquivModulo. Require Export Crypto.Util.ZUtil.Hints. Require Export Crypto.Util.ZUtil.Land. @@ -30,26 +31,9 @@ Import Nat. Local Open Scope Z. Module Z. - 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 mul_comm3 x y z : x * (y * z) = y * (x * z). Proof. lia. Qed. - Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. - Proof. intros; omega. Qed. - Hint Resolve positive_is_nonzero : zarith. - - 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 pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. Proof. @@ -59,7 +43,7 @@ Module Z. Qed. (** TODO: Should we get rid of this duplicate? *) - Notation gt0_neq0 := positive_is_nonzero (only parsing). + Notation gt0_neq0 := Z.positive_is_nonzero (only parsing). Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. @@ -708,19 +692,6 @@ Module Z. Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. Proof. lia. 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 shiftl_opp_l a n : Z.shiftl (-a) n = - Z.shiftl a n - (if Z_zerop (a mod 2 ^ (- n)) then 0 else 1). Proof. @@ -747,18 +718,6 @@ Module Z. Hint Rewrite shiftr_opp_l : push_Zshift. Hint Rewrite <- shiftr_opp_l : pull_Zshift. - 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 sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. Proof. intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). @@ -805,12 +764,6 @@ Module Z. Qed. Hint Resolve mod_eq_le_to_eq : zarith. - Lemma div_same' a b : b <> 0 -> a = b -> a / b = 1. - Proof. - intros; subst; auto with zarith. - Qed. - Hint Resolve div_same' : zarith. - Lemma mod_eq_le_div_1 a b : 0 < a <= b -> a mod b = 0 -> a / b = 1. Proof. auto with zarith. Qed. Hint Resolve mod_eq_le_div_1 : zarith. 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