(* File: Fermat_Test.thy Authors: Daniel Stüwe, Manuel Eberl The probabilistic prime test known as Fermat's test *) section ‹Fermat's Test› theory Fermat_Test imports Fermat_Witness Generalized_Primality_Test begin definition "fermat_test = primality_test (λn a. fermat_liar a n)" text ‹ The Fermat test is a good probabilistic primality test on non-Carmichael numbers. › locale fermat_test_not_Carmichael_number = fixes n :: nat assumes not_Carmichael_number: "¬Carmichael_number n ∨ n < 3" begin sublocale fermat_test: good_prob_primality_test "λa n. fermat_liar n a" n "1 / 2" rewrites "primality_test (λ a n. fermat_liar n a) = fermat_test" proof - show "good_prob_primality_test (λa n. fermat_liar n a) n (1 / 2)" using not_Carmichael_number not_Carmichael_number_imp_card_fermat_witness_bound(3)[of n] prime_imp_fermat_liar[of n] by unfold_locales auto qed (auto simp: fermat_test_def) end lemma not_coprime_imp_fermat_witness: fixes n :: nat assumes "n > 1" "¬coprime a n" shows "fermat_witness a n" using assms lucas_coprime_lemma[of "n - 1" a n] by (auto simp: fermat_witness_def) theorem fermat_test_prime: assumes "prime n" shows "fermat_test n = return_pmf True" proof - interpret fermat_test_not_Carmichael_number n using assms Carmichael_number_not_prime by unfold_locales auto from assms show ?thesis by (rule fermat_test.prime) qed theorem fermat_test_composite: assumes "¬prime n" "¬Carmichael_number n ∨ n < 3" shows "pmf (fermat_test n) True < 1 / 2" proof - interpret fermat_test_not_Carmichael_number n by unfold_locales fact+ from assms(1) show ?thesis by (rule fermat_test.composite) qed text ‹ For a Carmichael number $n$, Fermat's test as defined above mistakenly returns `True' with probability $(\varphi(n)-1) / (n - 2)$. This probability is close to 1 if ‹n› has few and big prime factors; it is not quite as bad if it has many and/or small factors, but in that case, simple trial division can also detect compositeness. Moreover, Fermat's test only succeeds for a Carmichael number if it happens to guess a number that is not coprime to ‹n›. In that case, the fact that we have found a number between 2 and ‹n› that is not coprime to ‹n› alone is proof that ‹n› is composite, and indeed we can even find a non-trivial factor by computing the GCD. This means that for Carmichael numbers, Fermat's test is essentially no better than the very crude method of attempting to guess numbers coprime to ‹n›. This means that, in general, Fermat's test is not very helpful for Carmichael numbers. › theorem fermat_test_Carmichael_number: assumes "Carmichael_number n" shows "fermat_test n = bernoulli_pmf (real (totient n - 1) / real (n - 2))" proof (rule eq_bernoulli_pmfI) from assms have n: "n > 3" "odd n" using Carmichael_number_odd Carmichael_number_gt_3 by auto from n have "fermat_test n = pmf_of_set {2..<n} ⤜ (λa. return_pmf (fermat_liar a n))" by (simp add: fermat_test_def primality_test_def) also have "… = pmf_of_set {2..<n} ⤜ (λa. return_pmf (coprime a n))" using n assms lucas_coprime_lemma[of "n - 1" _ n] by (intro bind_pmf_cong refl) (auto simp: Carmichael_number_def fermat_liar_def) also have "pmf … True = (∑a=2..<n. indicat_real {True} (coprime a n)) / real (n - 2)" using n by (auto simp: pmf_bind_pmf_of_set) also have "(∑a=2..<n. indicat_real {True} (coprime a n)) = (∑a | a ∈ {2..<n} ∧ coprime a n. 1)" by (intro sum.mono_neutral_cong_right) auto also have "… = card {a∈{2..<n}. coprime a n}" by simp also have "{a∈{2..<n}. coprime a n} = totatives n - {1}" using n by (auto simp: totatives_def order.strict_iff_order[of _ n]) also have "card … = totient n - 1" using n by (subst card_Diff_subset) (auto simp: totient_def) finally show "pmf (fermat_test n) True = real (totient n - 1) / real (n - 2)" using n by simp qed end