diff options
Diffstat (limited to 'coqprime/num/Pock.v')
| -rw-r--r-- | coqprime/num/Pock.v | 964 |
1 files changed, 0 insertions, 964 deletions
diff --git a/coqprime/num/Pock.v b/coqprime/num/Pock.v deleted file mode 100644 index 3b467af5a..000000000 --- a/coqprime/num/Pock.v +++ /dev/null @@ -1,964 +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 ZArith Znumtheory Zpow_facts. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31. -Require Import Pmod. -Require Import Mod_op. -Require Import W. -Require Import Lucas. -Require Export PocklingtonCertificat. -Require Import NEll. -Import CyclicAxioms DoubleType DoubleBase List. - -Open Scope Z_scope. - -Section test. - -Variable w: Type. -Variable w_op: ZnZ.Ops w. -Variable op_spec: ZnZ.Specs w_op. -Variable p: positive. -Variable b: w. - -Notation "[| x |]" := - (ZnZ.to_Z x) (at level 0, x at level 99). - -Hypothesis b_pos: 0 < [|b|]. - -Variable m_op: mod_op w. -Variable m_op_spec: mod_spec w_op b m_op. - -Open Scope positive_scope. -Open Scope P_scope. - -Let pow := m_op.(power_mod). -Let times := m_op.(mul_mod). -Let pred:= m_op.(pred_mod). - -(* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *) -(* invariant a mod N = a *) -Definition fold_pow_mod (a: w) l := - fold_left - (fun a' (qp:positive*positive) => pow a' (fst qp)) - l a. - -Lemma fold_pow_mod_spec : forall l (a:w), - ([|a|] < [|b|])%Z -> [|fold_pow_mod a l|] = ([|a|]^(mkProd' l) mod [|b|])%Z. -intros l; unfold fold_pow_mod; elim l; simpl fold_left; simpl mkProd'; auto; clear l. -intros a H; rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. -case (ZnZ.spec_to_Z a); auto with zarith. -intros (p1, q1) l Rec a H. -case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2. -rewrite Rec. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -rewrite <- Zpower_mod. -rewrite times_Zmult; rewrite Zpower_mult; auto with zarith. -apply Zle_lt_trans with (2 := H); auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -Qed. - - -Fixpoint all_pow_mod (prod a: w) (l:dec_prime) {struct l}: w*w := - match l with - | nil => (prod,a) - | (q,_) :: l => - let m := pred (fold_pow_mod a l) in - all_pow_mod (times prod m) (pow a q) l - end. - - -Lemma snd_all_pow_mod : - forall l (prod a :w), ([|a|] < [|b|])%Z -> - [|snd (all_pow_mod prod a l)|] = ([|a|]^(mkProd' l) mod [|b|])%Z. -intros l; elim l; simpl all_pow_mod; simpl mkProd'; simpl snd; clear l. -intros _ a H; rewrite Zpower_1_r; auto with zarith. -rewrite Zmod_small; auto with zarith. -case (ZnZ.spec_to_Z a); auto with zarith. -intros (p1, q1) l Rec prod a H. -case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2. -rewrite Rec; auto with zarith. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -rewrite <- Zpower_mod. -rewrite times_Zmult; rewrite Zpower_mult; auto with zarith. -apply Zle_lt_trans with (2 := H); auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -Qed. - -Lemma fold_aux : forall a N l prod, - (fold_left - (fun (r : Z) (k : positive * positive) => - r * (a ^(N / fst k) - 1) mod [|b|]) l (prod mod [|b|]) mod [|b|] = - fold_left - (fun (r : Z) (k : positive * positive) => - r * (a^(N / fst k) - 1)) l prod mod [|b|])%Z. -induction l;simpl;intros. -rewrite Zmod_mod; auto with zarith. -rewrite <- IHl; auto with zarith. -rewrite Zmult_mod; auto with zarith. -rewrite Zmod_mod; auto with zarith. -rewrite <- Zmult_mod; auto with zarith. -Qed. - -Lemma fst_all_pow_mod : - forall l (a:w) (R:positive) (prod A :w), - [|prod|] = ([|prod|] mod [|b|])%Z -> - [|A|] = ([|a|]^R mod [|b|])%Z -> - [|fst (all_pow_mod prod A l)|] = - ((fold_left - (fun r (k:positive*positive) => - (r * ([|a|] ^ (R* mkProd' l / (fst k)) - 1))) l [|prod|]) mod [|b|])%Z. -intros l; elim l; simpl all_pow_mod; simpl fold_left; simpl fst; - auto with zarith; clear l. -intros (p1,q1) l Rec; simpl fst. -intros a R prod A H1 H2. -assert (F: (0 <= [|A|] < [|b|])%Z). -rewrite H2. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -assert (F1: ((fun x => x = x mod [|b|])%Z [|fold_pow_mod A l|])). -rewrite Zmod_small; auto. -rewrite fold_pow_mod_spec; auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -assert (F2: ((fun x => x = x mod [|b|])%Z [|pred (fold_pow_mod A l)|])). -rewrite Zmod_small; auto. -rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]); - auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite (Rec a (R * p1)%positive); auto with zarith. -rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]); - auto with zarith. -rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]); - auto with zarith. -rewrite fold_pow_mod_spec; auto with zarith. -rewrite H2. -repeat rewrite Zpos_mult. -repeat rewrite times_Zmult. -repeat rewrite <- Zmult_assoc. -apply sym_equal; rewrite <- fold_aux; auto with zarith. -apply sym_equal; rewrite <- fold_aux; auto with zarith. -eq_tac; auto. -match goal with |- context[fold_left ?x _ _] => - apply f_equal2 with (f := fold_left x); auto with zarith -end. -rewrite Zmod_mod; auto with zarith. -rewrite (Zmult_comm R); repeat rewrite <- Zmult_assoc; - rewrite (Zmult_comm p1); rewrite Z_div_mult; auto with zarith. -repeat rewrite (Zmult_mod [|prod|]);auto with zmisc. -eq_tac; [idtac | eq_tac]; auto. -eq_tac; auto. -rewrite Zmod_mod; auto. -repeat rewrite (fun x => Zminus_mod x 1); auto with zarith. -eq_tac; auto; eq_tac; auto. -rewrite Zmult_comm; rewrite <- Zpower_mod; auto with zmisc. -rewrite Zpower_mult; auto with zarith. -rewrite Zmod_mod; auto with zarith. -rewrite Zmod_small; auto. -rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]); - auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); - auto with zarith. -apply trans_equal with ([|A|] ^ p1 mod [|b|])%Z; auto. -rewrite H2. -rewrite Zpos_mult_morphism; rewrite Zpower_mult; auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -rewrite Zmod_small; auto. -Qed. - - -Fixpoint pow_mod_pred (a:w) (l:dec_prime) {struct l} : w := - match l with - | nil => a - | (q, p)::l => - if (p ?= 1) then pow_mod_pred a l - else - let a' := iter_pos (Ppred p) _ (fun x => pow x q) a in - pow_mod_pred a' l - end. - -Lemma iter_pow_mod_spec : forall q p a, [|a|] = ([|a|] mod [|b|])%Z -> - ([|iter_pos p _ (fun x => pow x q) a|] = [|a|]^q^p mod [|b|])%Z. -intros q1 p1; elim p1; simpl iter_pos; clear p1. -intros p1 Rec a Ha. -rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); - auto with zarith. -repeat rewrite Rec; auto with zarith. -match goal with |- (Zpower_pos ?X ?Y mod ?Z = _)%Z => - apply trans_equal with (X ^ Y mod Z)%Z; auto -end. -repeat rewrite <- Zpower_mod; auto with zmisc. -repeat rewrite <- Zpower_mult; auto with zmisc. -repeat rewrite <- Zpower_mod; auto with zmisc. -repeat rewrite <- Zpower_mult; auto with zarith zmisc. -eq_tac; auto. -eq_tac; auto. -rewrite Zpos_xI. -assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp; - clear tmp. -repeat rewrite Zpower_exp; auto with zarith. -rewrite Zpower_1_r; try ring; auto with misc. -rewrite Zmod_mod; auto with zarith. -rewrite Rec; auto with zmisc. -rewrite Zmod_mod; auto with zarith. -rewrite Rec; auto with zmisc. -rewrite Zmod_mod; auto with zarith. -intros p1 Rec a Ha. -repeat rewrite Rec; auto with zarith. -repeat rewrite <- Zpower_mod; auto with zmisc. -repeat rewrite <- Zpower_mult; auto with zmisc. -eq_tac; auto. -eq_tac; auto. -rewrite Zpos_xO. -assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp; - clear tmp. -repeat rewrite Zpower_exp; auto with zarith. -rewrite Zmod_mod; auto with zarith. -intros a Ha; rewrite Zpower_1_r; auto with zarith. -rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); - auto with zarith. -Qed. - -Lemma pow_mod_pred_spec : forall l a, - ([|a|] = [|a|] mod [|b|] -> - [|pow_mod_pred a l|] = [|a|]^(mkProd_pred l) mod [|b|])%Z. -intros l; elim l; simpl pow_mod_pred; simpl mkProd_pred; clear l. -intros; rewrite Zpower_1_r; auto with zarith. -intros (p1,q1) l Rec a H; simpl snd; simpl fst. -case (q1 ?= 1)%P; auto with zarith. -rewrite Rec; auto. -rewrite iter_pow_mod_spec; auto with zarith. -rewrite times_Zmult; rewrite pow_Zpower. -rewrite <- Zpower_mod; auto with zarith. -rewrite Zpower_mult; auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite iter_pow_mod_spec; auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -Qed. - -End test. - -Require Import Bits. - -Definition test_pock N a dec sqrt := - if (2 ?< N) then - let Nm1 := Ppred N in - let F1 := mkProd dec in - match (Nm1 / F1)%P with - | (Npos R1, N0) => - if is_odd R1 then - if is_even F1 then - if (1 ?< a) then - let (s,r') := (R1 / (xO F1))%P in - match r' with - | Npos r => - if (a ?< N) then - let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in - let wN := znz_of_Z op (Zpos N) in - let wa := znz_of_Z op (Zpos a) in - let w1 := znz_of_Z op 1 in - let mod_op := make_mod_op op wN in - let pow := mod_op.(power_mod) in - let ttimes := mod_op.(mul_mod) in - let pred:= mod_op.(pred_mod) in - let gcd:= ZnZ.gcd in - let A := pow_mod_pred _ mod_op (pow wa R1) dec in - match all_pow_mod _ mod_op w1 A dec with - | (p, aNm1) => - match ZnZ.to_Z aNm1 with - (Zpos xH) => - match ZnZ.to_Z (gcd p wN) with - (Zpos xH) => - if check_s_r s r sqrt then - (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1) - else false - | _ => false - end - | _ => false - end - end else false - | _ => false - end - else false - else false - else false - | _=> false - end - else false. - -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. -unfold test_pock;intros N a dec sqrt H. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If1; auto -end. -2: intros; discriminate. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n). -simpl fst; simpl snd; intros (H1, H2). -destruct R1 as [ |R1]. -intros; discriminate. -destruct n. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If2; auto -end. -assert (If0: Zodd R1). -apply is_odd_Zodd; auto. -clear If2; rename If0 into If2. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If3; auto -end. -assert (If0: Zeven (mkProd dec)). -apply is_even_Zeven; auto. -clear If3; rename If0 into If3. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If4; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -2: intros; discriminate. -generalize (div_eucl_spec R1 (xO (mkProd dec))); - destruct ((R1 / xO (mkProd dec))%P) as (s,r'); simpl fst; - simpl snd; intros (H3, H4). -destruct r' as [ |r]. -intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If5; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -2: intros; discriminate. -set (bb := Peano.pred (nat_of_P (get_height 31 (plength N)))). -set (w_op := cmk_op bb). -assert (op_spec: ZnZ.Specs w_op). -unfold bb, w_op; apply cmk_spec; auto. -assert (F0: N < DoubleType.base (ZnZ.digits w_op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold w_op, DoubleType.base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold bb. - set (p := plength N). - replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (F1: ZnZ.to_Z (ZnZ.of_Z N) = N). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F2: 1 < ZnZ.to_Z (ZnZ.of_Z N)). -rewrite F1; auto with zarith. -assert (F3: 0 < ZnZ.to_Z (ZnZ.of_Z N)); auto with zarith. -assert (F4: ZnZ.to_Z (ZnZ.of_Z a) = a). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F5: ZnZ.to_Z (ZnZ.of_Z 1) = 1). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec). -rewrite Zpos_mult. -rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith. -simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus; - auto with zarith. -assert (m_spec: mod_spec w_op (znz_of_Z w_op N) - (make_mod_op w_op (znz_of_Z w_op N))). -apply make_mod_spec; auto with zarith. -match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] => - generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec - u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t); - generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t); - fold bb w_op; - case (all_pow_mod x y z t u); simpl fst; simpl snd -end. -intros prod aNm1; intros H5 H6. -case_eq (ZnZ.to_Z aNm1). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If6. -case_eq (ZnZ.to_Z (ZnZ.gcd prod (znz_of_Z w_op N))). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If7. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If8; auto -end. -2: intros; discriminate. -intros If9. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -assert (U1: N - 1 = mkProd dec * R1). -rewrite <- Ppred_Zminus in H1; auto with zarith. -rewrite H1; simpl. -repeat rewrite Zpos_mult; auto with zarith. -assert (HH: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. -apply Z_mod_lt; auto with zarith. -rewrite <- Z_div_mod_eq; auto with zarith. -rewrite H3. -rewrite (Zpos_xO (mkProd dec)). -simpl Z_of_N; ring. -case HH; clear HH; intros HH1 HH2. -apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1); - auto with zmisc zarith. -case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith. -simpl in H2; auto with zarith. -intros HH; contradict If3; rewrite <- HH. -apply Zodd_not_Zeven; red; 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 trans_equal with (2 := If6). -rewrite H5. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -rewrite F1. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4. -rewrite <- Zpower_mod; auto with zarith. -rewrite <- Zpower_mult; auto with zarith. -rewrite mkProd_pred_mkProd; auto with zarith. -rewrite U1; rewrite Zmult_comm. -rewrite Zpower_mult; auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -match type of H6 with _ -> _ -> ?X => - assert (tmp: X); [apply H6 | clear H6; rename tmp into H6]; - auto with zarith -end. -rewrite F1. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1). -rewrite F5; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith. -rewrite Zpower_mult; auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -rewrite (power_mod_spec m_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4); auto. -rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N); auto. -auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a) in H6. -change (znz_of_Z w_op N) with (ZnZ.of_Z N) in H6. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1) in H6. -rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6. -case in_mkProd_prime_div_in with (3 := Hdec); auto. -intros p1 Hp1. -rewrite <- F6 in H6. -apply Zis_gcd_gcd; auto with zarith. -change (rel_prime (a ^ ((N - 1) / p) - 1) N). -match type of H6 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 4; rewrite <- If7; rewrite <- H6. -pattern N at 2; rewrite <- F1. -apply ZnZ.spec_gcd; auto with zarith. -assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b, - In b l -> (forall x, P (f x b)) -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a, - P a -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -intros A B f P l; elim l; simpl; auto. -intros A B f P l; elim l; simpl; auto. -intros a1 b HH; case HH. -intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto. -apply foldtmp0; auto. -apply Rec with (b := b); auto with zarith. -match goal with |- context [fold_left ?f _ _] => - apply (foldtmp _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) - with (b := (p, p1)); auto with zarith -end. -rewrite <- HH2. -clear F0; match goal with H: ?X < ?Y |- ?X < ?Z => - replace Z with Y; auto -end. -repeat (rewrite Zpos_plus || rewrite Zpos_mult || rewrite times_Zmult). -rewrite Zpos_xO; ring. -rewrite <- HH1; rewrite <- HH2. -apply check_s_r_correct with sqrt; auto. -Qed. - -(* Simple version of pocklington for primo *) -Definition test_spock N a dec := - if (2 ?< N) then - let Nm1 := Ppred N in - let F1 := mkProd dec in - match (Nm1 / F1)%P with - | (Npos R1, N0) => - if (1 ?< a) then - if (a ?< N) then - if (N ?< F1 * F1) then - let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in - let wN := znz_of_Z op (Zpos N) in - let wa := znz_of_Z op (Zpos a) in - let w1 := znz_of_Z op 1 in - let mod_op := make_mod_op op wN in - let pow := mod_op.(power_mod) in - let ttimes := mod_op.(mul_mod) in - let pred:= mod_op.(pred_mod) in - let gcd:= ZnZ.gcd in - let A := pow_mod_pred _ mod_op (pow wa R1) dec in - match all_pow_mod _ mod_op w1 A dec with - | (p, aNm1) => - match ZnZ.to_Z aNm1 with - (Zpos xH) => - match ZnZ.to_Z (gcd p wN) with - (Zpos xH) => true - | _ => false - end - | _ => false - end - end else false - else false - else false - | _=> false - end - else false. - -Lemma test_spock_correct : forall N a dec, - (forall k, In k dec -> prime (Zpos (fst k))) -> - test_spock N a dec = true -> - prime N. -unfold test_spock;intros N a dec H. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If1; auto -end. -2: intros; discriminate. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n). -simpl fst; simpl snd; intros (H1, H2). -destruct R1 as [ |R1]. -intros; discriminate. -destruct n. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If2; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -2: intros; discriminate. -(* -set (bb := pred (nat_of_P (get_height 31 (plength N)))). -set (w_op := cmk_op bb). -assert (op_spec: znz_spec w_op). -unfold bb, w_op; apply cmk_spec; auto. -assert (F0: N < Basic_type.base (znz_digits w_op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold w_op, Basic_type.base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold bb. - set (p := plength N). - replace (Z_of_nat (pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -*) -set (bb := Peano.pred (nat_of_P (get_height 31 (plength N)))). -set (w_op := cmk_op bb). -assert (op_spec: ZnZ.Specs w_op). -unfold bb, w_op; apply cmk_spec; auto. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If3; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If4; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -assert (F0: N < DoubleType.base (ZnZ.digits w_op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold w_op, DoubleType.base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold bb. - set (p := plength N). - replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (F1: ZnZ.to_Z (ZnZ.of_Z N) = N). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F2: 1 < ZnZ.to_Z (ZnZ.of_Z N)). -rewrite F1; auto with zarith. -assert (F3: 0 < ZnZ.to_Z (ZnZ.of_Z N)); auto with zarith. -assert (F4: ZnZ.to_Z (ZnZ.of_Z a) = a). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F5: ZnZ.to_Z (ZnZ.of_Z 1) = 1). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec). -rewrite Zpos_mult. -rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith. -simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus; - auto with zarith. -assert (m_spec: mod_spec w_op (znz_of_Z w_op N) - (make_mod_op w_op (znz_of_Z w_op N))). -apply make_mod_spec; auto with zarith. -match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] => - generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec - u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t); - generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t); - fold bb w_op; - case (all_pow_mod x y z t u); simpl fst; simpl snd -end. -2: intros; discriminate. -intros prod aNm1; intros H5 H6. -case_eq (ZnZ.to_Z aNm1). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If5. -case_eq (ZnZ.to_Z (ZnZ.gcd prod (znz_of_Z w_op N))). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If6 _. -assert (U1: N - 1 = mkProd dec * R1). -rewrite <- Ppred_Zminus in H1; auto with zarith. -rewrite H1; simpl. -repeat rewrite Zpos_mult; auto with zarith. -apply PocklingtonCorollary1 with (F1:=mkProd dec) (R1:=R1); - auto with zmisc zarith. -case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith. -simpl in H2; auto with zarith. -intros HH; contradict If4; rewrite Zpos_mult_morphism; - rewrite <- HH. -apply Zle_not_lt; auto with zarith. -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 trans_equal with (2 := If5). -rewrite H5. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -rewrite F1. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4. -rewrite <- Zpower_mod; auto with zarith. -rewrite <- Zpower_mult; auto with zarith. -rewrite mkProd_pred_mkProd; auto with zarith. -rewrite U1; rewrite Zmult_comm. -rewrite Zpower_mult; auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -match type of H6 with _ -> _ -> ?X => - assert (tmp: X); [apply H6 | clear H6; rename tmp into H6]; - auto with zarith -end. -rewrite F1. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1). -rewrite F5; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -repeat (rewrite F1 || rewrite F4). -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith. -rewrite Zpower_mult; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N) in H6. -change (znz_of_Z w_op a) with (ZnZ.of_Z a) in H6. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1) in H6. -rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6. -case in_mkProd_prime_div_in with (3 := Hdec); auto. -intros p1 Hp1. -rewrite <- F6 in H6. -apply Zis_gcd_gcd; auto with zarith. -change (rel_prime (a ^ ((N - 1) / p) - 1) N). -match type of H6 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 4; rewrite <- If6; rewrite <- H6. -pattern N at 2; rewrite <- F1. -apply ZnZ.spec_gcd; auto with zarith. -assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b, - In b l -> (forall x, P (f x b)) -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a, - P a -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -intros A B f P l; elim l; simpl; auto. -intros A B f P l; elim l; simpl; auto. -intros a1 b HH; case HH. -intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto. -apply foldtmp0; auto. -apply Rec with (b := b); auto with zarith. -match goal with |- context [fold_left ?f _ _] => - apply (foldtmp _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) - with (b := (p, p1)); auto with zarith -end. -intros; discriminate. -Qed. - -Fixpoint test_Certif (lc : Certif) : bool := - match lc with - | nil => true - | (Proof_certif _ _) :: lc => test_Certif lc - | (Lucas_certif n p) :: lc => - let xx := test_Certif lc in - if xx then - let yy := gt2 p in - if yy then - match p with - Zpos p1 => - let zz := Mp p in - match zz with - | Zpos n' => - if (n ?= n')%P then - let tt := lucas p1 in - match tt with - | Z0 => true - | _ => false - end - else false - | _ => false - end - | _ => false - end - else false - else false - | (Pock_certif n a dec sqrt) :: lc => - let xx := test_pock n a dec sqrt in - if xx then - let yy := all_in lc dec in - (if yy then test_Certif lc else false) - else false - | (SPock_certif n a dec) :: lc => - let xx :=test_spock n a dec in - if xx then - let yy := all_in lc dec in - (if yy then test_Certif lc else false) - else false - | (Ell_certif n ss l a b x y) :: lc => - let xx := ell_test n ss l a b x y in - if xx then - let yy := all_in lc l in - if yy then test_Certif lc else false - else false - end. - -Lemma test_Certif_In_Prime : - forall lc, test_Certif lc = true -> - forall c, In c lc -> prime (nprim c). -intros lc; elim lc; simpl; auto. -intros _ c H; case H. -intros a; case a; simpl; clear a lc. -intros N p l Rec H c [H1 | H1]; subst; auto with arith. -intros n p l; case (test_Certif l); auto with zarith. -2: intros; discriminate. -intros H H1 c [H2 | H2]; subst; auto with arith. -simpl nprim. -generalize H1; clear H1. -case_eq (gt2 p). -2: intros; discriminate. -case p; clear p; try (intros; discriminate; fail). -unfold gt2; intros p H1. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -unfold Mp; case_eq (2 ^ p -1); try (intros; discriminate; fail). -intros p1 Hp1. -case_eq (n ?= p1)%P; try rewrite <- Hp1. -2: intros; discriminate. -intros H2. -match goal with H: (?X ?= ?Y)%P = true |- _ => - generalize (is_eq_eq _ _ H); clear H; intros H -end. -generalize (lucas_prime H1); rewrite Hp1; rewrite <- H2. -case (lucas p); try (intros; discriminate; fail); auto. -intros N a d p l H. -generalize (test_pock_correct N a d p). -case (test_pock N a d p); auto. -2: intros; discriminate. -generalize (all_in_In l d). -case (all_in l d). -2: intros; discriminate. -intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto. -apply H2; auto. -intros k Hk. -case H1 with (2 := Hk); auto. -intros x (Hx1, Hx2); rewrite Hx2; auto. -intros N a d l H. -generalize (test_spock_correct N a d). -case test_spock; auto. -2: intros; discriminate. -generalize (all_in_In l d). -case (all_in l d). -2: intros; discriminate. -intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto. -apply H2; auto. -intros k Hk. -case H1 with (2 := Hk); auto. -intros x (Hx1, Hx2); rewrite Hx2; auto. -intros N S l A B x y l1. -generalize (all_in_In l1 l). -generalize (ell_test_correct N S l A B x y). -case ell_test. -case all_in; auto. -intros H1 H2 H3 H4 c [H5 | H5]; try subst c; simpl; auto. -apply H1. -intros p Hp; case (H2 (refl_equal true) p); auto. -intros x1 (Hx1, Hx2); rewrite Hx2; auto. -intros; discriminate. -intros; 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. - |