# Library mathcomp.algebra.poly

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop finset tuple.
From mathcomp Require Import div ssralg countalg binomial.
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 (big endian representation); the coefficient type R must have a canonical ringType structure cR. In fact {poly R} denotes the concrete type polynomial cR; R is just a phantom argument that lets type inference reconstruct the (hidden) ringType structure cR. 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) 0, 1, - p, p + q, == the usual ring operations: {poly R} has a canonical p * q, p ^+ n, ... ringType structure, which is commutative / integral when R is commutative / integral, respectively. 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 function mapping p to p. [u]; this function can only be used for u in a commutative ring, so it is always a linear ring morphism from {poly R} to R. horner_alg a == given a in some R-algebra A, the function evaluating a polynomial p at a; it is always a linear ring 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.
Declare Scope unity_root_scope.
Import GRing.Theory.
Local Open Scope ring_scope.
Reserved Notation "{ 'poly' T }" (at level 0, format "{ 'poly' T }").
Reserved Notation "c %:P" (at level 2, format "c %:P").
Reserved Notation "p ^:P" (at level 2, format "p ^:P").
Reserved Notation "'X" (at level 0).
Reserved Notation "''X^' n" (at level 3, n at level 2, format "''X^' n").
Reserved Notation "\poly_ ( i < n ) E"
(at level 36, 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 )" (at level 8, format "p ^`N ( n )").
Reserved Notation "n .-unity_root" (at level 2, format "n .-unity_root").
Reserved Notation "n .-primitive_root"
(at level 2, format "n .-primitive_root").
Local Notation simp := Monoid.simpm.
Section Polynomial.
Variable R : semiRingType.
Defines a polynomial as a sequence with <> 0 last element
Record polynomial := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}.
Lemma poly_inj : injective polyseq.
Definition coefp i (p : polynomial) := p`_i.
End Polynomial.
We need to break off the section here to let the Bind Scope directives take effect.
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 : semiRingType.
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.
Definition poly_nil := @Polynomial R [::] (oner_neq0 R).
Definition polyC c : {poly R} := insubd poly_nil [:: c].
Local Notation "c %:P" := (polyC c).
Remember the boolean (c != 0) is coerced to 1 if true and 0 if false
Lemma polyseqC c : c%:P = nseq (c != 0) c :> seq R.
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.
Extensional interpretation (poly <=> nat -> R)
Lemma polyP p q : nth 0 p =1 nth 0 q ↔ p = q.
Lemma size1_polyC p : size p ≤ 1 → p = (p`_0)%:P.
Builds a polynomial by extension.
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.
Lemma size_cons_poly c p :
size (cons_poly c p) = (if nilp p && (c == 0) then 0 else (size p).+1).
Lemma coef_cons c p i : (cons_poly c p)`_i = if i == 0 then c else p`_i.-1.
Build a polynomial directly from a list of coefficients.
Definition Poly := foldr cons_poly 0%:P.
Lemma PolyK c s : last c s != 0 → Poly s = s :> seq R.
Lemma polyseqK p : Poly p = p.
Lemma size_Poly s : size (Poly s) ≤ size s.
Lemma coef_Poly s i : (Poly s)`_i = s`_i.
Build a polynomial from an infinite sequence of coefficients and a bound.
Definition poly_expanded_def n E := Poly (mkseq E n).
Fact poly_key : unit.
Definition poly := locked_with poly_key poly_expanded_def.
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.
Lemma size_poly n E : size (\poly_(i < n) E i) ≤ n.
Lemma size_poly_eq n E : E n.-1 != 0 → size (\poly_(i < n) E i) = n.
Lemma coef_poly n E k : (\poly_(i < n) E i)`_k = (if k < n then E k else 0).
Lemma lead_coef_poly n E :
n > 0 → E n.-1 != 0 → lead_coef (\poly_(i < n) E i) = E n.-1.
Lemma coefK p : \poly_(i < size p) p`_i = p.
Nmodule structure for polynomial
Definition add_poly_def p q := \poly_(i < maxn (size p) (size q)) (p`_i + q`_i).
Fact add_poly_key : unit.
Definition add_poly := locked_with add_poly_key add_poly_def.
Canonical add_poly_unlockable := [unlockable fun add_poly].
Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
Fact add_polyA : associative add_poly.
Fact add_polyC : commutative add_poly.
Fact add_poly0 : left_id 0%:P add_poly.
Properties of the zero polynomial
Lemma polyC0 : 0%:P = 0 :> {poly R}.
Lemma polyseq0 : (0 : {poly R}) = [::] :> seq R.
Lemma size_poly0 : size (0 : {poly R}) = 0%N.
Lemma coef0 i : (0 : {poly R})`_i = 0.
Lemma lead_coef0 : lead_coef 0 = 0 :> R.
Lemma size_poly_eq0 p : (size p == 0) = (p == 0).
Lemma size_poly_leq0 p : (size p ≤ 0) = (p == 0).
Lemma size_poly_leq0P p : reflect (p = 0) (size p ≤ 0).
Lemma size_poly_gt0 p : (0 < size p) = (p != 0).
Lemma gt_size_poly_neq0 p n : (size p > n)%N → p != 0.
Lemma nil_poly p : nilp p = (p == 0).
Lemma poly0Vpos p : {p = 0} + {size p > 0}.
Lemma polySpred p : p != 0 → size p = (size p).-1.+1.
Lemma lead_coef_eq0 p : (lead_coef p == 0) = (p == 0).
Lemma polyC_eq0 (c : R) : (c%:P == 0) = (c == 0).
Lemma size_poly1P p : reflect (exists2 c, c != 0 & p = c%:P) (size p == 1).
Lemma size_polyC_leq1 (c : R) : (size c%:P ≤ 1)%N.
Lemma leq_sizeP p i : reflect (∀ j, i ≤ j → p`_j = 0) (size p ≤ i).
Size, leading coef, morphism properties of coef
Lemma coefD p q i : (p + q)`_i = p`_i + q`_i.
Lemma polyCD : {morph polyC : a b / a + b}.
Lemma size_add p q : size (p + q) ≤ maxn (size p) (size q).
Lemma size_addl p q : size p > size q → size (p + q) = size p.
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).
Lemma lead_coefDl p q : size p > size q → lead_coef (p + q) = lead_coef p.
Lemma lead_coefDr p q : size q > size p → lead_coef (p + q) = lead_coef q.
Polynomial semiring structure.
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.
Definition mul_poly := locked_with mul_poly_key mul_poly_def.
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)%N.
Fact coef_mul_poly_rev p q i :
(mul_poly p q)`_i = \sum_(j < i.+1) p`_(i - j)%N × q`_j.
Fact mul_polyA : associative mul_poly.
Fact mul_1poly : left_id 1%:P mul_poly.
Fact mul_poly1 : right_id 1%:P mul_poly.
Fact mul_polyDl : left_distributive mul_poly +%R.
Fact mul_polyDr : right_distributive mul_poly +%R.
Fact mul_0poly : left_zero 0%:P mul_poly.
Fact mul_poly0 : right_zero 0%:P mul_poly.
Fact poly1_neq0 : 1%:P != 0 :> {poly R}.
Lemma polyC1 : 1%:P = 1 :> {poly R}.
Lemma polyseq1 : (1 : {poly R}) = [:: 1] :> seq R.
Lemma size_poly1 : size (1 : {poly R}) = 1.
Lemma coef1 i : (1 : {poly R})`_i = (i == 0)%:R.
Lemma lead_coef1 : lead_coef 1 = 1 :> R.
Lemma coefM p q i : (p × q)`_i = \sum_(j < i.+1) p`_j × q`_(i - j)%N.
Lemma coefMr p q i : (p × q)`_i = \sum_(j < i.+1) p`_(i - j)%N × q`_j.
Lemma coef0M p q : (p × q)`_0 = p`_0 × q`_0.
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.
Lemma size_mul_leq 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.
Lemma size_proper_mul p q :
lead_coef p × lead_coef q != 0 → size (p × q) = (size p + size q).-1.
Lemma lead_coef_proper_mul p q :
let c := lead_coef p × lead_coef q in c != 0 → lead_coef (p × q) = c.
Lemma size_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|.
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_exp_leq p n : size (p ^+ n) ≤ ((size p).-1 × n).+1.
End SemiPolynomialTheory.
Section PolynomialTheory.
Variable R : ringType.
Implicit Types (a b c x y z : R) (p q r d : {poly R}).
Local Notation "c %:P" := (polyC c).
Local Notation "\poly_ ( i < n ) E" := (poly n (fun i : nat ⇒ E)).
Zmodule structure for polynomial
Definition opp_poly_def p := \poly_(i < size p) - p`_i.
Fact opp_poly_key : unit.
Definition opp_poly := locked_with opp_poly_key opp_poly_def.
Canonical opp_poly_unlockable := [unlockable fun opp_poly].
Fact coef_opp_poly p i : (opp_poly p)`_i = - p`_i.
Fact add_polyN : left_inverse 0%:P opp_poly (@add_poly _).
Size, leading coef, morphism properties of coef
Lemma coefN p i : (- p)`_i = - p`_i.
Lemma coefB p q i : (p - q)`_i = p`_i - q`_i.
Lemma coefMn p n i : (p *+ n)`_i = p`_i *+ n.
Lemma coefMNn 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 polyCN : {morph (@polyC R) : c / - c}.
Lemma polyCB : {morph (@polyC R) : a b / a - b}.
Lemma polyCMn n : {morph (@polyC R) : c / c *+ n}.
Lemma size_opp p : size (- p) = size p.
Lemma lead_coefN p : lead_coef (- p) = - lead_coef p.
Polynomial ring structure.
Fact polyC_multiplicative : multiplicative (@polyC R).
Lemma polyC_exp n : {morph (@polyC R) : c / c ^+ n}.
Lemma polyC_natr n : n%:R%:P = n%:R :> {poly R}.
Lemma char_poly : [char {poly R}] =i [char R].
Lemma size_Msign p n : size ((-1) ^+ n × p) = size p.
Fact coefp0_multiplicative : multiplicative (coefp 0 : {poly R} → R).
Algebra structure of polynomials.
Definition scale_poly_def a (p : {poly R}) := \poly_(i < size p) (a × p`_i).
Fact scale_poly_key : unit.
Definition scale_poly := locked_with scale_poly_key scale_poly_def.
Canonical scale_poly_unlockable := [unlockable fun scale_poly].
Fact scale_polyE a p : scale_poly a p = a%:P × p.
Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a × b) p.
Fact scale_1poly : left_id 1 scale_poly.
Fact scale_polyDr a : {morph scale_poly a : p q / p + q}.
Fact scale_polyDl p : {morph scale_poly^~ p : a b / a + b}.
Fact scale_polyAl a p q : scale_poly a (p × q) = scale_poly a p × q.
Lemma mul_polyC a p : a%:P × p = a *: p.
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.
Lemma size_scale_leq a p : size (a *: p) ≤ size p.
The indeterminate, at last!
Definition polyX_def := @Poly R [:: 0; 1].
Fact polyX_key : unit.
Definition polyX : {poly R} := locked_with polyX_key polyX_def.
Canonical polyX_unlockable := [unlockable of polyX].
Local Notation "'X" := polyX.
Lemma polyseqX : 'X = [:: 0; 1] :> seq R.
Lemma size_polyX : size 'X = 2.
Lemma polyX_eq0 : ('X == 0) = false.
Lemma coefX i : 'X`_i = (i == 1)%:R.
Lemma lead_coefX : lead_coef 'X = 1.
Lemma commr_polyX p : GRing.comm p 'X.
Lemma coefMX p i : (p × 'X)`_i = (if (i == 0)%N then 0 else p`_i.-1).
Lemma coefXM p i : ('X × p)`_i = (if (i == 0)%N then 0 else p`_i.-1).
Lemma cons_poly_def p a : cons_poly a p = p × 'X + a%:P.
Lemma poly_ind (K : {poly R} → Type) :
K 0 → (∀ p c, K p → K (p × 'X + c%:P)) → (∀ p, K p).
Lemma polyseqXaddC a : 'X + a%:P = [:: a; 1] :> seq R.
Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R.
Lemma size_XsubC a : size ('X - a%:P) = 2.
Lemma size_XaddC b : size ('X + b%:P) = 2.
Lemma lead_coefXaddC a : lead_coef ('X + a%:P) = 1.
Lemma lead_coefXsubC a : lead_coef ('X - a%:P) = 1.
Lemma polyXsubC_eq0 a : ('X - a%:P == 0) = false.
Lemma size_MXaddC p c :
size (p × 'X + c%:P) = (if (p == 0) && (c == 0) then 0 else (size p).+1).
Lemma polyseqMX p : p != 0 → p × 'X = 0 :: p :> seq R.
Lemma size_mulX p : p != 0 → size (p × 'X) = (size p).+1.
Lemma lead_coefMX p : lead_coef (p × 'X) = lead_coef p.
Lemma size_XmulC a : a != 0 → size ('X × a%:P) = 2.
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.
Lemma size_polyXn n : size 'X^n = n.+1.
Lemma commr_polyXn p n : GRing.comm p 'X^n.
Lemma lead_coefXn n : lead_coef 'X^n = 1.
Lemma lead_coefXnaddC n c : 0 < n → lead_coef ('X^n + c%:P) = 1.
Lemma lead_coefXnsubC n c : 0 < n → lead_coef ('X^n - c%:P) = 1.
Lemma size_XnaddC n c : 0 < n → size ('X^n + c%:P) = n.+1.
Lemma size_XnsubC n c : 0 < n → size ('X^n - c%:P) = n.+1.
Lemma polyseqMXn n p : p != 0 → p × 'X^n = ncons n 0 p :> seq R.
Lemma coefMXn n p i : (p × 'X^n)`_i = if i < n then 0 else p`_(i - n).
Lemma size_mulXn n p : p != 0 → size (p × 'X^n) = (n + size p)%N.
Lemma coefXnM n p i : ('X^n × p)`_i = if i < n then 0 else p`_(i - n).
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.
Expansion of a polynomial as an indexed sum
Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i.
Monic predicate
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).
Lemma monicP p : reflect (lead_coef p = 1) (p \is monic).
Lemma monic1 : 1 \is monic.
Lemma monicX : 'X \is monic.
Lemma monicXn n : 'X^n \is monic.
Lemma monic_neq0 p : p \is monic → p != 0.
Lemma lead_coef_monicM p q : p \is monic → lead_coef (p × q) = lead_coef q.
Lemma lead_coef_Mmonic p q : q \is monic → lead_coef (p × q) = lead_coef p.
Lemma size_monicM p q :
p \is monic → q != 0 → size (p × q) = (size p + size q).-1.
Lemma size_Mmonic p q :
p != 0 → q \is monic → size (p × q) = (size p + size q).-1.
Lemma monicMl p q : p \is monic → (p × q \is monic) = (q \is monic).
Lemma monicMr p q : q \is monic → (p × q \is monic) = (p \is monic).
Fact monic_mulr_closed : mulr_closed monic.
Lemma monic_exp p n : p \is monic → p ^+ n \is monic.
Lemma monic_prod I rI (P : pred I) (F : I → {poly R}):
(∀ i, P i → F i \is monic) → \prod_(i <- rI | P i) F i \is monic.
Lemma monicXaddC c : 'X + c%:P \is monic.
Lemma monicXsubC c : 'X - c%:P \is monic.
Lemma monic_prod_XsubC I rI (P : pred I) (F : I → R) :
\prod_(i <- rI | P i) ('X - (F i)%:P) \is monic.
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.
Lemma size_prod_XsubC I rI (F : I → R) :
size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1.
Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
Lemma monicXnaddC n c : 0 < n → 'X^n + c%:P \is monic.
Lemma monicXnsubC n c : 0 < n → 'X^n - c%:P \is monic.
Some facts about regular elements.
Lemma lreg_lead p : GRing.lreg (lead_coef p) → GRing.lreg p.
Lemma rreg_lead p : GRing.rreg (lead_coef p) → GRing.rreg p.
Lemma lreg_lead0 p : GRing.lreg (lead_coef p) → p != 0.
Lemma rreg_lead0 p : GRing.rreg (lead_coef p) → p != 0.
Lemma lreg_size c p : GRing.lreg c → size (c *: p) = size p.
Lemma lreg_polyZ_eq0 c p : GRing.lreg c → (c *: p == 0) = (p == 0).
Lemma lead_coef_lreg c p :
GRing.lreg c → lead_coef (c *: p) = c × lead_coef p.
Lemma rreg_size c p : GRing.rreg c → size (p × c%:P) = size p.
Lemma rreg_polyMC_eq0 c p : GRing.rreg c → (p × c%:P == 0) = (p == 0).
Lemma rreg_div0 q r d :
GRing.rreg (lead_coef d) → size r < size d →
(q × d + r == 0) = (q == 0) && (r == 0).
Lemma monic_comreg p :
p \is monic → GRing.comm p (lead_coef p)%:P ∧ GRing.rreg (lead_coef p).
Lemma monic_lreg p : p \is monic → GRing.lreg p.
Lemma monic_rreg p : p \is monic → GRing.rreg p.
Horner evaluation of polynomials
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.
Lemma hornerMX p x : (p × 'X).[x] = p.[x] × x.
Lemma horner_Poly s x : (Poly s).[x] = horner_rec s x.
Lemma horner_coef p x : p.[x] = \sum_(i < size p) p`_i × x ^+ i.
Lemma horner_coef_wide n p x :
size p ≤ n → p.[x] = \sum_(i < n) p`_i × x ^+ i.
Lemma horner_poly n E x : (\poly_(i < n) E i).[x] = \sum_(i < n) E i × x ^+ i.
Lemma hornerN p x : (- p).[x] = - p.[x].
Lemma hornerD p q x : (p + q).[x] = p.[x] + q.[x].
Lemma hornerXsubC a x : ('X - a%:P).[x] = x - a.
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].
Lemma hornerCM a p x : (a%:P × p).[x] = a × p.[x].
Lemma hornerZ c p x : (c *: p).[x] = c × p.[x].
Lemma hornerMn n p x : (p *+ n).[x] = p.[x] *+ n.
Definition comm_coef p x := ∀ 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.
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].
Lemma hornerM_comm p q x : comm_poly q x → (p × q).[x] = p.[x] × q.[x].
Lemma comm_polyM p q x: comm_poly p x → comm_poly q x → comm_poly (p × q) x.
Lemma horner_exp_comm p x n : comm_poly p x → (p ^+ n).[x] = p.[x] ^+ n.
Lemma comm_poly_exp p n x: comm_poly p x → comm_poly (p ^+ n) x.
Lemma hornerXn x n : ('X^n).[x] = x ^+ n.
Definition hornerE_comm :=
(hornerD, hornerN, hornerX, hornerC, horner_cons,
simp, hornerCM, hornerZ,
(fun p x ⇒ hornerM_comm p (comm_polyX x))).
Definition root p : pred R := fun x ⇒ p.[x] == 0.
Lemma mem_root p x : x \in root p = (p.[x] == 0).
Lemma rootE p x : (root p x = (p.[x] == 0)) × ((x \in root p) = (p.[x] == 0)).
Lemma rootP p x : reflect (p.[x] = 0) (root p x).
Lemma rootPt p x : reflect (p.[x] == 0) (root p x).
Lemma rootPf p x : reflect ((p.[x] == 0) = false) (~~ root p x).
Lemma rootC a x : root a%:P x = (a == 0).
Lemma root0 x : root 0 x.
Lemma root1 x : ~~ root 1 x.
Lemma rootX x : root 'X x = (x == 0).
Lemma rootN p x : root (- p) x = root p x.
Lemma root_size_gt1 a p : p != 0 → root p a → 1 < size p.
Lemma root_XsubC a x : root ('X - a%:P) x = (x == a).
Lemma root_XaddC a x : root ('X + a%:P) x = (x == - a).
Theorem factor_theorem p a : reflect (∃ q, p = q × ('X - a%:P)) (root p a).
Lemma multiplicity_XsubC p a :
{m | exists2 q, (p != 0) ==> ~~ root q a & p = q × ('X - a%:P) ^+ m}.
Roots of unity.
#[deprecated(since="mathcomp 2.3.0",note="Use size_XnsubC instead.")]
Lemma size_Xn_sub_1 n : n > 0 → size ('X^n - 1 : {poly R}) = n.+1.
#[deprecated(since="mathcomp 2.3.0'",note="Use monicXnsubC instead.")]
Lemma monic_Xn_sub_1 n : n > 0 → 'X^n - 1 \is monic.
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).
Definition primitive_root_of_unity n z :=
(n > 0) && [∀ 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)}.
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.
Lemma prim_expr_mod i : z ^+ (i %% n) = z ^+ i.
Lemma prim_order_dvd i : (n %| i) = (z ^+ i == 1).
Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j) = (i == j %[mod n]).
Lemma exp_prim_root k : (n %/ gcdn k n).-primitive_root (z ^+ k).
Lemma dvdn_prim_root m : (m %| n)%N → m.-primitive_root (z ^+ (n %/ m)).
Lemma prim_root_eq0 : (z == 0) = (n == 0%N).
End OnePrimitive.
Lemma prim_root_exp_coprime n z k :
n.-primitive_root z → n.-primitive_root (z ^+ k) = coprime k n.
Lifting a ring predicate to polynomials.
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 :
(∀ i, i < n → E i \in S) → \poly_(i < n) E i \is a polyOver S.
Section PolyOverAdd.
Variable S : addrClosed R.
Lemma polyOverP {p} : reflect (∀ i, p`_i \in S) (p \in polyOver S).
Lemma polyOverC c : (c%:P \in polyOver S) = (c \in S).
Fact polyOver_addr_closed : addr_closed (polyOver S).
End PolyOverAdd.
Section PolyOverSemiRing2.
Variable S : semiring2Closed R.
Lemma polyOver_mulr_2closed : GRing.mulr_2closed (polyOver S).
End PolyOverSemiRing2.
Fact polyOverNr (zmodS : zmodClosed R) : oppr_closed (polyOver zmodS).
Section PolyOverSemiring.
Variable S : semiringClosed R.
Fact polyOver_mul1_closed : 1 \in (polyOver S).
Lemma polyOverZ : {in S & polyOver S, ∀ 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, ∀ p x, p.[x] \in S}.
End PolyOverSemiring.
Section PolyOverRing.
Variable S : subringClosed R.
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).
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).
End PolyOverRing.
Single derivative.
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.
Lemma polyOver_deriv (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p, p^`() \is a polyOver ringS}.
Lemma derivC c : c%:P^`() = 0.
Lemma derivX : ('X)^`() = 1.
Lemma derivXn n : 'X^n^`() = 'X^n.-1 *+ n.
Fact deriv_is_linear : linear deriv.
Lemma deriv0 : 0^`() = 0.
Lemma derivD : {morph deriv : p q / p + q}.
Lemma derivN : {morph deriv : p / - p}.
Lemma derivB : {morph deriv : p q / p - q}.
Lemma derivXsubC (a : R) : ('X - a%:P)^`() = 1.
Lemma derivMn n p : (p *+ n)^`() = p^`() *+ n.
Lemma derivMNn n p : (p *- n)^`() = p^`() *- n.
Lemma derivZ c p : (c *: p)^`() = c *: p^`().
Lemma deriv_mulC c p : (c%:P × p)^`() = c%:P × p^`().
Lemma derivMXaddC p c : (p × 'X + c%:P)^`() = p + p^`() × 'X.
Lemma derivM p q : (p × q)^`() = p^`() × q + p × q^`().
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).
Iterated derivative.
Definition derivn n p := iter n deriv p.
Local Notation "a ^` ( n )" := (derivn n a) : ring_scope.
Lemma derivn0 p : p^`(0) = p.
Lemma derivn1 p : p^`(1) = p^`().
Lemma derivnS p n : p^`(n.+1) = p^`(n)^`().
Lemma derivSn p n : p^`(n.+1) = p^`()^`(n).
Lemma coef_derivn n p i : p^`(n)`_i = p`_(n + i) *+ (n + i) ^_ n.
Lemma polyOver_derivn (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p n, p^`(n) \is a polyOver ringS}.
Fact derivn_is_linear n : linear (derivn 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}.
Lemma derivnB n : {morph derivn n : p q / p - q}.
Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.
Lemma derivnMNn n m p : (p *- m)^`(n) = p^`(n) *- m.
Lemma derivnN n : {morph derivn n : p / - p}.
Lemma derivnZ n : scalable (derivn n).
Lemma derivnXn m n : 'X^m^`(n) = 'X^(m - n) *+ m ^_ n.
Lemma derivnMXaddC n p c :
(p × 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) × 'X.
Lemma derivn_poly0 p n : size p ≤ n → p^`(n) = 0.
Lemma lt_size_deriv (p : {poly R}) : p != 0 → size p^`() < size p.
A normalising version of derivation to get the division by n! in Taylor
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).
Here is the division by n!
Lemma nderivn_def n p : p^`(n) = p^`N(n) *+ n`!.
Lemma polyOver_nderivn (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p n, p^`N(n) \in polyOver ringS}.
Lemma nderivn0 p : p^`N(0) = p.
Lemma nderivn1 p : p^`N(1) = p^`().
Lemma nderivnC c n : (c%:P)^`N(n) = if n == 0 then c%:P else 0.
Lemma nderivnXn m n : 'X^m^`N(n) = 'X^(m - n) *+ 'C(m, n).
Fact nderivn_is_linear n : linear (nderivn n).
Lemma nderivnD n : {morph nderivn n : p q / p + q}.
Lemma nderivnB n : {morph nderivn n : p q / p - q}.
Lemma nderivnMn n m p : (p *+ m)^`N(n) = p^`N(n) *+ m.
Lemma nderivnMNn n m p : (p *- m)^`N(n) = p^`N(n) *- m.
Lemma nderivnN n : {morph nderivn n : p / - p}.
Lemma nderivnZ n : scalable (nderivn n).
Lemma nderivnMXaddC n p c :
(p × 'X + c%:P)^`N(n.+1) = p^`N(n) + p^`N(n.+1) × 'X.
Lemma nderivn_poly0 p n : size p ≤ n → p^`N(n) = 0.
Lemma nderiv_taylor p x h :
GRing.comm x h → p.[x + h] = \sum_(i < size p) p^`N(i).[x] × h ^+ i.
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.
Lemma eq_poly n E1 E2 : (∀ i, i < n → E1 i = E2 i) →
poly n E1 = poly n E2 :> {poly R}.
End PolynomialTheory.
Arguments monic {R}.
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 "n .-unity_root" := (root_of_unity n) : ring_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : 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 monic_pred _ _ /.
Arguments monicP {R p}.
Arguments rootP {R p x}.
Arguments rootPf {R p x}.
Arguments rootPt {R p x}.
Arguments unity_rootP {R n z}.
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.
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_charF p : (p %| n)%N → p \in [char R] = false.
Lemma char_prim_root : [char R]^'.-nat n.
Lemma prim_root_pi_eq0 m : \pi(n).-nat m → m%:R != 0 :> R.
Lemma prim_root_dvd_eq0 m : (m %| n)%N → m%:R != 0 :> R.
Lemma prim_root_natf_neq0 : n%:R != 0 :> R.
End IdomainPrimRoot.
Container morphism.
Section MapPoly.
Section Definitions.
Variables (aR rR : ringType) (f : aR → rR).
Definition map_poly (p : {poly aR}) := \poly_(i < size p) f p`_i.
Alternative definition; the one above is more convenient because it lets us use the lemmas on \poly, e.g., size (map_poly p) <= size p is an instance of size_poly.
Lemma map_polyE p : map_poly p = Poly (map f p).
Definition commr_rmorph u := ∀ x, GRing.comm u (f x).
Definition horner_morph u of commr_rmorph u := fun p ⇒ (map_poly p).[u].
End Definitions.
Variables aR rR : ringType.
Section Combinatorial.
Variables (iR : ringType) (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.
Lemma map_Poly_id0 s : f 0 = 0 → (Poly s)^f = Poly (map f s).
Lemma map_poly_comp_id0 (g : iR → aR) p :
f 0 = 0 → map_poly (f \o g) p = (map_poly g p)^f.
Lemma size_map_poly_id0 p : f (lead_coef p) != 0 → size p^f = size p.
Lemma map_poly_eq0_id0 p : f (lead_coef p) != 0 → (p^f == 0) = (p == 0).
Lemma lead_coef_map_id0 p :
f 0 = 0 → f (lead_coef p) != 0 → lead_coef p^f = f (lead_coef p).
Hypotheses (inj_f : injective f) (f_0 : f 0 = 0).
Lemma size_map_inj_poly p : size p^f = size p.
Lemma map_inj_poly : injective (map_poly f).
Lemma lead_coef_map_inj p : lead_coef p^f = f (lead_coef p).
End Combinatorial.
Lemma map_polyK (f : aR → rR) g :
cancel g f → f 0 = 0 → cancel (map_poly g) (map_poly f).
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}.
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}.
Section Additive.
Variables (iR : ringType) (f : {additive aR → rR}).
Local Notation "p ^f" := (map_poly (GRing.Additive.sort f) p) : ring_scope.
Lemma coef_map p i : p^f`_i = f p`_i.
Lemma map_Poly s : (Poly s)^f = Poly (map f s).
Lemma map_poly_comp (g : iR → aR) p :
map_poly (f \o g) p = map_poly f (map_poly g p).
Fact map_poly_is_additive : additive (map_poly f).
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).
End Additive.
Variable f : {rmorphism aR → rR}.
Implicit Types p : {poly aR}.
Local Notation "p ^f" := (map_poly (GRing.RMorphism.sort f) p) : ring_scope.
Fact map_poly_is_multiplicative : multiplicative (map_poly f).
Lemma map_polyZ c p : (c *: p)^f = f c *: p^f.
Lemma map_polyX : ('X)^f = 'X.
Lemma map_polyXn n : ('X^n)^f = 'X^n.
Lemma map_polyXaddC x : ('X + x%:P)^f = 'X + (f x)%:P.
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).
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.
Lemma monic_map p : p \is monic → p^f \is monic.
Lemma horner_map p x : p^f.[f x] = f p.[x].
Lemma map_comm_poly p x : comm_poly p x → comm_poly p^f (f x).
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).
Lemma rmorph_unity_root n z : n.-unity_root z → n.-unity_root (f z).
Section HornerMorph.
Variable u : rR.
Hypothesis cfu : commr_rmorph f u.
Lemma horner_morphC a : horner_morph cfu a%:P = f a.
Lemma horner_morphX : horner_morph cfu 'X = u.
Fact horner_is_linear : linear_for (f \; *%R) (horner_morph cfu).
Fact horner_is_multiplicative : multiplicative (horner_morph cfu).
End HornerMorph.
Lemma deriv_map p : p^f^`() = (p^`())^f.
Lemma derivn_map p n : p^f^`(n) = (p^`(n))^f.
Lemma nderivn_map p n : p^f^`N(n) = (p^`N(n))^f.
End MapPoly.
Lemma mapf_root (F : fieldType) (R : ringType) (f : {rmorphism F → R})
(p : {poly F}) (x : F) : root (map_poly f p) (f x) = root p x.
Morphisms from the polynomial ring, and the initiality of polynomials with respect to these.
Section MorphPoly.
Variable (aR rR : ringType) (pf : {rmorphism {poly aR} → rR}).
Lemma poly_morphX_comm : commr_rmorph (pf \o polyC) (pf 'X).
Lemma poly_initial : pf =1 horner_morph poly_morphX_comm.
End MorphPoly.
Notation "p ^:P" := (map_poly polyC p) : ring_scope.
Section PolyCompose.
Variable R : ringType.
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.
Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0).
Lemma root_polyC p x : root p^:P x%:P = root p x.
Lemma comp_polyE p q : p \Po q = \sum_(i < size p) p`_i *: q^+i.
Lemma coef_comp_poly p q n :
(p \Po q)`_n = \sum_(i < size p) p`_i × (q ^+ i)`_n.
Lemma polyOver_comp (ringS : semiringClosed R) :
{in polyOver ringS &, ∀ p q, p \Po q \in polyOver ringS}.
Lemma comp_polyCr p c : p \Po c%:P = p.[c]%:P.
Lemma comp_poly0r p : p \Po 0 = (p`_0)%:P.
Lemma comp_polyC c p : c%:P \Po p = c%:P.
Fact comp_poly_is_linear p : linear (comp_poly p).
Lemma comp_poly0 p : 0 \Po p = 0.
Lemma comp_polyD p q r : (p + q) \Po r = (p \Po r) + (q \Po r).
Lemma comp_polyB p q r : (p - q) \Po r = (p \Po r) - (q \Po r).
Lemma comp_polyZ c p q : (c *: p) \Po q = c *: (p \Po q).
Lemma comp_polyXr p : p \Po 'X = p.
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 comp_polyXaddC_K p z : (p \Po ('X + z%:P)) \Po ('X - z%:P) = p.
Lemma size_comp_poly_leq p q :
size (p \Po q) ≤ ((size p).-1 × (size q).-1).+1.
Lemma comp_Xn_poly p n : 'X^n \Po p = p ^+ n.
Lemma coef_comp_poly_Xn p n i : 0 < n →
(p \Po 'X^n)`_i = if n %| i then p`_(i %/ n) else 0.
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.
End PolyCompose.
Notation "p \Po q" := (comp_poly q p) : ring_scope.
Lemma map_comp_poly (aR rR : ringType) (f : {rmorphism aR → rR}) p q :
map_poly f (p \Po q) = map_poly f p \Po map_poly f q.
Section Surgery.
Variable R : ringType.
Implicit Type p q : {poly R}.
Even part of a polynomial
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).
Lemma coef_even_poly p i : (even_poly p)`_i = p`_i.*2.
Lemma even_polyE s p : size p ≤ s.*2 → even_poly p = \poly_(i < s) p`_i.*2.
Lemma size_even_poly_eq p : odd (size p) →
size (even_poly p) = uphalf (size p).
Lemma even_polyD p q : even_poly (p + q) = even_poly p + even_poly q.
Lemma even_polyZ k p : even_poly (k *: p) = k *: even_poly p.
Fact even_poly_is_linear : linear even_poly.
Lemma even_polyC (c : R) : even_poly c%:P = c%:P.
Odd part of a polynomial
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.
Lemma coef_odd_poly p i : (odd_poly p)`_i = p`_i.*2.+1.
Lemma odd_polyE s p :
size p ≤ s.*2.+1 → odd_poly p = \poly_(i < s) p`_i.*2.+1.
Lemma odd_polyC (c : R) : odd_poly c%:P = 0.
Lemma odd_polyD p q : odd_poly (p + q) = odd_poly p + odd_poly q.
Lemma odd_polyZ k p : odd_poly (k *: p) = k *: odd_poly p.
Fact odd_poly_is_linear : linear odd_poly.
Lemma size_odd_poly_eq p : ~~ odd (size p) → size (odd_poly p) = (size p)./2.
Lemma odd_polyMX p : odd_poly (p × 'X) = even_poly p.
Lemma even_polyMX p : even_poly (p × 'X) = odd_poly p × 'X.
Lemma sum_even_poly p :
\sum_(i < size p | ~~ odd i) p`_i *: 'X^i = even_poly p \Po 'X^2.
Lemma sum_odd_poly p :
\sum_(i < size p | odd i) p`_i *: 'X^i = (odd_poly p \Po 'X^2) × 'X.
Decomposition in odd and even part
Lemma poly_even_odd p : even_poly p \Po 'X^2 + (odd_poly p \Po 'X^2) × 'X = p.
take and drop for polynomials
Definition take_poly m p := \poly_(i < m) p`_i.
Lemma size_take_poly m p : size (take_poly m p) ≤ m.
Lemma coef_take_poly m p i : (take_poly m p)`_i = if i < m then p`_i else 0.
Lemma take_poly_id m p : size p ≤ m → take_poly m p = p.
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.
Fact take_poly_is_linear m : linear (take_poly 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).
Lemma take_poly0l p : take_poly 0 p = 0.
Lemma take_poly0r m : take_poly m 0 = 0.
Lemma take_polyMXn m n p :
take_poly m (p × 'X^n) = take_poly (m - n) p × 'X^n.
Lemma take_polyMXn_0 n p : take_poly n (p × 'X^n) = 0.
Lemma take_polyDMXn n p q : size p ≤ n → take_poly n (p + q × 'X^n) = p.
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.
Lemma size_drop_poly n p : size (drop_poly n p) = (size p - n)%N.
Lemma sum_drop_poly n p :
\sum_(n ≤ i < size p) p`_i *: 'X^i = drop_poly n p × 'X^n.
Lemma drop_polyD m p q : drop_poly m (p + q) = drop_poly m p + drop_poly m q.
Lemma drop_polyZ k m p : drop_poly m (k *: p) = k *: drop_poly m p.
Fact drop_poly_is_linear m : linear (drop_poly 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).
Lemma drop_poly0l p : drop_poly 0 p = p.
Lemma drop_poly0r m : drop_poly m 0 = 0.
Lemma drop_polyMXn m n p :
drop_poly m (p × 'X^n) = drop_poly (m - n) p × 'X^(n - m).
Lemma drop_polyMXn_id n p : drop_poly n (p × 'X^ n) = p.
Lemma drop_polyDMXn n p q : size p ≤ n → drop_poly n (p + q × 'X^n) = q.
Lemma poly_take_drop n p : take_poly n p + drop_poly n p × 'X^n = p.
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.
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 PolynomialComRing.
Variable R : comRingType.
Implicit Types p q : {poly R}.
Fact poly_mul_comm p q : p × q = q × p.
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.
Lemma coefPn_prod_XsubC (ps : seq R) : size ps != 0 →
(\prod_(p <- ps) ('X - p%:P))`_((size ps).-1) =
- \sum_(p <- ps) p.
Lemma coef0_prod_XsubC (ps : seq R) :
(\prod_(p <- ps) ('X - p%:P))`_0 =
(-1) ^+ (size ps) × \prod_(p <- ps) p.
Lemma hornerM p q x : (p × q).[x] = p.[x] × q.[x].
Lemma horner_exp p x n : (p ^+ n).[x] = p.[x] ^+ n.
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].
Definition hornerE :=
(hornerD, hornerN, hornerX, hornerC, horner_exp,
simp, hornerCM, hornerZ, hornerM, horner_cons).
Definition horner_eval (x : R) := horner^~ x.
Lemma horner_evalE x p : horner_eval x p = p.[x].
Fact horner_eval_is_linear x : linear_for *%R (horner_eval x).
Fact horner_eval_is_multiplicative x : multiplicative (horner_eval x).
Section HornerAlg.
Variable A : algType R. (* For univariate polys, commutativity is not needed *)
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.
Lemma horner_algX : horner_alg 'X = a.
End Defs.
Variable (pf : {lrmorphism {poly R} → A}).
Lemma poly_alg_initial : pf =1 horner_alg (pf 'X).
End HornerAlg.
Fact comp_poly_multiplicative q : multiplicative (comp_poly q).
Lemma comp_polyM p q r : (p × q) \Po r = (p \Po r) × (q \Po r).
Lemma comp_polyA p q r : p \Po (q \Po r) = (p \Po q) \Po r.
Lemma horner_comp p q x : (p \Po q).[x] = p.[q.[x]].
Lemma root_comp p q x : root (p \Po q) x = root p (q.[x]).
Lemma deriv_comp p q : (p \Po q) ^`() = (p ^`() \Po q) × q^`().
Lemma deriv_exp p n : (p ^+ n)^`() = p^`() × p ^+ n.-1 *+ n.
Definition derivCE := (derivE, deriv_exp).
End PolynomialComRing.
Section PolynomialIdomain.
Integral domain structure on poly
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.
Fact poly_idomainAxiom p q : p × q = 0 → (p == 0) || (q == 0).
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}.
Fact poly_intro_unit p q : q × p = 1 → p \in poly_unit.
Fact poly_inv_out : {in [predC poly_unit], poly_inv =1 id}.
Lemma poly_unitE p :
(p \in GRing.unit) = (size p == 1) && (p`_0 \in GRing.unit).
Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p`_0)^-1%:P else p.
Lemma polyCV c : c%:P^-1 = (c^-1)%:P.
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.
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.
Lemma lead_coefM p q : lead_coef (p × q) = lead_coef p × lead_coef q.
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).
Lemma lead_coefZ a p : lead_coef (a *: p) = a × lead_coef p.
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}) :
(∀ i, P i → F i != 0) →
size (\prod_(i | P i) F i) = ((\sum_(i | P i) size (F i)).+1 - #|P|)%N.
Lemma size_prod_seq (I : eqType) (s : seq I) (F : I → {poly R}) :
(∀ i, i \in s → F i != 0) →
size (\prod_(i <- s) F i) = ((\sum_(i <- s) size (F i)).+1 - size s)%N.
Lemma size_mul_eq1 p q : (size (p × q) == 1) = ((size p == 1) && (size q == 1)).
Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I → {poly R}) :
reflect (∀ i, P i && (i \in s) → size (F i) = 1)
(size (\prod_(i <- s | P i) F i) == 1%N).
Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I → {poly R}) :
reflect (∀ i, P i → size (F i) = 1)
(size (\prod_(i | P i) F i) == 1).
Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 × n)%N.
Lemma lead_coef_exp p n : lead_coef (p ^+ n) = lead_coef p ^+ n.
Lemma root_prod_XsubC rs x :
root (\prod_(a <- rs) ('X - a%:P)) x = (x \in rs).
Lemma root_exp_XsubC n a x : root (('X - a%:P) ^+ n.+1) x = (x == a).
Lemma size_comp_poly p q :
(size (p \Po q)).-1 = ((size p).-1 × (size q).-1)%N.
Lemma lead_coef_comp p q : size q > 1 →
lead_coef (p \Po q) = (lead_coef p) × lead_coef q ^+ (size p).-1.
Lemma comp_poly_eq0 p q : size q > 1 → (p \Po q == 0) = (p == 0).
Lemma size_comp_poly2 p q : size q = 2 → size (p \Po q) = size p.
Lemma comp_poly2_eq0 p q : size q = 2 → (p \Po q == 0) = (p == 0).
Theorem max_poly_roots p rs :
p != 0 → all (root p) rs → uniq rs → size rs < size p.
Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs → uniq rs →
(size rs ≥ size p)%N → p = 0.
End PolynomialIdomain.
FIXME: these are seamingly artificial ways to close the inheritance graph We make parameters more and more precise to trigger completion by HB
Section MapFieldPoly.
Variables (F : fieldType) (R : ringType) (f : {rmorphism F → R}).
Local Notation "p ^f" := (map_poly f p) : ring_scope.
Lemma size_map_poly p : size p^f = size p.
Lemma lead_coef_map p : lead_coef p^f = f (lead_coef p).
Lemma map_poly_eq0 p : (p^f == 0) = (p == 0).
Lemma map_poly_inj : injective (map_poly f).
Lemma map_monic p : (p^f \is monic) = (p \is monic).
Lemma map_poly_com p x : comm_poly p^f (f x).
Lemma fmorph_root p x : root p^f (f x) = root p x.
Lemma fmorph_unity_root n z : n.-unity_root (f z) = n.-unity_root z.
Lemma fmorph_primitive_root n z :
n.-primitive_root (f z) = n.-primitive_root z.
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 →
∃ q, p = q × \prod_(z <- rs) ('X - z%:P).
Theorem max_ring_poly_roots p rs :
p != 0 → all (root p) rs → uniq_roots rs → size rs < size p.
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).
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}.
Lemma uniq_rootsE rs : uniq_roots rs = uniq rs.
Lemma root_ZXsubC (a b r : F) : a != 0 →
root (a *: 'X - b%:P) r = (r == b / a).
Section UnityRoots.
Variable n : nat.
Lemma max_unity_roots rs :
n > 0 → all n.-unity_root rs → uniq rs → size rs ≤ n.
Lemma mem_unity_roots rs :
n > 0 → all n.-unity_root rs → uniq rs → size rs = n →
n.-unity_root =i rs.
Showing the existence of a primitive root requires the theory in cyclic.
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.
Lemma prim_rootP x : x ^+ n = 1 → {i : 'I_n | x = z ^+ i}.
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).
Lemma map_uniq_roots s : uniq_roots (map f s) = uniq s.
End MapPolyRoots.
Section AutPolyRoot.
The action of automorphisms on roots of unity.
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}.
Lemma aut_unity_rootP u z n : n > 0 → z ^+ n = 1 → {k | u z = z ^+ k}.
Lemma aut_unity_rootC u v z n : n > 0 → z ^+ n = 1 → u (v z) = v (u z).
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.
Let aneq0 : a != 0.
Let a2neq0 : 2 × a != 0.
Let sqa2neq0 : (2 × a) ^+ 2 != 0.
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.
Let delta := b ^+ 2 - 4 × a × c.
Lemma deg2_poly_canonical :
p = a *: (('X + (b / (2 × a))%:P)^+2 - (delta / (4 × a ^+ 2))%:P).
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).
Lemma deg2_poly_root1 : root p r1.
Lemma deg2_poly_root2 : root p r2.
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.
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.
Lemma deg2_poly_root2 : root p r2.
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 → ∀ x, ~~ root q x)}}.
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 (∃ x, root p x) (size p != 1).
Lemma closed_nonrootP p : reflect (∃ x, ~~ root p x) (p != 0).
End UseAxiom.
End PreClosedField.
Section ClosedField.
Variable F : closedFieldType.
Implicit Type p : {poly F}.
Let closedF := @solve_monicpoly F.
Lemma closed_rootP p : reflect (∃ x, root p x) (size p != 1).
Lemma closed_nonrootP p : reflect (∃ x, ~~ root p x) (p != 0).
Lemma closed_field_poly_normal p :
{r : seq F | p = lead_coef p *: \prod_(z <- r) ('X - z%:P)}.
End ClosedField.