diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-13 12:44:43 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-13 12:44:43 -0400 |
commit | 401058d999a6eaa38ce31b2ee9356a65b63498d2 (patch) | |
tree | 12d050078c95a25a8f00e982196bbe1e64989415 | |
parent | a30bbfe60d619e13601985340b1b70b150aecc28 (diff) |
Split off more ZUtil things
-rw-r--r-- | _CoqProject | 4 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 341 | ||||
-rw-r--r-- | src/Util/ZUtil/Div.v | 65 | ||||
-rw-r--r-- | src/Util/ZUtil/EquivModulo.v | 77 | ||||
-rw-r--r-- | src/Util/ZUtil/Modulo.v | 61 | ||||
-rw-r--r-- | src/Util/ZUtil/Quot.v | 104 | ||||
-rw-r--r-- | src/Util/ZUtil/Sgn.v | 12 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics.v | 1 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/RewriteModSmall.v | 47 |
9 files changed, 375 insertions, 337 deletions
diff --git a/_CoqProject b/_CoqProject index 1a15e0fc4..7d440951a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -295,12 +295,15 @@ src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v src/Util/ZUtil/Definitions.v src/Util/ZUtil/Div.v +src/Util/ZUtil/EquivModulo.v src/Util/ZUtil/Hints.v src/Util/ZUtil/Land.v src/Util/ZUtil/Modulo.v src/Util/ZUtil/Morphisms.v src/Util/ZUtil/Notations.v src/Util/ZUtil/Pow2Mod.v +src/Util/ZUtil/Quot.v +src/Util/ZUtil/Sgn.v src/Util/ZUtil/Stabilization.v src/Util/ZUtil/Tactics.v src/Util/ZUtil/Testbit.v @@ -317,6 +320,7 @@ src/Util/ZUtil/Tactics/LtbToLt.v src/Util/ZUtil/Tactics/PeelLe.v src/Util/ZUtil/Tactics/PrimeBound.v src/Util/ZUtil/Tactics/ReplaceNegWithPos.v +src/Util/ZUtil/Tactics/RewriteModSmall.v src/Util/ZUtil/Tactics/SimplifyFractionsLe.v src/Util/ZUtil/Tactics/ZeroBounds.v src/Util/ZUtil/Tactics/Ztestbit.v diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 8ada7afee..91e42598e 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -13,12 +13,15 @@ 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.EquivModulo. Require Export Crypto.Util.ZUtil.Hints. Require Export Crypto.Util.ZUtil.Land. Require Export Crypto.Util.ZUtil.Modulo. Require Export Crypto.Util.ZUtil.Morphisms. Require Export Crypto.Util.ZUtil.Notations. Require Export Crypto.Util.ZUtil.Pow2Mod. +Require Export Crypto.Util.ZUtil.Quot. +Require Export Crypto.Util.ZUtil.Sgn. Require Export Crypto.Util.ZUtil.Tactics. Require Export Crypto.Util.ZUtil.Testbit. Require Export Crypto.Util.ZUtil.ZSimplify. @@ -120,39 +123,6 @@ Module Z. 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). - Proof. - intros. - rewrite (Z_div_mod_eq a m) at 2 by auto. - ring. - Qed. - - Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. - Proof. - intros. - rewrite (Z_div_mod_eq a m) at 2 by auto. - ring. - Qed. - - Hint Rewrite mul_div_eq mul_div_eq' using zutil_arith : zdiv_to_mod. - Hint Rewrite <- mul_div_eq' using zutil_arith : zmod_to_div. - - Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m). - Proof. - intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. - Qed. - - Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod. - Hint Rewrite <-mul_div_eq_full using zutil_arith : zmod_to_div. - - Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. - Proof. - intros. - apply Z.div_small. - auto using Z.mod_pos_bound. - Qed. - Hint Rewrite mod_div_eq0 using zutil_arith : zsimplify. - Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). Proof. @@ -812,68 +782,6 @@ Module Z. Hint Resolve div_small_sym mod_small_sym : zarith. - Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. - Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. - - Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. - Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. - - Hint Rewrite div_add_l' div_add' using zutil_arith : zsimplify. - - Lemma div_sub a b c : c <> 0 -> (a - b * c) / c = a / c - b. - Proof. intros; rewrite <- !Z.add_opp_r, <- Z.div_add by lia; apply f_equal2; lia. Qed. - - Lemma div_sub' a b c : c <> 0 -> (a - c * b) / c = a / c - b. - Proof. intro; rewrite <- div_sub, (Z.mul_comm c); try lia. Qed. - - Hint Rewrite div_sub div_sub' using zutil_arith : zsimplify. - - Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. - Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. - - Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. - Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed. - - Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. - Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed. - - Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. - Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed. - - Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using zutil_arith : zsimplify. - - Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. - Proof. - intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. - autorewrite with zsimplify; reflexivity. - Qed. - - Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. - Proof. - intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. - autorewrite with zsimplify; reflexivity. - Qed. - - Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using zutil_arith : zsimplify. - - Lemma div_mul_skip_pow base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> x * base^e0 / y / base^e1 = x * base^(e0 - e1) / y. - Proof. - intros. - assert (0 < base^e1) by auto with zarith. - replace (base^e0) with (base^(e0 - e1) * base^e1) by (autorewrite with pull_Zpow zsimplify; reflexivity). - rewrite !Z.mul_assoc. - autorewrite with zsimplify; lia. - Qed. - Hint Rewrite div_mul_skip_pow using zutil_arith : zsimplify. - - Lemma div_mul_skip_pow' base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> base^e0 * x / y / base^e1 = base^(e0 - e1) * x / y. - Proof. - intros. - rewrite (Z.mul_comm (base^e0) x), div_mul_skip_pow by lia. - auto using f_equal2 with lia. - Qed. - Hint Rewrite div_mul_skip_pow' using zutil_arith : zsimplify. - Lemma mod_eq_le_to_eq a b : 0 < a <= b -> a mod b = 0 -> a = b. Proof. intros H H'. @@ -945,34 +853,6 @@ Module Z. Proof. reflexivity. Qed. Hint Rewrite <- two_p_two_eq_four : push_Zpow. - Lemma f_equal_mul_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x * y) mod m = (x' * y') mod m. - Proof. - intros H0 H1; rewrite Zmult_mod, H0, H1, <- Zmult_mod; reflexivity. - Qed. - Hint Resolve f_equal_mul_mod : zarith. - - Lemma f_equal_add_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x + y) mod m = (x' + y') mod m. - Proof. - intros H0 H1; rewrite Zplus_mod, H0, H1, <- Zplus_mod; reflexivity. - Qed. - Hint Resolve f_equal_add_mod : zarith. - - Lemma f_equal_opp_mod x x' m : x mod m = x' mod m -> (-x) mod m = (-x') mod m. - Proof. - intro H. - destruct (Z_zerop (x mod m)) as [H'|H'], (Z_zerop (x' mod m)) as [H''|H'']; - try congruence. - { rewrite !Z_mod_zero_opp_full by assumption; reflexivity. } - { rewrite Z_mod_nz_opp_full, H, <- Z_mod_nz_opp_full by assumption; reflexivity. } - Qed. - Hint Resolve f_equal_opp_mod : zarith. - - Lemma f_equal_sub_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x - y) mod m = (x' - y') mod m. - Proof. - rewrite <- !Z.add_opp_r; auto with zarith. - Qed. - Hint Resolve f_equal_sub_mod : zarith. - Lemma base_pow_neg b n : n < 0 -> b^n = 0. Proof. destruct n; intro H; try reflexivity; compute in H; congruence. @@ -1196,11 +1076,7 @@ Module Z. Hint Resolve div_sub_mod_cond : zarith. Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n. - Proof. - intros. - replace a with ((a - n * b) + n * b) by lia. - autorewrite with zsimplify; reflexivity. - Qed. + Proof. intros; Z.div_mod_to_quot_rem; nia. Qed. Hint Rewrite div_between using zutil_arith : zsimplify. Lemma mod_small_n n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a mod b = a - n * b. @@ -1652,46 +1528,6 @@ Module Z. { subst; cbv -[Z.le]; split; omega. } Qed. - Lemma mod_mod_small a n m - (Hnm : (m mod n = 0)%Z) - (Hnm_le : (0 < n <= m)%Z) - (H : (a mod m < n)%Z) - : ((a mod n) mod m = a mod m)%Z. - Proof. - assert ((a mod n) < m)%Z - by (eapply Z.lt_le_trans; [ apply Z.mod_pos_bound | ]; omega). - rewrite (Z.mod_small _ m) by auto with zarith. - apply Z.mod_divide in Hnm; [ | omega ]. - destruct Hnm as [x ?]; subst. - repeat match goal with - | [ H : context[(_ mod _)%Z] |- _ ] - => revert H - end. - Z.div_mod_to_quot_rem. - lazymatch goal with - | [ H : a = (?x * ?n * ?q) + _, H' : a = (?n * ?q') + _ |- _ ] - => assert (q' = x * q) by nia; subst q'; nia - end. - Qed. - - (** [rewrite_mod_small] is a better version of [rewrite Z.mod_small - by rewrite_mod_small_solver]; it backtracks across occurences - that the solver fails to solve the side-conditions on. *) - Ltac rewrite_mod_small_solver := - zutil_arith_more_inequalities. - Ltac rewrite_mod_small := - repeat match goal with - | [ |- context[?x mod ?y] ] - => rewrite (Z.mod_small x y) by rewrite_mod_small_solver - end. - Ltac rewrite_mod_mod_small := - repeat match goal with - | [ |- context[(?a mod ?n) mod ?m] ] - => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver - end. - Ltac rewrite_mod_small_more := - repeat (rewrite_mod_small || rewrite_mod_mod_small). - Lemma shiftl_le_Proper2 y : Proper (Z.le ==> Z.le) (fun x => Z.shiftl x y). Proof. @@ -1811,166 +1647,6 @@ Module Z. pose proof (Zlt_cases x 0). destruct (0 <=? x), (x <? 0); try omega. Qed. - - Lemma quot_div_full a b : Z.quot a b = Z.sgn a * Z.sgn b * (Z.abs a / Z.abs b). - Proof. - destruct (Z_zerop b); [ subst | apply Z.quot_div; assumption ]. - destruct a; simpl; reflexivity. - Qed. - - Lemma div_abs_sgn_nonneg a b : 0 <= Z.sgn (Z.abs a / Z.abs b). - Proof. - generalize (Zdiv_sgn (Z.abs a) (Z.abs b)). - destruct a, b; simpl; omega. - Qed. - Hint Resolve div_abs_sgn_nonneg : zarith. - - Local Arguments Z.mul !_ !_. - - Lemma quot_sgn_nonneg a b : 0 <= Z.sgn (Z.quot a b) * Z.sgn a * Z.sgn b. - Proof. - rewrite quot_div_full, !Z.sgn_mul, !Z.sgn_sgn. - set (d := Z.abs a / Z.abs b). - destruct a, b; simpl; try (subst d; simpl; omega); - try rewrite (Z.mul_opp_l 1); - do 2 try rewrite (Z.mul_opp_r _ 1); - rewrite ?Z.mul_1_l, ?Z.mul_1_r, ?Z.opp_involutive; - apply div_abs_sgn_nonneg. - Qed. - - Lemma quot_nonneg_same_sgn a b : Z.sgn a = Z.sgn b -> 0 <= Z.quot a b. - Proof. - intro H. - generalize (quot_sgn_nonneg a b); rewrite H. - rewrite <- Z.mul_assoc, <- Z.sgn_mul. - destruct (Z_zerop b); [ subst; destruct a; unfold Z.quot; simpl in *; congruence | ]. - rewrite (Z.sgn_pos (_ * _)) by nia. - intro; apply Z.sgn_nonneg; omega. - Qed. - - Lemma mul_quot_eq_full a m : m <> 0 -> m * (Z.quot a m) = a - a mod (Z.abs m * Z.sgn a). - Proof. - intro Hm. - assert (0 <> m * m) by (intro; apply Hm; nia). - assert (0 < m * m) by nia. - assert (0 <> Z.abs m) by (destruct m; simpl in *; try congruence). - rewrite quot_div_full. - rewrite <- (Z.abs_sgn m) at 1. - transitivity ((Z.sgn m * Z.sgn m) * Z.sgn a * (Z.abs m * (Z.abs a / Z.abs m))); [ nia | ]. - rewrite <- Z.sgn_mul, Z.sgn_pos, Z.mul_1_l, Z.mul_div_eq_full by omega. - rewrite Z.mul_sub_distr_l. - rewrite Z.mul_comm, Z.abs_sgn. - destruct a; simpl Z.sgn; simpl Z.abs; autorewrite with zsimplify_const; [ reflexivity | reflexivity | ]. - repeat match goal with |- context[-1 * ?x] => replace (-1 * x) with (-x) by omega end. - repeat match goal with |- context[?x * -1] => replace (x * -1) with (-x) by omega end. - rewrite <- Zmod_opp_opp; simpl Z.opp. - reflexivity. - Qed. - - Lemma quot_sub_sgn a : Z.quot (a - Z.sgn a) a = 0. - Proof. - rewrite quot_div_full. - destruct (Z_zerop a); subst; [ lia | ]. - rewrite Z.div_small; lia. - Qed. - - Lemma quot_small_abs a b : 0 <= Z.abs a < Z.abs b -> Z.quot a b = 0. - Proof. - intros; rewrite Z.quot_small_iff by lia; lia. - Qed. - - Lemma quot_add_sub_sgn_small a b : b <> 0 -> Z.sgn a = Z.sgn b -> Z.quot (a + b - Z.sgn b) b = Z.quot (a - Z.sgn b) b + 1. - Proof. - destruct (Z_zerop a), (Z_zerop b), (Z_lt_le_dec a 0), (Z_lt_le_dec b 0), (Z_lt_le_dec 1 (Z.abs a)); - subst; - try lia; - rewrite !Z.quot_div_full; - try rewrite (Z.sgn_neg a) by omega; - try rewrite (Z.sgn_neg b) by omega; - repeat first [ reflexivity - | rewrite Z.sgn_neg by lia - | rewrite Z.sgn_pos by lia - | rewrite Z.abs_eq by lia - | rewrite Z.abs_neq by lia - | rewrite !Z.mul_opp_l - | rewrite Z.abs_opp in * - | rewrite Z.abs_eq in * by omega - | match goal with - | [ |- context[-1 * ?x] ] - => replace (-1 * x) with (-x) by omega - | [ |- context[?x * -1] ] - => replace (x * -1) with (-x) by omega - | [ |- context[-?x - ?y] ] - => replace (-x - y) with (-(x + y)) by omega - | [ |- context[-?x + - ?y] ] - => replace (-x + - y) with (-(x + y)) by omega - | [ |- context[(?a + ?b + ?c) / ?b] ] - => replace (a + b + c) with (((a + c) + b * 1)) by lia; rewrite Z.div_add' by omega - | [ |- context[(?a + ?b - ?c) / ?b] ] - => replace (a + b - c) with (((a - c) + b * 1)) by lia; rewrite Z.div_add' by omega - end - | progress intros - | progress Z.replace_all_neg_with_pos - | progress autorewrite with zsimplify ]. - Qed. - - Section equiv_modulo. - Context (N : Z). - Definition equiv_modulo x y := x mod N = y mod N. - Local Infix "==" := equiv_modulo. - - Local Instance equiv_modulo_Reflexive : Reflexive equiv_modulo := fun _ => Logic.eq_refl. - Local Instance equiv_modulo_Symmetric : Symmetric equiv_modulo := fun _ _ => @Logic.eq_sym _ _ _. - Local Instance equiv_modulo_Transitive : Transitive equiv_modulo := fun _ _ _ => @Logic.eq_trans _ _ _ _. - - Local Instance mul_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.mul. - Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. - - Local Instance add_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.add. - Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. - - Local Instance sub_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.sub. - Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. - - Local Instance opp_mod_Proper : Proper (equiv_modulo ==> equiv_modulo) Z.opp. - Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. - - Local Instance modulo_equiv_modulo_Proper - : Proper (equiv_modulo ==> (fun x y => x = N /\ N = y) ==> Logic.eq) Z.modulo. - Proof. - repeat intro; hnf in *; intuition congruence. - Qed. - Local Instance eq_to_ProperProxy : ProperProxy (fun x y : Z => x = N /\ N = y) N. - Proof. split; reflexivity. Qed. - - Lemma div_to_inv_modulo a x x' : x > 0 -> x * x' mod N = 1 mod N -> (a / x) == ((a - a mod x) * x'). - Proof using Type. - intros H xinv. - replace (a / x) with ((a / x) * 1) by lia. - change (x * x' == 1) in xinv. - rewrite <- xinv. - replace ((a / x) * (x * x')) with ((x * (a / x)) * x') by lia. - rewrite Z.mul_div_eq by assumption. - reflexivity. - Qed. - End equiv_modulo. - Hint Rewrite div_to_inv_modulo using solve [ eassumption | lia ] : zstrip_div. - - Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *) - Existing Instance equiv_modulo_Reflexive. - Existing Instance eq_Reflexive. (* prioritize [Reflexive eq] *) - Existing Instance equiv_modulo_Symmetric. - Existing Instance equiv_modulo_Transitive. - Existing Instance mul_mod_Proper. - Existing Instance add_mod_Proper. - Existing Instance sub_mod_Proper. - Existing Instance opp_mod_Proper. - Existing Instance modulo_equiv_modulo_Proper. - Existing Instance eq_to_ProperProxy. - End EquivModuloInstances. - Module RemoveEquivModuloInstances (dummy : Nop). - Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances. - End RemoveEquivModuloInstances. End Z. Module N2Z. @@ -2107,12 +1783,3 @@ Ltac pull_Zmod := => rewrite (Zmod_mod x z) | _ => progress autorewrite with pull_Zmod end. - -(** Change [_ mod _ = _ mod _] to [Z.equiv_modulo _ _ _] *) -Ltac Zmod_to_equiv_modulo := - repeat match goal with - | [ H : context T[?x mod ?M = ?y mod ?M] |- _ ] - => let T' := context T[Z.equiv_modulo M x y] in change T' in H - | [ |- context T[?x mod ?M = ?y mod ?M] ] - => let T' := context T[Z.equiv_modulo M x y] in change T' - end. diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 325818a2c..b054ec8e5 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -1,6 +1,9 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn. Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. Local Open Scope Z_scope. Module Z. @@ -33,4 +36,66 @@ Module Z. | [ x : Z |- _ ] => destruct x end ]. Qed. + + Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. + Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. + + Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. + Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. + + Hint Rewrite div_add_l' div_add' using zutil_arith : zsimplify. + + Lemma div_sub a b c : c <> 0 -> (a - b * c) / c = a / c - b. + Proof. intros; rewrite <- !Z.add_opp_r, <- Z.div_add by lia; apply f_equal2; lia. Qed. + + Lemma div_sub' a b c : c <> 0 -> (a - c * b) / c = a / c - b. + Proof. intro; rewrite <- div_sub, (Z.mul_comm c); try lia. Qed. + + Hint Rewrite div_sub div_sub' using zutil_arith : zsimplify. + + Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b. + Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed. + + Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b. + Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed. + + Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b. + Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed. + + Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b. + Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed. + + Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using zutil_arith : zsimplify. + + Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify. reflexivity. + Qed. + + Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia. + autorewrite with zsimplify; reflexivity. + Qed. + + Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using zutil_arith : zsimplify. + + Lemma div_mul_skip_pow base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> x * base^e0 / y / base^e1 = x * base^(e0 - e1) / y. + Proof. + intros. + assert (0 < base^e1) by auto with zarith. + replace (base^e0) with (base^(e0 - e1) * base^e1) by (autorewrite with pull_Zpow zsimplify; reflexivity). + rewrite !Z.mul_assoc. + autorewrite with zsimplify; lia. + Qed. + Hint Rewrite div_mul_skip_pow using zutil_arith : zsimplify. + + Lemma div_mul_skip_pow' base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> base^e0 * x / y / base^e1 = base^(e0 - e1) * x / y. + Proof. + intros. + rewrite (Z.mul_comm (base^e0) x), div_mul_skip_pow by lia. + auto using f_equal2 with lia. + Qed. + Hint Rewrite div_mul_skip_pow' using zutil_arith : zsimplify. End Z. diff --git a/src/Util/ZUtil/EquivModulo.v b/src/Util/ZUtil/EquivModulo.v new file mode 100644 index 000000000..93de3f267 --- /dev/null +++ b/src/Util/ZUtil/EquivModulo.v @@ -0,0 +1,77 @@ +Require Import Coq.Classes.Morphisms. +Require Import Coq.Structures.Equalities. +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Modulo. +Local Open Scope Z_scope. + +Module Z. + Section equiv_modulo. + Context (N : Z). + Definition equiv_modulo x y := x mod N = y mod N. + Local Infix "==" := equiv_modulo. + + Local Instance equiv_modulo_Reflexive : Reflexive equiv_modulo := fun _ => Logic.eq_refl. + Local Instance equiv_modulo_Symmetric : Symmetric equiv_modulo := fun _ _ => @Logic.eq_sym _ _ _. + Local Instance equiv_modulo_Transitive : Transitive equiv_modulo := fun _ _ _ => @Logic.eq_trans _ _ _ _. + + Local Instance mul_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.mul. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Local Instance add_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.add. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Local Instance sub_mod_Proper : Proper (equiv_modulo ==> equiv_modulo ==> equiv_modulo) Z.sub. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Local Instance opp_mod_Proper : Proper (equiv_modulo ==> equiv_modulo) Z.opp. + Proof. unfold equiv_modulo, Proper, respectful; auto with zarith. Qed. + + Local Instance modulo_equiv_modulo_Proper + : Proper (equiv_modulo ==> (fun x y => x = N /\ N = y) ==> Logic.eq) Z.modulo. + Proof. + repeat intro; hnf in *; intuition congruence. + Qed. + Local Instance eq_to_ProperProxy : ProperProxy (fun x y : Z => x = N /\ N = y) N. + Proof. split; reflexivity. Qed. + + Lemma div_to_inv_modulo a x x' : x > 0 -> x * x' mod N = 1 mod N -> (a / x) == ((a - a mod x) * x'). + Proof using Type. + intros H xinv. + replace (a / x) with ((a / x) * 1) by lia. + change (x * x' == 1) in xinv. + rewrite <- xinv. + replace ((a / x) * (x * x')) with ((x * (a / x)) * x') by lia. + rewrite Z.mul_div_eq by assumption. + reflexivity. + Qed. + End equiv_modulo. + Hint Rewrite div_to_inv_modulo using solve [ eassumption | lia ] : zstrip_div. + + Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *) + Existing Instance equiv_modulo_Reflexive. + Existing Instance eq_Reflexive. (* prioritize [Reflexive eq] *) + Existing Instance equiv_modulo_Symmetric. + Existing Instance equiv_modulo_Transitive. + Existing Instance mul_mod_Proper. + Existing Instance add_mod_Proper. + Existing Instance sub_mod_Proper. + Existing Instance opp_mod_Proper. + Existing Instance modulo_equiv_modulo_Proper. + Existing Instance eq_to_ProperProxy. + End EquivModuloInstances. + Module RemoveEquivModuloInstances (dummy : Nop). + Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances. + End RemoveEquivModuloInstances. +End Z. + +(** Change [_ mod _ = _ mod _] to [Z.equiv_modulo _ _ _] *) +Ltac Zmod_to_equiv_modulo := + repeat match goal with + | [ H : context T[?x mod ?M = ?y mod ?M] |- _ ] + => let T' := context T[Z.equiv_modulo M x y] in change T' in H + | [ |- context T[?x mod ?M = ?y mod ?M] ] + => let T' := context T[Z.equiv_modulo M x y] in change T' + end. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 42f85ae90..88d201c03 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -83,4 +83,65 @@ Module Z. rewrite <-H by (change 0%nat with (Z.to_nat 0); rewrite Z2Nat.inj_iff; omega). rewrite !Nat2Z.id; reflexivity. Qed. + + Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m). + Proof. + intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring. + Qed. + + Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod. + Hint Rewrite <-mul_div_eq_full using zutil_arith : zmod_to_div. + + Lemma f_equal_mul_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x * y) mod m = (x' * y') mod m. + Proof. + intros H0 H1; rewrite Zmult_mod, H0, H1, <- Zmult_mod; reflexivity. + Qed. + Hint Resolve f_equal_mul_mod : zarith. + + Lemma f_equal_add_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x + y) mod m = (x' + y') mod m. + Proof. + intros H0 H1; rewrite Zplus_mod, H0, H1, <- Zplus_mod; reflexivity. + Qed. + Hint Resolve f_equal_add_mod : zarith. + + Lemma f_equal_opp_mod x x' m : x mod m = x' mod m -> (-x) mod m = (-x') mod m. + Proof. + intro H. + destruct (Z_zerop (x mod m)) as [H'|H'], (Z_zerop (x' mod m)) as [H''|H'']; + try congruence. + { rewrite !Z_mod_zero_opp_full by assumption; reflexivity. } + { rewrite Z_mod_nz_opp_full, H, <- Z_mod_nz_opp_full by assumption; reflexivity. } + Qed. + Hint Resolve f_equal_opp_mod : zarith. + + Lemma f_equal_sub_mod x y x' y' m : x mod m = x' mod m -> y mod m = y' mod m -> (x - y) mod m = (x' - y') mod m. + Proof. + rewrite <- !Z.add_opp_r; auto with zarith. + Qed. + Hint Resolve f_equal_sub_mod : zarith. + + Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m). + Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. + Qed. + + Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z. + Proof. + intros. + rewrite (Z_div_mod_eq a m) at 2 by auto. + ring. + Qed. + + Hint Rewrite mul_div_eq mul_div_eq' using zutil_arith : zdiv_to_mod. + Hint Rewrite <- mul_div_eq' using zutil_arith : zmod_to_div. + + Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0. + Proof. + intros. + apply Z.div_small. + auto using Z.mod_pos_bound. + Qed. + Hint Rewrite mod_div_eq0 using zutil_arith : zsimplify. End Z. diff --git a/src/Util/ZUtil/Quot.v b/src/Util/ZUtil/Quot.v new file mode 100644 index 000000000..0c8a3361d --- /dev/null +++ b/src/Util/ZUtil/Quot.v @@ -0,0 +1,104 @@ +Require Import Coq.ZArith.ZArith Coq.omega.Omega Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Sgn. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Local Open Scope Z_scope. + +Module Z. + Lemma quot_div_full a b : Z.quot a b = Z.sgn a * Z.sgn b * (Z.abs a / Z.abs b). + Proof. + destruct (Z_zerop b); [ subst | apply Z.quot_div; assumption ]. + destruct a; simpl; reflexivity. + Qed. + + Local Arguments Z.mul !_ !_. + + Lemma quot_sgn_nonneg a b : 0 <= Z.sgn (Z.quot a b) * Z.sgn a * Z.sgn b. + Proof. + rewrite quot_div_full, !Z.sgn_mul, !Z.sgn_sgn. + set (d := Z.abs a / Z.abs b). + destruct a, b; simpl; try (subst d; simpl; omega); + try rewrite (Z.mul_opp_l 1); + do 2 try rewrite (Z.mul_opp_r _ 1); + rewrite ?Z.mul_1_l, ?Z.mul_1_r, ?Z.opp_involutive; + apply Z.div_abs_sgn_nonneg. + Qed. + + Lemma quot_nonneg_same_sgn a b : Z.sgn a = Z.sgn b -> 0 <= Z.quot a b. + Proof. + intro H. + generalize (quot_sgn_nonneg a b); rewrite H. + rewrite <- Z.mul_assoc, <- Z.sgn_mul. + destruct (Z_zerop b); [ subst; destruct a; unfold Z.quot; simpl in *; congruence | ]. + rewrite (Z.sgn_pos (_ * _)) by nia. + intro; apply Z.sgn_nonneg; omega. + Qed. + + Lemma mul_quot_eq_full a m : m <> 0 -> m * (Z.quot a m) = a - a mod (Z.abs m * Z.sgn a). + Proof. + intro Hm. + assert (0 <> m * m) by (intro; apply Hm; nia). + assert (0 < m * m) by nia. + assert (0 <> Z.abs m) by (destruct m; simpl in *; try congruence). + rewrite quot_div_full. + rewrite <- (Z.abs_sgn m) at 1. + transitivity ((Z.sgn m * Z.sgn m) * Z.sgn a * (Z.abs m * (Z.abs a / Z.abs m))); [ nia | ]. + rewrite <- Z.sgn_mul, Z.sgn_pos, Z.mul_1_l, Z.mul_div_eq_full by omega. + rewrite Z.mul_sub_distr_l. + rewrite Z.mul_comm, Z.abs_sgn. + destruct a; simpl Z.sgn; simpl Z.abs; autorewrite with zsimplify_const; [ reflexivity | reflexivity | ]. + repeat match goal with |- context[-1 * ?x] => replace (-1 * x) with (-x) by omega end. + repeat match goal with |- context[?x * -1] => replace (x * -1) with (-x) by omega end. + rewrite <- Zmod_opp_opp; simpl Z.opp. + reflexivity. + Qed. + + Lemma quot_sub_sgn a : Z.quot (a - Z.sgn a) a = 0. + Proof. + rewrite quot_div_full. + destruct (Z_zerop a); subst; [ lia | ]. + rewrite Z.div_small; lia. + Qed. + + Lemma quot_small_abs a b : 0 <= Z.abs a < Z.abs b -> Z.quot a b = 0. + Proof. + intros; rewrite Z.quot_small_iff by lia; lia. + Qed. + + Lemma quot_add_sub_sgn_small a b : b <> 0 -> Z.sgn a = Z.sgn b -> Z.quot (a + b - Z.sgn b) b = Z.quot (a - Z.sgn b) b + 1. + Proof. + destruct (Z_zerop a), (Z_zerop b), (Z_lt_le_dec a 0), (Z_lt_le_dec b 0), (Z_lt_le_dec 1 (Z.abs a)); + subst; + try lia; + rewrite !Z.quot_div_full; + try rewrite (Z.sgn_neg a) by omega; + try rewrite (Z.sgn_neg b) by omega; + repeat first [ reflexivity + | rewrite Z.sgn_neg by lia + | rewrite Z.sgn_pos by lia + | rewrite Z.abs_eq by lia + | rewrite Z.abs_neq by lia + | rewrite !Z.mul_opp_l + | rewrite Z.abs_opp in * + | rewrite Z.abs_eq in * by omega + | match goal with + | [ |- context[-1 * ?x] ] + => replace (-1 * x) with (-x) by omega + | [ |- context[?x * -1] ] + => replace (x * -1) with (-x) by omega + | [ |- context[-?x - ?y] ] + => replace (-x - y) with (-(x + y)) by omega + | [ |- context[-?x + - ?y] ] + => replace (-x + - y) with (-(x + y)) by omega + | [ |- context[(?a + ?b + ?c) / ?b] ] + => replace (a + b + c) with (((a + c) + b * 1)) by lia; rewrite Z.div_add' by omega + | [ |- context[(?a + ?b - ?c) / ?b] ] + => replace (a + b - c) with (((a - c) + b * 1)) by lia; rewrite Z.div_add' by omega + end + | progress intros + | progress Z.replace_all_neg_with_pos + | progress autorewrite with zsimplify ]. + Qed. +End Z. diff --git a/src/Util/ZUtil/Sgn.v b/src/Util/ZUtil/Sgn.v new file mode 100644 index 000000000..a3e6182bc --- /dev/null +++ b/src/Util/ZUtil/Sgn.v @@ -0,0 +1,12 @@ +Require Import Coq.ZArith.ZArith Coq.omega.Omega. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma div_abs_sgn_nonneg a b : 0 <= Z.sgn (Z.abs a / Z.abs b). + Proof. + generalize (Zdiv_sgn (Z.abs a) (Z.abs b)). + destruct a, b; simpl; omega. + Qed. + Hint Resolve div_abs_sgn_nonneg : zarith. +End Z. diff --git a/src/Util/ZUtil/Tactics.v b/src/Util/ZUtil/Tactics.v index 3700611df..7dfb8ff46 100644 --- a/src/Util/ZUtil/Tactics.v +++ b/src/Util/ZUtil/Tactics.v @@ -6,6 +6,7 @@ Require Export Crypto.Util.ZUtil.Tactics.LtbToLt. Require Export Crypto.Util.ZUtil.Tactics.PeelLe. Require Export Crypto.Util.ZUtil.Tactics.PrimeBound. Require Export Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Export Crypto.Util.ZUtil.Tactics.RewriteModSmall. Require Export Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe. Require Export Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Export Crypto.Util.ZUtil.Tactics.Ztestbit. diff --git a/src/Util/ZUtil/Tactics/RewriteModSmall.v b/src/Util/ZUtil/Tactics/RewriteModSmall.v new file mode 100644 index 000000000..45598b0c5 --- /dev/null +++ b/src/Util/ZUtil/Tactics/RewriteModSmall.v @@ -0,0 +1,47 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Local Open Scope Z_scope. + +Module Z. + Lemma mod_mod_small a n m + (Hnm : (m mod n = 0)%Z) + (Hnm_le : (0 < n <= m)%Z) + (H : (a mod m < n)%Z) + : ((a mod n) mod m = a mod m)%Z. + Proof. + assert ((a mod n) < m)%Z + by (eapply Z.lt_le_trans; [ apply Z.mod_pos_bound | ]; omega). + rewrite (Z.mod_small _ m) by auto with zarith. + apply Z.mod_divide in Hnm; [ | omega ]. + destruct Hnm as [x ?]; subst. + repeat match goal with + | [ H : context[(_ mod _)%Z] |- _ ] + => revert H + end. + Z.div_mod_to_quot_rem. + lazymatch goal with + | [ H : a = (?x * ?n * ?q) + _, H' : a = (?n * ?q') + _ |- _ ] + => assert (q' = x * q) by nia; subst q'; nia + end. + Qed. + + (** [rewrite_mod_small] is a better version of [rewrite Z.mod_small + by rewrite_mod_small_solver]; it backtracks across occurences + that the solver fails to solve the side-conditions on. *) + Ltac rewrite_mod_small_solver := + zutil_arith_more_inequalities. + Ltac rewrite_mod_small := + repeat match goal with + | [ |- context[?x mod ?y] ] + => rewrite (Z.mod_small x y) by rewrite_mod_small_solver + end. + Ltac rewrite_mod_mod_small := + repeat match goal with + | [ |- context[(?a mod ?n) mod ?m] ] + => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver + end. + Ltac rewrite_mod_small_more := + repeat (rewrite_mod_small || rewrite_mod_mod_small). +End Z. |