proposition: 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.
proof: Proof. 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 (Pos.pred N) (mkProd dec)); destruct ((Pos.pred 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 := Peano.pred (nat_of_P (get_height 63 (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 Z.lt_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 63 (plength N)); unfold bb. set (p := plength N). replace (Z_of_nat (Peano.pred (nat_of_P (get_height 63 p)))) with ((Zpos (get_height 63 p) - 1) ). auto with zarith. rewrite <- Nat.sub_1_r; rewrite inj_minus1. rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. generalize (lt_O_nat_of_P (get_height 63 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. 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 by auto with zarith. rewrite H1; simpl. repeat rewrite Zpos_mult; auto with zarith. apply PocklingtonCorollary1 with (F1:=mkProd dec) (R1:=R1). case (Zle_lt_or_eq 1 (mkProd dec)). simpl in H2; auto with zarith. easy. intros HH; contradict If4; rewrite Zpos_mult_morphism; rewrite <- HH. apply Zle_not_lt; auto with zarith. 1-3: auto with zmisc 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). 2: auto with zarith. rewrite F1. rewrite m_spec.(power_mod_spec) with (t := a). 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;[idtac | auto with zarith]. rewrite <- Zpower_mult;[idtac|auto with zarith|auto with zarith]. rewrite mkProd_pred_mkProd. rewrite U1; rewrite Zmult_comm. rewrite Zpower_mult; [idtac|auto with zarith|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). 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). 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] 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). 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 => Z.divide (a ^ ((N - 1) / p) - 1) k)) with (b := (p, p1)); auto with zarith end. intros; discriminate. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) Pmod Mod_op W Lucas PocklingtonCertificat NEll Bits