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% #&Dagger;# *)
  24
  25 (*#* printing {/} %\ensuremath{/}% #/# *)
  26
  27 (*#* printing {1/} %\ensuremath{\frac1\cdot}% #1/# *)
  28
  29 (*#* printing [/]?[//] %\ensuremath{/?\ddagger}% #/?&Dagger;# *)
  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