helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_NthCoeff".
  18
  19 include "CoRN_notation.ma".
  20
  21 (* $Id: CPoly_NthCoeff.v,v 1.6 2004/04/23 10:00:53 lcf Exp $ *)
  22
  23 include "algebra/CPolynomials.ma".
  24
  25 (*#*
  26 * Polynomials: Nth Coefficient
  27 %\begin{convention}% Let [R] be a ring and write [RX] for the ring of
  28 polynomials over [R].
  29 %\end{convention}%
  30
  31 ** Definitions
  32 *)
  33
  34 (* UNEXPORTED
  35 Section NthCoeff_def.
  36 *)
  37
  38 inline "cic:/CoRN/algebra/CPoly_NthCoeff/R.var".
  39
  40 (* begin hide *)
  41
  42 (* end hide *)
  43
  44 (*#*
  45 The [n]-th coefficient of a polynomial. The default value is
  46 [Zero:CR] e.g. if the [n] is higher than the length. For the
  47 polynomial $a_0 +a_1 X +a_2 X^2 + \cdots + a_n X^n$ #a0 +a1 X +a2 X^2
  48 + ... + an X^n#, the [Zero]-th coefficient is $a_0$#a0#, the first
  49 is $a_1$#a1# etcetera.  *)
  50
  51 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff.con".
  52
  53 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_strext.con".
  54
  55 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_wd.con".
  56
  57 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_fun.con".
  58
  59 (*#*
  60 %\begin{shortcoming}%
  61 We would like to use [nth_coeff_fun n] all the time.
  62 However, Coq's coercion mechanism doesn't support this properly:
  63 the term
  64 [(nth_coeff_fun n p)] won't get parsed, and has to be written as
  65 [((nth_coeff_fun n) p)] instead.
  66
  67 So, in the names of lemmas, we write [(nth_coeff n p)],
  68 which always (e.g. in proofs) can be converted
  69 to [((nth_coeff_fun n) p)].
  70 %\end{shortcoming}%
  71 *)
  72
  73 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nonConst.con".
  74
  75 (*#*
  76 The following is probably NOT needed.  These functions are
  77 NOT extensional, that is, they are not CSetoid functions.
  78 *)
  79
  80 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_ok.con".
  81
  82 (* The in_coeff predicate*)
  83
  84 inline "cic:/CoRN/algebra/CPoly_NthCoeff/in_coeff.con".
  85
  86 (*#*
  87 The [cpoly_zero] case should be [c [=] Zero] in order to be extensional.
  88 *)
  89
  90 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_S.con".
  91
  92 (* UNEXPORTED
  93 End NthCoeff_def.
  94 *)
  95
  96 (* UNEXPORTED
  97 Implicit Arguments nth_coeff [R].
  98 *)
  99
 100 (* UNEXPORTED
 101 Implicit Arguments nth_coeff_fun [R].
 102 *)
 103
 104 (* UNEXPORTED
 105 Hint Resolve nth_coeff_wd: algebra_c.
 106 *)
 107
 108 (* UNEXPORTED
 109 Section NthCoeff_props.
 110 *)
 111
 112 (*#* ** Properties of [nth_coeff] *)
 113
 114 inline "cic:/CoRN/algebra/CPoly_NthCoeff/R.var".
 115
 116 (* begin hide *)
 117
 118 (* end hide *)
 119
 120 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_zero.con".
 121
 122 inline "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_lin.con".
 123
 124 inline "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_lin.con".
 125
 126 inline "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_c_.con".
 127
 128 inline "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_O_x_mult.con".
 129
 130 inline "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_x_mult.con".
 131
 132 inline "cic:/CoRN/algebra/CPoly_NthCoeff/coeff_Sm_mult_x_.con".
 133
 134 (* UNEXPORTED
 135 Hint Resolve nth_coeff_zero coeff_O_lin coeff_Sm_lin coeff_O_c_
 136   coeff_O_x_mult coeff_Sm_x_mult coeff_Sm_mult_x_: algebra.
 137 *)
 138
 139 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_ap_zero_imp.con".
 140
 141 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_plus.con".
 142
 143 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_inv.con".
 144
 145 (* UNEXPORTED
 146 Hint Resolve nth_coeff_inv: algebra.
 147 *)
 148
 149 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_c_mult_p.con".
 150
 151 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_p_mult_c_.con".
 152
 153 (* UNEXPORTED
 154 Hint Resolve nth_coeff_c_mult_p nth_coeff_p_mult_c_ nth_coeff_plus: algebra.
 155 *)
 156
 157 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_complicated.con".
 158
 159 inline "cic:/CoRN/algebra/CPoly_NthCoeff/all_nth_coeff_eq_imp.con".
 160
 161 inline "cic:/CoRN/algebra/CPoly_NthCoeff/poly_at_zero.con".
 162
 163 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_inv'.con".
 164
 165 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_minus.con".
 166
 167 (* UNEXPORTED
 168 Hint Resolve nth_coeff_minus: algebra.
 169 *)
 170
 171 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_sum0.con".
 172
 173 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_sum.con".
 174
 175 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_nexp_eq.con".
 176
 177 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_nexp_neq.con".
 178
 179 inline "cic:/CoRN/algebra/CPoly_NthCoeff/nth_coeff_mult.con".
 180
 181 (* UNEXPORTED
 182 End NthCoeff_props.
 183 *)
 184
 185 (* UNEXPORTED
 186 Hint Resolve nth_coeff_wd: algebra_c.
 187 *)
 188
 189 (* UNEXPORTED
 190 Hint Resolve nth_coeff_complicated poly_at_zero nth_coeff_inv: algebra.
 191 *)
 192
 193 (* UNEXPORTED
 194 Hint Resolve nth_coeff_inv' nth_coeff_c_mult_p nth_coeff_mult: algebra.
 195 *)
 196
 197 (* UNEXPORTED
 198 Hint Resolve nth_coeff_zero nth_coeff_plus nth_coeff_minus: algebra.
 199 *)
 200
 201 (* UNEXPORTED
 202 Hint Resolve nth_coeff_nexp_eq nth_coeff_nexp_neq: algebra.
 203 *)
 204