CoRN.algebra.CPoly_NthCoeff

Require Export CPolynomials.
Require Import Morphisms.
Require Import CRings.

Polynomials: Nth Coefficient

Let R be a ring and write RX for the ring of polynomials over R.

Definitions

Section NthCoeff_def.

Variable R : CRing.

The n-th coefficient of a polynomial. The default value is Zero:CR e.g. if the n is higher than the length. For the polynomial a0 +a1 X +a2 X^2 + ... + an X^n, the Zero-th coefficient is a0, the first is a1 etcetera.

Fixpoint nth_coeff (n : nat) (p : RX) {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 : ∀ n p p', nth_coeff n p [#] nth_coeff n p' → p [#] p'.
Proof.
do 3 intro.
generalize n.
clear n.
pattern p, p' in |- ×.
apply Ccpoly_double_sym_ind.
   unfold Csymmetric in |- ×.
   intros.
   apply ap_symmetric_unfolded.
   apply X with n.
   apply ap_symmetric_unfolded.
   assumption.
  intro p0.
  pattern p0 in |- ×.
  apply Ccpoly_induc.
   simpl in |- ×.
   intros.
   elim (ap_irreflexive_unfolded _ _ X).
  do 4 intro.
  elim n.
   simpl in |- ×.
   auto.
  intros.
  cut (c [#] [0] or p1 [#] [0]).
   intro; apply _linear_ap_zero.
   auto.
  right.
  apply X with n0.
  astepr ([0]:R). auto.
  intros.
induction n as [| n Hrecn].
  simpl in X0.
  cut (c [#] d or p0 [#] q).
   auto.
  auto.
cut (c [#] d or p0 [#] q).
  auto.
right.
apply X with n.
exact X0.
Qed.

Lemma nth_coeff_wd : ∀ n p p', p [=] p' → nth_coeff n p [=] nth_coeff n p'.
Proof.
intros.
generalize (fun_strext_imp_wd _ _ (nth_coeff n)); intro.
unfold fun_wd in H0.
apply H0.
  unfold fun_strext in |- ×.
  intros.
  apply nth_coeff_strext with n.
  assumption.
assumption.
Qed.

Global Instance: ∀ n, Proper (@st_eq _ ==> @st_eq _) (nth_coeff n).
Proof. intros n ??. apply (nth_coeff_wd n). Qed.

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

Definition nonConst p : CProp := {n : nat | 0 < n | nth_coeff n p [#] [0]}.

The following is probably NOT needed. These functions are NOT extensional, that is, they are not CSetoid functions.

Fixpoint nth_coeff_ok (n : nat) (p : RX) {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 : RX) {struct p} : Prop :=
  match p with
  | cpoly_zero ⇒ False
  | 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 : ∀ m p c,
in_coeff (nth_coeff m p) p → in_coeff (nth_coeff (S m) (c [+X *]p)) (c [+X *]p).
Proof.
simpl in |- *; auto.
Qed.

End NthCoeff_def.

Implicit Arguments nth_coeff [R].
Implicit Arguments nth_coeff_fun [R].

Hint Resolve nth_coeff_wd: algebra_c.

Section NthCoeff_props.

Properties of nth_coeff

Variable R : CRing.

Lemma nth_coeff_zero : ∀ n, nth_coeff n ([0]:RX) [=] [0].
Proof.
intros.
simpl in |- ×.
algebra.
Qed.

Lemma coeff_O_lin : ∀ p (c : R), nth_coeff 0 (c [+X *]p) [=] c.
Proof.
intros.
simpl in |- ×.
algebra.
Qed.

Lemma coeff_Sm_lin : ∀ p (c : R) m, nth_coeff (S m) (c [+X *]p) [=] nth_coeff m p.
Proof.
intros.
simpl in |- ×.
algebra.
Qed.

Lemma coeff_O_c_ : ∀ c : R, nth_coeff 0 (_C_ c) [=] c.
Proof.
intros.
simpl in |- ×.
algebra.
Qed.

Lemma coeff_O_x_mult : ∀ p : RX, nth_coeff 0 (_X_[*]p) [=] [0].
Proof.
intros.
astepl (nth_coeff 0 ([0][+]_X_[*]p)).
astepl (nth_coeff 0 (_C_ [0][+]_X_[*]p)).
astepl (nth_coeff 0 ([0][+X *]p)).
simpl in |- ×.
algebra.
Qed.

Lemma coeff_Sm_x_mult : ∀ (p : RX) m, nth_coeff (S m) (_X_[*]p) [=] nth_coeff m p.
Proof.
intros.
astepl (nth_coeff (S m) ([0][+]_X_[*]p)).
astepl (nth_coeff (S m) (_C_ [0][+]_X_[*]p)).
astepl (nth_coeff (S m) ([0][+X *]p)).
simpl in |- ×.
algebra.
Qed.

Lemma coeff_Sm_mult_x_ : ∀ (p : RX) m, nth_coeff (S m) (p [*]_X_) [=] nth_coeff m p.
Proof.
intros.
astepl (nth_coeff (S m) (_X_[*]p)).
apply coeff_Sm_x_mult.
Qed.

Hint Resolve nth_coeff_zero coeff_O_lin coeff_Sm_lin coeff_O_c_
  coeff_O_x_mult coeff_Sm_x_mult coeff_Sm_mult_x_: algebra.

Lemma nth_coeff_ap_zero_imp : ∀ (p : RX) n, nth_coeff n p [#] [0] → p [#] [0].
Proof.
intros.
cut (nth_coeff n p [#] nth_coeff n [0]).
  intro H0.
  apply (nth_coeff_strext _ _ _ _ H0).
algebra.
Qed.

Lemma nth_coeff_plus : ∀ (p q : RX) n,
nth_coeff n (p [+]q) [=] nth_coeff n p [+]nth_coeff n q.
Proof.
do 2 intro.
pattern p, q in |- ×.
apply poly_double_comp_ind.
   intros.
   astepl (nth_coeff n (p1[+]q1)).
   astepr (nth_coeff n p1[+]nth_coeff n q1).
   apply H1.
  intros.
  simpl in |- ×.
  algebra.
intros.
elim n.
  simpl in |- ×.
  algebra.
intros.
astepl (nth_coeff n0 (p0[+]q0)).
generalize (H n0); intro.
astepl (nth_coeff n0 p0[+]nth_coeff n0 q0).
algebra.
Qed.

Lemma nth_coeff_inv : ∀ (p : RX) n, nth_coeff n [--]p [=] [--] (nth_coeff n p ).
Proof.
intro.
pattern p in |- ×.
apply cpoly_induc.
  intros.
  simpl in |- ×.
  algebra.
intros.
elim n.
  simpl in |- ×.
  algebra.
intros. simpl in |- ×.
apply H.
Qed.

Hint Resolve nth_coeff_inv: algebra.

Lemma nth_coeff_c_mult_p : ∀ (p : RX) c n, nth_coeff n (_C_ c [*]p) [=] c [*]nth_coeff n p.
Proof.
do 2 intro.
pattern p in |- ×.
apply cpoly_induc.
  intros.
  astepl (nth_coeff n ([0]:RX)).
  astepr (c[*][0]).
  astepl ([0]:R).
  algebra.
intros.
elim n.
  simpl in |- ×.
  algebra.
intros.
astepl (nth_coeff (S n0) (c[*]c0[+X *]_C_ c[*]p0)).
astepl (nth_coeff n0 (_C_ c[*]p0)).
astepl (c[*]nth_coeff n0 p0).
algebra.
Qed.

Lemma nth_coeff_p_mult_c_ : ∀ (p : RX) c n, nth_coeff n (p [*]_C_ c) [=] nth_coeff n p [*]c.
Proof.
intros.
astepl (nth_coeff n (_C_ c[*]p)).
astepr (c[*]nth_coeff n p).
apply nth_coeff_c_mult_p.
Qed.

Hint Resolve nth_coeff_c_mult_p nth_coeff_p_mult_c_ nth_coeff_plus: algebra.

Lemma nth_coeff_complicated : ∀ a b (p : RX) n,
nth_coeff (S n) ((_C_ a [*]_X_[+]_C_ b ) [*]p) [=] a [*]nth_coeff n p [+]b [*]nth_coeff (S n) p.
Proof.
intros.
astepl (nth_coeff (S n) (_C_ a[*]_X_[*]p[+]_C_ b[*]p)).
astepl (nth_coeff (S n) (_C_ a[*]_X_[*]p) [+]nth_coeff (S n) (_C_ b[*]p)).
astepl (nth_coeff (S n) (_C_ a[*] (_X_[*]p)) [+]b[*]nth_coeff (S n) p).
astepl (a[*]nth_coeff (S n) (_X_[*]p) [+]b[*]nth_coeff (S n) p).
algebra.
Qed.

Lemma all_nth_coeff_eq_imp : ∀ p p' : RX,
(∀ i, nth_coeff i p [=] nth_coeff i p') → p [=] p'.
Proof.
intro. induction p as [| s p Hrecp]; intros;
   [ induction p' as [| s p' Hrecp'] | induction p' as [| s0 p' Hrecp'] ]; intros.
    algebra.
   simpl in |- ×. simpl in H. simpl in Hrecp'. split.
   apply eq_symmetric_unfolded. apply (H 0). apply Hrecp'.
    intros. apply (H (S i)).
   simpl in |- ×. simpl in H. simpl in Hrecp. split.
  apply (H 0).
  change ([0] [=] (p:RX )) in |- ×. apply eq_symmetric_unfolded. simpl in |- ×. apply Hrecp.
  intros. apply (H (S i)).
  simpl in |- ×. simpl in H. split.
apply (H 0).
change ((p:RX ) [=] (p':RX )) in |- ×. apply Hrecp. intros. apply (H (S i)).
Qed.

Lemma poly_at_zero : ∀ p : RX, p ! [0] [=] nth_coeff 0 p.
Proof.
intros. induction p as [| s p Hrecp]; intros.
simpl in |- ×. algebra.
  simpl in |- ×. Step_final (s[+][0]).
Qed.

Lemma nth_coeff_inv' : ∀ (p : RX) i,
nth_coeff i (cpoly_inv _ p) [=] [--] (nth_coeff i p ).
Proof.
intros. change (nth_coeff i [--] (p:RX ) [=] [--] (nth_coeff i p)) in |- ×. algebra.
Qed.

Lemma nth_coeff_minus : ∀ (p q : RX) i,
nth_coeff i (p [-]q) [=] nth_coeff i p [-]nth_coeff i q.
Proof.
intros.
astepl (nth_coeff i (p[+][--]q)).
astepl (nth_coeff i p[+]nth_coeff i [--]q).
Step_final (nth_coeff i p[+][--] (nth_coeff i q)).
Qed.

Hint Resolve nth_coeff_minus: algebra.

Lemma nth_coeff_sum0 : ∀ (p_ : nat → RX) k n,
nth_coeff k (Sum0 n p_) [=] Sum0 n (fun i ⇒ nth_coeff k (p_ i)).
Proof.
intros. induction n as [| n Hrecn]; intros.
simpl in |- ×. algebra.
  change (nth_coeff k (Sum0 n p_[+]p_ n) [=]
    Sum0 n (fun i : nat ⇒ nth_coeff k (p_ i)) [+]nth_coeff k (p_ n)) in |- ×.
Step_final (nth_coeff k (Sum0 n p_) [+]nth_coeff k (p_ n)).
Qed.

Lemma nth_coeff_sum : ∀ (p_ : nat → RX) k m n,
nth_coeff k (Sum m n p_) [=] Sum m n (fun i ⇒ nth_coeff k (p_ i)).
Proof.
unfold Sum in |- ×. unfold Sum1 in |- ×. intros.
astepl (nth_coeff k (Sum0 (S n) p_) [-]nth_coeff k (Sum0 m p_)).
apply cg_minus_wd; apply nth_coeff_sum0.
Qed.

Lemma nth_coeff_nexp_eq : ∀ i, nth_coeff i (_X_[^]i) [=] ([1]:R ).
Proof.
intros. induction i as [| i Hreci]; intros.
simpl in |- ×. algebra.
  change (nth_coeff (S i) (_X_[^]i[*]_X_) [=] ([1]:R )) in |- ×.
Step_final (nth_coeff i (_X_[^]i):R).
Qed.

Lemma nth_coeff_nexp_neq : ∀ i j, i ≠ j → nth_coeff i (_X_[^]j) [=] ([0]:R ).
Proof.
intro; induction i as [| i Hreci]; intros;
   [ induction j as [| j Hrecj] | induction j as [| j Hrecj] ]; intros.
    elim (H (refl_equal _)).
   Step_final (nth_coeff 0 (_X_[*]_X_[^]j):R).
  simpl in |- ×. algebra.
  change (nth_coeff (S i) (_X_[^]j[*]_X_) [=] ([0]:R )) in |- ×.
astepl (nth_coeff i (_X_[^]j):R).
apply Hreci. auto.
Qed.

Lemma nth_coeff_mult : ∀ (p q : RX) n,
nth_coeff n (p [*]q) [=] Sum 0 n (fun i ⇒ nth_coeff i p [*]nth_coeff (n - i) q).
Proof.
intro; induction p as [| s p Hrecp]. intros.
  stepl (nth_coeff n ([0]:RX)).
   simpl in |- ×. apply eq_symmetric_unfolded.
   apply Sum_zero. auto with arith. intros. algebra.
    apply nth_coeff_wd.
  change ([0][=][0][*]q).
  algebra.
intros.
apply eq_transitive_unfolded with (nth_coeff n (_C_ s[*]q[+]_X_[*] ((p:RX ) [*]q))).
  apply nth_coeff_wd.
  change ((s[+X *]p) [*]q [=] _C_ s[*]q[+]_X_[*] ((p:RX ) [*]q)) in |- ×.
  astepl ((_C_ s[+]_X_[*]p) [*]q).
  Step_final (_C_ s[*]q[+]_X_[*]p[*]q).
astepl (nth_coeff n (_C_ s[*]q) [+]nth_coeff n (_X_[*] ((p:RX ) [*]q))).
astepl (s[*]nth_coeff n q[+]nth_coeff n (_X_[*] ((p:RX ) [*]q))).
induction n as [| n Hrecn]; intros.
  astepl (s[*]nth_coeff 0 q[+][0]).
  astepl (s[*]nth_coeff 0 q).
  astepl (nth_coeff 0 (cpoly_linear _ s p) [*]nth_coeff 0 q).
  pattern 0 at 2 in |- ×. replace 0 with (0 - 0).
  apply eq_symmetric_unfolded.
   apply Sum_one with (f := fun i : nat ⇒ nth_coeff i (cpoly_linear _ s p) [*]nth_coeff (0 - i) q).
  auto.
astepl (s[*]nth_coeff (S n) q[+]nth_coeff n ((p:RX ) [*]q)).
apply eq_transitive_unfolded with (nth_coeff 0 (cpoly_linear _ s p) [*]nth_coeff (S n - 0) q[+]
   Sum 1 (S n) (fun i : nat ⇒ nth_coeff i (cpoly_linear _ s p) [*]nth_coeff (S n - i) q)).
  apply bin_op_wd_unfolded. algebra.
   astepl (Sum 0 n (fun i : nat ⇒ nth_coeff i p[*]nth_coeff (n - i) q)).
  apply Sum_shift. intros. simpl in |- ×. algebra.
  apply eq_symmetric_unfolded.
apply Sum_first with (f := fun i : nat ⇒ nth_coeff i (cpoly_linear _ s p) [*]nth_coeff (S n - i) q).
Qed.

End NthCoeff_props.

Hint Resolve nth_coeff_wd: algebra_c.
Hint Resolve nth_coeff_complicated poly_at_zero nth_coeff_inv: algebra.
Hint Resolve nth_coeff_inv' nth_coeff_c_mult_p nth_coeff_mult: algebra.
Hint Resolve nth_coeff_zero nth_coeff_plus nth_coeff_minus: algebra.
Hint Resolve nth_coeff_nexp_eq nth_coeff_nexp_neq: algebra.