Module mathcomp.algebra.poly
From HB Require Import structures.From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop finset tuple div binomial.
From mathcomp Require Import nmodule rings_modules_and_algebras divalg decfield.
From mathcomp Require Import countalg.
This file provides a library for univariate polynomials over ring
structures; it also provides an extended theory for polynomials whose
coefficients range over commutative rings and integral domains.
{poly R} == the type of polynomials with coefficients of type R,
represented as lists with a non zero last element in
little endian representation; the coefficient type R
must be a nzSemiRingType. {poly R} inherits the
nzSemiRingType, nzRingType, comNzSemiRingType,
comNzRingType, and idomainType structures of R.
p : seq R == the big-endian sequence of coefficients of p, via
the coercion polyseq : polynomial >-> seq.
Poly s == the polynomial with coefficient sequence s (ignoring
trailing zeroes).
\poly_(i < n) E(i) == the polynomial of degree at most n - 1 whose
coefficients are given by the general term E(i)
polyC c, c%:P == the constant polynomial c
'X == the (unique) variable
'X^n == a power of 'X; 'X^0 is 1, 'X^1 is convertible to 'X
p`_i == the coefficient of 'X^i in p; this is in fact just
the ring_scope notation generic seq-indexing using
nth 0%R, combined with the polyseq coercion.
*** The multi-rule coefE simplifies p`_i
coefp i == the linear function p |-> p`_i (self-exapanding).
size p == 1 + the degree of p, or 0 if p = 0 (this is the
generic seq function combined with polyseq).
lead_coef p == the coefficient of the highest monomial in p, or 0
if p = 0 (hence lead_coef p = 0 iff p = 0)
p \is monic <=> lead_coef p == 1 (0 is not monic).
p \is a polyOver S <=> the coefficients of p satisfy S; S should have a
key that should be (at least) an addrPred.
p.[x] == the evaluation of a polynomial p at a point x using
the Horner scheme
*** The multi-rule hornerE (resp., hornerE_comm) unwinds
horner evaluation of a polynomial expression (resp.,
in a non commutative ring, with side conditions).
p^`() == formal derivative of p
p^`(n) == formal n-derivative of p
p^`N(n) == formal n-derivative of p divided by n!
p \Po q == polynomial composition; because this is naturally a
a linear morphism in the first argument, this
notation is transposed (q comes before p for redex
selection, etc).
:= \sum(i < size p) p`_i *: q ^+ i
odd_poly p == monomials of odd degree of p
even_poly p == monomials of even degree of p
take_poly n p == polynomial p without its monomials of degree >= n
drop_poly n p == polynomial p divided by X^n
comm_poly p x == x and p.[x] commute; this is a sufficient condition
for evaluating (q * p).[x] as q.[x] * p.[x] when R
is not commutative.
comm_coef p x == x commutes with all the coefficients of p (clearly,
this implies comm_poly p x).
root p x == x is a root of p, i.e., p.[x] = 0
n.-unity_root x == x is an nth root of unity, i.e., a root of 'X^n - 1
n.-primitive_root x == x is a primitive nth root of unity, i.e., n is the
least positive integer m > 0 such that x ^+ m = 1.
*** The submodule poly.UnityRootTheory can be used to
import selectively the part of the theory of roots
of unity that doesn't mention polynomials explicitly
map_poly f p == the image of the polynomial by the function f (which
(locally, p^f) is usually a ring morphism).
p^:P == p lifted to {poly {poly R}} (:= map_poly polyC p).
commr_rmorph f u == u commutes with the image of f (i.e., with all f x).
horner_morph cfu == given cfu : commr_rmorph f u, the function mapping p
to the value of map_poly f p at u; this is a ring
morphism from {poly R} to the codomain of f when f
is a ring morphism.
horner_eval u == the (semi)linear function mapping p to p.[u], which
is a (semi)algebra morphism when u is in a
commutative (semi)ring.
horner_alg a == given a in some R-(semi)algebra A, the function
evaluating a polynomial p at a; it is always a
(semi)algebra morphism from {poly R} to A.
diff_roots x y == x and y are distinct roots; if R is a field, this
just means x != y, but this concept is generalized
to the case where R is only a ring with units (i.e.,
a unitRingType); in which case it means that x and y
commute, and that the difference x - y is a unit
(i.e., has a multiplicative inverse) in R.
to just x != y).
uniq_roots s == s is a sequence or pairwise distinct roots, in the
sense of diff_roots p above.
*** We only show that these operations and properties are transferred by
morphisms whose domain is a field (thus ensuring injectivity).
We prove the factor_theorem, and the max_poly_roots inequality relating
the number of distinct roots of a polynomial and its size.
The some polynomial lemmas use following suffix interpretation :
C - constant polynomial (as in polyseqC : a%:P = nseq (a != 0) a).
X - the polynomial variable 'X (as in coefX : 'X`_i = (i == 1%N)).
Xn - power of 'X (as in monicXn : monic 'X^n).
Pdeg2.Field (exported by the present library) : theory of the degree 2
polynomials.
Pdeg2.FieldMonic : theory of Pdeg2.Field specialized to monic polynomials.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope unity_root_scope.
Import GRing.Theory.
Local Open Scope ring_scope.
Reserved Notation "{ 'poly' T }" (format "{ 'poly' T }").
Reserved Notation "c %:P" (format "c %:P").
Reserved Notation "p ^:P" (format "p ^:P").
Reserved Notation "'X".
Reserved Notation "''X^' n" (at level 1, format "''X^' n").
Reserved Notation "\poly_ ( i < n ) E"
(at level 34, E at level 36, i, n at level 50,
format "\poly_ ( i < n ) E").
Reserved Notation "p \Po q" (at level 50).
Reserved Notation "p ^`N ( n )" (format "p ^`N ( n )").
Reserved Notation "n .-unity_root" (format "n .-unity_root").
Reserved Notation "n .-primitive_root" (format "n .-primitive_root").
Local Notation simp := Monoid.simpm.
Section Polynomial.
Variable R : nzSemiRingType.
Record polynomial := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}.
HB.instance Definition _ := [isSub for polyseq].
HB.instance Definition _ := [Choice of polynomial by <:].
Lemma poly_inj : injective polyseq
Proof.
Definition coefp i (p : polynomial) := p`_i.
End Polynomial.
Bind Scope ring_scope with polynomial.
Arguments polynomial R%_type.
Arguments polyseq {R} p%_R.
Arguments poly_inj {R} [p1%_R p2%_R] : rename.
Arguments coefp {R} i%_N / p%_R.
Notation "{ 'poly' T }" := (polynomial T) : type_scope.
Section SemiPolynomialTheory.
Variable R : nzSemiRingType.
Implicit Types (a b c x y z : R) (p q r d : {poly R}).
Definition lead_coef p := p`_(size p).-1.
Lemma lead_coefE p : lead_coef p = p`_(size p).-1
Proof.
by []. Qed.
Definition poly_nil := @Polynomial R [::] (oner_neq0 R).
Definition polyC c : {poly R} := insubd poly_nil [:: c].
Local Notation "c %:P" := (polyC c).
Lemma polyseqC c : c%:P = nseq (c != 0) c :> seq R.
Proof.
Lemma size_polyC c : size c%:P = (c != 0).
Lemma coefC c i : c%:P`_i = if i == 0 then c else 0.
Lemma polyCK : cancel polyC (coefp 0).
Lemma polyC_inj : injective polyC.
Lemma lead_coefC c : lead_coef c%:P = c.
Lemma polyP p q : nth 0 p =1 nth 0 q <-> p = q.
Proof.
split=> [eq_pq | -> //]; apply: poly_inj.
without loss lt_pq: p q eq_pq / size p < size q.
move=> IH; case: (ltngtP (size p) (size q)); try by move/IH->.
by move/(@eq_from_nth _ 0); apply.
case: q => q nz_q /= in lt_pq eq_pq *; case/eqP: nz_q.
by rewrite (last_nth 0) -(subnKC lt_pq) /= -eq_pq nth_default ?leq_addr.
Qed.
without loss lt_pq: p q eq_pq / size p < size q.
move=> IH; case: (ltngtP (size p) (size q)); try by move/IH->.
by move/(@eq_from_nth _ 0); apply.
case: q => q nz_q /= in lt_pq eq_pq *; case/eqP: nz_q.
by rewrite (last_nth 0) -(subnKC lt_pq) /= -eq_pq nth_default ?leq_addr.
Qed.
Lemma size1_polyC p : size p <= 1 -> p = (p`_0)%:P.
Proof.
move=> le_p_1; apply/polyP=> i; rewrite coefC.
by case: i => // i; rewrite nth_default // (leq_trans le_p_1).
Qed.
by case: i => // i; rewrite nth_default // (leq_trans le_p_1).
Qed.
Definition cons_poly c p : {poly R} :=
if p is Polynomial ((_ :: _) as s) ns then
@Polynomial R (c :: s) ns
else c%:P.
Lemma polyseq_cons c p :
cons_poly c p = (if ~~ nilp p then c :: p else c%:P) :> seq R.
Proof.
by case: p => [[]]. Qed.
Lemma size_cons_poly c p :
size (cons_poly c p) = (if nilp p && (c == 0) then 0 else (size p).+1).
Proof.
Lemma coef_cons c p i : (cons_poly c p)`_i = if i == 0 then c else p`_i.-1.
Definition Poly := foldr cons_poly 0%:P.
Lemma PolyK c s : last c s != 0 -> Poly s = s :> seq R.
Proof.
case: s => {c}/= [_ |c s]; first by rewrite polyseqC eqxx.
elim: s c => /= [|a s IHs] c nz_c; rewrite polyseq_cons ?{}IHs //.
by rewrite !polyseqC !eqxx nz_c.
Qed.
elim: s c => /= [|a s IHs] c nz_c; rewrite polyseq_cons ?{}IHs //.
by rewrite !polyseqC !eqxx nz_c.
Qed.
Lemma polyseqK p : Poly p = p.
Lemma size_Poly s : size (Poly s) <= size s.
Proof.
elim: s => [|c s IHs] /=; first by rewrite polyseqC eqxx.
by rewrite size_cons_poly; case: ifP.
Qed.
by rewrite size_cons_poly; case: ifP.
Qed.
Lemma coef_Poly s i : (Poly s)`_i = s`_i.
Definition poly_expanded_def n E := Poly (mkseq E n).
Fact poly_key : unit
Proof.
by []. Qed.
Canonical poly_unlockable := [unlockable fun poly].
Local Notation "\poly_ ( i < n ) E" := (poly n (fun i : nat => E)).
Lemma polyseq_poly n E :
E n.-1 != 0 -> \poly_(i < n) E i = mkseq [eta E] n :> seq R.
Proof.
Lemma size_poly n E : size (\poly_(i < n) E i) <= n.
Proof.
Lemma size_poly_eq n E : E n.-1 != 0 -> size (\poly_(i < n) E i) = n.
Proof.
Lemma coef_poly n E k : (\poly_(i < n) E i)`_k = (if k < n then E k else 0).
Proof.
rewrite unlock coef_Poly.
have [lt_kn | le_nk] := ltnP k n; first by rewrite nth_mkseq.
by rewrite nth_default // size_mkseq.
Qed.
have [lt_kn | le_nk] := ltnP k n; first by rewrite nth_mkseq.
by rewrite nth_default // size_mkseq.
Qed.
Lemma lead_coef_poly n E :
n > 0 -> E n.-1 != 0 -> lead_coef (\poly_(i < n) E i) = E n.-1.
Proof.
Lemma coefK p : \poly_(i < size p) p`_i = p.
Proof.
Definition add_poly_def p q := \poly_(i < maxn (size p) (size q)) (p`_i + q`_i).
Fact add_poly_key : unit
Proof.
by []. Qed.
Canonical add_poly_unlockable := [unlockable fun add_poly].
Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
Proof.
Fact add_polyA : associative add_poly.
Proof.
Fact add_polyC : commutative add_poly.
Proof.
Fact add_poly0 : left_id 0%:P add_poly.
Proof.
HB.instance Definition _ := GRing.isNmodule.Build (polynomial R)
add_polyA add_polyC add_poly0.
Lemma polyC0 : 0%:P = 0 :> {poly R}
Proof.
by []. Qed.
Lemma polyseq0 : (0 : {poly R}) = [::] :> seq R.
Lemma size_poly0 : size (0 : {poly R}) = 0%N.
Proof.
Lemma coef0 i : (0 : {poly R})`_i = 0.
Lemma lead_coef0 : lead_coef 0 = 0 :> R
Proof.
Lemma size_poly_eq0 p : (size p == 0) = (p == 0).
Lemma size_poly_leq0 p : (size p <= 0) = (p == 0).
Proof.
Lemma size_poly_leq0P p : reflect (p = 0) (size p <= 0).
Proof.
Lemma size_poly_gt0 p : (0 < size p) = (p != 0).
Proof.
Lemma gt_size_poly_neq0 p n : size p > n -> p != 0.
Proof.
Lemma nil_poly p : nilp p = (p == 0).
Proof.
Lemma poly0Vpos p : {p = 0} + {size p > 0}.
Proof.
Lemma polySpred p : p != 0 -> size p = (size p).-1.+1.
Proof.
Lemma lead_coef_eq0 p : (lead_coef p == 0) = (p == 0).
Proof.
Lemma polyC_eq0 c : (c%:P == 0) = (c == 0).
Lemma size_poly1P p : reflect (exists2 c, c != 0 & p = c%:P) (size p == 1).
Proof.
apply: (iffP eqP) => [pC | [c nz_c ->]]; last by rewrite size_polyC nz_c.
have def_p: p = (p`_0)%:P by rewrite -size1_polyC ?pC.
by exists p`_0; rewrite // -polyC_eq0 -def_p -size_poly_eq0 pC.
Qed.
have def_p: p = (p`_0)%:P by rewrite -size1_polyC ?pC.
by exists p`_0; rewrite // -polyC_eq0 -def_p -size_poly_eq0 pC.
Qed.
Lemma size_polyC_leq1 c : (size c%:P <= 1)%N.
Proof.
Lemma leq_sizeP p i : reflect (forall j, i <= j -> p`_j = 0) (size p <= i).
Proof.
apply: (iffP idP) => [hp j hij| hp].
by apply: nth_default; apply: leq_trans hij.
case: (eqVneq p) (lead_coef_eq0 p) => [->|p0]; first by rewrite size_poly0.
rewrite leqNgt; apply/contraFN => hs.
by apply/eqP/hp; rewrite -ltnS (ltn_predK hs).
Qed.
by apply: nth_default; apply: leq_trans hij.
case: (eqVneq p) (lead_coef_eq0 p) => [->|p0]; first by rewrite size_poly0.
rewrite leqNgt; apply/contraFN => hs.
by apply/eqP/hp; rewrite -ltnS (ltn_predK hs).
Qed.
Lemma coefD p q i : (p + q)`_i = p`_i + q`_i.
Proof.
HB.instance Definition _ i := GRing.isNmodMorphism.Build {poly R} R (coefp i)
(coef0 i, fun p q => coefD p q i).
Lemma coefMn p n i : (p *+ n)`_i = p`_i *+ n.
Lemma coef_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) k :
(\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
Lemma polyCD : {morph polyC : a b / a + b}.
HB.instance Definition _ := GRing.isNmodMorphism.Build R {poly R} polyC
(polyC0, polyCD).
Lemma polyCMn n : {morph polyC : c / c *+ n}
Proof.
Lemma size_polyD p q : size (p + q) <= maxn (size p) (size q).
Lemma size_polyDl p q : size p > size q -> size (p + q) = size p.
Proof.
move=> ltqp; rewrite -[+%R]/add_poly unlock size_poly_eq (maxn_idPl (ltnW _))//.
by rewrite addrC nth_default ?simp ?nth_last //; case: p ltqp => [[]].
Qed.
by rewrite addrC nth_default ?simp ?nth_last //; case: p ltqp => [[]].
Qed.
Lemma size_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) :
size (\sum_(i <- r | P i) F i) <= \max_(i <- r | P i) size (F i).
Proof.
elim/big_rec2: _ => [|i p q _ IHp]; first by rewrite size_poly0.
by rewrite -(maxn_idPr IHp) maxnA leq_max size_polyD.
Qed.
by rewrite -(maxn_idPr IHp) maxnA leq_max size_polyD.
Qed.
Lemma lead_coefDl p q : size p > size q -> lead_coef (p + q) = lead_coef p.
Proof.
move=> ltqp; rewrite /lead_coef coefD size_polyDl //.
by rewrite addrC nth_default ?simp // -ltnS (ltn_predK ltqp).
Qed.
by rewrite addrC nth_default ?simp // -ltnS (ltn_predK ltqp).
Qed.
Lemma lead_coefDr p q : size q > size p -> lead_coef (p + q) = lead_coef q.
Proof.
Definition mul_poly_def p q :=
\poly_(i < (size p + size q).-1) (\sum_(j < i.+1) p`_j * q`_(i - j)).
Fact mul_poly_key : unit
Proof.
by []. Qed.
Canonical mul_poly_unlockable := [unlockable fun mul_poly].
Fact coef_mul_poly p q i :
(mul_poly p q)`_i = \sum_(j < i.+1) p`_j * q`_(i - j).
Proof.
Fact coef_mul_poly_rev p q i :
(mul_poly p q)`_i = \sum_(j < i.+1) p`_(i - j) * q`_j.
Proof.
rewrite coef_mul_poly (reindex_inj rev_ord_inj) /=.
by apply: eq_bigr => j _; rewrite (sub_ordK j).
Qed.
by apply: eq_bigr => j _; rewrite (sub_ordK j).
Qed.
Fact mul_polyA : associative mul_poly.
Proof.
move=> p q r; apply/polyP=> i; rewrite coef_mul_poly coef_mul_poly_rev.
pose coef3 j k := p`_j * (q`_(i - j - k) * r`_k).
transitivity (\sum_(j < i.+1) \sum_(k < i.+1 | k <= i - j) coef3 j k).
apply: eq_bigr => /= j _; rewrite coef_mul_poly_rev big_distrr /=.
by rewrite (big_ord_narrow_leq (leq_subr _ _)).
rewrite (exchange_big_dep predT) //=; apply: eq_bigr => k _.
transitivity (\sum_(j < i.+1 | j <= i - k) coef3 j k).
apply: eq_bigl => j; rewrite -ltnS -(ltnS j) -!subSn ?leq_ord //.
by rewrite -subn_gt0 -(subn_gt0 j) -!subnDA addnC.
rewrite (big_ord_narrow_leq (leq_subr _ _)) coef_mul_poly big_distrl /=.
by apply: eq_bigr => j _; rewrite /coef3 -!subnDA addnC mulrA.
Qed.
pose coef3 j k := p`_j * (q`_(i - j - k) * r`_k).
transitivity (\sum_(j < i.+1) \sum_(k < i.+1 | k <= i - j) coef3 j k).
apply: eq_bigr => /= j _; rewrite coef_mul_poly_rev big_distrr /=.
by rewrite (big_ord_narrow_leq (leq_subr _ _)).
rewrite (exchange_big_dep predT) //=; apply: eq_bigr => k _.
transitivity (\sum_(j < i.+1 | j <= i - k) coef3 j k).
apply: eq_bigl => j; rewrite -ltnS -(ltnS j) -!subSn ?leq_ord //.
by rewrite -subn_gt0 -(subn_gt0 j) -!subnDA addnC.
rewrite (big_ord_narrow_leq (leq_subr _ _)) coef_mul_poly big_distrl /=.
by apply: eq_bigr => j _; rewrite /coef3 -!subnDA addnC mulrA.
Qed.
Fact mul_1poly : left_id 1%:P mul_poly.
Proof.
move=> p; apply/polyP => i; rewrite coef_mul_poly big_ord_recl subn0.
by rewrite big1 => [j _|]; rewrite coefC !simp.
Qed.
by rewrite big1 => [j _|]; rewrite coefC !simp.
Qed.
Fact mul_poly1 : right_id 1%:P mul_poly.
Proof.
move=> p; apply/polyP => i; rewrite coef_mul_poly_rev big_ord_recl subn0.
by rewrite big1 => [j _|]; rewrite coefC !simp.
Qed.
by rewrite big1 => [j _|]; rewrite coefC !simp.
Qed.
Fact mul_polyDl : left_distributive mul_poly +%R.
Proof.
Fact mul_polyDr : right_distributive mul_poly +%R.
Proof.
Fact mul_0poly : left_zero 0%:P mul_poly.
Proof.
move=> p; apply/polyP => i; rewrite coef_mul_poly big_ord_recl subn0.
by rewrite big1 => [j _|]; rewrite coefC !simp // coefC; case: ifP.
Qed.
by rewrite big1 => [j _|]; rewrite coefC !simp // coefC; case: ifP.
Qed.
Fact mul_poly0 : right_zero 0%:P mul_poly.
Proof.
move=> p; apply/polyP => i; rewrite coef_mul_poly_rev big_ord_recl subn0.
by rewrite big1 => [j _|]; rewrite coefC !simp // coefC; case: ifP.
Qed.
by rewrite big1 => [j _|]; rewrite coefC !simp // coefC; case: ifP.
Qed.
Fact poly1_neq0 : 1%:P != 0 :> {poly R}.
HB.instance Definition _ := GRing.Nmodule_isNzSemiRing.Build (polynomial R)
mul_polyA mul_1poly mul_poly1 mul_polyDl mul_polyDr mul_0poly mul_poly0
poly1_neq0.
Lemma polyC1 : 1%:P = 1 :> {poly R}
Proof.
by []. Qed.
Lemma polyseq1 : (1 : {poly R}) = [:: 1] :> seq R.
Lemma size_poly1 : size (1 : {poly R}) = 1.
Proof.
Lemma coef1 i : (1 : {poly R})`_i = (i == 0)%:R.
Lemma lead_coef1 : lead_coef 1 = 1 :> R
Proof.
Lemma coefM p q i : (p * q)`_i = \sum_(j < i.+1) p`_j * q`_(i - j).
Proof.
Lemma coefMr p q i : (p * q)`_i = \sum_(j < i.+1) p`_(i - j) * q`_j.
Proof.
Lemma coef0M p q : (p * q)`_0 = p`_0 * q`_0.
Fact coefp0_is_monoid_morphism : monoid_morphism (coefp 0).
#[deprecated(since="mathcomp 2.5.0", use=coefp0_is_monoid_morphism)]
Definition coefp0_multiplicative :=
(fun g => (g.2, g.1)) coefp0_is_monoid_morphism.
HB.instance Definition _ := GRing.isMonoidMorphism.Build {poly R} R (coefp 0)
coefp0_is_monoid_morphism.
Lemma coef0_prod I rI (F : I -> {poly R}) P :
(\prod_(i <- rI| P i) F i)`_0 = \prod_(i <- rI | P i) (F i)`_0.
Proof.
Lemma size_polyMleq p q : size (p * q) <= (size p + size q).-1.
Lemma mul_lead_coef p q :
lead_coef p * lead_coef q = (p * q)`_(size p + size q).-2.
Proof.
pose dp := (size p).-1; pose dq := (size q).-1.
have [-> | nz_p] := eqVneq p 0; first by rewrite lead_coef0 !mul0r coef0.
have [-> | nz_q] := eqVneq q 0; first by rewrite lead_coef0 !mulr0 coef0.
have ->: (size p + size q).-2 = (dp + dq)%N.
by do 2!rewrite polySpred // addSn addnC.
have lt_p_pq: dp < (dp + dq).+1 by rewrite ltnS leq_addr.
rewrite coefM (bigD1 (Ordinal lt_p_pq)) ?big1 ?simp ?addKn //= => i.
rewrite -val_eqE neq_ltn /= => /orP[lt_i_p | gt_i_p]; last first.
by rewrite nth_default ?mul0r //; rewrite -polySpred in gt_i_p.
rewrite [q`__]nth_default ?mulr0 //= -subSS -{1}addnS -polySpred //.
by rewrite addnC -addnBA ?leq_addr.
Qed.
have [-> | nz_p] := eqVneq p 0; first by rewrite lead_coef0 !mul0r coef0.
have [-> | nz_q] := eqVneq q 0; first by rewrite lead_coef0 !mulr0 coef0.
have ->: (size p + size q).-2 = (dp + dq)%N.
by do 2!rewrite polySpred // addSn addnC.
have lt_p_pq: dp < (dp + dq).+1 by rewrite ltnS leq_addr.
rewrite coefM (bigD1 (Ordinal lt_p_pq)) ?big1 ?simp ?addKn //= => i.
rewrite -val_eqE neq_ltn /= => /orP[lt_i_p | gt_i_p]; last first.
by rewrite nth_default ?mul0r //; rewrite -polySpred in gt_i_p.
rewrite [q`__]nth_default ?mulr0 //= -subSS -{1}addnS -polySpred //.
by rewrite addnC -addnBA ?leq_addr.
Qed.
Lemma size_proper_mul p q :
lead_coef p * lead_coef q != 0 -> size (p * q) = (size p + size q).-1.
Proof.
apply: contraNeq; rewrite mul_lead_coef eqn_leq size_polyMleq -ltnNge => lt_pq.
by rewrite nth_default // -subn1 -(leq_add2l 1) -leq_subLR leq_sub2r.
Qed.
by rewrite nth_default // -subn1 -(leq_add2l 1) -leq_subLR leq_sub2r.
Qed.
Lemma lead_coef_proper_mul p q :
let c := lead_coef p * lead_coef q in c != 0 -> lead_coef (p * q) = c.
Proof.
Lemma size_poly_prod_leq (I : finType) (P : pred I) (F : I -> {poly R}) :
size (\prod_(i | P i) F i) <= (\sum_(i | P i) size (F i)).+1 - #|P|.
Proof.
rewrite -sum1_card.
elim/big_rec3: _ => [|i n m p _ IHp]; first by rewrite size_poly1.
have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 size_poly0.
rewrite (leq_trans (size_polyMleq _ _)) // subnS -!subn1 leq_sub2r //.
rewrite -addnS -addnBA ?leq_add2l // ltnW // -subn_gt0 (leq_trans _ IHp) //.
by rewrite polySpred.
Qed.
elim/big_rec3: _ => [|i n m p _ IHp]; first by rewrite size_poly1.
have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 size_poly0.
rewrite (leq_trans (size_polyMleq _ _)) // subnS -!subn1 leq_sub2r //.
rewrite -addnS -addnBA ?leq_add2l // ltnW // -subn_gt0 (leq_trans _ IHp) //.
by rewrite polySpred.
Qed.
Lemma coefCM c p i : (c%:P * p)`_i = c * p`_i.
Lemma coefMC c p i : (p * c%:P)`_i = p`_i * c.
Lemma polyCM : {morph polyC : a b / a * b}.
Lemma size_poly_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1.
Proof.
elim: n => [|n IHn]; first by rewrite size_poly1.
have [-> | nzp] := poly0Vpos p; first by rewrite exprS mul0r size_poly0.
rewrite exprS (leq_trans (size_polyMleq _ _)) //.
by rewrite -{1}(prednK nzp) mulnS -addnS leq_add2l.
Qed.
have [-> | nzp] := poly0Vpos p; first by rewrite exprS mul0r size_poly0.
rewrite exprS (leq_trans (size_polyMleq _ _)) //.
by rewrite -{1}(prednK nzp) mulnS -addnS leq_add2l.
Qed.
Fact polyC_is_monoid_morphism : monoid_morphism polyC.
Proof.
Definition polyC_multiplicative :=
(fun g => (g.2, g.1)) polyC_is_monoid_morphism.
HB.instance Definition _ := GRing.isMonoidMorphism.Build R {poly R} polyC
polyC_is_monoid_morphism.
Lemma polyC_exp n : {morph polyC : c / c ^+ n}
Proof.
Lemma polyC_natr n : n%:R%:P = n%:R :> {poly R}
Proof.
Lemma pchar_poly : [pchar {poly R}] =i [pchar R].
Proof.
Definition scale_poly_def a (p : {poly R}) := \poly_(i < size p) (a * p`_i).
Fact scale_poly_key : unit
Proof.
by []. Qed.
Canonical scale_poly_unlockable := [unlockable fun scale_poly].
Fact scale_polyE a p : scale_poly a p = a%:P * p.
Proof.
Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a * b) p.
Proof.
Fact scale_0poly p : scale_poly 0 p = 0.
Proof.
Fact scale_1poly : left_id 1 scale_poly.
Proof.
Fact scale_polyDr a : {morph scale_poly a : p q / p + q}.
Proof.
Fact scale_polyDl p : {morph scale_poly^~ p : a b / a + b}.
Proof.
Fact scale_polyAl a p q : scale_poly a (p * q) = scale_poly a p * q.
Proof.
HB.instance Definition _ := GRing.Nmodule_isLSemiModule.Build R (polynomial R)
scale_polyA scale_0poly scale_1poly scale_polyDr scale_polyDl.
HB.instance Definition _ :=
GRing.LSemiModule_isLSemiAlgebra.Build R (polynomial R) scale_polyAl.
Lemma mul_polyC a p : a%:P * p = a *: p.
Proof.
Lemma scale_polyC a b : a *: b%:P = (a * b)%:P.
Lemma alg_polyC a : a%:A = a%:P :> {poly R}.
Lemma coefZ a p i : (a *: p)`_i = a * p`_i.
Proof.
rewrite -[*:%R]/scale_poly unlock coef_poly.
by case: leqP => // le_p_n; rewrite nth_default ?mulr0.
Qed.
by case: leqP => // le_p_n; rewrite nth_default ?mulr0.
Qed.
Lemma size_scale_leq a p : size (a *: p) <= size p.
Proof.
HB.instance Definition _ i := GRing.isScalable.Build R {poly R} R *%R (coefp i)
(fun a => coefZ a ^~ i).
HB.instance Definition _ := GRing.Linear.on (coefp 0).
Definition polyX_def := Poly [:: 0; 1].
Fact polyX_key : unit
Proof.
by []. Qed.
Canonical polyX_unlockable := [unlockable of polyX].
Local Notation "'X" := polyX.
Lemma polyseqX : 'X = [:: 0; 1] :> seq R.
Proof.
Lemma size_polyX : size 'X = 2
Proof.
Lemma polyX_eq0 : ('X == 0) = false.
Proof.
Lemma coefX i : 'X`_i = (i == 1)%:R.
Lemma lead_coefX : lead_coef 'X = 1.
Lemma commr_polyX p : GRing.comm p 'X.
Proof.
Lemma coefMX p i : (p * 'X)`_i = (if (i == 0)%N then 0 else p`_i.-1).
Proof.
Lemma coefXM p i : ('X * p)`_i = (if (i == 0)%N then 0 else p`_i.-1).
Proof.
Lemma cons_poly_def p a : cons_poly a p = p * 'X + a%:P.
Lemma poly_ind (K : {poly R} -> Type) :
K 0 -> (forall p c, K p -> K (p * 'X + c%:P)) -> (forall p, K p).
Proof.
move=> K0 Kcons p; rewrite -[p]polyseqK.
by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons.
Qed.
by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons.
Qed.
Lemma polyseqXaddC a : 'X + a%:P = [:: a; 1] :> seq R.
Proof.
Lemma size_XaddC b : size ('X + b%:P) = 2.
Proof.
Lemma lead_coefXaddC a : lead_coef ('X + a%:P) = 1.
Proof.
Lemma size_MXaddC p c :
size (p * 'X + c%:P) = (if (p == 0) && (c == 0) then 0 else (size p).+1).
Proof.
Lemma polyseqMX p : p != 0 -> p * 'X = 0 :: p :> seq R.
Proof.
Lemma size_mulX p : p != 0 -> size (p * 'X) = (size p).+1.
Proof.
Lemma lead_coefMX p : lead_coef (p * 'X) = lead_coef p.
Proof.
Lemma size_XmulC a : a != 0 -> size ('X * a%:P) = 2.
Proof.
Local Notation "''X^' n" := ('X ^+ n).
Lemma coefXn n i : 'X^n`_i = (i == n)%:R.
Lemma polyseqXn n : 'X^n = rcons (nseq n 0) 1 :> seq R.
Proof.
elim: n => [|n IHn]; rewrite ?polyseq1 // exprSr.
by rewrite polyseqMX -?size_poly_eq0 IHn ?size_rcons.
Qed.
by rewrite polyseqMX -?size_poly_eq0 IHn ?size_rcons.
Qed.
Lemma size_polyXn n : size 'X^n = n.+1.
Proof.
Lemma commr_polyXn p n : GRing.comm p 'X^n.
Proof.
Lemma lead_coefXn n : lead_coef 'X^n = 1.
Proof.
Lemma lead_coefXnaddC n c : 0 < n -> lead_coef ('X^n + c%:P) = 1.
Proof.
move=> n_gt0; rewrite lead_coefDl ?lead_coefXn//.
by rewrite size_polyC size_polyXn ltnS (leq_trans (leq_b1 _)).
Qed.
by rewrite size_polyC size_polyXn ltnS (leq_trans (leq_b1 _)).
Qed.
Lemma size_XnaddC n c : 0 < n -> size ('X^n + c%:P) = n.+1.
Proof.
Lemma polyseqMXn n p : p != 0 -> p * 'X^n = ncons n 0 p :> seq R.
Proof.
Lemma coefMXn n p i : (p * 'X^n)`_i = if i < n then 0 else p`_(i - n).
Proof.
Lemma size_mulXn n p : p != 0 -> size (p * 'X^n) = (n + size p)%N.
Proof.
Lemma coefXnM n p i : ('X^n * p)`_i = if i < n then 0 else p`_(i - n).
Proof.
Lemma coef_sumMXn I (r : seq I) (P : pred I) (p : I -> R) (n : I -> nat) k :
(\sum_(i <- r | P i) p i *: 'X^(n i))`_k =
\sum_(i <- r | P i && (n i == k)) p i.
Proof.
Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i.
Proof.
Lemma eq_poly n E1 E2 : (forall i, i < n -> E1 i = E2 i) ->
poly n E1 = poly n E2 :> {poly R}.
Implicit Types s rs : seq R.
Fixpoint horner_rec s x := if s is a :: s' then horner_rec s' x * x + a else 0.
Definition horner p := horner_rec p.
Local Notation "p .[ x ]" := (horner p x) : ring_scope.
Lemma horner0 x : (0 : {poly R}).[x] = 0.
Lemma hornerC c x : (c%:P).[x] = c.
Lemma hornerX x : 'X.[x] = x.
Lemma horner_cons p c x : (cons_poly c p).[x] = p.[x] * x + c.
Lemma horner_coef0 p : p.[0] = p`_0.
Lemma hornerMXaddC p c x : (p * 'X + c%:P).[x] = p.[x] * x + c.
Proof.
Lemma hornerMX p x : (p * 'X).[x] = p.[x] * x.
Proof.
Lemma horner_Poly s x : (Poly s).[x] = horner_rec s x.
Proof.
Lemma horner_coef p x : p.[x] = \sum_(i < size p) p`_i * x ^+ i.
Proof.
Lemma horner_coef_wide n p x :
size p <= n -> p.[x] = \sum_(i < n) p`_i * x ^+ i.
Proof.
move=> le_p_n.
rewrite horner_coef (big_ord_widen n (fun i => p`_i * x ^+ i)) // big_mkcond.
by apply: eq_bigr => i _; case: ltnP => // le_p_i; rewrite nth_default ?simp.
Qed.
rewrite horner_coef (big_ord_widen n (fun i => p`_i * x ^+ i)) // big_mkcond.
by apply: eq_bigr => i _; case: ltnP => // le_p_i; rewrite nth_default ?simp.
Qed.
Lemma horner_poly n E x : (\poly_(i < n) E i).[x] = \sum_(i < n) E i * x ^+ i.
Proof.
rewrite (@horner_coef_wide n) ?size_poly //.
by apply: eq_bigr => i _; rewrite coef_poly ltn_ord.
Qed.
by apply: eq_bigr => i _; rewrite coef_poly ltn_ord.
Qed.
Lemma hornerD p q x : (p + q).[x] = p.[x] + q.[x].
Proof.
Lemma hornerCM a p x : (a%:P * p).[x] = a * p.[x].
Proof.
Lemma hornerZ c p x : (c *: p).[x] = c * p.[x].
Definition horner_eval (x : R) := horner^~ x.
Lemma horner_evalE x p : horner_eval x p = p.[x]
Proof.
by []. Qed.
HB.instance Definition _ x :=
GRing.isSemilinear.Build R {poly R} R _ (horner_eval x)
((fun c p => hornerZ c p x), (fun p q => hornerD p q x)).
Lemma horner_sum I (r : seq I) (P : pred I) F x :
(\sum_(i <- r | P i) F i).[x] = \sum_(i <- r | P i) (F i).[x].
Proof.
Lemma hornerMn n p x : (p *+ n).[x] = p.[x] *+ n.
Proof.
Definition comm_coef p x := forall i, p`_i * x = x * p`_i.
Definition comm_poly p x := x * p.[x] = p.[x] * x.
Lemma comm_coef_poly p x : comm_coef p x -> comm_poly p x.
Proof.
move=> cpx; rewrite /comm_poly !horner_coef big_distrl big_distrr /=.
by apply: eq_bigr => i _; rewrite /= mulrA -cpx -!mulrA commrX.
Qed.
by apply: eq_bigr => i _; rewrite /= mulrA -cpx -!mulrA commrX.
Qed.
Lemma comm_poly0 x : comm_poly 0 x.
Lemma comm_poly1 x : comm_poly 1 x.
Lemma comm_polyX x : comm_poly 'X x.
Lemma comm_polyD p q x: comm_poly p x -> comm_poly q x -> comm_poly (p + q) x.
Lemma commr_horner a b p : GRing.comm a b -> comm_coef p a -> GRing.comm a p.[b].
Proof.
move=> cab cpa; rewrite horner_coef; apply: commr_sum => i _.
by apply: commrM => //; apply: commrX.
Qed.
by apply: commrM => //; apply: commrX.
Qed.
Lemma hornerM_comm p q x : comm_poly q x -> (p * q).[x] = p.[x] * q.[x].
Proof.
Lemma comm_polyM p q x: comm_poly p x -> comm_poly q x -> comm_poly (p * q) x.
Proof.
Lemma horner_exp_comm p x n : comm_poly p x -> (p ^+ n).[x] = p.[x] ^+ n.
Proof.
move=> comm_px; elim: n => [|n IHn]; first by rewrite hornerC.
by rewrite !exprSr -IHn hornerM_comm.
Qed.
by rewrite !exprSr -IHn hornerM_comm.
Qed.
Lemma comm_poly_exp p n x: comm_poly p x -> comm_poly (p ^+ n) x.
Proof.
Lemma hornerXn x n : ('X^n).[x] = x ^+ n.
Proof.
Implicit Type S : {pred R}.
Definition polyOver_pred S := fun p : {poly R} => all (mem S) p.
Arguments polyOver_pred _ _ /.
Definition polyOver S := [qualify a p | polyOver_pred S p].
Lemma polyOverS (S1 S2 : {pred R}) :
{subset S1 <= S2} -> {subset polyOver S1 <= polyOver S2}.
Lemma polyOver0 S : 0 \is a polyOver S.
Lemma polyOver_poly S n E :
(forall i, i < n -> E i \in S) -> \poly_(i < n) E i \is a polyOver S.
Proof.
Section PolyOverAdd.
Variable S : addrClosed R.
Lemma polyOverP {p} : reflect (forall i, p`_i \in S) (p \in polyOver S).
Proof.
Lemma polyOverC c : (c%:P \in polyOver S) = (c \in S).
Fact polyOver_nmod_closed : nmod_closed (polyOver S).
Proof.
polyOver_nmod_closed.
End PolyOverAdd.
Section PolyOverSemiRing2.
Variable S : semiring2Closed R.
Lemma polyOver_mulr_2closed : GRing.mulr_2closed (polyOver S).
Proof.
polyOver_mulr_2closed.
End PolyOverSemiRing2.
Section PolyOverSemiring.
Variable S : semiringClosed R.
Fact polyOver_mul1_closed : 1 \in polyOver S.
HB.instance Definition _ := GRing.isMul1Closed.Build {poly R} (polyOver_pred S)
polyOver_mul1_closed.
Lemma polyOverZ : {in S & polyOver S, forall c p, c *: p \is a polyOver S}.
Lemma polyOverX : 'X \in polyOver S.
Lemma polyOverXn n : 'X^n \in polyOver S.
Lemma rpred_horner : {in polyOver S & S, forall p x, p.[x] \in S}.
Proof.
move=> p x /polyOverP Sp Sx; rewrite horner_coef rpred_sum // => i _.
by rewrite rpredM ?rpredX.
Qed.
by rewrite rpredM ?rpredX.
Qed.
End PolyOverSemiring.
Definition deriv p := \poly_(i < (size p).-1) (p`_i.+1 *+ i.+1).
Local Notation "a ^` ()" := (deriv a).
Lemma coef_deriv p i : p^`()`_i = p`_i.+1 *+ i.+1.
Proof.
Lemma polyOver_deriv (ringS : semiringClosed R) :
{in polyOver ringS, forall p, p^`() \is a polyOver ringS}.
Proof.
Lemma derivC c : c%:P^`() = 0.
Proof.
Lemma derivX : ('X)^`() = 1.
Proof.
Lemma derivXn n : ('X^n)^`() = 'X^(n.-1) *+ n.
Proof.
Fact deriv_is_semilinear : semilinear deriv.
Proof.
split=> [k p|p q]; apply/polyP => i.
by rewrite !(coef_deriv, coefZ) mulrnAr.
by rewrite !(coef_deriv, coefD) mulrnDl.
Qed.
by rewrite !(coef_deriv, coefZ) mulrnAr.
by rewrite !(coef_deriv, coefD) mulrnDl.
Qed.
deriv_is_semilinear.
Lemma deriv0 : 0^`() = 0.
Proof.
Lemma derivD : {morph deriv : p q / p + q}.
Proof.
Lemma derivMn n p : (p *+ n)^`() = p^`() *+ n.
Proof.
Lemma derivZ c p : (c *: p)^`() = c *: p^`().
Proof.
Lemma deriv_mulC c p : (c%:P * p)^`() = c%:P * p^`().
Lemma derivMXaddC p c : (p * 'X + c%:P)^`() = p + p^`() * 'X.
Proof.
Lemma derivM p q : (p * q)^`() = p^`() * q + p * q^`().
Proof.
elim/poly_ind: p => [|p b IHp]; first by rewrite !(mul0r, add0r, derivC).
rewrite mulrDl -mulrA -commr_polyX mulrA -[_ * 'X]addr0 raddfD /= !derivMXaddC.
by rewrite deriv_mulC IHp !mulrDl -!mulrA !commr_polyX !addrA.
Qed.
rewrite mulrDl -mulrA -commr_polyX mulrA -[_ * 'X]addr0 raddfD /= !derivMXaddC.
by rewrite deriv_mulC IHp !mulrDl -!mulrA !commr_polyX !addrA.
Qed.
Definition derivn n p := iter n deriv p.
Local Notation "a ^` ( n )" := (derivn n a) : ring_scope.
Lemma derivn0 p : p^`(0) = p.
Proof.
by []. Qed.
Lemma derivn1 p : p^`(1) = p^`().
Proof.
by []. Qed.
Lemma derivnS p n : p^`(n.+1) = p^`(n)^`().
Proof.
by []. Qed.
Lemma derivSn p n : p^`(n.+1) = p^`()^`(n).
Proof.
Lemma coef_derivn n p i : p^`(n)`_i = p`_(n + i) *+ (n + i) ^_ n.
Proof.
Lemma polyOver_derivn (ringS : semiringClosed R) :
{in polyOver ringS, forall p n, p^`(n) \is a polyOver ringS}.
Proof.
Fact derivn_is_semilinear n : semilinear (derivn n).
Proof.
GRing.isSemilinear.Build R {poly R} {poly R} _ (derivn n)
(derivn_is_semilinear n).
Lemma derivnC c n : c%:P^`(n) = if n == 0 then c%:P else 0.
Lemma derivnD n : {morph derivn n : p q / p + q}.
Proof.
Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.
Proof.
Lemma derivnZ n : scalable (derivn n).
Proof.
Lemma derivnXn m n : ('X^m)^`(n) = 'X^(m - n) *+ m ^_ n.
Proof.
Lemma derivnMXaddC n p c :
(p * 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) * 'X.
Proof.
Lemma derivn_poly0 p n : size p <= n -> p^`(n) = 0.
Proof.
move=> le_p_n; apply/polyP=> i; rewrite coef_derivn.
rewrite nth_default; last by rewrite mul0rn coef0.
exact/(leq_trans le_p_n)/leq_addr.
Qed.
rewrite nth_default; last by rewrite mul0rn coef0.
exact/(leq_trans le_p_n)/leq_addr.
Qed.
Lemma lt_size_deriv (p : {poly R}) : p != 0 -> size p^`() < size p.
Definition nderivn n p := \poly_(i < size p - n) (p`_(n + i) *+ 'C(n + i, n)).
Local Notation "a ^`N ( n )" := (nderivn n a) : ring_scope.
Lemma coef_nderivn n p i : p^`N(n)`_i = p`_(n + i) *+ 'C(n + i, n).
Proof.
Lemma nderivn_def n p : p^`(n) = p^`N(n) *+ n`!.
Proof.
Lemma polyOver_nderivn (ringS : semiringClosed R) :
{in polyOver ringS, forall p n, p^`N(n) \in polyOver ringS}.
Proof.
Lemma nderivn0 p : p^`N(0) = p.
Proof.
Lemma nderivn1 p : p^`N(1) = p^`().
Proof.
Lemma nderivnC c n : (c%:P)^`N(n) = if n == 0 then c%:P else 0.
Proof.
Lemma nderivnXn m n : ('X^m)^`N(n) = 'X^(m - n) *+ 'C(m, n).
Proof.
Fact nderivn_is_semilinear n : semilinear (nderivn n).
Proof.
split=> [k p|p q]; apply/polyP => i.
by rewrite !(coef_nderivn, coefZ) mulrnAr.
by rewrite !(coef_nderivn, coefD) mulrnDl.
Qed.
by rewrite !(coef_nderivn, coefZ) mulrnAr.
by rewrite !(coef_nderivn, coefD) mulrnDl.
Qed.
GRing.isSemilinear.Build R {poly R} {poly R} _ (nderivn n)
(nderivn_is_semilinear n).
Lemma nderivnD n : {morph nderivn n : p q / p + q}.
Proof.
Lemma nderivnMn n m p : (p *+ m)^`N(n) = p^`N(n) *+ m.
Proof.
Lemma nderivnZ n : scalable (nderivn n).
Proof.
Lemma nderivnMXaddC n p c :
(p * 'X + c%:P)^`N(n.+1) = p^`N(n) + p^`N(n.+1) * 'X.
Proof.
Lemma nderivn_poly0 p n : size p <= n -> p^`N(n) = 0.
Proof.
move=> le_p_n; apply/polyP=> i; rewrite coef_nderivn.
rewrite nth_default; last by rewrite mul0rn coef0.
exact/(leq_trans le_p_n)/leq_addr.
Qed.
rewrite nth_default; last by rewrite mul0rn coef0.
exact/(leq_trans le_p_n)/leq_addr.
Qed.
Lemma nderiv_taylor p x h :
GRing.comm x h -> p.[x + h] = \sum_(i < size p) p^`N(i).[x] * h ^+ i.
Proof.
move/commrX=> cxh; elim/poly_ind: p => [|p c IHp].
by rewrite size_poly0 big_ord0 horner0.
rewrite hornerMXaddC size_MXaddC.
have [-> | nz_p] := eqVneq p 0.
rewrite horner0 !simp; have [-> | _] := c =P 0; first by rewrite big_ord0.
by rewrite size_poly0 big_ord_recl big_ord0 nderivn0 hornerC !simp.
rewrite big_ord_recl nderivn0 !simp hornerMXaddC addrAC; congr (_ + _).
rewrite mulrDr {}IHp !big_distrl polySpred //= big_ord_recl /= mulr1 -addrA.
rewrite nderivn0 /bump /(addn 1) /=; congr (_ + _).
rewrite !big_ord_recr /= nderivnMXaddC -mulrA -exprSr -polySpred // !addrA.
congr (_ + _); last by rewrite (nderivn_poly0 (leqnn _)) !simp.
rewrite addrC -big_split /=; apply: eq_bigr => i _.
rewrite nderivnMXaddC hornerD (hornerM_comm _ (comm_polyX _)) hornerX.
by rewrite mulrDl -!mulrA -exprSr cxh.
Qed.
by rewrite size_poly0 big_ord0 horner0.
rewrite hornerMXaddC size_MXaddC.
have [-> | nz_p] := eqVneq p 0.
rewrite horner0 !simp; have [-> | _] := c =P 0; first by rewrite big_ord0.
by rewrite size_poly0 big_ord_recl big_ord0 nderivn0 hornerC !simp.
rewrite big_ord_recl nderivn0 !simp hornerMXaddC addrAC; congr (_ + _).
rewrite mulrDr {}IHp !big_distrl polySpred //= big_ord_recl /= mulr1 -addrA.
rewrite nderivn0 /bump /(addn 1) /=; congr (_ + _).
rewrite !big_ord_recr /= nderivnMXaddC -mulrA -exprSr -polySpred // !addrA.
congr (_ + _); last by rewrite (nderivn_poly0 (leqnn _)) !simp.
rewrite addrC -big_split /=; apply: eq_bigr => i _.
rewrite nderivnMXaddC hornerD (hornerM_comm _ (comm_polyX _)) hornerX.
by rewrite mulrDl -!mulrA -exprSr cxh.
Qed.
Lemma nderiv_taylor_wide n p x h :
GRing.comm x h -> size p <= n ->
p.[x + h] = \sum_(i < n) p^`N(i).[x] * h ^+ i.
Proof.
move/nderiv_taylor=> -> le_p_n.
rewrite (big_ord_widen n (fun i => p^`N(i).[x] * h ^+ i)) // big_mkcond.
apply: eq_bigr => i _; case: leqP => // /nderivn_poly0->.
by rewrite horner0 simp.
Qed.
rewrite (big_ord_widen n (fun i => p^`N(i).[x] * h ^+ i)) // big_mkcond.
apply: eq_bigr => i _; case: leqP => // /nderivn_poly0->.
by rewrite horner0 simp.
Qed.
Definition monic_pred := fun p => lead_coef p == 1.
Arguments monic_pred _ /.
Definition monic := [qualify p | monic_pred p].
Lemma monicE p : (p \is monic) = (lead_coef p == 1)
Proof.
by []. Qed.
Proof.
Lemma monic1 : 1 \is monic
Proof.
Proof.
Proof.
Lemma monic_neq0 p : p \is monic -> p != 0.
Proof.
Lemma lead_coef_monicM p q : p \is monic -> lead_coef (p * q) = lead_coef q.
Proof.
have [-> | nz_q] := eqVneq q 0; first by rewrite mulr0.
by move/monicP=> mon_p; rewrite lead_coef_proper_mul mon_p mul1r ?lead_coef_eq0.
Qed.
by move/monicP=> mon_p; rewrite lead_coef_proper_mul mon_p mul1r ?lead_coef_eq0.
Qed.
Lemma lead_coef_Mmonic p q : q \is monic -> lead_coef (p * q) = lead_coef p.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite mul0r.
by move/monicP=> mon_q; rewrite lead_coef_proper_mul mon_q mulr1 ?lead_coef_eq0.
Qed.
by move/monicP=> mon_q; rewrite lead_coef_proper_mul mon_q mulr1 ?lead_coef_eq0.
Qed.
Lemma size_monicM p q :
p \is monic -> q != 0 -> size (p * q) = (size p + size q).-1.
Proof.
Lemma size_Mmonic p q :
p != 0 -> q \is monic -> size (p * q) = (size p + size q).-1.
Proof.
Lemma monicMl p q : p \is monic -> (p * q \is monic) = (q \is monic).
Proof.
Lemma monicMr p q : q \is monic -> (p * q \is monic) = (p \is monic).
Proof.
Fact monic_mulr_closed : mulr_closed monic.
HB.instance Definition _ := GRing.isMulClosed.Build {poly R} monic_pred
monic_mulr_closed.
Lemma monic_exp p n : p \is monic -> p ^+ n \is monic.
Proof.
Lemma monic_prod I rI (P : pred I) (F : I -> {poly R}):
(forall i, P i -> F i \is monic) -> \prod_(i <- rI | P i) F i \is monic.
Proof.
Lemma monicXaddC c : 'X + c%:P \is monic.
Proof.
Lemma monicXnaddC n c : 0 < n -> 'X^n + c%:P \is monic.
Proof.
Lemma lreg_lead0 p : GRing.lreg (lead_coef p) -> p != 0.
Proof.
Lemma rreg_lead0 p : GRing.rreg (lead_coef p) -> p != 0.
Proof.
Lemma lreg_size c p : GRing.lreg c -> size (c *: p) = size p.
Proof.
move=> reg_c; have [-> | nz_p] := eqVneq p 0; first by rewrite scaler0.
rewrite -mul_polyC size_proper_mul; last by rewrite size_polyC lreg_neq0.
by rewrite lead_coefC mulrI_eq0 ?lead_coef_eq0.
Qed.
rewrite -mul_polyC size_proper_mul; last by rewrite size_polyC lreg_neq0.
by rewrite lead_coefC mulrI_eq0 ?lead_coef_eq0.
Qed.
Lemma lreg_polyZ_eq0 c p : GRing.lreg c -> (c *: p == 0) = (p == 0).
Proof.
Lemma lead_coef_lreg c p : GRing.lreg c -> lead_coef (c *: p) = c * lead_coef p.
Proof.
Lemma rreg_size c p : GRing.rreg c -> size (p * c%:P) = size p.
Proof.
move=> reg_c; have [-> | nz_p] := eqVneq p 0; first by rewrite mul0r.
rewrite size_proper_mul; last by rewrite size_polyC rreg_neq0 ?addn1.
by rewrite lead_coefC mulIr_eq0 ?lead_coef_eq0.
Qed.
rewrite size_proper_mul; last by rewrite size_polyC rreg_neq0 ?addn1.
by rewrite lead_coefC mulIr_eq0 ?lead_coef_eq0.
Qed.
Lemma rreg_polyMC_eq0 c p : GRing.rreg c -> (p * c%:P == 0) = (p == 0).
Proof.
Lemma rreg_div0 q r d :
GRing.rreg (lead_coef d) -> size r < size d ->
(q * d + r == 0) = (q == 0) && (r == 0).
Proof.
move=> /mulIr_eq0 reg_d lt_r_d; rewrite addrC.
have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r addr0.
have qd0: lead_coef q * lead_coef d != 0 by rewrite reg_d lead_coef_eq0.
apply/negbTE; rewrite -size_poly_eq0 addrC size_polyDl; last first.
by rewrite size_poly_eq0 -lead_coef_eq0 lead_coef_proper_mul.
apply: leq_trans lt_r_d _; rewrite size_proper_mul //.
move: nz_q; rewrite -size_poly_eq0.
by case: (size q) => [//|] ? _; rewrite addSn /= leq_addl.
Qed.
have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r addr0.
have qd0: lead_coef q * lead_coef d != 0 by rewrite reg_d lead_coef_eq0.
apply/negbTE; rewrite -size_poly_eq0 addrC size_polyDl; last first.
by rewrite size_poly_eq0 -lead_coef_eq0 lead_coef_proper_mul.
apply: leq_trans lt_r_d _; rewrite size_proper_mul //.
move: nz_q; rewrite -size_poly_eq0.
by case: (size q) => [//|] ? _; rewrite addSn /= leq_addl.
Qed.
Lemma monic_comreg p :
p \is monic -> GRing.comm p (lead_coef p)%:P /\ GRing.rreg (lead_coef p).
Definition root p : pred R := fun x => p.[x] == 0.
Lemma mem_root p x : (x \in root p) = (p.[x] == 0).
Proof.
by []. Qed.
Lemma rootE p x : (root p x = (p.[x] == 0)) * ((x \in root p) = (p.[x] == 0)).
Proof.
by []. Qed.
Lemma rootP p x : reflect (p.[x] = 0) (root p x).
Proof.
Lemma rootPt p x : reflect (p.[x] == 0) (root p x).
Proof.
Lemma rootPf p x : reflect ((p.[x] == 0) = false) (~~ root p x).
Proof.
Lemma rootC a x : root a%:P x = (a == 0).
Lemma root0 x : root 0 x.
Proof.
Lemma root1 x : ~~ root 1 x.
Lemma rootX x : root 'X x = (x == 0).
Lemma root_size_gt1 a p : p != 0 -> root p a -> 1 < size p.
Proof.
End SemiPolynomialTheory.
Prenex Implicits polyC polyCK Poly polyseqK lead_coef horner polyOver.
Prenex Implicits deriv derivn root.
Notation "\poly_ ( i < n ) E" := (poly n (fun i => E)) : ring_scope.
Notation "c %:P" := (polyC c) : ring_scope.
Notation "'X" := (polyX _) : ring_scope.
Notation "''X^' n" := ('X ^+ n) : ring_scope.
Notation "p .[ x ]" := (horner p x) : ring_scope.
Notation "a ^` ()" := (deriv a) : ring_scope.
Notation "a ^` ( n )" := (derivn n a) : ring_scope.
Notation "a ^`N ( n )" := (nderivn n a) : ring_scope.
Arguments polyOver_pred _ _ _ /.
Arguments polyOverP {R S p}.
Arguments polyC_inj {R} [x1 x2] eq_x12P.
Arguments eq_poly {R n} [E1] E2 eq_E12.
Arguments monic {R}.
Arguments monic_pred _ _ /.
Arguments monicP {R p}.
Arguments rootP {R p x}.
Arguments rootPf {R p x}.
Arguments rootPt {R p x}.
#[deprecated(since="mathcomp 2.4.0", use=size_polyD)]
Notation size_add := size_polyD (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=size_polyDl)]
Notation size_addl := size_polyDl (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=size_polyMleq)]
Notation size_mul_leq := size_polyMleq (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=size_poly_prod_leq)]
Notation size_prod_leq := size_poly_prod_leq (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=size_poly_exp_leq)]
Notation size_exp_leq := size_poly_exp_leq (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=pchar_poly)]
Notation char_poly := pchar_poly (only parsing).
Section PolynomialTheory.
Variable R : nzRingType.
Implicit Types (a b c x y z : R) (p q r d : {poly R}).
Definition opp_poly_def p := \poly_(i < size p) - p`_i.
Fact opp_poly_key : unit
Proof.
by []. Qed.
Canonical opp_poly_unlockable := [unlockable fun opp_poly].
Fact coef_opp_poly p i : (opp_poly p)`_i = - p`_i.
Proof.
Fact add_polyN : left_inverse 0%:P opp_poly (@add_poly _).
Proof.
HB.instance Definition _ := GRing.Nmodule_isZmodule.Build (polynomial R)
add_polyN.
Lemma coefN p i : (- p)`_i = - p`_i.
Proof.
Lemma coefB p q i : (p - q)`_i = p`_i - q`_i.
Lemma coefMNn p n i : (p *- n)`_i = p`_i *- n.
Lemma polyCN : {morph (@polyC R) : c / - c}.
Proof.
Lemma polyCB : {morph (@polyC R) : a b / a - b}.
Proof.
Lemma size_polyN p : size (- p) = size p.
Lemma lead_coefN p : lead_coef (- p) = - lead_coef p.
Proof.
Lemma size_Msign p n : size ((-1) ^+ n * p) = size p.
Proof.
Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R.
Proof.
Lemma size_XsubC a : size ('X - a%:P) = 2.
Proof.
Lemma lead_coefXsubC a : lead_coef ('X - a%:P) = 1.
Proof.
Lemma polyXsubC_eq0 a : ('X - a%:P == 0) = false.
Proof.
Lemma lead_coefXnsubC n c : 0 < n -> lead_coef ('X^n - c%:P) = 1.
Proof.
Lemma size_XnsubC n c : 0 < n -> size ('X^n - c%:P) = n.+1.
Proof.
#[deprecated(since="mathcomp 2.3.0", use=size_XnsubC)]
Lemma size_Xn_sub_1 n : n > 0 -> size ('X^n - 1 : {poly R}) = n.+1.
Proof.
exact/size_XnsubC. Qed.
Lemma hornerN p x : (- p).[x] = - p.[x].
Lemma hornerXsubC a x : ('X - a%:P).[x] = x - a.
Definition hornerE_comm :=
(hornerD, hornerN, hornerX, hornerC, horner_cons,
simp, hornerCM, hornerZ,
(fun p x => hornerM_comm p (comm_polyX x))).
Fact polyOverNr (zmodS : zmodClosed R) : oppr_closed (polyOver zmodS).
HB.instance Definition _ (zmodS : zmodClosed R) :=
GRing.isOppClosed.Build {poly R} (polyOver_pred zmodS) (@polyOverNr _).
Section PolyOverRing.
Variable S : subringClosed R.
HB.instance Definition _ := GRing.MulClosed.on (polyOver_pred S).
Lemma polyOverXaddC c : ('X + c%:P \in polyOver S) = (c \in S).
Lemma polyOverXnaddC n c : ('X^n + c%:P \is a polyOver S) = (c \in S).
Proof.
Lemma polyOverXsubC c : ('X - c%:P \in polyOver S) = (c \in S).
Lemma polyOverXnsubC n c : ('X^n - c%:P \is a polyOver S) = (c \in S).
Proof.
End PolyOverRing.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact deriv_is_linear : linear (@deriv R)
Proof.
Lemma derivN : {morph deriv : p / - p}.
Proof.
Lemma derivB : {morph deriv : p q / p - q}.
Proof.
Lemma derivXsubC (a : R) : ('X - a%:P)^`() = 1.
Lemma derivMNn n p : (p *- n)^`() = p^`() *- n.
Proof.
Definition derivE := Eval lazy beta delta [morphism_2 morphism_1] in
(derivZ, deriv_mulC, derivC, derivX, derivMXaddC, derivXsubC, derivM, derivB,
derivD, derivN, derivXn, derivM, derivMn).
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact derivn_is_linear n : linear (@derivn R n)
Proof.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact nderivn_is_linear n : linear (@nderivn R n)
Proof.
Lemma derivnB n : {morph derivn n : p q / p - q}.
Proof.
Lemma derivnMNn n m p : (p *- m)^`(n) = p^`(n) *- m.
Proof.
Lemma derivnN n : {morph derivn n : p / - p}.
Proof.
Lemma nderivnB n : {morph nderivn n : p q / p - q}.
Proof.
Lemma nderivnMNn n m p : (p *- m)^`N(n) = p^`N(n) *- m.
Proof.
Lemma nderivnN n : {morph nderivn n : p / - p}.
Proof.
Lemma monicXsubC c : 'X - c%:P \is monic.
Proof.
Lemma monic_prod_XsubC I rI (P : pred I) (F : I -> R) :
\prod_(i <- rI | P i) ('X - (F i)%:P) \is monic.
Proof.
Lemma lead_coef_prod_XsubC I rI (P : pred I) (F : I -> R) :
lead_coef (\prod_(i <- rI | P i) ('X - (F i)%:P)) = 1.
Proof.
Lemma size_prod_XsubC I rI (F : I -> R) :
size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1.
Proof.
elim: rI => [|i r /= <-]; rewrite ?big_nil ?size_poly1 // big_cons.
rewrite size_monicM ?monicXsubC ?monic_neq0 ?monic_prod_XsubC //.
by rewrite size_XsubC.
Qed.
rewrite size_monicM ?monicXsubC ?monic_neq0 ?monic_prod_XsubC //.
by rewrite size_XsubC.
Qed.
Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
Proof.
rewrite -[n]card_ord -prodr_const -big_filter size_prod_XsubC.
by have [e _ _ [_ ->]] := big_enumP.
Qed.
by have [e _ _ [_ ->]] := big_enumP.
Qed.
Lemma monicXnsubC n c : 0 < n -> 'X^n - c%:P \is monic.
Proof.
#[deprecated(since="mathcomp 2.3.0'", use=monicXnsubC)]
Lemma monic_Xn_sub_1 n : n > 0 -> 'X^n - 1 \is @monic R.
Proof.
exact/monicXnsubC. Qed.
Lemma lreg_lead p : GRing.lreg (lead_coef p) -> GRing.lreg p.
Proof.
move/mulrI_eq0=> reg_p; apply: mulrI0_lreg => q; apply/contra_eq => nz_q.
by rewrite -lead_coef_eq0 lead_coef_proper_mul reg_p lead_coef_eq0.
Qed.
by rewrite -lead_coef_eq0 lead_coef_proper_mul reg_p lead_coef_eq0.
Qed.
Lemma rreg_lead p : GRing.rreg (lead_coef p) -> GRing.rreg p.
Proof.
move/mulIr_eq0=> reg_p; apply: mulIr0_rreg => q; apply/contra_eq => nz_q.
by rewrite -lead_coef_eq0 lead_coef_proper_mul reg_p lead_coef_eq0.
Qed.
by rewrite -lead_coef_eq0 lead_coef_proper_mul reg_p lead_coef_eq0.
Qed.
Lemma monic_lreg p : p \is monic -> GRing.lreg p.
Lemma monic_rreg p : p \is monic -> GRing.rreg p.
Lemma rootN p x : root (- p) x = root p x.
Lemma root_XsubC a x : root ('X - a%:P) x = (x == a).
Proof.
Lemma root_XaddC a x : root ('X + a%:P) x = (x == - a).
Proof.
Theorem factor_theorem p a : reflect (exists q, p = q * ('X - a%:P)) (root p a).
Proof.
apply: (iffP eqP) => [pa0 | [q ->]]; last first.
by rewrite hornerM_comm /comm_poly hornerXsubC subrr ?simp.
exists (\poly_(i < size p) horner_rec (drop i.+1 p) a).
apply/polyP=> i; rewrite mulrBr coefB coefMX coefMC !coef_poly.
apply: canRL (addrK _) _; rewrite addrC; have [le_p_i | lt_i_p] := leqP.
rewrite nth_default // !simp drop_oversize ?if_same //.
exact: leq_trans (leqSpred _).
case: i => [|i] in lt_i_p *; last by rewrite ltnW // (drop_nth 0 lt_i_p).
by rewrite drop1 /= -{}pa0 /horner; case: (p : seq R) lt_i_p.
Qed.
by rewrite hornerM_comm /comm_poly hornerXsubC subrr ?simp.
exists (\poly_(i < size p) horner_rec (drop i.+1 p) a).
apply/polyP=> i; rewrite mulrBr coefB coefMX coefMC !coef_poly.
apply: canRL (addrK _) _; rewrite addrC; have [le_p_i | lt_i_p] := leqP.
rewrite nth_default // !simp drop_oversize ?if_same //.
exact: leq_trans (leqSpred _).
case: i => [|i] in lt_i_p *; last by rewrite ltnW // (drop_nth 0 lt_i_p).
by rewrite drop1 /= -{}pa0 /horner; case: (p : seq R) lt_i_p.
Qed.
Lemma multiplicity_XsubC p a :
{m | exists2 q, (p != 0) ==> ~~ root q a & p = q * ('X - a%:P) ^+ m}.
Proof.
have [n le_p_n] := ubnP (size p); elim: n => // n IHn in p le_p_n *.
have [-> | nz_p /=] := eqVneq p 0; first by exists 0, 0; rewrite ?mul0r.
have [/sig_eqW[p1 Dp] | nz_pa] := altP (factor_theorem p a); last first.
by exists 0%N, p; rewrite ?mulr1.
have nz_p1: p1 != 0 by apply: contraNneq nz_p => p1_0; rewrite Dp p1_0 mul0r.
have /IHn[m /sig2_eqW[q nz_qa Dp1]]: size p1 < n.
by rewrite Dp size_Mmonic ?monicXsubC // size_XsubC addn2 in le_p_n.
by exists m.+1, q; [rewrite nz_p1 in nz_qa | rewrite exprSr mulrA -Dp1].
Qed.
have [-> | nz_p /=] := eqVneq p 0; first by exists 0, 0; rewrite ?mul0r.
have [/sig_eqW[p1 Dp] | nz_pa] := altP (factor_theorem p a); last first.
by exists 0%N, p; rewrite ?mulr1.
have nz_p1: p1 != 0 by apply: contraNneq nz_p => p1_0; rewrite Dp p1_0 mul0r.
have /IHn[m /sig2_eqW[q nz_qa Dp1]]: size p1 < n.
by rewrite Dp size_Mmonic ?monicXsubC // size_XsubC addn2 in le_p_n.
by exists m.+1, q; [rewrite nz_p1 in nz_qa | rewrite exprSr mulrA -Dp1].
Qed.
Definition root_of_unity n : pred R := root ('X^n - 1).
Local Notation "n .-unity_root" := (root_of_unity n) : ring_scope.
Lemma unity_rootE n z : n.-unity_root z = (z ^+ n == 1).
Lemma unity_rootP n z : reflect (z ^+ n = 1) (n.-unity_root z).
Proof.
Definition primitive_root_of_unity n z :=
(n > 0) && [forall i : 'I_n, i.+1.-unity_root z == (i.+1 == n)].
Local Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.
Lemma prim_order_exists n z :
n > 0 -> z ^+ n = 1 -> {m | m.-primitive_root z & (m %| n)}.
Proof.
move=> n_gt0 zn1.
have: exists m, (m > 0) && (z ^+ m == 1) by exists n; rewrite n_gt0 /= zn1.
case/ex_minnP=> m /andP[m_gt0 /eqP zm1] m_min.
exists m.
apply/andP; split=> //; apply/eqfunP=> [[i]] /=.
rewrite leq_eqVlt unity_rootE.
case: eqP => [-> _ | _]; first by rewrite zm1 eqxx.
by apply: contraTF => zi1; rewrite -leqNgt m_min.
have: n %% m < m by rewrite ltn_mod.
apply: contraLR; rewrite -lt0n -leqNgt => nm_gt0; apply: m_min.
by rewrite nm_gt0 /= expr_mod ?zn1.
Qed.
have: exists m, (m > 0) && (z ^+ m == 1) by exists n; rewrite n_gt0 /= zn1.
case/ex_minnP=> m /andP[m_gt0 /eqP zm1] m_min.
exists m.
apply/andP; split=> //; apply/eqfunP=> [[i]] /=.
rewrite leq_eqVlt unity_rootE.
case: eqP => [-> _ | _]; first by rewrite zm1 eqxx.
by apply: contraTF => zi1; rewrite -leqNgt m_min.
have: n %% m < m by rewrite ltn_mod.
apply: contraLR; rewrite -lt0n -leqNgt => nm_gt0; apply: m_min.
by rewrite nm_gt0 /= expr_mod ?zn1.
Qed.
Section OnePrimitive.
Variables (n : nat) (z : R).
Hypothesis prim_z : n.-primitive_root z.
Lemma prim_order_gt0 : n > 0
Let n_gt0 := prim_order_gt0.
Lemma prim_expr_order : z ^+ n = 1.
Proof.
Lemma prim_expr_mod i : z ^+ (i %% n) = z ^+ i.
Proof.
Lemma prim_order_dvd i : (n %| i) = (z ^+ i == 1).
Proof.
Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j) = (i == j %[mod n]).
Proof.
wlog le_ji: i j / j <= i.
move=> IH; case: (leqP j i) => [|/ltnW] /IH //.
by rewrite eq_sym (eq_sym (j %% n)%N).
rewrite -{1}(subnKC le_ji) exprD -prim_expr_mod eqn_mod_dvd //.
rewrite prim_order_dvd; apply/eqP/eqP=> [|->]; last by rewrite mulr1.
move/(congr1 ( *%R (z ^+ (n - j %% n)))); rewrite mulrA -exprD.
by rewrite subnK ?prim_expr_order ?mul1r // ltnW ?ltn_mod.
Qed.
move=> IH; case: (leqP j i) => [|/ltnW] /IH //.
by rewrite eq_sym (eq_sym (j %% n)%N).
rewrite -{1}(subnKC le_ji) exprD -prim_expr_mod eqn_mod_dvd //.
rewrite prim_order_dvd; apply/eqP/eqP=> [|->]; last by rewrite mulr1.
move/(congr1 ( *%R (z ^+ (n - j %% n)))); rewrite mulrA -exprD.
by rewrite subnK ?prim_expr_order ?mul1r // ltnW ?ltn_mod.
Qed.
Lemma exp_prim_root k : (n %/ gcdn k n).-primitive_root (z ^+ k).
Proof.
set d := gcdn k n; have d_gt0: (0 < d)%N by rewrite gcdn_gt0 orbC n_gt0.
have [d_dv_k d_dv_n]: (d %| k /\ d %| n)%N by rewrite dvdn_gcdl dvdn_gcdr.
set q := (n %/ d)%N; rewrite /q.-primitive_root ltn_divRL // n_gt0.
apply/forallP=> i; rewrite unity_rootE -exprM -prim_order_dvd.
rewrite -(divnK d_dv_n) -/q -(divnK d_dv_k) mulnAC dvdn_pmul2r //.
apply/eqP; apply/idP/idP=> [|/eqP->]; last by rewrite dvdn_mull.
rewrite Gauss_dvdr; last by rewrite eqn_leq ltn_ord; apply: dvdn_leq.
by rewrite /coprime gcdnC -(eqn_pmul2r d_gt0) mul1n muln_gcdl !divnK.
Qed.
have [d_dv_k d_dv_n]: (d %| k /\ d %| n)%N by rewrite dvdn_gcdl dvdn_gcdr.
set q := (n %/ d)%N; rewrite /q.-primitive_root ltn_divRL // n_gt0.
apply/forallP=> i; rewrite unity_rootE -exprM -prim_order_dvd.
rewrite -(divnK d_dv_n) -/q -(divnK d_dv_k) mulnAC dvdn_pmul2r //.
apply/eqP; apply/idP/idP=> [|/eqP->]; last by rewrite dvdn_mull.
rewrite Gauss_dvdr; last by rewrite eqn_leq ltn_ord; apply: dvdn_leq.
by rewrite /coprime gcdnC -(eqn_pmul2r d_gt0) mul1n muln_gcdl !divnK.
Qed.
Lemma dvdn_prim_root m : (m %| n)%N -> m.-primitive_root (z ^+ (n %/ m)).
Proof.
Lemma prim_root_eq0 : (z == 0) = (n == 0%N).
Proof.
End OnePrimitive.
Lemma prim_root_exp_coprime n z k :
n.-primitive_root z -> n.-primitive_root (z ^+ k) = coprime k n.
Proof.
move=> prim_z; have n_gt0 := prim_order_gt0 prim_z.
apply/idP/idP=> [prim_zk | co_k_n].
set d := gcdn k n; have dv_d_n: (d %| n)%N := dvdn_gcdr _ _.
rewrite /coprime -/d -(eqn_pmul2r n_gt0) mul1n -{2}(gcdnMl n d).
rewrite -{2}(divnK dv_d_n) (mulnC _ d) -muln_gcdr (gcdn_idPr _) //.
rewrite (prim_order_dvd prim_zk) -exprM -(prim_order_dvd prim_z).
by rewrite muln_divCA_gcd dvdn_mulr.
have zkn_1: z ^+ k ^+ n = 1 by rewrite exprAC (prim_expr_order prim_z) expr1n.
have{zkn_1} [m prim_zk dv_m_n]:= prim_order_exists n_gt0 zkn_1.
suffices /eqP <-: m == n by [].
rewrite eqn_dvd dv_m_n -(@Gauss_dvdr n k m) 1?coprime_sym //=.
by rewrite (prim_order_dvd prim_z) exprM (prim_expr_order prim_zk).
Qed.
apply/idP/idP=> [prim_zk | co_k_n].
set d := gcdn k n; have dv_d_n: (d %| n)%N := dvdn_gcdr _ _.
rewrite /coprime -/d -(eqn_pmul2r n_gt0) mul1n -{2}(gcdnMl n d).
rewrite -{2}(divnK dv_d_n) (mulnC _ d) -muln_gcdr (gcdn_idPr _) //.
rewrite (prim_order_dvd prim_zk) -exprM -(prim_order_dvd prim_z).
by rewrite muln_divCA_gcd dvdn_mulr.
have zkn_1: z ^+ k ^+ n = 1 by rewrite exprAC (prim_expr_order prim_z) expr1n.
have{zkn_1} [m prim_zk dv_m_n]:= prim_order_exists n_gt0 zkn_1.
suffices /eqP <-: m == n by [].
rewrite eqn_dvd dv_m_n -(@Gauss_dvdr n k m) 1?coprime_sym //=.
by rewrite (prim_order_dvd prim_z) exprM (prim_expr_order prim_zk).
Qed.
End PolynomialTheory.
Notation "n .-unity_root" := (root_of_unity n) : ring_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.
Arguments unity_rootP {R n z}.
#[deprecated(since="mathcomp 2.4.0", use=size_polyN)]
Notation size_opp := size_polyN (only parsing).
Section MapPoly.
Section Definitions.
Variables (aR rR : nzSemiRingType) (f : aR -> rR).
Definition map_poly (p : {poly aR}) := \poly_(i < size p) f p`_i.
Lemma map_polyE p : map_poly p = Poly (map f p).
Proof.
rewrite /map_poly unlock; congr Poly.
apply: (@eq_from_nth _ 0); rewrite size_mkseq ?size_map // => i lt_i_p.
by rewrite [RHS](nth_map 0) ?nth_mkseq.
Qed.
apply: (@eq_from_nth _ 0); rewrite size_mkseq ?size_map // => i lt_i_p.
by rewrite [RHS](nth_map 0) ?nth_mkseq.
Qed.
Definition commr_rmorph u := forall x, GRing.comm u (f x).
Definition horner_morph u & commr_rmorph u := fun p => (map_poly p).[u].
End Definitions.
Variables aR rR : nzSemiRingType.
Section Combinatorial.
Variables (iR : nzSemiRingType) (f : aR -> rR).
Local Notation "p ^f" := (map_poly f p) : ring_scope.
Lemma map_poly0 : 0^f = 0.
Lemma eq_map_poly (g : aR -> rR) : f =1 g -> map_poly f =1 map_poly g.
Lemma map_poly_id g (p : {poly iR}) :
{in (p : seq iR), g =1 id} -> map_poly g p = p.
Lemma coef_map_id0 p i : f 0 = 0 -> (p^f)`_i = f p`_i.
Proof.
Lemma map_Poly_id0 s : f 0 = 0 -> (Poly s)^f = Poly (map f s).
Proof.
move=> f0; apply/polyP=> j; rewrite coef_map_id0 ?coef_Poly //.
have [/(nth_map 0 0)->// | le_s_j] := ltnP j (size s).
by rewrite !nth_default ?size_map.
Qed.
have [/(nth_map 0 0)->// | le_s_j] := ltnP j (size s).
by rewrite !nth_default ?size_map.
Qed.
Lemma map_poly_comp_id0 (g : iR -> aR) p :
f 0 = 0 -> map_poly (f \o g) p = (map_poly g p)^f.
Proof.
Lemma size_map_poly_id0 p : f (lead_coef p) != 0 -> size p^f = size p.
Proof.
Lemma map_poly_eq0_id0 p : f (lead_coef p) != 0 -> (p^f == 0) = (p == 0).
Proof.
Lemma lead_coef_map_id0 p :
f 0 = 0 -> f (lead_coef p) != 0 -> lead_coef p^f = f (lead_coef p).
Proof.
Hypotheses (inj_f : injective f) (f_0 : f 0 = 0).
Lemma size_map_inj_poly p : size p^f = size p.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite map_poly0 !size_poly0.
by rewrite size_map_poly_id0 // -f_0 (inj_eq inj_f) lead_coef_eq0.
Qed.
by rewrite size_map_poly_id0 // -f_0 (inj_eq inj_f) lead_coef_eq0.
Qed.
Lemma map_inj_poly : injective (map_poly f).
Proof.
Lemma lead_coef_map_inj p : lead_coef p^f = f (lead_coef p).
Proof.
End Combinatorial.
Lemma map_polyK (f : aR -> rR) g :
cancel g f -> f 0 = 0 -> cancel (map_poly g) (map_poly f).
Proof.
Lemma eq_in_map_poly_id0 (f g : aR -> rR) (S : addrClosed aR) :
f 0 = 0 -> g 0 = 0 -> {in S, f =1 g} ->
{in polyOver S, map_poly f =1 map_poly g}.
Proof.
Lemma eq_in_map_poly (f g : {additive aR -> rR}) (S : addrClosed aR) :
{in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}.
Proof.
Section Additive.
Variables (iR : nzSemiRingType) (f : {additive aR -> rR}).
Local Notation "p ^f" := (map_poly f p) : ring_scope.
Lemma coef_map p i : p^f`_i = f p`_i.
Proof.
Lemma map_Poly s : (Poly s)^f = Poly (map f s).
Proof.
Lemma map_poly_comp (g : iR -> aR) p :
map_poly (f \o g) p = map_poly f (map_poly g p).
Proof.
Fact map_poly_is_nmod_morphism : nmod_morphism (map_poly f).
Proof.
GRing.isNmodMorphism.Build {poly aR} {poly rR} (map_poly f)
map_poly_is_nmod_morphism.
Lemma map_polyC a : (a%:P)^f = (f a)%:P.
Lemma lead_coef_map_eq p :
f (lead_coef p) != 0 -> lead_coef p^f = f (lead_coef p).
Proof.
End Additive.
Variable f : {rmorphism aR -> rR}.
Implicit Types p : {poly aR}.
Local Notation "p ^f" := (map_poly f p) : ring_scope.
Fact map_poly_is_monoid_morphism : monoid_morphism (map_poly f).
Proof.
Definition map_poly_is_multiplicative :=
(fun g => (g.2, g.1)) map_poly_is_monoid_morphism.
HB.instance Definition _ :=
GRing.isMonoidMorphism.Build {poly aR} {poly rR} (map_poly f)
map_poly_is_monoid_morphism.
Lemma map_polyZ c p : (c *: p)^f = f c *: p^f.
HB.instance Definition _ :=
GRing.isScalable.Build aR {poly aR} {poly rR} (f \; *:%R) (map_poly f)
map_polyZ.
Lemma map_polyX : ('X)^f = 'X.
Proof.
Lemma map_polyXn n : ('X^n)^f = 'X^n.
Lemma map_polyXaddC x : ('X + x%:P)^f = 'X + (f x)%:P.
Lemma monic_map p : p \is monic -> p^f \is monic.
Proof.
Lemma horner_map p x : p^f.[f x] = f p.[x].
Proof.
elim/poly_ind: p => [|p c IHp]; first by rewrite !(rmorph0, horner0).
rewrite hornerMXaddC !rmorphD !rmorphM /=.
by rewrite map_polyX map_polyC hornerMXaddC IHp.
Qed.
rewrite hornerMXaddC !rmorphD !rmorphM /=.
by rewrite map_polyX map_polyC hornerMXaddC IHp.
Qed.
Lemma map_comm_poly p x : comm_poly p x -> comm_poly p^f (f x).
Proof.
Lemma map_comm_coef p x : comm_coef p x -> comm_coef p^f (f x).
Lemma rmorph_root p x : root p x -> root p^f (f x).
Proof.
Section HornerMorph.
Variable u : rR.
Hypothesis cfu : commr_rmorph f u.
Lemma horner_morphC a : horner_morph cfu a%:P = f a.
Proof.
Lemma horner_morphX : horner_morph cfu 'X = u.
Proof.
Fact horner_is_semilinear : semilinear_for (f \; *%R) (horner_morph cfu).
Proof.
split=> [c p|p q]; rewrite /horner_morph; first by rewrite linearZ hornerZ.
by rewrite linearD hornerD.
Qed.
by rewrite linearD hornerD.
Qed.
Fact horner_is_monoid_morphism : monoid_morphism (horner_morph cfu).
Proof.
split=> [|p q]; first by rewrite /horner_morph rmorph1 hornerC.
rewrite /horner_morph rmorphM /= hornerM_comm //.
by apply: comm_coef_poly => i; rewrite coef_map cfu.
Qed.
rewrite /horner_morph rmorphM /= hornerM_comm //.
by apply: comm_coef_poly => i; rewrite coef_map cfu.
Qed.
Definition horner_is_multiplicative :=
(fun g => (g.2, g.1)) horner_is_monoid_morphism.
HB.instance Definition _ :=
GRing.isSemilinear.Build aR {poly aR} rR _ (horner_morph cfu)
horner_is_semilinear.
HB.instance Definition _ :=
GRing.isMonoidMorphism.Build {poly aR} rR (horner_morph cfu)
horner_is_monoid_morphism.
End HornerMorph.
Lemma deriv_map p : p^f^`() = (p^`())^f.
Proof.
Lemma derivn_map p n : p^f^`(n) = (p^`(n))^f.
Proof.
Lemma nderivn_map p n : p^f^`N(n) = (p^`N(n))^f.
Proof.
End MapPoly.
Section MapPoly.
Variables aR rR : nzRingType.
Variable f : {rmorphism aR -> rR}.
Implicit Types p : {poly aR}.
Local Notation "p ^f" := (map_poly f p) : ring_scope.
#[deprecated(since="mathcomp 2.5.0", use=raddfB)]
Fact map_poly_is_zmod_morphism : zmod_morphism (map_poly f).
Proof.
Fact map_poly_is_additive : zmod_morphism (map_poly f).
Proof.
Lemma map_polyXsubC x : ('X - x%:P)^f = 'X - (f x)%:P.
Lemma map_prod_XsubC I (rI : seq I) P F :
(\prod_(i <- rI | P i) ('X - (F i)%:P))^f =
\prod_(i <- rI | P i) ('X - (f (F i))%:P).
Proof.
Lemma prod_map_poly (ar : seq aR) P :
\prod_(x <- map f ar | P x) ('X - x%:P) =
(\prod_(x <- ar | P (f x)) ('X - x%:P))^f.
Proof.
Lemma rmorph_unity_root n z : n.-unity_root z -> n.-unity_root (f z).
Proof.
move/(rmorph_root f); rewrite rootE rmorphB hornerD hornerN.
by rewrite /= map_polyXn rmorph1 hornerC hornerXn subr_eq0 unity_rootE.
Qed.
by rewrite /= map_polyXn rmorph1 hornerC hornerXn subr_eq0 unity_rootE.
Qed.
Section HornerMorph.
Variable u : rR.
Hypothesis cfu : commr_rmorph f u.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact horner_is_linear : linear_for (f \; *%R) (horner_morph cfu).
Proof.
End HornerMorph.
End MapPoly.
Section HornerAlg.
Variable (R : nzSemiRingType) (A : nzSemiAlgType R).
Section Defs.
Variable a : A.
Lemma in_alg_comm : commr_rmorph (in_alg A) a.
Definition horner_alg := horner_morph in_alg_comm.
Lemma horner_algC c : horner_alg c%:P = c%:A.
Proof.
Lemma horner_algX : horner_alg 'X = a.
Proof.
HB.instance Definition _ := GRing.LRMorphism.on horner_alg.
End Defs.
Variable (pf : {lrmorphism {poly R} -> A}).
Lemma poly_alg_initial : pf =1 horner_alg (pf 'X).
Proof.
apply: poly_ind => [|p a IHp]; first by rewrite !rmorph0.
rewrite !rmorphD !rmorphM /= -{}IHp horner_algC ?horner_algX.
by rewrite -alg_polyC rmorph_alg.
Qed.
rewrite !rmorphD !rmorphM /= -{}IHp horner_algC ?horner_algX.
by rewrite -alg_polyC rmorph_alg.
Qed.
End HornerAlg.
Lemma mapf_root (F : fieldType) (R : nzRingType) (f : {rmorphism F -> R})
(p : {poly F}) (x : F) : root (map_poly f p) (f x) = root p x.
Proof.
Section MorphPoly.
Variable (aR rR : nzSemiRingType) (pf : {rmorphism {poly aR} -> rR}).
Lemma poly_morphX_comm : commr_rmorph (pf \o polyC) (pf 'X).
Proof.
Lemma poly_initial : pf =1 horner_morph poly_morphX_comm.
Proof.
apply: poly_ind => [|p a IHp]; first by rewrite !rmorph0.
by rewrite !rmorphD !rmorphM /= -{}IHp horner_morphC ?horner_morphX.
Qed.
by rewrite !rmorphD !rmorphM /= -{}IHp horner_morphC ?horner_morphX.
Qed.
End MorphPoly.
Notation "p ^:P" := (map_poly polyC p) : ring_scope.
Section PolyCompose.
Variable R : nzSemiRingType.
Implicit Types p q : {poly R}.
Definition comp_poly q p := p^:P.[q].
Local Notation "p \Po q" := (comp_poly q p) : ring_scope.
Lemma size_map_polyC p : size p^:P = size p.
Proof.
Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0).
Proof.
Lemma root_polyC p x : root p^:P x%:P = root p x.
Proof.
Lemma comp_polyE p q : p \Po q = \sum_(i < size p) p`_i *: q^+i.
Proof.
Lemma coef_comp_poly p q n :
(p \Po q)`_n = \sum_(i < size p) p`_i * (q ^+ i)`_n.
Proof.
Lemma polyOver_comp (ringS : semiringClosed R) :
{in polyOver ringS &, forall p q, p \Po q \in polyOver ringS}.
Proof.
move=> p q /polyOverP Sp Sq; rewrite comp_polyE rpred_sum // => i _.
by rewrite polyOverZ ?rpredX.
Qed.
by rewrite polyOverZ ?rpredX.
Qed.
Lemma comp_polyCr p c : p \Po c%:P = p.[c]%:P.
Proof.
Lemma comp_poly0r p : p \Po 0 = (p`_0)%:P.
Proof.
Lemma comp_polyC c p : c%:P \Po p = c%:P.
Fact comp_poly_is_semilinear p : semilinear (comp_poly p).
Proof.
GRing.isSemilinear.Build R {poly R} {poly R} _ (comp_poly p)
(comp_poly_is_semilinear p).
Lemma comp_poly0 p : 0 \Po p = 0.
Proof.
Lemma comp_polyD p q r : (p + q) \Po r = (p \Po r) + (q \Po r).
Proof.
Lemma comp_polyZ c p q : (c *: p) \Po q = c *: (p \Po q).
Proof.
Lemma comp_polyXr p : p \Po 'X = p.
Proof.
Lemma comp_polyX p : 'X \Po p = p.
Lemma comp_poly_MXaddC c p q : (p * 'X + c%:P) \Po q = (p \Po q) * q + c%:P.
Lemma size_comp_poly_leq p q :
size (p \Po q) <= ((size p).-1 * (size q).-1).+1.
Proof.
rewrite comp_polyE (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _.
rewrite (leq_trans (size_scale_leq _ _))//.
rewrite (leq_trans (size_poly_exp_leq _ _))//.
by rewrite ltnS mulnC leq_mul // -{2}(subnKC (valP i)) leq_addr.
Qed.
rewrite (leq_trans (size_scale_leq _ _))//.
rewrite (leq_trans (size_poly_exp_leq _ _))//.
by rewrite ltnS mulnC leq_mul // -{2}(subnKC (valP i)) leq_addr.
Qed.
Lemma comp_Xn_poly p n : 'X^n \Po p = p ^+ n.
Proof.
Lemma coef_comp_poly_Xn p n i : 0 < n ->
(p \Po 'X^n)`_i = if n %| i then p`_(i %/ n) else 0.
Proof.
move=> n_gt0; rewrite comp_polyE; under eq_bigr do rewrite -exprM mulnC.
rewrite coef_sumMXn/=; case: dvdnP => [[j ->]|nD]; last first.
by rewrite big1// => j /eqP ?; case: nD; exists j.
under eq_bigl do rewrite eqn_mul2r gtn_eqF//.
by rewrite big_ord1_eq if_nth ?leqVgt ?mulnK.
Qed.
rewrite coef_sumMXn/=; case: dvdnP => [[j ->]|nD]; last first.
by rewrite big1// => j /eqP ?; case: nD; exists j.
under eq_bigl do rewrite eqn_mul2r gtn_eqF//.
by rewrite big_ord1_eq if_nth ?leqVgt ?mulnK.
Qed.
Lemma comp_poly_Xn p n : 0 < n ->
p \Po 'X^n = \poly_(i < size p * n) if n %| i then p`_(i %/ n) else 0.
Proof.
End PolyCompose.
Notation "p \Po q" := (comp_poly q p) : ring_scope.
Lemma map_comp_poly (aR rR : nzRingType) (f : {rmorphism aR -> rR}) p q :
map_poly f (p \Po q) = map_poly f p \Po map_poly f q.
Proof.
elim/poly_ind: p => [|p a IHp]; first by rewrite !raddf0.
rewrite comp_poly_MXaddC !rmorphD !rmorphM /= !map_polyC map_polyX.
by rewrite comp_poly_MXaddC -IHp.
Qed.
rewrite comp_poly_MXaddC !rmorphD !rmorphM /= !map_polyC map_polyX.
by rewrite comp_poly_MXaddC -IHp.
Qed.
Section IdomainPrimRoot.
Variables (R : idomainType) (n : nat) (z : R).
Hypothesis prim_z : n.-primitive_root z.
Import prime.
Let n_gt0 := prim_order_gt0 prim_z.
Lemma prim_root_pcharF p : (p %| n)%N -> (p \in [pchar R]) = false.
Proof.
move=> pn; apply: contraTF isT => pchar_p; have p_prime := pcharf_prime pchar_p.
have /dvdnP[[|k] n_eq_kp] := pn; first by rewrite n_eq_kp in (n_gt0).
have /eqP := prim_expr_order prim_z; rewrite n_eq_kp exprM.
rewrite -pFrobenius_autE -(pFrobenius_aut1 pchar_p) -subr_eq0 -rmorphB/=.
rewrite pFrobenius_autE expf_eq0// prime_gt0//= subr_eq0.
rewrite -(prim_order_dvd prim_z) n_eq_kp mulnC -dvdn_divRL// divnn/= dvdn1.
by case: ltngtP (prime_gt1 p_prime).
Qed.
have /dvdnP[[|k] n_eq_kp] := pn; first by rewrite n_eq_kp in (n_gt0).
have /eqP := prim_expr_order prim_z; rewrite n_eq_kp exprM.
rewrite -pFrobenius_autE -(pFrobenius_aut1 pchar_p) -subr_eq0 -rmorphB/=.
rewrite pFrobenius_autE expf_eq0// prime_gt0//= subr_eq0.
rewrite -(prim_order_dvd prim_z) n_eq_kp mulnC -dvdn_divRL// divnn/= dvdn1.
by case: ltngtP (prime_gt1 p_prime).
Qed.
Lemma pchar_prim_root : [pchar R]^'.-nat n.
Proof.
Lemma prim_root_pi_eq0 m : \pi(n).-nat m -> m%:R != 0 :> R.
Proof.
Lemma prim_root_dvd_eq0 m : (m %| n)%N -> m%:R != 0 :> R.
Proof.
case: m => [|m mn]; first by rewrite dvd0n gtn_eqF.
by rewrite prim_root_pi_eq0 ?(sub_in_pnat (in1W (pi_of_dvd mn _))) ?pnat_pi.
Qed.
by rewrite prim_root_pi_eq0 ?(sub_in_pnat (in1W (pi_of_dvd mn _))) ?pnat_pi.
Qed.
Lemma prim_root_natf_neq0 : n%:R != 0 :> R.
Proof.
End IdomainPrimRoot.
#[deprecated(since="mathcomp 2.4.0", use=prim_root_pcharF)]
Notation prim_root_charF := prim_root_pcharF (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=pchar_prim_root)]
Notation char_prim_root := pchar_prim_root (only parsing).
Section PolyCompose.
Variable R : nzRingType.
Implicit Types p q : {poly R}.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact comp_poly_is_linear p : linear (comp_poly p)
Proof.
Lemma comp_polyB p q r : (p - q) \Po r = (p \Po r) - (q \Po r).
Proof.
Lemma comp_polyXaddC_K p z : (p \Po ('X + z%:P)) \Po ('X - z%:P) = p.
Proof.
have addzK: ('X + z%:P) \Po ('X - z%:P) = 'X.
by rewrite raddfD /= comp_polyC comp_polyX subrK.
elim/poly_ind: p => [|p c IHp]; first by rewrite !comp_poly0.
rewrite comp_poly_MXaddC linearD /= comp_polyC {1}/comp_poly rmorphM /=.
by rewrite hornerM_comm /comm_poly -!/(_ \Po _) ?IHp ?addzK ?commr_polyX.
Qed.
by rewrite raddfD /= comp_polyC comp_polyX subrK.
elim/poly_ind: p => [|p c IHp]; first by rewrite !comp_poly0.
rewrite comp_poly_MXaddC linearD /= comp_polyC {1}/comp_poly rmorphM /=.
by rewrite hornerM_comm /comm_poly -!/(_ \Po _) ?IHp ?addzK ?commr_polyX.
Qed.
End PolyCompose.
Section Surgery.
Variable R : nzSemiRingType.
Implicit Type p q : {poly R}.
Definition even_poly p : {poly R} := \poly_(i < uphalf (size p)) p`_i.*2.
Lemma size_even_poly p : size (even_poly p) <= uphalf (size p).
Proof.
Lemma coef_even_poly p i : (even_poly p)`_i = p`_i.*2.
Proof.
Lemma even_polyE s p : size p <= s.*2 -> even_poly p = \poly_(i < s) p`_i.*2.
Proof.
move=> pLs2; apply/polyP => i; rewrite coef_even_poly !coef_poly if_nth //.
by case: ltnP => //= ?; rewrite (leq_trans pLs2) ?leq_double.
Qed.
by case: ltnP => //= ?; rewrite (leq_trans pLs2) ?leq_double.
Qed.
Lemma size_even_poly_eq p : odd (size p) ->
size (even_poly p) = uphalf (size p).
Proof.
move=> p_even; rewrite size_poly_eq// double_pred odd_uphalfK//=.
by rewrite lead_coef_eq0 -size_poly_eq0; case: size p_even.
Qed.
by rewrite lead_coef_eq0 -size_poly_eq0; case: size p_even.
Qed.
Lemma even_polyD p q : even_poly (p + q) = even_poly p + even_poly q.
Proof.
Lemma even_polyZ k p : even_poly (k *: p) = k *: even_poly p.
Proof.
HB.instance Definition _ :=
GRing.isSemilinear.Build R {poly R} {poly R} _ even_poly
(even_polyZ, even_polyD).
Lemma even_polyC (c : R) : even_poly c%:P = c%:P.
Proof.
Definition odd_poly p : {poly R} := \poly_(i < (size p)./2) p`_i.*2.+1.
Lemma size_odd_poly p : size (odd_poly p) <= (size p)./2.
Proof.
Lemma coef_odd_poly p i : (odd_poly p)`_i = p`_i.*2.+1.
Proof.
Lemma odd_polyE s p :
size p <= s.*2.+1 -> odd_poly p = \poly_(i < s) p`_i.*2.+1.
Proof.
move=> pLs2; apply/polyP => i; rewrite coef_odd_poly !coef_poly if_nth //.
by case: ltnP => //= ?; rewrite (leq_trans pLs2) ?ltnS ?leq_double.
Qed.
by case: ltnP => //= ?; rewrite (leq_trans pLs2) ?ltnS ?leq_double.
Qed.
Lemma odd_polyC (c : R) : odd_poly c%:P = 0.
Proof.
Lemma odd_polyD p q : odd_poly (p + q) = odd_poly p + odd_poly q.
Proof.
Lemma odd_polyZ k p : odd_poly (k *: p) = k *: odd_poly p.
Proof.
HB.instance Definition _ :=
GRing.isSemilinear.Build R {poly R} {poly R} _ odd_poly
(odd_polyZ, odd_polyD).
Lemma size_odd_poly_eq p : ~~ odd (size p) -> size (odd_poly p) = (size p)./2.
Proof.
have [->|p_neq0] := eqVneq p 0; first by rewrite odd_polyC size_poly0.
move=> p_odd; rewrite size_poly_eq// -subn1 doubleB subn2 even_halfK//.
rewrite prednK ?lead_coef_eq0// ltn_predRL.
by move: p_neq0 p_odd; rewrite -size_poly_eq0; case: (size p) => [|[]].
Qed.
move=> p_odd; rewrite size_poly_eq// -subn1 doubleB subn2 even_halfK//.
rewrite prednK ?lead_coef_eq0// ltn_predRL.
by move: p_neq0 p_odd; rewrite -size_poly_eq0; case: (size p) => [|[]].
Qed.
Lemma odd_polyMX p : odd_poly (p * 'X) = even_poly p.
Proof.
Lemma even_polyMX p : even_poly (p * 'X) = odd_poly p * 'X.
Proof.
Lemma sum_even_poly p :
\sum_(i < size p | ~~ odd i) p`_i *: 'X^i = even_poly p \Po 'X^2.
Proof.
apply/polyP => i; rewrite coef_comp_poly_Xn// coef_sumMXn coef_even_poly.
rewrite (big_ord1_cond_eq _ _ (negb \o _))/= -dvdn2 andbC -muln2.
by case: dvdnP => //= -[k ->]; rewrite mulnK// if_nth ?leqVgt.
Qed.
rewrite (big_ord1_cond_eq _ _ (negb \o _))/= -dvdn2 andbC -muln2.
by case: dvdnP => //= -[k ->]; rewrite mulnK// if_nth ?leqVgt.
Qed.
Lemma sum_odd_poly p :
\sum_(i < size p | odd i) p`_i *: 'X^i = (odd_poly p \Po 'X^2) * 'X.
Proof.
apply/polyP => i; rewrite coefMX coef_comp_poly_Xn// coef_sumMXn coef_odd_poly/=.
case: i => [|i]//=; first by rewrite big_andbC big1// => -[[|j]//].
rewrite big_ord1_cond_eq/= -dvdn2 andbC -muln2.
by case: dvdnP => //= -[k ->]; rewrite mulnK// if_nth ?leqVgt.
Qed.
case: i => [|i]//=; first by rewrite big_andbC big1// => -[[|j]//].
rewrite big_ord1_cond_eq/= -dvdn2 andbC -muln2.
by case: dvdnP => //= -[k ->]; rewrite mulnK// if_nth ?leqVgt.
Qed.
Lemma poly_even_odd p : even_poly p \Po 'X^2 + (odd_poly p \Po 'X^2) * 'X = p.
Proof.
Definition take_poly m p := \poly_(i < m) p`_i.
Lemma size_take_poly m p : size (take_poly m p) <= m.
Proof.
Lemma coef_take_poly m p i : (take_poly m p)`_i = if i < m then p`_i else 0.
Proof.
Lemma take_poly_id m p : size p <= m -> take_poly m p = p.
Proof.
Lemma take_polyD m p q : take_poly m (p + q) = take_poly m p + take_poly m q.
Lemma take_polyZ k m p : take_poly m (k *: p) = k *: take_poly m p.
HB.instance Definition _ m := GRing.isSemilinear.Build R {poly R} {poly R} _
(take_poly m) (take_polyZ^~ m, take_polyD m).
Lemma take_poly_sum m I r P (p : I -> {poly R}) :
take_poly m (\sum_(i <- r | P i) p i) = \sum_(i <- r| P i) take_poly m (p i).
Proof.
Lemma take_poly0l p : take_poly 0 p = 0.
Proof.
Lemma take_poly0r m : take_poly m 0 = 0.
Proof.
Lemma take_polyMXn m n p : take_poly m (p * 'X^n) = take_poly (m - n) p * 'X^n.
Proof.
have [->|/eqP p_neq0] := p =P 0; first by rewrite !(mul0r, take_poly0r).
apply/polyP => i; rewrite !(coef_take_poly, coefMXn).
by have [iLn|nLi] := leqP n i; rewrite ?if_same// ltn_sub2rE.
Qed.
apply/polyP => i; rewrite !(coef_take_poly, coefMXn).
by have [iLn|nLi] := leqP n i; rewrite ?if_same// ltn_sub2rE.
Qed.
Lemma take_polyMXn_0 n p : take_poly n (p * 'X^n) = 0.
Proof.
Lemma take_polyDMXn n p q : size p <= n -> take_poly n (p + q * 'X^n) = p.
Proof.
Definition drop_poly m p := \poly_(i < size p - m) p`_(i + m).
Lemma coef_drop_poly m p i : (drop_poly m p)`_i = p`_(i + m).
Lemma drop_poly_eq0 m p : size p <= m -> drop_poly m p = 0.
Proof.
Lemma size_drop_poly n p : size (drop_poly n p) = (size p - n)%N.
Proof.
have [pLn|nLp] := leqP (size p) n.
by rewrite (eqP pLn) drop_poly_eq0 ?size_poly0.
have p_neq0 : p != 0 by rewrite -size_poly_gt0 (leq_trans _ nLp).
by rewrite size_poly_eq// predn_sub subnK ?lead_coef_eq0// -ltnS -polySpred.
Qed.
by rewrite (eqP pLn) drop_poly_eq0 ?size_poly0.
have p_neq0 : p != 0 by rewrite -size_poly_gt0 (leq_trans _ nLp).
by rewrite size_poly_eq// predn_sub subnK ?lead_coef_eq0// -ltnS -polySpred.
Qed.
Lemma sum_drop_poly n p :
\sum_(n <= i < size p) p`_i *: 'X^i = drop_poly n p * 'X^n.
Proof.
Lemma drop_polyD m p q : drop_poly m (p + q) = drop_poly m p + drop_poly m q.
Proof.
Lemma drop_polyZ k m p : drop_poly m (k *: p) = k *: drop_poly m p.
Proof.
HB.instance Definition _ m := GRing.isSemilinear.Build R {poly R} {poly R} _
(drop_poly m) (drop_polyZ^~ m, drop_polyD m).
Lemma drop_poly_sum m I r P (p : I -> {poly R}) :
drop_poly m (\sum_(i <- r | P i) p i) = \sum_(i <- r | P i) drop_poly m (p i).
Proof.
Lemma drop_poly0l p : drop_poly 0 p = p.
Lemma drop_poly0r m : drop_poly m 0 = 0
Proof.
Lemma drop_polyMXn m n p :
drop_poly m (p * 'X^n) = drop_poly (m - n) p * 'X^(n - m).
Proof.
Lemma drop_polyMXn_id n p : drop_poly n (p * 'X^ n) = p.
Proof.
Lemma drop_polyDMXn n p q : size p <= n -> drop_poly n (p + q * 'X^n) = q.
Proof.
Lemma poly_take_drop n p : take_poly n p + drop_poly n p * 'X^n = p.
Proof.
apply/polyP => i; rewrite coefD coefMXn coef_take_poly coef_drop_poly.
by case: ltnP => ni; rewrite ?addr0 ?add0r//= subnK.
Qed.
by case: ltnP => ni; rewrite ?addr0 ?add0r//= subnK.
Qed.
Lemma eqp_take_drop n p q :
take_poly n p = take_poly n q -> drop_poly n p = drop_poly n q -> p = q.
Proof.
End Surgery.
Section Surgery.
Variable R : nzRingType.
Implicit Type p q : {poly R}.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact even_poly_is_linear : linear (@even_poly R)
Proof.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact odd_poly_is_linear : linear (@odd_poly R)
Proof.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact take_poly_is_linear m : linear (@take_poly R m).
Proof.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact drop_poly_is_linear m : linear (@drop_poly R m).
Proof.
End Surgery.
Definition coefE :=
(coef0, coef1, coefC, coefX, coefXn, coef_sumMXn,
coefZ, coefMC, coefCM, coefXnM, coefMXn, coefXM, coefMX, coefMNn, coefMn,
coefN, coefB, coefD, coef_even_poly, coef_odd_poly,
coef_take_poly, coef_drop_poly, coef_cons, coef_Poly, coef_poly,
coef_deriv, coef_nderivn, coef_derivn, coef_map, coef_sum,
coef_comp_poly_Xn, coef_comp_poly).
Section PolynomialComNzSemiRing.
Variable R : comNzSemiRingType.
Implicit Types p q : {poly R}.
Fact poly_mul_comm p q : p * q = q * p.
HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build {poly R}
poly_mul_comm.
HB.instance Definition _ :=
GRing.LSemiAlgebra_isComSemiAlgebra.Build R {poly R}.
Lemma hornerM p q x : (p * q).[x] = p.[x] * q.[x].
Proof.
Fact horner_eval_is_monoid_morphism (x : R) : monoid_morphism (horner_eval x).
Proof.
Definition horner_eval_is_multiplicative x :=
(fun g => (g.2, g.1)) (horner_eval_is_monoid_morphism x).
HB.instance Definition _ x :=
GRing.isMonoidMorphism.Build {poly R} R (horner_eval x)
(horner_eval_is_monoid_morphism x).
Lemma horner_exp p x n : (p ^+ n).[x] = p.[x] ^+ n.
Proof.
Lemma horner_prod I r (P : pred I) (F : I -> {poly R}) x :
(\prod_(i <- r | P i) F i).[x] = \prod_(i <- r | P i) (F i).[x].
Proof.
Definition hornerE :=
(hornerD, hornerN, hornerX, hornerC, horner_exp,
simp, hornerCM, hornerZ, hornerM, horner_cons).
Fact comp_poly_is_monoid_morphism q : monoid_morphism (comp_poly q).
Proof.
split=> [|p1 p2]; first by rewrite comp_polyC.
by rewrite /comp_poly rmorphM hornerM_comm //; apply: mulrC.
Qed.
by rewrite /comp_poly rmorphM hornerM_comm //; apply: mulrC.
Qed.
Definition comp_poly_multiplicative q :=
(fun g => (g.2, g.1)) (comp_poly_is_monoid_morphism q).
HB.instance Definition _ q := GRing.isMonoidMorphism.Build _ _ (comp_poly q)
(comp_poly_is_monoid_morphism q).
Lemma comp_polyM p q r : (p * q) \Po r = (p \Po r) * (q \Po r).
Proof.
Lemma comp_polyA p q r : p \Po (q \Po r) = (p \Po q) \Po r.
Proof.
elim/poly_ind: p => [|p c IHp]; first by rewrite !comp_polyC.
by rewrite !comp_polyD !comp_polyM !comp_polyX IHp !comp_polyC.
Qed.
by rewrite !comp_polyD !comp_polyM !comp_polyX IHp !comp_polyC.
Qed.
Lemma horner_comp p q x : (p \Po q).[x] = p.[q.[x]].
Proof.
Lemma root_comp p q x : root (p \Po q) x = root p (q.[x]).
Proof.
Lemma deriv_comp p q : (p \Po q) ^`() = (p ^`() \Po q) * q^`().
Proof.
elim/poly_ind: p => [|p c IHp]; first by rewrite !(deriv0, comp_poly0) mul0r.
rewrite comp_poly_MXaddC derivD derivC derivM IHp derivMXaddC comp_polyD.
by rewrite comp_polyM comp_polyX addr0 addrC mulrAC -mulrDl.
Qed.
rewrite comp_poly_MXaddC derivD derivC derivM IHp derivMXaddC comp_polyD.
by rewrite comp_polyM comp_polyX addr0 addrC mulrAC -mulrDl.
Qed.
Lemma deriv_exp p n : (p ^+ n)^`() = p^`() * p ^+ n.-1 *+ n.
Proof.
Definition derivCE := (derivE, deriv_exp).
End PolynomialComNzSemiRing.
Section PolynomialComNzRing.
Variable R : comNzRingType.
Implicit Types p q : {poly R}.
HB.instance Definition _ := GRing.NzRing.on {poly R}.
Lemma coef_prod_XsubC (ps : seq R) (n : nat) :
(n <= size ps)%N ->
(\prod_(p <- ps) ('X - p%:P))`_n =
(-1) ^+ (size ps - n)%N *
\sum_(I in {set 'I_(size ps)} | #|I| == (size ps - n)%N)
\prod_(i in I) ps`_i.
Proof.
move=> nle.
under eq_bigr => i _ do rewrite addrC -raddfN/=.
rewrite -{1}(in_tupleE ps) -(map_tnth_enum (_ ps)) big_map.
rewrite enumT bigA_distr /= coef_sum.
transitivity (\sum_(I in {set 'I_(size ps)}) if #|I| == (size ps - n)%N then
\prod_(i < size ps | i \in I) - ps`_i else 0).
apply eq_bigr => I _.
rewrite big_if/= big_const iter_mulr_1 -rmorph_prod/= coefCM coefXn.
under eq_bigr => i _ do rewrite (tnth_nth 0)/=.
rewrite -[#|I| == _](eqn_add2r n) subnK//.
rewrite -[X in (_ + _)%N == X]card_ord -(cardC I) eqn_add2l.
by case: ifP; rewrite ?mulr1 ?mulr0.
by rewrite -big_mkcond mulr_sumr/=; apply: eq_bigr => I /eqP <-; rewrite prodrN.
Qed.
under eq_bigr => i _ do rewrite addrC -raddfN/=.
rewrite -{1}(in_tupleE ps) -(map_tnth_enum (_ ps)) big_map.
rewrite enumT bigA_distr /= coef_sum.
transitivity (\sum_(I in {set 'I_(size ps)}) if #|I| == (size ps - n)%N then
\prod_(i < size ps | i \in I) - ps`_i else 0).
apply eq_bigr => I _.
rewrite big_if/= big_const iter_mulr_1 -rmorph_prod/= coefCM coefXn.
under eq_bigr => i _ do rewrite (tnth_nth 0)/=.
rewrite -[#|I| == _](eqn_add2r n) subnK//.
rewrite -[X in (_ + _)%N == X]card_ord -(cardC I) eqn_add2l.
by case: ifP; rewrite ?mulr1 ?mulr0.
by rewrite -big_mkcond mulr_sumr/=; apply: eq_bigr => I /eqP <-; rewrite prodrN.
Qed.
Lemma coefPn_prod_XsubC (ps : seq R) : size ps != 0 ->
(\prod_(p <- ps) ('X - p%:P))`_((size ps).-1) = - \sum_(p <- ps) p.
Proof.
rewrite coef_prod_XsubC ?leq_pred// => ps0.
have -> : (size ps - (size ps).-1 = 1)%N.
by move: ps0; case: (size ps) => // n _; exact: subSnn.
rewrite expr1 mulN1r; congr GRing.opp.
set f : 'I_(size ps) -> {set 'I_(size ps)} := fun a => [set a].
transitivity (\sum_(I in imset f (mem setT)) \prod_(i in I) ps`_i).
apply: congr_big => // I /=.
by apply/cards1P/imsetP => [[a ->] | [a _ ->]]; exists a.
rewrite big_imset/=.
by move=> i j _ _ ij; apply/set1P; rewrite -/(f j) -ij set11.
rewrite -[in RHS](in_tupleE ps) -(map_tnth_enum (_ ps)) big_map enumT.
apply: congr_big => // i; first exact: in_setT.
by rewrite big_set1 (tnth_nth 0).
Qed.
have -> : (size ps - (size ps).-1 = 1)%N.
by move: ps0; case: (size ps) => // n _; exact: subSnn.
rewrite expr1 mulN1r; congr GRing.opp.
set f : 'I_(size ps) -> {set 'I_(size ps)} := fun a => [set a].
transitivity (\sum_(I in imset f (mem setT)) \prod_(i in I) ps`_i).
apply: congr_big => // I /=.
by apply/cards1P/imsetP => [[a ->] | [a _ ->]]; exists a.
rewrite big_imset/=.
by move=> i j _ _ ij; apply/set1P; rewrite -/(f j) -ij set11.
rewrite -[in RHS](in_tupleE ps) -(map_tnth_enum (_ ps)) big_map enumT.
apply: congr_big => // i; first exact: in_setT.
by rewrite big_set1 (tnth_nth 0).
Qed.
Lemma coef0_prod_XsubC (ps : seq R) :
(\prod_(p <- ps) ('X - p%:P))`_0 = (-1) ^+ (size ps) * \prod_(p <- ps) p.
Proof.
rewrite coef_prod_XsubC// subn0; congr GRing.mul.
transitivity (\sum_(I in [set setT : {set 'I_(size ps)}]) \prod_(i in I) ps`_i).
apply: congr_big =>// i/=.
apply/idP/set1P => [/eqP cardE | ->]; last by rewrite cardsT card_ord.
by apply/eqP; rewrite eqEcard subsetT cardsT card_ord cardE leqnn.
rewrite big_set1 -[in RHS](in_tupleE ps) -(map_tnth_enum (_ ps)) big_map enumT.
apply: congr_big => // i; first exact: in_setT.
by rewrite (tnth_nth 0).
Qed.
transitivity (\sum_(I in [set setT : {set 'I_(size ps)}]) \prod_(i in I) ps`_i).
apply: congr_big =>// i/=.
apply/idP/set1P => [/eqP cardE | ->]; last by rewrite cardsT card_ord.
by apply/eqP; rewrite eqEcard subsetT cardsT card_ord cardE leqnn.
rewrite big_set1 -[in RHS](in_tupleE ps) -(map_tnth_enum (_ ps)) big_map enumT.
apply: congr_big => // i; first exact: in_setT.
by rewrite (tnth_nth 0).
Qed.
#[deprecated(since="mathcomp 2.5.0", use=linearP)]
Fact horner_eval_is_linear x : linear_for *%R (@horner_eval R x).
Proof.
End PolynomialComNzRing.
Section PolynomialIdomain.
Variable R : idomainType.
Implicit Types (a b x y : R) (p q r m : {poly R}).
Lemma size_mul p q : p != 0 -> q != 0 -> size (p * q) = (size p + size q).-1.
Proof.
Fact poly_idomainAxiom p q : p * q = 0 -> (p == 0) || (q == 0).
Proof.
Definition poly_unit : pred {poly R} :=
fun p => (size p == 1) && (p`_0 \in GRing.unit).
Definition poly_inv p := if p \in poly_unit then (p`_0)^-1%:P else p.
Fact poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}.
Proof.
Fact poly_intro_unit p q : q * p = 1 -> p \in poly_unit.
Proof.
move=> pq1; apply/andP; split; last first.
apply/unitrP; exists q`_0.
by rewrite 2!mulrC -!/(coefp 0 _) -rmorphM pq1 rmorph1.
have: size (q * p) == 1 by rewrite pq1 size_poly1.
have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 size_poly0.
have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r size_poly0.
rewrite size_mul // (polySpred nz_p) (polySpred nz_q) addnS addSn !eqSS.
by rewrite addn_eq0 => /andP[].
Qed.
apply/unitrP; exists q`_0.
by rewrite 2!mulrC -!/(coefp 0 _) -rmorphM pq1 rmorph1.
have: size (q * p) == 1 by rewrite pq1 size_poly1.
have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 size_poly0.
have [-> | nz_q] := eqVneq q 0; first by rewrite mul0r size_poly0.
rewrite size_mul // (polySpred nz_p) (polySpred nz_q) addnS addSn !eqSS.
by rewrite addn_eq0 => /andP[].
Qed.
Fact poly_inv_out : {in [predC poly_unit], poly_inv =1 id}.
HB.instance Definition _ := GRing.ComNzRing_hasMulInverse.Build (polynomial R)
poly_mulVp poly_intro_unit poly_inv_out.
HB.instance Definition _ := GRing.ComUnitRing_isIntegral.Build (polynomial R)
poly_idomainAxiom.
Lemma poly_unitE p :
(p \in GRing.unit) = (size p == 1) && (p`_0 \in GRing.unit).
Proof.
by []. Qed.
Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p`_0)^-1%:P else p.
Proof.
by []. Qed.
Lemma polyCV c : c%:P^-1 = (c^-1)%:P.
Proof.
Lemma rootM p q x : root (p * q) x = root p x || root q x.
Lemma rootZ x a p : a != 0 -> root (a *: p) x = root p x.
Lemma root_exp p n a: comm_poly p a -> (0 < n)%N -> root (p ^+ n) a = root p a.
Proof.
Lemma size_scale a p : a != 0 -> size (a *: p) = size p.
Lemma size_Cmul a p : a != 0 -> size (a%:P * p) = size p.
Proof.
Lemma lead_coefM p q : lead_coef (p * q) = lead_coef p * lead_coef q.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite !(mul0r, lead_coef0).
have [-> | nz_q] := eqVneq q 0; first by rewrite !(mulr0, lead_coef0).
by rewrite lead_coef_proper_mul // mulf_neq0 ?lead_coef_eq0.
Qed.
have [-> | nz_q] := eqVneq q 0; first by rewrite !(mulr0, lead_coef0).
by rewrite lead_coef_proper_mul // mulf_neq0 ?lead_coef_eq0.
Qed.
Lemma lead_coef_prod I rI (P : {pred I}) (p : I -> {poly R}) :
lead_coef (\prod_(i <- rI | P i) p i) = \prod_(i <- rI | P i) lead_coef (p i).
Proof.
Lemma lead_coefZ a p : lead_coef (a *: p) = a * lead_coef p.
Proof.
Lemma scale_poly_eq0 a p : (a *: p == 0) = (a == 0) || (p == 0).
Lemma size_prod (I : finType) (P : pred I) (F : I -> {poly R}) :
(forall i, P i -> F i != 0) ->
size (\prod_(i | P i) F i) = ((\sum_(i | P i) size (F i)).+1 - #|P|)%N.
Proof.
move=> nzF; transitivity (\sum_(i | P i) (size (F i)).-1).+1; last first.
apply: canRL (addKn _) _; rewrite addnS -sum1_card -big_split /=.
by congr _.+1; apply: eq_bigr => i /nzF/polySpred.
elim/big_rec2: _ => [|i d p /nzF nzFi IHp]; first by rewrite size_poly1.
by rewrite size_mul // -?size_poly_eq0 IHp // addnS polySpred.
Qed.
apply: canRL (addKn _) _; rewrite addnS -sum1_card -big_split /=.
by congr _.+1; apply: eq_bigr => i /nzF/polySpred.
elim/big_rec2: _ => [|i d p /nzF nzFi IHp]; first by rewrite size_poly1.
by rewrite size_mul // -?size_poly_eq0 IHp // addnS polySpred.
Qed.
Lemma size_prod_seq (I : eqType) (s : seq I) (F : I -> {poly R}) :
(forall i, i \in s -> F i != 0) ->
size (\prod_(i <- s) F i) = ((\sum_(i <- s) size (F i)).+1 - size s)%N.
Proof.
Lemma size_mul_eq1 p q : (size (p * q) == 1) = ((size p == 1) && (size q == 1)).
Proof.
have [->|pNZ] := eqVneq p 0; first by rewrite mul0r size_poly0.
have [->|qNZ] := eqVneq q 0; first by rewrite mulr0 size_poly0 andbF.
rewrite size_mul //.
by move: pNZ qNZ; rewrite -!size_poly_gt0; (do 2 case: size) => //= n [|[|]].
Qed.
have [->|qNZ] := eqVneq q 0; first by rewrite mulr0 size_poly0 andbF.
rewrite size_mul //.
by move: pNZ qNZ; rewrite -!size_poly_gt0; (do 2 case: size) => //= n [|[|]].
Qed.
Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) :
reflect (forall i, P i && (i \in s) -> size (F i) = 1)
(size (\prod_(i <- s | P i) F i) == 1%N).
Proof.
rewrite (big_morph _ (id1:=true) size_mul_eq1) ?size_polyC ?oner_neq0//.
rewrite big_all_cond; apply/(iffP allP).
by move=> h i /andP[Pi ins]; apply/eqP/(implyP (h i ins) Pi).
by move=> h i ins; apply/implyP => Pi; rewrite h ?Pi.
Qed.
rewrite big_all_cond; apply/(iffP allP).
by move=> h i /andP[Pi ins]; apply/eqP/(implyP (h i ins) Pi).
by move=> h i ins; apply/implyP => Pi; rewrite h ?Pi.
Qed.
Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) :
reflect (forall i, P i -> size (F i) = 1)
(size (\prod_(i | P i) F i) == 1).
Proof.
apply: (iffP (size_prod_seq_eq1 _ _ _)) => Hi i.
by move=> Pi; apply: Hi; rewrite Pi /= mem_index_enum.
by rewrite mem_index_enum andbT; apply: Hi.
Qed.
by move=> Pi; apply: Hi; rewrite Pi /= mem_index_enum.
by rewrite mem_index_enum andbT; apply: Hi.
Qed.
Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N.
Proof.
Lemma lead_coef_exp p n : lead_coef (p ^+ n) = lead_coef p ^+ n.
Proof.
Lemma root_prod_XsubC rs x :
root (\prod_(a <- rs) ('X - a%:P)) x = (x \in rs).
Proof.
Lemma root_exp_XsubC n a x : root (('X - a%:P) ^+ n.+1) x = (x == a).
Proof.
Lemma size_comp_poly p q :
(size (p \Po q)).-1 = ((size p).-1 * (size q).-1)%N.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite comp_poly0 size_poly0.
have [/size1_polyC-> | nc_q] := leqP (size q) 1.
by rewrite comp_polyCr !size_polyC -!sub1b -!subnS muln0.
have nz_q: q != 0 by rewrite -size_poly_eq0 -(subnKC nc_q).
rewrite mulnC comp_polyE (polySpred nz_p) /= big_ord_recr /= addrC.
rewrite size_polyDl size_scale ?lead_coef_eq0 ?size_exp //=.
rewrite [ltnRHS]polySpred ?expf_neq0 // ltnS size_exp.
rewrite (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _.
rewrite (leq_trans (size_scale_leq _ _)) // polySpred ?expf_neq0 //.
by rewrite size_exp -(subnKC nc_q) ltn_pmul2l.
Qed.
have [/size1_polyC-> | nc_q] := leqP (size q) 1.
by rewrite comp_polyCr !size_polyC -!sub1b -!subnS muln0.
have nz_q: q != 0 by rewrite -size_poly_eq0 -(subnKC nc_q).
rewrite mulnC comp_polyE (polySpred nz_p) /= big_ord_recr /= addrC.
rewrite size_polyDl size_scale ?lead_coef_eq0 ?size_exp //=.
rewrite [ltnRHS]polySpred ?expf_neq0 // ltnS size_exp.
rewrite (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _.
rewrite (leq_trans (size_scale_leq _ _)) // polySpred ?expf_neq0 //.
by rewrite size_exp -(subnKC nc_q) ltn_pmul2l.
Qed.
Lemma lead_coef_comp p q : size q > 1 ->
lead_coef (p \Po q) = (lead_coef p) * lead_coef q ^+ (size p).-1.
Proof.
move=> q_gt1; rewrite !lead_coefE coef_comp_poly size_comp_poly.
have [->|nz_p] := eqVneq p 0; first by rewrite size_poly0 big_ord0 coef0 mul0r.
rewrite polySpred //= big_ord_recr /= big1 ?add0r => [i _|]; last first.
by rewrite -!lead_coefE -lead_coef_exp !lead_coefE size_exp mulnC.
rewrite [X in _ * X]nth_default ?mulr0 ?(leq_trans (size_poly_exp_leq _ _)) //.
by rewrite mulnC ltn_mul2r -subn1 subn_gt0 q_gt1 /=.
Qed.
have [->|nz_p] := eqVneq p 0; first by rewrite size_poly0 big_ord0 coef0 mul0r.
rewrite polySpred //= big_ord_recr /= big1 ?add0r => [i _|]; last first.
by rewrite -!lead_coefE -lead_coef_exp !lead_coefE size_exp mulnC.
rewrite [X in _ * X]nth_default ?mulr0 ?(leq_trans (size_poly_exp_leq _ _)) //.
by rewrite mulnC ltn_mul2r -subn1 subn_gt0 q_gt1 /=.
Qed.
Lemma comp_poly_eq0 p q : size q > 1 -> (p \Po q == 0) = (p == 0).
Proof.
move=> sq_gt1; rewrite -!lead_coef_eq0 lead_coef_comp //.
rewrite mulf_eq0 expf_eq0 !lead_coef_eq0 -[q == 0]size_poly_leq0.
by rewrite [_ <= 0]leqNgt (leq_ltn_trans _ sq_gt1) ?andbF ?orbF.
Qed.
rewrite mulf_eq0 expf_eq0 !lead_coef_eq0 -[q == 0]size_poly_leq0.
by rewrite [_ <= 0]leqNgt (leq_ltn_trans _ sq_gt1) ?andbF ?orbF.
Qed.
Lemma size_comp_poly2 p q : size q = 2 -> size (p \Po q) = size p.
Proof.
move=> sq2; have [->|pN0] := eqVneq p 0; first by rewrite comp_polyC.
by rewrite polySpred ?size_comp_poly ?comp_poly_eq0 ?sq2 // muln1 polySpred.
Qed.
by rewrite polySpred ?size_comp_poly ?comp_poly_eq0 ?sq2 // muln1 polySpred.
Qed.
Lemma comp_poly2_eq0 p q : size q = 2 -> (p \Po q == 0) = (p == 0).
Proof.
Theorem max_poly_roots p rs :
p != 0 -> all (root p) rs -> uniq rs -> size rs < size p.
Proof.
elim: rs p => [p pn0 _ _ | r rs ihrs p pn0] /=; first by rewrite size_poly_gt0.
case/andP => rpr arrs /andP [rnrs urs]; case/factor_theorem: rpr => q epq.
have [q0 | ?] := eqVneq q 0; first by move: pn0; rewrite epq q0 mul0r eqxx.
have -> : size p = (size q).+1.
by rewrite epq size_Mmonic ?monicXsubC // size_XsubC addnC.
suff /eq_in_all h : {in rs, root q =1 root p} by apply: ihrs => //; rewrite h.
move=> x xrs; rewrite epq rootM root_XsubC orbC; case: (eqVneq x r) => // exr.
by move: rnrs; rewrite -exr xrs.
Qed.
case/andP => rpr arrs /andP [rnrs urs]; case/factor_theorem: rpr => q epq.
have [q0 | ?] := eqVneq q 0; first by move: pn0; rewrite epq q0 mul0r eqxx.
have -> : size p = (size q).+1.
by rewrite epq size_Mmonic ?monicXsubC // size_XsubC addnC.
suff /eq_in_all h : {in rs, root q =1 root p} by apply: ihrs => //; rewrite h.
move=> x xrs; rewrite epq rootM root_XsubC orbC; case: (eqVneq x r) => // exr.
by move: rnrs; rewrite -exr xrs.
Qed.
Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs -> uniq rs ->
(size rs >= size p)%N -> p = 0.
Proof.
End PolynomialIdomain.
HB.instance Definition _ (R : countNzSemiRingType) :=
[Countable of polynomial R by <:].
HB.instance Definition _ (R : countNzRingType) :=
[Countable of polynomial R by <:].
HB.instance Definition _ (R : countComNzSemiRingType) :=
[Countable of polynomial R by <:].
HB.instance Definition _ (R : countComNzRingType) :=
[Countable of polynomial R by <:].
HB.instance Definition _ (R : countIdomainType) :=
[Countable of polynomial R by <:].
Section MapFieldPoly.
Variables (F : fieldType) (R : nzRingType) (f : {rmorphism F -> R}).
Local Notation "p ^f" := (map_poly f p) : ring_scope.
Lemma size_map_poly p : size p^f = size p.
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite rmorph0 !size_poly0.
by rewrite size_poly_eq // fmorph_eq0 // lead_coef_eq0.
Qed.
by rewrite size_poly_eq // fmorph_eq0 // lead_coef_eq0.
Qed.
Lemma lead_coef_map p : lead_coef p^f = f (lead_coef p).
Proof.
have [-> | nz_p] := eqVneq p 0; first by rewrite !(rmorph0, lead_coef0).
by rewrite lead_coef_map_eq // fmorph_eq0 // lead_coef_eq0.
Qed.
by rewrite lead_coef_map_eq // fmorph_eq0 // lead_coef_eq0.
Qed.
Lemma map_poly_eq0 p : (p^f == 0) = (p == 0).
Proof.
Lemma map_poly_inj : injective (map_poly f).
Proof.
move=> p q eqfpq; apply/eqP; rewrite -subr_eq0 -map_poly_eq0.
by rewrite rmorphB /= eqfpq subrr.
Qed.
by rewrite rmorphB /= eqfpq subrr.
Qed.
Lemma map_monic p : (p^f \is monic) = (p \is monic).
Proof.
Lemma map_poly_com p x : comm_poly p^f (f x).
Proof.
Lemma fmorph_root p x : root p^f (f x) = root p x.
Proof.
Lemma fmorph_unity_root n z : n.-unity_root (f z) = n.-unity_root z.
Proof.
Lemma fmorph_primitive_root n z :
n.-primitive_root (f z) = n.-primitive_root z.
Proof.
End MapFieldPoly.
Arguments map_poly_inj {F R} f [p1 p2] : rename.
Section MaxRoots.
Variable R : unitRingType.
Implicit Types (x y : R) (rs : seq R) (p : {poly R}).
Definition diff_roots (x y : R) := (x * y == y * x) && (y - x \in GRing.unit).
Fixpoint uniq_roots rs :=
if rs is x :: rs' then all (diff_roots x) rs' && uniq_roots rs' else true.
Lemma uniq_roots_prod_XsubC p rs :
all (root p) rs -> uniq_roots rs ->
exists q, p = q * \prod_(z <- rs) ('X - z%:P).
Proof.
elim: rs => [|z rs IHrs] /=; first by rewrite big_nil; exists p; rewrite mulr1.
case/andP=> rpz rprs /andP[drs urs]; case: IHrs => {urs rprs}// q def_p.
have [|q' def_q] := factor_theorem q z _; last first.
by exists q'; rewrite big_cons mulrA -def_q.
rewrite {p}def_p in rpz.
elim/last_ind: rs drs rpz => [|rs t IHrs] /=; first by rewrite big_nil mulr1.
rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs{}IHrs].
rewrite -cats1 big_cat big_seq1 /= mulrA rootE hornerM_comm.
by rewrite /comm_poly hornerXsubC mulrBl mulrBr czt.
rewrite hornerXsubC -opprB mulrN oppr_eq0 -(mul0r (t - z)).
by rewrite (inj_eq (mulIr Uzt)) => /IHrs.
Qed.
case/andP=> rpz rprs /andP[drs urs]; case: IHrs => {urs rprs}// q def_p.
have [|q' def_q] := factor_theorem q z _; last first.
by exists q'; rewrite big_cons mulrA -def_q.
rewrite {p}def_p in rpz.
elim/last_ind: rs drs rpz => [|rs t IHrs] /=; first by rewrite big_nil mulr1.
rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs{}IHrs].
rewrite -cats1 big_cat big_seq1 /= mulrA rootE hornerM_comm.
by rewrite /comm_poly hornerXsubC mulrBl mulrBr czt.
rewrite hornerXsubC -opprB mulrN oppr_eq0 -(mul0r (t - z)).
by rewrite (inj_eq (mulIr Uzt)) => /IHrs.
Qed.
Theorem max_ring_poly_roots p rs :
p != 0 -> all (root p) rs -> uniq_roots rs -> size rs < size p.
Proof.
move=> nz_p _ /(@uniq_roots_prod_XsubC p)[// | q def_p]; rewrite def_p in nz_p *.
have nz_q: q != 0 by apply: contraNneq nz_p => ->; rewrite mul0r.
rewrite size_Mmonic ?monic_prod_XsubC // (polySpred nz_q) addSn /=.
by rewrite size_prod_XsubC leq_addl.
Qed.
have nz_q: q != 0 by apply: contraNneq nz_p => ->; rewrite mul0r.
rewrite size_Mmonic ?monic_prod_XsubC // (polySpred nz_q) addSn /=.
by rewrite size_prod_XsubC leq_addl.
Qed.
Lemma all_roots_prod_XsubC p rs :
size p = (size rs).+1 -> all (root p) rs -> uniq_roots rs ->
p = lead_coef p *: \prod_(z <- rs) ('X - z%:P).
Proof.
move=> size_p /uniq_roots_prod_XsubC def_p Urs.
case/def_p: Urs => q -> {p def_p} in size_p *.
have [q0 | nz_q] := eqVneq q 0; first by rewrite q0 mul0r size_poly0 in size_p.
have{q nz_q size_p} /size_poly1P[c _ ->]: size q == 1.
rewrite -(eqn_add2r (size rs)) add1n -size_p.
by rewrite size_Mmonic ?monic_prod_XsubC // size_prod_XsubC addnS.
by rewrite lead_coef_Mmonic ?monic_prod_XsubC // lead_coefC mul_polyC.
Qed.
case/def_p: Urs => q -> {p def_p} in size_p *.
have [q0 | nz_q] := eqVneq q 0; first by rewrite q0 mul0r size_poly0 in size_p.
have{q nz_q size_p} /size_poly1P[c _ ->]: size q == 1.
rewrite -(eqn_add2r (size rs)) add1n -size_p.
by rewrite size_Mmonic ?monic_prod_XsubC // size_prod_XsubC addnS.
by rewrite lead_coef_Mmonic ?monic_prod_XsubC // lead_coefC mul_polyC.
Qed.
End MaxRoots.
Section FieldRoots.
Variable F : fieldType.
Implicit Types (p : {poly F}) (rs : seq F).
Lemma poly2_root p : size p = 2 -> {r | root p r}.
Proof.
Lemma uniq_rootsE rs : uniq_roots rs = uniq rs.
Proof.
Lemma root_ZXsubC (a b r : F) : a != 0 ->
root (a *: 'X - b%:P) r = (r == b / a).
Proof.
Section UnityRoots.
Variable n : nat.
Lemma max_unity_roots rs :
n > 0 -> all n.-unity_root rs -> uniq rs -> size rs <= n.
Proof.
move=> n_gt0 rs_n_1 Urs; have szPn := size_XnsubC (1 : F) n_gt0.
by rewrite -ltnS -szPn max_poly_roots -?size_poly_eq0 ?szPn.
Qed.
by rewrite -ltnS -szPn max_poly_roots -?size_poly_eq0 ?szPn.
Qed.
Lemma mem_unity_roots rs :
n > 0 -> all n.-unity_root rs -> uniq rs -> size rs = n ->
n.-unity_root =i rs.
Proof.
Variable z : F.
Hypothesis prim_z : n.-primitive_root z.
Let zn := [seq z ^+ i | i <- index_iota 0 n].
Lemma factor_Xn_sub_1 : \prod_(0 <= i < n) ('X - (z ^+ i)%:P) = 'X^n - 1.
Proof.
transitivity (\prod_(w <- zn) ('X - w%:P)); first by rewrite big_map.
have n_gt0: n > 0 := prim_order_gt0 prim_z.
rewrite (@all_roots_prod_XsubC _ ('X^n - 1) zn).
- by rewrite size_XnsubC // size_map size_iota subn0.
- apply/allP=> _ /mapP[i _ ->] /=; rewrite rootE !hornerE.
by rewrite exprAC (prim_expr_order prim_z) expr1n subrr.
- rewrite uniq_rootsE map_inj_in_uniq ?iota_uniq // => i j.
rewrite !mem_index_iota => ltin ltjn /eqP.
by rewrite (eq_prim_root_expr prim_z) !modn_small // => /eqP.
by rewrite (monicP (monicXnsubC 1 n_gt0)) scale1r.
Qed.
have n_gt0: n > 0 := prim_order_gt0 prim_z.
rewrite (@all_roots_prod_XsubC _ ('X^n - 1) zn).
- by rewrite size_XnsubC // size_map size_iota subn0.
- apply/allP=> _ /mapP[i _ ->] /=; rewrite rootE !hornerE.
by rewrite exprAC (prim_expr_order prim_z) expr1n subrr.
- rewrite uniq_rootsE map_inj_in_uniq ?iota_uniq // => i j.
rewrite !mem_index_iota => ltin ltjn /eqP.
by rewrite (eq_prim_root_expr prim_z) !modn_small // => /eqP.
by rewrite (monicP (monicXnsubC 1 n_gt0)) scale1r.
Qed.
Lemma prim_rootP x : x ^+ n = 1 -> {i : 'I_n | x = z ^+ i}.
Proof.
move=> xn1; pose logx := [pred i : 'I_n | x == z ^+ i].
case: (pickP logx) => [i /eqP-> | no_i]; first by exists i.
case: notF; suffices{no_i}: x \in zn.
case/mapP=> i; rewrite mem_index_iota => lt_i_n def_x.
by rewrite -(no_i (Ordinal lt_i_n)) /= -def_x.
rewrite -root_prod_XsubC big_map factor_Xn_sub_1.
by rewrite [root _ x]unity_rootE xn1.
Qed.
case: (pickP logx) => [i /eqP-> | no_i]; first by exists i.
case: notF; suffices{no_i}: x \in zn.
case/mapP=> i; rewrite mem_index_iota => lt_i_n def_x.
by rewrite -(no_i (Ordinal lt_i_n)) /= -def_x.
rewrite -root_prod_XsubC big_map factor_Xn_sub_1.
by rewrite [root _ x]unity_rootE xn1.
Qed.
End UnityRoots.
End FieldRoots.
Section MapPolyRoots.
Variables (F : fieldType) (R : unitRingType) (f : {rmorphism F -> R}).
Lemma map_diff_roots x y : diff_roots (f x) (f y) = (x != y).
Proof.
rewrite /diff_roots -rmorphB // fmorph_unit // subr_eq0 //.
by rewrite rmorph_comm // eqxx eq_sym.
Qed.
by rewrite rmorph_comm // eqxx eq_sym.
Qed.
Lemma map_uniq_roots s : uniq_roots (map f s) = uniq s.
Proof.
elim: s => //= x s ->; congr (_ && _); elim: s => //= y s ->.
by rewrite map_diff_roots -negb_or.
Qed.
by rewrite map_diff_roots -negb_or.
Qed.
End MapPolyRoots.
Section AutPolyRoot.
Variable F : fieldType.
Implicit Types u v : {rmorphism F -> F}.
Lemma aut_prim_rootP u z n :
n.-primitive_root z -> {k | coprime k n & u z = z ^+ k}.
Proof.
move=> prim_z; have:= prim_z; rewrite -(fmorph_primitive_root u) => prim_uz.
have [[k _] /= def_uz] := prim_rootP prim_z (prim_expr_order prim_uz).
by exists k; rewrite // -(prim_root_exp_coprime _ prim_z) -def_uz.
Qed.
have [[k _] /= def_uz] := prim_rootP prim_z (prim_expr_order prim_uz).
by exists k; rewrite // -(prim_root_exp_coprime _ prim_z) -def_uz.
Qed.
Lemma aut_unity_rootP u z n : n > 0 -> z ^+ n = 1 -> {k | u z = z ^+ k}.
Proof.
Lemma aut_unity_rootC u v z n : n > 0 -> z ^+ n = 1 -> u (v z) = v (u z).
Proof.
move=> n_gt0 /(aut_unity_rootP _ n_gt0) def_z.
have [[i def_uz] [j def_vz]] := (def_z u, def_z v).
by rewrite def_vz def_uz !rmorphXn /= def_vz def_uz exprAC.
Qed.
have [[i def_uz] [j def_vz]] := (def_z u, def_z v).
by rewrite def_vz def_uz !rmorphXn /= def_vz def_uz exprAC.
Qed.
End AutPolyRoot.
Module UnityRootTheory.
Notation "n .-unity_root" := (root_of_unity n) : unity_root_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : unity_root_scope.
Open Scope unity_root_scope.
Definition unity_rootE := unity_rootE.
Definition unity_rootP := @unity_rootP.
Arguments unity_rootP {R n z}.
Definition prim_order_exists := prim_order_exists.
Notation prim_order_gt0 := prim_order_gt0.
Notation prim_expr_order := prim_expr_order.
Definition prim_expr_mod := prim_expr_mod.
Definition prim_order_dvd := prim_order_dvd.
Definition eq_prim_root_expr := eq_prim_root_expr.
Definition rmorph_unity_root := rmorph_unity_root.
Definition fmorph_unity_root := fmorph_unity_root.
Definition fmorph_primitive_root := fmorph_primitive_root.
Definition max_unity_roots := max_unity_roots.
Definition mem_unity_roots := mem_unity_roots.
Definition prim_rootP := prim_rootP.
End UnityRootTheory.
Module Export Pdeg2.
Module Export Field.
Section Pdeg2Field.
Variable F : fieldType.
Hypothesis nz2 : 2 != 0 :> F.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let pneq0 : p != 0
Proof.
Proof.
Proof.
Proof.
Let aa4 : 4 * a * a = (2 * a)^+2.
Let splitr (x : F) : x = x / 2 + x / 2.
Let pE : p = a *: 'X^2 + b *: 'X + c%:P.
Proof.
Let delta := b ^+ 2 - 4 * a * c.
Lemma deg2_poly_canonical :
p = a *: (('X + (b / (2 * a))%:P)^+2 - (delta / (4 * a ^+ 2))%:P).
Proof.
rewrite pE sqrrD -!addrA scalerDr; congr +%R; rewrite addrA scalerDr; congr +%R.
- rewrite -mulrDr -polyCD -!mul_polyC mulrA mulrAC -polyCM.
by rewrite [a * _]mulrC mulrDl invfM -!mulrA mulVf// mulr1 -splitr.
- rewrite [a ^+ 2]expr2 mulrA aa4 -polyC_exp -polyCB expr_div_n -mulrBl subKr.
by rewrite scale_polyC mulrCA mulrACA aa4 mulrCA mulfV// mulr1.
Qed.
- rewrite -mulrDr -polyCD -!mul_polyC mulrA mulrAC -polyCM.
by rewrite [a * _]mulrC mulrDl invfM -!mulrA mulVf// mulr1 -splitr.
- rewrite [a ^+ 2]expr2 mulrA aa4 -polyC_exp -polyCB expr_div_n -mulrBl subKr.
by rewrite scale_polyC mulrCA mulrACA aa4 mulrCA mulfV// mulr1.
Qed.
Variable r : F.
Hypothesis r_sqrt_delta : r ^+ 2 = delta.
Let r1 := (- b - r) / (2 * a).
Let r2 := (- b + r) / (2 * a).
Lemma deg2_poly_factor : p = a *: ('X - r1%:P) * ('X - r2%:P).
Proof.
Lemma deg2_poly_root1 : root p r1.
Proof.
apply/factor_theorem.
by exists (a *: ('X - r2%:P)); rewrite deg2_poly_factor -!scalerAl mulrC.
Qed.
by exists (a *: ('X - r2%:P)); rewrite deg2_poly_factor -!scalerAl mulrC.
Qed.
Lemma deg2_poly_root2 : root p r2.
Proof.
End Pdeg2Field.
End Field.
Module FieldMonic.
Section Pdeg2FieldMonic.
Variable F : fieldType.
Hypothesis nz2 : 2 != 0 :> F.
Variable p : {poly F}.
Hypothesis degp : size p = 3.
Hypothesis monicp : p \is monic.
Let a := p`_2.
Let b := p`_1.
Let c := p`_0.
Let a1 : a = 1
Proof.
Let delta := b ^+ 2 - 4 * c.
Lemma deg2_poly_canonical : p = (('X + (b / 2)%:P)^+2 - (delta / 4)%:P).
Variable r : F.
Hypothesis r_sqrt_delta : r ^+ 2 = delta.
Let r1 := (- b - r) / 2.
Let r2 := (- b + r) / 2.
Lemma deg2_poly_factor : p = ('X - r1%:P) * ('X - r2%:P).
Lemma deg2_poly_root1 : root p r1.
Proof.
Lemma deg2_poly_root2 : root p r2.
Proof.
End Pdeg2FieldMonic.
End FieldMonic.
End Pdeg2.
Section DecField.
Variable F : decFieldType.
Lemma dec_factor_theorem (p : {poly F}) :
{s : seq F & {q : {poly F} | p = q * \prod_(x <- s) ('X - x%:P)
/\ (q != 0 -> forall x, ~~ root q x)}}.
Proof.
pose polyT (p : seq F) := (foldr (fun c f => f * 'X_0 + c%:T) (0%R)%:T p)%T.
have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x].
by rewrite /horner; elim: (val q) => //= ? ? ->.
have [n] := ubnP (size p); elim: n => // n IHn in p *.
have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T).
case: ifP => [_ /sig_eqW[x]|_ noroot]; last first.
exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x.
by apply/negP=> /rootP rpx; apply: noroot; exists x; rewrite eval_polyT.
rewrite eval_polyT => /rootP/factor_theorem/sig_eqW[p1 ->].
have [->|nz_p1] := eqVneq p1 0; first by exists [::], 0; rewrite !mul0r eqxx.
rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 => /IHn[s [q [-> irr_q]]].
by exists (rcons s x), q; rewrite -cats1 big_cat big_seq1 mulrA.
Qed.
have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x].
by rewrite /horner; elim: (val q) => //= ? ? ->.
have [n] := ubnP (size p); elim: n => // n IHn in p *.
have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T).
case: ifP => [_ /sig_eqW[x]|_ noroot]; last first.
exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x.
by apply/negP=> /rootP rpx; apply: noroot; exists x; rewrite eval_polyT.
rewrite eval_polyT => /rootP/factor_theorem/sig_eqW[p1 ->].
have [->|nz_p1] := eqVneq p1 0; first by exists [::], 0; rewrite !mul0r eqxx.
rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 => /IHn[s [q [-> irr_q]]].
by exists (rcons s x), q; rewrite -cats1 big_cat big_seq1 mulrA.
Qed.
End DecField.
Module PreClosedField.
Section UseAxiom.
Variable F : fieldType.
Hypothesis closedF : GRing.closed_field_axiom F.
Implicit Type p : {poly F}.
Lemma closed_rootP p : reflect (exists x, root p x) (size p != 1).
Proof.
have [-> | nz_p] := eqVneq p 0.
by rewrite size_poly0; left; exists 0; rewrite root0.
rewrite neq_ltn [in _ < 1]polySpred //=.
apply: (iffP idP) => [p_gt1 | [a]]; last exact: root_size_gt1.
pose n := (size p).-1; have n_gt0: n > 0 by rewrite -ltnS -polySpred.
have [a Dan] := closedF (fun i => - p`_i / lead_coef p) n_gt0.
exists a; apply/rootP; rewrite horner_coef polySpred // big_ord_recr /= -/n.
rewrite {}Dan mulr_sumr -big_split big1 //= => i _.
by rewrite -!mulrA mulrCA mulNr mulVKf ?subrr ?lead_coef_eq0.
Qed.
by rewrite size_poly0; left; exists 0; rewrite root0.
rewrite neq_ltn [in _ < 1]polySpred //=.
apply: (iffP idP) => [p_gt1 | [a]]; last exact: root_size_gt1.
pose n := (size p).-1; have n_gt0: n > 0 by rewrite -ltnS -polySpred.
have [a Dan] := closedF (fun i => - p`_i / lead_coef p) n_gt0.
exists a; apply/rootP; rewrite horner_coef polySpred // big_ord_recr /= -/n.
rewrite {}Dan mulr_sumr -big_split big1 //= => i _.
by rewrite -!mulrA mulrCA mulNr mulVKf ?subrr ?lead_coef_eq0.
Qed.
Lemma closed_nonrootP p : reflect (exists x, ~~ root p x) (p != 0).
Proof.
apply: (iffP idP) => [nz_p | [x]]; last first.
by apply: contraNneq => ->; apply: root0.
have [[x /rootP p1x0]|] := altP (closed_rootP (p - 1)).
by exists x; rewrite -[p](subrK 1) /root hornerD p1x0 add0r hornerC oner_eq0.
rewrite negbK => /size_poly1P[c _ /(canRL (subrK 1)) Dp].
by exists 0; rewrite Dp -raddfD polyC_eq0 rootC in nz_p *.
Qed.
by apply: contraNneq => ->; apply: root0.
have [[x /rootP p1x0]|] := altP (closed_rootP (p - 1)).
by exists x; rewrite -[p](subrK 1) /root hornerD p1x0 add0r hornerC oner_eq0.
rewrite negbK => /size_poly1P[c _ /(canRL (subrK 1)) Dp].
by exists 0; rewrite Dp -raddfD polyC_eq0 rootC in nz_p *.
Qed.
End UseAxiom.
End PreClosedField.
Section ClosedField.
Variable F : closedFieldType.
Implicit Type p : {poly F}.
Let closedF := @solve_monicpoly F.
Lemma closed_rootP p : reflect (exists x, root p x) (size p != 1).
Proof.
Lemma closed_nonrootP p : reflect (exists x, ~~ root p x) (p != 0).
Proof.
Lemma closed_field_poly_normal p :
{r : seq F | p = lead_coef p *: \prod_(z <- r) ('X - z%:P)}.
Proof.
apply: sig_eqW; have [r [q [->]]] /= := dec_factor_theorem p.
have [->|] := eqVneq; first by exists [::]; rewrite mul0r lead_coef0 scale0r.
have [[x rqx ? /(_ isT x) /negP /(_ rqx)] //|] := altP (closed_rootP q).
rewrite negbK => /size_poly1P [c c_neq0-> _ _]; exists r.
rewrite mul_polyC lead_coefZ (monicP _) ?mulr1 //.
by rewrite monic_prod => // i; rewrite monicXsubC.
Qed.
have [->|] := eqVneq; first by exists [::]; rewrite mul0r lead_coef0 scale0r.
have [[x rqx ? /(_ isT x) /negP /(_ rqx)] //|] := altP (closed_rootP q).
rewrite negbK => /size_poly1P [c c_neq0-> _ _]; exists r.
rewrite mul_polyC lead_coefZ (monicP _) ?mulr1 //.
by rewrite monic_prod => // i; rewrite monicXsubC.
Qed.
End ClosedField.