Theory Solovay_Strassen_Test

(*
  File:     Solovay_Strassen.thy
  Authors:  Daniel Stüwe, Manuel Eberl

  The Solovay--Strassen primality test.
*)
section ‹The Solovay--Strassen Test›
theory Solovay_Strassen_Test
imports 
  Generalized_Primality_Test
  Euler_Witness
begin

definition solovay_strassen_witness :: "nat ⇒ nat ⇒ bool" where
  "solovay_strassen_witness n a =
     (let x = Jacobi (int a) (int n) in x ≠ 0 ∧ [x = int a ^ ((n - 1) div 2)] (mod n))"

definition solovay_strassen :: "nat ⇒ bool pmf" where
  "solovay_strassen = primality_test solovay_strassen_witness"

lemma prime_imp_solovay_strassen_witness:
  assumes "prime p" "odd p" "a ∈ {2..<p}"
  shows   "solovay_strassen_witness p a"
proof -
  have eq: "Jacobi a p = Legendre a p"
    using prime_p_Jacobi_eq_Legendre assms by simp
  from ‹prime p› have "coprime p a"
    by (rule prime_imp_coprime) (use assms in auto)

  show ?thesis unfolding solovay_strassen_witness_def Let_def eq
  proof
    from ‹coprime p a› and ‹prime p› show "Legendre (int a) (int p) ≠ 0"
      by (auto simp: coprime_commute)
  next
    show "[Legendre (int a) (int p) = int a ^ ((p - 1) div 2)] (mod int p)"
      using assms by (intro euler_criterion) auto
  qed
qed
    
lemma card_solovay_strassen_liars_composite:
  fixes n :: nat
  assumes "¬prime n" "n > 2" "odd n"
  shows   "card {a ∈ {2..<n}. solovay_strassen_witness n a} < (n - 2) div 2"
    (is "card ?A < _")
proof -
  interpret euler_witness_context n
    using assms unfolding euler_witness_context_def by simp
  have "card H < (n - 1) div 2"
    by (intro card_euler_liars_cosets_limit(2) assms)
  also from assms have "H = insert 1 ?A"
    by (auto simp: solovay_strassen_witness_def Let_def
                   euler_witness_def H_def Jacobi_eq_0_iff_not_coprime)
  also have "card … = card ?A + 1"
    by (subst card.insert) auto
  finally show "card ?A < (n - 2) div 2"
    by linarith
qed

interpretation solovay_strassen: good_prob_primality_test solovay_strassen_witness n "1 / 2"
  rewrites "primality_test solovay_strassen_witness = solovay_strassen"
proof -
  show "good_prob_primality_test solovay_strassen_witness n (1 / 2)"
  proof
    fix n :: nat assume "¬prime n" "n > 2" "odd n"
    thus "real (card {a. 2 ≤ a ∧ a < n ∧ solovay_strassen_witness n a}) < (1 / 2) * real (n - 2)"
      using card_solovay_strassen_liars_composite[of n] by auto
  qed (use prime_imp_solovay_strassen_witness in auto)
qed (simp_all add: solovay_strassen_def)

end