Theory Rabin_Irreducibility_Test_Code

section ‹Executable Code for Rabin's Irreducibility Test›

theory Rabin_Irreducibility_Test_Code
  imports
    Finite_Fields_Poly_Ring_Code
    Finite_Fields_Mod_Ring_Code
    Rabin_Irreducibility_Test
begin

fun pcoprime⇩C :: "('a, 'b) idx_ring_scheme ⇒ 'a list ⇒ 'a list ⇒ bool"
  where "pcoprime⇩C R f g = (length (snd (ext_euclidean R f g)) = 1)"

declare pcoprime⇩C.simps[simp del]

lemma pcoprime_c:
  assumes "field⇩C R"
  assumes "f ∈ carrier (poly_ring (ring_of R))"
  assumes "g ∈ carrier (poly_ring (ring_of R))"
  shows "pcoprime⇩C R f g ⟷ pcoprime⇘ring_of R⇙ f g"  (is "?L = ?R")
proof (cases "f = [] ∧ g = []")
  case True
  interpret field "ring_of R"
    using assms(1) unfolding field⇩C_def by simp
  interpret d_poly_ring: domain "poly_ring (ring_of R)"
    by (rule univ_poly_is_domain[OF carrier_is_subring])

  have "?L = False" using True by (simp add: pcoprime⇩C.simps ext_euclidean.simps poly_def)
  also have "... ⟷  (length 𝟬⇘poly_ring (ring_of R)⇙ = 1)" by (simp add:univ_poly_zero)
  also have "... ⟷ pcoprime⇘ring_of R⇙ 𝟬⇘poly_ring (ring_of R)⇙  []"
    by (subst pcoprime_zero_iff) (simp_all)
  also have "... ⟷ ?R" using True by (simp add: univ_poly_zero)
  finally show ?thesis by simp
next
  case False

  let ?P = "poly_ring (ring_of R)"
  interpret field "ring_of R"
    using assms(1) unfolding field⇩C_def by simp
  interpret d_poly_ring: domain "poly_ring (ring_of R)"
    by (rule univ_poly_is_domain[OF carrier_is_subring])

  obtain s u v where suv_def: "((u,v),s) = ext_euclidean R f g" by (metis surj_pair)

  have s_eq:"s = f ⊗⇘?P⇙ u ⊕⇘?P⇙ g ⊗⇘?P⇙ v" (is "?T1")
    and s_div_f: "s pdivides⇘ring_of R⇙ f" and s_div_g: "s pdivides⇘ring_of R⇙ g" (is "?T3")
    and suv_carr: "{s, u, v} ⊆ carrier ?P"
    and s_nz: "s ≠ []"
    using False suv_def[symmetric] ext_euclidean[OF assms(1,2,3)] by auto

  have "?L ⟷ length s = 1" using suv_def[symmetric] by (simp add:pcoprime⇩C.simps)
  also have "... ⟷ ?R"
    unfolding pcoprime_def
  proof (intro iffI impI ballI)
    fix r assume len_s: "length s = 1"
    assume r_carr:"r ∈ carrier ?P"
      and "r pdivides⇘ring_of R⇙ f ∧ r pdivides⇘ring_of R⇙ g"
    hence r_div: "pmod f r = 𝟬⇘?P⇙"  "pmod g r = 𝟬⇘?P⇙" unfolding univ_poly_zero
      using assms(2,3) pmod_zero_iff_pdivides[OF carrier_is_subfield] by auto

    have "pmod s r = pmod (f ⊗⇘?P⇙ u) r ⊕⇘?P⇙ pmod (g ⊗⇘?P⇙ v) r"
      using r_carr suv_carr assms unfolding s_eq
      by (intro long_division_add[OF carrier_is_subfield]) auto
    also have "... = pmod (pmod f r ⊗⇘?P⇙ u) r  ⊕⇘?P⇙ pmod (pmod g r ⊗⇘?P⇙ v) r"
      using r_carr suv_carr assms by (intro arg_cong2[where f="(⊕⇘?P⇙)"] pmod_mult_left) auto
    also have "... = pmod 𝟬⇘?P⇙ r  ⊕⇘?P⇙ pmod 𝟬⇘?P⇙ r"
      using suv_carr unfolding r_div by simp
    also have "... = []" using r_carr unfolding univ_poly_zero
      by (simp add: long_division_zero[OF carrier_is_subfield] univ_poly_add)
    finally have "pmod s r =  []" by simp
    hence "r pdivides⇘ring_of R⇙ s"
      using r_carr suv_carr pmod_zero_iff_pdivides[OF carrier_is_subfield] by auto
    hence "degree r ≤ degree s"
      using s_nz r_carr suv_carr by (intro pdivides_imp_degree_le[OF carrier_is_subring]) auto
    thus "degree r = 0" using len_s by simp
  next
    assume "∀r∈carrier ?P. r pdivides⇘ring_of R⇙ f ∧ r pdivides⇘ring_of R⇙ g ⟶ degree r = 0"
    hence "degree s = 0" using s_div_f s_div_g suv_carr by simp
    thus "length s =1" using s_nz
      by (metis diff_is_0_eq diffs0_imp_equal length_0_conv less_one linorder_le_less_linear)
  qed
  finally show ?thesis by simp
