1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CPoly_NthCoeff.v,v 1.6 2004/04/23 10:00:53 lcf Exp $ *)
21 include "algebra/CPolynomials.ma".
24 * Polynomials: Nth Coefficient
25 %\begin{convention}% Let [R] be a ring and write [RX] for the ring of
36 alias id "R" = "cic:/CoRN/algebra/CPoly_NthCoeff/NthCoeff_def/R.var".
41 Notation RX := (cpoly_cring R).
47 The [n]-th coefficient of a polynomial. The default value is
48 [Zero:CR] e.g. if the [n] is higher than the length. For the
49 polynomial $a_0 +a_1 X +a_2 X^2 + \cdots + a_n X^n$ #a0 +a1 X +a2 X^2
50 + ... + an X^n#, the [Zero]-th coefficient is $a_0$#a0#, the first
51 is $a_1$#a1# etcetera. *)
53 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff.con" as definition.
55 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_strext.con" as lemma.
57 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_wd.con" as lemma.
59 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_fun.con" as definition.
63 We would like to use [nth_coeff_fun n] all the time.
64 However, Coq's coercion mechanism doesn't support this properly:
66 [(nth_coeff_fun n p)] won't get parsed, and has to be written as
67 [((nth_coeff_fun n) p)] instead.
69 So, in the names of lemmas, we write [(nth_coeff n p)],
70 which always (e.g. in proofs) can be converted
71 to [((nth_coeff_fun n) p)].
75 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nonConst.con" as definition.
78 The following is probably NOT needed. These functions are
79 NOT extensional, that is, they are not CSetoid functions.
82 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_ok.con" as definition.
84 (* The in_coeff predicate*)
86 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/in_coeff.con" as definition.
89 The [cpoly_zero] case should be [c [=] Zero] in order to be extensional.
92 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_S.con" as lemma.
99 Implicit Arguments nth_coeff [R].
103 Implicit Arguments nth_coeff_fun [R].
107 Hint Resolve nth_coeff_wd: algebra_c.
111 Section NthCoeff_props
114 (*#* ** Properties of [nth_coeff] *)
116 alias id "R" = "cic:/CoRN/algebra/CPoly_NthCoeff/NthCoeff_props/R.var".
121 Notation RX := (cpoly_cring R).
126 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_zero.con" as lemma.
128 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_lin.con" as lemma.
130 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_lin.con" as lemma.
132 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_c_.con" as lemma.
134 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_x_mult.con" as lemma.
136 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_x_mult.con" as lemma.
138 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_mult_x_.con" as lemma.
141 Hint Resolve nth_coeff_zero coeff_O_lin coeff_Sm_lin coeff_O_c_
142 coeff_O_x_mult coeff_Sm_x_mult coeff_Sm_mult_x_: algebra.
145 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_ap_zero_imp.con" as lemma.
147 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_plus.con" as lemma.
149 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_inv.con" as lemma.
152 Hint Resolve nth_coeff_inv: algebra.
155 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_c_mult_p.con" as lemma.
157 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_p_mult_c_.con" as lemma.
160 Hint Resolve nth_coeff_c_mult_p nth_coeff_p_mult_c_ nth_coeff_plus: algebra.
163 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_complicated.con" as lemma.
165 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/all_nth_coeff_eq_imp.con" as lemma.
167 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/poly_at_zero.con" as lemma.
169 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_inv'.con" as lemma.
171 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_minus.con" as lemma.
174 Hint Resolve nth_coeff_minus: algebra.
177 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_sum0.con" as lemma.
179 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_sum.con" as lemma.
181 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_nexp_eq.con" as lemma.
183 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_nexp_neq.con" as lemma.
185 inline procedural "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_mult.con" as lemma.
192 Hint Resolve nth_coeff_wd: algebra_c.
196 Hint Resolve nth_coeff_complicated poly_at_zero nth_coeff_inv: algebra.
200 Hint Resolve nth_coeff_inv' nth_coeff_c_mult_p nth_coeff_mult: algebra.
204 Hint Resolve nth_coeff_zero nth_coeff_plus nth_coeff_minus: algebra.
208 Hint Resolve nth_coeff_nexp_eq nth_coeff_nexp_neq: algebra.