Library mathcomp.algebra.qpoly
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype tuple bigop binomial finset finfun ssralg.
From mathcomp Require Import countalg finalg poly polydiv perm fingroup matrix.
From mathcomp Require Import mxalgebra mxpoly vector countalg.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype tuple bigop binomial finset finfun ssralg.
From mathcomp Require Import countalg finalg poly polydiv perm fingroup matrix.
From mathcomp Require Import mxalgebra mxpoly vector countalg.
This file defines the algebras R[X]/<p> and their theory.
It mimics the zmod file for polynomials
First, it defines polynomials of bounded size (equivalent of 'I_n),
gives it a structure of choice, finite and countable (semi)ring, ..., and
lmodule, when possible.
Internally, the construction uses poly_rV and rVpoly, but they should not
be exposed.
We provide two bases: the 'X^i and the lagrange polynomials.
{poly_n R} == the type of polynomial of size at most n
irreducibleb p == boolean decision procedure for irreducibility
of a bounded size polynomial over a finite idomain
Considering {poly_n F} over a field F, it is a vectType and
'nX^i == 'X^i as an element of {poly_n R}
npolyX == [tuple 'X^0, ..., 'X^(n - 1) ], basis of {poly_n R}
x.-lagrange == lagrange basis of {poly_n R} wrt x : nat -> F
x.-lagrange_ i == the ith lagrange polynomial wrt the sampling points x
Second, it defines polynomials quotiented by a poly (equivalent of 'Z_p),
as bounded polynomial. As we are aiming to build a ring structure we need
the polynomial to be monic and of size greater than one. If it is not the
case we quotient by 'X
mk_monic p == the actual polynomial on which we quotient
if p is monic and of size > 1 it is p otherwise 'X
{poly %/ p} == defined as {poly_(size (mk_poly p)).-1 R} on which
there is a ring structure
in_qpoly q == turn the polynomial q into an element of {poly %/ p} by
taking a modulo
'qX == in_qpoly 'X
The last part that defines the field structure when the quotient is an
irreducible polynomial is defined in field/qfpoly
Set Implicit Arguments.
Import GRing.Theory.
Import Pdiv.CommonRing.
Import Pdiv.RingMonic.
Import Pdiv.Field.
Local Open Scope ring_scope.
Reserved Notation "'{poly_' n R }" (n at level 2, format "'{poly_' n R }").
Reserved Notation "''nX^' i" (at level 1, format "''nX^' i").
Reserved Notation "x .-lagrange" (format "x .-lagrange").
Reserved Notation "x .-lagrange_" (format "x .-lagrange_").
Reserved Notation "'qX".
Reserved Notation "{ 'poly' '%/' p }"
(p at level 2, format "{ 'poly' '%/' p }").
Section NPoly.
Context {R : nzSemiRingType} (n : nat).
Definition poly_of_size_pred := fun p : {poly R} ⇒ size p ≤ n.
Arguments poly_of_size_pred _ /.
Definition poly_of_size := [qualify a p | poly_of_size_pred p].
Fact npoly_subsemimod_closed : subsemimod_closed poly_of_size.
Record npoly : predArgType := NPoly {
polyn :> {poly R};
_ : polyn \is a poly_of_size
}.
Lemma npoly_is_a_poly_of_size (p : npoly) : val p \is a poly_of_size.
Hint Resolve npoly_is_a_poly_of_size : core.
Lemma size_npoly (p : npoly) : size p ≤ n.
Hint Resolve size_npoly : core.
Definition npoly_rV : npoly → 'rV[R]_n := poly_rV \o val.
Definition rVnpoly : 'rV[R]_n → npoly := insubd (0 : npoly) \o rVpoly.
Arguments rVnpoly /.
Arguments npoly_rV /.
Lemma npoly_rV_K : cancel npoly_rV rVnpoly.
Lemma rVnpolyK : cancel rVnpoly npoly_rV.
Hint Resolve npoly_rV_K rVnpolyK : core.
Lemma npoly_vect_axiom : SemiVector.axiom n npoly.
End NPoly.
Arguments poly_of_size_pred _ _ /.
Arguments npoly {R}%_type n%_N.
Notation "'{poly_' n R }" := (@npoly R n) : type_scope.
#[global]
Hint Resolve size_npoly npoly_is_a_poly_of_size : core.
Arguments poly_of_size_pred _ _ _ /.
Arguments npoly : clear implicits.
Section SemiNPolyTheory.
Context (R : nzSemiRingType) {n : nat}.
Fact polyn_is_semilinear : semilinear (@polyn _ _ : {poly_n R} → _).
Canonical mk_npoly (E : nat → R) : {poly_n R} :=
@NPoly R _ (\poly_(i < n) E i) (size_poly _ _).
Fact size_npoly0 : size (0 : {poly R}) ≤ n.
Definition npoly0 := NPoly (size_npoly0).
Fact npolyp_key : unit.
Definition npolyp : {poly R} → {poly_n R} :=
locked_with npolyp_key (mk_npoly \o (nth 0)).
Definition npoly_of_seq := npolyp \o Poly.
Lemma npolyP (p q : {poly_n R}) : nth 0 p =1 nth 0 q ↔ p = q.
Lemma coef_npolyp (p : {poly R}) i : (npolyp p)`_i = if i < n then p`_i else 0.
Lemma big_coef_npoly (p : {poly_n R}) i : n ≤ i → p`_i = 0.
Lemma npolypK (p : {poly R}) : size p ≤ n → npolyp p = p :> {poly R}.
Lemma coefn_sum (I : Type) (r : seq I) (P : pred I)
(F : I → {poly_n R}) (k : nat) :
(\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
End SemiNPolyTheory.
Arguments mk_npoly {R} n E.
Arguments npolyp {R} n p.
Section NPolyTheory.
Variables (R : nzRingType) (n : nat).
Fact npoly_oppr_closed : oppr_closed (@poly_of_size R n).
End NPolyTheory.
Section FinSemiNPolyTheory.
Variable R : finNzSemiRingType.
Variable n : nat.
Implicit Types p q : {poly_n R}.
Definition npoly_enum : seq {poly_n R} :=
if n isn't n.+1 then [:: npoly0 _] else
pmap insub [seq \poly_(i < n.+1) c (inord i) | c : (R ^ n.+1)%type].
Lemma npoly_enum_uniq : uniq npoly_enum.
Lemma mem_npoly_enum p : p \in npoly_enum.
Lemma card_npoly : #|{poly_n R}| = (#|R| ^ n)%N.
End FinSemiNPolyTheory.
Section Irreducible.
Variable R : finIdomainType.
Variable p : {poly R}.
Definition irreducibleb :=
((1 < size p) &&
[∀ q : {poly_((size p).-1) R}, (rdvdp q p)%R ==> (size q ≤ 1)])%N.
Lemma irreducibleP : reflect (irreducible_poly p) irreducibleb.
End Irreducible.
Section Vspace.
Variable (K : fieldType) (n : nat).
Lemma dim_polyn : \dim (fullv : {vspace {poly_n K}}) = n.
Definition npolyX : n.-tuple {poly_n K} := [tuple npolyp n 'X^i | i < n].
Notation "''nX^' i" := (tnth npolyX i).
Lemma npolyXE (i : 'I_n) : 'nX^i = 'X^i :> {poly _}.
Lemma nth_npolyX (i : 'I_n) : npolyX`_i = 'nX^i.
Lemma npolyX_free : free npolyX.
Lemma npolyX_full : basis_of fullv npolyX.
Lemma npolyX_coords (p : {poly_n K}) i : coord npolyX i p = p`_i.
Lemma npolyX_gen (p : {poly K}) : (size p ≤ n)%N →
p = \sum_(i < n) p`_i *: 'nX^i.
Section lagrange.
Variables (x : nat → K).
Notation lagrange_def := (fun i :'I_n ⇒
let k := i in let p := \prod_(j < n | j != k) ('X - (x j)%:P)
in (p.[x k]^-1)%:P × p).
Fact lagrange_key : unit.
Definition lagrange := locked_with lagrange_key
[tuple npolyp n (lagrange_def i) | i < n].
Notation lagrange_ := (tnth lagrange).
Hypothesis n_gt0 : (0 < n)%N.
Hypothesis x_inj : injective x.
Let lagrange_def_sample (i j : 'I_n) : (lagrange_def i).[x j] = (i == j)%:R.
Let size_lagrange_def i : size (lagrange_def i) = n.
Lemma lagrangeE i : lagrange_ i = lagrange_def i :> {poly _}.
Lemma nth_lagrange (i : 'I_n) : lagrange`_i = lagrange_ i.
Lemma size_lagrange_ i : size (lagrange_ i) = n.
Lemma size_lagrange : size lagrange = n.
Lemma lagrange_sample (i j : 'I_n) : (lagrange_ i).[x j] = (i == j)%:R.
Lemma lagrange_free : free lagrange.
Lemma lagrange_full : basis_of fullv lagrange.
Lemma lagrange_coords (p : {poly_n K}) i : coord lagrange i p = p.[x i].
Lemma lagrange_gen (p : {poly K}) : (size p ≤ n)%N →
p = \sum_(i < n) p.[x i]%:P × lagrange_ i.
End lagrange.
End Vspace.
Notation "''nX^' i" := (tnth (npolyX _) i) : ring_scope.
Notation "x .-lagrange" := (lagrange x) : ring_scope.
Notation "x .-lagrange_" := (tnth x.-lagrange) : ring_scope.
Section Qpoly.
Variable R : nzSemiRingType.
Variable h : {poly R}.
Definition mk_monic :=
if (1 < size h)%N && (h \is monic) then h else 'X.
Definition qpoly := {poly_(size mk_monic).-1 R}.
End Qpoly.
Notation "{ 'poly' '%/' p }" := (qpoly p) : type_scope.
Section QpolyProp.
Variable R : nzRingType.
Variable h : {poly R}.
Lemma monic_mk_monic : (mk_monic h) \is monic.
Lemma size_mk_monic_gt1 : (1 < size (mk_monic h))%N.
Lemma size_mk_monic_gt0 : (0 < size (mk_monic h))%N.
Lemma mk_monic_neq0 : mk_monic h != 0.
Lemma size_mk_monic (p : {poly %/ h}) : size p < size (mk_monic h).
standard inject
Lemma poly_of_size_mod p :
rmodp p (mk_monic h) \is a poly_of_size (size (mk_monic h)).-1.
Definition in_qpoly p : {poly %/ h} := NPoly (poly_of_size_mod p).
Lemma in_qpoly_small (p : {poly R}) :
size p < size (mk_monic h) → in_qpoly p = p :> {poly R}.
Lemma in_qpoly0 : in_qpoly 0 = 0.
Lemma in_qpolyD p q : in_qpoly (p + q) = in_qpoly p + in_qpoly q.
Lemma in_qpolyZ a p : in_qpoly (a *: p) = a *: in_qpoly p.
Fact in_qpoly_is_linear : linear in_qpoly.
Lemma qpolyC_proof k :
(k%:P : {poly R}) \is a poly_of_size (size (mk_monic h)).-1.
Definition qpolyC k : {poly %/ h} := NPoly (qpolyC_proof k).
Lemma qpolyCE k : qpolyC k = k%:P :> {poly R}.
Lemma qpolyC0 : qpolyC 0 = 0.
Definition qpoly1 := qpolyC 1.
Definition qpoly_mul (q1 q2 : {poly %/ h}) : {poly %/ h} :=
in_qpoly ((q1 : {poly R}) × q2).
Lemma qpoly_mul1z : left_id qpoly1 qpoly_mul.
Lemma qpoly_mulz1 : right_id qpoly1 qpoly_mul.
Lemma qpoly_nontrivial : qpoly1 != 0.
Definition qpolyX := in_qpoly 'X.
Notation "'qX" := qpolyX.
Lemma qpolyXE : 2 < size h → h \is monic → 'qX = 'X :> {poly R}.
End QpolyProp.
Notation "'qX" := (qpolyX _) : ring_scope.
Lemma mk_monic_X (R : nzSemiRingType) : mk_monic 'X = 'X :> {poly R}.
Lemma mk_monic_Xn (R : nzSemiRingType) n :
mk_monic 'X^n = 'X^(n.-1.+1) :> {poly R}.
Lemma card_qpoly (R : finNzSemiRingType) (h : {poly R}):
#|{poly %/ h}| = #|R| ^ (size (mk_monic h)).-1.
Lemma card_monic_qpoly (R : finNzSemiRingType) (h : {poly R}):
1 < size h → h \is monic → #|{poly %/ h}| = #|R| ^ (size h).-1.
Section QRing.
Variable A : comNzRingType.
Variable h : {poly A}.
rmodp p (mk_monic h) \is a poly_of_size (size (mk_monic h)).-1.
Definition in_qpoly p : {poly %/ h} := NPoly (poly_of_size_mod p).
Lemma in_qpoly_small (p : {poly R}) :
size p < size (mk_monic h) → in_qpoly p = p :> {poly R}.
Lemma in_qpoly0 : in_qpoly 0 = 0.
Lemma in_qpolyD p q : in_qpoly (p + q) = in_qpoly p + in_qpoly q.
Lemma in_qpolyZ a p : in_qpoly (a *: p) = a *: in_qpoly p.
Fact in_qpoly_is_linear : linear in_qpoly.
Lemma qpolyC_proof k :
(k%:P : {poly R}) \is a poly_of_size (size (mk_monic h)).-1.
Definition qpolyC k : {poly %/ h} := NPoly (qpolyC_proof k).
Lemma qpolyCE k : qpolyC k = k%:P :> {poly R}.
Lemma qpolyC0 : qpolyC 0 = 0.
Definition qpoly1 := qpolyC 1.
Definition qpoly_mul (q1 q2 : {poly %/ h}) : {poly %/ h} :=
in_qpoly ((q1 : {poly R}) × q2).
Lemma qpoly_mul1z : left_id qpoly1 qpoly_mul.
Lemma qpoly_mulz1 : right_id qpoly1 qpoly_mul.
Lemma qpoly_nontrivial : qpoly1 != 0.
Definition qpolyX := in_qpoly 'X.
Notation "'qX" := qpolyX.
Lemma qpolyXE : 2 < size h → h \is monic → 'qX = 'X :> {poly R}.
End QpolyProp.
Notation "'qX" := (qpolyX _) : ring_scope.
Lemma mk_monic_X (R : nzSemiRingType) : mk_monic 'X = 'X :> {poly R}.
Lemma mk_monic_Xn (R : nzSemiRingType) n :
mk_monic 'X^n = 'X^(n.-1.+1) :> {poly R}.
Lemma card_qpoly (R : finNzSemiRingType) (h : {poly R}):
#|{poly %/ h}| = #|R| ^ (size (mk_monic h)).-1.
Lemma card_monic_qpoly (R : finNzSemiRingType) (h : {poly R}):
1 < size h → h \is monic → #|{poly %/ h}| = #|R| ^ (size h).-1.
Section QRing.
Variable A : comNzRingType.
Variable h : {poly A}.
Ring operations
Lemma qpoly_mulC : commutative (@qpoly_mul A h).
Lemma qpoly_mulA : associative (@qpoly_mul A h).
Lemma qpoly_mul_addr : right_distributive (@qpoly_mul A h) +%R.
Lemma qpoly_mul_addl : left_distributive (@qpoly_mul A h) +%R.
Lemma in_qpoly1 : in_qpoly h 1 = 1.
Lemma in_qpolyM q1 q2 : in_qpoly h (q1 × q2) = in_qpoly h q1 × in_qpoly h q2.
Fact in_qpoly_monoid_morphism : monoid_morphism (in_qpoly h).
#[deprecated(since="mathcomp 2.5.0",
note="use `in_qpoly_is_monoid_morphism` instead")]
Definition in_qpoly_is_multiplicative :=
(fun g ⇒ (g.2,g.1)) in_qpoly_monoid_morphism.
Lemma poly_of_qpoly_sum I (r : seq I) (P1 : pred I) (F : I → {poly %/ h}) :
((\sum_(i <- r | P1 i) F i) =
\sum_(p <- r | P1 p) ((F p) : {poly A}) :> {poly A})%R.
Lemma poly_of_qpolyD (p q : {poly %/ h}) :
p + q= (p : {poly A}) + q :> {poly A}.
Lemma qpolyC_natr p : (p%:R : {poly %/ h}) = p%:R :> {poly A}.
Lemma pchar_qpoly : [pchar {poly %/ h}] =i [pchar A].
Lemma poly_of_qpolyM (p q : {poly %/ h}) :
p × q = rmodp ((p : {poly A}) × q) (mk_monic h) :> {poly A}.
Lemma poly_of_qpolyX (p : {poly %/ h}) n :
p ^+ n = rmodp ((p : {poly A}) ^+ n) (mk_monic h) :> {poly A}.
Lemma qpolyCN (a : A) : qpolyC h (- a) = -(qpolyC h a).
Lemma qpolyCD : {morph (qpolyC h) : a b / a + b >-> a + b}%R.
Lemma qpolyCM : {morph (qpolyC h) : a b / a × b >-> a × b}%R.
Lemma qpolyC_is_zmod_morphism : zmod_morphism (qpolyC h).
#[deprecated(since="mathcomp 2.5.0",
note="use `qpolyC_is_zmod_morphism` instead")]
Definition qpolyC_is_additive := qpolyC_is_zmod_morphism.
Lemma qpolyC_is_monoid_morphism : monoid_morphism (qpolyC h).
#[deprecated(since="mathcomp 2.5.0",
note="use `qpolyC_is_monoid_morphism` instead")]
Definition qpolyC_is_multiplicative :=
(fun g ⇒ (g.2,g.1)) qpolyC_is_monoid_morphism.
Definition qpoly_scale k (p : {poly %/ h}) : {poly %/ h} := (k *: p)%R.
Fact qpoly_scaleA a b p :
qpoly_scale a (qpoly_scale b p) = qpoly_scale (a × b) p.
Fact qpoly_scale1l : left_id 1%R qpoly_scale.
Fact qpoly_scaleDr a : {morph qpoly_scale a : p q / (p + q)%R}.
Fact qpoly_scaleDl p : {morph qpoly_scale^~ p : a b / a + b}%R.
Fact qpoly_scaleAl a p q : qpoly_scale a (p × q) = (qpoly_scale a p × q).
Fact qpoly_scaleAr a p q : qpoly_scale a (p × q) = p × (qpoly_scale a q).
Lemma poly_of_qpolyZ (p : {poly %/ h}) a :
a *: p = a *: (p : {poly A}) :> {poly A}.
End QRing.
#[deprecated(since="mathcomp 2.4.0", note="Use pchar_qpoly instead.")]
Notation char_qpoly := (pchar_qpoly) (only parsing).
Section Field.
Variable R : fieldType.
Variable h : {poly R}.
Local Notation hQ := (mk_monic h).
Definition qpoly_inv (p : {poly %/ h}) :=
if coprimep hQ p then let v : {poly %/ h} := in_qpoly h (egcdp hQ p).2 in
((lead_coef (v × p)) ^-1 *: v) else p.
Ugly
Lemma qpoly_mulVz (p : {poly %/ h}) : coprimep hQ p → (qpoly_inv p × p = 1)%R.
Lemma qpoly_mulzV (p : {poly %/ h}) :
coprimep hQ p → (p × (qpoly_inv p) = 1)%R.
Lemma qpoly_intro_unit (p q : {poly %/ h}) : (q × p = 1)%R → coprimep hQ p.
Lemma qpoly_inv_out (p : {poly %/ h}) : ~~ coprimep hQ p → qpoly_inv p = p.
Lemma irreducible_poly_coprime (A : idomainType) (p q : {poly A}) :
irreducible_poly p → coprimep p q = ~~(p %| q)%R.
End Field.
Lemma qpoly_mulzV (p : {poly %/ h}) :
coprimep hQ p → (p × (qpoly_inv p) = 1)%R.
Lemma qpoly_intro_unit (p q : {poly %/ h}) : (q × p = 1)%R → coprimep hQ p.
Lemma qpoly_inv_out (p : {poly %/ h}) : ~~ coprimep hQ p → qpoly_inv p = p.
Lemma irreducible_poly_coprime (A : idomainType) (p q : {poly A}) :
irreducible_poly p → coprimep p q = ~~(p %| q)%R.
End Field.