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 From 3f5cde96b69075c019a502d43a35c11021735b89 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 11:40:54 -0700 Subject: Update .mailmap --- .mailmap | 1 + 1 file changed, 1 insertion(+) diff --git a/.mailmap b/.mailmap index 9cc1664d1..75f129145 100644 --- a/.mailmap +++ b/.mailmap @@ -7,6 +7,7 @@ Adam Chlipala Adam Chlipala Andres Erbsen Andres Erbsen Andres Erbsen Jade Philipoom Jade Philipoom +Jade Philipoom jadephilipoom Jade Philipoom jadep Jade Philipoom jadep Jason Gross Jason Gross -- cgit v1.2.3 From bcd99195575ca1c45d49c21a46b9caaecd9bbc10 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 11:44:29 -0700 Subject: Add more ZUtil lemmas We really want rewrite mod AC here... --- src/Util/ZUtil.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 9bd134f10..a1d53f02b 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -647,6 +647,20 @@ Module Z. rewrite div_mul_diff_exact by assumption; lia. Qed. + Lemma div_mul_diff_exact'' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : a * c / b = (a / b) * c + (c * (a mod b)) / b. + Proof. + rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. + Qed. + + Lemma div_mul_diff_exact''' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : (a / b) * c = a * c / b - (c * (a mod b)) / b. + Proof. + rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; 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. -- cgit v1.2.3 From f2ff0b784cf671c608ece8ce081fecf8d24622f1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 11:55:21 -0700 Subject: More ZUtil helper lemmas --- src/Util/ZUtil.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a1d53f02b..370628b3c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -683,6 +683,43 @@ Module Z. Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. + Lemma sub_same_minus (x y : Z) : x - (x - y) = y. + Proof. lia. Qed. + Hint Rewrite sub_same_minus : zsimplify. + Lemma sub_same_plus (x y : Z) : x - (x + y) = -y. + Proof. lia. Qed. + Hint Rewrite sub_same_plus : zsimplify. + Lemma sub_same_minus_plus (x y z : Z) : x - (x - y + z) = y - z. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_plus : zsimplify. + Lemma sub_same_plus_plus (x y z : Z) : x - (x + y + z) = -y - z. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_plus : zsimplify. + Lemma sub_same_minus_minus (x y z : Z) : x - (x - y - z) = y + z. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_minus : zsimplify. + Lemma sub_same_plus_minus (x y z : Z) : x - (x + y - z) = z - y. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_minus : zsimplify. + Lemma sub_same_minus_then_plus (x y w : Z) : x - (x - y) + w = y + w. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_then_plus : zsimplify. + Lemma sub_same_plus_then_plus (x y w : Z) : x - (x + y) + w = w - y. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_then_plus : zsimplify. + Lemma sub_same_minus_plus_then_plus (x y z w : Z) : x - (x - y + z) + w = y - z + w. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_plus_then_plus : zsimplify. + Lemma sub_same_plus_plus_then_plus (x y z w : Z) : x - (x + y + z) + w = w - y - z. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_plus_then_plus : zsimplify. + Lemma sub_same_minus_minus_then_plus (x y z w : Z) : x - (x - y - z) + w = y + z + w. + Proof. lia. Qed. + Hint Rewrite sub_same_minus_minus : zsimplify. + Lemma sub_same_plus_minus_then_plus (x y z w : Z) : x - (x + y - z) + w = z - y + w. + Proof. lia. Qed. + Hint Rewrite sub_same_plus_minus_then_plus : zsimplify. + (** * [Z.simplify_fractions_le] *) (** The culmination of this series of tactics, [Z.simplify_fractions_le], will use the fact that [a * (b / c) <= -- cgit v1.2.3 From f4e35faa34145ab24aad021025b7d0d6e7f2214c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 13:49:52 -0700 Subject: Add more ZUtil --- src/Util/ZUtil.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 370628b3c..d0aa12e58 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -984,6 +984,22 @@ Module Z. Qed. Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify. + + Lemma div_small_neg x y : 0 < -x < y -> x / y = -1. + Proof. + intro H; rewrite <- (Z.opp_involutive x). + rewrite Z.div_opp_l_complete by lia. + generalize dependent (-x); clear x; intros x H. + autorewrite with zsimplify; break_match; lia. + Qed. + Hint Rewrite div_small_neg using lia : zsimplify. + + Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y < z -> (x - y) / z = if x Date: Thu, 21 Jul 2016 13:51:35 -0700 Subject: Fix broken proofs --- src/Util/ZUtil.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d0aa12e58..00e227e2d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -990,16 +990,17 @@ Module Z. intro H; rewrite <- (Z.opp_involutive x). rewrite Z.div_opp_l_complete by lia. generalize dependent (-x); clear x; intros x H. - autorewrite with zsimplify; break_match; lia. + autorewrite with zsimplify; edestruct Z_zerop; lia. Qed. Hint Rewrite div_small_neg using lia : zsimplify. Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y < z -> (x - y) / z = if x Date: Thu, 21 Jul 2016 14:00:42 -0700 Subject: Another ZUtil lemma --- src/Util/ZUtil.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 00e227e2d..97bfd44a2 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1001,6 +1001,9 @@ Module Z. intros; autorewrite with zsimplify; lia. Qed. Hint Rewrite div_sub_small using lia : zsimplify. + + Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. + Proof. lia. Qed. End Z. Module Export BoundsTactics. -- cgit v1.2.3 From 57bd30d9c16ff44c0fb7b771bdb1fcd579f7b08d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 14:07:08 -0700 Subject: Add another ZUtil lemma --- src/Util/ZUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 97bfd44a2..d26859ecc 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1004,6 +1004,13 @@ Module Z. Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. Proof. lia. Qed. + + Lemma mul_div_lt_by_le x y z b : 0 <= y < z -> 0 <= x < b -> x * y / z < b. + Proof. + intros [? ?] [? ?]; eapply Z.le_lt_trans; [ | eassumption ]. + auto with zarith. + Qed. + Hint Resolve mul_div_lt_by_le : zarith. End Z. Module Export BoundsTactics. -- cgit v1.2.3 From ae8fe63991e3207f63f4bbf919206e7693807e34 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 14:28:12 -0700 Subject: Split up proof in BarrettReduction.Z In particular, we do equality reasoning in one place and inequality reasoning in another. This makes it very clear how the inequality reasoning follows from the equality reasoning. --- src/ModularArithmetic/BarrettReduction/Z.v | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/ModularArithmetic/BarrettReduction/Z.v index 8b472d5d8..7ee51afaf 100644 --- a/src/ModularArithmetic/BarrettReduction/Z.v +++ b/src/ModularArithmetic/BarrettReduction/Z.v @@ -86,20 +86,23 @@ Section barrett. (** Also, if [a < n²] then [r < 2n]. *) (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *) Context (a_small : a < 4^k). + Lemma q_nice : { b : bool | q = a / n + if b then -1 else 0 }. + Proof. + assert (0 <= (4 ^ k * a / n) mod 4 ^ k < 4 ^ k) by auto with zarith lia. + assert (0 <= a * (4 ^ k mod n) / n < 4 ^ k) by (auto with zero_bounds zarith lia). + subst q r m. + rewrite (Z.div_mul_diff_exact''' (4^k) n a) by lia. + rewrite (Z_div_mod_eq (4^k * _ / n) (4^k)) by lia. + autorewrite with push_Zmul push_Zopp zsimplify zstrip_div. + eexists; reflexivity. + Qed. + Lemma r_small : r < 2 * n. Proof. - Hint Rewrite (Z.div_small a (4^k)) (Z.mod_small a (4^k)) using lia : zsimplify. Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. - cut (r + 1 <= 2 * n); [ lia | ]. - pose proof k_nonnegative; subst r q m. - assert (0 <= 2^(k-1)) by zero_bounds. - assert (4^k <> 0) by auto with zarith lia. assert (a mod n < n) by auto with zarith lia. - pose proof (Z.mod_pos_bound (a * 4^k / n) (4^k)). - transitivity (a - (a * 4 ^ k / n - a) / 4 ^ k * n + 1). - { rewrite <- (Z.mul_comm a); auto 6 with zarith lia. } - rewrite (Z_div_mod_eq (_ * 4^k / n) (4^k)) by lia. - autorewrite with push_Zmul push_Zopp zsimplify zstrip_div. + subst r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m. + autorewrite with push_Zmul zsimplify zstrip_div. break_match; auto with lia. Qed. -- cgit v1.2.3 From 7aa62e567ab15ac0ac11ed9d2a11333ba29084f0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 14:42:51 -0700 Subject: Add another lemma to zarith --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d26859ecc..50962cb4d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -14,7 +14,7 @@ Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. -Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl : zarith. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero : zarith. Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith. (** Only hints that are always safe to apply (i.e., reversible), and -- cgit v1.2.3