]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/algebra/CFields.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / CoRN / algebra / CFields.mma
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 include "CoRN.ma".
18
19 (* $Id: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *)
20
21 (*#* printing [/] %\ensuremath{/}% #/# *)
22
23 (*#* printing [//] %\ensuremath\ddagger% #‡# *)
24
25 (*#* printing {/} %\ensuremath{/}% #/# *)
26
27 (*#* printing {1/} %\ensuremath{\frac1\cdot}% #1/# *)
28
29 (*#* printing [/]?[//] %\ensuremath{/?\ddagger}% #/?‡# *)
30
31 include "algebra/CRings.ma".
32
33 (* UNEXPORTED
34 Transparent sym_eq.
35 *)
36
37 (* UNEXPORTED
38 Transparent f_equal.
39 *)
40
41 (* UNEXPORTED
42 Transparent cs_crr.
43 *)
44
45 (* UNEXPORTED
46 Transparent csg_crr.
47 *)
48
49 (* UNEXPORTED
50 Transparent cm_crr.
51 *)
52
53 (* UNEXPORTED
54 Transparent cg_crr.
55 *)
56
57 (* UNEXPORTED
58 Transparent cr_crr.
59 *)
60
61 (* UNEXPORTED
62 Transparent csf_fun.
63 *)
64
65 (* UNEXPORTED
66 Transparent csbf_fun.
67 *)
68
69 (* UNEXPORTED
70 Transparent csr_rel.
71 *)
72
73 (* UNEXPORTED
74 Transparent cs_eq.
75 *)
76
77 (* UNEXPORTED
78 Transparent cs_neq.
79 *)
80
81 (* UNEXPORTED
82 Transparent cs_ap.
83 *)
84
85 (* UNEXPORTED
86 Transparent cm_unit.
87 *)
88
89 (* UNEXPORTED
90 Transparent csg_op.
91 *)
92
93 (* UNEXPORTED
94 Transparent cg_inv.
95 *)
96
97 (* UNEXPORTED
98 Transparent cg_minus.
99 *)
100
101 (* UNEXPORTED
102 Transparent cr_one.
103 *)
104
105 (* UNEXPORTED
106 Transparent cr_mult.
107 *)
108
109 (* UNEXPORTED
110 Transparent nexp_op.
111 *)
112
113 (* Begin_SpecReals *)
114
115 (* FIELDS *)
116
117 (*#*
118 * Fields %\label{section:fields}%
119 ** Definition of the notion Field
120 *)
121
122 inline procedural "cic:/CoRN/algebra/CFields/is_CField.con" as definition.
123
124 inline procedural "cic:/CoRN/algebra/CFields/CField.ind".
125
126 (* COERCION
127 cic:/matita/CoRN-Procedural/algebra/CFields/cf_crr.con
128 *)
129
130 (* End_SpecReals *)
131
132 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl'.con" as definition.
133
134 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl.con" as definition.
135
136 (* UNEXPORTED
137 Implicit Arguments f_rcpcl [F].
138 *)
139
140 (*#*
141 [cf_div] is the division in a field. It is defined in terms of
142 multiplication and the reciprocal. [x[/]y] is only defined if
143 we have a proof of [y [#] Zero].
144 *)
145
146 inline procedural "cic:/CoRN/algebra/CFields/cf_div.con" as definition.
147
148 (* UNEXPORTED
149 Implicit Arguments cf_div [F].
150 *)
151
152 (* NOTATION
153 Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
154 *)
155
156 (*#*
157 %\begin{convention}\label{convention:div-form}%
158 - Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy].
159 - In lemmas, a hypothesis that [t [#] Zero] will be named [t_].
160 - We do not use [NonZeros], but write the condition [ [#] Zero] separately.
161 - In each lemma, we use only variables for proof objects, and these variables
162  are universally quantified.
163 For example, the informal lemma
164 $\frac{1}{x}\cdot\frac{1}{y} = \frac{1}{x\cdot y}$
165 #(1/x).(1/y) = 1/(x.y)# for all [x] and [y]is formalized as
166 [[
167 forall (x y : F) x_ y_ xy_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//]xy_
168 ]]
169 and not as
170 [[
171 forall (x y : F) x_ y_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//](prod_nz x y x_ y_)
172 ]]
173 We have made this choice to make it easier to apply lemmas; this can
174 be quite awkward if we would use the last formulation.
175 - So every division occurring in the formulation of a lemma is of the
176 form [e[/]e'[//]H] where [H] is a variable.  Only exceptions: we may
177 write [e[/] (Snring n)] and [e[/]TwoNZ], [e[/]ThreeNZ] and so on.
178 (Constants like [TwoNZ] will be defined later on.)
179
180 %\end{convention}%
181
182 ** Field axioms
183 %\begin{convention}% Let [F] be a field.
184 %\end{convention}%
185 *)
186
187 (* UNEXPORTED
188 Section Field_axioms
189 *)
190
191 (* UNEXPORTED
192 cic:/CoRN/algebra/CFields/Field_axioms/F.var
193 *)
194
195 inline procedural "cic:/CoRN/algebra/CFields/CField_is_CField.con" as lemma.
196
197 inline procedural "cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con" as lemma.
198
199 (* UNEXPORTED
200 End Field_axioms
201 *)
202
203 (* UNEXPORTED
204 Section Field_basics
205 *)
206
207 (*#* ** Field basics
208 %\begin{convention}% Let [F] be a field.
209 %\end{convention}%
210 *)
211
212 (* UNEXPORTED
213 cic:/CoRN/algebra/CFields/Field_basics/F.var
214 *)
215
216 inline procedural "cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con" as lemma.
217
218 inline procedural "cic:/CoRN/algebra/CFields/field_mult_inv.con" as lemma.
219
220 (* UNEXPORTED
221 Hint Resolve field_mult_inv: algebra.
222 *)
223
224 inline procedural "cic:/CoRN/algebra/CFields/field_mult_inv_op.con" as lemma.
225
226 (* UNEXPORTED
227 End Field_basics
228 *)
229
230 (* UNEXPORTED
231 Hint Resolve field_mult_inv field_mult_inv_op: algebra.
232 *)
233
234 (* UNEXPORTED
235 Section Field_multiplication
236 *)
237
238 (*#*
239 ** Properties of multiplication
240 %\begin{convention}% Let [F] be a field.
241 %\end{convention}%
242 *)
243
244 (* UNEXPORTED
245 cic:/CoRN/algebra/CFields/Field_multiplication/F.var
246 *)
247
248 inline procedural "cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con" as lemma.
249
250 inline procedural "cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con" as lemma.
251
252 inline procedural "cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con" as lemma.
253
254 inline procedural "cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con" as lemma.
255
256 inline procedural "cic:/CoRN/algebra/CFields/mult_resp_neq.con" as lemma.
257
258 inline procedural "cic:/CoRN/algebra/CFields/mult_eq_zero.con" as lemma.
259
260 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_lft.con" as lemma.
261
262 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_rht.con" as lemma.
263
264 inline procedural "cic:/CoRN/algebra/CFields/square_eq_aux.con" as lemma.
265
266 inline procedural "cic:/CoRN/algebra/CFields/square_eq_weak.con" as lemma.
267
268 inline procedural "cic:/CoRN/algebra/CFields/cond_square_eq.con" as lemma.
269
270 (* UNEXPORTED
271 End Field_multiplication
272 *)
273
274 (* UNEXPORTED
275 Section x_square
276 *)
277
278 inline procedural "cic:/CoRN/algebra/CFields/x_xminone.con" as lemma.
279
280 inline procedural "cic:/CoRN/algebra/CFields/square_id.con" as lemma.
281
282 (* UNEXPORTED
283 End x_square
284 *)
285
286 (* UNEXPORTED
287 Hint Resolve mult_resp_ap_zero: algebra.
288 *)
289
290 (* UNEXPORTED
291 Section Rcpcl_properties
292 *)
293
294 (*#*
295 ** Properties of reciprocal
296 %\begin{convention}% Let [F] be a field.
297 %\end{convention}%
298 *)
299
300 (* UNEXPORTED
301 cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var
302 *)
303
304 inline procedural "cic:/CoRN/algebra/CFields/inv_one.con" as lemma.
305
306 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_wd.con" as lemma.
307
308 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_mult.con" as lemma.
309
310 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con" as lemma.
311
312 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con" as lemma.
313
314 (* UNEXPORTED
315 End Rcpcl_properties
316 *)
317
318 (* UNEXPORTED
319 Section MultipGroup
320 *)
321
322 (*#*
323 ** The multiplicative group of nonzeros of a field.
324 %\begin{convention}% Let [F] be a field
325 %\end{convention}%
326 *)
327
328 (* UNEXPORTED
329 cic:/CoRN/algebra/CFields/MultipGroup/F.var
330 *)
331
332 (*#*
333 The multiplicative monoid of NonZeros.
334 *)
335
336 inline procedural "cic:/CoRN/algebra/CFields/NonZeroMonoid.con" as definition.
337
338 inline procedural "cic:/CoRN/algebra/CFields/fmg_cs_inv.con" as definition.
339
340 inline procedural "cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con" as lemma.
341
342 inline procedural "cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con" as lemma.
343
344 (* UNEXPORTED
345 End MultipGroup
346 *)
347
348 (* UNEXPORTED
349 Section Div_properties
350 *)
351
352 (*#*
353 ** Properties of division
354 %\begin{convention}% Let [F] be a field.
355 %\end{convention}%
356
357 %\begin{nameconvention}%
358 In the names of lemmas, we denote [[/]] by [div], and
359 [One[/]] by [recip].
360 %\end{nameconvention}%
361 *)
362
363 (* UNEXPORTED
364 cic:/CoRN/algebra/CFields/Div_properties/F.var
365 *)
366
367 inline procedural "cic:/CoRN/algebra/CFields/div_prop.con" as lemma.
368
369 inline procedural "cic:/CoRN/algebra/CFields/div_1.con" as lemma.
370
371 inline procedural "cic:/CoRN/algebra/CFields/div_1'.con" as lemma.
372
373 inline procedural "cic:/CoRN/algebra/CFields/div_1''.con" as lemma.
374
375 (* UNEXPORTED
376 Hint Resolve div_1: algebra.
377 *)
378
379 inline procedural "cic:/CoRN/algebra/CFields/x_div_x.con" as lemma.
380
381 (* UNEXPORTED
382 Hint Resolve x_div_x: algebra.
383 *)
384
385 inline procedural "cic:/CoRN/algebra/CFields/x_div_one.con" as lemma.
386
387 (*#*
388 The next lemma says $x\cdot\frac{y}{z} = \frac{x\cdot y}{z}$
389 #x.(y/z) = (x.y)/z#.
390 *)
391
392 inline procedural "cic:/CoRN/algebra/CFields/x_mult_y_div_z.con" as lemma.
393
394 (* UNEXPORTED
395 Hint Resolve x_mult_y_div_z: algebra.
396 *)
397
398 inline procedural "cic:/CoRN/algebra/CFields/div_wd.con" as lemma.
399
400 (* UNEXPORTED
401 Hint Resolve div_wd: algebra_c.
402 *)
403
404 (*#*
405 The next lemma says $\frac{\frac{x}{y}}{z} = \frac{x}{y\cdot z}$
406 #[(x/y)/z = x/(y.z)]#
407 *)
408
409 inline procedural "cic:/CoRN/algebra/CFields/div_div.con" as lemma.
410
411 inline procedural "cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con" as lemma.
412
413 inline procedural "cic:/CoRN/algebra/CFields/div_resp_ap_zero.con" as lemma.
414
415 (*#*
416 The next lemma says $\frac{x}{\frac{y}{z}} = \frac{x\cdot z}{y}$
417 #[x/(y/z) = (x.z)/y]#
418 *)
419
420 inline procedural "cic:/CoRN/algebra/CFields/div_div2.con" as lemma.
421
422 (*#*
423 The next lemma says $\frac{x\cdot p}{y\cdot q} = \frac{x}{y}\cdot \frac{p}{q}$
424 #[(x.p)/(y.q) = (x/y).(p/q)]#
425 *)
426
427 inline procedural "cic:/CoRN/algebra/CFields/mult_of_divs.con" as lemma.
428
429 inline procedural "cic:/CoRN/algebra/CFields/div_dist.con" as lemma.
430
431 inline procedural "cic:/CoRN/algebra/CFields/div_dist'.con" as lemma.
432
433 inline procedural "cic:/CoRN/algebra/CFields/div_semi_sym.con" as lemma.
434
435 (* UNEXPORTED
436 Hint Resolve div_semi_sym: algebra.
437 *)
438
439 inline procedural "cic:/CoRN/algebra/CFields/eq_div.con" as lemma.
440
441 inline procedural "cic:/CoRN/algebra/CFields/div_strext.con" as lemma.
442
443 (* UNEXPORTED
444 End Div_properties
445 *)
446
447 (* UNEXPORTED
448 Hint Resolve div_1 div_1' div_1'' div_wd x_div_x x_div_one div_div div_div2
449   mult_of_divs x_mult_y_div_z mult_of_divs div_dist div_dist' div_semi_sym
450   div_prop: algebra.
451 *)
452
453 (*#*
454 ** Cancellation laws for apartness and multiplication
455 %\begin{convention}% Let [F] be a field
456 %\end{convention}%
457 *)
458
459 (* UNEXPORTED
460 Section Mult_Cancel_Ap_Zero
461 *)
462
463 (* UNEXPORTED
464 cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var
465 *)
466
467 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con" as lemma.
468
469 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con" as lemma.
470
471 inline procedural "cic:/CoRN/algebra/CFields/recip_ap_zero.con" as lemma.
472
473 inline procedural "cic:/CoRN/algebra/CFields/recip_resp_ap.con" as lemma.
474
475 (* UNEXPORTED
476 End Mult_Cancel_Ap_Zero
477 *)
478
479 (* UNEXPORTED
480 Section CField_Ops
481 *)
482
483 (*#*
484 ** Functional Operations
485
486 We now move on to lifting these operations to functions.  As we are
487 dealing with %\emph{partial}% #<i>partial</i># functions, we don't
488 have to worry explicitly about the function by which we are dividing
489 being non-zero everywhere; this will simply be encoded in its domain.
490
491 %\begin{convention}%
492 Let [X] be a Field and [F,G:(PartFunct X)] have domains respectively
493 [P] and [Q].
494 %\end{convention}%
495 *)
496
497 (* UNEXPORTED
498 cic:/CoRN/algebra/CFields/CField_Ops/X.var
499 *)
500
501 (* UNEXPORTED
502 cic:/CoRN/algebra/CFields/CField_Ops/F.var
503 *)
504
505 (* UNEXPORTED
506 cic:/CoRN/algebra/CFields/CField_Ops/G.var
507 *)
508
509 (* begin hide *)
510
511 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/P.con" "CField_Ops__" as definition.
512
513 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Q.con" "CField_Ops__" as definition.
514
515 (* end hide *)
516
517 (* UNEXPORTED
518 Section Part_Function_Recip
519 *)
520
521 (*#*
522 Some auxiliary notions are helpful in defining the domain.
523 *)
524
525 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/R.con" "CField_Ops__Part_Function_Recip__" as definition.
526
527 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/Ext2R.con" "CField_Ops__Part_Function_Recip__" as definition.
528
529 inline procedural "cic:/CoRN/algebra/CFields/part_function_recip_strext.con" as lemma.
530
531 inline procedural "cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con" as lemma.
532
533 inline procedural "cic:/CoRN/algebra/CFields/Frecip.con" as definition.
534
535 (* UNEXPORTED
536 End Part_Function_Recip
537 *)
538
539 (* UNEXPORTED
540 Section Part_Function_Div
541 *)
542
543 (*#*
544 For division things work out almost in the same way.
545 *)
546
547 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/R.con" "CField_Ops__Part_Function_Div__" as definition.
548
549 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/Ext2R.con" "CField_Ops__Part_Function_Div__" as definition.
550
551 inline procedural "cic:/CoRN/algebra/CFields/part_function_div_strext.con" as lemma.
552
553 inline procedural "cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con" as lemma.
554
555 inline procedural "cic:/CoRN/algebra/CFields/Fdiv.con" as definition.
556
557 (* UNEXPORTED
558 End Part_Function_Div
559 *)
560
561 (*#*
562 %\begin{convention}% Let [R:X->CProp].
563 %\end{convention}%
564 *)
565
566 (* UNEXPORTED
567 cic:/CoRN/algebra/CFields/CField_Ops/R.var
568 *)
569
570 inline procedural "cic:/CoRN/algebra/CFields/included_FRecip.con" as lemma.
571
572 inline procedural "cic:/CoRN/algebra/CFields/included_FRecip'.con" as lemma.
573
574 inline procedural "cic:/CoRN/algebra/CFields/included_FDiv.con" as lemma.
575
576 inline procedural "cic:/CoRN/algebra/CFields/included_FDiv'.con" as lemma.
577
578 inline procedural "cic:/CoRN/algebra/CFields/included_FDiv''.con" as lemma.
579
580 (* UNEXPORTED
581 End CField_Ops
582 *)
583
584 (* UNEXPORTED
585 Implicit Arguments Frecip [X].
586 *)
587
588 (* NOTATION
589 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
590 *)
591
592 (* UNEXPORTED
593 Implicit Arguments Fdiv [X].
594 *)
595
596 (* NOTATION
597 Infix "{/}" := Fdiv (at level 41, no associativity).
598 *)
599
600 (* UNEXPORTED
601 Hint Resolve included_FRecip included_FDiv : included.
602 *)
603
604 (* UNEXPORTED
605 Hint Immediate included_FRecip' included_FDiv' included_FDiv'' : included.
606 *)
607