CoRN.algebra.CPolynomials



Require Import CRing_Homomorphisms.
Require Import Rational.

Polynomials

The first section only proves the polynomials form a ring. Section gives some basic properties of equality and induction of polynomials.

Definition of polynomials; they form a ring


Section CPoly_CRing.
Let CR be a ring.

Variable CR : CRing.

The intuition behind the type cpoly is the following

Inductive cpoly : Type :=
  | cpoly_zero : cpoly
  | cpoly_linear : CRcpolycpoly.

Definition cpoly_constant (c : CR) : cpoly := cpoly_linear c cpoly_zero.

Definition cpoly_one : cpoly := cpoly_constant [1].

Some useful induction lemmas for doubly quantified propositions.

Lemma Ccpoly_double_ind0 : P : cpolycpolyCProp,
 ( p, P p cpoly_zero) → ( p, P cpoly_zero p) →
 ( p q c d, P p qP (cpoly_linear c p) (cpoly_linear d q)) → p q, P p q.
Proof.
 simple induction p; auto.
 simple induction q; auto.
Qed.

Lemma Ccpoly_double_sym_ind0 : P : cpolycpolyCProp,
 Csymmetric P → ( p, P p cpoly_zero) →
( p q c d, P p qP (cpoly_linear c p) (cpoly_linear d q)) → p q, P p q.
Proof.
 intros.
 apply Ccpoly_double_ind0; auto.
Qed.

Lemma Ccpoly_double_ind0' : P : cpolycpolyCProp,
 ( p, P cpoly_zero p) → ( p c, P (cpoly_linear c p) cpoly_zero) →
 ( p q c d, P p qP (cpoly_linear c p) (cpoly_linear d q)) → p q, P p q.
Proof.
 simple induction p; auto.
 simple induction q; auto.
Qed.

Lemma cpoly_double_ind0 : P : cpolycpolyProp,
 ( p, P p cpoly_zero) → ( p, P cpoly_zero p) →
 ( p q c d, P p qP (cpoly_linear c p) (cpoly_linear d q)) → p q, P p q.
Proof.
 simple induction p; auto.
 simple induction q; auto.
Qed.

Lemma cpoly_double_sym_ind0 : P : cpolycpolyProp,
 Tsymmetric P → ( p, P p cpoly_zero) →
 ( p q c d, P p qP (cpoly_linear c p) (cpoly_linear d q)) → p q, P p q.
Proof.
 intros.
 apply cpoly_double_ind0; auto.
Qed.

Lemma cpoly_double_ind0' : P : cpolycpolyProp,
 ( p, P cpoly_zero p) → ( p c, P (cpoly_linear c p) cpoly_zero) →
 ( p q c d, P p qP (cpoly_linear c p) (cpoly_linear d q)) → p q, P p q.
Proof.
 simple induction p; auto.
 simple induction q; auto.
Qed.

The polynomials form a setoid

Fixpoint cpoly_eq_zero (p : cpoly) : Prop :=
  match p with
  | cpoly_zeroTrue
  | cpoly_linear c p1c [=] [0] cpoly_eq_zero p1
  end.

Fixpoint cpoly_eq (p q : cpoly) {struct p} : Prop :=
  match p with
  | cpoly_zerocpoly_eq_zero q
  | cpoly_linear c p1
      match q with
      | cpoly_zerocpoly_eq_zero p
      | cpoly_linear d q1c [=] d cpoly_eq p1 q1
      end
  end.

Lemma cpoly_eq_p_zero : p, cpoly_eq p cpoly_zero = cpoly_eq_zero p.
Proof.
 simple induction p; auto.
Qed.

