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.
  Admitted.

  Instance: Transitive poly_eq.
  Admitted.

  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.
  Admitted.

End contents.