diff --git a/metadata/entries/Finite_Fields.toml b/metadata/entries/Finite_Fields.toml --- a/metadata/entries/Finite_Fields.toml +++ b/metadata/entries/Finite_Fields.toml @@ -1,37 +1,39 @@ title = "Finite Fields" date = 2022-06-08 topics = [ "Mathematics/Algebra", ] abstract = """ This entry formalizes the classification of the finite fields (also called Galois fields): For each prime power $p^n$ there exists exactly one (up to isomorphisms) finite field of that size and there are no other finite fields. The derivation includes a formalization of the -characteristic of rings, the Frobenius endomorphism, formal -differentiation for polynomials in HOL-Algebra and Gauss' formula -for the number of monic irreducible polynomials over finite fields: \\[ +characteristic of rings, the Frobenius endomorphism, formal differentiation +for polynomials in HOL-Algebra, Rabin's test for the irreducibility of +polynomials and Gauss' formula for the number of monic irreducible +polynomials over finite fields: \\[ \\frac{1}{n} \\sum_{d | n} \\mu(d) p^{n/d} \\textrm{.} \\] The proofs are -based on the books from Ireland -and Rosen, as well as, Lidl and +and Rosen, Rabin, as +well as, Lidl and Niederreiter.""" license = "bsd" note = "" [authors] [authors.karayel] homepage = "karayel_homepage" [contributors] [notify] karayel = "karayel_email" [history] +2023-01-17 = "Added Rabin's test for the irreducibility of polynomials in finite fields." [extra] [related] diff --git a/thys/Finite_Fields/ROOT b/thys/Finite_Fields/ROOT --- a/thys/Finite_Fields/ROOT +++ b/thys/Finite_Fields/ROOT @@ -1,18 +1,19 @@ chapter AFP session Finite_Fields = "HOL-Algebra" + options [timeout = 600] sessions Dirichlet_Series theories Card_Irreducible_Polynomials Card_Irreducible_Polynomials_Aux Finite_Fields_Factorization_Ext Finite_Fields_Isomorphic Finite_Fields_Preliminary_Results Formal_Polynomial_Derivatives Monic_Polynomial_Factorization Ring_Characteristic + Rabin_Irreducibility_Test document_files "root.tex" "root.bib" diff --git a/thys/Finite_Fields/Rabin_Irreducibility_Test.thy b/thys/Finite_Fields/Rabin_Irreducibility_Test.thy new file mode 100644 --- /dev/null +++ b/thys/Finite_Fields/Rabin_Irreducibility_Test.thy @@ -0,0 +1,371 @@ +section \Rabin's test for irreducible polynomials\ + +theory Rabin_Irreducibility_Test + imports Card_Irreducible_Polynomials_Aux +begin + +text \This section introduces an effective test for irreducibility of polynomials +(in finite fields) based on Rabin~\cite[rabin1980].\ + +lemma (in domain) coeff_a_inv: + assumes "subring K R" + assumes "f \ carrier (K[X])" + shows "coeff (\\<^bsub>K[X]\<^esub> f) i = \ (coeff f i)" (is "?L = ?R") +proof - + have "?L = coeff (map (a_inv R) f) i" + unfolding univ_poly_a_inv_def'[OF assms(1,2)] by simp + also have "... = ?R" by (induction f) auto + finally show ?thesis by simp +qed + +lemma (in comm_monoid) irreducible_prod_unit: + assumes "f \ carrier G" "x \ Units G" + shows "irreducible G f = irreducible G (x \ f)" (is "?L = ?R") +proof + assume "?L" + thus ?R using irreducible_prod_lI assms by auto +next + have "inv x \ (x \ f) = (inv x \ x) \ f" + using assms by (intro m_assoc[symmetric]) auto + also have "... = f" using assms by simp + finally have 0: "inv x \ (x \ f) = f" by simp + assume ?R + hence "irreducible G (inv x \ (x \ f) )" using irreducible_prod_lI assms by blast + thus ?L using 0 by simp +qed + +definition pcoprime :: "_ \ 'a list \ 'a list \ bool" ("pcoprime\") + where "pcoprime\<^bsub>R\<^esub> p q = + (\r \ carrier (poly_ring R). r pdivides\<^bsub>R\<^esub> p \ r pdivides\<^bsub>R\<^esub> q \ degree r = 0)" + +lemma pcoprimeI: + assumes "\r. r \ carrier (poly_ring R) \ r pdivides \<^bsub>R\<^esub> p \ r pdivides\<^bsub>R\<^esub> q \ degree r = 0" + shows "pcoprime\<^bsub>R\<^esub> p q" + using assms unfolding pcoprime_def by auto + +context field +begin + +interpretation r:polynomial_ring R "(carrier R)" + unfolding polynomial_ring_def polynomial_ring_axioms_def + using carrier_is_subfield field_axioms by force + +lemma pcoprime_one: "pcoprime\<^bsub>R\<^esub> p \\<^bsub>poly_ring R\<^esub>" +proof (rule pcoprimeI) + fix r + assume r_carr: "r \ carrier (poly_ring R)" + moreover assume "r pdivides \<^bsub>R\<^esub> \\<^bsub>poly_ring R\<^esub>" + moreover have "\\<^bsub>poly_ring R\<^esub> \ []" by (simp add:univ_poly_one) + ultimately have "degree r \ degree \\<^bsub>poly_ring R\<^esub>" + by (intro pdivides_imp_degree_le[OF carrier_is_subring] r_carr) auto + also have "... = 0" by (simp add:univ_poly_one) + finally show "degree r = 0" by auto +qed + +lemma pcoprime_left_factor: + assumes "x \ carrier (poly_ring R)" + assumes "y \ carrier (poly_ring R)" + assumes "z \ carrier (poly_ring R)" + assumes "pcoprime\<^bsub>R\<^esub> (x \\<^bsub>poly_ring R\<^esub> y) z" + shows "pcoprime\<^bsub>R\<^esub> x z" +proof (rule pcoprimeI) + fix r + assume r_carr: "r \ carrier (poly_ring R)" + assume "r pdivides \<^bsub>R\<^esub> x" + hence "r pdivides \<^bsub>R\<^esub> (x \\<^bsub>poly_ring R\<^esub> y)" + using assms(1,2) r_carr r.p.divides_prod_r unfolding pdivides_def by simp + moreover assume "r pdivides \<^bsub>R\<^esub> z" + ultimately show "degree r = 0" using assms(4) r_carr unfolding pcoprime_def by simp +qed + +lemma pcoprime_sym: + shows "pcoprime x y = pcoprime y x" + unfolding pcoprime_def by auto + +lemma pcoprime_left_assoc_cong_aux: + assumes "x1 \ carrier (poly_ring R)" "x2 \ carrier (poly_ring R)" + assumes "x2 \\<^bsub>poly_ring R\<^esub> x1" + assumes "y \ carrier (poly_ring R)" + assumes "pcoprime x1 y" + shows "pcoprime x2 y" + using assms r.p.divides_cong_r[OF _ assms(3)] unfolding pcoprime_def pdivides_def by simp + +lemma pcoprime_left_assoc_cong: + assumes "x1 \ carrier (poly_ring R)" "x2 \ carrier (poly_ring R)" + assumes "x1 \\<^bsub>poly_ring R\<^esub> x2" + assumes "y \ carrier (poly_ring R)" + shows "pcoprime x1 y = pcoprime x2 y" + using assms pcoprime_left_assoc_cong_aux r.p.associated_sym by metis + +lemma pcoprime_right_assoc_cong: + assumes "x1 \ carrier (poly_ring R)" "x2 \ carrier (poly_ring R)" + assumes "x1 \\<^bsub>poly_ring R\<^esub> x2" + assumes "y \ carrier (poly_ring R)" + shows "pcoprime y x1 = pcoprime y x2" + using assms pcoprime_sym pcoprime_left_assoc_cong by metis + +lemma pcoprime_step: + assumes "f \ carrier (poly_ring R)" + assumes "g \ carrier (poly_ring R)" + shows "pcoprime f g \ pcoprime g (f pmod g)" +proof - + have "d pdivides f \ d pdivides (f pmod g)" if "d \ carrier (poly_ring R)" "d pdivides g" for d + proof - + have "d pdivides f \ d pdivides (g \\<^bsub>r.P\<^esub> (f pdiv g) \\<^bsub>r.P\<^esub> (f pmod g))" + using pdiv_pmod[OF carrier_is_subfield assms] by simp + also have "... \ d pdivides ((f pmod g))" + using that assms long_division_closed[OF carrier_is_subfield] r.p.divides_prod_r + unfolding pdivides_def by (intro r.p.div_sum_iff) simp_all + finally show ?thesis by simp + qed + hence "d pdivides f \ d pdivides g \ d pdivides g \ d pdivides (f pmod g)" + if "d \ carrier (poly_ring R)" for d + using that by auto + thus ?thesis + unfolding pcoprime_def by auto +qed + +lemma pcoprime_zero_iff: + assumes "f \ carrier (poly_ring R)" + shows "pcoprime f [] \ length f = 1" +proof - + consider (i) "length f = 0" | (ii) "length f = 1" | (iii) "length f > 1" + by linarith + thus ?thesis + proof (cases) + case i + hence "f = []" by simp + moreover have "X pdivides []" using r.pdivides_zero r.var_closed(1) by blast + moreover have "degree X = 1" using degree_var by simp + ultimately have "\pcoprime f []" using r.var_closed(1) unfolding pcoprime_def by auto + then show ?thesis using i by auto + next + case ii + hence "f \ []" "degree f = 0" by auto + hence "degree d = 0" if "d pdivides f" "d \ carrier (poly_ring R)" for d + using that(1) pdivides_imp_degree_le[OF carrier_is_subring that(2) assms] by simp + hence "pcoprime f []" unfolding pcoprime_def by auto + then show ?thesis using ii by simp + next + case iii + have "f pdivides f" using assms unfolding pdivides_def by simp + moreover have "f pdivides []" using assms r.pdivides_zero by blast + moreover have "degree f > 0" using iii by simp + ultimately have "\pcoprime f []" using assms unfolding pcoprime_def by auto + then show ?thesis using iii by auto + qed +qed + +end + +context finite_field +begin + +interpretation r:polynomial_ring R "(carrier R)" + unfolding polynomial_ring_def polynomial_ring_axioms_def + using carrier_is_subfield field_axioms by force + +lemma exists_irreducible_proper_factor: + assumes "monic_poly R f" "degree f > 0" "\monic_irreducible_poly R f" + shows "\g. monic_irreducible_poly R g \ g pdivides\<^bsub>R\<^esub> f \ degree g < degree f" +proof - + define S where "S = {d. monic_irreducible_poly R d \ 0 < pmult d f}" + + have f_carr: "f \ carrier (poly_ring R)" "f \ \\<^bsub>poly_ring R\<^esub>" + using assms(1) unfolding monic_poly_def univ_poly_zero by auto + + have "S \ {}" + proof (rule ccontr) + assume S_empty: "\(S \ {})" + have "f = (\\<^bsub>poly_ring R\<^esub>d\S. d [^]\<^bsub>poly_ring R\<^esub> pmult d f)" + unfolding S_def by (intro factor_monic_poly assms(1)) + also have "... = \\<^bsub>poly_ring R\<^esub>" using S_empty by simp + finally have "f = \\<^bsub>poly_ring R\<^esub>" by simp + hence "degree f = 0" using degree_one by simp + thus "False" using assms(2) by simp + qed + then obtain g where g_irred: "monic_irreducible_poly R g" and "0 < pmult g f" + unfolding S_def by auto + + hence "1 \ pmult g f" by simp + + hence g_div: "g pdivides f" using multiplicity_ge_1_iff_pdivides f_carr g_irred by blast + + then obtain h where f_def: "f = g \\<^bsub>poly_ring R\<^esub> h" and h_carr:"h \ carrier (poly_ring R)" + unfolding pdivides_def by auto + + have g_nz: "g \ \\<^bsub>poly_ring R\<^esub>" and h_nz: "h \ \\<^bsub>poly_ring R\<^esub>" + and g_carr: "g \ carrier (poly_ring R)" + using f_carr(2) h_carr g_irred unfolding f_def monic_irreducible_poly_def monic_poly_def + by auto + + have "degree f = degree g + degree h" + using g_nz h_nz g_carr h_carr unfolding f_def by (intro degree_mult[OF r.K_subring]) auto + moreover have "degree h > 0" + proof (rule ccontr) + assume "\(degree h > 0)" + hence "degree h = 0" by simp + hence "h \ Units (poly_ring R)" + using h_carr h_nz by (simp add: carrier_is_subfield univ_poly_units' univ_poly_zero) + hence "f \\<^bsub>poly_ring R\<^esub> g" + unfolding f_def using g_carr r.p.associatedI2' by force + hence "f \\<^bsub>mult_of (poly_ring R)\<^esub> g" + using f_carr g_nz g_carr by (simp add: r.p.assoc_iff_assoc_mult) + hence "f = g" + using monic_poly_not_assoc assms(1) g_irred unfolding monic_irreducible_poly_def by simp + hence "monic_irreducible_poly R f" + using g_irred by simp + thus "False" + using assms(3) by auto + qed + ultimately have "degree g < degree f" by simp + thus ?thesis using g_irred g_div by auto +qed + +theorem rabin_irreducibility_condition: + assumes "monic_poly R f" "degree f > 0" + defines "N \ {degree f div p | p . Factorial_Ring.prime p \ p dvd degree f}" + shows "monic_irreducible_poly R f \ + (f pdivides gauss_poly R (order R^degree f) \ (\n \ N. pcoprime (gauss_poly R (order R^n)) f))" + (is "?L \ ?R1 \ ?R2") +proof - + have f_carr: "f \ carrier (poly_ring R)" + using assms(1) unfolding monic_poly_def by blast + + have "?R1" if "?L" + using div_gauss_poly_iff[where n="degree f"] that assms(2) by simp + moreover have "False" if cthat:"\pcoprime (gauss_poly R (order R^n)) f" "?L" "n \ N" for n + proof - + obtain d where d_def: + "d pdivides f" + "d pdivides (gauss_poly R (order R^n))" "degree d > 0" "d \ carrier (poly_ring R)" + using cthat(1) unfolding pcoprime_def by auto + + obtain p where p_def: + "n = degree f div p" "Factorial_Ring.prime p" "p dvd degree f" + using cthat(3) unfolding N_def by auto + + have n_gt_0: "n > 0" + using p_def assms(2) by (metis dvd_div_eq_0_iff gr0I) + + have "d \ Units (poly_ring R)" + using d_def(3,4) univ_poly_units'[OF carrier_is_subfield] by simp + hence "f pdivides d" + using cthat(2) d_def(1,4) unfolding monic_irreducible_poly_def ring_irreducible_def + Divisibility.irreducible_def properfactor_def pdivides_def f_carr by auto + hence "f pdivides (gauss_poly R (order R^n))" + using d_def(2,4) f_carr r.p.divides_trans unfolding pdivides_def by metis + hence "degree f dvd n" + using n_gt_0 div_gauss_poly_iff[OF _ cthat(2)] by auto + thus "False" + using p_def by (metis assms(2) div_less_dividend n_gt_0 nat_dvd_not_less prime_gt_1_nat) + qed + moreover have "False" if not_l:"\?L" and r1:"?R1" and r2: "?R2" + proof - + obtain g where g_def: "g pdivides f" "degree g < degree f" "monic_irreducible_poly R g" + using r1 not_l exists_irreducible_proper_factor assms(1,2) by auto + + have g_carr: "g \ carrier (poly_ring R)" and g_nz: "g \ \\<^bsub>poly_ring R\<^esub>" + using g_def(3) unfolding monic_irreducible_poly_def monic_poly_def by (auto simp:univ_poly_zero) + + have "g pdivides gauss_poly R (order R^degree f)" + using g_carr r1 g_def(1) unfolding pdivides_def using r.p.divides_trans by blast + + hence "degree g dvd degree f" + using div_gauss_poly_iff[OF assms(2) g_def(3)] by auto + + then obtain t where deg_f_def:"degree f = t * degree g" + by fastforce + hence "t > 1" using g_def(2) by simp + then obtain p where p_prime: "Factorial_Ring.prime p" "p dvd t" + by (metis order_less_irrefl prime_factor_nat) + hence p_div_deg_f: "p dvd degree f" + unfolding deg_f_def by simp + define n where "n = degree f div p" + have n_in_N: "n \ N" + unfolding N_def n_def using p_prime(1) p_div_deg_f by auto + + have deg_g_dvd_n: "degree g dvd n" + using p_prime(2) unfolding n_def deg_f_def by auto + + have n_gt_0: "n > 0" + using p_div_deg_f assms(2) p_prime(1) unfolding n_def + by (metis dvd_div_eq_0_iff gr0I) + + have deg_g_gt_0: "degree g > 0" + using monic_poly_min_degree[OF g_def(3)] by simp + + have 0:"g pdivides gauss_poly R (order R^n)" + using deg_g_dvd_n div_gauss_poly_iff[OF n_gt_0 g_def(3)] by simp + + have "pcoprime (gauss_poly R (order R^n)) f" + using n_in_N r2 by simp + thus "False" + using 0 g_def(1) g_carr deg_g_gt_0 unfolding pcoprime_def by simp + qed + ultimately show ?thesis + by auto +qed + +text \A more general variance of the previous theorem for non-monic polynomials. The result is +from Lemma~1 \cite[rabin1980].\ + +theorem rabin_irreducibility_condition_2: + assumes "f \ carrier (poly_ring R)" "degree f > 0" + defines "N \ {degree f div p | p . Factorial_Ring.prime p \ p dvd degree f}" + shows "pirreducible (carrier R) f \ + (f pdivides gauss_poly R (order R^degree f) \ (\n \ N. pcoprime (gauss_poly R (order R^n)) f))" + (is "?L \ ?R1 \ ?R2") +proof - + define \ where "\ = [inv (hd f)]" + let ?g = "(\x. gauss_poly R (order R^x))" + let ?h = "\ \\<^bsub>poly_ring R\<^esub> f" + + have f_nz: "f \ \\<^bsub>poly_ring R\<^esub>" unfolding univ_poly_zero using assms(2) by auto + + hence "hd f \ carrier R - {\}" using assms(1) lead_coeff_carr by simp + hence "inv (hd f) \ carrier R - {\}" using field_Units by auto + hence \_unit: "\ \ Units (poly_ring R)" + unfolding \_def using univ_poly_carrier_units by simp + + have \_nz: "\ \ \\<^bsub>poly_ring R\<^esub>" unfolding univ_poly_zero \_def by simp + have "hd ?h = hd \ \ hd f" + using \_nz f_nz assms(1) \_unit by (intro lead_coeff_mult) auto + also have "... = inv (hd f) \ hd f" unfolding \_def by simp + also have "... = \" using lead_coeff_carr f_nz assms(1) by (simp add: field_Units) + finally have "hd ?h = \" by simp + moreover have "?h \ []" + using \_nz f_nz univ_poly_zero by (metis \_unit assms(1) r.p.Units_closed r.p.integral) + ultimately have h_monic: "monic_poly R ?h" + using r.p.Units_closed[OF \_unit] assms(1) unfolding monic_poly_def by auto + + have "degree ?h = degree \ + degree f" + using assms(1) f_nz \_unit \_nz by (intro degree_mult[OF carrier_is_subring]) auto + also have "... = degree f" unfolding \_def by simp + finally have deg_f: "degree f = degree ?h" by simp + + have hf_cong:"?h \\<^bsub>r.P\<^esub> f" + using assms(1) \_unit by (simp add: r.p.Units_closed r.p.associatedI2 r.p.m_comm) + hence 0: "f pdivides ?g (degree f) \ ?h pdivides ?g (degree f)" + unfolding pdivides_def using r.p.divides_cong_l r.p.associated_sym + using r.p.Units_closed[OF \_unit] assms(1) gauss_poly_carr by blast + + have 1: "pcoprime (?g n) f \ pcoprime (?g n) ?h" for n + using hf_cong r.p.associated_sym r.p.Units_closed[OF \_unit] assms(1) + by (intro pcoprime_right_assoc_cong gauss_poly_carr) auto + + have "?L \ pirreducible (carrier R) (\ \\<^bsub>poly_ring R\<^esub> f)" + using \_unit \_nz assms(1) f_nz r.p.integral unfolding ring_irreducible_def + by (intro arg_cong2[where f="(\)"] r.p.irreducible_prod_unit assms) auto + also have "... \ monic_irreducible_poly R (\ \\<^bsub>poly_ring R\<^esub> f)" + using h_monic unfolding monic_irreducible_poly_def by auto + also have "... \ ?h pdivides ?g (degree f) \ (\n \ N. pcoprime (?g n) ?h)" + using assms(2) unfolding N_def deg_f by (intro rabin_irreducibility_condition h_monic) auto + also have "... \ f pdivides ?g (degree f) \ (\n \ N. pcoprime (?g n) f)" + using 0 1 by simp + finally show ?thesis by simp +qed + +end + +end \ No newline at end of file diff --git a/thys/Finite_Fields/document/root.bib b/thys/Finite_Fields/document/root.bib --- a/thys/Finite_Fields/document/root.bib +++ b/thys/Finite_Fields/document/root.bib @@ -1,42 +1,53 @@ @book{ireland1982, author = {Kenneth Ireland and Michael Rosen}, title = {A classical introduction to modern number theory}, series = {Graduate texts in mathematics}, volume = {84}, publisher = {Springer}, year = {1982}, isbn = {978-0-387-90625-6}, timestamp = {Fri, 28 Jun 2019 12:45:52 +0200}, biburl = {https://dblp.org/rec/books/daglib/0068082.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @book{lidl1986, author = {Lidl, Rudolf and Niederreiter, Harald}, title = {Introduction to Finite Fields and Their Applications}, year = {1986}, isbn = {0521307066}, publisher = {Cambridge University Press}, address = {USA} } @article{chebolu2010, title={Counting Irreducible Polynomials over Finite Fields Using the Inclusion-Exclusion Principle}, author={Sunil K. Chebolu and J{\'a}n Min{\'a}{\v{c}}}, journal={Mathematics Magazine}, year={2010}, volume={84}, pages={369 - 371} } @article{Dirichlet_Series-AFP, author = {Manuel Eberl}, title = {Dirichlet Series}, journal = {Archive of Formal Proofs}, month = oct, year = 2017, note = {\url{https://isa-afp.org/entries/Dirichlet_Series.html}, Formal proof development}, ISSN = {2150-914x}, -} \ No newline at end of file +} + +@article{rabin1980, + author = {Rabin, Michael O.}, + title = {Probabilistic Algorithms in Finite Fields}, + journal = {SIAM Journal on Computing}, + volume = {9}, + number = {2}, + pages = {273-280}, + year = {1980}, + doi = {10.1137/0209024}, +} diff --git a/thys/Finite_Fields/document/root.tex b/thys/Finite_Fields/document/root.tex --- a/thys/Finite_Fields/document/root.tex +++ b/thys/Finite_Fields/document/root.tex @@ -1,37 +1,37 @@ \documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage{pdfsetup} \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Finite Fields} \author{Emin Karayel} \maketitle \abstract{This entry formalizes the classification of the finite fields (also called Galois fields): For each prime power $p^n$ there exists exactly one (up to isomorphisms) finite field of that size and there are no other finite fields. -The derivation includes a formalization of the characteristic of rings, the Frobenius endomorphism, -formal differentiation for polynomials in HOL-Algebra and Gauss' formula for the number of -monic irreducible polynomials over finite fields: +The derivation includes a formalization of the characteristic of rings, the Frobenius endomorphism, +formal differentiation for polynomials in HOL-Algebra, Rabin's test for the irreducibility of +polynomials and Gauss' formula for the number of monic irreducible polynomials over finite fields: \[ \frac{1}{n} \sum_{d | n} \mu(d) p^{n/d} \textrm{.} \] -The proofs are based on the books from Ireland and Rosen~\cite{ireland1982}, as well as, -Lidl and Niederreiter~\cite{lidl1986}. +The proofs are based on the books and publications from Ireland and Rosen~\cite{ireland1982}, Lidl +and Niederreiter~\cite{lidl1986}, as well as, Rabin~\cite{rabin1980}. } - + \parindent 0pt\parskip 0.5ex \tableofcontents \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document} \ No newline at end of file