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