Fixpoint cpoly_ap_zero (p : cpoly) : CProp :=
  match p with
  | cpoly_zeroFalse
  | cpoly_linear c p1c [#] [0] or cpoly_ap_zero p1
  end.

Fixpoint cpoly_ap (p q : cpoly) {struct p} : CProp :=
  match p with
  | cpoly_zerocpoly_ap_zero q
  | cpoly_linear c p1
      match q with
      | cpoly_zerocpoly_ap_zero p
      | cpoly_linear d q1c [#] d or cpoly_ap p1 q1
      end
  end.

Lemma cpoly_ap_p_zero : p, cpoly_ap_zero p = cpoly_ap p cpoly_zero.
Proof.
 simple induction p; auto.
Qed.

Lemma irreflexive_cpoly_ap : irreflexive cpoly_ap.
Proof.
 red in |- ×.
 intro p; induction p as [| s p Hrecp].
  intro H; elim H.
 intro H.
 elim H.
  apply ap_irreflexive_unfolded.
 assumption.
Qed.

Lemma symmetric_cpoly_ap : Csymmetric cpoly_ap.
Proof.
 red in |- ×.
 intros x y.
 pattern x, y in |- ×.
 apply Ccpoly_double_ind0'.
   simpl in |- *; simple induction p; auto.
  simpl in |- *; auto.
 simpl in |- ×.
 intros p q c d H H0.
 elim H0; intro H1.
  left.
  apply ap_symmetric_unfolded.
  assumption.
 auto.
Qed.

Lemma cotransitive_cpoly_ap : cotransitive cpoly_ap.
Proof.
 red in |- ×.
 intros x y.
 pattern x, y in |- ×.
 apply Ccpoly_double_sym_ind0.
   red in |- *; intros p q H H0 r.
   generalize (symmetric_cpoly_ap _ _ H0); intro H1.
   elim (H H1 r); intro H2; [ right | left ]; apply symmetric_cpoly_ap; assumption.
  simpl in |- *; intros p H z.
  generalize H.
  pattern p, z in |- ×.
  apply Ccpoly_double_ind0'.
    simpl in |- *; intros q H0; elim H0.
   simpl in |- *; auto.
  simpl in |- *; intros r q c d H0 H1.
  elim H1; intro H2.
   generalize (ap_cotransitive_unfolded _ _ _ H2 d); intro H3.
   elim H3; auto.
  rewrite cpoly_ap_p_zero in H2.
  elim (H0 H2); auto.
  right; right; rewrite cpoly_ap_p_zero; assumption.
 intros p q c d H H0 r.
 simpl in H0.
 elim H0; intro H1.
  induction r as [| s r Hrecr].
   simpl in |- ×.
   generalize (ap_cotransitive_unfolded _ _ _ H1 [0]); intro H2.
   elim H2; auto.
   intro H3.
   right; left; apply ap_symmetric_unfolded; assumption.
  simpl in |- ×.
  generalize (ap_cotransitive_unfolded _ _ _ H1 s); intro H2.
  elim H2; auto.
 induction r as [| s r Hrecr].
  simpl in |- ×.
  cut (cpoly_ap_zero p or cpoly_ap_zero q).
   intro H2; elim H2; auto.
  generalize H1; pattern p, q in |- *; apply Ccpoly_double_ind0.
    simpl in |- ×.
    intros r H2.
    left; rewrite cpoly_ap_p_zero; assumption.
   auto.
  simpl in |- ×.
  intros p0 q0 c0 d0 H2 H3.
  elim H3; intro H4.
   elim (ap_cotransitive_unfolded _ _ _ H4 [0]); intro H5.
    auto.
   right; left; apply ap_symmetric_unfolded; assumption.
  elim (H2 H4); auto.
 simpl in |- ×.
 elim (H H1 r); auto.
Qed.

Lemma tight_apart_cpoly_ap : tight_apart cpoly_eq cpoly_ap.
Proof.
 red in |- ×.
 intros x y.
 pattern x, y in |- ×.
 apply cpoly_double_ind0'.
   simple induction p.
    simpl in |- ×.
    unfold iff in |- ×.
    unfold Not in |- ×.
    split.
     auto.
    intros H H0; inversion H0.
   simpl in |- ×.
   intros s c H.
   cut (Not (s [#] [0]) s [=] [0]).
    unfold Not in |- ×.
    intro H0.
    elim H0; intros H1 H2.
    split.
     intro H3.
     split; auto.
     elim H; intros H4 H5.
     apply H4.
     intro H6.
     auto.
    intros H3 H4.
    elim H3; intros H5 H6.
    elim H4; intros H7.
     auto.
    elim H; intros H8 H9.
    unfold Not in H8.
    elim H9; assumption.
   apply (ap_tight CR).
  simple induction p.
   simpl in |- ×.
   intro c.
   cut (Not (c [#] [0]) c [=] [0]).
    unfold Not in |- ×.
    intro H.
    elim H; intros H0 H1.
    split.
     auto.
    intros H2 H3.
    elim H3; intro H4.
     tauto.
    elim H4.
   apply (ap_tight CR).
  simpl in |- ×.
  intros s c H d.
  generalize (H d).
  generalize (ap_tight CR d [0]).
  generalize (ap_tight CR s [0]).
  unfold Not in |- ×.
  intros H0 H1 H2.
  elim H0; clear H0; intros H3 H4.
  elim H1; clear H1; intros H0 H5.
  elim H2; clear H2; intros H1 H6.
  tauto.
 simpl in |- ×.
 unfold Not in |- ×.
 intros p q c d H.
 elim H; intros H0 H1.
 split.
  intro H2.
  split.
   generalize (ap_tight CR c d).
   unfold Not in |- *; tauto.
  tauto.
 intros H2 H3.
 elim H3.
  elim H2.
  intros H4 H5 H6.
  generalize (ap_tight CR c d).
  unfold Not in |- ×.
  tauto.
 elim H2.
 auto.
Qed.

Lemma cpoly_is_CSetoid : is_CSetoid _ cpoly_eq cpoly_ap.
Proof.
 apply Build_is_CSetoid.
    exact irreflexive_cpoly_ap.
   exact symmetric_cpoly_ap.
  exact cotransitive_cpoly_ap.
 exact tight_apart_cpoly_ap.
Qed.

Definition cpoly_csetoid := Build_CSetoid _ _ _ cpoly_is_CSetoid.
Canonical Structure cpoly_csetoid.
Canonical Structure cpoly_setoid := cs_crr cpoly_csetoid.

Now that we know that the polynomials form a setoid, we can use the notation with [#] and [=] . In order to use this notation, we introduce cpoly_zero_cs and cpoly_linear_cs, so that Coq recognizes we are talking about a setoid. We formulate the induction properties and the most basic properties of equality and apartness in terms of these generators.

Let cpoly_zero_cs : cpoly_csetoid := cpoly_zero.

Let cpoly_linear_cs c (p : cpoly_csetoid) : cpoly_csetoid := cpoly_linear c p.

Lemma Ccpoly_ind_cs : P : cpoly_csetoidCProp,
 P cpoly_zero_cs → ( p c, P pP (cpoly_linear_cs c p)) → p, P p.
Proof.
 simple induction p; auto.
Qed.

Lemma Ccpoly_double_ind0_cs : P : cpoly_csetoidcpoly_csetoidCProp,
 ( p, P p cpoly_zero_cs) → ( p, P cpoly_zero_cs p) →
 ( p q c d, P p qP (cpoly_linear_cs c p) (cpoly_linear_cs d q)) → p q, P p q.
Proof.
 simple induction p.
  auto.
 simple induction q.
  auto.
 simpl in X1.
 unfold cpoly_linear_cs in X1.
 auto.
Qed.

Lemma Ccpoly_double_sym_ind0_cs : P : cpoly_csetoidcpoly_csetoidCProp,
 Csymmetric P → ( p, P p cpoly_zero_cs) →
 ( p q c d, P p qP (cpoly_linear_cs c p) (cpoly_linear_cs d q)) → p q, P p q.
Proof.
 intros.
 apply Ccpoly_double_ind0; auto.
Qed.

Lemma cpoly_ind_cs : P : cpoly_csetoidProp,
 P cpoly_zero_cs → ( p c, P pP (cpoly_linear_cs c p)) → p, P p.
Proof.
 simple induction p; auto.
Qed.

Lemma cpoly_double_ind0_cs : P : cpoly_csetoidcpoly_csetoidProp,
 ( p, P p cpoly_zero_cs) → ( p, P cpoly_zero_cs p) →
 ( p q c d, P p qP (cpoly_linear_cs c p) (cpoly_linear_cs d q)) → p q, P p q.
Proof.
 simple induction p.
  auto.
 simple induction q.
  auto.
 simpl in H1.
 unfold cpoly_linear_cs in H1.
 auto.
Qed.

Lemma cpoly_double_sym_ind0_cs : P : cpoly_csetoidcpoly_csetoidProp,
 Tsymmetric P → ( p, P p cpoly_zero_cs) →
 ( p q c d, P p qP (cpoly_linear_cs c p) (cpoly_linear_cs d q)) → p q, P p q.
Proof.
 intros.
 apply cpoly_double_ind0; auto.
Qed.

Lemma cpoly_lin_eq_zero_ : p c,
 cpoly_linear_cs c p [=] cpoly_zero_csc [=] [0] p [=] cpoly_zero_cs.
Proof.
 unfold cpoly_linear_cs in |- ×.
 unfold cpoly_zero_cs in |- ×.
 simpl in |- ×.
 intros p c H.
 elim H; intros.
 split; auto.
 rewrite cpoly_eq_p_zero.
 assumption.
Qed.

Lemma _cpoly_lin_eq_zero : p c,
 c [=] [0] p [=] cpoly_zero_cscpoly_linear_cs c p [=] cpoly_zero_cs.
Proof.
 unfold cpoly_linear_cs in |- ×.
 unfold cpoly_zero_cs in |- ×.
 simpl in |- ×.
 intros p c H.
 elim H; intros.
 split; auto.
 rewrite <- cpoly_eq_p_zero.
 assumption.
Qed.

Lemma cpoly_zero_eq_lin_ : p c,
 cpoly_zero_cs [=] cpoly_linear_cs c pc [=] [0] cpoly_zero_cs [=] p.
Proof.
 auto.
Qed.

Lemma _cpoly_zero_eq_lin : p c,
 c [=] [0] cpoly_zero_cs [=] pcpoly_zero_cs [=] cpoly_linear_cs c p.
Proof.
 auto.
Qed.

Lemma cpoly_lin_eq_lin_ : p q c d,
 cpoly_linear_cs c p [=] cpoly_linear_cs d qc [=] d p [=] q.
Proof.
 auto.
Qed.

Lemma _cpoly_lin_eq_lin : p q c d,
 c [=] d p [=] qcpoly_linear_cs c p [=] cpoly_linear_cs d q.
Proof.
 auto.
Qed.

Lemma cpoly_lin_ap_zero_ : p c,
 cpoly_linear_cs c p [#] cpoly_zero_csc [#] [0] or p [#] cpoly_zero_cs.
Proof.
 unfold cpoly_zero_cs in |- ×.
 intros p c H.
 cut (cpoly_ap (cpoly_linear c p) cpoly_zero); auto.
 intro H0.
 simpl in H0.
 elim H0; auto.
 right.
 rewrite <- cpoly_ap_p_zero.
 assumption.
Qed.

Lemma _cpoly_lin_ap_zero : p c,
 c [#] [0] or p [#] cpoly_zero_cscpoly_linear_cs c p [#] cpoly_zero_cs.
Proof.
 unfold cpoly_zero_cs in |- ×.
 intros.
 simpl in |- ×.
 elim X; try auto.
 intros.
 right.
 rewrite cpoly_ap_p_zero.
 assumption.
Qed.

Lemma cpoly_lin_ap_zero : p c,
 (cpoly_linear_cs c p [#] cpoly_zero_cs) = (c [#] [0] or p [#] cpoly_zero_cs).
Proof.
 intros.
 simpl in |- ×.
 unfold cpoly_zero_cs in |- ×.
 rewrite cpoly_ap_p_zero.
 reflexivity.
Qed.

Lemma cpoly_zero_ap_lin_ : p c,
 cpoly_zero_cs [#] cpoly_linear_cs c pc [#] [0] or cpoly_zero_cs [#] p.
Proof.
 intros.
 simpl in |- ×.
 assumption.
Qed.

Lemma _cpoly_zero_ap_lin : p c,
 c [#] [0] or cpoly_zero_cs [#] pcpoly_zero_cs [#] cpoly_linear_cs c p.
Proof.
 intros.
 simpl in |- ×.
 assumption.
Qed.

Lemma cpoly_zero_ap_lin : p c,
 (cpoly_zero_cs [#] cpoly_linear_cs c p) = (c [#] [0] or cpoly_zero_cs [#] p).
Proof. reflexivity. Qed.

Lemma cpoly_lin_ap_lin_ : p q c d,
 cpoly_linear_cs c p [#] cpoly_linear_cs d qc [#] d or p [#] q.
Proof. auto. Qed.

Lemma _cpoly_lin_ap_lin : p q c d,
 c [#] d or p [#] qcpoly_linear_cs c p [#] cpoly_linear_cs d q.
Proof. auto. Qed.

Lemma cpoly_lin_ap_lin : p q c d,
 (cpoly_linear_cs c p [#] cpoly_linear_cs d q) = (c [#] d or p [#] q).
Proof. reflexivity. Qed.

Lemma cpoly_linear_strext : bin_fun_strext _ _ _ cpoly_linear_cs.
Proof.
 unfold bin_fun_strext in |- ×.
 intros until 1.
 apply cpoly_lin_ap_lin_;assumption.
Qed.

Lemma cpoly_linear_wd : bin_fun_wd _ _ _ cpoly_linear_cs.
Proof.
 apply bin_fun_strext_imp_wd. now repeat intro.
Qed.

Definition cpoly_linear_fun := Build_CSetoid_bin_fun _ _ _ _ cpoly_linear_strext.

Lemma Ccpoly_double_comp_ind : P : cpoly_csetoidcpoly_csetoidCProp,
 ( p1 p2 q1 q2, p1 [=] p2q1 [=] q2P p1 q1P p2 q2) →
 P cpoly_zero_cs cpoly_zero_cs
 ( p q c d, P p qP (cpoly_linear_cs c p) (cpoly_linear_cs d q)) → p q, P p q.
Proof.
 intros.
 apply Ccpoly_double_ind0_cs.
   intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs;[assumption|].
   intros p1 c. intros.
   apply X with (cpoly_linear_cs c p1) (cpoly_linear_cs [0] cpoly_zero_cs).
     algebra.
    apply _cpoly_lin_eq_zero.
    split; algebra.
   apply X1; assumption.
  intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs.
   assumption.
  intros.
  apply X with (cpoly_linear_cs [0] cpoly_zero_cs) (cpoly_linear_cs c p1).
    apply _cpoly_lin_eq_zero;split; algebra.
   algebra.
  apply X1; assumption.
 now apply X1.
Qed.

Lemma Ccpoly_triple_comp_ind :
  P : cpoly_csetoidcpoly_csetoidcpoly_csetoidCProp,
 ( p1 p2 q1 q2 r1 r2,
  p1 [=] p2q1 [=] q2r1 [=] r2P p1 q1 r1P p2 q2 r2) →
 P cpoly_zero_cs cpoly_zero_cs cpoly_zero_cs
 ( p q r c d e,
  P p q rP (cpoly_linear_cs c p) (cpoly_linear_cs d q) (cpoly_linear_cs e r)) →
  p q r, P p q r.
Proof.
 do 6 intro.
 pattern p, q in |- ×.
 apply Ccpoly_double_comp_ind.
   intros.
   apply X with p1 q1 r.
      assumption.
     assumption.
    algebra.
   apply X2.
  intro r; pattern r in |- *; apply Ccpoly_ind_cs.
   assumption.
  intros.
  apply X with (cpoly_linear_cs [0] cpoly_zero_cs) (cpoly_linear_cs [0] cpoly_zero_cs)
    (cpoly_linear_cs c p0).
     apply _cpoly_lin_eq_zero; split; algebra.
    apply _cpoly_lin_eq_zero; split; algebra.
   algebra.
  apply X1.
  assumption.
 do 6 intro.
 pattern r in |- *; apply Ccpoly_ind_cs.
  apply X with (cpoly_linear_cs c p0) (cpoly_linear_cs d q0) (cpoly_linear_cs [0] cpoly_zero_cs).
     algebra.
    algebra.
   apply _cpoly_lin_eq_zero; split; algebra.
  apply X1.
  apply X2.
 intros.
 apply X1.
 apply X2.
Qed.

Lemma cpoly_double_comp_ind : P : cpoly_csetoidcpoly_csetoidProp,
 ( p1 p2 q1 q2, p1 [=] p2q1 [=] q2P p1 q1P p2 q2) →
 P cpoly_zero_cs cpoly_zero_cs
 ( p q c d, P p qP (cpoly_linear_cs c p) (cpoly_linear_cs d q)) → p q, P p q.
Proof.
 intros.
 apply cpoly_double_ind0_cs.
   intro p0; pattern p0 in |- *; apply cpoly_ind_cs.
    assumption.
   intros.
   apply H with (cpoly_linear_cs c p1) (cpoly_linear_cs [0] cpoly_zero_cs).
     algebra.
    apply _cpoly_lin_eq_zero.
    split; algebra.
   apply H1.
   assumption.
  intro p0; pattern p0 in |- *; apply cpoly_ind_cs.
   assumption.
  intros.
  apply H with (cpoly_linear_cs [0] cpoly_zero_cs) (cpoly_linear_cs c p1).
    apply _cpoly_lin_eq_zero.
    split; algebra.
   algebra.
  now apply H1.
 now apply H1.
Qed.

Lemma cpoly_triple_comp_ind :
  P : cpoly_csetoidcpoly_csetoidcpoly_csetoidProp,
 ( p1 p2 q1 q2 r1 r2,
  p1 [=] p2q1 [=] q2r1 [=] r2P p1 q1 r1P p2 q2 r2) →
 P cpoly_zero_cs cpoly_zero_cs cpoly_zero_cs
 ( p q r c d e,
  P p q rP (cpoly_linear_cs c p) (cpoly_linear_cs d q) (cpoly_linear_cs e r)) →
  p q r, P p q r.
Proof.
 do 6 intro.
 pattern p, q in |- ×.
 apply cpoly_double_comp_ind.
   intros.
   apply H with p1 q1 r.
      assumption.
     assumption.
    algebra.
   apply H4.
  intro r; pattern r in |- *; apply cpoly_ind_cs.
   assumption.
  intros.
  apply H with (cpoly_linear_cs [0] cpoly_zero_cs) (cpoly_linear_cs [0] cpoly_zero_cs)
    (cpoly_linear_cs c p0).
     apply _cpoly_lin_eq_zero; split; algebra.
    apply _cpoly_lin_eq_zero; split; algebra.
   algebra.
  apply H1.
  assumption.
 do 6 intro.
 pattern r in |- *; apply cpoly_ind_cs.
  apply H with (cpoly_linear_cs c p0) (cpoly_linear_cs d q0) (cpoly_linear_cs [0] cpoly_zero_cs).
     algebra.
    algebra.
   apply _cpoly_lin_eq_zero; split; algebra.
  apply H1.
  apply H2.
 intros.
 apply H1.
 apply H2.
Qed.

The polynomials form a semi-group and a monoid


Fixpoint cpoly_plus (p q : cpoly) {struct p} : cpoly :=
  match p with
  | cpoly_zeroq
  | cpoly_linear c p1
      match q with
      | cpoly_zerop
      | cpoly_linear d q1cpoly_linear (c[+]d) (cpoly_plus p1 q1)
      end
  end.

Definition cpoly_plus_cs (p q : cpoly_csetoid) : cpoly_csetoid := cpoly_plus p q.

Lemma cpoly_zero_plus : p, cpoly_plus_cs cpoly_zero_cs p = p.
Proof.
 auto.
Qed.

Lemma cpoly_plus_zero : p, cpoly_plus_cs p cpoly_zero_cs = p.
Proof.
 simple induction p.
  auto.
 auto.
Qed.

Lemma cpoly_lin_plus_lin : p q c d,
 cpoly_plus_cs (cpoly_linear_cs c p) (cpoly_linear_cs d q) =
  cpoly_linear_cs (c[+]d) (cpoly_plus_cs p q).
Proof.
 auto.
Qed.

Lemma cpoly_plus_commutative : p q, cpoly_plus_cs p q [=] cpoly_plus_cs q p.
Proof.
 intros.
 pattern p, q in |- ×.
 apply cpoly_double_sym_ind0_cs.
   unfold Tsymmetric in |- ×.
   intros.
   algebra.
  intro p0.
  rewrite cpoly_zero_plus.
  rewrite cpoly_plus_zero.
  algebra.
 intros.
 repeat rewrite cpoly_lin_plus_lin.
 apply _cpoly_lin_eq_lin.
 split.
  algebra.
 assumption.
Qed.

Lemma cpoly_plus_q_ap_q : p q, cpoly_plus_cs p q [#] qp [#] cpoly_zero_cs.
Proof.
 intro p; pattern p in |- *; apply Ccpoly_ind_cs.
  intro.
  rewrite cpoly_zero_plus.
  intro H.
  elimtype False.
  apply (ap_irreflexive _ _ H).
 do 4 intro.
 pattern q in |- *; apply Ccpoly_ind_cs.
  rewrite cpoly_plus_zero.
  auto.
 do 3 intro.
 rewrite cpoly_lin_plus_lin.
 intros.
 cut (c[+]c0 [#] c0 or cpoly_plus_cs p0 p1 [#] p1).
  intros.
  2: apply cpoly_lin_ap_lin_.
  2: assumption.
 cut (c [#] [0] or p0 [#] cpoly_zero_cs).
  intro. apply _cpoly_lin_ap_zero. assumption.
  elim X1; intro.
  left.
  apply cg_ap_cancel_rht with c0.
  astepr c0. auto.
  right.
 generalize (X _ b); intro.
 assumption.
Qed.

Lemma cpoly_p_plus_ap_p : p q, cpoly_plus_cs p q [#] pq [#] cpoly_zero.
Proof.
 intros.
 apply cpoly_plus_q_ap_q with p.
 apply ap_wdl_unfolded with (cpoly_plus_cs p q).
  assumption.
 apply cpoly_plus_commutative.
Qed.

Lemma cpoly_ap_zero_plus : p q,
 cpoly_plus_cs p q [#] cpoly_zero_csp [#] cpoly_zero_cs or q [#] cpoly_zero_cs.
Proof.
 intros p q; pattern p, q in |- *; apply Ccpoly_double_sym_ind0_cs.
   unfold Csymmetric in |- ×.
   intros x y H H0.
   elim H.
     auto. auto.
    astepl (cpoly_plus_cs y x). auto.
    apply cpoly_plus_commutative.
  intros p0 H.
  left.
  rewrite cpoly_plus_zero in H.
  assumption.
 intros p0 q0 c d.
 rewrite cpoly_lin_plus_lin.
 intros.
 cut (c[+]d [#] [0] or cpoly_plus_cs p0 q0 [#] cpoly_zero_cs).
  2: apply cpoly_lin_ap_zero_.
  2: assumption.
 clear X0.
 intros H0.
 elim H0; intro H1.
  cut (c[+]d [#] [0][+][0]).
   intro H2.
   elim (cs_bin_op_strext _ _ _ _ _ _ H2); intro H3.
    left.
    simpl in |- ×.
    left.
    assumption.
   right.
   cut (d [#] [0] or q0 [#] cpoly_zero_cs).
    intro H4.
    apply _cpoly_lin_ap_zero.
    auto.
   left.
   assumption.
  astepr ([0]:CR). auto.
  elim (X H1); intro.
  left.
  cut (c [#] [0] or p0 [#] cpoly_zero_cs).
   intro; apply _cpoly_lin_ap_zero.
   auto.
  right.
  assumption.
 right.
 cut (d [#] [0] or q0 [#] cpoly_zero_cs).
  intro.
  apply _cpoly_lin_ap_zero.
  auto.
 right.
 assumption.
Qed.

Lemma cpoly_plus_op_strext : bin_op_strext cpoly_csetoid cpoly_plus_cs.
Proof.
 unfold bin_op_strext in |- ×.
 unfold bin_fun_strext in |- ×.
 intros x1 x2.
 pattern x1, x2 in |- ×.
 apply Ccpoly_double_sym_ind0_cs.
   unfold Csymmetric in |- ×.
   intros.
   generalize (ap_symmetric_unfolded _ _ _ X0); intro H1.
   generalize (X _ _ H1); intro H2.
   elim H2; intro H3; generalize (ap_symmetric_unfolded _ _ _ H3); auto.
  intro p; pattern p in |- *; apply Ccpoly_ind_cs.
   intro; intro H.
   simpl in |- *; auto.
  intros s c H y1 y2.
  pattern y1, y2 in |- ×.
  apply Ccpoly_double_ind0_cs.
    intros p0 H0.
    apply cpoly_ap_zero_plus.
    apply H0.
   intro p0.
   intro H0.
   elim (ap_cotransitive _ _ _ H0 cpoly_zero_cs); auto.
  do 4 intro.
  intros.
  cut (c[+]c0 [#] d or cpoly_plus_cs s p0 [#] q).
   2: apply cpoly_lin_ap_lin_; assumption.
  clear X0; intro H1.
  elim H1; intro H2.
   cut (c[+]c0 [#] [0][+]d).
    intro H3.
    elim (cs_bin_op_strext _ _ _ _ _ _ H3).
     intro H4.
     left.
     apply _cpoly_lin_ap_zero.
     auto.
    intro.
    right.
    apply _cpoly_lin_ap_lin.
    auto.
   astepr d. auto.
   elim (H _ _ H2); auto.
   intro.
   left.
   apply _cpoly_lin_ap_zero.
   auto.
  right.
  apply _cpoly_lin_ap_lin.
  auto.
 do 7 intro.
 pattern y1, y2 in |- ×.
 apply Ccpoly_double_ind0_cs.
   intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs.
    auto.
   intros.
   cut (c[+]c0 [#] d or cpoly_plus_cs p p1 [#] q).
    intro H2.
    2: apply cpoly_lin_ap_lin_.
    2: auto.
   elim H2; intro H3.
    cut (c[+]c0 [#] d[+][0]).
     intro H4.
     elim (cs_bin_op_strext _ _ _ _ _ _ H4).
      intro.
      left.
      apply _cpoly_lin_ap_lin.
      auto.
     intro.
     right.
     apply _cpoly_lin_ap_zero.
     auto.
    astepr d. auto.
    elim X with p1 cpoly_zero_cs.
     intro.
     left.
     apply _cpoly_lin_ap_lin.
     auto.
    right.
    apply _cpoly_lin_ap_zero.
    auto.
   rewrite cpoly_plus_zero.
   assumption.
  intro p0; pattern p0 in |- *; apply Ccpoly_ind_cs.
   auto.
  intros.
  cut (c [#] d[+]c0 or p [#] cpoly_plus_cs q p1).
   2: apply cpoly_lin_ap_lin_.
   2: assumption.
  clear X1; intro H1.
  elim H1; intro H2.
   cut (c[+][0] [#] d[+]c0).
    intro H3.
    elim (cs_bin_op_strext _ _ _ _ _ _ H3).
     intro.
     left.
     unfold cpoly_linear_cs in |- *; simpl in |- *; auto.
    intro.
    right.
    left.
    apply ap_symmetric_unfolded.
    assumption.
   astepl c. auto.
   elim X with cpoly_zero_cs p1.
    intro.
    left.
    unfold cpoly_linear_cs in |- *; simpl in |- *; auto.
   intro.
   right.
   right; auto.
  rewrite cpoly_plus_zero.
  assumption.
 intros.
 elim X1; intro H2.
  elim (cs_bin_op_strext _ _ _ _ _ _ H2); auto.
   intro.
   left.
   left; auto.
  intro. right.
  left; auto.
 simpl in H2.
 elim (X _ _ H2).
  intro.
  left; right; auto.
 right; right; auto.
Qed.

Lemma cpoly_plus_op_wd : bin_op_wd cpoly_csetoid cpoly_plus_cs.
Proof.
 unfold bin_op_wd in |- ×.
 apply bin_fun_strext_imp_wd.
 exact cpoly_plus_op_strext.
Qed.

Definition cpoly_plus_op := Build_CSetoid_bin_op _ _ cpoly_plus_op_strext.

Lemma cpoly_plus_associative : associative cpoly_plus_op.
Proof.
 unfold associative in |- ×.
 intros p q r.
 change (cpoly_plus_cs p (cpoly_plus_cs q r) [=] cpoly_plus_cs (cpoly_plus_cs p q) r) in |- ×.
 pattern p, q, r in |- *; apply cpoly_triple_comp_ind.
   intros.
   apply eq_transitive_unfolded with (cpoly_plus_cs p1 (cpoly_plus_cs q1 r1)).
    apply eq_symmetric_unfolded.
    apply cpoly_plus_op_wd.
     assumption.
    apply cpoly_plus_op_wd.
     assumption.
    assumption.
   astepl (cpoly_plus_cs (cpoly_plus_cs p1 q1) r1).
   apply cpoly_plus_op_wd.
    apply cpoly_plus_op_wd.
     assumption.
    assumption.
   assumption.
  simpl in |- ×.
  auto.
 intros.
 repeat rewrite cpoly_lin_plus_lin.
 apply _cpoly_lin_eq_lin.
 split.
  algebra.
 assumption.
Qed.

Definition cpoly_csemi_grp := Build_CSemiGroup _ _ cpoly_plus_associative.
Canonical Structure cpoly_csemi_grp.

Lemma cpoly_cm_proof : is_CMonoid cpoly_csemi_grp cpoly_zero.
Proof.
 apply Build_is_CMonoid.
  intro; rewritecpoly_plus_zero;algebra.
 intro x.
 eapply eq_transitive_unfolded.
  apply cpoly_plus_commutative.
 rewrite cpoly_plus_zero;algebra.
Qed.

Definition cpoly_cmonoid := Build_CMonoid _ _ cpoly_cm_proof.
Canonical Structure cpoly_cmonoid.

The polynomials form a group


Fixpoint cpoly_inv (p : cpoly) : cpoly :=
  match p with
  | cpoly_zerocpoly_zero
  | cpoly_linear c p1cpoly_linear [--]c (cpoly_inv p1)
  end.

Definition cpoly_inv_cs (p : cpoly_csetoid) : cpoly_csetoid := cpoly_inv p.

Lemma cpoly_inv_zero : cpoly_inv_cs cpoly_zero_cs = cpoly_zero_cs.
Proof.
 auto.
Qed.

Lemma cpoly_inv_lin : p c,
 cpoly_inv_cs (cpoly_linear_cs c p) = cpoly_linear_cs [--]c (cpoly_inv_cs p).
Proof. simple induction p; auto. Qed.

Lemma cpoly_inv_op_strext : un_op_strext cpoly_csetoid cpoly_inv_cs.
Proof.
 unfold un_op_strext in |- ×.
 unfold fun_strext in |- ×.
 intros x y.
 pattern x, y in |- ×.
 apply Ccpoly_double_sym_ind0_cs.
   unfold Csymmetric in |- ×.
   intros.
   apply ap_symmetric_unfolded.
   apply X.
   apply ap_symmetric_unfolded.
   assumption.
  intro p; pattern p in |- *; apply Ccpoly_ind_cs.
   auto.
  intros.
  cut ( [--]c [#] [0] or cpoly_inv_cs p0 [#] cpoly_zero_cs).
   2: apply cpoly_lin_ap_zero_.
   2: auto.
  clear X0; intro H0.
  apply _cpoly_lin_ap_zero.
  auto.
  elim H0.
   left.
   astepl ( [--][--]c). algebra.
   right.
  apply X.
  assumption.
 intros.
 cut ( [--]c [#] [--]d or cpoly_inv_cs p [#] cpoly_inv_cs q).
  2: apply cpoly_lin_ap_lin_.
  2: auto.
 clear X0; intro H0.
 auto.
 elim H0; intro.
  left.
  astepl ( [--][--]c).
  astepr ( [--][--]d).
  apply inv_resp_ap.
  assumption.
 right.
 apply X.
 assumption.
Qed.

Lemma cpoly_inv_op_wd : un_op_wd cpoly_csetoid cpoly_inv_cs.
Proof.
 apply fun_strext_imp_wd. exact cpoly_inv_op_strext.
Qed.

Definition cpoly_inv_op := Build_CSetoid_un_op _ _ cpoly_inv_op_strext.

Lemma cpoly_cg_proof : is_CGroup cpoly_cmonoid cpoly_inv_op.
Proof.
 intro x.
 unfold is_inverse in |- ×.
 assert (x[+]cpoly_inv_cs x [=] [0]).
  pattern x in |- *; apply cpoly_ind_cs.
   rewrite cpoly_inv_zero.
   rewritecpoly_plus_zero.
   simpl; auto.
  intros.
  rewrite cpoly_inv_lin.
  rewritecpoly_lin_plus_lin.
  apply _cpoly_lin_eq_zero.
  split;[algebra|assumption].
 split; auto.
 eapply eq_transitive_unfolded.
  apply cpoly_plus_commutative.
 auto.
Qed.

Definition cpoly_cgroup := Build_CGroup _ _ cpoly_cg_proof.
Canonical Structure cpoly_cgroup.

Lemma cpoly_cag_proof : is_CAbGroup cpoly_cgroup.
Proof. repeat intro. apply: cpoly_plus_commutative. Qed.

Definition cpoly_cabgroup := Build_CAbGroup _ cpoly_cag_proof.
Canonical Structure cpoly_cabgroup.

The polynomials form a ring


Fixpoint cpoly_mult_cr (q : cpoly) (c : CR) {struct q} : cpoly :=
  match q with
  | cpoly_zerocpoly_zero
  | cpoly_linear d q1cpoly_linear (c[*]d) (cpoly_mult_cr q1 c)
  end.

Fixpoint cpoly_mult (p q : cpoly) {struct p} : cpoly :=
  match p with
  | cpoly_zerocpoly_zero
  | cpoly_linear c p1
      cpoly_plus (cpoly_mult_cr q c) (cpoly_linear [0] (cpoly_mult p1 q))
  end.

Definition cpoly_mult_cr_cs (p : cpoly_csetoid) c : cpoly_csetoid :=
  cpoly_mult_cr p c.

Lemma cpoly_zero_mult_cr : c,
 cpoly_mult_cr_cs cpoly_zero_cs c = cpoly_zero_cs.
Proof. auto. Qed.

Lemma cpoly_lin_mult_cr : c d q,
 cpoly_mult_cr_cs (cpoly_linear_cs d q) c =
  cpoly_linear_cs (c[*]d) (cpoly_mult_cr_cs q c).
Proof. auto. Qed.

Lemma cpoly_mult_cr_zero : p, cpoly_mult_cr_cs p [0] [=] cpoly_zero_cs.
Proof.
 intro; pattern p in |- *; apply cpoly_ind_cs.
  rewrite cpoly_zero_mult_cr.
  algebra.
 intros.
 rewrite cpoly_lin_mult_cr.
 apply _cpoly_lin_eq_zero.
 split.
  algebra.
 assumption.
Qed.

Lemma cpoly_mult_cr_strext : bin_fun_strext _ _ _ cpoly_mult_cr_cs.
Proof.
 unfold bin_fun_strext in |- ×.
 do 4 intro.
 pattern x1, x2 in |- ×.
 apply Ccpoly_double_ind0_cs.
   intro.
   rewrite cpoly_zero_mult_cr.
   intro H.
   left.
   generalize H.
   pattern p in |- ×.
   apply Ccpoly_ind_cs.
    rewrite cpoly_zero_mult_cr.
    auto.
   do 2 intro.
   rewrite cpoly_lin_mult_cr.
   intros.
   cut (y1[*]c [#] [0] or cpoly_mult_cr_cs p0 y1 [#] cpoly_zero_cs).
    2: apply cpoly_lin_ap_zero_.
    2: auto.
   clear H0; intro H1.
   cut (c [#] [0] or p0 [#] cpoly_zero_cs).
    intro; apply _cpoly_lin_ap_zero.
    auto.
   elim H1; intro H2.
    generalize (cring_mult_ap_zero_op _ _ _ H2); intro.
    auto.
   right.
   auto.
  rewrite cpoly_zero_mult_cr.
  intros.
  left.
  generalize X.
  pattern p in |- *; apply Ccpoly_ind_cs.
   rewrite cpoly_zero_mult_cr.
   auto.
  do 2 intro.
  rewrite cpoly_lin_mult_cr.
  intros.
  cut (y2[*]c [#] [0] or cpoly_zero_cs [#] cpoly_mult_cr_cs p0 y2).
   2: apply cpoly_zero_ap_lin_.
   2: auto.
  clear X1; intro H1.
  cut (c [#] [0] or cpoly_zero_cs [#] p0).
   intro.
   apply _cpoly_zero_ap_lin. auto.
   elim H1; intro H2.
   generalize (cring_mult_ap_zero_op _ _ _ H2); auto.
  right.
  auto.
 do 4 intro.
 repeat rewrite cpoly_lin_mult_cr.
 intros.
 cut (y1[*]c [#] y2[*]d or cpoly_mult_cr_cs p y1 [#] cpoly_mult_cr_cs q y2).
  2: apply cpoly_lin_ap_lin_.
  2: auto.
 clear X0; intro H0.
 cut ((c [#] d or p [#] q) or y1 [#] y2).
  intro.
  elim X0; try auto.
 elim H0; intro H1.
  generalize (cs_bin_op_strext _ _ _ _ _ _ H1); tauto.
 elim X; auto.
Qed.

Lemma cpoly_mult_cr_wd : bin_fun_wd _ _ _ cpoly_mult_cr_cs.
Proof.
 apply bin_fun_strext_imp_wd.
 exact cpoly_mult_cr_strext.
Qed.

Definition cpoly_mult_cs (p q : cpoly_csetoid) : cpoly_csetoid := cpoly_mult p q.

Lemma cpoly_zero_mult : q, cpoly_mult_cs cpoly_zero_cs q = cpoly_zero_cs.
Proof. auto. Qed.

Lemma cpoly_lin_mult : c p q,
 cpoly_mult_cs (cpoly_linear_cs c p) q =
  cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_linear_cs [0] (cpoly_mult_cs p q)).
Proof. auto. Qed.

Lemma cpoly_mult_op_strext : bin_op_strext cpoly_csetoid cpoly_mult_cs.
Proof.
 do 4 intro.
 pattern x1, x2 in |- ×.
 apply Ccpoly_double_ind0_cs.
   rewrite cpoly_zero_mult.
   intro; pattern p in |- *; apply Ccpoly_ind_cs.
    rewrite cpoly_zero_mult.
    auto.
   do 2 intro.
   rewrite cpoly_lin_mult.
   intros.
   cut ((c [#] [0] or p0 [#] cpoly_zero_cs) or y1 [#] y2).
    intro H1. elim H1. intro; left; apply _cpoly_lin_ap_zero; assumption.
    auto.
   cut (cpoly_plus_cs (cpoly_mult_cr_cs y1 c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 y1)) [#]
     cpoly_plus_cs (cpoly_mult_cr_cs y2 [0]) (cpoly_linear_cs [0] (cpoly_mult_cs cpoly_zero_cs y2))).
    intro H1.
    elim (cpoly_plus_op_strext _ _ _ _ H1); intro H2.
     elim (cpoly_mult_cr_strext _ _ _ _ H2); auto.
    elim H2; intro H3.
     elim (ap_irreflexive _ _ H3).
    rewrite cpoly_zero_mult in H3.
    elim X; auto.
   rewrite cpoly_zero_mult.
   apply ap_wdr_unfolded with cpoly_zero_cs.
    assumption.
   astepl (cpoly_plus_cs cpoly_zero_cs cpoly_zero_cs).
   apply cpoly_plus_op_wd.
    apply eq_symmetric_unfolded.
    apply cpoly_mult_cr_zero.
   apply _cpoly_zero_eq_lin.
   split; algebra.
  intro; pattern p in |- *; apply Ccpoly_ind_cs.
   auto.
  intros.
  cut ((c [#] [0] or cpoly_zero_cs [#] p0) or y1 [#] y2).
   intro.
   elim X1; try auto.
  cut (cpoly_plus_cs (cpoly_mult_cr_cs y1 [0])
    (cpoly_linear_cs [0] (cpoly_mult_cs cpoly_zero_cs y1)) [#] cpoly_plus_cs (cpoly_mult_cr_cs y2 c)
      (cpoly_linear_cs [0] (cpoly_mult_cs p0 y2))).
   intro H1.
   elim (cpoly_plus_op_strext _ _ _ _ H1); intro H2.
    elim (cpoly_mult_cr_strext _ _ _ _ H2); auto.
    intro.
    left. left.
    apply ap_symmetric_unfolded.
    assumption.
   cut (([0]:CR) [#] [0] or cpoly_mult_cs cpoly_zero_cs y1 [#] cpoly_mult_cs p0 y2).
    2: apply cpoly_lin_ap_lin_; auto.
   clear H2; intro H2.
   elim H2; intro H3.
    elim (ap_irreflexive _ _ H3).
   rewrite cpoly_zero_mult in H3.
   elim X; auto.
  rewrite cpoly_zero_mult.
  apply ap_wdl_unfolded with cpoly_zero_cs.
   assumption.
  astepl (cpoly_plus_cs cpoly_zero_cs cpoly_zero_cs).
  apply cpoly_plus_op_wd.
   apply eq_symmetric_unfolded.
   apply cpoly_mult_cr_zero.
  apply _cpoly_zero_eq_lin.
  split; algebra.
 intros.
 cut ((c [#] d or p [#] q) or y1 [#] y2).
  intro.
  auto.
 elim (cpoly_plus_op_strext _ _ _ _ X0); intro H1.
  elim (cpoly_mult_cr_strext _ _ _ _ H1); auto.
 elim H1; intro H2.
  elim (ap_irreflexive _ _ H2).
 elim X; auto.
Qed.

Lemma cpoly_mult_op_wd : bin_op_wd cpoly_csetoid cpoly_mult.
Proof.
 apply bin_fun_strext_imp_wd. exact cpoly_mult_op_strext.
Qed.

Definition cpoly_mult_op := Build_CSetoid_bin_op _ _ cpoly_mult_op_strext.

Lemma cpoly_mult_cr_dist : p q c,
 cpoly_mult_cr_cs (cpoly_plus_cs p q) c [=]
  cpoly_plus_cs (cpoly_mult_cr_cs p c) (cpoly_mult_cr_cs q c).
Proof.
 intros.
 pattern p, q in |- ×.
 apply cpoly_double_comp_ind.
   intros.
   apply eq_transitive_unfolded with (cpoly_mult_cr_cs (cpoly_plus_cs p1 q1) c).
    apply eq_symmetric_unfolded.
    apply cpoly_mult_cr_wd.
     apply cpoly_plus_op_wd.
      assumption.
     assumption.
    algebra.
   astepl (cpoly_plus_cs (cpoly_mult_cr_cs p1 c) (cpoly_mult_cr_cs q1 c)).
   apply cpoly_plus_op_wd.
    apply cpoly_mult_cr_wd; algebra.
   apply cpoly_mult_cr_wd; algebra.
  repeat rewrite cpoly_zero_plus.
  algebra.
 intros.
 repeat rewrite cpoly_lin_mult_cr.
 repeat rewrite cpoly_lin_plus_lin.
 apply: _cpoly_lin_eq_lin.
 split; algebra.
Qed.

Lemma cpoly_cr_dist : distributive cpoly_mult_op cpoly_plus_op.
Proof.
 unfold distributive in |- ×.
 intros p q r.
 change (cpoly_mult_cs p (cpoly_plus_cs q r) [=]
   cpoly_plus_cs (cpoly_mult_cs p q) (cpoly_mult_cs p r)) in |- ×.
 pattern p in |- ×. apply cpoly_ind_cs.
 repeat rewrite cpoly_zero_mult.
  rewrite cpoly_zero_plus.
  algebra.
 intros.
 repeat rewrite cpoly_lin_mult.
 apply eq_transitive_unfolded with (cpoly_plus_cs
   (cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_mult_cr_cs r c))
     (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))
       (cpoly_linear_cs [0] (cpoly_mult_cs p0 r)))).
  apply cpoly_plus_op_wd.
   apply cpoly_mult_cr_dist.
  rewrite cpoly_lin_plus_lin.
  apply _cpoly_lin_eq_lin.
  split.
   algebra.
  assumption.
 clear H.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c)
   (cpoly_plus_cs (cpoly_mult_cr_cs r c) (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))
     (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))))).
  apply eq_symmetric_unfolded.
  apply cpoly_plus_associative.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c)
   (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) (cpoly_plus_cs (cpoly_mult_cr_cs r c)
     (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))))).
  apply cpoly_plus_op_wd.
   algebra.
  apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_plus_cs (cpoly_mult_cr_cs r c)
    (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))).
   apply cpoly_plus_associative.
  apply eq_transitive_unfolded with (cpoly_plus_cs
    (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))
      (cpoly_mult_cr_cs r c)) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))).
   apply cpoly_plus_op_wd.
    apply cpoly_plus_commutative.
   algebra.
  apply eq_symmetric_unfolded.
  apply cpoly_plus_associative.
 apply cpoly_plus_associative.
Qed.

Lemma cpoly_mult_cr_assoc_mult_cr : p c d,
 cpoly_mult_cr_cs (cpoly_mult_cr_cs p c) d [=] cpoly_mult_cr_cs p (d[*]c).
Proof.
 intros.
 pattern p in |- *; apply cpoly_ind_cs.
  repeat rewrite cpoly_zero_mult_cr.
  algebra.
 intros.
 repeat rewrite cpoly_lin_mult_cr.
 apply _cpoly_lin_eq_lin.
 split.
  algebra.
 assumption.
Qed.

Lemma cpoly_mult_cr_assoc_mult : p q c,
 cpoly_mult_cr_cs (cpoly_mult_cs p q) c [=] cpoly_mult_cs (cpoly_mult_cr_cs p c) q.
Proof.
 intros.
 pattern p in |- *; apply cpoly_ind_cs.
  rewrite cpoly_zero_mult.
  rewritecpoly_zero_mult_cr; reflexivity.
 intros.
 rewrite cpoly_lin_mult.
 repeat rewrite cpoly_lin_mult_cr.
 rewrite cpoly_lin_mult.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs (cpoly_mult_cr_cs q c0) c)
   (cpoly_mult_cr_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) c)).
  apply cpoly_mult_cr_dist.
 apply cpoly_plus_op_wd.
  apply cpoly_mult_cr_assoc_mult_cr.
 rewrite cpoly_lin_mult_cr.
 apply _cpoly_lin_eq_lin.
 split;algebra.
Qed.

Lemma cpoly_mult_zero : p, cpoly_mult_cs p cpoly_zero_cs [=] cpoly_zero_cs.
Proof.
 intros.
 pattern p in |- *; apply cpoly_ind_cs.
  algebra.
 intros.
 rewrite cpoly_lin_mult.
 rewrite cpoly_zero_mult_cr.
 rewrite cpoly_zero_plus.
 apply _cpoly_lin_eq_zero.
 split;algebra.
Qed.

Lemma cpoly_mult_lin : c p q,
 cpoly_mult_cs p (cpoly_linear_cs c q) [=]
  cpoly_plus_cs (cpoly_mult_cr_cs p c) (cpoly_linear_cs [0] (cpoly_mult_cs p q)).
Proof.
 intros.
 pattern p in |- *; apply cpoly_ind_cs.
  repeat rewrite cpoly_zero_mult.
  rewrite cpoly_zero_mult_cr.
  rewrite cpoly_zero_plus.
  apply _cpoly_zero_eq_lin.
  algebra.
 intros.
 repeat rewrite cpoly_lin_mult.
 repeat rewrite cpoly_lin_mult_cr.
 repeat rewrite cpoly_lin_plus_lin.
 apply _cpoly_lin_eq_lin. split.
 algebra.
 apply eq_transitive_unfolded with (cpoly_plus_cs
   (cpoly_plus_cs (cpoly_mult_cr_cs p0 c) (cpoly_mult_cr_cs q c0))
     (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))).
  2: apply eq_symmetric_unfolded.
  2: apply cpoly_plus_associative.
 apply eq_transitive_unfolded with (cpoly_plus_cs
   (cpoly_plus_cs (cpoly_mult_cr_cs q c0) (cpoly_mult_cr_cs p0 c))
     (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))).
  2: apply cpoly_plus_op_wd.
   3: algebra.
  2: apply cpoly_plus_commutative.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c0)
   (cpoly_plus_cs (cpoly_mult_cr_cs p0 c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)))).
  2: apply cpoly_plus_associative.
 apply cpoly_plus_op_wd.
  algebra.
 assumption.
Qed.

Lemma cpoly_mult_commutative :
  p q : cpoly_csetoid, cpoly_mult_cs p q [=] cpoly_mult_cs q p.
Proof.
 intros.
 pattern p in |- ×.
 apply cpoly_ind_cs.
  rewrite cpoly_zero_mult.
  apply eq_symmetric_unfolded.
  apply cpoly_mult_zero.
 intros.
 rewrite cpoly_lin_mult.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c)
   (cpoly_linear_cs [0] (cpoly_mult_cs q p0))).
  2: apply eq_symmetric_unfolded; apply cpoly_mult_lin.
 apply cpoly_plus_op_wd.
  algebra.
 apply cpoly_linear_wd.
  algebra.
 assumption.
Qed.

Lemma cpoly_mult_dist_rht : p q r,
 cpoly_mult_cs (cpoly_plus_cs p q) r [=]
  cpoly_plus_cs (cpoly_mult_cs p r) (cpoly_mult_cs q r).
Proof.
 intros.
 apply eq_transitive_unfolded with (cpoly_mult_cs r (cpoly_plus_cs p q)).
  apply cpoly_mult_commutative.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cs r p) (cpoly_mult_cs r q)).
  generalize cpoly_cr_dist; intro.
  unfold distributive in H.
  simpl in H.
  simpl in |- ×.
  apply H.
 apply cpoly_plus_op_wd.
  apply cpoly_mult_commutative.
 apply cpoly_mult_commutative.
Qed.

Lemma cpoly_mult_assoc : associative cpoly_mult_op.
Proof.
 unfold associative in |- ×.
 intros p q r.
 change (cpoly_mult_cs p (cpoly_mult_cs q r) [=] cpoly_mult_cs (cpoly_mult_cs p q) r) in |- ×.
 pattern p in |- *; apply cpoly_ind_cs.
  repeat rewrite cpoly_zero_mult.
  algebra.
 intros.
 repeat rewrite cpoly_lin_mult.
 apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cs (cpoly_mult_cr_cs q c) r)
   (cpoly_mult_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) r)).
  apply cpoly_plus_op_wd.
   apply cpoly_mult_cr_assoc_mult.
  rewrite cpoly_lin_mult.
  apply eq_transitive_unfolded with (cpoly_plus_cs cpoly_zero_cs
    (cpoly_linear_cs [0] (cpoly_mult_cs (cpoly_mult_cs p0 q) r))).
   rewrite cpoly_zero_plus.
   apply _cpoly_lin_eq_lin.
   split.
    algebra.
   assumption.
  apply cpoly_plus_op_wd.
   apply eq_symmetric_unfolded.
   apply cpoly_mult_cr_zero.
  apply _cpoly_lin_eq_lin.
  split.
   algebra.
  algebra.
 apply eq_symmetric_unfolded.
 apply cpoly_mult_dist_rht.
Qed.

Lemma cpoly_mult_cr_one : p, cpoly_mult_cr_cs p [1] [=] p.
Proof.
 intro.
 pattern p in |- *; apply cpoly_ind_cs.
  algebra.
 intros.
 rewrite cpoly_lin_mult_cr.
 apply _cpoly_lin_eq_lin.
 algebra.
Qed.

Lemma cpoly_one_mult : p, cpoly_mult_cs cpoly_one p [=] p.
Proof.
 intro.
 unfold cpoly_one in |- ×.
 unfold cpoly_constant in |- ×.
 replace (cpoly_linear [1] cpoly_zero) with (cpoly_linear_cs [1] cpoly_zero).
  2: reflexivity.
 rewrite cpoly_lin_mult.
 rewrite cpoly_zero_mult.
 apply eq_transitive_unfolded with (cpoly_plus_cs p cpoly_zero_cs).
  apply cpoly_plus_op_wd.
   apply cpoly_mult_cr_one.
  apply _cpoly_lin_eq_zero; algebra.
 rewrite cpoly_plus_zero; algebra.
Qed.

Lemma cpoly_mult_one : p, cpoly_mult_cs p cpoly_one [=] p.
Proof.
 intro.
 apply eq_transitive_unfolded with (cpoly_mult_cs cpoly_one p).
  apply cpoly_mult_commutative.
 apply cpoly_one_mult.
Qed.

Lemma cpoly_mult_monoid :
 is_CMonoid (Build_CSemiGroup _ _ cpoly_mult_assoc) cpoly_one.
Proof.
 apply Build_is_CMonoid.
  exact cpoly_mult_one.
 exact cpoly_one_mult.
Qed.

Lemma cpoly_cr_non_triv : cpoly_ap cpoly_one cpoly_zero.
Proof.
 change (cpoly_linear_cs [1] cpoly_zero_cs [#] cpoly_zero_cs) in |- ×.
 cut (([1]:CR) [#] [0] or cpoly_zero_cs [#] cpoly_zero_cs).
  auto.
 left.
 algebra.
Qed.

cring_old uses the original definition of polynomial multiplication
cpoly_mult_fast produces smaller lengthed polynomials when multiplying by zero. For example Eval simpl in cpoly_mult_cs _ _X_ ([0]:cpoly_cring Q_as_CRing) returns cpoly_linear Q_as_CRing QZERO (cpoly_linear Q_as_CRing QZERO (cpoly_zero Q_as_CRing)) while Eval simpl in cpoly_mult_fast_cs _ _X_ ([0]:cpoly_cring Q_as_CRing) returns cpoly_zero Q_as_CRing.
Smaller lengthed polynomials means faster operations, and better estimates of the degree of a polynomial.

Definition cpoly_mult_fast (p q : cpoly) : cpoly :=
  match q with
  | cpoly_zerocpoly_zero
  | _cpoly_mult p q
  end.

Definition cpoly_mult_fast_cs (p q : cpoly_csetoid) : cpoly_csetoid := cpoly_mult_fast p q.

cpoly_mult_fast is proven correct with respect the the original multiplication in cpoly_cring_old

Lemma cpoly_mult_fast_ap_equiv : p1 p2 q1 q2,
(cpoly_mult_fast_cs p1 q1)[#](cpoly_mult_cs p2 q2)p1[#]p2 or q1[#]q2.
 destruct q1 as [|c q1]; destruct q2 as [|c0 q2]; intros X; simpl in X.
Proof.
    rewrite cpoly_ap_p_zero in X.
    elim (ap_irreflexive cpoly_csetoid cpoly_zero).
    stepl (cpoly_mult_cs p2 cpoly_zero).
     assumption.
    apply cpoly_mult_zero.
   rewrite cpoly_ap_p_zero in X.
   right.
   apply ap_symmetric.
   eapply cring_mult_ap_zero_op with (R:=cpoly_cring_old).
   apply X.
  right.
  eapply cring_mult_ap_zero_op with (R:=cpoly_cring_old).
  change (cpoly_mult p1 (cpoly_linear c q1)) with (cpoly_mult_cs p1 (cpoly_linear c q1)) in X.
  stepr (cpoly_mult_cs p2 cpoly_zero).
   apply X.
  apply cpoly_mult_zero.
 apply cpoly_mult_op_strext.
 apply X.
Qed.

Lemma cpoly_mult_fast_equiv : p q,
(cpoly_mult_fast_cs p q)[=](cpoly_mult_cs p q).
Proof.
 intros p q.
 apply not_ap_imp_eq.
 intro H.
 assert (p[#]p or q[#]q).
  apply cpoly_mult_fast_ap_equiv.
  assumption.
 destruct X as [X|X]; apply (ap_irreflexive _ _ X).
Qed.

Lemma cpoly_mult_fast_op_strext : bin_op_strext cpoly_csetoid cpoly_mult_fast_cs.
Proof.
 intros x1 x2 y1 y2 H.
 apply cpoly_mult_op_strext.
 stepl (cpoly_mult_fast_cs x1 y1).
  stepr (cpoly_mult_fast_cs x2 y2).
   assumption.
  apply cpoly_mult_fast_equiv.
 apply cpoly_mult_fast_equiv.
Qed.

Definition cpoly_mult_fast_op := Build_CSetoid_bin_op _ _ cpoly_mult_fast_op_strext.

Lemma cpoly_is_CRing : is_CRing cpoly_cabgroup cpoly_one cpoly_mult_fast_op.
Proof.
 assert (mult_assoc:(associative cpoly_mult_fast_op)).
  intros p q r.
  stepl (cpoly_mult_op p (cpoly_mult_op q r)).
   stepr (cpoly_mult_op (cpoly_mult_op p q) r).
    apply cpoly_mult_assoc.
   stepl (cpoly_mult_op (cpoly_mult_fast_op p q) r).
    apply eq_symmetric; apply cpoly_mult_fast_equiv.
   apply bin_op_wd_unfolded.
    apply cpoly_mult_fast_equiv.
   apply eq_reflexive.
  stepl (cpoly_mult_op p (cpoly_mult_fast_op q r)).
   apply eq_symmetric; apply cpoly_mult_fast_equiv.
  apply bin_op_wd_unfolded.
   apply eq_reflexive.
  apply cpoly_mult_fast_equiv.
 eapply Build_is_CRing with mult_assoc.
    split.
     intro p.
     stepl (cpoly_mult_op p cpoly_one).
      apply cpoly_mult_one.
     apply eq_symmetric; apply cpoly_mult_fast_equiv.
    intro p.
    stepl (cpoly_mult_op cpoly_one p).
     apply cpoly_one_mult.
    apply eq_symmetric; apply cpoly_mult_fast_equiv.
   intros p q.
   stepl (cpoly_mult_op p q).
    stepr (cpoly_mult_op q p).
     apply cpoly_mult_commutative.
    apply eq_symmetric; apply cpoly_mult_fast_equiv.
   apply eq_symmetric; apply cpoly_mult_fast_equiv.
  intros p q r.
  stepl (cpoly_mult_op p (q[+]r)).
   stepr (cpoly_plus_op (cpoly_mult_op p q) (cpoly_mult_op p r)).
    apply cpoly_cr_dist.
   apply bin_op_wd_unfolded; apply eq_symmetric; apply cpoly_mult_fast_equiv.
  apply eq_symmetric; apply cpoly_mult_fast_equiv.
 exact cpoly_cr_non_triv.
Qed.

Definition cpoly_cring : CRing := Build_CRing _ _ _ cpoly_is_CRing.
Canonical Structure cpoly_cring.

Lemma cpoly_constant_strext :
 fun_strext (S1:=CR) (S2:=cpoly_cring) cpoly_constant.
Proof.
 unfold fun_strext in |- ×.
 unfold cpoly_constant in |- ×.
 simpl in |- ×.
 intros x y H.
 elim H.
  auto.
 intro.
 elim b.
Qed.

Lemma cpoly_constant_wd : fun_wd (S1:=CR) (S2:=cpoly_cring) cpoly_constant.
Proof.
 apply fun_strext_imp_wd.
 exact cpoly_constant_strext.
Qed.

Definition cpoly_constant_fun := Build_CSetoid_fun _ _ _ cpoly_constant_strext.

Definition cpoly_var : cpoly_cring := cpoly_linear_cs [0] ([1]:cpoly_cring).
Notation "'_X_'" := cpoly_var.

Definition cpoly_x_minus_c c : cpoly_cring :=
 cpoly_linear_cs [--]c ([1]:cpoly_cring).

Lemma cpoly_x_minus_c_strext :
 fun_strext (S1:=CR) (S2:=cpoly_cring) cpoly_x_minus_c.
Proof.
 unfold fun_strext in |- ×.
 unfold cpoly_x_minus_c in |- ×.
 simpl in |- ×.
 intros x y H.
 elim H; intro H0.
  apply (cs_un_op_strext _ _ _ _ H0).
 elim H0; intro H1.
  elim (ap_irreflexive_unfolded _ _ H1).
 elim H1.
Qed.

Lemma cpoly_x_minus_c_wd : fun_wd (S1:=CR) (S2:=cpoly_cring) cpoly_x_minus_c.
Proof.
 apply fun_strext_imp_wd.
 exact cpoly_x_minus_c_strext.
Qed.

Definition cpoly_ring_th:= (CRing_Ring cpoly_cring).
End CPoly_CRing.

Canonical Structure cpoly_cring.
Notation "'_X_'" := (@cpoly_var _).

Definition cpoly_linear_fun' (CR : CRing) :
 CSetoid_bin_fun CR (cpoly_cring CR) (cpoly_cring CR) := cpoly_linear_fun CR.

Implicit Arguments cpoly_linear_fun' [CR].
Infix "+x×" := cpoly_linear_fun' (at level 50, left associativity).

Apartness, equality, and induction


Section CPoly_CRing_ctd.

Let CR be a ring, p and q polynomials over that ring, and c and d elements of the ring.
Variable CR : CRing.
Add Ring cpolycring_th : (CRing_Ring (cpoly_cring CR)).

Notation R[x] := (cpoly_cring CR).

Section helpful_section.

Variables p q : R[x].
Variables c d : CR.
It should be possible to merge most of this section using the new apply
Lemma linear_eq_zero_ : c[+X*]p [=] [0]c [=] [0] p [=] [0].
Proof cpoly_lin_eq_zero_ CR p c.

Lemma _linear_eq_zero : c [=] [0] p [=] [0]c[+X*]p [=] [0].
Proof _cpoly_lin_eq_zero CR p c.

Lemma zero_eq_linear_ : [0] [=] c[+X*]pc [=] [0] [0] [=] p.
Proof cpoly_zero_eq_lin_ CR p c.

Lemma _zero_eq_linear : c [=] [0] [0] [=] p[0] [=] c[+X*]p.
Proof _cpoly_zero_eq_lin CR p c.

Lemma linear_eq_linear_ : c[+X*]p [=] d[+X*]qc [=] d p [=] q.
Proof cpoly_lin_eq_lin_ CR p q c d.

Lemma _linear_eq_linear : c [=] d p [=] qc[+X*]p [=] d[+X*]q.
Proof _cpoly_lin_eq_lin CR p q c d.

Lemma linear_ap_zero_ : c[+X*]p [#] [0]c [#] [0] or p [#] [0].
Proof cpoly_lin_ap_zero_ CR p c.

Lemma _linear_ap_zero : c [#] [0] or p [#] [0]c[+X*]p [#] [0].
Proof _cpoly_lin_ap_zero CR p c.

Lemma linear_ap_zero : (c[+X*]p [#] [0]) = (c [#] [0] or p [#] [0]).
Proof cpoly_lin_ap_zero CR p c.

Lemma zero_ap_linear_ : [0] [#] c[+X*]pc [#] [0] or [0] [#] p.
Proof cpoly_zero_ap_lin_ CR p c.

Lemma _zero_ap_linear : c [#] [0] or [0] [#] p[0] [#] c[+X*]p.
Proof _cpoly_zero_ap_lin CR p c.

Lemma zero_ap_linear : ([0] [#] c[+X*]p) = (c [#] [0] or [0] [#] p).
Proof cpoly_zero_ap_lin CR p c.

Lemma linear_ap_linear_ : c[+X*]p [#] d[+X*]qc [#] d or p [#] q.
Proof cpoly_lin_ap_lin_ CR p q c d.

Lemma _linear_ap_linear : c [#] d or p [#] qc[+X*]p [#] d[+X*]q.
Proof _cpoly_lin_ap_lin CR p q c d.

Lemma linear_ap_linear : (c[+X*]p [#] d[+X*]q) = (c [#] d or p [#] q).
Proof cpoly_lin_ap_lin CR p q c d.

End helpful_section.

Lemma Ccpoly_induc : P : R[x]CProp, P [0]
 ( p c, P pP (c[+X*]p)) → p, P p.
Proof (Ccpoly_ind_cs CR).

Lemma Ccpoly_double_sym_ind : P : R[x]R[x]CProp,
 Csymmetric P → ( p, P p [0]) →
 ( p q c d, P p qP (c[+X*]p) (d[+X*]q)) → p q, P p q.
Proof (Ccpoly_double_sym_ind0_cs CR).

Lemma Cpoly_double_comp_ind : P : R[x]R[x]CProp,
 ( p1 p2 q1 q2, p1 [=] p2q1 [=] q2P p1 q1P p2 q2) → P [0] [0]
 ( p q c d, P p qP (c[+X*]p) (d[+X*]q)) → p q, P p q.
Proof (Ccpoly_double_comp_ind CR).

Lemma Cpoly_triple_comp_ind : P : R[x]R[x]R[x]CProp,
 ( p1 p2 q1 q2 r1 r2,
  p1 [=] p2q1 [=] q2r1 [=] r2P p1 q1 r1P p2 q2 r2) →
 P [0] [0] [0] → ( p q r c d e, P p q rP (c[+X*]p) (d[+X*]q) (e[+X*]r)) →
  p q r, P p q r.
Proof (Ccpoly_triple_comp_ind CR).

Lemma cpoly_induc : P : R[x]Prop,
 P [0] → ( p c, P pP (c[+X*]p)) → p, P p.
Proof (cpoly_ind_cs CR).

Lemma cpoly_double_sym_ind : P : R[x]R[x]Prop,
 Tsymmetric P → ( p, P p [0]) →
 ( p q c d, P p qP (c[+X*]p) (d[+X*]q)) → p q, P p q.
Proof (cpoly_double_sym_ind0_cs CR).

Lemma poly_double_comp_ind : P : R[x]R[x]Prop,
 ( p1 p2 q1 q2, p1 [=] p2q1 [=] q2P p1 q1P p2 q2) → P [0] [0]
 ( p q c d, P p qP (c[+X*]p) (d[+X*]q)) → p q, P p q.
Proof (cpoly_double_comp_ind CR).

Lemma poly_triple_comp_ind : P : R[x]R[x]R[x]Prop,
 ( p1 p2 q1 q2 r1 r2,
  p1 [=] p2q1 [=] q2r1 [=] r2P p1 q1 r1P p2 q2 r2) →
 P [0] [0] [0]
 ( p q r c d e, P p q rP (c[+X*]p) (d[+X*]q) (e[+X*]r)) → p q r, P p q r.
Proof (cpoly_triple_comp_ind CR).

Transparent cpoly_cring.
Transparent cpoly_cgroup.
Transparent cpoly_csetoid.

Fixpoint cpoly_apply (p : R[x]) (x : CR) {struct p} : CR :=
  match p with
  | cpoly_zero[0]
  | cpoly_linear c p1c[+]x[*]cpoly_apply p1 x
  end.

Lemma cpoly_apply_strext : bin_fun_strext _ _ _ cpoly_apply.
Proof.
 unfold bin_fun_strext in |- ×.
 do 2 intro.
 pattern x1, x2 in |- ×.
 apply Ccpoly_double_sym_ind.
   unfold Csymmetric in |- ×.
   intros.
   generalize (ap_symmetric _ _ _ X0); intro.
   elim (X _ _ X1); intro.
    left.
    apply ap_symmetric_unfolded.
    assumption.
   right.
   apply ap_symmetric_unfolded.
   assumption.
  do 3 intro.
  pattern p in |- ×.
  apply Ccpoly_induc.
   simpl in |- ×.
   intro H.
   elim (ap_irreflexive _ _ H).
  intros.
  simpl in X0.
  simpl in X.
  cut (c[+]y1[*]cpoly_apply p0 y1 [#] [0][+]y1[*][0]).
   intro.
   elim (cs_bin_op_strext _ _ _ _ _ _ X1); intro H2.
    left.
    cut (c [#] [0] or p0 [#] [0]).
     intro.
     apply _linear_ap_zero.
     auto.
    left.
    assumption.
   elim (cs_bin_op_strext _ _ _ _ _ _ H2); intro H3.
    elim (ap_irreflexive _ _ H3).
   elim (X H3); intro H4.
    left.
    cut (c [#] [0] or p0 [#] [0]).
     intro; apply _linear_ap_zero.
     auto.
    right.
    exact H4.
   auto.
  astepr ([0][+]([0]:CR)).
  astepr ([0]:CR). auto.
  simpl in |- ×.
 intros.
 elim (cs_bin_op_strext _ _ _ _ _ _ X0); intro H1.
  auto.
 elim (cs_bin_op_strext _ _ _ _ _ _ H1); intro H2.
  auto.
 elim (X _ _ H2); auto.
Qed.

Lemma cpoly_apply_wd : bin_fun_wd _ _ _ cpoly_apply.
Proof.
 apply bin_fun_strext_imp_wd.
 exact cpoly_apply_strext.
Qed.

Definition cpoly_apply_fun := Build_CSetoid_bin_fun _ _ _ _ cpoly_apply_strext.

End CPoly_CRing_ctd.

cpoly_apply_fun is denoted infix by ! The first argument is left implicit, so the application of polynomial f (seen as a function) to argument x can be written as f!x. In the names of lemmas, we write apply.

Implicit Arguments cpoly_apply_fun [CR].
Infix "!" := cpoly_apply_fun (at level 1, no associativity).

Basic properties of polynomials

Let R be a ring and write R[x] for the ring of polynomials over R.

Section Poly_properties.
Variable R : CRing.
Add Ring cpolycring_thR : (cpoly_ring_th R).
Notation R[x] := (cpoly_cring R).

Lemma cpoly_const_one : [1] [=] cpoly_constant_fun _ ([1]:R).
Proof.
 simpl in |- *; split; algebra.
Qed.

Lemma cpoly_const_plus : a b : R, cpoly_constant_fun _ (a[+]b) [=] cpoly_constant_fun _ a[+]cpoly_constant_fun _ b.
Proof.
 simpl in |- *; split; algebra.
Qed.

Lemma cpoly_const_mult : a b : R, cpoly_constant_fun _ (a[*]b) [=] cpoly_constant_fun _ a[*] cpoly_constant_fun _ b.
Proof.
 simpl in |- *; split; algebra.
Qed.

Definition polyconst : RingHom R R[x] := Build_RingHom _ _ _ cpoly_const_plus cpoly_const_mult cpoly_const_one.
Notation "'_C_'" := polyconst.

Lemma c_one : [1] [=] _C_ ([1]:R).
Proof.
 simpl in |- *; split; algebra.
Qed.

Lemma c_plus : a b : R, _C_ (a[+]b) [=] _C_ a[+] _C_ b.
Proof.
 simpl in |- *; split; algebra.
Qed.

Lemma c_mult : a b : R, _C_ (a[*]b) [=] _C_ a[*] _C_ b.
Proof.
 simpl in |- *; split; algebra.
Qed.

Lemma c_zero : [0] [=] _C_ ([0]:R).
Proof.
 simpl in |- *; split; algebra.
Qed.

Constant and identity


Lemma cpoly_X_ : _X_ [=] ([0]:R[x]) [+X*][1].
Proof.
 algebra.
Qed.

Lemma cpoly_C_ : c : R, _C_ c [=] c[+X*][0].
Proof.
 algebra.
Qed.

Hint Resolve cpoly_X_ cpoly_C_: algebra.

Lemma cpoly_const_eq : c d : R, c [=] d_C_ c [=] _C_ d.
Proof.
 algebra.
Qed.

Lemma cpoly_lin : (p : R[x]) (c : R), c[+X*]p [=] _C_ c[+]_X_[*]p.
Proof.
 intros.
 astepr (c[+X*][0][+] ((cpoly_mult_cr_cs _ p [0]:R[x]) [+] (cpoly_linear _ ([0]:R)
   (cpoly_mult_cs _ (cpoly_one R) (p:cpoly_csetoid R)) :cpoly_csetoid R))).
  cut (cpoly_mult_cr_cs R p [0] [=] ([0]:R[x])).
   intro.
   astepr (c[+X*][0][+] (([0]:R[x]) [+] (cpoly_linear _ ([0]:R)
     (cpoly_mult_cs _ (cpoly_one R) (p:cpoly_csetoid R)) :cpoly_csetoid R))).
   2: apply (cpoly_mult_cr_zero R p).
  cut ((cpoly_mult_cs _ (cpoly_one R) (p:cpoly_csetoid R):cpoly_csetoid R) [=] p).
   intro.
   apply eq_transitive_unfolded with
     (c[+X*][0][+](([0]:R[x]) [+]cpoly_linear _ ([0]:R) (p:cpoly_csetoid R))).
    2: apply bin_op_wd_unfolded.
     2: algebra.
    2: apply bin_op_wd_unfolded.
     2: algebra.
    2: apply (cpoly_linear_wd R).
     2: algebra.
    2: apply eq_symmetric_unfolded.
    2: apply cpoly_one_mult.
   astepr (c[+X*][0][+]cpoly_linear _ ([0]:R) (p:cpoly_csetoid R)).
   astepr (c[+][0][+X*]([0][+]p)).
   astepr (c[+X*]p).
   algebra.
  apply cpoly_one_mult.
 destruct p.
  simpl.
  algebra.
 simpl.
 split.
  auto with ×.
 apply eq_reflexive with (S:=cpoly_cring R).
Qed.

Hint Resolve cpoly_lin: algebra.

Lemma poly_linear : c f, (cpoly_linear _ c f:R[x]) [=] _X_[*]f[+]_C_ c.
Proof.
 intros.
 astepr (_C_ c[+]_X_[*]f).
 exact (cpoly_lin f c).
Qed.

Lemma poly_c_apzero : a : R, _C_ a [#] [0]a [#] [0].
Proof.
 intros.
 cut (_C_ a [#] _C_ [0]).
  intro H0.
  generalize (csf_strext _ _ _ _ _ H0); auto.
 Hint Resolve c_zero: algebra.
 astepr ([0]:R[x]). auto.
Qed.

Lemma c_mult_lin : (p : R[x]) c d, _C_ c[*] (d[+X*]p) [=] c[*]d[+X*]_C_ c[*]p.
Proof.
 intros.
 pattern p in |- ×.
 apply cpoly_induc.
  simpl in |- ×.
  repeat split; algebra.
 intros. simpl in |- ×.
 repeat split; algebra.
 change ((cpoly_mult_cr R p0 c:R[x]) [=] (cpoly_mult_cr R p0 c:R[x])[+][0]) in |- ×.
 algebra.
Qed.

Lemma lin_mult : (p q : R[x]) c, (c[+X*]p) [*]q [=] _C_ c[*]q[+]_X_[*] (p[*]q).
Proof.
 intros.
 astepl ((_C_ c[+]_X_[*]p)[*]q).
 astepl (_C_ c[*]q[+]_X_[*]p[*]q).
 algebra.
Qed.

Hint Resolve lin_mult: algebra.

Application of polynomials


Lemma poly_eq_zero : p : R[x], p [=] cpoly_zero R x, p ! x [=] [0].
Proof.
 intros.
 astepl (cpoly_zero R) ! x.
 change ([0] ! x [=] [0]) in |- ×.
 algebra.
Qed.

Lemma apply_wd : (p p' : R[x]) x x', p [=] p'x [=] x'p ! x [=] p' ! x'.
Proof.
 algebra.
Qed.

Lemma cpolyap_pres_eq : (f : R[x]) x y, x [=] yf ! x [=] f ! y.
Proof.
 algebra.
Qed.

Lemma cpolyap_strext : (f : R[x]) x y, f ! x [#] f ! yx [#] y.
Proof.
 intros f x y H.
 elim (csbf_strext _ _ _ _ _ _ _ _ H); intro H0.
  elim (ap_irreflexive_unfolded _ _ H0).
 assumption.
Qed.

Definition cpoly_csetoid_op (f : R[x]) : CSetoid_un_op R :=
 Build_CSetoid_fun _ _ (fun xf ! x) (cpolyap_strext f).

Definition FPoly p := total_eq_part _ (cpoly_csetoid_op p).

Lemma c_apply : c x : R, (_C_ c) ! x [=] c.
Proof.
 intros.
 simpl in |- ×.
 astepl (c[+][0]).
 algebra.
Qed.

Lemma x_apply : x : R, _X_ ! x [=] x.
Proof.
 intros.
 simpl in |- ×.
 astepl (x[*]([1][+]x[*][0])).
 astepl (x[*]([1][+][0])).
 astepl (x[*][1]).
 algebra.
Qed.

Lemma plus_apply : (p q : R[x]) x, (p[+]q) ! x [=] p ! x[+]q ! x.
Proof.
 intros.
 pattern p, q in |- *; apply poly_double_comp_ind.
   intros.
   astepl (p1[+]q1) ! x.
   astepr (p1 ! x[+]q1 ! x).
   algebra.
  simpl in |- ×.
  algebra.
 intros.
 astepl (c[+]d[+]x[*](p0[+]q0) ! x).
 astepr (c[+]x[*]p0 ! x[+](d[+]x[*]q0 ! x)).
 astepl (c[+]d[+]x[*](p0 ! x[+]q0 ! x)).
 astepl (c[+]d[+](x[*]p0 ! x[+]x[*]q0 ! x)).
 astepl (c[+](d[+](x[*]p0 ! x[+]x[*]q0 ! x))).
 astepr (c[+](x[*]p0 ! x[+](d[+]x[*]q0 ! x))).
 astepl (c[+](d[+]x[*]p0 ! x[+]x[*]q0 ! x)).
 astepr (c[+](x[*]p0 ! x[+]d[+]x[*]q0 ! x)).
 algebra.
Qed.

Lemma inv_apply : (p : R[x]) x, ( [--]p) ! x [=] [--]p ! x.
Proof.
 intros.
 pattern p in |- ×.
 apply cpoly_induc.
  simpl in |- ×.
  algebra.
 intros.
 astepl ( [--]c[+]x[*]( [--]p0) ! x).
 astepr ( [--](c[+]x[*]p0 ! x)).
 astepr ( [--]c[+][--](x[*]p0 ! x)).
 astepr ( [--]c[+]x[*][--]p0 ! x).
 algebra.
Qed.

Hint Resolve plus_apply inv_apply: algebra.

Lemma minus_apply : (p q : R[x]) x, (p[-]q) ! x [=] p ! x[-]q ! x.
Proof.
 intros.
 astepl (p[+][--]q) ! x.
 astepr (p ! x[+][--]q ! x).
 astepl (p ! x[+]( [--]q) ! x).
 algebra.
Qed.

Lemma c_mult_apply : (q : R[x]) c x, (_C_ c[*]q) ! x [=] c[*]q ! x.
Proof.
 intros.
 astepl ((cpoly_mult_cr R q c:R[x])[+]([0][+X*][0])) ! x.
  astepl ((cpoly_mult_cr R q c) ! x[+]([0][+X*][0]) ! x).
  astepl ((cpoly_mult_cr R q c) ! x[+]([0][+]x[*][0])).
  astepl ((cpoly_mult_cr R q c) ! x[+]([0][+][0])).
  astepl ((cpoly_mult_cr R q c) ! x[+][0]).
  astepl (cpoly_mult_cr R q c) ! x.
  pattern q in |- ×.
  apply cpoly_induc.
   simpl in |- ×.
   algebra.
  intros.
  astepl (c[*]c0[+X*]cpoly_mult_cr R p c) ! x.
  astepl (c[*]c0[+]x[*](cpoly_mult_cr R p c) ! x).
  astepl (c[*]c0[+]x[*](c[*]p ! x)).
  astepr (c[*](c0[+]x[*]p ! x)).
  astepr (c[*]c0[+]c[*](x[*]p ! x)).
  apply bin_op_wd_unfolded.
   algebra.
  astepl (x[*]c[*]p ! x).
  astepr (c[*]x[*]p ! x).
  algebra.
 stepr ((cpoly_mult _ (_C_ c) q)!x).
  apply eq_reflexive.
 apply apply_wd.
  apply eq_symmetric.
  apply (cpoly_mult_fast_equiv _ (_C_ c) q).
 apply eq_reflexive.
Qed.

Hint Resolve c_mult_apply: algebra.

Lemma mult_apply : (p q : R[x]) x, (p[*]q) ! x [=] p ! x[*]q ! x.
Proof.
 intros.
 pattern p in |- ×.
 apply cpoly_induc.
  astepl ([0] ! x).
  simpl in |- ×.
  algebra.
 intros.
 astepl (_C_ c[*]q[+]_X_[*](p0[*]q)) ! x.
 astepl ((_C_ c[*]q) ! x[+](_X_[*](p0[*]q)) ! x).
 astepl ((_C_ c[*]q) ! x[+]([0][+]_X_[*](p0[*]q)) ! x).
 astepl ((_C_ c[*]q) ! x[+](_C_ [0][+]_X_[*](p0[*]q)) ! x).
 astepl ((_C_ c[*]q) ! x[+]([0][+X*]p0[*]q) ! x).
 astepl ((_C_ c[*]q) ! x[+]([0][+]x[*](p0[*]q) ! x)).
 astepl (c[*]q ! x[+]x[*](p0[*]q) ! x).
 astepl (c[*]q ! x[+]x[*](p0 ! x[*]q ! x)).
 astepr ((c[+]x[*]p0 ! x)[*]q ! x).
 astepr (c[*]q ! x[+]x[*]p0 ! x[*]q ! x).
 algebra.
Qed.

Hint Resolve mult_apply: algebra.

Lemma one_apply : x : R, [1] ! x [=] [1].
Proof.
 intro.
 astepl (_C_ [1]) ! x.
 apply c_apply.
Qed.

Hint Resolve one_apply: algebra.

Lemma nexp_apply : (p : R[x]) n x, (p[^]n) ! x [=] p ! x[^]n.
Proof.
 intros.
 induction n as [| n Hrecn].
  astepl ([1]:R[x]) ! x.
  astepl ([1]:R).
  algebra.
 astepl (p[*]p[^]n) ! x.
 astepl (p ! x[*](p[^]n) ! x).
 astepl (p ! x[*]p ! x[^]n).
 algebra.
Qed.

Lemma poly_inv_apply : (p : R[x]) x, (cpoly_inv _ p) ! x [=] [--]p ! x.
Proof inv_apply.

Lemma Sum0_cpoly_ap : (f : natR[x]) a k, (Sum0 k f) ! a [=] Sum0 k (fun i(f i) ! a).
Proof.
 intros.
 induction k as [| k Hreck].
  simpl in |- ×.
  algebra.
 astepl (Sum0 k f[+]f k) ! a.
 astepl ((Sum0 k f) ! a[+](f k) ! a).
 astepl (Sum0 k (fun i : nat(f i) ! a)[+](f k) ! a).
 simpl in |- ×.
 algebra.
Qed.

Lemma Sum_cpoly_ap : (f : natR[x]) a k l,
 (Sum k l f) ! a [=] Sum k l (fun i(f i) ! a).
Proof.
 unfold Sum in |- ×.
 unfold Sum1 in |- ×.
 intros.
 unfold cg_minus in |- ×.
 astepl ((Sum0 (S l) f) ! a[+]( [--](Sum0 k f)) ! a).
 astepl ((Sum0 (S l) f) ! a[+][--](Sum0 k f) ! a).
 apply bin_op_wd_unfolded.
  apply Sum0_cpoly_ap.
 apply un_op_wd_unfolded.
 apply Sum0_cpoly_ap.
Qed.

Lemma cm_Sum_apply (l: list (cpoly_cring R)) (x: R):
 (cm_Sum l) ! x [=] cm_Sum (map (fun ee ! x) l).
Proof.
 induction l.
  reflexivity.
 change ((a [+] cm_Sum l) ! x[=]cm_Sum (map (fun e : cpoly_cring Re ! x) (a :: l))).
 rewrite plus_apply, IHl.
 reflexivity.
Qed.

Hint Rewrite cm_Sum_apply: apply.

Lemma cr_Product_apply (l: list (cpoly_cring R)) (x: R):
 (cr_Product l) ! x [=] cr_Product (map (fun ee ! x) l).
Proof.
 induction l.
  simpl.
  rewrite cring_mult_zero.
  apply cm_rht_unit_unfolded.
 change ((a [*] cr_Product l) ! x[=]cr_Product (map (fun e : cpoly_cring Re ! x) (a :: l))).
 rewrite mult_apply, IHl.
 reflexivity.
Qed.

Hint Rewrite cr_Product_apply: apply.

End Poly_properties.

Notation "'_C_'" := (@polyconst _).

Induction properties of polynomials for Prop

Section Poly_Prop_Induction.

Variable CR : CRing.
Add Ring cpolycring_thCR : (cpoly_ring_th CR).
Notation Cpoly := (cpoly CR).

Notation Cpoly_zero := (cpoly_zero CR).

Notation Cpoly_linear := (cpoly_linear CR).

Notation Cpoly_cring := (cpoly_cring CR).

Lemma cpoly_double_ind : P : Cpoly_cringCpoly_cringProp,
 ( p, P p [0]) → ( p, P [0] p) →
 ( p q c d, P p qP (c[+X*]p) (d[+X*]q)) → p q, P p q.
Proof (cpoly_double_ind0_cs CR).

End Poly_Prop_Induction.

Hint Resolve poly_linear cpoly_lin: algebra.
Hint Resolve apply_wd cpoly_const_eq: algebra_c.
Hint Resolve c_apply x_apply inv_apply plus_apply minus_apply mult_apply
  nexp_apply: algebra.
Hint Resolve one_apply c_zero c_one c_mult: algebra.
Hint Resolve poly_inv_apply: algebra.
Hint Resolve c_mult_lin: algebra.

Hint Rewrite one_apply c_apply x_apply mult_apply plus_apply minus_apply : apply.
Hint Rewrite inv_apply nexp_apply c_mult_apply poly_inv_apply : apply.
Ltac poly_apply:= autorewrite with apply; simpl.
The tactic poly_apply applies polynomials to arguments

Section Derivative.

Variable R:CRing.
Add Ring cpolycring_thR1 : (cpoly_ring_th R).
Notation R[x]:= (cpoly_cring R).

Fixpoint cpoly_diff (p : R[x]) : R[x] :=
match p with
| cpoly_zero[0]
| cpoly_linear c p1p1[+]([0][+X*](cpoly_diff p1))
end.

Lemma cpoly_diff_strext : un_op_strext _ cpoly_diff.
Proof.
 intros x.
 induction x.
  induction y.
   auto with ×.
  intros Hxy.
  right.
  abstract ( destruct (cpoly_ap_zero_plus _ _ _ (ap_symmetric _ _ _ Hxy)) as [c|[c|c]];
    [apply (ap_symmetric _ _ _ c) |elim (ap_irreflexive _ _ c) |apply IHy;apply c]).
 intros [|a y] Hxy.
  simpl in Hxy.
  right.
  abstract ( destruct (cpoly_ap_zero_plus _ _ _ Hxy) as [c|[c|c]]; [apply (ap_symmetric _ _ _ c)
    |elim (ap_irreflexive _ _ c)
      |change ([0][#]x); apply ap_symmetric; apply IHx; apply ap_symmetric; apply c]).
 right.
 destruct (cpoly_plus_op_strext _ _ _ _ _ Hxy) as [c|[c|c]].
   assumption.
  elim (ap_irreflexive _ _ c).
 apply IHx; apply c.
Defined.

Lemma cpoly_diff_wd : un_op_wd _ cpoly_diff.
Proof.
 apply fun_strext_imp_wd.
 apply cpoly_diff_strext.
Qed.

Definition cpolyder := Build_CSetoid_un_op _ _ cpoly_diff_strext.
Notation "'_D_'" := cpolyder.

Lemma diff_zero : _D_ [0][=][0].
Proof.
 reflexivity.
Qed.

Lemma diff_one : _D_ [1][=][0].
Proof.
 simpl; split; auto with *; reflexivity.
Qed.

Lemma diff_const : c, _D_ (_C_ c)[=][0].
Proof.
 simpl; split; auto with ×.
Qed.

Lemma diff_x : _D_ _X_[=][1].
Proof.
 simpl; split; auto with ×.
Qed.

Lemma diff_linear : a (p:R[x]), _D_ (a[+X*]p)[=]p[+]_X_[*]_D_ p.
Proof.
 intros a p.
 change (p[+]([0][+X*]_D_ p)[=]p[+]_X_[*]_D_ p).
 rewritecpoly_lin.
 rewrite <- c_zero.
 ring.
Qed.

Lemma diff_plus : (p q:R[x]), _D_ (p[+]q)[=]_D_ p[+]_D_ q.
Proof.
 induction p.
  reflexivity.
 intros [|a q].
  rewritecm_rht_unit_unfolded.
  change (cpoly_zero R) with ([0]:cpoly_cring R).
  rewritediff_zero; algebra.
 change ((p[+]q)[+]cpoly_linear _ [0] (_D_ (p[+]q))[=]
   (p[+]cpoly_linear _ [0] (_D_ p))[+](q[+]cpoly_linear _ [0] (_D_ q))).
 do 3 rewritepoly_linear.
 change (st_car R[x]) in p, q.
 change (p[+]q[+](_X_[*]_D_ (p[+]q)[+]_C_ [0])[=]
   p[+](_X_[*]_D_ p[+]_C_ [0])[+](q[+](_X_[*]_D_ q[+]_C_ [0]))).
 rewrite → (IHp q).
 rewrite <- c_zero.
 ring.
Qed.

Lemma diff_c_mult : c (p:R[x]), _D_ (_C_ c[*]p)[=]_C_ c[*]_D_ p.
Proof.
 intros c p.
 induction p.
  auto with ×.
 change (_D_ (cpoly_linear R s p)) with (p[+]([0][+X*](_D_ p))).
 change (cpoly_linear R s p) with (s[+X*]p).
 rewritec_mult_lin.
 change (_D_ (c[*]s[+X*]_C_ c[*]p)) with (_C_ c[*]p [+] ([0][+X*](_D_ (_C_ c[*]p)))).
 rewriteIHp.
 do 2 rewritecpoly_lin.
 rewrite <- c_zero.

 change
 (@st_eq R[x]
  (@csg_op R[x] (@cr_mult R[x] (polyconst R c) p)
     (@csg_op R[x] (cm_unit R[x])
        (@cr_mult R[x] (cpoly_var R) (@cr_mult R[x] (polyconst R c) (cpolyder p)))))
  (@cr_mult R[x] (polyconst R c)
     (@csg_op R[x] p
        (@csg_op R[x] (cm_unit R[x]) (@cr_mult R[x] (cpoly_var R) (cpolyder p)))))).
 ring.
Qed.

Lemma diff_mult : (p q:R[x]), _D_ (p[*]q)[=]_D_ p[*]q [+] p[*]_D_ q.
Proof.
 induction p.
  intros q.
  change (_D_([0][*]q)[=][0][*]q[+][0][*]_D_ q).
  stepl (_D_([0]:R[x])). 2: now destruct q.
  rewritediff_zero.
  ring.
 intros q.
 change (st_car R[x]) in p.
 change (_D_((s[+X*]p)[*]q)[=]_D_(s[+X*]p)[*]q[+](s[+X*]p)[*]_D_ q).
 do 2 rewritelin_mult.
 rewritediff_linear.
 rewritediff_plus.
 setoid_replace (_D_ ((_C_ s:R[x])[*]q)) with (_C_ s[*]_D_ q) by apply diff_c_mult.
 setoid_replace (((_X_:R[x])[*](p[*]q)):R[x])
   with ((((_X_:R[x])[*](p[*]q)))[+][0]) by (symmetry;apply cm_rht_unit_unfolded).
 setoid_replace ([0]:R[x]) with (_C_ [0]:R[x]) by apply c_zero.
 rewrite <- poly_linear.
 change (_D_ (cpoly_linear R [0] (p[*]q))) with (p[*]q [+] ([0][+X*]_D_ (p[*]q))).
 rewritecpoly_lin.
 rewrite <- c_zero.
 rewriteIHp.
 ring.
Qed.

End Derivative.
Notation "'_D_'" := (@cpolyder _).

Hint Rewrite diff_zero diff_one diff_const diff_x diff_plus diff_c_mult diff_mult diff_linear : poly_diff.
Section Map.

Variable R S : CRing.
Add Ring cpolycring_thRR : (cpoly_ring_th R).
Add Ring cpolycring_thSS : (cpoly_ring_th S).
Variable f : RingHom R S.
Notation R[x] := (cpoly_cring R).
Notation SX := (cpoly_cring S).

Fixpoint cpoly_map_fun (p:R[x]) : SX :=
match p with
| cpoly_zerocpoly_zero _
| cpoly_linear c p1cpoly_linear _ (f c) (cpoly_map_fun p1)
end.

Lemma cpoly_map_strext : fun_strext cpoly_map_fun.
Proof.
 intros x.
 induction x; intros y H.
  induction y.
   elim H.
  destruct H as [H|H].
   left.
   eapply rh_apzero; apply H.
  right.
  apply IHy.
  apply H.
 destruct y as [|c y].
  destruct H as [H|H].
   left.
   eapply rh_apzero; apply H.
  right.
  change ([0][#]x).
  apply ap_symmetric.
  apply IHx.
  apply ap_symmetric.
  apply H.
 destruct H as [H|H].
  left.
  eapply rh_strext; apply H.
 right.
 apply IHx.
 apply H.
Defined.

Definition cpoly_map_csf : CSetoid_fun R[x] SX := Build_CSetoid_fun _ _ _ cpoly_map_strext.

Lemma cpoly_map_pres_plus : fun_pres_plus _ _ cpoly_map_csf.
Proof.
 unfold fun_pres_plus.
 apply (cpoly_double_ind0 R).
   intros p.
   change (cpoly_map_csf(p[+][0])[=]cpoly_map_csf p[+][0]).
   stepr (cpoly_map_csf p). 2: ring.
   apply csf_wd.
   cut ( p: cpoly_cring R, csg_op p [0] [=] p). easy.
   intros. ring.
  reflexivity.
 intros p q c d H.
 split.
  apply rh_pres_plus.
 apply H.
Qed.

Lemma cpoly_map_pres_mult : fun_pres_mult _ _ cpoly_map_csf.
Proof.
 unfold fun_pres_mult.
 assert (X: x y, cpoly_map_csf (cpoly_mult_cr _ x y)[=]cpoly_mult_cr _ (cpoly_map_csf x) (f y)).
  induction x; intros y.
   apply eq_reflexive.
  split.
   apply rh_pres_mult.
  apply IHx.
 apply (cpoly_double_ind0 R).
   intros p.
   apply eq_reflexive.
  intros p.
  change (st_car R[x]) in p.
  change (cpoly_zero R) with ([0]:R[x]).
  stepl (cpoly_map_csf ([0]:R[x])).
   change (cpoly_map_csf [0]) with ([0]:SX).
   ring.
  apply csf_wd; ring.
 intros p q c d H.
 split.
  autorewrite with ringHomPush.
  reflexivity.
 change (st_car R[x]) in p,q.
 change (cpoly_map_csf ((cpoly_mult_cr _ q c)[+](p[*](cpoly_linear _ d q)))
   [=](cpoly_mult_cr _ (cpoly_map_csf q) (f c))[+](cpoly_map_csf p)[*](cpoly_map_csf (cpoly_linear _ d q))).
 stepl ((cpoly_map_csf (cpoly_mult_cr R q c))[+](cpoly_map_csf (p[*]cpoly_linear R d q)));
  [| apply eq_symmetric; apply cpoly_map_pres_plus].
 apply csbf_wd.
  apply X.
 stepl (cpoly_map_csf ((cpoly_linear R d q:R[x])[*]p)); [| apply csf_wd;ring].
 stepr (cpoly_map_csf (cpoly_linear R d q)[*]cpoly_map_csf p).
  2:apply (mult_commut_unfolded SX).
 change ((cpoly_linear R d q:R[x])[*]p) with (cpoly_mult_fast_cs _ (cpoly_linear R d q) p).
 rewritecpoly_mult_fast_equiv.
 rewrite cpoly_lin_mult.
 change (cpoly_map_csf (cpoly_linear R d q:R[x])[*]cpoly_map_csf p)
   with (cpoly_mult_fast_cs _ (cpoly_linear S (f d) (cpoly_map_csf q)) (cpoly_map_csf p)).
 rewritecpoly_mult_fast_equiv.
 rewrite cpoly_lin_mult.
 stepl (cpoly_map_csf (cpoly_mult_cr_cs R p d)[+]cpoly_map_csf (cpoly_linear R [0] (cpoly_mult_cs R q p)));
  [| apply eq_symmetric; apply cpoly_map_pres_plus].
 change (cpoly_map_fun (cpoly_mult_cr_cs R p d)[+] cpoly_map_fun ([0][+X*] (cpoly_mult_cs R q p))[=]
   (cpoly_mult_cr_cs S (cpoly_map_fun p) (f d))[+]
     ([0][+X*](cpoly_mult_cs S (cpoly_map_fun q) (cpoly_map_fun p)))).
 apply csbf_wd.
  apply X.
 split.
  auto with ×.
 change ((cpoly_map_csf (cpoly_mult_cs R q p))[=](cpoly_mult_cs S (cpoly_map_csf q) (cpoly_map_csf p))).
 repeat setoid_rewrite <- cpoly_mult_fast_equiv.
 change (cpoly_map_csf (q[*]p)[=]cpoly_map_csf q[*]cpoly_map_csf p).
 stepr (cpoly_map_csf p[*]cpoly_map_csf q). 2: ring.
 rewrite <- H.
 apply csf_wd;ring.
Qed.

Lemma cpoly_map_pres_unit : fun_pres_unit _ _ cpoly_map_csf.
Proof.
 split.
  apply rh_pres_unit.
 constructor.
Qed.

Definition cpoly_map := Build_RingHom _ _ _ cpoly_map_pres_plus cpoly_map_pres_mult cpoly_map_pres_unit.

Lemma cpoly_map_X : cpoly_map _X_[=]_X_.
Proof.
 repeat split.
  apply rh_pres_zero.
 apply rh_pres_unit.
Qed.

Lemma cpoly_map_C : c, cpoly_map (_C_ c)[=]_C_ (f c).
Proof. reflexivity. Qed.

Lemma cpoly_map_diff : p, cpoly_map (_D_ p) [=] _D_ (cpoly_map p).
Proof.
 induction p.
  reflexivity.
 change (cpoly_map (_D_ (s[+X*]p))[=]_D_ (f s[+X*](cpoly_map p))).
 do 2 rewritediff_linear.
 autorewrite with ringHomPush.
 rewriteIHp.
 rewritecpoly_map_X.
 reflexivity.
Qed.

Lemma cpoly_map_apply : p x, f (p ! x)[=] (cpoly_map p) ! (f x).
Proof.
 induction p.
  intros x.
  apply rh_pres_zero.
 intros x.
 simpl in ×.
 rewriterh_pres_plus.
 rewriterh_pres_mult.
 rewriteIHp.
 reflexivity.
Qed.

End Map.
Implicit Arguments cpoly_map [R S].

Lemma cpoly_map_compose : R S T (g:RingHom S T) (f:RingHom R S) p,
 (cpoly_map (RHcompose _ _ _ g f) p)[=]cpoly_map g (cpoly_map f p).
Proof.
 induction p.
  constructor.
 split.
  reflexivity.
 apply IHp.
Qed.