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: 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]# *)
31 include "tactics/RingReflection.ma".
34 The first section only proves the polynomials form a ring, and nothing more
36 Section%~\ref{section:poly-equality}% gives some basic properties of
37 equality and induction of polynomials.
38 ** Definition of polynomials; they form a ring
39 %\label{section:poly-ring}%
47 %\begin{convention}% Let [CR] be a ring.
51 alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/CR.var".
54 The intuition behind the type [cpoly] is the following
55 - [(cpoly CR)] is $CR[X]$ #CR[X]#;
56 - [cpoly_zero] is the `empty' polynomial with no coefficients;
57 - [(cpoly_linear c p)] is [c[+]X[*]p]
61 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly.ind".
63 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant.con".
65 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one.con".
68 Some useful induction lemmas for doubly quantified propositions.
71 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0.con".
73 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0.con".
75 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0'.con".
77 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0.con".
79 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0.con".
81 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0'.con".
83 (*#* *** The polynomials form a setoid
86 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_zero.con".
88 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq.con".
90 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_eq_p_zero.con".
92 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero.con".
94 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap.con".
96 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_p_zero.con".
98 inline procedural "cic:/CoRN/algebra/CPolynomials/irreflexive_cpoly_ap.con".
100 inline procedural "cic:/CoRN/algebra/CPolynomials/symmetric_cpoly_ap.con".
102 inline procedural "cic:/CoRN/algebra/CPolynomials/cotransitive_cpoly_ap.con".
104 inline procedural "cic:/CoRN/algebra/CPolynomials/tight_apart_cpoly_ap.con".
106 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CSetoid.con".
108 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid.con".
111 Now that we know that the polynomials form a setoid, we can use the
112 notation with [ [#] ] and [ [=] ]. In order to use this notation,
113 we introduce [cpoly_zero_cs] and [cpoly_linear_cs], so that Coq
114 recognizes we are talking about a setoid.
115 We formulate the induction properties and
116 the most basic properties of equality and apartness
117 in terms of these generators.
120 inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_zero_cs.con" "CPoly_CRing__".
122 inline procedural "cic:/CoRN/algebra/CPolynomials/CPoly_CRing/cpoly_linear_cs.con" "CPoly_CRing__".
124 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_ind_cs.con".
126 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_ind0_cs.con".
128 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind0_cs.con".
130 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ind_cs.con".
132 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind0_cs.con".
134 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind0_cs.con".
136 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_zero_.con".
138 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_zero.con".
140 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_eq_lin_.con".
142 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_eq_lin.con".
144 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_eq_lin_.con".
146 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_eq_lin.con".
148 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero_.con".
150 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_zero.con".
152 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_zero.con".
154 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin_.con".
156 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_zero_ap_lin.con".
158 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_ap_lin.con".
160 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin_.con".
162 inline procedural "cic:/CoRN/algebra/CPolynomials/_cpoly_lin_ap_lin.con".
164 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_ap_lin.con".
166 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_strext.con".
168 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_wd.con".
170 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun.con".
172 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_comp_ind.con".
174 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_triple_comp_ind.con".
176 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_comp_ind.con".
178 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_triple_comp_ind.con".
181 *** The polynomials form a semi-group and a monoid
184 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus.con".
186 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_cs.con".
188 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_plus.con".
190 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_zero.con".
192 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_plus_lin.con".
194 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_commutative.con".
196 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_q_ap_q.con".
198 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_p_plus_ap_p.con".
200 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_ap_zero_plus.con".
202 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_strext.con".
204 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op_wd.con".
206 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_op.con".
208 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_plus_associative.con".
210 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csemi_grp.con".
212 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cm_proof.con".
214 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cmonoid.con".
216 (*#* *** The polynomials form a group
219 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv.con".
221 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_cs.con".
223 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_zero.con".
225 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_lin.con".
227 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_strext.con".
229 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op_wd.con".
231 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_inv_op.con".
233 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cg_proof.con".
235 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cgroup.con".
237 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cag_proof.con".
239 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cabgroup.con".
241 (*#* *** The polynomials form a ring
244 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr.con".
246 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult.con".
248 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_cs.con".
250 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult_cr.con".
252 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult_cr.con".
254 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_zero.con".
256 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_strext.con".
258 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_wd.con".
260 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cs.con".
262 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_zero_mult.con".
264 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin_mult.con".
266 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_strext.con".
268 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op_wd.con".
270 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_op.con".
272 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_dist.con".
274 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_dist.con".
276 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult_cr.con".
278 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_assoc_mult.con".
280 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_zero.con".
282 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_lin.con".
284 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_commutative.con".
286 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_dist_rht.con".
288 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_assoc.con".
290 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_cr_one.con".
292 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_one_mult.con".
294 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_one.con".
296 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_mult_monoid.con".
298 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cr_non_triv.con".
300 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_is_CRing.con".
302 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_cring.con".
304 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_strext.con".
306 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_constant_wd.con".
308 inline procedural "cic:/CoRN/algebra/CPolynomials/_C_.con".
310 inline procedural "cic:/CoRN/algebra/CPolynomials/_X_.con".
312 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c.con".
314 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_strext.con".
316 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_x_minus_c_wd.con".
323 Implicit Arguments _C_ [CR].
327 Implicit Arguments _X_ [CR].
330 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_linear_fun'.con".
333 Implicit Arguments cpoly_linear_fun' [CR].
337 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
340 (*#* ** Apartness, equality, and induction
341 %\label{section:poly-equality}%
345 Section CPoly_CRing_ctd
350 Let [CR] be a ring, [p] and [q] polynomials over that ring, and [c] and [d]
351 elements of the ring.
355 alias id "CR" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/CR.var".
358 Notation RX := (cpoly_cring CR).
362 Section helpful_section
365 alias id "p" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/p.var".
367 alias id "q" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/q.var".
369 alias id "c" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/c.var".
371 alias id "d" = "cic:/CoRN/algebra/CPolynomials/CPoly_CRing_ctd/helpful_section/d.var".
373 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_zero_.con".
375 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_zero.con".
377 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_eq_linear_.con".
379 inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_eq_linear.con".
381 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_eq_linear_.con".
383 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_eq_linear.con".
385 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero_.con".
387 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_zero.con".
389 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_zero.con".
391 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear_.con".
393 inline procedural "cic:/CoRN/algebra/CPolynomials/_zero_ap_linear.con".
395 inline procedural "cic:/CoRN/algebra/CPolynomials/zero_ap_linear.con".
397 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear_.con".
399 inline procedural "cic:/CoRN/algebra/CPolynomials/_linear_ap_linear.con".
401 inline procedural "cic:/CoRN/algebra/CPolynomials/linear_ap_linear.con".
407 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_induc.con".
409 inline procedural "cic:/CoRN/algebra/CPolynomials/Ccpoly_double_sym_ind.con".
411 inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_double_comp_ind.con".
413 inline procedural "cic:/CoRN/algebra/CPolynomials/Cpoly_triple_comp_ind.con".
415 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_induc.con".
417 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_sym_ind.con".
419 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_double_comp_ind.con".
421 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_triple_comp_ind.con".
424 Transparent cpoly_cring.
428 Transparent cpoly_cgroup.
432 Transparent cpoly_csetoid.
435 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply.con".
437 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_strext.con".
439 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_wd.con".
441 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_apply_fun.con".
449 [cpoly_apply_fun] is denoted infix by [!]
450 The first argument is left implicit, so the application of
451 polynomial [f] (seen as a function) to argument [x] can be written as [f!x].
452 In the names of lemmas, we write [apply].
457 Implicit Arguments cpoly_apply_fun [CR].
461 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
465 ** Basic properties of polynomials
467 Let [R] be a ring and write [RX] for the ring of polynomials over [R].
472 Section Poly_properties
475 alias id "R" = "cic:/CoRN/algebra/CPolynomials/Poly_properties/R.var".
478 Notation RX := (cpoly_cring R).
482 *** Constant and identity
485 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_X_.con".
487 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_C_.con".
490 Hint Resolve cpoly_X_ cpoly_C_: algebra.
493 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_const_eq.con".
495 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_zero.con".
497 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_one.con".
499 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult.con".
501 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_lin.con".
504 Hint Resolve cpoly_lin: algebra.
509 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_linear.con".
512 Hint Resolve _c_zero: algebra.
515 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_c_apzero.con".
517 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_lin.con".
521 inline procedural "cic:/CoRN/algebra/CPolynomials/lin_mult.con".
524 Hint Resolve lin_mult: algebra.
527 (*#* *** Application of polynomials
530 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_eq_zero.con".
532 inline procedural "cic:/CoRN/algebra/CPolynomials/apply_wd.con".
534 inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_pres_eq.con".
536 inline procedural "cic:/CoRN/algebra/CPolynomials/cpolyap_strext.con".
538 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_csetoid_op.con".
540 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_apply.con".
542 inline procedural "cic:/CoRN/algebra/CPolynomials/_x_apply.con".
544 inline procedural "cic:/CoRN/algebra/CPolynomials/plus_apply.con".
546 inline procedural "cic:/CoRN/algebra/CPolynomials/inv_apply.con".
549 Hint Resolve plus_apply inv_apply: algebra.
552 inline procedural "cic:/CoRN/algebra/CPolynomials/minus_apply.con".
554 inline procedural "cic:/CoRN/algebra/CPolynomials/_c_mult_apply.con".
557 Hint Resolve _c_mult_apply: algebra.
560 inline procedural "cic:/CoRN/algebra/CPolynomials/mult_apply.con".
563 Hint Resolve mult_apply: algebra.
566 inline procedural "cic:/CoRN/algebra/CPolynomials/one_apply.con".
569 Hint Resolve one_apply: algebra.
572 inline procedural "cic:/CoRN/algebra/CPolynomials/nexp_apply.con".
576 inline procedural "cic:/CoRN/algebra/CPolynomials/poly_inv_apply.con".
578 inline procedural "cic:/CoRN/algebra/CPolynomials/Sum0_cpoly_ap.con".
580 inline procedural "cic:/CoRN/algebra/CPolynomials/Sum_cpoly_ap.con".
586 (*#* ** Induction properties of polynomials for [Prop]
590 Section Poly_Prop_Induction
593 alias id "CR" = "cic:/CoRN/algebra/CPolynomials/Poly_Prop_Induction/CR.var".
596 Notation Cpoly := (cpoly CR).
600 Notation Cpoly_zero := (cpoly_zero CR).
604 Notation Cpoly_linear := (cpoly_linear CR).
608 Notation Cpoly_cring := (cpoly_cring CR).
611 inline procedural "cic:/CoRN/algebra/CPolynomials/cpoly_double_ind.con".
614 End Poly_Prop_Induction
618 Hint Resolve poly_linear cpoly_lin: algebra.
622 Hint Resolve apply_wd cpoly_const_eq: algebra_c.
626 Hint Resolve _c_apply _x_apply inv_apply plus_apply minus_apply mult_apply
631 Hint Resolve one_apply _c_zero _c_one _c_mult: algebra.
635 Hint Resolve poly_inv_apply: algebra.
639 Hint Resolve _c_mult_lin: algebra.