(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: CPoly_NthCoeff.v,v 1.6 2004/04/23 10:00:53 lcf Exp $ *) include "algebra/CPolynomials.ma". (*#* * Polynomials: Nth Coefficient %\begin{convention}% Let [R] be a ring and write [RX] for the ring of polynomials over [R]. %\end{convention}% ** Definitions *) (* UNEXPORTED Section NthCoeff_def *) (* UNEXPORTED cic:/CoRN/algebra/CPoly_NthCoeff/NthCoeff_def/R.var *) (* begin hide *) (* NOTATION Notation RX := (cpoly_cring R). *) (* end hide *) (*#* 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 $a_0 +a_1 X +a_2 X^2 + \cdots + a_n X^n$ #a0 +a1 X +a2 X^2 + ... + an X^n#, the [Zero]-th coefficient is $a_0$#a0#, the first is $a_1$#a1# etcetera. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff.con" as definition. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_wd.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_fun.con" as definition. (*#* %\begin{shortcoming}% 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)]. %\end{shortcoming}% *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nonConst.con" as definition. (*#* The following is probably NOT needed. These functions are NOT extensional, that is, they are not CSetoid functions. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_ok.con" as definition. (* The in_coeff predicate*) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/in_coeff.con" as definition. (*#* The [cpoly_zero] case should be [c [=] Zero] in order to be extensional. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_S.con" as lemma. (* UNEXPORTED End NthCoeff_def *) (* UNEXPORTED Implicit Arguments nth_coeff [R]. *) (* UNEXPORTED Implicit Arguments nth_coeff_fun [R]. *) (* UNEXPORTED Hint Resolve nth_coeff_wd: algebra_c. *) (* UNEXPORTED Section NthCoeff_props *) (*#* ** Properties of [nth_coeff] *) (* UNEXPORTED cic:/CoRN/algebra/CPoly_NthCoeff/NthCoeff_props/R.var *) (* begin hide *) (* NOTATION Notation RX := (cpoly_cring R). *) (* end hide *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_lin.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_lin.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_c_.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_x_mult.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_x_mult.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_mult_x_.con" as lemma. (* UNEXPORTED 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. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_ap_zero_imp.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_plus.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_inv.con" as lemma. (* UNEXPORTED Hint Resolve nth_coeff_inv: algebra. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_c_mult_p.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_p_mult_c_.con" as lemma. (* UNEXPORTED Hint Resolve nth_coeff_c_mult_p nth_coeff_p_mult_c_ nth_coeff_plus: algebra. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_complicated.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/all_nth_coeff_eq_imp.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/poly_at_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_inv'.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_minus.con" as lemma. (* UNEXPORTED Hint Resolve nth_coeff_minus: algebra. *) inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_sum0.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_sum.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_nexp_eq.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_nexp_neq.con" as lemma. inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_mult.con" as lemma. (* UNEXPORTED End NthCoeff_props *) (* UNEXPORTED Hint Resolve nth_coeff_wd: algebra_c. *) (* UNEXPORTED Hint Resolve nth_coeff_complicated poly_at_zero nth_coeff_inv: algebra. *) (* UNEXPORTED Hint Resolve nth_coeff_inv' nth_coeff_c_mult_p nth_coeff_mult: algebra. *) (* UNEXPORTED Hint Resolve nth_coeff_zero nth_coeff_plus nth_coeff_minus: algebra. *) (* UNEXPORTED Hint Resolve nth_coeff_nexp_eq nth_coeff_nexp_neq: algebra. *)