proposition: Theorem prime_test_correct : forall n:nat, prime_test n = true -> ~(exists k:nat, k <> 1 /\ k <> n /\ (exists q:nat, n = q*k))%nat.
proof: Proof. intros n; case_eq n. - simpl; intros Heq Hd; discriminate. - intros n0; case_eq n0. + simpl; intros Heq1 Heq2 Hd; discriminate. + unfold prime_test; intros n1 Heqn0 Heqn. assert (H1ltn : (1 < n)%nat). * rewrite Heqn; auto with arith. * rewrite <- Heqn. lazy beta zeta delta [prime_test]. case_eq (Z.sqrt (Z_of_nat n)). intros Hsqrt_eq. elim (Zlt_asym 1 (Z_of_nat n)). lia. lapply (Z.sqrt_spec (Z_of_nat n)). rewrite Hsqrt_eq; simpl. lia. lia. intros p Hsqrt_eq Htest_eq (k, (Hn1, (Hnn, (q,Heq)))). assert (H0ltn:(0 < n)%nat) by lia. assert (Hkltn:(k < n)%nat). assert (Heq' : n=(k*q)%nat). rewrite Heq; ring. generalize (divisor_smaller n q H0ltn k Heq'). lia. assert (Hex: exists k':nat, (1 < (Z_of_nat k') <= (Z.sqrt (Z_of_nat n))) /\ (exists q':nat, n=(k'*q')%nat)). elim (div_Zsqrt (Z_of_nat k) (Z_of_nat n) (Z_of_nat q)). intros Hint1; exists k;split. lia. exists q; rewrite Heq; ring. intros Hint2; exists q; split. split. elim (Zle_or_lt (Z_of_nat q) 1); auto. intros hqle1; assert (Hq1: q = 1%nat). lia. rewrite Hq1 in Heq; simpl in Heq; elim Hnn; rewrite Heq; ring. tauto. exists k; auto. split. case_eq k. intros Hk0; rewrite Hk0 in Heq; rewrite Heq in H1ltn; rewrite Nat.mul_0_r in H1ltn; lia. intros; unfold Z.lt; simpl; auto. lia. rewrite Zmult_comm; rewrite <- inj_mult; rewrite Heq;auto. elim Hex; intros k' ((H1ltk', Hk'ltsqrt), Hex'); clear Hex. case_eq p. intros p' Hp; rewrite Hp in Htest_eq. elim (test_odds_correct (Z.abs_nat (Zpos p')) n (Zpos p)) with k'. rewrite Z_to_nat_and_back. rewrite Hp. auto with zarith. auto with zarith. auto. repeat rewrite Zminus_0_r in Htest_eq. rewrite Hp; auto. split. lia. apply Z_of_nat_le. rewrite inj_plus. rewrite inj_mult. rewrite Z_to_nat_and_back. simpl (Z_of_nat 2). simpl (Z_of_nat 1). rewrite <- Zpos_xI. rewrite <- Hp. rewrite <- Hsqrt_eq; auto. auto with zarith. auto. intros p' Hp; rewrite Hp in Htest_eq. elim (test_odds_correct (Z.abs_nat (Zpos p')) n (Zpos p + 1)) with k'. rewrite Z_to_nat_and_back. rewrite Hp; rewrite Zpos_xO; ring. generalize (lt_Zpos p'); intros; lia. auto. rewrite <- Hp in Htest_eq; auto. split; [lia|]. apply Z_of_nat_le. rewrite inj_plus. rewrite inj_mult. rewrite Z_to_nat_and_back. simpl (Z_of_nat 2); simpl (Z_of_nat 1). rewrite <- Zpos_xO. rewrite <- Hp; lia. auto with zarith. auto. intros Hp; rewrite Hp in Hsqrt_eq. rewrite Hsqrt_eq in Hk'ltsqrt. lia. intros p Hsqrt_eq. elim (Zle_not_lt 0 (Z.sqrt (Z_of_nat n))). apply Z.sqrt_nonneg. rewrite Hsqrt_eq. apply Zneg_lt. Qed.
imports: ZArith Arith Bool Lia