Polynomials
The first section only proves the polynomials form a ring, and nothing more interesting. Section gives some basic properties of equality and induction of polynomials.Definition of polynomials; they form a ring
Let CR be a ring.
The intuition behind the type cpoly is the following
- (cpoly CR) is CR[X];
- cpoly_zero is the `empty' polynomial with no coefficients;
- (cpoly_linear c p) is c+X×p
Inductive cpoly : Type :=
| cpoly_zero : cpoly
| cpoly_linear : CR -> cpoly -> cpoly.
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 : forall P : cpoly -> cpoly -> CProp,
(forall p, P p cpoly_zero) -> (forall p, P cpoly_zero p) ->
(forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
Lemma Ccpoly_double_sym_ind0 : forall P : cpoly -> cpoly -> CProp,
Csymmetric P -> (forall p, P p cpoly_zero) ->
(forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
Lemma Ccpoly_double_ind0' : forall P : cpoly -> cpoly -> CProp,
(forall p, P cpoly_zero p) -> (forall p c, P (cpoly_linear c p) cpoly_zero) ->
(forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
Lemma cpoly_double_ind0 : forall P : cpoly -> cpoly -> Prop,
(forall p, P p cpoly_zero) -> (forall p, P cpoly_zero p) ->
(forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
Lemma cpoly_double_sym_ind0 : forall P : cpoly -> cpoly -> Prop,
Tsymmetric P -> (forall p, P p cpoly_zero) ->
(forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
Lemma cpoly_double_ind0' : forall P : cpoly -> cpoly -> Prop,
(forall p, P cpoly_zero p) -> (forall p c, P (cpoly_linear c p) cpoly_zero) ->
(forall p q c d, P p q -> P (cpoly_linear c p) (cpoly_linear d q)) -> forall p q, P p q.
Fixpoint cpoly_eq_zero (p : cpoly) : Prop :=
match p with
| cpoly_zero => True
| cpoly_linear c p1 => c [=] 0 /\ cpoly_eq_zero p1
end.
Fixpoint cpoly_eq (p q : cpoly) {struct p} : Prop :=
match p with
| cpoly_zero => cpoly_eq_zero q
| cpoly_linear c p1 =>
match q with
| cpoly_zero => cpoly_eq_zero p
| cpoly_linear d q1 => c [=] d /\ cpoly_eq p1 q1
end
end.
Lemma cpoly_eq_p_zero : forall p, cpoly_eq p cpoly_zero = cpoly_eq_zero p.
Fixpoint cpoly_ap_zero (p : cpoly) : CProp :=
match p with
| cpoly_zero => ⊥
| cpoly_linear c p1 => c [#] 0 or cpoly_ap_zero p1
end.
Fixpoint cpoly_ap (p q : cpoly) {struct p} : CProp :=
match p with
| cpoly_zero => cpoly_ap_zero q
| cpoly_linear c p1 =>
match q with
| cpoly_zero => cpoly_ap_zero p
| cpoly_linear d q1 => c [#] d or cpoly_ap p1 q1
end
end.
Lemma cpoly_ap_p_zero : forall p, cpoly_ap_zero p = cpoly_ap p cpoly_zero.
Lemma irreflexive_cpoly_ap : irreflexive cpoly_ap.
Lemma symmetric_cpoly_ap : Csymmetric cpoly_ap.
Lemma cotransitive_cpoly_ap : cotransitive cpoly_ap.
Lemma tight_apart_cpoly_ap : tight_apart cpoly_eq cpoly_ap.
Lemma cpoly_is_CSetoid : is_CSetoid _ cpoly_eq cpoly_ap.
Definition cpoly_csetoid := Build_CSetoid _ _ _ cpoly_is_CSetoid.
Canonical Structure cpoly_csetoid.
Canonical Structure cpoly_setoid := cs_crr cpoly_csetoid.
match p with
| cpoly_zero => True
| cpoly_linear c p1 => c [=] 0 /\ cpoly_eq_zero p1
end.
Fixpoint cpoly_eq (p q : cpoly) {struct p} : Prop :=
match p with
| cpoly_zero => cpoly_eq_zero q
| cpoly_linear c p1 =>
match q with
| cpoly_zero => cpoly_eq_zero p
| cpoly_linear d q1 => c [=] d /\ cpoly_eq p1 q1
end
end.
Lemma cpoly_eq_p_zero : forall p, cpoly_eq p cpoly_zero = cpoly_eq_zero p.
Fixpoint cpoly_ap_zero (p : cpoly) : CProp :=
match p with
| cpoly_zero => ⊥
| cpoly_linear c p1 => c [#] 0 or cpoly_ap_zero p1
end.
Fixpoint cpoly_ap (p q : cpoly) {struct p} : CProp :=
match p with
| cpoly_zero => cpoly_ap_zero q
| cpoly_linear c p1 =>
match q with
| cpoly_zero => cpoly_ap_zero p
| cpoly_linear d q1 => c [#] d or cpoly_ap p1 q1
end
end.
Lemma cpoly_ap_p_zero : forall p, cpoly_ap_zero p = cpoly_ap p cpoly_zero.
Lemma irreflexive_cpoly_ap : irreflexive cpoly_ap.
Lemma symmetric_cpoly_ap : Csymmetric cpoly_ap.
Lemma cotransitive_cpoly_ap : cotransitive cpoly_ap.
Lemma tight_apart_cpoly_ap : tight_apart cpoly_eq cpoly_ap.
Lemma cpoly_is_CSetoid : is_CSetoid _ cpoly_eq cpoly_ap.
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 : forall P : cpoly_csetoid -> CProp,
P cpoly_zero_cs -> (forall p c, P p -> P (cpoly_linear_cs c p)) -> forall p, P p.
Lemma Ccpoly_double_ind0_cs : forall P : cpoly_csetoid -> cpoly_csetoid -> CProp,
(forall p, P p cpoly_zero_cs) -> (forall p, P cpoly_zero_cs p) ->
(forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
Lemma Ccpoly_double_sym_ind0_cs : forall P : cpoly_csetoid -> cpoly_csetoid -> CProp,
Csymmetric P -> (forall p, P p cpoly_zero_cs) ->
(forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
Lemma cpoly_ind_cs : forall P : cpoly_csetoid -> Prop,
P cpoly_zero_cs -> (forall p c, P p -> P (cpoly_linear_cs c p)) -> forall p, P p.
Lemma cpoly_double_ind0_cs : forall P : cpoly_csetoid -> cpoly_csetoid -> Prop,
(forall p, P p cpoly_zero_cs) -> (forall p, P cpoly_zero_cs p) ->
(forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
Lemma cpoly_double_sym_ind0_cs : forall P : cpoly_csetoid -> cpoly_csetoid -> Prop,
Tsymmetric P -> (forall p, P p cpoly_zero_cs) ->
(forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
Lemma cpoly_lin_eq_zero_ : forall p c,
cpoly_linear_cs c p [=] cpoly_zero_cs -> c [=] 0 /\ p [=] cpoly_zero_cs.
Lemma _cpoly_lin_eq_zero : forall p c,
c [=] 0 /\ p [=] cpoly_zero_cs -> cpoly_linear_cs c p [=] cpoly_zero_cs.
Lemma cpoly_zero_eq_lin_ : forall p c,
cpoly_zero_cs [=] cpoly_linear_cs c p -> c [=] 0 /\ cpoly_zero_cs [=] p.
Lemma _cpoly_zero_eq_lin : forall p c,
c [=] 0 /\ cpoly_zero_cs [=] p -> cpoly_zero_cs [=] cpoly_linear_cs c p.
Lemma cpoly_lin_eq_lin_ : forall p q c d,
cpoly_linear_cs c p [=] cpoly_linear_cs d q -> c [=] d /\ p [=] q.
Lemma _cpoly_lin_eq_lin : forall p q c d,
c [=] d /\ p [=] q -> cpoly_linear_cs c p [=] cpoly_linear_cs d q.
Lemma cpoly_lin_ap_zero_ : forall p c,
cpoly_linear_cs c p [#] cpoly_zero_cs -> c [#] 0 or p [#] cpoly_zero_cs.
Lemma _cpoly_lin_ap_zero : forall p c,
c [#] 0 or p [#] cpoly_zero_cs -> cpoly_linear_cs c p [#] cpoly_zero_cs.
Lemma cpoly_lin_ap_zero : forall p c,
(cpoly_linear_cs c p [#] cpoly_zero_cs) = (c [#] 0 or p [#] cpoly_zero_cs).
Lemma cpoly_zero_ap_lin_ : forall p c,
cpoly_zero_cs [#] cpoly_linear_cs c p -> c [#] 0 or cpoly_zero_cs [#] p.
Lemma _cpoly_zero_ap_lin : forall p c,
c [#] 0 or cpoly_zero_cs [#] p -> cpoly_zero_cs [#] cpoly_linear_cs c p.
Lemma cpoly_zero_ap_lin : forall p c,
(cpoly_zero_cs [#] cpoly_linear_cs c p) = (c [#] 0 or cpoly_zero_cs [#] p).
Lemma cpoly_lin_ap_lin_ : forall p q c d,
cpoly_linear_cs c p [#] cpoly_linear_cs d q -> c [#] d or p [#] q.
Lemma _cpoly_lin_ap_lin : forall p q c d,
c [#] d or p [#] q -> cpoly_linear_cs c p [#] cpoly_linear_cs d q.
Lemma cpoly_lin_ap_lin : forall p q c d,
(cpoly_linear_cs c p [#] cpoly_linear_cs d q) = (c [#] d or p [#] q).
Lemma cpoly_linear_strext : bin_fun_strext _ _ _ cpoly_linear_cs.
Lemma cpoly_linear_wd : bin_fun_wd _ _ _ cpoly_linear_cs.
Definition cpoly_linear_fun := Build_CSetoid_bin_fun _ _ _ _ cpoly_linear_strext.
Lemma Ccpoly_double_comp_ind : forall P : cpoly_csetoid -> cpoly_csetoid -> CProp,
(forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) ->
P cpoly_zero_cs cpoly_zero_cs ->
(forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
Lemma Ccpoly_triple_comp_ind :
forall P : cpoly_csetoid -> cpoly_csetoid -> cpoly_csetoid -> CProp,
(forall p1 p2 q1 q2 r1 r2,
p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) ->
P cpoly_zero_cs cpoly_zero_cs cpoly_zero_cs ->
(forall p q r c d e,
P p q r -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q) (cpoly_linear_cs e r)) ->
forall p q r, P p q r.
Lemma cpoly_double_comp_ind : forall P : cpoly_csetoid -> cpoly_csetoid -> Prop,
(forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) ->
P cpoly_zero_cs cpoly_zero_cs ->
(forall p q c d, P p q -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q)) -> forall p q, P p q.
Lemma cpoly_triple_comp_ind :
forall P : cpoly_csetoid -> cpoly_csetoid -> cpoly_csetoid -> Prop,
(forall p1 p2 q1 q2 r1 r2,
p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) ->
P cpoly_zero_cs cpoly_zero_cs cpoly_zero_cs ->
(forall p q r c d e,
P p q r -> P (cpoly_linear_cs c p) (cpoly_linear_cs d q) (cpoly_linear_cs e r)) ->
forall p q r, P p q r.
Fixpoint cpoly_plus (p q : cpoly) {struct p} : cpoly :=
match p with
| cpoly_zero => q
| cpoly_linear c p1 =>
match q with
| cpoly_zero => p
| cpoly_linear d q1 => cpoly_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 : forall p, cpoly_plus_cs cpoly_zero_cs p = p.
Lemma cpoly_plus_zero : forall p, cpoly_plus_cs p cpoly_zero_cs = p.
Lemma cpoly_lin_plus_lin : forall 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).
Lemma cpoly_plus_commutative : forall p q, cpoly_plus_cs p q [=] cpoly_plus_cs q p.
Lemma cpoly_plus_q_ap_q : forall p q, cpoly_plus_cs p q [#] q -> p [#] cpoly_zero_cs.
Lemma cpoly_p_plus_ap_p : forall p q, cpoly_plus_cs p q [#] p -> q [#] cpoly_zero.
Lemma cpoly_ap_zero_plus : forall p q,
cpoly_plus_cs p q [#] cpoly_zero_cs -> p [#] cpoly_zero_cs or q [#] cpoly_zero_cs.
Lemma cpoly_plus_op_strext : bin_op_strext cpoly_csetoid cpoly_plus_cs.
Lemma cpoly_plus_op_wd : bin_op_wd cpoly_csetoid cpoly_plus_cs.
Definition cpoly_plus_op := Build_CSetoid_bin_op _ _ cpoly_plus_op_strext.
Lemma cpoly_plus_associative : associative cpoly_plus_op.
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.
Definition cpoly_cmonoid := Build_CMonoid _ _ cpoly_cm_proof.
Canonical Structure cpoly_cmonoid.
Fixpoint cpoly_inv (p : cpoly) : cpoly :=
match p with
| cpoly_zero => cpoly_zero
| cpoly_linear c p1 => cpoly_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.
Lemma cpoly_inv_lin : forall p c,
cpoly_inv_cs (cpoly_linear_cs c p) = cpoly_linear_cs [--]c (cpoly_inv_cs p).
Lemma cpoly_inv_op_strext : un_op_strext cpoly_csetoid cpoly_inv_cs.
Lemma cpoly_inv_op_wd : un_op_wd cpoly_csetoid cpoly_inv_cs.
Definition cpoly_inv_op := Build_CSetoid_un_op _ _ cpoly_inv_op_strext.
Lemma cpoly_cg_proof : is_CGroup cpoly_cmonoid cpoly_inv_op.
Definition cpoly_cgroup := Build_CGroup _ _ cpoly_cg_proof.
Canonical Structure cpoly_cgroup.
Lemma cpoly_cag_proof : is_CAbGroup cpoly_cgroup.
Definition cpoly_cabgroup := Build_CAbGroup _ cpoly_cag_proof.
Canonical Structure cpoly_cgroup.
Fixpoint cpoly_mult_cr (q : cpoly) (c : CR) {struct q} : cpoly :=
match q with
| cpoly_zero => cpoly_zero
| cpoly_linear d q1 => cpoly_linear (c[*]d) (cpoly_mult_cr q1 c)
end.
Fixpoint cpoly_mult (p q : cpoly) {struct p} : cpoly :=
match p with
| cpoly_zero => cpoly_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 : forall c,
cpoly_mult_cr_cs cpoly_zero_cs c = cpoly_zero_cs.
Lemma cpoly_lin_mult_cr : forall c d q,
cpoly_mult_cr_cs (cpoly_linear_cs d q) c =
cpoly_linear_cs (c[*]d) (cpoly_mult_cr_cs q c).
Lemma cpoly_mult_cr_zero : forall p, cpoly_mult_cr_cs p 0 [=] cpoly_zero_cs.
Lemma cpoly_mult_cr_strext : bin_fun_strext _ _ _ cpoly_mult_cr_cs.
Lemma cpoly_mult_cr_wd : bin_fun_wd _ _ _ cpoly_mult_cr_cs.
Definition cpoly_mult_cs (p q : cpoly_csetoid) : cpoly_csetoid := cpoly_mult p q.
Lemma cpoly_zero_mult : forall q, cpoly_mult_cs cpoly_zero_cs q = cpoly_zero_cs.
Lemma cpoly_lin_mult : forall 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)).
Lemma cpoly_mult_op_strext : bin_op_strext cpoly_csetoid cpoly_mult_cs.
Lemma cpoly_mult_op_wd : bin_op_wd cpoly_csetoid cpoly_mult.
Definition cpoly_mult_op := Build_CSetoid_bin_op _ _ cpoly_mult_op_strext.
Lemma cpoly_mult_cr_dist : forall 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).
Lemma cpoly_cr_dist : distributive cpoly_mult_op cpoly_plus_op.
Lemma cpoly_mult_cr_assoc_mult_cr : forall p c d,
cpoly_mult_cr_cs (cpoly_mult_cr_cs p c) d [=] cpoly_mult_cr_cs p (d[*]c).
Lemma cpoly_mult_cr_assoc_mult : forall p q c,
cpoly_mult_cr_cs (cpoly_mult_cs p q) c [=] cpoly_mult_cs (cpoly_mult_cr_cs p c) q.
Lemma cpoly_mult_zero : forall p, cpoly_mult_cs p cpoly_zero_cs [=] cpoly_zero_cs.
Lemma cpoly_mult_lin : forall 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)).
Lemma cpoly_mult_commutative :
forall p q : cpoly_csetoid, cpoly_mult_cs p q [=] cpoly_mult_cs q p.
Lemma cpoly_mult_dist_rht : forall 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).
Lemma cpoly_mult_assoc : associative cpoly_mult_op.
Lemma cpoly_mult_cr_one : forall p, cpoly_mult_cr_cs p 1 [=] p.
Lemma cpoly_one_mult : forall p, cpoly_mult_cs cpoly_one p [=] p.
Lemma cpoly_mult_one : forall p, cpoly_mult_cs p cpoly_one [=] p.
Lemma cpoly_mult_monoid :
is_CMonoid (Build_CSemiGroup _ _ cpoly_mult_assoc) cpoly_one.
Lemma cpoly_cr_non_triv : cpoly_ap cpoly_one cpoly_zero.
cring_old uses the original definition of polynomial multiplication
Lemma cpoly_is_CRing_old : is_CRing cpoly_cabgroup cpoly_one cpoly_mult_op.
Definition cpoly_cring_old : CRing := Build_CRing _ _ _ cpoly_is_CRing_old.
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 0Q (cpoly_linear Q_as_CRing 0Q (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.
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_zero => cpoly_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 : forall p1 p2 q1 q2,
(cpoly_mult_fast_cs p1 q1)[#](cpoly_mult_cs p2 q2) -> p1[#]p2 or q1[#]q2.
Lemma cpoly_mult_fast_equiv : forall p q,
(cpoly_mult_fast_cs p q)[=](cpoly_mult_cs p q).
Lemma cpoly_mult_fast_op_strext : bin_op_strext cpoly_csetoid cpoly_mult_fast_cs.
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.
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.
Lemma cpoly_constant_wd : fun_wd (S1:=CR) (S2:=cpoly_cring) cpoly_constant.
Definition cpoly_constant_fun := Build_CSetoid_fun _ _ _ cpoly_constant_strext.
Definition _X_ : cpoly_cring := cpoly_linear_cs 0 (1:cpoly_cring).
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.
Lemma cpoly_x_minus_c_wd : fun_wd (S1:=CR) (S2:=cpoly_cring) cpoly_x_minus_c.
End CPoly_CRing.
Definition cpoly_linear_fun' (CR : CRing) :
CSetoid_bin_fun CR (cpoly_cring CR) (cpoly_cring CR) := cpoly_linear_fun CR.
Infix "+x×" := cpoly_linear_fun' (at level 50, left associativity).
Let CR be a ring, p and q polynomials over that ring, and c and d
elements of the ring.
Variable CR : CRing.
Notation R[x] := (cpoly_cring CR).
Section helpful_section.
Variables p q : R[x].
Variables c d : CR.
Lemma linear_eq_zero_ : c[+X*]p [=] 0 -> c [=] 0 /\ p [=] 0.
Lemma _linear_eq_zero : c [=] 0 /\ p [=] 0 -> c[+X*]p [=] 0.
Lemma zero_eq_linear_ : 0 [=] c[+X*]p -> c [=] 0 /\ 0 [=] p.
Lemma _zero_eq_linear : c [=] 0 /\ 0 [=] p -> 0 [=] c[+X*]p.
Lemma linear_eq_linear_ : c[+X*]p [=] d[+X*]q -> c [=] d /\ p [=] q.
Lemma _linear_eq_linear : c [=] d /\ p [=] q -> c[+X*]p [=] d[+X*]q.
Lemma linear_ap_zero_ : c[+X*]p [#] 0 -> c [#] 0 or p [#] 0.
Lemma _linear_ap_zero : c [#] 0 or p [#] 0 -> c[+X*]p [#] 0.
Lemma linear_ap_zero : (c[+X*]p [#] 0) = (c [#] 0 or p [#] 0).
Lemma zero_ap_linear_ : 0 [#] c[+X*]p -> c [#] 0 or 0 [#] p.
Lemma _zero_ap_linear : c [#] 0 or 0 [#] p -> 0 [#] c[+X*]p.
Lemma zero_ap_linear : (0 [#] c[+X*]p) = (c [#] 0 or 0 [#] p).
Lemma linear_ap_linear_ : c[+X*]p [#] d[+X*]q -> c [#] d or p [#] q.
Lemma _linear_ap_linear : c [#] d or p [#] q -> c[+X*]p [#] d[+X*]q.
Lemma linear_ap_linear : (c[+X*]p [#] d[+X*]q) = (c [#] d or p [#] q).
End helpful_section.
Lemma Ccpoly_induc : forall P : R[x] -> CProp, P 0 ->
(forall p c, P p -> P (c[+X*]p)) -> forall p, P p.
Lemma Ccpoly_double_sym_ind : forall P : R[x] -> R[x] -> CProp,
Csymmetric P -> (forall p, P p 0) ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma Cpoly_double_comp_ind : forall P : R[x] -> R[x] -> CProp,
(forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P 0 0 ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma Cpoly_triple_comp_ind : forall P : R[x] -> R[x] -> R[x] -> CProp,
(forall p1 p2 q1 q2 r1 r2,
p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) ->
P 0 0 0 -> (forall p q r c d e, P p q r -> P (c[+X*]p) (d[+X*]q) (e[+X*]r)) ->
forall p q r, P p q r.
Lemma cpoly_induc : forall P : R[x] -> Prop,
P 0 -> (forall p c, P p -> P (c[+X*]p)) -> forall p, P p.
Lemma cpoly_double_sym_ind : forall P : R[x] -> R[x] -> Prop,
Tsymmetric P -> (forall p, P p 0) ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma poly_double_comp_ind : forall P : R[x] -> R[x] -> Prop,
(forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P 0 0 ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma poly_triple_comp_ind : forall P : R[x] -> R[x] -> R[x] -> Prop,
(forall p1 p2 q1 q2 r1 r2,
p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) ->
P 0 0 0 ->
(forall p q r c d e, P p q r -> P (c[+X*]p) (d[+X*]q) (e[+X*]r)) -> forall p q r, P p q r.
Fixpoint cpoly_apply (p : R[x]) (x : CR) {struct p} : CR :=
match p with
| cpoly_zero => 0
| cpoly_linear c p1 => c[+]x[*]cpoly_apply p1 x
end.
Lemma cpoly_apply_strext : bin_fun_strext _ _ _ cpoly_apply.
Lemma cpoly_apply_wd : bin_fun_wd _ _ _ cpoly_apply.
Definition cpoly_apply_fun := Build_CSetoid_bin_fun _ _ _ _ cpoly_apply_strext.
End CPoly_CRing_ctd.
Notation R[x] := (cpoly_cring CR).
Section helpful_section.
Variables p q : R[x].
Variables c d : CR.
Lemma linear_eq_zero_ : c[+X*]p [=] 0 -> c [=] 0 /\ p [=] 0.
Lemma _linear_eq_zero : c [=] 0 /\ p [=] 0 -> c[+X*]p [=] 0.
Lemma zero_eq_linear_ : 0 [=] c[+X*]p -> c [=] 0 /\ 0 [=] p.
Lemma _zero_eq_linear : c [=] 0 /\ 0 [=] p -> 0 [=] c[+X*]p.
Lemma linear_eq_linear_ : c[+X*]p [=] d[+X*]q -> c [=] d /\ p [=] q.
Lemma _linear_eq_linear : c [=] d /\ p [=] q -> c[+X*]p [=] d[+X*]q.
Lemma linear_ap_zero_ : c[+X*]p [#] 0 -> c [#] 0 or p [#] 0.
Lemma _linear_ap_zero : c [#] 0 or p [#] 0 -> c[+X*]p [#] 0.
Lemma linear_ap_zero : (c[+X*]p [#] 0) = (c [#] 0 or p [#] 0).
Lemma zero_ap_linear_ : 0 [#] c[+X*]p -> c [#] 0 or 0 [#] p.
Lemma _zero_ap_linear : c [#] 0 or 0 [#] p -> 0 [#] c[+X*]p.
Lemma zero_ap_linear : (0 [#] c[+X*]p) = (c [#] 0 or 0 [#] p).
Lemma linear_ap_linear_ : c[+X*]p [#] d[+X*]q -> c [#] d or p [#] q.
Lemma _linear_ap_linear : c [#] d or p [#] q -> c[+X*]p [#] d[+X*]q.
Lemma linear_ap_linear : (c[+X*]p [#] d[+X*]q) = (c [#] d or p [#] q).
End helpful_section.
Lemma Ccpoly_induc : forall P : R[x] -> CProp, P 0 ->
(forall p c, P p -> P (c[+X*]p)) -> forall p, P p.
Lemma Ccpoly_double_sym_ind : forall P : R[x] -> R[x] -> CProp,
Csymmetric P -> (forall p, P p 0) ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma Cpoly_double_comp_ind : forall P : R[x] -> R[x] -> CProp,
(forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P 0 0 ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma Cpoly_triple_comp_ind : forall P : R[x] -> R[x] -> R[x] -> CProp,
(forall p1 p2 q1 q2 r1 r2,
p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) ->
P 0 0 0 -> (forall p q r c d e, P p q r -> P (c[+X*]p) (d[+X*]q) (e[+X*]r)) ->
forall p q r, P p q r.
Lemma cpoly_induc : forall P : R[x] -> Prop,
P 0 -> (forall p c, P p -> P (c[+X*]p)) -> forall p, P p.
Lemma cpoly_double_sym_ind : forall P : R[x] -> R[x] -> Prop,
Tsymmetric P -> (forall p, P p 0) ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma poly_double_comp_ind : forall P : R[x] -> R[x] -> Prop,
(forall p1 p2 q1 q2, p1 [=] p2 -> q1 [=] q2 -> P p1 q1 -> P p2 q2) -> P 0 0 ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
Lemma poly_triple_comp_ind : forall P : R[x] -> R[x] -> R[x] -> Prop,
(forall p1 p2 q1 q2 r1 r2,
p1 [=] p2 -> q1 [=] q2 -> r1 [=] r2 -> P p1 q1 r1 -> P p2 q2 r2) ->
P 0 0 0 ->
(forall p q r c d e, P p q r -> P (c[+X*]p) (d[+X*]q) (e[+X*]r)) -> forall p q r, P p q r.
Fixpoint cpoly_apply (p : R[x]) (x : CR) {struct p} : CR :=
match p with
| cpoly_zero => 0
| cpoly_linear c p1 => c[+]x[*]cpoly_apply p1 x
end.
Lemma cpoly_apply_strext : bin_fun_strext _ _ _ cpoly_apply.
Lemma cpoly_apply_wd : bin_fun_wd _ _ _ cpoly_apply.
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.
Section Poly_properties.
Variable R : CRing.
Notation R[x] := (cpoly_cring R).
Lemma cpoly_const_one : 1 [=] cpoly_constant_fun _ (1:R).
Lemma cpoly_const_plus : forall a b : R, cpoly_constant_fun _ (a[+]b) [=] cpoly_constant_fun _ a[+]cpoly_constant_fun _ b.
Lemma cpoly_const_mult : forall a b : R, cpoly_constant_fun _ (a[*]b) [=] cpoly_constant_fun _ a[*] cpoly_constant_fun _ b.
Definition _C_ : RingHom R R[x] := Build_RingHom _ _ _ cpoly_const_plus cpoly_const_mult cpoly_const_one.
Lemma _c_one : 1 [=] _C_ (1:R).
Lemma _c_plus : forall a b : R, _C_ (a[+]b) [=] _C_ a[+] _C_ b.
Lemma _c_mult : forall a b : R, _C_ (a[*]b) [=] _C_ a[*] _C_ b.
Lemma _c_zero : 0 [=] _C_ (0:R).
Lemma cpoly_X_ : _X_ [=] (0:RX) [+X*]1.
Lemma cpoly_C_ : forall c : R, _C_ c [=] c[+X*]0.
Lemma cpoly_const_eq : forall c d : R, c [=] d -> _C_ c [=] _C_ d.
Lemma cpoly_lin : forall (p : R[x]) (c : R), c[+X*]p [=] _C_ c[+]_X_[*]p.
Lemma poly_linear : forall c f, (cpoly_linear _ c f:RX) [=] _X_[*]f[+]_C_ c.
Lemma poly_c_apzero : forall a : R, _C_ a [#] 0 -> a [#] 0.
Lemma _c_mult_lin : forall (p : R[x]) c d, _C_ c[*] (d[+X*]p) [=] c[*]d[+X*]_C_ c[*]p.
Lemma lin_mult : forall (p q : R[x]) c, (c[+X*]p) [*]q [=] _C_ c[*]q[+]_X_[*] (p[*]q).
Lemma poly_eq_zero : forall p : R[x], p [=] cpoly_zero R -> forall x, p ! x [=] 0.
Lemma apply_wd : forall (p p' : R[x]) x x', p [=] p' -> x [=] x' -> p ! x [=] p' ! x'.
Lemma cpolyap_pres_eq : forall (f : R[x]) x y, x [=] y -> f ! x [=] f ! y.
Lemma cpolyap_strext : forall (f : R[x]) x y, f ! x [#] f ! y -> x [#] y.
Definition cpoly_csetoid_op (f : R[x]) : CSetoid_un_op R :=
Build_CSetoid_fun _ _ (fun x => f ! x) (cpolyap_strext f).
Definition FPoly p := total_eq_part _ (cpoly_csetoid_op p).
Lemma _c_apply : forall c x : R, (_C_ c) ! x [=] c.
Lemma _x_apply : forall x : R, _X_ ! x [=] x.
Lemma plus_apply : forall (p q : R[x]) x, (p[+]q) ! x [=] p ! x[+]q ! x.
Lemma inv_apply : forall (p : R[x]) x, ( [--]p) ! x [=] [--]p ! x.
Lemma minus_apply : forall (p q : R[x]) x, (p[-]q) ! x [=] p ! x[-]q ! x.
Lemma _c_mult_apply : forall (q : R[x]) c x, (_C_ c[*]q) ! x [=] c[*]q ! x.
Lemma mult_apply : forall (p q : R[x]) x, (p[*]q) ! x [=] p ! x[*]q ! x.
Lemma one_apply : forall x : R, 1 ! x [=] 1.
Lemma nexp_apply : forall (p : R[x]) n x, (p[^]n) ! x [=] p ! x[^]n.
Lemma poly_inv_apply : forall (p : R[x]) x, (cpoly_inv _ p) ! x [=] [--]p ! x.
Lemma Sum0_cpoly_ap : forall (f : N -> R[x]) a k, (∑0 k f) ! a [=] ∑0 k (fun i => (f i) ! a).
Lemma Sum_cpoly_ap : forall (f : N -> R[x]) a k l,
(∑ k l f) ! a [=] ∑ k l (fun i => (f i) ! a).
End Poly_properties.
Section Poly_Prop_Induction.
Variable CR : CRing.
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 : forall P : Cpoly_cring -> Cpoly_cring -> Prop,
(forall p, P p 0) -> (forall p, P 0 p) ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
End Poly_Prop_Induction.
Section Derivative.
Variable R:CRing.
Let R[x] := cpoly_cring R.
Fixpoint cpoly_diff (p : R[x]) : R[x] :=
match p with
| cpoly_zero => 0
| cpoly_linear c p1 => p1[+](0[+X*](cpoly_diff p1))
end.
Lemma cpoly_diff_strext : un_op_strext _ cpoly_diff.
Lemma cpoly_diff_wd : un_op_wd _ cpoly_diff.
Definition _D_ := Build_CSetoid_un_op _ _ cpoly_diff_strext.
Lemma diff_zero : _D_ 0[=]0.
Lemma diff_one : _D_ 1[=]0.
Lemma diff_const : forall c, _D_ (_C_ c)[=]0.
Lemma diff_x : _D_ _X_[=]1.
Lemma diff_linear : forall a (p:RX), _D_ (a[+X*]p)[=]p[+]_X_[*]_D_ p.
Lemma diff_plus : forall (p q:RX), _D_ (p[+]q)[=]_D_ p[+]_D_ q.
Lemma diff_c_mult : forall c (p:RX), _D_ (_C_ c[*]p)[=]_C_ c[*]_D_ p.
Lemma diff_mult : forall (p q:RX), _D_ (p[*]q)[=]_D_ p[*]q [+] p[*]_D_ q.
End Derivative.
Section Map.
Variable R S : CRing.
Variable f : RingHom R S.
Let R[x] := cpoly_cring R.
Let SX := cpoly_cring S.
Fixpoint cpoly_map_fun (p:RX) : SX :=
match p with
| cpoly_zero => cpoly_zero _
| cpoly_linear c p1 => cpoly_linear _ (f c) (cpoly_map_fun p1)
end.
Lemma cpoly_map_strext : fun_strext cpoly_map_fun.
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.
Lemma cpoly_map_pres_mult : fun_pres_mult _ _ cpoly_map_csf.
Lemma cpoly_map_pres_unit : fun_pres_unit _ _ cpoly_map_csf.
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_.
Lemma cpoly_map_C : forall c, cpoly_map (_C_ c)[=]_C_ (f c).
Lemma cpoly_map_diff : forall p, cpoly_map (_D_ p) [=] _D_ (cpoly_map p).
Lemma cpoly_map_apply : forall p x, f (p ! x)[=] (cpoly_map p) ! (f x).
End Map.
Lemma cpoly_map_compose : forall 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).
Variable CR : CRing.
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 : forall P : Cpoly_cring -> Cpoly_cring -> Prop,
(forall p, P p 0) -> (forall p, P 0 p) ->
(forall p q c d, P p q -> P (c[+X*]p) (d[+X*]q)) -> forall p q, P p q.
End Poly_Prop_Induction.
Section Derivative.
Variable R:CRing.
Let R[x] := cpoly_cring R.
Fixpoint cpoly_diff (p : R[x]) : R[x] :=
match p with
| cpoly_zero => 0
| cpoly_linear c p1 => p1[+](0[+X*](cpoly_diff p1))
end.
Lemma cpoly_diff_strext : un_op_strext _ cpoly_diff.
Lemma cpoly_diff_wd : un_op_wd _ cpoly_diff.
Definition _D_ := Build_CSetoid_un_op _ _ cpoly_diff_strext.
Lemma diff_zero : _D_ 0[=]0.
Lemma diff_one : _D_ 1[=]0.
Lemma diff_const : forall c, _D_ (_C_ c)[=]0.
Lemma diff_x : _D_ _X_[=]1.
Lemma diff_linear : forall a (p:RX), _D_ (a[+X*]p)[=]p[+]_X_[*]_D_ p.
Lemma diff_plus : forall (p q:RX), _D_ (p[+]q)[=]_D_ p[+]_D_ q.
Lemma diff_c_mult : forall c (p:RX), _D_ (_C_ c[*]p)[=]_C_ c[*]_D_ p.
Lemma diff_mult : forall (p q:RX), _D_ (p[*]q)[=]_D_ p[*]q [+] p[*]_D_ q.
End Derivative.
Section Map.
Variable R S : CRing.
Variable f : RingHom R S.
Let R[x] := cpoly_cring R.
Let SX := cpoly_cring S.
Fixpoint cpoly_map_fun (p:RX) : SX :=
match p with
| cpoly_zero => cpoly_zero _
| cpoly_linear c p1 => cpoly_linear _ (f c) (cpoly_map_fun p1)
end.
Lemma cpoly_map_strext : fun_strext cpoly_map_fun.
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.
Lemma cpoly_map_pres_mult : fun_pres_mult _ _ cpoly_map_csf.
Lemma cpoly_map_pres_unit : fun_pres_unit _ _ cpoly_map_csf.
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_.
Lemma cpoly_map_C : forall c, cpoly_map (_C_ c)[=]_C_ (f c).
Lemma cpoly_map_diff : forall p, cpoly_map (_D_ p) [=] _D_ (cpoly_map p).
Lemma cpoly_map_apply : forall p x, f (p ! x)[=] (cpoly_map p) ! (f x).
End Map.
Lemma cpoly_map_compose : forall 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).