diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-13 12:14:27 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-13 12:14:27 -0400 |
commit | a30bbfe60d619e13601985340b1b70b150aecc28 (patch) | |
tree | 778062d35ecd7beb8f5c3a8e6fcc2292e1ade3af | |
parent | 6e5dfa6ad6aca6aa19b7d1348817bd2c23d8fdad (diff) |
Split off more of ZUtil
-rw-r--r-- | _CoqProject | 3 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 136 | ||||
-rw-r--r-- | src/Util/ZUtil/Land.v | 13 | ||||
-rw-r--r-- | src/Util/ZUtil/Modulo.v | 86 | ||||
-rw-r--r-- | src/Util/ZUtil/Pow2Mod.v | 54 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/DivModToQuotRem.v | 4 |
6 files changed, 161 insertions, 135 deletions
diff --git a/_CoqProject b/_CoqProject index 56d473b25..1a15e0fc4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -296,8 +296,11 @@ src/Util/Tactics/VM.v src/Util/ZUtil/Definitions.v src/Util/ZUtil/Div.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/Stabilization.v src/Util/ZUtil/Tactics.v src/Util/ZUtil/Testbit.v diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 9a2b7b838..8ada7afee 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -14,8 +14,11 @@ Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.ZUtil.Definitions. Require Export Crypto.Util.ZUtil.Div. 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.Tactics. Require Export Crypto.Util.ZUtil.Testbit. Require Export Crypto.Util.ZUtil.ZSimplify. @@ -23,58 +26,6 @@ Import Nat. Local Open Scope Z. Module Z. - Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b). - Proof. - intros. - unfold Z.pow2_mod. - rewrite Z.land_ones; auto. - Qed. - Hint Rewrite <- Z.pow2_mod_spec using zutil_arith : convert_to_Ztestbit. - - Lemma pow2_mod_0_r : forall a, Z.pow2_mod a 0 = 0. - Proof. - intros; rewrite Z.pow2_mod_spec, Z.mod_1_r; reflexivity. - Qed. - - Lemma pow2_mod_0_l : forall n, 0 <= n -> Z.pow2_mod 0 n = 0. - Proof. - intros; rewrite Z.pow2_mod_spec, Z.mod_0_l; try reflexivity; try apply Z.pow_nonzero; omega. - Qed. - - Lemma pow2_mod_split : forall a n m, 0 <= n -> 0 <= m -> - Z.pow2_mod a (n + m) = Z.lor (Z.pow2_mod a n) ((Z.pow2_mod (a >> n) m) << n). - Proof. - intros; cbv [Z.pow2_mod]. - apply Z.bits_inj'; intros. - repeat progress (try break_match; autorewrite with Ztestbit zsimplify; try reflexivity). - try match goal with H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] => - rewrite !Z.testbit_neg_r with (n := a - b) by omega end. - autorewrite with Ztestbit; reflexivity. - Qed. - - Lemma pow2_mod_pow2_mod : forall a n m, 0 <= n -> 0 <= m -> - Z.pow2_mod (Z.pow2_mod a n) m = Z.pow2_mod a (Z.min n m). - Proof. - intros; cbv [Z.pow2_mod]. - apply Z.bits_inj'; intros. - apply Z.min_case_strong; intros; repeat progress (try break_match; autorewrite with Ztestbit zsimplify; try reflexivity). - Qed. - - Lemma pow2_mod_pos_bound a b : 0 < b -> 0 <= Z.pow2_mod a b < 2^b. - Proof. - intros; rewrite Z.pow2_mod_spec by omega. - auto with zarith. - Qed. - Hint Resolve pow2_mod_pos_bound : zarith. - - Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. - Proof. - intros; apply Z.bits_inj'; intros. - rewrite !Z.land_spec. - case_eq (Z.testbit b n); intros; - rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. - 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. @@ -84,7 +35,6 @@ Module Z. 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 -> @@ -96,40 +46,6 @@ Module Z. apply Z.divide_pos_le; try (apply Zmod_divide); omega. Qed. - Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. - Proof. intros; subst; auto. Qed. - - Hint Resolve elim_mod : zarith. - - Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c. - Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. - Hint Rewrite mod_add_full : zsimplify. - - Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b. - Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. - Hint Rewrite mod_add_l_full : zsimplify. - - Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b. - Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. - Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a. - Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. - Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify. - - Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. - Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. - - Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. - Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. - Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. - Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. - - Lemma add_pow_mod_l : forall a b c, a <> 0 -> 0 < b -> - ((a ^ b) + c) mod a = c mod a. - Proof. - intros; replace b with (b - 1 + 1) by ring; - rewrite Z.pow_add_r, Z.pow_1_r by omega; auto using Z.mod_add_l. - Qed. - Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. Proof. @@ -160,52 +76,6 @@ Module Z. Hint Rewrite pow_Zpow : push_Zof_nat. Hint Rewrite <- pow_Zpow : pull_Zof_nat. - Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> - a ^ x mod m = 0. - Proof. - intros. - replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). - induction (Z.to_nat x). { - simpl in *; omega. - } { - rewrite Nat2Z.inj_succ in *. - rewrite Z.pow_succ_r by omega. - rewrite Z.mul_mod by omega. - case_eq n; intros. { - subst. simpl. - rewrite Zmod_1_l by omega. - rewrite H1. - apply Zmod_0_l. - } { - subst. - rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). - rewrite H1. - auto. - } - } - Qed. - - Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> - a ^ b mod m = (a mod m) ^ b mod m. - Proof. - intros; rewrite <- (Z2Nat.id b) by auto. - induction (Z.to_nat b); auto. - rewrite Nat2Z.inj_succ. - do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. - rewrite Z.mul_mod by auto. - rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. - rewrite <- IHn by auto. - rewrite Z.mod_mod by auto. - reflexivity. - Qed. - - Lemma mod_to_nat x m (Hm:(0 < m)%Z) (Hx:(0 <= x)%Z) : (Z.to_nat x mod Z.to_nat m = Z.to_nat (x mod m))%nat. - pose proof Zdiv.mod_Zmod (Z.to_nat x) (Z.to_nat m) as H; - rewrite !Z2Nat.id in H by omega. - rewrite <-H by (change 0%nat with (Z.to_nat 0); rewrite Z2Nat.inj_iff; omega). - rewrite !Nat2Z.id; reflexivity. - Qed. - Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), (a | b * (a / c)) -> (c | a) -> (c | b). Proof. diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v new file mode 100644 index 000000000..b3d3f3727 --- /dev/null +++ b/src/Util/ZUtil/Land.v @@ -0,0 +1,13 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Notations. +Local Open Scope Z_scope. + +Module Z. + Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. + Proof. + intros; apply Z.bits_inj'; intros. + rewrite !Z.land_spec. + case_eq (Z.testbit b n); intros; + rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. + Qed. +End Z. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v new file mode 100644 index 000000000..42f85ae90 --- /dev/null +++ b/src/Util/ZUtil/Modulo.v @@ -0,0 +1,86 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.ZArith.Znumtheory. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Local Open Scope Z_scope. + +Module Z. + Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m. + Proof. intros; subst; auto. Qed. + Hint Resolve elim_mod : zarith. + + Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c. + Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add_full : zsimplify. + + Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b. + Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add_l_full : zsimplify. + + Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b. + Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a. + Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify. + + Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b. + Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + + Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b. + Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed. + Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a. + Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed. + + Lemma add_pow_mod_l : forall a b c, a <> 0 -> 0 < b -> + ((a ^ b) + c) mod a = c mod a. + Proof. + intros; replace b with (b - 1 + 1) by ring; + rewrite Z.pow_add_r, Z.pow_1_r by omega; auto using Z.mod_add_l. + Qed. + + Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> + a ^ x mod m = 0. + Proof. + intros. + replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). + induction (Z.to_nat x). { + simpl in *; omega. + } { + rewrite Nat2Z.inj_succ in *. + rewrite Z.pow_succ_r by omega. + rewrite Z.mul_mod by omega. + case_eq n; intros. { + subst. simpl. + rewrite Zmod_1_l by omega. + rewrite H1. + apply Zmod_0_l. + } { + subst. + rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). + rewrite H1. + auto. + } + } + Qed. + + Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> + a ^ b mod m = (a mod m) ^ b mod m. + Proof. + intros; rewrite <- (Z2Nat.id b) by auto. + induction (Z.to_nat b); auto. + rewrite Nat2Z.inj_succ. + do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. + rewrite Z.mul_mod by auto. + rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. + rewrite <- IHn by auto. + rewrite Z.mod_mod by auto. + reflexivity. + Qed. + + Lemma mod_to_nat x m (Hm:(0 < m)%Z) (Hx:(0 <= x)%Z) : (Z.to_nat x mod Z.to_nat m = Z.to_nat (x mod m))%nat. + pose proof Zdiv.mod_Zmod (Z.to_nat x) (Z.to_nat m) as H; + rewrite !Z2Nat.id in H by omega. + rewrite <-H by (change 0%nat with (Z.to_nat 0); rewrite Z2Nat.inj_iff; omega). + rewrite !Nat2Z.id; reflexivity. + Qed. +End Z. diff --git a/src/Util/ZUtil/Pow2Mod.v b/src/Util/ZUtil/Pow2Mod.v new file mode 100644 index 000000000..237ca19dc --- /dev/null +++ b/src/Util/ZUtil/Pow2Mod.v @@ -0,0 +1,54 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.Ztestbit. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.Tactics.BreakMatch. +Local Open Scope Z_scope. + +Module Z. + Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b). + Proof. + intros. + unfold Z.pow2_mod. + rewrite Z.land_ones; auto. + Qed. + Hint Rewrite <- Z.pow2_mod_spec using zutil_arith : convert_to_Ztestbit. + + Lemma pow2_mod_0_r : forall a, Z.pow2_mod a 0 = 0. + Proof. + intros; rewrite Z.pow2_mod_spec, Z.mod_1_r; reflexivity. + Qed. + + Lemma pow2_mod_0_l : forall n, 0 <= n -> Z.pow2_mod 0 n = 0. + Proof. + intros; rewrite Z.pow2_mod_spec, Z.mod_0_l; try reflexivity; try apply Z.pow_nonzero; omega. + Qed. + + Lemma pow2_mod_split : forall a n m, 0 <= n -> 0 <= m -> + Z.pow2_mod a (n + m) = Z.lor (Z.pow2_mod a n) ((Z.pow2_mod (a >> n) m) << n). + Proof. + intros; cbv [Z.pow2_mod]. + apply Z.bits_inj'; intros. + repeat progress (try break_match; autorewrite with Ztestbit zsimplify; try reflexivity). + try match goal with H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] => + rewrite !Z.testbit_neg_r with (n := a - b) by omega end. + autorewrite with Ztestbit; reflexivity. + Qed. + + Lemma pow2_mod_pow2_mod : forall a n m, 0 <= n -> 0 <= m -> + Z.pow2_mod (Z.pow2_mod a n) m = Z.pow2_mod a (Z.min n m). + Proof. + intros; cbv [Z.pow2_mod]. + apply Z.bits_inj'; intros. + apply Z.min_case_strong; intros; repeat progress (try break_match; autorewrite with Ztestbit zsimplify; try reflexivity). + Qed. + + Lemma pow2_mod_pos_bound a b : 0 < b -> 0 <= Z.pow2_mod a b < 2^b. + Proof. + intros; rewrite Z.pow2_mod_spec by omega. + auto with zarith. + Qed. + Hint Resolve pow2_mod_pos_bound : zarith. +End Z. diff --git a/src/Util/ZUtil/Tactics/DivModToQuotRem.v b/src/Util/ZUtil/Tactics/DivModToQuotRem.v index b37047397..178844d3b 100644 --- a/src/Util/ZUtil/Tactics/DivModToQuotRem.v +++ b/src/Util/ZUtil/Tactics/DivModToQuotRem.v @@ -26,8 +26,8 @@ Module Z. clear H'; revert H'' ]; let q := fresh "q" in let r := fresh "r" in - set (q := x / y); - set (r := x mod y); + set (q := x / y) in *; + set (r := x mod y) in *; clearbody q r. Ltac div_mod_to_quot_rem_step := |