qed

text ‹The following is a fast version of @{term "pmod"} for polynomials (to a high power) that
need to be reduced, this is used for the higher order term of the Gauss polynomial.›

fun pmod_pow⇩C :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ nat ⇒ 'a list ⇒ 'a list"
  where "pmod_pow⇩C F f n g = (
    let r = (if n ≥ 2 then pmod_pow⇩C F f (n div 2) g ^⇩C⇘poly F⇙ 2 else 1⇩C⇘poly F⇙)
    in pmod⇩C F (r *⇩C⇘poly F⇙ (f ^⇩C⇘poly F⇙ (n mod 2))) g)"

declare pmod_pow⇩C.simps[simp del]

lemma pmod_pow_c:
  assumes "field⇩C R"
  assumes "f ∈ carrier (poly_ring (ring_of R))"
  assumes "g ∈ carrier (poly_ring (ring_of R))"
  shows "pmod_pow⇩C R f n g = ring.pmod (ring_of R) (f [^]⇘poly_ring (ring_of R)⇙ n) g"
proof (induction n rule:nat_less_induct)
  case (1 n)

  let ?P = "poly_ring (ring_of R)"
  interpret field "ring_of R"
    using assms(1) unfolding field⇩C_def by simp
  interpret d_poly_ring: domain "poly_ring (ring_of R)"
    by (rule univ_poly_is_domain[OF carrier_is_subring])

  have ring_c: "ring⇩C R" using assms(1) unfolding field⇩C_def domain⇩C_def cring⇩C_def by auto
  have d_poly: "domain⇩C (poly R)" using assms (1) unfolding field⇩C_def by (intro poly_domain) auto

  have ind: "pmod_pow⇩C R f m g = pmod (f [^]⇘?P⇙ m) g" if "m < n" for m
    using 1 that by auto

  define r where "r = (if n ≥ 2 then pmod_pow⇩C R f (n div 2) g ^⇩C⇘poly R⇙ 2 else 1⇩C⇘poly R⇙)"

  have "pmod r g = pmod (f [^]⇘?P⇙ (n - (n mod 2))) g ∧ r ∈ carrier ?P"
  proof (cases "n ≥ 2")
    case True
    hence "r = pmod_pow⇩C R f (n div 2) g [^]⇘?P⇙ (2 :: nat)"
      unfolding r_def domain_cD[OF d_poly] by (simp add:ring_of_poly[OF ring_c])
    also have "... = pmod (f [^]⇘?P⇙ (n div 2)) g [^]⇘?P⇙ (2 :: nat)"
      using True by (intro arg_cong2[where f="([^]⇘?P⇙)"] refl ind) auto
    finally have r_alt: "r = pmod (f [^]⇘?P⇙ (n div 2)) g [^]⇘?P⇙ (2 :: nat)"
      by simp

    have "pmod r g = pmod (pmod (f [^]⇘?P⇙ (n div 2)) g ⊗⇘?P⇙ pmod (f [^]⇘?P⇙ (n div 2)) g) g"
      unfolding r_alt using assms(2,3) long_division_closed[OF carrier_is_subfield]
      by (simp add:numeral_eq_Suc) algebra
    also have "... = pmod (f [^]⇘?P⇙ (n div 2) ⊗⇘?P⇙ f [^]⇘?P⇙ (n div 2)) g"
      using assms(2,3) by (intro pmod_mult_both[symmetric]) auto
    also have "... = pmod (f [^]⇘?P⇙ ((n div 2)+(n div 2))) g"
      using assms(2,3) by (subst d_poly_ring.nat_pow_mult) auto
    also have "... = pmod (f [^]⇘?P⇙ (n - (n mod 2))) g"
      by (intro arg_cong2[where f="pmod"] refl arg_cong2[where f="([^]⇘?P⇙)"]) presburger
    finally have "pmod r g = pmod (f [^]⇘?P⇙ (n - (n mod 2))) g"
      by simp
    moreover have "r ∈ carrier ?P"
      using assms(2,3) long_division_closed[OF carrier_is_subfield] unfolding r_alt by auto
    ultimately show ?thesis by auto
  next
    case False
    hence "r = 𝟭⇘?P⇙"
      unfolding r_def using domain_cD[OF d_poly] ring_of_poly[OF ring_c] by simp
    also have "... = f [^]⇘?P⇙ (0 :: nat)" by simp
    also have "... = f [^]⇘?P⇙ (n - (n mod 2))"
      using False by (intro arg_cong2[where f="([^]⇘?P⇙)"] refl) auto
    finally have "r = f [^]⇘?P⇙ (n - (n mod 2))" by simp
    then show ?thesis using assms(2) by simp
  qed

  hence r_exp: "pmod r g = pmod (f [^]⇘?P⇙ (n - (n mod 2))) g" and r_carr: "r ∈ carrier ?P"
    by auto

  have "pmod_pow⇩C R f n g = pmod⇩C R (r *⇩C⇘poly R⇙ (f ^⇩C⇘poly R⇙ (n mod 2))) g"
    by (subst pmod_pow⇩C.simps) (simp add:r_def[symmetric])
  also have "... = pmod⇩C R (r ⊗⇘?P⇙ (f [^]⇘?P⇙ (n mod 2))) g"
    unfolding domain_cD[OF d_poly] by (simp add:ring_of_poly[OF ring_c])
  also have "... = pmod (r ⊗⇘?P⇙ (f [^]⇘?P⇙ (n mod 2))) g"
    using r_carr assms(2,3) by (intro pmod_c[OF assms(1)]) auto
  also have "... = pmod (pmod r g ⊗⇘?P⇙ (f [^]⇘?P⇙ (n mod 2))) g"
    using r_carr assms(2,3) by (intro pmod_mult_left) auto
  also have "... = pmod (f [^]⇘?P⇙ (n - (n mod 2)) ⊗⇘?P⇙ (f [^]⇘?P⇙ (n mod 2))) g"
    using assms(2,3) unfolding r_exp by (intro pmod_mult_left[symmetric]) auto
  also have "... = pmod (f [^]⇘?P⇙ ((n - (n mod 2)) + (n mod 2))) g"
    using assms(2,3) by (intro arg_cong2[where f="pmod"] refl d_poly_ring.nat_pow_mult) auto
  also have "... = pmod (f [^]⇘?P⇙ n) g" by simp
  finally show "pmod_pow⇩C R f n g = pmod (f [^]⇘?P⇙ n) g" by simp
