From 9cd94e813572b183245b67d6c621af847601478d Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Sat, 23 Jan 2016 15:16:50 -0500 Subject: NumTheoryUtil : code cleanup; moved some lemmas to ZUtil. --- src/Util/NumTheoryUtil.v | 509 ++++++++++++----------------------------------- 1 file changed, 126 insertions(+), 383 deletions(-) (limited to 'src/Util/NumTheoryUtil.v') diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 251f120b0..4f673b545 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -5,270 +5,7 @@ Require Import Coqprime.Zp. Require Import VerdiTactics. Local Open Scope Z. -(* TODO : integrate Andres's Fermat's little theorem proof *) -Lemma fermat_little: forall (a p : Z) (prime_p : prime p), - a mod p <> 0 -> a ^ (p - 1) mod p = 1. -Admitted. - -Ltac prime_bound := match goal with -| H : prime ?p |- _ => pose proof (prime_ge_2 p H); try omega -end. - -Lemma prime_minus1_div2_nonneg : forall (x p : Z) (prime_p : prime p), - x * 2 + 1 = p -> 0 < x. -Proof. - intros; prime_bound. -Qed. - -Lemma squared_fermat_little: forall (a x p : Z) (prime_p : prime p), - x * 2 + 1 = p -> a mod p <> 0 -> (a * a) ^ x mod p = 1. -Proof. - intros. - rewrite <- Z.pow_2_r. - rewrite <- Z.pow_mul_r by - (pose proof (prime_minus1_div2_nonneg x p prime_p H); omega). - rewrite Z.mul_comm. - replace (x * 2) with (x * 2 + 1 - 1) by omega. - rewrite H. - apply fermat_little; auto. -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 euler_criterion_reverse : forall (a x p : Z) (prime_p : prime p), - (x * 2 + 1 = p) -> (a mod p <> 0) -> - (exists b, b * b mod p = a mod p) -> (a ^ x mod p = 1). -Proof. - intros. - destruct H1. - assert (x0 mod p <> 0). { - intuition. - assert (2 > 0) by omega. - assert (p > 1) by prime_bound. - pose proof (mod_exp_0 x0 2 p H3 H4 H2); clear H3; clear H4. - rewrite Z.pow_2_r in H5. - rewrite H5 in H1. - intuition. - } - pose proof (squared_fermat_little x0 x p prime_p H H2). - assert (0 <= x) by (pose proof (prime_minus1_div2_nonneg x p prime_p H); omega). - assert (p <> 0) by prime_bound. - rewrite mod_pow by auto. - pose proof (mod_pow (x0 * x0) p x H4 H5). - rewrite H3 in H6. - rewrite H1 in H6. - auto. -Qed. -(* -Fixpoint order_mod' y p i r := - match i with - | O => r - | S i' => if (Zeq_bool (y ^ (Z.of_nat i) mod p) 1) - then order_mod' y p i' (Z.of_nat i) - else order_mod' y p i' r - end. - -Definition order_mod y p := order_mod' y p (Z.to_nat (p - 2)) (p - 1). - -Lemma order_mod'_le_r : forall y p i r, Z.of_nat i <= r -> - order_mod' y p i r <= r. -Proof. - induction i; intros; try (simpl; omega). - unfold order_mod'; fold order_mod'. - assert (Z.of_nat i <= Z.of_nat (S i)) by (rewrite <- Nat2Z.inj_le; omega). - break_if. { - specialize (IHi (Z.of_nat (S i)) H0). - omega. - } { - apply IHi. - omega. - } -Qed. - -Lemma order_mod'_pos : forall y p i r, 1 <= r -> 1 <= order_mod' y p i r. -Proof. - induction i; intros; auto. - unfold order_mod'; fold order_mod'. - break_if; apply IHi; auto. - replace 1 with (Z.of_nat 1) by auto. - rewrite <- Nat2Z.inj_le. - pose proof (lt_0_Sn i); omega. -Qed. - -Lemma order_mod_bounds : forall y p (prime_p : prime p), - 1 <= order_mod y p <= p - 1. -Proof. - unfold order_mod; split; intros. { - apply order_mod'_pos; prime_bound. - } { - apply order_mod'_le_r. - rewrite Z2Nat.id; prime_bound; omega. - } -Qed. - -Lemma order_mod'_id : forall y p i r, - y ^ r mod p = 1 -> - y ^ (order_mod' y p i r) mod p = 1. -Proof. - induction i; intros; [simpl; auto |]. - unfold order_mod'; fold order_mod'. - break_if; auto. - apply IHi. - apply Zeq_bool_eq; auto. -Qed. - -Lemma order_mod_id : forall y p (prime_p : prime p), (y mod p <> 0) -> y ^ (order_mod y p) mod p = 1. -Proof. - intros. - unfold order_mod; apply order_mod'_id. - apply fermat_little; auto. -Qed. - -Lemma order_mod'_upper_bound : forall x y p i r, 1 <= x <= Z.of_nat i -> - (Z.of_nat i <= r) -> (y ^ x mod p = 1) -> order_mod' y p i r <= x. -Proof. - induction i; intros; try (simpl in H; omega). - unfold order_mod'; fold order_mod'. - assert (Z.of_nat i <= Z.of_nat (S i)) by (rewrite <- Nat2Z.inj_le; omega). - break_if. { - specialize (IHi (Z.of_nat (S i))). - destruct (Z.eq_dec x (Z.of_nat (S i))). { - rewrite e. - apply order_mod'_le_r; auto. - } { - destruct H. - rewrite Nat2Z.inj_succ in H3. - apply (Z.le_succ_r x (Z.of_nat i)) in H3. - destruct H3; intuition. - rewrite Nat2Z.inj_succ. - rewrite H3. - apply order_mod'_le_r. - omega. - } - } { - destruct H. - apply Z.le_lteq in H3; destruct H3. { - rewrite Nat2Z.inj_succ in H3. - apply IHi; omega. - } { - exfalso. - destruct H3. - apply Zeq_is_eq_bool in H1. - rewrite Heqb in H1. - intuition. - } - } -Qed. - -Lemma order_mod_upper_bound : forall x y p (prime_p : prime p), - (1 <= x <= p - 2) -> - (y ^ x mod p = 1) -> order_mod y p <= x. -Proof. - unfold order_mod; intros. - apply order_mod'_upper_bound; (rewrite Z2Nat.id; omega) || prime_bound. -Qed. - -Lemma order_mod_lowest : forall x y p (prime_p : prime p), - 1 <= x < order_mod y p -> y ^ x mod p <> 1. -Proof. - intros. - intuition. - pose proof (order_mod_upper_bound x y p prime_p). - assert (1 <= x <= p - 2) as x_bounds. { - pose proof (order_mod_bounds y p prime_p). - omega. - } - specialize (H x_bounds H0). - omega. -Qed. - -Lemma pow_mod_order : forall x y p (prime_p : prime p), 1 <= x -> - y ^ x mod p = 1 -> y ^ (x mod (order_mod y p)) mod p = 1. -Proof. - intros. - remember (order_mod y p) as ord. - pose proof (order_mod_bounds y p prime_p). - assert (0 <= x / ord) by (apply Z.div_pos; omega). - assert (y mod p <> 0) by (intuition; apply (mod_exp_0 _ x) in H3; prime_bound). - rewrite (Z_div_mod_eq x ord) in H0 by omega. - rewrite Z.pow_add_r in H0 by (try apply Z.mul_nonneg_nonneg; - try apply Z.mod_pos_bound; omega). - rewrite Zmult_mod in H0. - rewrite Z.pow_mul_r in H0 by (try apply Z.mod_pos_bound; omega). - rewrite mod_pow in H0 by (prime_bound || auto). - rewrite Heqord in H0 at 1. - rewrite order_mod_id in H0; auto. - rewrite Z.pow_1_l in H0 by auto. - rewrite Z.mod_1_l in H0 by prime_bound. - rewrite Z.mul_1_l in H0. - rewrite Z.mod_mod in H0 by prime_bound. - auto. -Qed. - -Lemma order_mod_divide : forall x y p (prime_p : prime p), 0 <= x -> - y ^ x mod p = 1 -> (order_mod y p | x). -Proof. - intros. - pose proof (order_mod_bounds y p prime_p). - destruct (Z.eq_dec x 0); [subst; apply Z.divide_0_r|]. - apply pow_mod_order in H0; (omega || auto). - assert (0 < order_mod y p) by omega. - apply (Z.mod_pos_bound x _) in H2. - pose proof (Z.nonpos_pos_cases (x mod order_mod y p)). - destruct H3. { - assert (x mod order_mod y p = 0) by omega. - apply Z.mod_divide; omega. - } { - assert (1 <= x mod order_mod y p <= p - 2) by omega. - pose proof (order_mod_upper_bound _ y p prime_p H4 H0). - omega. - } -Qed. - -Lemma e_order_order_mod : forall y p (prime_p : prime p) (lt_1_p : 1 < p), - EGroup.e_order Z.eq_dec y (ZPGroup p lt_1_p) = FGroup.g_order (ZPGroup p lt_1_p) - -> order_mod y p = p - 1. -Proof. -Admitted. -*) - +(* TODO: move somewhere else for lemmas about Coqprime? *) Lemma in_ZPGroup_range (n : Z) (n_pos : 1 < n) (p : Z) : List.In p (FGroup.s (ZPGroup n n_pos)) -> 1 <= p < n. Proof. @@ -302,118 +39,116 @@ Proof. auto. Qed. -Lemma exists_primitive_root_power : forall p (prime_p : prime p) (lt_1_p : 1 < p) - (p_odd : p <> 2) (* This is provable for p = 2, but we are lazy. *), - (exists y, List.In y (FGroup.s (ZPGroup p lt_1_p)) - /\ EGroup.e_order Z.eq_dec y (ZPGroup p lt_1_p) = FGroup.g_order (ZPGroup p lt_1_p) - /\ (forall x (x_range : 1 <= x <= p - 1), exists j, 0 <= j <= p - 1 /\ y ^ j mod p = x)). +Section EulerCriterion. + +Variable x p : Z. +Hypothesis prime_p : prime p. +Hypothesis neq_p_2 : p <> 2. (* Euler's Criterion is also provable with p = 2, but we do not need it and are lazy.*) +Hypothesis x_id : x * 2 + 1 = p. + + +Lemma lt_1_p : 1 < p. Proof. prime_bound. Qed. +Lemma x_pos: 0 < x. Proof. prime_bound. Qed. +Lemma x_nonneg: 0 <= x. Proof. prime_bound. Qed. + +Lemma x_id_inv : x = (p - 1) / 2. Proof. - intros. - destruct (Zp_cyclic p lt_1_p prime_p) as [y [y_in_ZPGroup y_order]]. - exists y; repeat split; auto. - intros x x_range. - pose proof (in_ZPGroup_range p lt_1_p y y_in_ZPGroup) as y_range1. - assert (0 <= y < p) as y_range0 by omega. - pose proof (rel_prime_le_prime y p prime_p y_range1) as rel_prime_y_p. - pose proof (in_ZPGroup p lt_1_p y rel_prime_y_p y_range0) as in_ZPGroup_y. - destruct (EGroup.support_gpow Z Z.eq_dec (pmult p) y (ZPGroup p lt_1_p) in_ZPGroup_y x) as [k [k_range gpow_y_k]]. - assert (rel_prime x p) by (apply rel_prime_le_prime; (omega || auto)). - assert (List.In x (FGroup.s (ZPGroup p lt_1_p))). - apply in_ZPGroup; (omega || auto). - apply generator_subgroup_is_group; eauto. - exists k; split. { - split; try omega. - unfold EGroup.e_order in y_order. - rewrite y_order in k_range. - rewrite <- phi_is_order in k_range. - rewrite Euler.prime_phi_n_minus_1 in k_range; (omega || auto). - } - assert (y mod p = y) as y_small by (apply Z.mod_small; omega). - rewrite <- y_small in gpow_y_k. - rewrite <- (Zpower_mod_is_gpow y k p lt_1_p) in gpow_y_k by (omega || auto). - auto. + intros; apply Zeq_plus_swap in x_id. + replace (p - 1) with (2 * ((p - 1) / 2)) in x_id by + (symmetry; apply Z_div_exact_2; [omega | rewrite <- x_id; apply Z_mod_mult]). + ring_simplify in x_id; apply Z.mul_cancel_l in x_id; omega. Qed. -Lemma pred_odd : forall x, ~ (2 | x) -> (2 | x - 1). +Lemma mod_p_order : FGroup.g_order (ZPGroup p lt_1_p) = p - 1. Proof. - intros. - rewrite <- Z.mod_divide in H by omega. - rewrite <- Z.mod_divide by omega. - pose proof (Zmod_odd x). - break_if; intuition. - replace x with (Z.succ (x - 1)) in Heqb by omega. - rewrite Z.odd_succ in Heqb. - pose proof (Zmod_even (x - 1)). - rewrite Heqb in H1; simpl in H1; auto. + intros; rewrite <- phi_is_order. + apply Euler.prime_phi_n_minus_1; auto. Qed. -Ltac Zdivide_exists_mul := match goal with -| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H -| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides -end; (omega || auto). +Lemma p_odd : Z.odd p = true. +Proof. + pose proof (prime_odd_or_2 p prime_p). + destruct H; auto. +Qed. -Lemma prime_pred_divide2 : forall p (prime_p : prime p) (p_odd : p <> 2), - (2 | p - 1). +Lemma prime_pred_even : Z.even (p - 1) = true. Proof. intros. - apply pred_odd. - intuition. - Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound p 2); omega]. - rewrite Z.mul_comm in H. - apply Zdivide_intro in H. - apply prime_divisors in H; auto. - intuition. - prime_bound. + rewrite <- Z.odd_succ. + replace (Z.succ (p - 1)) with p by ring. + apply p_odd. Qed. -Lemma prime_odd : forall p (prime_p : prime p) (p_odd : p <> 2), - Zodd p. +Lemma fermat_little: forall a (a_nonzero : a mod p <> 0), + a ^ (p - 1) mod p = 1. +Proof. +Admitted. + +Lemma squared_fermat_little: forall a (a_nonzero : a mod p <> 0), + (a * a) ^ x mod p = 1. Proof. intros. - pose proof (prime_pred_divide2 p prime_p p_odd). - assert (Zeven (p - 1)) by (Zdivide_exists_mul; [rewrite H; apply Zeven_2p - | pose proof (Zmod_pos_bound (p - 1) 2); omega]). - replace p with (Z.succ (p - 1)) by ring. - apply Zodd_Sn; auto. + rewrite <- Z.pow_2_r. + rewrite <- Z.pow_mul_r by (apply x_nonneg || omega). + replace (2 * x) with (x * 2 + 1 - 1) by omega. + rewrite x_id. + apply fermat_little; auto. Qed. -Lemma prime_minus1_div2_exact : forall x p (prime_p : prime p) (p_odd : p <> 2), - (x * 2 + 1 = p) -> x = (p - 1) / 2. +Lemma euler_criterion_reverse : forall a (a_nonzero : a mod p <> 0), + (exists b, b * b mod p = a mod p) -> (a ^ x mod p = 1). Proof. - intros. - apply Zeq_plus_swap in H. - replace (p - 1) with (2 * ((p - 1) / 2)) in H by - (symmetry; apply Z_div_exact_2; try apply Z.mod_divide; - try apply prime_pred_divide2; (auto || omega)). - ring_simplify in H. - apply Z.mul_cancel_l in H; omega. + intros ? ? a_square. + destruct a_square as [b a_square]. + assert (b mod p <> 0) as b_nonzero. { + intuition. + rewrite <- Z.pow_2_r in a_square. + rewrite mod_exp_0 in a_square by prime_bound. + auto. + } + pose proof (squared_fermat_little b b_nonzero). + rewrite mod_pow in * by prime_bound. + rewrite <- a_square; auto. Qed. -Lemma divide_mul_div: forall a b c, a <> 0 -> c <> 0 -> - (a | b * (a / c)) -> (c | a) -> (c | b). +Lemma exists_primitive_root_power : + (exists y, List.In y (FGroup.s (ZPGroup p lt_1_p)) + /\ EGroup.e_order Z.eq_dec y (ZPGroup p lt_1_p) = FGroup.g_order (ZPGroup p lt_1_p) + /\ (forall a (a_range : 1 <= a <= p - 1), exists j, 0 <= j <= p - 1 /\ y ^ j mod p = a)). Proof. intros. - Zdivide_exists_mul. - Zdivide_exists_mul. - rewrite H2 in H1. - rewrite Z_div_mul' in H1 by auto. - replace (b * x) with (x * b) in H1 by ring. - replace (c * x * x0) with (x * (x0 * c)) in H1 by ring. - rewrite Z.mul_cancel_l in H1 by (intuition; rewrite H3 in H2; ring_simplify in H2; intuition). - eapply Zdivide_intro; eauto. + destruct (Zp_cyclic p lt_1_p prime_p) as [y [y_in_ZPGroup y_order]]. + exists y; repeat split; auto. + intros. + pose proof (in_ZPGroup_range p lt_1_p y y_in_ZPGroup) as y_range1. + assert (0 <= y < p) as y_range0 by omega. + assert (rel_prime y p) as rel_prime_y_p by (apply rel_prime_le_prime; omega || auto). + assert (rel_prime a p) as rel_prime_a_p by (apply rel_prime_le_prime; omega || auto). + assert (List.In a (FGroup.s (ZPGroup p lt_1_p))) as a_in_ZPGroup by (apply in_ZPGroup; omega || auto). + destruct (EGroup.support_gpow Z Z.eq_dec (pmult p) y (ZPGroup p lt_1_p) y_in_ZPGroup a) + as [k [k_range gpow_y_k]]; [apply generator_subgroup_is_group; auto |]. + exists k; split. { + unfold EGroup.e_order in y_order. + rewrite y_order in k_range. + rewrite mod_p_order in k_range. + omega. + } { + assert (y mod p = y) as y_small by (apply Z.mod_small; omega). + rewrite <- y_small in gpow_y_k. + rewrite <- (Zpower_mod_is_gpow y k p lt_1_p) in gpow_y_k by (omega || auto). + auto. + } Qed. Ltac ereplace x := match type of x with ?t => let e := fresh "e" in evar (e:t); replace x with e; subst e end. -Lemma euler_criterion : forall (a x p : Z) (prime_p : prime p) - (p_odd : p <> 2) (a_range : 1 <= a <= p - 1) (x_div2_minus1p : x * 2 + 1 = p) +Lemma euler_criterion : forall a (a_range : 1 <= a <= p - 1) (pow_a_x : a ^ x mod p = 1), exists b : Z, b * b mod p = a mod p. Proof. intros. - assert (1 < p) as lt_1_p by prime_bound. - destruct (exists_primitive_root_power p prime_p lt_1_p) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. - destruct (gpow_y a a_range) as [j [j_range pow_y_j]]. + destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. + destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y. rewrite mod_pow in pow_a_x by prime_bound. replace a with (a mod p) in pow_y_j by (apply Z.mod_small; omega). rewrite <- pow_y_j in pow_a_x. @@ -434,44 +169,47 @@ Proof. rewrite <- Z.pow_add_r by (apply Z.div_pos; omega). rewrite <- Z_div_plus by omega. rewrite Z.mul_comm. - rewrite (prime_minus1_div2_exact x p) in divide_mul_j_x; auto. + rewrite x_id_inv in divide_mul_j_x; auto. apply (divide_mul_div _ j 2) in divide_mul_j_x; try (apply prime_pred_divide2 || prime_bound); auto. rewrite <- Zdivide_Zdiv_eq by (auto || omega). rewrite Zplus_diag_eq_mult_2. rewrite Z_div_mult by omega; auto. + apply divide2_even_iff. + apply prime_pred_even. Qed. -Lemma divide2_1mod4 : forall x, x mod 4 = 1 -> 0 <= x -> (2 | x / 2). +End EulerCriterion. + +Lemma divide2_1mod4 : forall x (x_1mod4 : x mod 4 = 1) (x_nonneg : 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 + assert (Z.to_nat x mod 4 = 1)%nat as x_1mod4_nat. { + replace 1 with (Z.of_nat 1) in * by auto. + replace (x mod 4) with (Z.of_nat (Z.to_nat x mod 4)) in * by (rewrite mod_Zmod by omega; rewrite Z2Nat.id; auto). - apply Nat2Z.inj in H; auto. + apply Nat2Z.inj in x_1mod4; 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. + destruct (divide2_1mod4_nat c (Z.to_nat x) Heqc x_1mod4_nat) as [k k_id]. + replace 2%nat with (Z.to_nat 2) in * by auto. + apply inj_eq in k_id. + rewrite div_Zdiv in k_id by (replace (Z.to_nat 2) with 2%nat by auto; omega). + rewrite Nat2Z.inj_mul in k_id. + do 2 rewrite Z2Nat.id in k_id by omega. + rewrite Z.mul_comm in k_id. + symmetry in k_id. + apply Zdivide_intro in k_id; 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. + intros ? ? divide_2_y lt_1_x y_nonneg. + apply Zdivide_Zdiv_eq in divide_2_y; try omega. + rewrite divide_2_y. rewrite Z.pow_mul_r by omega. - assert ((x - 1)^2 mod x = 1). { - replace ((x - 1)^2) with (x ^ 2 - 2 * x + 1) + assert ((x - 1) ^ 2 mod x = 1) as square_case. { + 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. @@ -485,24 +223,29 @@ Proof. rewrite Z.pow_succ_r by apply Zle_0_nat. rewrite Zmult_mod. rewrite IHn. - rewrite H2. - simpl. - apply Zmod_1_l; auto. + rewrite square_case. + simpl; apply Zmod_1_l; auto. +Qed. + +Lemma prime_1mod4_neq2 : forall p (prime_p : prime p), (p mod 4 = 1) -> p <> 2. +Proof. + intros; intuition. + assert (4 <> 0)%Z as neq_4_0 by omega. + pose proof (Z.div_mod p 4 neq_4_0). + omega. Qed. Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p), (p mod 4 = 1)%Z -> exists b : Z, (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)). - replace (p - 1) with ((p - 1) mod p) by (apply Zmod_small; omega). - assert (p <> 2) as neq_p_2 by intuition. - apply (euler_criterion (p - 1) (p / 2) p prime_p); - [ auto | omega | | apply minus1_even_pow; (omega || auto); apply Z_div_pos; omega]. - pose proof (prime_odd p prime_p neq_p_2). - rewrite <- Zdiv2_div. - rewrite Zodd_div2; (ring || auto). + replace (p - 1) with ((p - 1) mod p) by (apply Zmod_small; split; prime_bound). + assert (p <> 2) as neq_p_2 by (apply prime_1mod4_neq2; auto). + apply (euler_criterion (p / 2) p prime_p). + + auto. + + destruct (prime_odd_or_2 p prime_p); intuition. + rewrite <- Zdiv2_div. + pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega. + + prime_bound. + + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound. Qed. -- cgit v1.2.3