diff options
author | jadep <jade.philipoom@gmail.com> | 2016-07-21 18:07:14 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-07-21 18:07:14 -0400 |
commit | e880359898151f81383844b602df0c6df7f88ad1 (patch) | |
tree | fcb6156e041e8b2ac30a8c465d1b4d1280d236f0 | |
parent | b9c708c7887a6abf8243c55a3d32f0d0305eb794 (diff) | |
parent | 7aa62e567ab15ac0ac11ed9d2a11333ba29084f0 (diff) |
Merge branch 'master' of github.com:mit-plv/fiat-crypto
-rw-r--r-- | .mailmap | 1 | ||||
-rw-r--r-- | src/ModularArithmetic/BarrettReduction/Z.v | 23 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 105 |
3 files changed, 113 insertions, 16 deletions
@@ -7,6 +7,7 @@ Adam Chlipala <adamc@csail.mit.edu> Adam Chlipala <adam@c Andres Erbsen <andreser@mit.edu> Andres Erbsen <andreser@mit.edu> Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres@krutt.org> Jade Philipoom <jadep@mit.edu> Jade Philipoom <jadep@mit.edu> +Jade Philipoom <jadep@mit.edu> jadephilipoom <jade.philipoom@gmail.com> Jade Philipoom <jadep@mit.edu> jadep <jade.philipoom@gmail.com> Jade Philipoom <jadep@mit.edu> jadep <jadep@mit.edu> Jason Gross <jgross@mit.edu> Jason Gross <jagro@google.com> 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. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 9b487a773..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 @@ -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,35 @@ 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_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. + 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. @@ -654,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) <= @@ -918,6 +984,33 @@ 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; 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 <? y then -1 else 0. + Proof. + pose proof (Zlt_cases x y). + (destruct (x <? y) eqn:?); + 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. + + 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. |