qed

text ‹The following function checks whether a given polynomial is coprime with the
Gauss polynomial $X^n - X$.›

definition pcoprime_with_gauss_poly :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ nat ⇒ bool"
  where "pcoprime_with_gauss_poly F p n =
    (pcoprime⇩C F p (pmod_pow⇩C F X⇩C⇘F⇙ n p +⇩C⇘poly F⇙ (-⇩C⇘poly F⇙ pmod⇩C F X⇩C⇘F⇙ p)))"


definition divides_gauss_poly :: "('a,'b) idx_ring_scheme ⇒ 'a list ⇒ nat ⇒ bool"
  where "divides_gauss_poly F p n =
    (pmod_pow⇩C F X⇩C⇘F⇙ n p +⇩C⇘poly F⇙ (-⇩C⇘poly F⇙ pmod⇩C F X⇩C⇘F⇙ p) = [])"

lemma mod_gauss_poly:
  assumes "field⇩C R"
  assumes "f ∈ carrier (poly_ring (ring_of R))"
  shows "pmod_pow⇩C R X⇩C⇘R⇙ n f +⇩C⇘poly R⇙ (-⇩C⇘poly R⇙ pmod⇩C R X⇩C⇘R⇙ f) =
    ring.pmod (ring_of R) (gauss_poly (ring_of R) n) f" (is "?L = ?R")
