diff options
Diffstat (limited to 'coqprime/Coqprime/LucasLehmer.v')
| -rw-r--r-- | coqprime/Coqprime/LucasLehmer.v | 61 |
1 files changed, 30 insertions, 31 deletions
diff --git a/coqprime/Coqprime/LucasLehmer.v b/coqprime/Coqprime/LucasLehmer.v index a0e3b8e46..6e3d218f2 100644 --- a/coqprime/Coqprime/LucasLehmer.v +++ b/coqprime/Coqprime/LucasLehmer.v @@ -7,11 +7,11 @@ (*************************************************************) (********************************************************************** - LucasLehamer.v - + LucasLehamer.v + Build the sequence for the primality test of Mersenne numbers - - Definition: LucasLehmer + + Definition: LucasLehmer **********************************************************************) Require Import ZArith. Require Import ZCAux. @@ -27,7 +27,7 @@ Require Import IGroup. Open Scope Z_scope. -(************************************** +(************************************** The seeds of the serie **************************************) @@ -43,13 +43,13 @@ Theorem w_mult_v : pmult w v = (1, 0). simpl; auto. Qed. -(************************************** +(************************************** Definition of the power function for pairs p^n **************************************) Definition ppow p n := match n with Zpos q => iter_pos _ (pmult p) (1, 0) q | _ => (1, 0) end. -(************************************** +(************************************** Some properties of ppow **************************************) @@ -66,7 +66,7 @@ Qed. Theorem ppow_op: forall a b p, iter_pos _ (pmult a) b p = pmult (iter_pos _ (pmult a) (1, 0) p) b. intros a b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b. -rewrite (Rec b). +rewrite (Rec b). try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. repeat rewrite pmult_assoc; auto. intros p Rec b. @@ -118,13 +118,13 @@ rewrite (fun x y => pmult_comm (iter_pos _ x y p3) p); auto. rewrite (pmult_assoc m); try apply pmult_comm; auto. Qed. -(************************************** +(************************************** We can now define our series of pairs s **************************************) Definition s n := pplus (ppow w (2 ^ n)) (ppow v (2 ^ n)). -(************************************** +(************************************** Some properties of s **************************************) @@ -149,7 +149,7 @@ repeat rewrite <- ppow_mult; auto with zarith. rewrite (pmult_comm v w); rewrite w_mult_v. rewrite ppow_1. repeat rewrite tpower_1. -rewrite pplus_comm; repeat rewrite <- pplus_assoc; +rewrite pplus_comm; repeat rewrite <- pplus_assoc; rewrite pplus_comm; repeat rewrite <- pplus_assoc. simpl; case (ppow (7, -4) (2 ^n)); simpl; intros z1 z2; eq_tac; auto with zarith. Qed. @@ -201,7 +201,7 @@ Section Lucas. Variable p: Z. -(************************************** +(************************************** Definition of the mersenne number **************************************) @@ -216,7 +216,7 @@ Qed. Hypothesis p_pos2: 2 < p. -(************************************** +(************************************** We suppose that the mersenne number divides s **************************************) @@ -224,7 +224,7 @@ Hypothesis Mp_divide_sn: (Mp | fst (s (p - 2))). Variable q: Z. -(************************************** +(************************************** We take a divisor of Mp and shows that Mp <= q^2, hence Mp is prime **************************************) @@ -236,7 +236,7 @@ Theorem q_pos: 1 < q. apply Zlt_trans with (2 := q_pos2); auto with zarith. Qed. -(************************************** +(************************************** The definition of the groups of inversible pairs **************************************) @@ -285,18 +285,18 @@ intros a _; left; rewrite zpmult_0_l; auto with zarith. intros; discriminate. Qed. -(************************************** +(************************************** The power function zpow: a^n **************************************) -Definition zpow a := gpow a pgroup. +Definition zpow a := gpow a pgroup. -(************************************** +(************************************** Some properties of zpow **************************************) -Theorem zpow_def: - forall a b, In a pgroup.(FGroup.s) -> 0 <= b -> +Theorem zpow_def: + forall a b, In a pgroup.(FGroup.s) -> 0 <= b -> zpow a b = ((fst (ppow a b)) mod q, (snd (ppow a b)) mod q). generalize q_pos; intros HM. generalize q_pos2; intros HM2. @@ -362,7 +362,7 @@ rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. unfold zpow; rewrite gpow_gpow; auto with zarith. generalize zpow_w_n_minus_1; unfold zpow; intros H1; rewrite H1; clear H1. simpl; unfold zpmult, pmult. -repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || +repeat (rewrite Zmult_0_l || rewrite Zmult_0_r || rewrite Zplus_0_l || rewrite Zplus_0_r || rewrite Zmult_1_r). eq_tac; auto. pattern (-1 mod q) at 1; rewrite <- (Zmod_mod (-1) q); auto with zarith. @@ -371,7 +371,7 @@ rewrite Zmod_small; auto with zarith. apply w_in_pgroup. Qed. -(************************************** +(************************************** As e = (1, 0), the previous equation implies that the order of the group divide 2^p **************************************) @@ -385,7 +385,7 @@ apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. exact zpow_w_n. Qed. -(************************************** +(************************************** So it is less than equal **************************************) @@ -396,19 +396,19 @@ apply Zpower_gt_0; auto with zarith. apply e_order_divide_pow. Qed. -(************************************** +(************************************** So order(w) must be 2^q **************************************) Theorem e_order_eq_pow: exists q, (e_order P_dec w pgroup) = 2 ^ q. -case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith. +case (Zdivide_power_2 (e_order P_dec w pgroup) 2 p); auto with zarith. apply Zlt_le_weak; apply e_order_pos. apply prime_2. apply e_order_divide_pow; auto. intros x H; exists x; auto with zarith. Qed. -(************************************** +(************************************** Buth this q can only be p otherwise it would contradict w^2^(p -1) = (-1, 0) **************************************) @@ -449,7 +449,7 @@ apply (gpow_e_order_is_e _ P_dec _ w pgroup). apply w_in_pgroup. Qed. -(************************************** +(************************************** We have then the expected conclusion **************************************) @@ -483,7 +483,7 @@ Qed. End Lucas. -(************************************** +(************************************** We build the sequence in Z **************************************) @@ -494,7 +494,7 @@ Definition SS p := | _ => (Zmodd 4 n) end. -Theorem SS_aux_correct: +Theorem SS_aux_correct: forall p z1 z2 n, 0 <= n -> 0 < z1 -> z2 = fst (s n) mod z1 -> iter_pos _ (fun x => Zmodd (Zsquare x - 2) z1) z2 p = fst (s (n + Zpos p)) mod z1. intros p; pattern p; apply Pind. @@ -558,7 +558,7 @@ pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith. replace (p - 1 + 1) with p; auto with zarith. Qed. -(************************************** +(************************************** The test **************************************) @@ -594,4 +594,3 @@ Qed. Theorem prime524287: prime 524287. exact (LucasTest 19 (refl_equal _)). Qed. - |