helm/software/matita/contribs/CoRN-Procedural/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".
 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".
 133
 134 inline procedural "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 procedural "cic:/CoRN/algebra/CFields/cf_div.con".
 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 alias id "F" = "cic:/CoRN/algebra/CFields/Field_axioms/F.var".
 192
 193 inline procedural "cic:/CoRN/algebra/CFields/CField_is_CField.con".
 194
 195 inline procedural "cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con".
 196
 197 (* UNEXPORTED
 198 End Field_axioms
 199 *)
 200
 201 (* UNEXPORTED
 202 Section Field_basics
 203 *)
 204
 205 (*#* ** Field basics
 206 %\begin{convention}% Let [F] be a field.
 207 %\end{convention}%
 208 *)
 209
 210 alias id "F" = "cic:/CoRN/algebra/CFields/Field_basics/F.var".
 211
 212 inline procedural "cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con".
 213
 214 inline procedural "cic:/CoRN/algebra/CFields/field_mult_inv.con".
 215
 216 (* UNEXPORTED
 217 Hint Resolve field_mult_inv: algebra.
 218 *)
 219
 220 inline procedural "cic:/CoRN/algebra/CFields/field_mult_inv_op.con".
 221
 222 (* UNEXPORTED
 223 End Field_basics
 224 *)
 225
 226 (* UNEXPORTED
 227 Hint Resolve field_mult_inv field_mult_inv_op: algebra.
 228 *)
 229
 230 (* UNEXPORTED
 231 Section Field_multiplication
 232 *)
 233
 234 (*#*
 235 ** Properties of multiplication
 236 %\begin{convention}% Let [F] be a field.
 237 %\end{convention}%
 238 *)
 239
 240 alias id "F" = "cic:/CoRN/algebra/CFields/Field_multiplication/F.var".
 241
 242 inline procedural "cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con".
 243
 244 inline procedural "cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con".
 245
 246 inline procedural "cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con".
 247
 248 inline procedural "cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con".
 249
 250 inline procedural "cic:/CoRN/algebra/CFields/mult_resp_neq.con".
 251
 252 inline procedural "cic:/CoRN/algebra/CFields/mult_eq_zero.con".
 253
 254 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_lft.con".
 255
 256 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_rht.con".
 257
 258 inline procedural "cic:/CoRN/algebra/CFields/square_eq_aux.con".
 259
 260 inline procedural "cic:/CoRN/algebra/CFields/square_eq_weak.con".
 261
 262 inline procedural "cic:/CoRN/algebra/CFields/cond_square_eq.con".
 263
 264 (* UNEXPORTED
 265 End Field_multiplication
 266 *)
 267
 268 (* UNEXPORTED
 269 Section x_square
 270 *)
 271
 272 inline procedural "cic:/CoRN/algebra/CFields/x_xminone.con".
 273
 274 inline procedural "cic:/CoRN/algebra/CFields/square_id.con".
 275
 276 (* UNEXPORTED
 277 End x_square
 278 *)
 279
 280 (* UNEXPORTED
 281 Hint Resolve mult_resp_ap_zero: algebra.
 282 *)
 283
 284 (* UNEXPORTED
 285 Section Rcpcl_properties
 286 *)
 287
 288 (*#*
 289 ** Properties of reciprocal
 290 %\begin{convention}% Let [F] be a field.
 291 %\end{convention}%
 292 *)
 293
 294 alias id "F" = "cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var".
 295
 296 inline procedural "cic:/CoRN/algebra/CFields/inv_one.con".
 297
 298 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_wd.con".
 299
 300 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_mult.con".
 301
 302 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con".
 303
 304 inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con".
 305
 306 (* UNEXPORTED
 307 End Rcpcl_properties
 308 *)
 309
 310 (* UNEXPORTED
 311 Section MultipGroup
 312 *)
 313
 314 (*#*
 315 ** The multiplicative group of nonzeros of a field.
 316 %\begin{convention}% Let [F] be a field
 317 %\end{convention}%
 318 *)
 319
 320 alias id "F" = "cic:/CoRN/algebra/CFields/MultipGroup/F.var".
 321
 322 (*#*
 323 The multiplicative monoid of NonZeros.
 324 *)
 325
 326 inline procedural "cic:/CoRN/algebra/CFields/NonZeroMonoid.con".
 327
 328 inline procedural "cic:/CoRN/algebra/CFields/fmg_cs_inv.con".
 329
 330 inline procedural "cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con".
 331
 332 inline procedural "cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con".
 333
 334 (* UNEXPORTED
 335 End MultipGroup
 336 *)
 337
 338 (* UNEXPORTED
 339 Section Div_properties
 340 *)
 341
 342 (*#*
 343 ** Properties of division
 344 %\begin{convention}% Let [F] be a field.
 345 %\end{convention}%
 346
 347 %\begin{nameconvention}%
 348 In the names of lemmas, we denote [[/]] by [div], and
 349 [One[/]] by [recip].
 350 %\end{nameconvention}%
 351 *)
 352
 353 alias id "F" = "cic:/CoRN/algebra/CFields/Div_properties/F.var".
 354
 355 inline procedural "cic:/CoRN/algebra/CFields/div_prop.con".
 356
 357 inline procedural "cic:/CoRN/algebra/CFields/div_1.con".
 358
 359 inline procedural "cic:/CoRN/algebra/CFields/div_1'.con".
 360
 361 inline procedural "cic:/CoRN/algebra/CFields/div_1''.con".
 362
 363 (* UNEXPORTED
 364 Hint Resolve div_1: algebra.
 365 *)
 366
 367 inline procedural "cic:/CoRN/algebra/CFields/x_div_x.con".
 368
 369 (* UNEXPORTED
 370 Hint Resolve x_div_x: algebra.
 371 *)
 372
 373 inline procedural "cic:/CoRN/algebra/CFields/x_div_one.con".
 374
 375 (*#*
 376 The next lemma says $x\cdot\frac{y}{z} = \frac{x\cdot y}{z}$
 377 #x.(y/z) = (x.y)/z#.
 378 *)
 379
 380 inline procedural "cic:/CoRN/algebra/CFields/x_mult_y_div_z.con".
 381
 382 (* UNEXPORTED
 383 Hint Resolve x_mult_y_div_z: algebra.
 384 *)
 385
 386 inline procedural "cic:/CoRN/algebra/CFields/div_wd.con".
 387
 388 (* UNEXPORTED
 389 Hint Resolve div_wd: algebra_c.
 390 *)
 391
 392 (*#*
 393 The next lemma says $\frac{\frac{x}{y}}{z} = \frac{x}{y\cdot z}$
 394 #[(x/y)/z = x/(y.z)]#
 395 *)
 396
 397 inline procedural "cic:/CoRN/algebra/CFields/div_div.con".
 398
 399 inline procedural "cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con".
 400
 401 inline procedural "cic:/CoRN/algebra/CFields/div_resp_ap_zero.con".
 402
 403 (*#*
 404 The next lemma says $\frac{x}{\frac{y}{z}} = \frac{x\cdot z}{y}$
 405 #[x/(y/z) = (x.z)/y]#
 406 *)
 407
 408 inline procedural "cic:/CoRN/algebra/CFields/div_div2.con".
 409
 410 (*#*
 411 The next lemma says $\frac{x\cdot p}{y\cdot q} = \frac{x}{y}\cdot \frac{p}{q}$
 412 #[(x.p)/(y.q) = (x/y).(p/q)]#
 413 *)
 414
 415 inline procedural "cic:/CoRN/algebra/CFields/mult_of_divs.con".
 416
 417 inline procedural "cic:/CoRN/algebra/CFields/div_dist.con".
 418
 419 inline procedural "cic:/CoRN/algebra/CFields/div_dist'.con".
 420
 421 inline procedural "cic:/CoRN/algebra/CFields/div_semi_sym.con".
 422
 423 (* UNEXPORTED
 424 Hint Resolve div_semi_sym: algebra.
 425 *)
 426
 427 inline procedural "cic:/CoRN/algebra/CFields/eq_div.con".
 428
 429 inline procedural "cic:/CoRN/algebra/CFields/div_strext.con".
 430
 431 (* UNEXPORTED
 432 End Div_properties
 433 *)
 434
 435 (* UNEXPORTED
 436 Hint Resolve div_1 div_1' div_1'' div_wd x_div_x x_div_one div_div div_div2
 437   mult_of_divs x_mult_y_div_z mult_of_divs div_dist div_dist' div_semi_sym
 438   div_prop: algebra.
 439 *)
 440
 441 (*#*
 442 ** Cancellation laws for apartness and multiplication
 443 %\begin{convention}% Let [F] be a field
 444 %\end{convention}%
 445 *)
 446
 447 (* UNEXPORTED
 448 Section Mult_Cancel_Ap_Zero
 449 *)
 450
 451 alias id "F" = "cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var".
 452
 453 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con".
 454
 455 inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con".
 456
 457 inline procedural "cic:/CoRN/algebra/CFields/recip_ap_zero.con".
 458
 459 inline procedural "cic:/CoRN/algebra/CFields/recip_resp_ap.con".
 460
 461 (* UNEXPORTED
 462 End Mult_Cancel_Ap_Zero
 463 *)
 464
 465 (* UNEXPORTED
 466 Section CField_Ops
 467 *)
 468
 469 (*#*
 470 ** Functional Operations
 471
 472 We now move on to lifting these operations to functions.  As we are
 473 dealing with %\emph{partial}% #<i>partial</i># functions, we don't
 474 have to worry explicitly about the function by which we are dividing
 475 being non-zero everywhere; this will simply be encoded in its domain.
 476
 477 %\begin{convention}%
 478 Let [X] be a Field and [F,G:(PartFunct X)] have domains respectively
 479 [P] and [Q].
 480 %\end{convention}%
 481 *)
 482
 483 alias id "X" = "cic:/CoRN/algebra/CFields/CField_Ops/X.var".
 484
 485 alias id "F" = "cic:/CoRN/algebra/CFields/CField_Ops/F.var".
 486
 487 alias id "G" = "cic:/CoRN/algebra/CFields/CField_Ops/G.var".
 488
 489 (* begin hide *)
 490
 491 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/P.con" "CField_Ops__".
 492
 493 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Q.con" "CField_Ops__".
 494
 495 (* end hide *)
 496
 497 (* UNEXPORTED
 498 Section Part_Function_Recip
 499 *)
 500
 501 (*#*
 502 Some auxiliary notions are helpful in defining the domain.
 503 *)
 504
 505 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/R.con" "CField_Ops__Part_Function_Recip__".
 506
 507 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/Ext2R.con" "CField_Ops__Part_Function_Recip__".
 508
 509 inline procedural "cic:/CoRN/algebra/CFields/part_function_recip_strext.con".
 510
 511 inline procedural "cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con".
 512
 513 inline procedural "cic:/CoRN/algebra/CFields/Frecip.con".
 514
 515 (* UNEXPORTED
 516 End Part_Function_Recip
 517 *)
 518
 519 (* UNEXPORTED
 520 Section Part_Function_Div
 521 *)
 522
 523 (*#*
 524 For division things work out almost in the same way.
 525 *)
 526
 527 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/R.con" "CField_Ops__Part_Function_Div__".
 528
 529 inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/Ext2R.con" "CField_Ops__Part_Function_Div__".
 530
 531 inline procedural "cic:/CoRN/algebra/CFields/part_function_div_strext.con".
 532
 533 inline procedural "cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con".
 534
 535 inline procedural "cic:/CoRN/algebra/CFields/Fdiv.con".
 536
 537 (* UNEXPORTED
 538 End Part_Function_Div
 539 *)
 540
 541 (*#*
 542 %\begin{convention}% Let [R:X->CProp].
 543 %\end{convention}%
 544 *)
 545
 546 alias id "R" = "cic:/CoRN/algebra/CFields/CField_Ops/R.var".
 547
 548 inline procedural "cic:/CoRN/algebra/CFields/included_FRecip.con".
 549
 550 inline procedural "cic:/CoRN/algebra/CFields/included_FRecip'.con".
 551
 552 inline procedural "cic:/CoRN/algebra/CFields/included_FDiv.con".
 553
 554 inline procedural "cic:/CoRN/algebra/CFields/included_FDiv'.con".
 555
 556 inline procedural "cic:/CoRN/algebra/CFields/included_FDiv''.con".
 557
 558 (* UNEXPORTED
 559 End CField_Ops
 560 *)
 561
 562 (* UNEXPORTED
 563 Implicit Arguments Frecip [X].
 564 *)
 565
 566 (* NOTATION
 567 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
 568 *)
 569
 570 (* UNEXPORTED
 571 Implicit Arguments Fdiv [X].
 572 *)
 573
 574 (* NOTATION
 575 Infix "{/}" := Fdiv (at level 41, no associativity).
 576 *)
 577
 578 (* UNEXPORTED
 579 Hint Resolve included_FRecip included_FDiv : included.
 580 *)
 581
 582 (* UNEXPORTED
 583 Hint Immediate included_FRecip' included_FDiv' included_FDiv'' : included.
 584 *)
 585