proof -
  interpret field "ring_of R"
    using assms(1) unfolding field⇩C_def by simp
  interpret d_poly_ring: domain "poly_ring (ring_of R)"
    by (rule univ_poly_is_domain[OF carrier_is_subring])

  have ring_c: "ring⇩C R" using assms(1) unfolding field⇩C_def domain⇩C_def cring⇩C_def by auto
  have d_poly: "domain⇩C (poly R)" using assms (1) unfolding field⇩C_def by (intro poly_domain) auto
  let ?P = "poly_ring (ring_of R)"

  have "?L = pmod_pow⇩C R X⇘ring_of R⇙ n f ⊕⇘?P⇙ -⇩C⇘poly R⇙ pmod⇩C R X⇘ring_of R⇙ f"
    by (simp add: poly_var domain_cD[OF d_poly] ring_of_poly[OF ring_c])
  also have "...= pmod (X⇘ring_of R⇙[^]⇘?P⇙ n) f⊕⇘?P⇙ -⇩C⇘poly R⇙ pmod X⇘ring_of R⇙ f"
    using assms var_carr[OF carrier_is_subring] by (intro refl arg_cong2[where f="(⊕⇘?P⇙)"]
        pmod_pow_c arg_cong[where f="λx. (-⇩C⇘poly R⇙ x)"] pmod_c) auto
  also have "... =pmod (X⇘ring_of R⇙[^]⇘?P⇙ n) f⊖⇘?P⇙ pmod X⇘ring_of R⇙ f"
    unfolding a_minus_def using assms(1,2) var_carr[OF carrier_is_subring]
      ring_of_poly[OF ring_c] long_division_closed[OF carrier_is_subfield]
    by (subst domain_cD[OF d_poly]) auto
  also have "... = pmod (X⇘ring_of R⇙[^]⇘?P⇙ n) f ⊕⇘?P⇙ pmod (⊖⇘?P⇙ X⇘ring_of R⇙) f"
    using assms(2) var_carr[OF carrier_is_subring]
    unfolding a_minus_def by (subst long_division_a_inv[OF carrier_is_subfield]) auto
  also have " ... = pmod (gauss_poly (ring_of R) n) f"
    using assms(2) var_carr[OF carrier_is_subring] var_pow_carr[OF carrier_is_subring]
    unfolding gauss_poly_def a_minus_def by (subst long_division_add[OF carrier_is_subfield]) auto
  finally show ?thesis by simp
qed

lemma pcoprime_with_gauss_poly:
  assumes "field⇩C R"
  assumes "f ∈ carrier (poly_ring (ring_of R))"
  shows "pcoprime_with_gauss_poly R f n ⟷ pcoprime⇘ring_of R⇙ (gauss_poly (ring_of R) n) f"
    (is "?L = ?R")
proof -
  interpret field "ring_of R"
    using assms(1) unfolding field⇩C_def by simp

  have "?L ⟷ pcoprime⇩C R f (pmod (gauss_poly (ring_of R) n) f)"
    unfolding pcoprime_with_gauss_poly_def using assms by (subst mod_gauss_poly) auto
  also have "... = pcoprime⇘ring_of R⇙ f (pmod (gauss_poly (ring_of R) n) f)"
    using assms gauss_poly_carr long_division_closed[OF carrier_is_subfield]
    by (intro pcoprime_c) auto
  also have "... = pcoprime⇘ring_of R⇙ (gauss_poly (ring_of R) n) f"
    by (intro pcoprime_step[symmetric] gauss_poly_carr assms)
  finally show ?thesis by simp
qed

lemma divides_gauss_poly:
  assumes "field⇩C R"
  assumes "f ∈ carrier (poly_ring (ring_of R))"
  shows "divides_gauss_poly R f n ⟷ f pdivides⇘ring_of R⇙ (gauss_poly (ring_of R) n)"
    (is "?L = ?R")
proof -
  interpret field "ring_of R"
    using assms(1) unfolding field⇩C_def by simp
  have "?L ⟷ (pmod (gauss_poly (ring_of R) n) f = [])"
    unfolding divides_gauss_poly_def using assms by (subst mod_gauss_poly) auto
  also have "... ⟷ ?R"
    using assms gauss_poly_carr by (intro pmod_zero_iff_pdivides[OF carrier_is_subfield]) auto
  finally show ?thesis
    by simp
qed


fun rabin_test_powers :: "('a, 'b) idx_ring_enum_scheme ⇒ nat ⇒ nat list"
  where "rabin_test_powers F n =
    map (λp. idx_size F^(n div p)) (filter (λp. prime p ∧ p dvd n) [2..<(n+1)] )"

text ‹Given a monic polynomial with coefficients over a finite field returns true, if it is
irreducible›

fun rabin_test :: "('a, 'b) idx_ring_enum_scheme ⇒ 'a list ⇒ bool"
  where "rabin_test F f = (
    if degree f = 0 then
      False
    else (if ¬divides_gauss_poly F f (idx_size F^degree f) then
      False
    else (list_all (pcoprime_with_gauss_poly F f) (rabin_test_powers F (degree f)))))"

declare rabin_test.simps[simp del]

context
  fixes R
  assumes field_R: "field⇩C R"
  assumes enum_R: "enum⇩C R"
begin

interpretation finite_field "(ring_of R)"
  using field_R enum_cD[OF enum_R] unfolding field⇩C_def
  by (simp add:finite_field_def finite_field_axioms_def)

lemma rabin_test_powers:
  assumes "n > 0"
  shows "set (rabin_test_powers R n) =
    {order (ring_of R)^ (n div p) | p . Factorial_Ring.prime p ∧ p dvd n}"
    (is "?L = ?R")
proof -
  let ?f = "(λx. order (ring_of R) ^ (n div x))"

  have 0:"p ∈ {2..n}" if "Factorial_Ring.prime p" "p dvd n"  for p
    using assms that by (simp add: dvd_imp_le prime_ge_2_nat)

  have "?L = ?f ` {p ∈ {2..n}.  Factorial_Ring.prime p ∧ p dvd n}"
    using enum_cD[OF enum_R] by auto
  also have "... = ?f ` {p.  Factorial_Ring.prime p ∧ p dvd n}"
    using 0 by (intro image_cong Collect_cong) auto
  also have "... = ?R"
    by auto
  finally show ?thesis by simp
qed

lemma rabin_test:
  assumes "monic_poly (ring_of R) f"
  shows "rabin_test R f ⟷ monic_irreducible_poly (ring_of R) f" (is "?L = ?R")
proof (cases "degree f = 0")
  case True
  thus ?thesis unfolding rabin_test.simps using monic_poly_min_degree by fastforce
next
  case False
  define N where "N = {degree f div p | p . Factorial_Ring.prime p ∧ p dvd degree f}"

  have f_carr: "f ∈ carrier (poly_ring (ring_of R))"
    using assms(1) unfolding monic_poly_def by auto

  have deg_f_gt_0: "degree f > 0"
    using False by auto
  have rt_powers: "set (rabin_test_powers R (degree f)) = (λx. order (ring_of R)^x) ` N"
    unfolding rabin_test_powers[OF deg_f_gt_0] N_def by auto

  have "?L ⟷ divides_gauss_poly R f (idx_size R ^ degree f) ∧
    (∀n ∈ set (rabin_test_powers R (degree f)). (pcoprime_with_gauss_poly R f n))"
    using False by (simp add: list_all_def rabin_test.simps del:rabin_test_powers.simps)
  also have "... ⟷ f pdivides⇘ring_of R⇙ (gauss_poly (ring_of R) (order (ring_of R) ^ degree f))
    ∧ (∀n ∈ N. pcoprime⇘ring_of R⇙ (gauss_poly (ring_of R) (order (ring_of R) ^n)) f)"
    unfolding divides_gauss_poly[OF field_R f_carr] pcoprime_with_gauss_poly[OF field_R f_carr]
      rt_powers enum_cD[OF enum_R] by simp
  also have "... ⟷ ?R"
    using False unfolding N_def by (intro rabin_irreducibility_condition[symmetric] assms(1)) auto
  finally show ?thesis by simp
qed

end

end