Theory Finite_Field_Factorization
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
a = lead_coeff f;
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)›
overloading use_distinct_degree_factorization ≡ use_distinct_degree_factorization
begin
definition use_distinct_degree_factorization
where [code_unfold]: "use_distinct_degree_factorization = False"
end
end