proposition: 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: Proof. unfold test_pock;intros. elimif. generalize (div_eucl_spec (Pos.pred N) (mkProd dec)); destruct ((Pos.pred 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 lia. 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 by mauto. rewrite <- Zpower_mult; mauto. } clear H12. intros H14. match type of H14 with _ -> _ -> _ -> ?X => assert (H12:X); try apply H14; clear H14 end. 1, 3: mauto. rewrite Zmod_small; mauto. assert (1 < mkProd dec). { assert (H14 := Zlt_0_pos (mkProd dec)). assert (1 <= mkProd dec) by 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). revert H8; mauto. apply Z_mod_lt; mauto. rewrite <- Z_div_mod_eq_full; 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). 1-2, 7-8: 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. 1-2: 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) 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; autorewrite with zmisc; intro H2. rewrite <- H2. match goal with |- context [fold_left ?f _ _] => apply (ListAux.fold_left_invol_in _ _ f (fun k => Z.divide (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.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod