Theory Finite_Fields.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 pcoprimeC :: "('a, 'b) idx_ring_scheme  'a list  'a list  bool"
  where "pcoprimeC R f g = (length (snd (ext_euclidean R f g)) = 1)"

declare pcoprimeC.simps[simp del]

lemma pcoprime_c:
  assumes "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  assumes "g  carrier (poly_ring (ring_of R))"
  shows "pcoprimeC R f g  pcoprimering_of Rf g"  (is "?L = ?R")
proof (cases "f = []  g = []")
  case True
  interpret field "ring_of R"
    using assms(1) unfolding fieldC_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: pcoprimeC.simps ext_euclidean.simps poly_def)
  also have "...   (length 𝟬poly_ring (ring_of R)= 1)" by (simp add:univ_poly_zero)
  also have "...  pcoprimering_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 fieldC_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 ?Pu ?Pg ?Pv" (is "?T1")
    and s_div_f: "s pdividesring_of Rf" and s_div_g: "s pdividesring_of Rg" (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:pcoprimeC.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 pdividesring_of Rf  r pdividesring_of Rg"
    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 ?Pu) r ?Ppmod (g ?Pv) 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 ?Pu) r  ?Ppmod (pmod g r ?Pv) r"
      using r_carr suv_carr assms by (intro arg_cong2[where f="(⊕?P)"] pmod_mult_left) auto
    also have "... = pmod 𝟬?Pr  ?Ppmod 𝟬?Pr"
      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 pdividesring_of Rs"
      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 "rcarrier ?P. r pdividesring_of Rf  r pdividesring_of Rg  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_powC :: "('a,'b) idx_ring_scheme  'a list  nat  'a list  'a list"
  where "pmod_powC F f n g = (
    let r = (if n  2 then pmod_powC F f (n div 2) g ^Cpoly F2 else 1Cpoly F)
    in pmodC F (r *Cpoly F(f ^Cpoly F(n mod 2))) g)"

declare pmod_powC.simps[simp del]

lemma pmod_pow_c:
  assumes "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  assumes "g  carrier (poly_ring (ring_of R))"
  shows "pmod_powC 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 fieldC_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: "ringC R" using assms(1) unfolding fieldC_def domainC_def cringC_def by auto
  have d_poly: "domainC (poly R)" using assms (1) unfolding fieldC_def by (intro poly_domain) auto

  have ind: "pmod_powC R f m g = pmod (f [^]?Pm) g" if "m < n" for m
    using 1 that by auto

  define r where "r = (if n  2 then pmod_powC R f (n div 2) g ^Cpoly R2 else 1Cpoly 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_powC 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 ?Ppmod (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) ?Pf [^]?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_powC R f n g = pmodC R (r *Cpoly R(f ^Cpoly R(n mod 2))) g"
    by (subst pmod_powC.simps) (simp add:r_def[symmetric])
  also have "... = pmodC 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 [^]?Pn) g" by simp
  finally show "pmod_powC R f n g = pmod (f [^]?Pn) 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 =
    (pcoprimeC F p (pmod_powC F XCFn p +Cpoly F(-Cpoly FpmodC F XCFp)))"


definition divides_gauss_poly :: "('a,'b) idx_ring_scheme  'a list  nat  bool"
  where "divides_gauss_poly F p n =
    (pmod_powC F XCFn p +Cpoly F(-Cpoly FpmodC F XCFp) = [])"

lemma mod_gauss_poly:
  assumes "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  shows "pmod_powC R XCRn f +Cpoly R(-Cpoly RpmodC R XCRf) =
    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 fieldC_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: "ringC R" using assms(1) unfolding fieldC_def domainC_def cringC_def by auto
  have d_poly: "domainC (poly R)" using assms (1) unfolding fieldC_def by (intro poly_domain) auto
  let ?P = "poly_ring (ring_of R)"

  have "?L = pmod_powC R Xring_of Rn f ?P-Cpoly RpmodC R Xring_of Rf"
    by (simp add: poly_var domain_cD[OF d_poly] ring_of_poly[OF ring_c])
  also have "...= pmod (Xring_of R[^]?Pn) f?P-Cpoly Rpmod Xring_of Rf"
    using assms var_carr[OF carrier_is_subring] by (intro refl arg_cong2[where f="(⊕?P)"]
        pmod_pow_c arg_cong[where f="λx. (-Cpoly Rx)"] pmod_c) auto
  also have "... =pmod (Xring_of R[^]?Pn) f?Ppmod Xring_of Rf"
    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 (Xring_of R[^]?Pn) f ?Ppmod (?PXring_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 "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  shows "pcoprime_with_gauss_poly R f n  pcoprimering_of R(gauss_poly (ring_of R) n) f"
    (is "?L = ?R")
proof -
  interpret field "ring_of R"
    using assms(1) unfolding fieldC_def by simp

  have "?L  pcoprimeC 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 "... = pcoprimering_of Rf (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 "... = pcoprimering_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 "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  shows "divides_gauss_poly R f n  f pdividesring_of R(gauss_poly (ring_of R) n)"
    (is "?L = ?R")
proof -
  interpret field "ring_of R"
    using assms(1) unfolding fieldC_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: "fieldC R"
  assumes enum_R: "enumC R"
begin

interpretation finite_field "(ring_of R)"
  using field_R enum_cD[OF enum_R] unfolding fieldC_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 pdividesring_of R(gauss_poly (ring_of R) (order (ring_of R) ^ degree f))
     (n  N. pcoprimering_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