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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPolynomials".
19 (* $Id: CPolynomials.v,v 1.9 2004/04/23 10:00:53 lcf Exp $ *)
21 (*#* printing _X_ %\ensuremath{x}% *)
23 (*#* printing _C_ %\ensuremath\diamond% *)
25 (*#* printing [+X*] %\ensuremath{+x\times}% #+x×# *)
27 (*#* printing RX %\ensuremath{R[x]}% #R[x]# *)
29 (*#* printing FX %\ensuremath{F[x]}% #F[x]# *)
36 The first section only proves the polynomials form a ring, and nothing more
38 Section%~\ref{section:poly-equality}% gives some basic properties of
39 equality and induction of polynomials.
40 ** Definition of polynomials; they form a ring
41 %\label{section:poly-ring}%
49 %\begin{convention}% Let [CR] be a ring.
53 inline cic:/CoRN/algebra/CPolynomials/CR.var.
56 The intuition behind the type [cpoly] is the following
57 - [(cpoly CR)] is $CR[X]$ #CR[X]#;
58 - [cpoly_zero] is the `empty' polynomial with no coefficients;
59 - [(cpoly_linear c p)] is [c[+]X[*]p]
63 inline cic:/CoRN/algebra/CPolynomials/cpoly.ind.
65 inline cic:/CoRN/algebra/CPolynomials/cpoly_constant.con.
67 inline cic:/CoRN/algebra/CPolynomials/cpoly_one.con.
70 Some useful induction lemmas for doubly quantified propositions.
73 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0.con.
75 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0.con.
77 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0'.con.
79 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0.con.
81 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0.con.
83 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0'.con.
85 (*#* *** The polynomials form a setoid
88 inline cic:/CoRN/algebra/CPolynomials/cpoly_eq_zero.con.
90 inline cic:/CoRN/algebra/CPolynomials/cpoly_eq.con.
92 inline cic:/CoRN/algebra/CPolynomials/cpoly_eq_p_zero.con.
94 inline cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero.con.
96 inline cic:/CoRN/algebra/CPolynomials/cpoly_ap.con.
98 inline cic:/CoRN/algebra/CPolynomials/cpoly_ap_p_zero.con.
100 inline cic:/CoRN/algebra/CPolynomials/irreflexive_cpoly_ap.con.
102 inline cic:/CoRN/algebra/CPolynomials/symmetric_cpoly_ap.con.
104 inline cic:/CoRN/algebra/CPolynomials/cotransitive_cpoly_ap.con.
106 inline cic:/CoRN/algebra/CPolynomials/tight_apart_cpoly_ap.con.
108 inline cic:/CoRN/algebra/CPolynomials/cpoly_is_CSetoid.con.
110 inline cic:/CoRN/algebra/CPolynomials/cpoly_csetoid.con.
113 Now that we know that the polynomials form a setoid, we can use the
114 notation with [ [#] ] and [ [=] ]. In order to use this notation,
115 we introduce [cpoly_zero_cs] and [cpoly_linear_cs], so that Coq
116 recognizes we are talking about a setoid.
117 We formulate the induction properties and
118 the most basic properties of equality and apartness
119 in terms of these generators.
122 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_cs.con.
124 inline cic:/CoRN/algebra/CPolynomials/cpoly_linear_cs.con.
126 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con.
128 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0_cs.con.
130 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0_cs.con.
132 inline cic:/CoRN/algebra/CPolynomials/cpoly_ind_cs.con.
134 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0_cs.con.
136 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0_cs.con.
138 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_zero_.con.
140 inline cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_zero.con.
142 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_eq_lin_.con.
144 inline cic:/CoRN/algebra/CPolynomials/_cpoly_zero_eq_lin.con.
146 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_lin_.con.
148 inline cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_lin.con.
150 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero_.con.
152 inline cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_zero.con.
154 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero.con.
156 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin_.con.
158 inline cic:/CoRN/algebra/CPolynomials/_cpoly_zero_ap_lin.con.
160 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin.con.
162 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin_.con.
164 inline cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_lin.con.
166 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin.con.
168 inline cic:/CoRN/algebra/CPolynomials/cpoly_linear_strext.con.
170 inline cic:/CoRN/algebra/CPolynomials/cpoly_linear_wd.con.
172 inline cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun.con.
174 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_comp_ind.con.
176 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_triple_comp_ind.con.
178 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_comp_ind.con.
180 inline cic:/CoRN/algebra/CPolynomials/cpoly_triple_comp_ind.con.
183 *** The polynomials form a semi-group and a monoid
186 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus.con.
188 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_cs.con.
190 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_plus.con.
192 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_zero.con.
194 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_plus_lin.con.
196 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_commutative.con.
198 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_q_ap_q.con.
200 inline cic:/CoRN/algebra/CPolynomials/cpoly_p_plus_ap_p.con.
202 inline cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero_plus.con.
204 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_strext.con.
206 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_wd.con.
208 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_op.con.
210 inline cic:/CoRN/algebra/CPolynomials/cpoly_plus_associative.con.
212 inline cic:/CoRN/algebra/CPolynomials/cpoly_csemi_grp.con.
214 inline cic:/CoRN/algebra/CPolynomials/cpoly_cm_proof.con.
216 inline cic:/CoRN/algebra/CPolynomials/cpoly_cmonoid.con.
218 (*#* *** The polynomials form a group
221 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv.con.
223 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv_cs.con.
225 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv_zero.con.
227 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv_lin.con.
229 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_strext.con.
231 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_wd.con.
233 inline cic:/CoRN/algebra/CPolynomials/cpoly_inv_op.con.
235 inline cic:/CoRN/algebra/CPolynomials/cpoly_cg_proof.con.
237 inline cic:/CoRN/algebra/CPolynomials/cpoly_cgroup.con.
239 inline cic:/CoRN/algebra/CPolynomials/cpoly_cag_proof.con.
241 inline cic:/CoRN/algebra/CPolynomials/cpoly_cabgroup.con.
243 (*#* *** The polynomials form a ring
246 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr.con.
248 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult.con.
250 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_cs.con.
252 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult_cr.con.
254 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult_cr.con.
256 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_zero.con.
258 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_strext.con.
260 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_wd.con.
262 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cs.con.
264 inline cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult.con.
266 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult.con.
268 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_strext.con.
270 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_wd.con.
272 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_op.con.
274 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_dist.con.
276 inline cic:/CoRN/algebra/CPolynomials/cpoly_cr_dist.con.
278 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult_cr.con.
280 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult.con.
282 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_zero.con.
284 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_lin.con.
286 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_commutative.con.
288 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_dist_rht.con.
290 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_assoc.con.
292 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_one.con.
294 inline cic:/CoRN/algebra/CPolynomials/cpoly_one_mult.con.
296 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_one.con.
298 inline cic:/CoRN/algebra/CPolynomials/cpoly_mult_monoid.con.
300 inline cic:/CoRN/algebra/CPolynomials/cpoly_cr_non_triv.con.
302 inline cic:/CoRN/algebra/CPolynomials/cpoly_is_CRing.con.
304 inline cic:/CoRN/algebra/CPolynomials/cpoly_cring.con.
306 inline cic:/CoRN/algebra/CPolynomials/cpoly_constant_strext.con.
308 inline cic:/CoRN/algebra/CPolynomials/cpoly_constant_wd.con.
310 inline cic:/CoRN/algebra/CPolynomials/_C_.con.
312 inline cic:/CoRN/algebra/CPolynomials/_X_.con.
314 inline cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c.con.
316 inline cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_strext.con.
318 inline cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con.
325 Implicit Arguments _C_ [CR].
329 Implicit Arguments _X_ [CR].
332 inline cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con.
335 Implicit Arguments cpoly_linear_fun' [CR].
338 (*#* ** Apartness, equality, and induction
339 %\label{section:poly-equality}%
343 Section CPoly_CRing_ctd.
348 Let [CR] be a ring, [p] and [q] polynomials over that ring, and [c] and [d]
349 elements of the ring.
353 inline cic:/CoRN/algebra/CPolynomials/CR.var.
356 Section helpful_section.
359 inline cic:/CoRN/algebra/CPolynomials/p.var.
361 inline cic:/CoRN/algebra/CPolynomials/q.var.
363 inline cic:/CoRN/algebra/CPolynomials/c.var.
365 inline cic:/CoRN/algebra/CPolynomials/d.var.
367 inline cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con.
369 inline cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con.
371 inline cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con.
373 inline cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con.
375 inline cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con.
377 inline cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con.
379 inline cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con.
381 inline cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con.
383 inline cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con.
385 inline cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con.
387 inline cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con.
389 inline cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con.
391 inline cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con.
393 inline cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con.
395 inline cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con.
401 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con.
403 inline cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con.
405 inline cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con.
407 inline cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con.
409 inline cic:/CoRN/algebra/CPolynomials/cpoly_induc.con.
411 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con.
413 inline cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con.
415 inline cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con.
418 Transparent cpoly_cring.
422 Transparent cpoly_cgroup.
426 Transparent cpoly_csetoid.
429 inline cic:/CoRN/algebra/CPolynomials/cpoly_apply.con.
431 inline cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con.
433 inline cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con.
435 inline cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con.
443 [cpoly_apply_fun] is denoted infix by [!]
444 The first argument is left implicit, so the application of
445 polynomial [f] (seen as a function) to argument [x] can be written as [f!x].
446 In the names of lemmas, we write [apply].
451 Implicit Arguments cpoly_apply_fun [CR].
455 ** Basic properties of polynomials
457 Let [R] be a ring and write [RX] for the ring of polynomials over [R].
462 Section Poly_properties.
465 inline cic:/CoRN/algebra/CPolynomials/R.var.
468 *** Constant and identity
471 inline cic:/CoRN/algebra/CPolynomials/cpoly_X_.con.
473 inline cic:/CoRN/algebra/CPolynomials/cpoly_C_.con.
476 Hint Resolve cpoly_X_ cpoly_C_: algebra.
479 inline cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con.
481 inline cic:/CoRN/algebra/CPolynomials/_c_zero.con.
483 inline cic:/CoRN/algebra/CPolynomials/_c_one.con.
485 inline cic:/CoRN/algebra/CPolynomials/_c_mult.con.
487 inline cic:/CoRN/algebra/CPolynomials/cpoly_lin.con.
490 Hint Resolve cpoly_lin: algebra.
495 inline cic:/CoRN/algebra/CPolynomials/poly_linear.con.
498 Hint Resolve _c_zero: algebra.
501 inline cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con.
503 inline cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con.
507 inline cic:/CoRN/algebra/CPolynomials/lin_mult.con.
510 Hint Resolve lin_mult: algebra.
513 (*#* *** Application of polynomials
516 inline cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con.
518 inline cic:/CoRN/algebra/CPolynomials/apply_wd.con.
520 inline cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con.
522 inline cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con.
524 inline cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con.
526 inline cic:/CoRN/algebra/CPolynomials/_c_apply.con.
528 inline cic:/CoRN/algebra/CPolynomials/_x_apply.con.
530 inline cic:/CoRN/algebra/CPolynomials/plus_apply.con.
532 inline cic:/CoRN/algebra/CPolynomials/inv_apply.con.
535 Hint Resolve plus_apply inv_apply: algebra.
538 inline cic:/CoRN/algebra/CPolynomials/minus_apply.con.
540 inline cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con.
543 Hint Resolve _c_mult_apply: algebra.
546 inline cic:/CoRN/algebra/CPolynomials/mult_apply.con.
549 Hint Resolve mult_apply: algebra.
552 inline cic:/CoRN/algebra/CPolynomials/one_apply.con.
555 Hint Resolve one_apply: algebra.
558 inline cic:/CoRN/algebra/CPolynomials/nexp_apply.con.
562 inline cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con.
564 inline cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con.
566 inline cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con.
572 (*#* ** Induction properties of polynomials for [Prop]
576 Section Poly_Prop_Induction.
579 inline cic:/CoRN/algebra/CPolynomials/CR.var.
581 inline cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con.
584 End Poly_Prop_Induction.
588 Hint Resolve poly_linear cpoly_lin: algebra.
592 Hint Resolve apply_wd cpoly_const_eq: algebra_c.
596 Hint Resolve _c_apply _x_apply inv_apply plus_apply minus_apply mult_apply
601 Hint Resolve one_apply _c_zero _c_one _c_mult: algebra.
605 Hint Resolve poly_inv_apply: algebra.
609 Hint Resolve _c_mult_lin: algebra.