diff options
Diffstat (limited to 'coqprime/Coqprime/PocklingtonCertificat.v')
| -rw-r--r-- | coqprime/Coqprime/PocklingtonCertificat.v | 755 |
1 files changed, 0 insertions, 755 deletions
diff --git a/coqprime/Coqprime/PocklingtonCertificat.v b/coqprime/Coqprime/PocklingtonCertificat.v deleted file mode 100644 index 9d3a032fd..000000000 --- a/coqprime/Coqprime/PocklingtonCertificat.v +++ /dev/null @@ -1,755 +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 List. -Require Import ZArith. -Require Import Zorder. -Require Import ZCAux. -Require Import LucasLehmer. -Require Import Pocklington. -Require Import ZCmisc. -Require Import Pmod. - -Definition dec_prime := list (positive * positive). - -Inductive singleCertif : Set := - | Proof_certif : forall N:positive, prime N -> singleCertif - | Lucas_certif : forall (n:positive) (p: Z), singleCertif - | Pock_certif : forall N a : positive, dec_prime -> positive -> singleCertif - | SPock_certif : forall N a : positive, dec_prime -> singleCertif - | Ell_certif: forall (N S: positive) (l: list (positive * positive)) - (A B x y: Z), singleCertif. - -Definition Certif := list singleCertif. - -Definition nprim sc := - match sc with - | Proof_certif n _ => n - | Lucas_certif n _ => n - | Pock_certif n _ _ _ => n - | SPock_certif n _ _ => n - | Ell_certif n _ _ _ _ _ _ => n - - end. - -Open Scope positive_scope. -Open Scope P_scope. - -Fixpoint pow (a p:positive) {struct p} : positive := - match p with - | xH => a - | xO p' =>let z := pow a p' in square z - | xI p' => let z := pow a p' in square z * a - end. - -Definition mkProd' (l:dec_prime) := - fold_right (fun (k:positive*positive) r => times (fst k) r) 1%positive l. - -Definition mkProd_pred (l:dec_prime) := - fold_right (fun (k:positive*positive) r => - if ((snd k) ?= 1)%P then r else times (pow (fst k) (Ppred (snd k))) r) - 1%positive l. - -Definition mkProd (l:dec_prime) := - fold_right (fun (k:positive*positive) r => times (pow (fst k) (snd k)) r) 1%positive l. - -(* [pow_mod a m n] return [a^m mod n] *) -Fixpoint pow_mod (a m n : positive) {struct m} : N := - match m with - | xH => (a mod n)%P - | xO m' => - let z := pow_mod a m' n in - match z with - | N0 => 0%N - | Npos z' => ((square z') mod n)%P - end - | xI m' => - let z := pow_mod a m' n in - match z with - | N0 => 0%N - | Npos z' => (((square z') * a)%P mod n)%P - end - end. - -Definition Npow_mod a m n := - match a with - | N0 => 0%N - | Npos a => pow_mod a m n - end. - -(* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *) -(* invariant a mod N = a *) -Definition fold_pow_mod a l n := - fold_left - (fun a' (qp:positive*positive) => Npow_mod a' (fst qp) n) - l a. - -Definition times_mod x y n := - match x, y with - | N0, _ => N0 - | _, N0 => N0 - | Npos x, Npos y => ((x * y)%P mod n) - end. - -Definition Npred_mod p n := - match p with - | N0 => Npos (Ppred n) - | Npos p => - if (p ?= 1) then N0 - else Npos (Ppred p) - end. - -Fixpoint all_pow_mod (prod a : N) (l:dec_prime) (n:positive) {struct l}: N*N := - match l with - | nil => (prod,a) - | (q,_) :: l => - let m := Npred_mod (fold_pow_mod a l n) n in - all_pow_mod (times_mod prod m n) (Npow_mod a q n) l n - end. - -Fixpoint pow_mod_pred (a:N) (l:dec_prime) (n:positive) {struct l} : N := - match l with - | nil => a - | (q,p)::l => - if (p ?= 1) then pow_mod_pred a l n - else - let a' := iter_pos _ (fun x => Npow_mod x q n) a (Ppred p) in - pow_mod_pred a' l n - end. - -Definition is_odd p := - match p with - | xO _ => false - | _ => true - end. - -Definition is_even p := - match p with - | xO _ => true - | _ => false - end. - -Definition check_s_r s r sqrt := - match s with - | N0 => true - | Npos p => - match (Zminus (square r) (xO (xO (xO p)))) with - | Zpos x => - let sqrt2 := square sqrt in - let sqrt12 := square (Psucc sqrt) in - if sqrt2 ?< x then x ?< sqrt12 - else false - | Zneg _ => true - | Z0 => false - end - end. - -Definition test_pock N a dec sqrt := - if (2 ?< N) then - let Nm1 := Ppred N in - let F1 := mkProd dec in - match Nm1 / F1 with - | (Npos R1, N0) => - if is_odd R1 then - if is_even F1 then - if (1 ?< a) then - let (s,r') := (R1 / (xO F1))in - match r' with - | Npos r => - let A := pow_mod_pred (pow_mod a R1 N) dec N in - match all_pow_mod 1%N A dec N with - | (Npos p, Npos aNm1) => - if (aNm1 ?= 1) then - if gcd p N ?= 1 then - if check_s_r s r sqrt then - (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1) - else false - else false - else false - | _ => false - end - | _ => false - end - else false - else false - else false - | _=> false - end - else false. - -Fixpoint is_in (p : positive) (lc : Certif) {struct lc} : bool := - match lc with - | nil => false - | c :: l => if p ?= (nprim c) then true else is_in p l - end. - -Fixpoint all_in (lc : Certif) (lp : dec_prime) {struct lp} : bool := - match lp with - | nil => true - | (p,_) :: lp => - if all_in lc lp - then is_in p lc - else false - end. - -Definition gt2 n := - match n with - | Zpos p => (2 ?< p)%positive - | _ => false - end. - -Fixpoint test_Certif (lc : Certif) : bool := - match lc with - | nil => true - | (Proof_certif _ _) :: lc => test_Certif lc - | (Lucas_certif n p) :: lc => - if test_Certif lc then - if gt2 p then - match Mp p with - | Zpos n' => - if (n ?= n') then - match SS p with - | Z0 => true - | _ => false - end - else false - | _ => false - end - else false - else false - | (Pock_certif n a dec sqrt) :: lc => - if test_pock n a dec sqrt then - if all_in lc dec then test_Certif lc else false - else false -(* Shoudl be done later to do it with Z *) - | (SPock_certif n a dec) :: lc => false - | (Ell_certif _ _ _ _ _ _ _):: lc => false - end. - -Lemma pos_eq_1_spec : - forall p, - if (p ?= 1)%P then p = xH - else (1 < p). -Proof. - unfold Zlt;destruct p;simpl; auto; red;reflexivity. -Qed. - -Open Scope Z_scope. -Lemma mod_unique : forall b q1 r1 q2 r2, - 0 <= r1 < b -> - 0 <= r2 < b -> - b * q1 + r1 = b * q2 + r2 -> - q1 = q2 /\ r1 = r2. -Proof with auto with zarith. - intros b q1 r1 q2 r2 H1 H2 H3. - assert (r2 = (b * q1 + r1) -b*q2). rewrite H3;ring. - assert (b*(q2 - q1) = r1 - r2 ). rewrite H;ring. - assert (-b < r1 - r2 < b). omega. - destruct (Ztrichotomy q1 q2) as [H5 | [H5 | H5]]. - assert (q2 - q1 >= 1). omega. - assert (r1- r2 >= b). - rewrite <- H0. - pattern b at 2; replace b with (b*1). - apply Zmult_ge_compat_l; omega. ring. - elimtype False; omega. - split;trivial. rewrite H;rewrite H5;ring. - assert (r1- r2 <= -b). - rewrite <- H0. - replace (-b) with (b*(-1)); try (ring;fail). - apply Zmult_le_compat_l; omega. - elimtype False; omega. -Qed. - -Lemma Zge_0_pos : forall p:positive, p>= 0. -Proof. - intros;unfold Zge;simpl;intro;discriminate. -Qed. - -Lemma Zge_0_pos_add : forall p:positive, p+p>= 0. -Proof. - intros;simpl;apply Zge_0_pos. -Qed. - -Hint Resolve Zpower_gt_0 Zlt_0_pos Zge_0_pos Zlt_le_weak Zge_0_pos_add: zmisc. - -Hint Rewrite Zpos_mult Zpower_mult Zpower_1_r Zmod_mod Zpower_exp - times_Zmult square_Zmult Psucc_Zplus: zmisc. - -Ltac mauto := - trivial;autorewrite with zmisc;trivial;auto with zmisc zarith. - -Lemma mod_lt : forall a (b:positive), a mod b < b. -Proof. - intros a b;destruct (Z_mod_lt a b);mauto. -Qed. -Hint Resolve mod_lt : zmisc. - -Lemma Zmult_mod_l : forall (n:positive) a b, (a mod n * b) mod n = (a * b) mod n. -Proof with mauto. - intros;rewrite Zmult_mod ... rewrite (Zmult_mod a) ... -Qed. - -Lemma Zmult_mod_r : forall (n:positive) a b, (a * (b mod n)) mod n = (a * b) mod n. -Proof with mauto. - intros;rewrite Zmult_mod ... rewrite (Zmult_mod a) ... -Qed. - -Lemma Zminus_mod_l : forall (n:positive) a b, (a mod n - b) mod n = (a - b) mod n. -Proof with mauto. - intros;rewrite Zminus_mod ... rewrite (Zminus_mod a) ... -Qed. - -Lemma Zminus_mod_r : forall (n:positive) a b, (a - (b mod n)) mod n = (a - b) mod n. -Proof with mauto. - intros;rewrite Zminus_mod ... rewrite (Zminus_mod a) ... -Qed. - -Hint Rewrite Zmult_mod_l Zmult_mod_r Zminus_mod_l Zminus_mod_r : zmisc. -Hint Rewrite <- Zpower_mod : zmisc. - -Lemma Pmod_Zmod : forall a b, Z_of_N (a mod b)%P = a mod b. -Proof. - intros a b; rewrite Pmod_div_eucl. - assert (b>0). mauto. - unfold Zmod; assert (H1 := Z_div_mod a b H). - destruct (Zdiv_eucl a b) as (q2, r2). - assert (H2 := div_eucl_spec a b). - assert (Z_of_N (fst (a / b)%P) = q2 /\ Z_of_N (snd (a/b)%P) = r2). - destruct H1;destruct H2. - apply mod_unique with b;mauto. - split;mauto. - unfold Zle;destruct (snd (a / b)%P);intro;discriminate. - rewrite <- H0;symmetry;rewrite Zmult_comm;trivial. - destruct H0;auto. -Qed. -Hint Rewrite Pmod_Zmod : zmisc. - -Lemma Zpower_0 : forall p : positive, 0^p = 0. -Proof. - intros;simpl;destruct p;unfold Zpower_pos;simpl;trivial. - generalize (iter_pos Z (Z.mul 0) 1 p). - induction p;simpl;trivial. -Qed. - -Lemma pow_Zpower : forall a p, Zpos (pow a p) = a ^ p. -Proof. - induction p; mauto; simpl; mauto; rewrite IHp; mauto. -Qed. -Hint Rewrite pow_Zpower : zmisc. - -Lemma pow_mod_spec : forall n a m, Z_of_N (pow_mod a m n) = a^m mod n. -Proof. - induction m; mauto; simpl; intros; mauto. - rewrite Zmult_mod; auto with zmisc. - rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. - rewrite <- IHm; mauto. - destruct (pow_mod a m n); mauto. - rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. - rewrite <- IHm. destruct (pow_mod a m n);simpl; mauto. -Qed. -Hint Rewrite pow_mod_spec Zpower_0 : zmisc. - -Lemma Npow_mod_spec : forall a p n, Z_of_N (Npow_mod a p n) = a^p mod n. -Proof. - intros a p n;destruct a; mauto; simpl; mauto. -Qed. -Hint Rewrite Npow_mod_spec : zmisc. - -Lemma iter_Npow_mod_spec : forall n q p a, - Z_of_N (iter_pos N (fun x : N => Npow_mod x q n) a p) = a^q^p mod n. -Proof. - induction p; mauto; intros; simpl Pos.iter; mauto; repeat rewrite IHp. - rewrite (Zpower_mod ((a ^ q ^ p) ^ q ^ p));auto with zmisc. - rewrite (Zpower_mod (a ^ q ^ p)); mauto. - mauto. -Qed. -Hint Rewrite iter_Npow_mod_spec : zmisc. - -Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), - Z_of_N a = a mod n -> - Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n. -Proof. - unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; - intros; mauto. - rewrite IHl; mauto. -Qed. -Hint Rewrite fold_pow_mod_spec : zmisc. - -Lemma pow_mod_pred_spec : forall (n:positive) l (a:N), - Z_of_N a = a mod n -> - Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n. -Proof. - unfold pow_mod_pred;induction l;simpl mkProd;intros; mauto. - destruct a as (q,p). - simpl mkProd_pred. - destruct (p ?= 1)%P; rewrite IHl; mauto; simpl. -Qed. -Hint Rewrite pow_mod_pred_spec : zmisc. - -Lemma mkProd_pred_mkProd : forall l, - (mkProd_pred l)*(mkProd' l) = mkProd l. -Proof. - induction l;simpl;intros; mauto. - generalize (pos_eq_1_spec (snd a)); destruct (snd a ?= 1)%P;intros. - rewrite H; mauto. - replace (mkProd_pred l * (fst a * mkProd' l)) with - (fst a *(mkProd_pred l * mkProd' l));try ring. - rewrite IHl; mauto. - rewrite Zmult_assoc. rewrite times_Zmult. - rewrite (Zmult_comm (pow (fst a) (Ppred (snd a)) * mkProd_pred l)). - rewrite Zmult_assoc. rewrite pow_Zpower. rewrite <-Ppred_Zminus;trivial. - rewrite <- Zpower_Zsucc; try omega. - replace (Zsucc (snd a - 1)) with ((snd a - 1)+1). - replace ((snd a - 1)+1) with (Zpos (snd a)); mauto. - rewrite <- IHl;repeat rewrite Zmult_assoc; mauto. - destruct (snd a - 1);trivial. - assert (1 < snd a); auto with zarith. -Qed. -Hint Rewrite mkProd_pred_mkProd : zmisc. - -Lemma lt_Zmod : forall p n, 0 <= p < n -> p mod n = p. -Proof. - intros a b H. - assert ( 0 <= a mod b < b). - apply Z_mod_lt; mauto. - destruct (mod_unique b (a/b) (a mod b) 0 a H0 H); mauto. - rewrite <- Z_div_mod_eq; mauto. -Qed. - -Lemma Npred_mod_spec : forall p n, Z_of_N p < Zpos n -> - 1 < Zpos n -> Z_of_N (Npred_mod p n) = (p - 1) mod n. -Proof. - destruct p;intros;simpl. - rewrite <- Ppred_Zminus; auto. - apply Zmod_unique with (q := -1); mauto. - assert (H1 := pos_eq_1_spec p);destruct (p?=1)%P. - rewrite H1; mauto. - unfold Z_of_N;rewrite <- Ppred_Zminus; auto. - simpl in H;symmetry; apply (lt_Zmod (p-1) n). - assert (1 < p); auto with zarith. -Qed. -Hint Rewrite Npred_mod_spec : zmisc. - -Lemma times_mod_spec : forall x y n, Z_of_N (times_mod x y n) = (x * y) mod n. -Proof. - intros; destruct x; mauto. - destruct y;simpl; mauto. -Qed. -Hint Rewrite times_mod_spec : zmisc. - -Lemma snd_all_pow_mod : - forall n l (prod a :N), - a mod (Zpos n) = a -> - Z_of_N (snd (all_pow_mod prod a l n)) = (a^(mkProd' l)) mod n. -Proof. - induction l; simpl all_pow_mod; simpl mkProd';intros; mauto. - destruct a as (q,p). - rewrite IHl; mauto. -Qed. - -Lemma fold_aux : forall a N (n:positive) l prod, - fold_left - (fun (r : Z) (k : positive * positive) => - r * (a ^(N / fst k) - 1) mod n) l (prod mod n) mod n = - fold_left - (fun (r : Z) (k : positive * positive) => - r * (a^(N / fst k) - 1)) l prod mod n. -Proof. - induction l;simpl;intros; mauto. -Qed. - -Lemma fst_all_pow_mod : - forall (n a:positive) l (R:positive) (prod A :N), - 1 < n -> - Z_of_N prod = prod mod n -> - Z_of_N A = a^R mod n -> - Z_of_N (fst (all_pow_mod prod A l n)) = - (fold_left - (fun r (k:positive*positive) => - (r * (a ^ (R* mkProd' l / (fst k)) - 1))) l prod) mod n. -Proof. - induction l;simpl;intros; mauto. - destruct a0 as (q,p);simpl. - assert (Z_of_N A = A mod n). - rewrite H1; mauto. - rewrite (IHl (R * q)%positive); mauto; mauto. - pattern (q * mkProd' l) at 2;rewrite (Zmult_comm q). - repeat rewrite Zmult_assoc. - rewrite Z_div_mult;auto with zmisc zarith. - rewrite <- fold_aux. - rewrite <- (fold_aux a (R * q * mkProd' l) n l (prod * (a ^ (R * mkProd' l) - 1)))... - assert ( ((prod * (A ^ mkProd' l - 1)) mod n) = - ((prod * ((a ^ R) ^ mkProd' l - 1)) mod n)). - repeat rewrite (Zmult_mod prod);auto with zmisc. - rewrite Zminus_mod;auto with zmisc. - rewrite (Zminus_mod ((a ^ R) ^ mkProd' l));auto with zmisc. - rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1; mauto. - rewrite H3; mauto. - rewrite H1; mauto. -Qed. - -Lemma is_odd_Zodd : forall p, is_odd p = true -> Zodd p. -Proof. - destruct p;intros;simpl;trivial;discriminate. -Qed. - -Lemma is_even_Zeven : forall p, is_even p = true -> Zeven p. -Proof. - destruct p;intros;simpl;trivial;discriminate. -Qed. - -Lemma lt_square : forall x y, 0 < x -> x < y -> x*x < y*y. -Proof. - intros; apply Zlt_trans with (x*y). - apply Zmult_lt_compat_l;trivial. - apply Zmult_lt_compat_r;trivial. omega. -Qed. - -Lemma le_square : forall x y, 0 <= x -> x <= y -> x*x <= y*y. -Proof. - intros; apply Zle_trans with (x*y). - apply Zmult_le_compat_l;trivial. - apply Zmult_le_compat_r;trivial. omega. -Qed. - -Lemma borned_square : forall x y, 0 <= x -> 0 <= y -> - x*x < y*y < (x+1)*(x+1) -> False. -Proof. - intros;destruct (Z_lt_ge_dec x y) as [z|z]. - assert (x + 1 <= y). omega. - assert (0 <= x+1). omega. - assert (H4 := le_square _ _ H3 H2). omega. - assert (H4 := le_square _ _ H0 (Zge_le _ _ z)). omega. -Qed. - -Lemma not_square : forall (sqrt:positive) n, sqrt * sqrt < n < (sqrt+1)*(sqrt + 1) -> ~(isSquare n). -Proof. - intros sqrt n H (y,H0). - destruct (Z_lt_ge_dec 0 y). - apply (borned_square sqrt y);mauto. - assert (y*y = (-y)*(-y)). ring. rewrite H1 in H0;clear H1. - apply (borned_square sqrt (-y));mauto. -Qed. - -Ltac spec_dec := - repeat match goal with - | [H:(?x ?= ?y)%P = _ |- _] => - generalize (is_eq_spec x y); - rewrite H;clear H; autorewrite with zmisc; - intro - | [H:(?x ?< ?y)%P = _ |- _] => - generalize (is_lt_spec x y); - rewrite H; clear H; autorewrite with zmisc; - intro - end. - -Ltac elimif := - match goal with - | [H: (if ?b then _ else _) = _ |- _] => - let H1 := fresh "H" in - (CaseEq b;intros H1; rewrite H1 in H; - try discriminate H); elimif - | _ => spec_dec - end. - -Lemma check_s_r_correct : forall s r sqrt, check_s_r s r sqrt = true -> - Z_of_N s = 0 \/ ~ isSquare (r * r - 8 * s). -Proof. - unfold check_s_r;intros. - destruct s as [|s]; trivial;auto. - right;CaseEq (square r - xO (xO (xO s)));[intros H1|intros p1 H1| intros p1 H1]; - rewrite H1 in H;try discriminate H. - elimif. - assert (Zpos (xO (xO (xO s))) = 8 * s). repeat rewrite Zpos_xO_add;ring. - generalizeclear H1; rewrite H2;mauto;intros. - apply (not_square sqrt). - simpl Z.of_N; rewrite H1;auto. - intros (y,Heq). - generalize H1 Heq;mauto. - unfold Z_of_N. - match goal with |- ?x = _ -> ?y = _ -> _ => - replace x with y; try ring - end. - intros Heq1;rewrite Heq1;intros Heq2. - destruct y;discriminate Heq2. -Qed. - -Lemma in_mkProd_prime_div_in : - forall p:positive, prime p -> - forall (l:dec_prime), - (forall k, In k l -> prime (fst k)) -> - Zdivide p (mkProd l) -> exists n,In (p, n) l. -Proof. - induction l;simpl mkProd; simpl In; mauto. - intros _ H1; absurd (p <= 1). - apply Zlt_not_le; apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. - apply Zdivide_le; auto with zarith. - intros. - case prime_mult with (2 := H1); auto with zarith; intros H2. - exists (snd a);left. - destruct a;simpl in *. - assert (Zpos p = Zpos p0). - rewrite (prime_div_Zpower_prime p1 p p0); mauto. - apply (H0 (p0,p1));auto. - inversion H3; auto. - destruct IHl as (n,H3); mauto. - exists n; auto. -Qed. - -Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P). -Proof. - intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros. - generalize (div_eucl_spec b a); mauto. - rewrite <- (Pmod_div_eucl b a). - CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2). - simpl in H1;rewrite Zplus_0_r in H1. - rewrite (gcd_mod0 _ _ Heq). - constructor;mauto. - apply Zdivide_intro with (fst (b/a)%P);trivial. - rewrite (gcd_mod _ _ _ Heq). - rewrite H1;apply Zis_gcd_sym. - rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *. - apply Zis_gcd_sym;auto. -Qed. - -Lemma test_pock_correct : forall N a dec sqrt, - (forall k, In k dec -> prime (Zpos (fst k))) -> - test_pock N a dec sqrt = true -> - prime N. -Proof. - unfold test_pock;intros. - elimif. - generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n); mauto;intros (H2,H3). - destruct R1 as [|R1];try discriminate H0. - destruct n;try discriminate H0. - elimif. - generalize (div_eucl_spec R1 (xO (mkProd dec))); - destruct ((R1 / xO (mkProd dec))%P) as (s,r'); mauto;intros (H7,H8). - destruct r' as [|r];try discriminate H0. - generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1 - (pow_mod_pred (pow_mod a R1 N) dec N)). - generalize (snd_all_pow_mod N dec 1 (pow_mod_pred (pow_mod a R1 N) dec N)). - destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as - (prod,aNm1); mauto; simpl Z_of_N. - destruct prod as [|prod];try discriminate H0. - destruct aNm1 as [|aNm1];try discriminate H0;elimif. - simpl in H3; simpl in H2. - rewrite <- Ppred_Zminus in H2;try omega. - rewrite <- Zmult_assoc;rewrite mkProd_pred_mkProd. - intros H12;assert (a^(N-1) mod N = 1). - pattern 1 at 2;rewrite <- H9;symmetry. - simpl Z.of_N in H12. - rewrite H2; rewrite H12; mauto. - rewrite <- Zpower_mult; mauto. - clear H12. - intros H14. - match type of H14 with _ -> _ -> _ -> ?X => - assert (H12:X); try apply H14; clear H14 - end; mauto. - rewrite Zmod_small; mauto. - assert (1 < mkProd dec). - assert (H14 := Zlt_0_pos (mkProd dec)). - assert (1 <= mkProd dec); mauto. - destruct (Zle_lt_or_eq _ _ H15); mauto. - inversion H16. rewrite <- H18 in H5;discriminate H5. - simpl in H8. - assert (Z_of_N s = R1 / (2 * mkProd dec) /\ Zpos r = R1 mod (2 * mkProd dec)). - apply mod_unique with (2 * mkProd dec);auto with zarith. - revert H8; mauto. - apply Z_mod_lt; mauto. - rewrite <- Z_div_mod_eq; mauto; rewrite H7. - simpl fst; simpl snd; simpl Z_of_N. - ring. - destruct H15 as (H15,Heqr). - apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1); - auto with zmisc zarith. - rewrite H2; mauto. - apply is_even_Zeven; auto. - apply is_odd_Zodd; auto. - intros p; case p; clear p. - intros HH; contradict HH. - apply not_prime_0. - 2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros; - discriminate. - intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith. - apply Zis_gcd_gcd; auto with zarith. - change (rel_prime (a ^ ((N - 1) / p) - 1) N). - match type of H12 with _ = ?X mod _ => - apply rel_prime_div with (p := X); auto with zarith - end. - apply rel_prime_mod_rev; auto with zarith. - red. - pattern 1 at 3; rewrite <- H10; rewrite <- H12. - apply Pmod.gcd_Zis_gcd. - destruct (in_mkProd_prime_div_in _ Hprime _ H Hdec) as (q,Hin). - revert H2; mauto; intro H2. - rewrite <- H2. - match goal with |- context [fold_left ?f _ _] => - apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) - with (b := (p, q)); auto with zarith - end. - rewrite <- Heqr. - generalizeclear H0; ring_simplify - (((mkProd dec + mkProd dec + r + 1) * mkProd dec + r) * mkProd dec + 1) - ((1 * mkProd dec + 1) * (2 * mkProd dec * mkProd dec + (r - 1) * mkProd dec + 1)); mauto. - rewrite <- H15;rewrite <- Heqr. - apply check_s_r_correct with sqrt; mauto. -Qed. - -Lemma is_in_In : - forall p lc, is_in p lc = true -> exists c, In c lc /\ p = nprim c. -Proof. - induction lc;simpl;try (intros;discriminate). - intros;elimif. - exists a;split;auto. inversion H0;trivial. - destruct (IHlc H) as [c [H1 H2]];exists c;auto. -Qed. - -Lemma all_in_In : - forall lc lp, all_in lc lp = true -> - forall pq, In pq lp -> exists c, In c lc /\ fst pq = nprim c. -Proof. - induction lp;simpl. intros H pq HF;elim HF. - intros;destruct a;elimif. - destruct H0;auto. - rewrite <- H0;simpl;apply is_in_In;trivial. -Qed. - -Lemma test_Certif_In_Prime : - forall lc, test_Certif lc = true -> - forall c, In c lc -> prime (nprim c). -Proof with mauto. - induction lc;simpl;intros. elim H0. - destruct H0. - subst c;destruct a;simpl... - elimif. - CaseEq (Mp p);[intros Heq|intros N' Heq|intros N' Heq];rewrite Heq in H; - try discriminate H. elimif. - CaseEq (SS p);[intros Heq'|intros N'' Heq'|intros N'' Heq'];rewrite Heq' in H; - try discriminate H. - rewrite H2;rewrite <- Heq. -apply LucasLehmer;trivial. -(destruct p; try discriminate H1). -simpl in H1; generalize (is_lt_spec 2 p); rewrite H1; auto. -elimif. -apply (test_pock_correct N a d p); mauto. - intros k Hin;destruct (all_in_In _ _ H1 _ Hin) as (c,(H2,H3)). - rewrite H3;auto. -discriminate. -discriminate. - destruct a;elimif;auto. -discriminate. -discriminate. -Qed. - -Lemma Pocklington_refl : - forall c lc, test_Certif (c::lc) = true -> prime (nprim c). -Proof. - intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto. -Qed. |