# implementations.polynomials

Require Import
List
abstract_algebra.

Section contents.
Context R `{Ring R}.

Definition poly := list R.

Coercion poly_constant (c : R) : poly := [c].

Global Instance poly_zero: RingZero poly := [].
Global Instance poly_one: RingOne poly := poly_constant 1.

Definition all (l: list Prop): Prop := fold_left and l True.

Definition poly_eq_zero: poly Prop := all map ((=) 0).

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.

Instance: Reflexive poly_eq.

Instance: Symmetric poly_eq.

Instance: Transitive poly_eq.

Global Instance: Setoid poly.

Global Instance: RingPlus poly := fix F p q :=
match p, q with
| [], _ => q
| _, [] => p
| h :: t, h' :: t' => h + h' :: F t t'
end.

Global Instance: GroupInv poly := map (-).

Fixpoint poly_mult_cr (q: poly) (c: R): poly :=
match q with
| [] => 0
| d :: q1 => c*d :: poly_mult_cr q1 c
end.

Global Instance: RingMult poly := fix F p q :=
match p with
| [] => 0
| c :: p1 => poly_mult_cr q c + (0 :: F p1 q)
end.

Global Instance: Ring poly.