Library MathClasses.implementations.polynomials
Require Import
Coq.Lists.List
MathClasses.interfaces.abstract_algebra
MathClasses.theory.rings
Ring.
Section contents.
Context R `{Ring R}.
Add Ring R: (stdlib_ring_theory R).
Definition poly := list R.
Coercion poly_constant (c : R) : poly := [c].
Global Instance poly_zero: Zero poly := [].
Global Instance poly_one: One poly := poly_constant 1.
Definition all (l: list Prop): Prop := fold_left and l True.
Lemma all_cons P Ps: all (P::Ps) ↔ P ∧ all Ps.
Proof.
unfold all.
revert P; generalize True as Q.
induction Ps as [|P' Ps IH]; intros.
{ cbn; tauto. }
change (fold_left and (P' :: Ps) (Q ∧ P) ↔ P ∧ fold_left and (P'::Ps) Q).
rewrite !IH.
transitivity (P' ∧ (P ∧ fold_left and Ps Q)); try tauto.
now rewrite <- (IH Q P).
Qed.
Arguments all: simpl never.
Definition poly_eq_zero: poly → Prop := all ∘ map ((=) 0).
Corollary poly_eq_zero_cons x p: poly_eq_zero (x::p) ↔ x = 0 ∧ poly_eq_zero p.
Proof.
unfold poly_eq_zero, compose; cbn; rewrite all_cons.
intuition now symmetry.
Qed.
Lemma poly_eq_zero_ind (P: poly → Prop) (case_nil: P [])
(casecons: ∀ x p, x = 0 → poly_eq_zero p → P p → P (x::p))
p: poly_eq_zero p → P p.
Proof.
induction p as [|x p IH]; auto.
intros [??]%poly_eq_zero_cons.
eauto.
Qed.
Global Instance poly_eq: Equiv poly :=
fix F p q :=
match p, q with
| [], _ => poly_eq_zero q
| _, [] => poly_eq_zero p
| h :: t, h' :: t' => h = h' ∧ F t t'
end.
Lemma poly_eq_p_zero p: (p = 0) ↔ poly_eq_zero p.
Proof. now destruct p. Qed.
Instance: Reflexive poly_eq.
Proof with intuition. repeat intro. induction x... split... Qed.
Lemma poly_eq_cons :
∀ (a b : R) (p q : poly), (a = b /\ poly_eq p q) <-> poly_eq (a :: p) (b :: q).
Proof. easy. Qed.
Lemma poly_eq_ind (P: poly → poly → Prop)
(case_0: ∀ p p', poly_eq_zero p → poly_eq_zero p' → P p p')
(case_cons: ∀ x x' p p', x = x' → p = p' → P p p' → P (x::p) (x'::p'))
p: ∀ p', p = p' → P p p'.
Proof.
induction p as [|x p IH]; intros [|x' p'] eqxy.
1,2,3: now apply case_0.
destruct eqxy.
apply case_cons; auto.
Qed.
Lemma poly_eq_zero_trans p q: poly_eq_zero p → poly_eq_zero q → p = q.
Proof.
revert q.
induction p as [|x p IH]; intros ? eqp eqq; auto.
destruct q as [|y q]; auto.
rewrite poly_eq_zero_cons in *.
rewrite <- poly_eq_cons.
destruct eqp as [-> ?], eqq as [-> ?]; split; eauto.
now apply IH.
Qed.
Instance: Symmetric poly_eq.
Proof.
intros p p' eqp.
pattern p, p'; apply poly_eq_ind; auto; clear p p' eqp.
- now intros; apply poly_eq_zero_trans.
- intros ???? eqx eqp IH.
rewrite <- poly_eq_cons; auto.
Qed.
Instance poly_eq_zero_proper: Proper (poly_eq ==> iff) poly_eq_zero.
Proof.
apply proper_sym_impl_iff.
{ apply _. }
red; refine (poly_eq_ind _ _ _).
- intros; hnf; auto.
- unfold impl; intros ???? eqx eqp IH.
rewrite !poly_eq_zero_cons, eqx; tauto.
Qed.
Instance: Transitive poly_eq.
Proof.
intros ??? eqxy; revert z.
pattern x, y; refine (poly_eq_ind _ _ _ x y eqxy); clear x y eqxy.
{ intros x y x0 y0 z eqz.
apply poly_eq_zero_trans; auto.
now rewrite <- eqz. }
intros ???? eqx eqp IH z eqz.
destruct z as [|x'' p''].
{ eapply poly_eq_zero_proper; eauto.
now split. }
destruct eqz as [eqx' eqp']; split; eauto.
Qed.
Global Instance: Setoid poly.
Proof. split; try apply _. Qed.
Global Instance: Plus poly := fix F p q :=
match p, q with
| [], _ => q
| _, [] => p
| h :: t, h' :: t' => h + h' :: F t t'
end.
Lemma poly_eq_zero_plus_l p q: poly_eq_zero p → p + q = q.
Proof.
intro eqp; revert q.
induction eqp as [|x p eqx eqp IH] using poly_eq_zero_ind.
{ easy. }
intros [|y q].
{ cbn -[poly_eq_zero].
rewrite poly_eq_zero_cons; auto. }
cbn; split; auto.
ring [eqx].
Qed.
Instance plus_commutative: Commutative (+).
Proof with (try easy); cbn.
intro.
induction x as [|x p IH]; intros [|y q]...
split; auto; ring.
Qed.
Corollary poly_eq_zero_plus_r p q: poly_eq_zero q → p + q = p.
Proof.
rewrite commutativity.
apply poly_eq_zero_plus_l.
Qed.
Corollary poly_eq_zero_plus p q: poly_eq_zero p → poly_eq_zero q → poly_eq_zero (p+q).
Proof.
intro.
rewrite <- !poly_eq_p_zero; intro.
now rewrite poly_eq_zero_plus_l.
Qed.
Global Instance poly_plus_proper: Proper (poly_eq ==> poly_eq ==> poly_eq) (+).
Proof.
unfold Proper, respectful.
refine (poly_eq_ind _ _ _).
{ intros p p' zp zp' q q' eqq.
rewrite !poly_eq_zero_plus_l; auto. }
intros ???? eqx eqp IH.
refine (poly_eq_ind _ _ _).
{ intros q q' zq zq'.
rewrite !poly_eq_zero_plus_r; auto.
cbn; auto. }
intros y y' q q' eqy eqq _.
cbn; split; eauto.
ring [eqx eqy].
Qed.
Instance plus_associative: Associative (+).
Proof with try easy.
do 2 red; induction x as [|x p IH]...
intros [|y q]...
intros [|z r]...
cbn; split; auto.
ring.
Qed.
Instance plus_left_id: LeftIdentity (+) 0.
Proof. now intro; rewrite poly_eq_zero_plus_l. Qed.
Instance plus_right_id: RightIdentity (+) 0.
Proof. now intro; rewrite poly_eq_zero_plus_r. Qed.
Instance poly_plus_monoid: Monoid poly.
Proof. repeat (split; try apply _). Qed.
Global Instance: Negate poly := map (-).
Lemma poly_negate_zero p: poly_eq_zero p ↔ poly_eq_zero (-p).
Proof.
induction p as [|x p IH].
{ easy. }
cbn.
rewrite !poly_eq_zero_cons, IH.
enough (x = 0 ↔ -x = 0) by tauto.
split; intro eq0; ring [eq0].
Qed.
Instance poly_negate_proper: Proper (poly_eq ==> poly_eq) (-).
Proof.
refine (poly_eq_ind _ _ _).
{ now intros ?? ->%poly_negate_zero%poly_eq_p_zero ->%poly_negate_zero%poly_eq_p_zero. }
intros ???? eqx eqp IH.
cbn; split; eauto.
Qed.
Instance poly_negate_l: LeftInverse (+) (-) 0.
Proof.
intro; rewrite poly_eq_p_zero.
induction x as [|x p IH]; cbn.
{ easy. }
rewrite poly_eq_zero_cons; split; auto.
ring.
Qed.
Instance poly_negate_r: RightInverse (+) (-) 0.
Proof. now intro; rewrite commutativity, left_inverse. Qed.
Instance poly_plus_abgroup: AbGroup poly.
Proof. repeat (split; try apply _). Qed.
Fixpoint poly_mult_cr (q: poly) (c: R): poly :=
match q with
| [] => 0
| d :: q1 => c*d :: poly_mult_cr q1 c
end.
Lemma poly_mult_cr_0_l q c: poly_eq_zero q → poly_eq_zero (poly_mult_cr q c).
Proof.
induction q as [|x q IH].
{ easy. }
cbn.
rewrite !poly_eq_zero_cons.
intros [-> ?]; split; auto.
ring.
Qed.
Instance poly_mult_cr_proper: Proper ((=) ==> (=) ==> (=)) poly_mult_cr.
Proof.
intros p p' eqp c c' eqc.
revert p p' eqp; refine (poly_eq_ind _ _ _).
{ now intros; apply poly_eq_zero_trans; apply poly_mult_cr_0_l. }
intros ???? eqx eqp IH.
split; auto; cbn.
ring [eqx eqc].
Qed.
Lemma poly_mult_cr_1_l x: poly_mult_cr 1 x = [x].
Proof. cbn; split; [ring|easy]. Qed.
Instance poly_mult_cr_1_r: RightIdentity poly_mult_cr 1.
Proof.
red; induction x as [|x p IH]; [easy|cbn].
split; auto; ring.
Qed.
Instance poly_mult_cr_dist_l: LeftHeteroDistribute poly_mult_cr (+) (+).
Proof.
intros x a b.
induction x as [|x p IH]; [easy|cbn].
split; auto; ring.
Qed.
Instance poly_mult_cr_dist_r: RightHeteroDistribute poly_mult_cr (+) (+).
Proof.
intros p q a.
revert q.
induction p as [|x p IH]; intros [|y q]; [easy..|cbn].
split; auto; ring.
Qed.
Instance poly_mult_cr_assoc: HeteroAssociative poly_mult_cr (.*.) poly_mult_cr poly_mult_cr.
Proof.
intros x a b.
induction x as [|p x IH]; [easy|cbn].
split; auto; ring.
Qed.
Lemma poly_mult_cr_0_r q c: c = 0 → poly_eq_zero (poly_mult_cr q c).
Proof.
intros ->.
induction q as [|x q IH]; [easy|cbn].
rewrite poly_eq_zero_cons; split; auto.
ring.
Qed.
Global Instance: Mult poly := fix F p q :=
match p with
| [] => 0
| c :: p1 => poly_mult_cr q c + (0 :: F p1 q)
end.
Lemma poly_mult_0_l p q: poly_eq_zero p → poly_eq_zero (p * q).
Proof.
induction 1 using poly_eq_zero_ind; [easy|cbn].
apply poly_eq_zero_plus.
- now apply poly_mult_cr_0_r.
- rewrite poly_eq_zero_cons; auto.
Qed.
Lemma poly_mult_0_r p q: poly_eq_zero q → poly_eq_zero (p * q).
Proof.
induction p as [|x p IH]; [easy|cbn].
intro eq0.
apply poly_eq_zero_plus.
- now apply poly_mult_cr_0_l.
- rewrite poly_eq_zero_cons; auto.
Qed.
Instance poly_mult_proper: Proper ((=) ==> (=) ==> (=)) (.*.).
Proof.
refine (poly_eq_ind _ _ _).
{ intros ?? zp zp' q q' eqq.
now apply poly_eq_zero_trans; apply poly_mult_0_l. }
intros ???? eqx eqp IH q q' eqq.
cbn.
apply poly_plus_proper.
{ now rewrite eqx, eqq. }
split; auto.
now apply IH.
Qed.
Instance poly_mult_left_distr: LeftDistribute (.*.) (+).
Proof.
intros p q r.
induction p as [|x p IH]; [easy|cbn].
rewrite (distribute_r q r x).
rewrite <- !associativity; apply poly_plus_proper; [easy|].
rewrite associativity, (commutativity (0::p*q)), <- associativity.
apply poly_plus_proper; [easy|].
cbn; split; [ring|easy].
Qed.
Lemma poly_mult_cons_r p q x: p * (x::q) = poly_mult_cr p x + (0 :: p * q).
Proof.
induction p as [|y p IH]; cbn; auto.
split; auto.
rewrite IH, !associativity, (commutativity (poly_mult_cr _ _)).
split; try easy.
ring.
Qed.
Instance poly_mult_comm: Commutative (.*.).
Proof.
intros p.
induction p as [|x p IH].
{ cbn; intro.
now apply poly_mult_0_r. }
intros [|y q]; cbn.
{ rewrite poly_eq_zero_cons; split; auto.
now apply poly_mult_0_r. }
split. 1: ring.
rewrite !poly_mult_cons_r, !associativity.
apply poly_plus_proper.
{ apply commutativity. }
rewrite <- poly_eq_cons; split; auto.
apply IH.
Qed.
Instance poly_mult_right_distr: RightDistribute (.*.) (+).
Proof.
intros p q r.
now rewrite commutativity, distribute_l, !(commutativity r).
Qed.
Instance poly_mult_1_l: LeftIdentity (.*.) 1.
Proof.
intro; cbn.
rewrite poly_mult_cr_1_r, poly_eq_zero_plus_r; auto.
now split.
Qed.
Instance poly_mult_1_r: RightIdentity (.*.) 1.
Proof.
intro; rewrite commutativity; apply left_identity.
Qed.
Instance poly_mult_assoc: Associative (.*.).
Proof with (try easy); cbn.
intros x.
induction x as [|x p IH]...
intros q r; cbn.
rewrite distribute_r.
apply poly_plus_proper; cbn -[poly_eq].
{ clear IH.
induction q as [|y q IH]...
rewrite distribute_r, <- associativity, (commutativity x y).
apply poly_plus_proper...
split; auto.
ring. }
assert (poly_mult_cr r 0 = 0) as ->.
{ now rewrite poly_eq_p_zero; apply poly_mult_cr_0_r. }
cbn; split; eauto.
now rewrite IH.
Qed.
Global Instance poly_ring: Ring poly.
Proof. repeat (split; try apply _). Qed.
End contents.
Coq.Lists.List
MathClasses.interfaces.abstract_algebra
MathClasses.theory.rings
Ring.
Section contents.
Context R `{Ring R}.
Add Ring R: (stdlib_ring_theory R).
Definition poly := list R.
Coercion poly_constant (c : R) : poly := [c].
Global Instance poly_zero: Zero poly := [].
Global Instance poly_one: One poly := poly_constant 1.
Definition all (l: list Prop): Prop := fold_left and l True.
Lemma all_cons P Ps: all (P::Ps) ↔ P ∧ all Ps.
Proof.
unfold all.
revert P; generalize True as Q.
induction Ps as [|P' Ps IH]; intros.
{ cbn; tauto. }
change (fold_left and (P' :: Ps) (Q ∧ P) ↔ P ∧ fold_left and (P'::Ps) Q).
rewrite !IH.
transitivity (P' ∧ (P ∧ fold_left and Ps Q)); try tauto.
now rewrite <- (IH Q P).
Qed.
Arguments all: simpl never.
Definition poly_eq_zero: poly → Prop := all ∘ map ((=) 0).
Corollary poly_eq_zero_cons x p: poly_eq_zero (x::p) ↔ x = 0 ∧ poly_eq_zero p.
Proof.
unfold poly_eq_zero, compose; cbn; rewrite all_cons.
intuition now symmetry.
Qed.
Lemma poly_eq_zero_ind (P: poly → Prop) (case_nil: P [])
(casecons: ∀ x p, x = 0 → poly_eq_zero p → P p → P (x::p))
p: poly_eq_zero p → P p.
Proof.
induction p as [|x p IH]; auto.
intros [??]%poly_eq_zero_cons.
eauto.
Qed.
Global Instance poly_eq: Equiv poly :=
fix F p q :=
match p, q with
| [], _ => poly_eq_zero q
| _, [] => poly_eq_zero p
| h :: t, h' :: t' => h = h' ∧ F t t'
end.
Lemma poly_eq_p_zero p: (p = 0) ↔ poly_eq_zero p.
Proof. now destruct p. Qed.
Instance: Reflexive poly_eq.
Proof with intuition. repeat intro. induction x... split... Qed.
Lemma poly_eq_cons :
∀ (a b : R) (p q : poly), (a = b /\ poly_eq p q) <-> poly_eq (a :: p) (b :: q).
Proof. easy. Qed.
Lemma poly_eq_ind (P: poly → poly → Prop)
(case_0: ∀ p p', poly_eq_zero p → poly_eq_zero p' → P p p')
(case_cons: ∀ x x' p p', x = x' → p = p' → P p p' → P (x::p) (x'::p'))
p: ∀ p', p = p' → P p p'.
Proof.
induction p as [|x p IH]; intros [|x' p'] eqxy.
1,2,3: now apply case_0.
destruct eqxy.
apply case_cons; auto.
Qed.
Lemma poly_eq_zero_trans p q: poly_eq_zero p → poly_eq_zero q → p = q.
Proof.
revert q.
induction p as [|x p IH]; intros ? eqp eqq; auto.
destruct q as [|y q]; auto.
rewrite poly_eq_zero_cons in *.
rewrite <- poly_eq_cons.
destruct eqp as [-> ?], eqq as [-> ?]; split; eauto.
now apply IH.
Qed.
Instance: Symmetric poly_eq.
Proof.
intros p p' eqp.
pattern p, p'; apply poly_eq_ind; auto; clear p p' eqp.
- now intros; apply poly_eq_zero_trans.
- intros ???? eqx eqp IH.
rewrite <- poly_eq_cons; auto.
Qed.
Instance poly_eq_zero_proper: Proper (poly_eq ==> iff) poly_eq_zero.
Proof.
apply proper_sym_impl_iff.
{ apply _. }
red; refine (poly_eq_ind _ _ _).
- intros; hnf; auto.
- unfold impl; intros ???? eqx eqp IH.
rewrite !poly_eq_zero_cons, eqx; tauto.
Qed.
Instance: Transitive poly_eq.
Proof.
intros ??? eqxy; revert z.
pattern x, y; refine (poly_eq_ind _ _ _ x y eqxy); clear x y eqxy.
{ intros x y x0 y0 z eqz.
apply poly_eq_zero_trans; auto.
now rewrite <- eqz. }
intros ???? eqx eqp IH z eqz.
destruct z as [|x'' p''].
{ eapply poly_eq_zero_proper; eauto.
now split. }
destruct eqz as [eqx' eqp']; split; eauto.
Qed.
Global Instance: Setoid poly.
Proof. split; try apply _. Qed.
Global Instance: Plus poly := fix F p q :=
match p, q with
| [], _ => q
| _, [] => p
| h :: t, h' :: t' => h + h' :: F t t'
end.
Lemma poly_eq_zero_plus_l p q: poly_eq_zero p → p + q = q.
Proof.
intro eqp; revert q.
induction eqp as [|x p eqx eqp IH] using poly_eq_zero_ind.
{ easy. }
intros [|y q].
{ cbn -[poly_eq_zero].
rewrite poly_eq_zero_cons; auto. }
cbn; split; auto.
ring [eqx].
Qed.
Instance plus_commutative: Commutative (+).
Proof with (try easy); cbn.
intro.
induction x as [|x p IH]; intros [|y q]...
split; auto; ring.
Qed.
Corollary poly_eq_zero_plus_r p q: poly_eq_zero q → p + q = p.
Proof.
rewrite commutativity.
apply poly_eq_zero_plus_l.
Qed.
Corollary poly_eq_zero_plus p q: poly_eq_zero p → poly_eq_zero q → poly_eq_zero (p+q).
Proof.
intro.
rewrite <- !poly_eq_p_zero; intro.
now rewrite poly_eq_zero_plus_l.
Qed.
Global Instance poly_plus_proper: Proper (poly_eq ==> poly_eq ==> poly_eq) (+).
Proof.
unfold Proper, respectful.
refine (poly_eq_ind _ _ _).
{ intros p p' zp zp' q q' eqq.
rewrite !poly_eq_zero_plus_l; auto. }
intros ???? eqx eqp IH.
refine (poly_eq_ind _ _ _).
{ intros q q' zq zq'.
rewrite !poly_eq_zero_plus_r; auto.
cbn; auto. }
intros y y' q q' eqy eqq _.
cbn; split; eauto.
ring [eqx eqy].
Qed.
Instance plus_associative: Associative (+).
Proof with try easy.
do 2 red; induction x as [|x p IH]...
intros [|y q]...
intros [|z r]...
cbn; split; auto.
ring.
Qed.
Instance plus_left_id: LeftIdentity (+) 0.
Proof. now intro; rewrite poly_eq_zero_plus_l. Qed.
Instance plus_right_id: RightIdentity (+) 0.
Proof. now intro; rewrite poly_eq_zero_plus_r. Qed.
Instance poly_plus_monoid: Monoid poly.
Proof. repeat (split; try apply _). Qed.
Global Instance: Negate poly := map (-).
Lemma poly_negate_zero p: poly_eq_zero p ↔ poly_eq_zero (-p).
Proof.
induction p as [|x p IH].
{ easy. }
cbn.
rewrite !poly_eq_zero_cons, IH.
enough (x = 0 ↔ -x = 0) by tauto.
split; intro eq0; ring [eq0].
Qed.
Instance poly_negate_proper: Proper (poly_eq ==> poly_eq) (-).
Proof.
refine (poly_eq_ind _ _ _).
{ now intros ?? ->%poly_negate_zero%poly_eq_p_zero ->%poly_negate_zero%poly_eq_p_zero. }
intros ???? eqx eqp IH.
cbn; split; eauto.
Qed.
Instance poly_negate_l: LeftInverse (+) (-) 0.
Proof.
intro; rewrite poly_eq_p_zero.
induction x as [|x p IH]; cbn.
{ easy. }
rewrite poly_eq_zero_cons; split; auto.
ring.
Qed.
Instance poly_negate_r: RightInverse (+) (-) 0.
Proof. now intro; rewrite commutativity, left_inverse. Qed.
Instance poly_plus_abgroup: AbGroup poly.
Proof. repeat (split; try apply _). Qed.
Fixpoint poly_mult_cr (q: poly) (c: R): poly :=
match q with
| [] => 0
| d :: q1 => c*d :: poly_mult_cr q1 c
end.
Lemma poly_mult_cr_0_l q c: poly_eq_zero q → poly_eq_zero (poly_mult_cr q c).
Proof.
induction q as [|x q IH].
{ easy. }
cbn.
rewrite !poly_eq_zero_cons.
intros [-> ?]; split; auto.
ring.
Qed.
Instance poly_mult_cr_proper: Proper ((=) ==> (=) ==> (=)) poly_mult_cr.
Proof.
intros p p' eqp c c' eqc.
revert p p' eqp; refine (poly_eq_ind _ _ _).
{ now intros; apply poly_eq_zero_trans; apply poly_mult_cr_0_l. }
intros ???? eqx eqp IH.
split; auto; cbn.
ring [eqx eqc].
Qed.
Lemma poly_mult_cr_1_l x: poly_mult_cr 1 x = [x].
Proof. cbn; split; [ring|easy]. Qed.
Instance poly_mult_cr_1_r: RightIdentity poly_mult_cr 1.
Proof.
red; induction x as [|x p IH]; [easy|cbn].
split; auto; ring.
Qed.
Instance poly_mult_cr_dist_l: LeftHeteroDistribute poly_mult_cr (+) (+).
Proof.
intros x a b.
induction x as [|x p IH]; [easy|cbn].
split; auto; ring.
Qed.
Instance poly_mult_cr_dist_r: RightHeteroDistribute poly_mult_cr (+) (+).
Proof.
intros p q a.
revert q.
induction p as [|x p IH]; intros [|y q]; [easy..|cbn].
split; auto; ring.
Qed.
Instance poly_mult_cr_assoc: HeteroAssociative poly_mult_cr (.*.) poly_mult_cr poly_mult_cr.
Proof.
intros x a b.
induction x as [|p x IH]; [easy|cbn].
split; auto; ring.
Qed.
Lemma poly_mult_cr_0_r q c: c = 0 → poly_eq_zero (poly_mult_cr q c).
Proof.
intros ->.
induction q as [|x q IH]; [easy|cbn].
rewrite poly_eq_zero_cons; split; auto.
ring.
Qed.
Global Instance: Mult poly := fix F p q :=
match p with
| [] => 0
| c :: p1 => poly_mult_cr q c + (0 :: F p1 q)
end.
Lemma poly_mult_0_l p q: poly_eq_zero p → poly_eq_zero (p * q).
Proof.
induction 1 using poly_eq_zero_ind; [easy|cbn].
apply poly_eq_zero_plus.
- now apply poly_mult_cr_0_r.
- rewrite poly_eq_zero_cons; auto.
Qed.
Lemma poly_mult_0_r p q: poly_eq_zero q → poly_eq_zero (p * q).
Proof.
induction p as [|x p IH]; [easy|cbn].
intro eq0.
apply poly_eq_zero_plus.
- now apply poly_mult_cr_0_l.
- rewrite poly_eq_zero_cons; auto.
Qed.
Instance poly_mult_proper: Proper ((=) ==> (=) ==> (=)) (.*.).
Proof.
refine (poly_eq_ind _ _ _).
{ intros ?? zp zp' q q' eqq.
now apply poly_eq_zero_trans; apply poly_mult_0_l. }
intros ???? eqx eqp IH q q' eqq.
cbn.
apply poly_plus_proper.
{ now rewrite eqx, eqq. }
split; auto.
now apply IH.
Qed.
Instance poly_mult_left_distr: LeftDistribute (.*.) (+).
Proof.
intros p q r.
induction p as [|x p IH]; [easy|cbn].
rewrite (distribute_r q r x).
rewrite <- !associativity; apply poly_plus_proper; [easy|].
rewrite associativity, (commutativity (0::p*q)), <- associativity.
apply poly_plus_proper; [easy|].
cbn; split; [ring|easy].
Qed.
Lemma poly_mult_cons_r p q x: p * (x::q) = poly_mult_cr p x + (0 :: p * q).
Proof.
induction p as [|y p IH]; cbn; auto.
split; auto.
rewrite IH, !associativity, (commutativity (poly_mult_cr _ _)).
split; try easy.
ring.
Qed.
Instance poly_mult_comm: Commutative (.*.).
Proof.
intros p.
induction p as [|x p IH].
{ cbn; intro.
now apply poly_mult_0_r. }
intros [|y q]; cbn.
{ rewrite poly_eq_zero_cons; split; auto.
now apply poly_mult_0_r. }
split. 1: ring.
rewrite !poly_mult_cons_r, !associativity.
apply poly_plus_proper.
{ apply commutativity. }
rewrite <- poly_eq_cons; split; auto.
apply IH.
Qed.
Instance poly_mult_right_distr: RightDistribute (.*.) (+).
Proof.
intros p q r.
now rewrite commutativity, distribute_l, !(commutativity r).
Qed.
Instance poly_mult_1_l: LeftIdentity (.*.) 1.
Proof.
intro; cbn.
rewrite poly_mult_cr_1_r, poly_eq_zero_plus_r; auto.
now split.
Qed.
Instance poly_mult_1_r: RightIdentity (.*.) 1.
Proof.
intro; rewrite commutativity; apply left_identity.
Qed.
Instance poly_mult_assoc: Associative (.*.).
Proof with (try easy); cbn.
intros x.
induction x as [|x p IH]...
intros q r; cbn.
rewrite distribute_r.
apply poly_plus_proper; cbn -[poly_eq].
{ clear IH.
induction q as [|y q IH]...
rewrite distribute_r, <- associativity, (commutativity x y).
apply poly_plus_proper...
split; auto.
ring. }
assert (poly_mult_cr r 0 = 0) as ->.
{ now rewrite poly_eq_p_zero; apply poly_mult_cr_0_r. }
cbn; split; eauto.
now rewrite IH.
Qed.
Global Instance poly_ring: Ring poly.
Proof. repeat (split; try apply _). Qed.
End contents.