diff options
-rw-r--r-- | src/Util/NatUtil.v | 56 | ||||
-rw-r--r-- | src/Util/NumTheoryUtil.v | 81 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 14 |
3 files changed, 151 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v new file mode 100644 index 000000000..afed2a231 --- /dev/null +++ b/src/Util/NatUtil.v @@ -0,0 +1,56 @@ +Require Import NPeano Omega. + +Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1. +Proof. + intros. + assert (b = 1 * b) by omega. + rewrite H0 at 1. + rewrite <- Nat.div_add by auto. + reflexivity. +Qed. + +Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2). +Proof. + assert (4 <> 0) as ne40 by omega. + induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. { + rewrite H0 in H1. + simpl in H1. + rewrite H1. + exists 0; auto. + } { + rewrite mult_succ_r in H1. + assert (4 <= x) as le4x by (apply Nat.div_str_pos_iff; omega). + rewrite <- Nat.add_1_r in H. + replace x with ((x - 4) + 4) in H by omega. + rewrite div_minus in H by auto. + apply Nat.add_cancel_r in H. + replace x with ((x - 4) + (1 * 4)) in H0 by omega. + rewrite Nat.mod_add in H0 by auto. + pose proof (IHc _ H H0). + destruct H2. + exists (x0 + 1). + rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto. + replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega. + apply Nat.add_cancel_r in H1. + replace (2 * (x0 + 1)) with (2 * x0 + 2) + by (rewrite Nat.mul_add_distr_l; auto). + rewrite H2. + rewrite <- Nat.div_add by omega. + f_equal. + simpl. + apply Nat.sub_add; auto. + } +Qed. + +Lemma Nat2N_inj_lt : forall n m, (N.of_nat n < N.of_nat m)%N <-> n < m. +Proof. + split; intros. { + rewrite nat_compare_lt. + rewrite Nnat.Nat2N.inj_compare. + rewrite N.compare_lt_iff; auto. + } { + rewrite <- N.compare_lt_iff. + rewrite <- Nnat.Nat2N.inj_compare. + rewrite <- nat_compare_lt; auto. + } +Qed. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v new file mode 100644 index 000000000..4a54e5437 --- /dev/null +++ b/src/Util/NumTheoryUtil.v @@ -0,0 +1,81 @@ +Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. +Require Import Omega NPeano Arith. +Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. +Local Open Scope Z. + +Lemma euler_criterion : forall (a x p : Z) (prime_p : prime p), + (x * 2 + 1 = p)%Z -> (a ^ x mod p = 1)%Z -> + exists b : Z, (0 <= b < p /\ b * b mod p = a)%Z. +Admitted. + +Lemma divide2_1mod4 : forall x, x mod 4 = 1 -> 0 <= x -> (2 | x / 2). +Proof. + intros. + assert (Z.to_nat x mod 4 = 1)%nat. { + replace 1%Z with (Z.of_nat 1) in H by auto. + replace (x mod 4)%Z with (Z.of_nat (Z.to_nat x mod 4)) in H + by (rewrite mod_Zmod by omega; rewrite Z2Nat.id; auto). + apply Nat2Z.inj in H; auto. + } + remember (Z.to_nat x / 4)%nat as c. + pose proof (divide2_1mod4_nat c (Z.to_nat x) Heqc H1). + destruct H2. + replace 2%nat with (Z.to_nat 2) in H2 by auto. + apply inj_eq in H2. + rewrite div_Zdiv in H2 by (replace (Z.to_nat 2) with 2%nat by auto; omega). + rewrite Nat2Z.inj_mul in H2. + do 2 rewrite Z2Nat.id in H2 by (auto || omega). + rewrite Z.mul_comm in H2. + symmetry in H2. + apply Zdivide_intro in H2; auto. +Qed. + +Lemma minus1_even_pow : forall x y, (2 | y) -> (1 < x) -> (0 <= y) -> ((x - 1) ^ y mod x = 1). +Proof. + intros. + apply Zdivide_Zdiv_eq in H; try omega. + rewrite H. + rewrite Z.pow_mul_r by omega. + assert ((x - 1)^2 mod x = 1). { + replace ((x - 1)^2) with (x ^ 2 - 2 * x + 1) + by (do 2 rewrite Z.pow_2_r; rewrite Z.mul_sub_distr_l; do 2 rewrite Z.mul_sub_distr_r; omega). + rewrite Zplus_mod. + rewrite Z.pow_2_r. + rewrite <- Z.mul_sub_distr_r. + rewrite Z_mod_mult. + do 2 rewrite Zmod_1_l by auto; auto. + } + rewrite <- (Z2Nat.id (y / 2)) by omega. + induction (Z.to_nat (y / 2)); try apply Zmod_1_l; auto. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite Zmult_mod. + rewrite IHn. + rewrite H2. + simpl. + apply Zmod_1_l; auto. +Qed. + +Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p), + (p mod 4 = 1)%Z -> exists b : Z, (0 <= b < p /\ b * b mod p = p - 1)%Z. +Proof. + intros. + assert (4 <> 0)%Z by omega. + pose proof (Z.div_mod p 4 H0). + pose proof (prime_ge_2 p (prime_p)). + assert (2 | p / 2)%Z by (apply divide2_1mod4; (auto || omega)). + apply (euler_criterion (p - 1) (p / 2) p prime_p); + [ | apply minus1_even_pow; (omega || auto); apply Z_div_pos; omega]. + rewrite <- H. + rewrite H1 at 3. + f_equal. + replace 4%Z with (2 * 2)%Z by auto. + rewrite <- Z.div_div by omega. + rewrite <- Zdivide_Zdiv_eq_2 by (auto || omega). + replace (2 * 2 * (p / 2) / 2)%Z with (2 * (2 * (p / 2)) / 2)%Z + by (f_equal; apply Z.mul_assoc). + rewrite ZUtil.Z_div_mul' by omega. + rewrite Z.mul_comm. + auto. +Qed. + diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5950f57ad..1a48abfd6 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,5 +1,7 @@ Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. Require Import Omega NPeano Arith. +Require Import Crypto.Util.NatUtil. +Require Import Bedrock.Word. Local Open Scope Z. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. @@ -50,3 +52,15 @@ Qed. Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0. intuition. Qed. + +Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)). +Proof. + induction n; intros; auto. + simpl pow2. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite untimes2. + rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega). + rewrite <- IHn. + auto. +Qed. |