Polynomials: Nth Coefficient
Let R be a ring and write R[x] for the ring of polynomials over R.Definitions
The n-th coefficient of a polynomial. The default value is
0:CR e.g. if the n is higher than the length. For the
polynomial a0 +a1 X +a2 X^2
+ ... + an X^n, the 0-th coefficient is a0, the first
is a1 etcetera.
Fixpoint nth_coeff (n : N) (p : R[x]) {struct p} : R :=
match p with
| cpoly_zero => 0
| cpoly_linear c q =>
match n with
| O => c
| S m => nth_coeff m q
end
end.
Lemma nth_coeff_strext : forall n p p', nth_coeff n p [#] nth_coeff n p' -> p [#] p'.
Lemma nth_coeff_wd : forall n p p', p [=] p' -> nth_coeff n p [=] nth_coeff n p'.
Definition nth_coeff_fun n := Build_CSetoid_fun _ _ _ (nth_coeff_strext n).
We would like to use nth_coeff_fun n all the time.
However, Coq's coercion mechanism doesn't support this properly:
the term
(nth_coeff_fun n p) won't get parsed, and has to be written as
((nth_coeff_fun n) p) instead.
So, in the names of lemmas, we write (nth_coeff n p), which always (e.g. in proofs) can be converted to ((nth_coeff_fun n) p).
So, in the names of lemmas, we write (nth_coeff n p), which always (e.g. in proofs) can be converted to ((nth_coeff_fun n) p).
The following is probably NOT needed. These functions are
NOT extensional, that is, they are not CSetoid functions.
Fixpoint nth_coeff_ok (n : N) (p : R[x]) {struct p} : bool :=
match n, p with
| O, cpoly_zero => false
| O, cpoly_linear c q => true
| S m, cpoly_zero => false
| S m, cpoly_linear c q => nth_coeff_ok m q
end.
Fixpoint in_coeff (c : R) (p : R[x]) {struct p} : Prop :=
match p with
| cpoly_zero => ⊥
| cpoly_linear d q => c [=] d \/ in_coeff c q
end.
The cpoly_zero case should be c ≡ 0 in order to be extensional.
Lemma nth_coeff_S : forall m p c,
in_coeff (nth_coeff m p) p -> in_coeff (nth_coeff (S m) (c[+X*]p)) (c[+X*]p).
End NthCoeff_def.
Section NthCoeff_props.
Variable R : CRing.
Lemma nth_coeff_zero : forall n, nth_coeff n (0:RX) [=] 0.
Lemma coeff_O_lin : forall p (c : R), nth_coeff 0 (c[+X*]p) [=] c.
Lemma coeff_Sm_lin : forall p (c : R) m, nth_coeff (S m) (c[+X*]p) [=] nth_coeff m p.
Lemma coeff_O_c_ : forall c : R, nth_coeff 0 (_C_ c) [=] c.
Lemma coeff_O_x_mult : forall p : R[x], nth_coeff 0 (_X_[*]p) [=] 0.
Lemma coeff_Sm_x_mult : forall (p : R[x]) m, nth_coeff (S m) (_X_[*]p) [=] nth_coeff m p.
Lemma coeff_Sm_mult_x_ : forall (p : R[x]) m, nth_coeff (S m) (p[*]_X_) [=] nth_coeff m p.
Lemma nth_coeff_ap_zero_imp : forall (p : R[x]) n, nth_coeff n p [#] 0 -> p [#] 0.
Lemma nth_coeff_plus : forall (p q : R[x]) n,
nth_coeff n (p[+]q) [=] nth_coeff n p[+]nth_coeff n q.
Lemma nth_coeff_inv : forall (p : R[x]) n, nth_coeff n [--]p [=] [--] (nth_coeff n p).
Lemma nth_coeff_c_mult_p : forall (p : R[x]) c n, nth_coeff n (_C_ c[*]p) [=] c[*]nth_coeff n p.
Lemma nth_coeff_p_mult_c_ : forall (p : R[x]) c n, nth_coeff n (p[*]_C_ c) [=] nth_coeff n p[*]c.
Lemma nth_coeff_complicated : forall a b (p : R[x]) n,
nth_coeff (S n) ((_C_ a[*]_X_[+]_C_ b) [*]p) [=] a[*]nth_coeff n p[+]b[*]nth_coeff (S n) p.
Lemma all_nth_coeff_eq_imp : forall p p' : R[x],
(forall i, nth_coeff i p [=] nth_coeff i p') -> p [=] p'.
Lemma poly_at_zero : forall p : R[x], p ! 0 [=] nth_coeff 0 p.
Lemma nth_coeff_inv' : forall (p : R[x]) i,
nth_coeff i (cpoly_inv _ p) [=] [--] (nth_coeff i p).
Lemma nth_coeff_minus : forall (p q : R[x]) i,
nth_coeff i (p[-]q) [=] nth_coeff i p[-]nth_coeff i q.
Lemma nth_coeff_sum0 : forall (p_ : N -> R[x]) k n,
nth_coeff k (∑0 n p_) [=] ∑0 n (fun i => nth_coeff k (p_ i)).
Lemma nth_coeff_sum : forall (p_ : N -> R[x]) k m n,
nth_coeff k (∑ m n p_) [=] ∑ m n (fun i => nth_coeff k (p_ i)).
Lemma nth_coeff_nexp_eq : forall i, nth_coeff i (_X_[^]i) [=] (1:R).
Lemma nth_coeff_nexp_neq : forall i j, i <> j -> nth_coeff i (_X_[^]j) [=] (0:R).
Lemma nth_coeff_mult : forall (p q : R[x]) n,
nth_coeff n (p[*]q) [=] ∑ 0 n (fun i => nth_coeff i p[*]nth_coeff (n - i) q).
End NthCoeff_props.