diff options
Diffstat (limited to 'coqprime/Coqprime/Pocklington.v')
| -rw-r--r-- | coqprime/Coqprime/Pocklington.v | 261 |
1 files changed, 0 insertions, 261 deletions
diff --git a/coqprime/Coqprime/Pocklington.v b/coqprime/Coqprime/Pocklington.v deleted file mode 100644 index 09c0b901c..000000000 --- a/coqprime/Coqprime/Pocklington.v +++ /dev/null @@ -1,261 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Import ZCAux. -Require Import Zp. -Require Import FGroup. -Require Import EGroup. -Require Import Euler. - -Open Scope Z_scope. - -Theorem Pocklington: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> - forall n, prime n -> (n | N) -> n mod F1 = 1. -intros N F1 R1 HF1 HR1 Neq Rec n Hn H. -assert (HN: 1 < N). -assert (0 < N - 1); auto with zarith. -rewrite Neq; auto with zarith. -apply Zlt_le_trans with (1* R1); auto with zarith. -assert (Hn1: 1 < n); auto with zarith. -apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. -assert (H1: (F1 | n - 1)). -2: rewrite <- (Zmod_small 1 F1); auto with zarith. -2: case H1; intros k H1'. -2: replace n with (1 + (n - 1)); auto with zarith. -2: rewrite H1'; apply Z_mod_plus; auto with zarith. -apply Zdivide_Zpower; auto with zarith. -intros p i Hp Hi HiF1. -case (Rec p); auto. -apply Zdivide_trans with (2 := HiF1). -apply Zpower_divide; auto with zarith. -intros a (Ha1, (Ha2, Ha3)). -assert (HNn: a ^ (N - 1) mod n = 1). -apply Zdivide_mod_minus; auto with zarith. -apply Zdivide_trans with (1 := H). -apply Zmod_divide_minus; auto with zarith. -assert (~(n | a)). -intros H1; absurd (0 = 1); auto with zarith. -rewrite <- HNn; auto. -apply sym_equal; apply Zdivide_mod; auto with zarith. -apply Zdivide_trans with (1 := H1); apply Zpower_divide; auto with zarith. -assert (Hr: rel_prime a n). -apply rel_prime_sym; apply prime_rel_prime; auto. -assert (Hz: 0 < Zorder a n). -apply Zorder_power_pos; auto. -apply Zdivide_trans with (Zorder a n). -apply prime_divide_Zpower_Zdiv with (N - 1); auto with zarith. -apply Zorder_div_power; auto with zarith. -intros H1; absurd (1 < n); auto; apply Zle_not_lt; apply Zdivide_le; auto with zarith. -rewrite <- Ha3; apply Zdivide_Zgcd; auto with zarith. -apply Zmod_divide_minus; auto with zarith. -case H1; intros t Ht; rewrite Ht. -assert (Ht1: 0 <= t). -apply Zmult_le_reg_r with (Zorder a n); auto with zarith. -rewrite Zmult_0_l; rewrite <- Ht. -apply Zge_le; apply Z_div_ge0; auto with zarith. -apply Zlt_gt; apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. -rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. -rewrite Zpower_mod; auto with zarith. -rewrite Zorder_power_is_1; auto with zarith. -rewrite Zpower_1_l; auto with zarith. -apply Zmod_small; auto with zarith. -apply Zdivide_trans with (1:= HiF1); rewrite Neq; apply Zdivide_factor_r. -apply Zorder_div; auto. -Qed. - -Theorem PocklingtonCorollary1: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> N < F1 * F1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> - prime N. -intros N F1 R1 H H1 H2 H3 H4; case (prime_dec N); intros H5; auto. -assert (HN: 1 < N). -assert (0 < N - 1); auto with zarith. -rewrite H2; auto with zarith. -apply Zlt_le_trans with (1* R1); auto with zarith. -case Zdivide_div_prime_le_square with (2:= H5); auto with zarith. -intros n (Hn, (Hn1, Hn2)). -assert (Hn3: 0 <= n). -apply Zle_trans with 2; try apply prime_ge_2; auto with zarith. -absurd (n = 1). -intros H6; contradict Hn; subst; apply not_prime_1. -rewrite <- (Zmod_small n F1); try split; auto. -apply Pocklington with (R1 := R1) (4 := H4); auto. -apply Zlt_square_mult_inv; auto with zarith. -Qed. - -Theorem PocklingtonCorollary2: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> - forall n, 0 <= n -> (n | N) -> n mod F1 = 1. -intros N F1 R1 H1 H2 H3 H4 n H5; pattern n; apply prime_induction; auto. -assert (HN: 1 < N). -assert (0 < N - 1); auto with zarith. -rewrite H3; auto with zarith. -apply Zlt_le_trans with (1* R1); auto with zarith. -intros (u, Hu); contradict HN; subst; rewrite Zmult_0_r; auto with zarith. -intro H6; rewrite Zmod_small; auto with zarith. -intros p q Hp Hp1 Hp2; rewrite Zmult_mod; auto with zarith. -rewrite Pocklington with (n := p) (R1 := R1) (4 := H4); auto. -rewrite Hp1. -rewrite Zmult_1_r; rewrite Zmod_small; auto with zarith. -apply Zdivide_trans with (2 := Hp2); apply Zdivide_factor_l. -apply Zdivide_trans with (2 := Hp2); apply Zdivide_factor_r; auto. -Qed. - -Definition isSquare x := exists y, x = y * y. - -Theorem PocklingtonExtra: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> - forall m, 1 <= m -> (forall l, 1 <= l < m -> ~((l * F1 + 1) | N)) -> - let s := (R1 / (2 * F1)) in - let r := (R1 mod (2 * F1)) in - N < (m * F1 + 1) * (2 * F1 * F1 + (r - m) * F1 + 1) -> - (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N. -intros N F1 R1 H1 H2 H3 OF1 ER1 H4 m H5 H6 s r H7 H8. -case (prime_dec N); auto; intros H9. -assert (HN: 1 < N). -assert (0 < N - 1); auto with zarith. -rewrite H3; auto with zarith. -apply Zlt_le_trans with (1* R1); auto with zarith. -case Zdivide_div_prime_le_square with N; auto. -intros X (Hx1, (Hx2, Hx3)). -assert (Hx0: 1 < X). -apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. -pose (c := (X / F1)). -assert(Hc1: 0 <= c); auto with zarith. -apply Zge_le; unfold c; apply Z_div_ge0; auto with zarith. -assert (Hc2: X = c * F1 + 1). -rewrite (Z_div_mod_eq X F1); auto with zarith. -eq_tac; auto. -rewrite (Zmult_comm F1); auto. -apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith. -case Zle_lt_or_eq with (1 := Hc1); clear Hc1; intros Hc1. -2: contradict Hx0; rewrite Hc2; try rewrite <- Hc1; auto with zarith. -case (Zle_or_lt m c); intros Hc3. -2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5; auto with zarith. -2: case (H6 c); auto with zarith; rewrite <- Hc2; auto. -2: contradict Hc3; rewrite <- H5; auto with zarith. -pose (d := ((N / X) / F1)). -assert(Hd0: 0 <= N / X); try apply Z_div_pos; auto with zarith. -(* -apply Zge_le; unfold d; repeat apply Z_div_ge0; auto with zarith. -*) -assert(Hd1: 0 <= d); auto with zarith. -apply Zge_le; unfold d; repeat apply Z_div_ge0; auto with zarith. -assert (Hd2: N / X = d * F1 + 1). -rewrite (Z_div_mod_eq (N / X) F1); auto with zarith. -eq_tac; auto. -rewrite (Zmult_comm F1); auto. -apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith. -exists X; auto with zarith. -apply Zdivide_Zdiv_eq; auto with zarith. -case Zle_lt_or_eq with (1 := Hd0); clear Hd0; intros Hd0. -2: contradict HN; rewrite (Zdivide_Zdiv_eq X N); auto with zarith. -2: rewrite <- Hd0; auto with zarith. -case (Zle_lt_or_eq 1 (N / X)); auto with zarith; clear Hd0; intros Hd0. -2: contradict H9; rewrite (Zdivide_Zdiv_eq X N); auto with zarith. -2: rewrite <- Hd0; rewrite Zmult_1_r; auto with zarith. -case Zle_lt_or_eq with (1 := Hd1); clear Hd1; intros Hd1. -2: contradict Hd0; rewrite Hd2; try rewrite <- Hd1; auto with zarith. -case (Zle_or_lt m d); intros Hd3. -2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5; auto with zarith. -2: case (H6 d); auto with zarith; rewrite <- Hd2; auto. -2: exists X; auto with zarith. -2: apply Zdivide_Zdiv_eq; auto with zarith. -2: contradict Hd3; rewrite <- H5; auto with zarith. -assert (L5: N = (c * F1 + 1) * (d * F1 + 1)). -rewrite <- Hc2; rewrite <- Hd2; apply Zdivide_Zdiv_eq; auto with zarith. -assert (L6: R1 = c * d * F1 + c + d). -apply trans_equal with ((N - 1) / F1). -rewrite H3; rewrite Zmult_comm; apply sym_equal; apply Z_div_mult; auto with zarith. -rewrite L5. -match goal with |- (?X / ?Y = ?Z) => replace X with (Z * Y) end; try ring; apply Z_div_mult; auto with zarith. -assert (L6_1: Zodd (c + d)). -case (Zeven_odd_dec (c + d)); auto; intros O1. -contradict ER1; apply Zeven_not_Zodd; rewrite L6; rewrite <- Zplus_assoc; apply Zeven_plus_Zeven; auto. -apply Zeven_mult_Zeven_r; auto. -assert (L6_2: Zeven (c * d)). -case (Zeven_odd_dec c); intros HH1. -apply Zeven_mult_Zeven_l; auto. -case (Zeven_odd_dec d); intros HH2. -apply Zeven_mult_Zeven_r; auto. -contradict L6_1; apply Zeven_not_Zodd; apply Zodd_plus_Zodd; auto. -assert ((c + d) mod (2 * F1) = r). -rewrite <- Z_mod_plus with (b := Zdiv2 (c * d)); auto with zarith. -match goal with |- ?X mod _ = _ => replace X with R1 end; auto. -rewrite L6; pattern (c * d) at 1. -rewrite Zeven_div2 with (1 := L6_2); ring. -assert (L9: c + d - r < 2 * F1). -apply Zplus_lt_reg_r with (r - m). -apply Zmult_lt_reg_r with (F1); auto with zarith. -apply Zplus_lt_reg_r with 1. -match goal with |- ?X < ?Y => - replace Y with (2 * F1 * F1 + (r - m) * F1 + 1); try ring; - replace X with ((((c + d) - m) * F1) + 1); try ring -end. -apply Zmult_lt_reg_r with (m * F1 + 1); auto with zarith. -apply Zlt_trans with (m * F1 + 0); auto with zarith. -rewrite Zplus_0_r; apply Zmult_lt_O_compat; auto with zarith. -repeat rewrite (fun x => Zmult_comm x (m * F1 + 1)). -apply Zle_lt_trans with (2 := H7). -rewrite L5. -match goal with |- ?X <= ?Y => - replace X with ((m * (c + d) - m * m ) * F1 * F1 + (c + d) * F1 + 1); try ring; - replace Y with ((c * d) * F1 * F1 + (c + d) * F1 + 1); try ring -end. -repeat apply Zplus_le_compat_r. -repeat apply Zmult_le_compat_r; auto with zarith. -assert (tmp: forall p q, 0 <= p - q -> q <= p); auto with zarith; try apply tmp. -match goal with |- _ <= ?X => - replace X with ((c - m) * (d - m)); try ring; auto with zarith -end. -assert (L10: c + d = r). -apply Zmod_closeby_eq with (2 * F1); auto with zarith. -unfold r; apply Z_mod_lt; auto with zarith. -assert (L11: 2 * s = c * d). -apply Zmult_reg_r with F1; auto with zarith. -apply trans_equal with (R1 - (c + d)). -rewrite L10; rewrite (Z_div_mod_eq R1 (2 * F1)); auto with zarith. -unfold s, r; ring. -rewrite L6; ring. -case H8; intro H10. -absurd (0 < c * d); auto with zarith. -apply Zmult_lt_O_compat; auto with zarith. -case H10; exists (c - d); auto with zarith. -rewrite <- L10. -replace (8 * s) with (4 * (2 * s)); auto with zarith; try rewrite L11; ring. -Qed. - -Theorem PocklingtonExtraCorollary: -forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 -> - (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> - let s := (R1 / (2 * F1)) in - let r := (R1 mod (2 * F1)) in - N < 2 * F1 * F1 * F1 -> (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N. -intros N F1 R1 H1 H2 H3 OF1 ER1 H4 s r H5 H6. -apply PocklingtonExtra with (6 := H4) (R1 := R1) (m := 1); auto with zarith. -apply Zlt_le_trans with (1 := H5). -match goal with |- ?X <= ?K * ((?Y + ?Z) + ?T) => - rewrite <- (Zplus_0_l X); - replace (K * ((Y + Z) + T)) with ((F1 * (Z + T) + Y + Z + T) + X);[idtac | ring] -end. -apply Zplus_le_compat_r. -case (Zle_lt_or_eq 0 r); unfold r; auto with zarith. -case (Z_mod_lt R1 (2 * F1)); auto with zarith. -intros HH; repeat ((rewrite <- (Zplus_0_r 0); apply Zplus_le_compat)); auto with zarith. -intros HH; contradict ER1; apply Zeven_not_Zodd. -rewrite (Z_div_mod_eq R1 (2 * F1)); auto with zarith. -rewrite <- HH; rewrite Zplus_0_r. -rewrite <- Zmult_assoc; apply Zeven_2p. -Qed. |