# Theory Finite_Field_Factorization

```(*
Authors:      Jose Divasón
Sebastiaan Joosten
René Thiemann
*)
section ‹A Combined Factorization Algorithm for Polynomials over GF(p)›

subsection‹Type Based Version›
text ‹We combine Berlekamp's algorithm with the distinct degree factorization
to obtain an efficient factorization algorithm for square-free polynomials in GF(p).›

theory Finite_Field_Factorization
imports Berlekamp_Type_Based
Distinct_Degree_Factorization
begin

text ‹We prove soundness of the finite field factorization,
indepedendent on whether distinct-degree-factorization is
applied as preprocessing or not.›
consts use_distinct_degree_factorization :: bool

context
assumes "SORT_CONSTRAINT('a::prime_card)"
begin

definition finite_field_factorization :: "'a mod_ring poly ⇒ 'a mod_ring × 'a mod_ring poly list" where
"finite_field_factorization f = (if degree f = 0 then (lead_coeff f,[]) else let
u = smult (inverse a) f;
gs = (if use_distinct_degree_factorization then distinct_degree_factorization u else [(1,u)]);
(irr,hs) = List.partition (λ (i,f). degree f = i) gs
in (a,map snd irr @ concat (map (λ (i,g). berlekamp_monic_factorization i g) hs)))"

lemma finite_field_factorization_explicit:
fixes f::"'a mod_ring poly"
assumes sf_f: "square_free f"
and us: "finite_field_factorization f = (c,us)"
shows "f = smult c (prod_list us) ∧ (∀ u ∈ set us. monic u ∧ irreducible u)"
proof (cases "degree f = 0")
case False note f = this
define g where "g = smult (inverse c) f"
obtain gs where dist: "(if use_distinct_degree_factorization then distinct_degree_factorization g else [(1,g)]) = gs" by auto
note us = us[unfolded finite_field_factorization_def Let_def]
from us f have c: "c = lead_coeff f" by auto
obtain irr hs where part: "List.partition (λ (i, f). degree f = i) gs = (irr,hs)" by force
from arg_cong[OF this, of fst] have irr: "irr = filter (λ (i, f). degree f = i) gs" by auto
from us[folded c, folded g_def, unfolded dist part split] f
have us: "us = map snd irr @ concat (map (λ(x, y). berlekamp_monic_factorization x y) hs)" by auto
from f c have c0: "c ≠ 0" by auto
from False c0 have deg_g: "degree g ≠ 0" unfolding g_def by auto
have mon_g: "monic g" unfolding g_def
by (metis c c0 field_class.field_inverse lead_coeff_smult)
from sf_f have sf_g: "square_free g" unfolding g_def by (simp add: c0)
from c0 have f: "f = smult c g" unfolding g_def by auto
have "g = prod_list (map snd gs) ∧ (∀ (i,f) ∈ set gs. degree f > 0 ∧ monic f ∧ (∀ h. h dvd f ⟶ degree h = i ⟶ irreducible h))"
proof (cases use_distinct_degree_factorization)
case True
with dist have "distinct_degree_factorization g = gs" by auto
note dist = distinct_degree_factorization[OF this sf_g mon_g]
from dist have g: "g = prod_list (map snd gs)" by auto
show ?thesis
proof (intro conjI[OF g] ballI, clarify)
fix i f
assume "(i,f) ∈ set gs"
with dist have "factors_of_same_degree i f" by auto
from factors_of_same_degreeD[OF this]
show "degree f > 0 ∧ monic f ∧ (∀h. h dvd f ⟶ degree h = i ⟶ irreducible h)" by auto
qed
next
case False
with dist have gs: "gs = [(1,g)]" by auto
show ?thesis unfolding gs using deg_g mon_g linear_irreducible⇩d[where 'a = "'a mod_ring"] by auto
qed
hence g_gs: "g = prod_list (map snd gs)"
and mon_gs: "⋀ i f. (i, f) ∈ set gs ⟹ monic f ∧ degree f > 0"
and irrI: "⋀ i f h . (i, f) ∈ set gs ⟹ h dvd f ⟹ degree h = i ⟹ irreducible h" by auto
have g: "g = prod_list (map snd irr) * prod_list (map snd hs)" unfolding g_gs
using prod_list_map_partition[OF part] .
{
fix f
assume "f ∈ snd ` set irr"
from this[unfolded irr] obtain i where *:  "(i,f) ∈ set gs" "degree f = i" by auto
have "f dvd f" by auto
from irrI[OF *(1) this *(2)] mon_gs[OF *(1)] have "monic f" "irreducible f" by auto
} note irr = this
let ?berl = "λ hs. concat (map (λ(x, y). berlekamp_monic_factorization x y) hs)"
have "set hs ⊆ set gs" using part by auto
hence "prod_list (map snd hs) = prod_list (?berl hs)
∧ (∀ f ∈ set (?berl hs). monic f ∧ irreducible⇩d f)"
proof (induct hs)
case (Cons ih hs)
obtain i h where ih: "ih = (i,h)" by force
have "?berl (Cons ih hs) = berlekamp_monic_factorization i h @ ?berl hs" unfolding ih by auto
from Cons(2)[unfolded ih] have mem: "(i,h) ∈ set gs" and sub: "set hs ⊆ set gs" by auto
note IH = Cons(1)[OF sub]
from mem have "h ∈ set (map snd gs)" by force
from square_free_factor[OF prod_list_dvd[OF this], folded g_gs, OF sf_g] have sf: "square_free h" .
from mon_gs[OF mem] irrI[OF mem] have *: "degree h > 0" "monic h"
"⋀ g. g dvd h ⟹ degree g = i ⟹ irreducible g" by auto
from berlekamp_monic_factorization[OF sf refl *(3) *(1-2), of i]
have berl: "prod_list (berlekamp_monic_factorization i h) = h"
and irr: "⋀ f. f ∈ set (berlekamp_monic_factorization i h) ⟹ monic f ∧ irreducible f" by auto
have "prod_list (map snd (Cons ih hs)) = h * prod_list (map snd hs)" unfolding ih by simp
also have "prod_list (map snd hs) = prod_list (?berl hs)" using IH by auto
finally have "prod_list (map snd (Cons ih hs)) = prod_list (?berl (Cons ih hs))"
unfolding ih using berl by auto
thus ?case using IH irr unfolding ih by auto
qed auto
with g irr have main: "g = prod_list us ∧ (∀ u ∈ set us. monic u ∧ irreducible⇩d u)" unfolding us
by auto
thus ?thesis unfolding f using sf_g by auto
next
case True
with us[unfolded finite_field_factorization_def] have "c = lead_coeff f" and us: "us = []" by auto
with degree0_coeffs[OF True] have f: "f = [:c:]" by auto
show ?thesis unfolding us f by (auto simp: normalize_poly_def)
qed

lemma finite_field_factorization:
fixes f::"'a mod_ring poly"
assumes sf_f: "square_free f"
and us: "finite_field_factorization f = (c,us)"
shows "unique_factorization Irr_Mon f (c, mset us)"
proof -
from finite_field_factorization_explicit[OF sf_f us]
have fact: "factorization Irr_Mon f (c, mset us)"
unfolding factorization_def split Irr_Mon_def by (auto simp: prod_mset_prod_list)
from sf_f[unfolded square_free_def] have "f ≠ 0" by auto
from exactly_one_factorization[OF this] fact
show ?thesis unfolding unique_factorization_def by auto
qed
end

text ‹Experiments revealed that preprocessing via
distinct-degree-factorization slows down the factorization
algorithm (statement for implementation in AFP 2017)›