matita/matita/contribs/CoRN-Decl/CoRN.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/CoRN".
  18
  19 include "preamble.ma".
  20
  21 (* From algebra/Basics ****************************************************)
  22
  23 (* NOTATION
  24 Notation Pair := (pair (B:=_)).
  25 *)
  26
  27 (* NOTATION
  28 Notation Proj1 := (proj1 (B:=_)).
  29 *)
  30
  31 (* NOTATION
  32 Notation Proj2 := (proj2 (B:=_)).
  33 *)
  34
  35 coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *).
  36
  37 (* From algebra/CAbGroups *************************************************)
  38
  39 coercion cic:/CoRN/algebra/CAbGroups/cag_crr.con 0 (* compounds *).
  40
  41 (* From algebra/CAbMonoids ************************************************)
  42
  43 coercion cic:/CoRN/algebra/CAbMonoids/cam_crr.con 0 (* compounds *).
  44
  45 (* From algebra/CFields ***************************************************)
  46
  47 coercion cic:/CoRN/algebra/CFields/cf_crr.con 0 (* compounds *).
  48
  49 (* NOTATION
  50 Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
  51 *)
  52
  53 (* NOTATION
  54 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
  55 *)
  56
  57 (* NOTATION
  58 Infix "{/}" := Fdiv (at level 41, no associativity).
  59 *)
  60
  61 (* From algebra/CGroups ***************************************************)
  62
  63 coercion cic:/CoRN/algebra/CGroups/cg_crr.con 0 (* compounds *).
  64
  65 (* NOTATION
  66 Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
  67 *)
  68
  69 (* NOTATION
  70 Infix "[-]" := cg_minus (at level 50, left associativity).
  71 *)
  72
  73 (* NOTATION
  74 Notation "{--} x" := (Finv x) (at level 2, right associativity).
  75 *)
  76
  77 (* NOTATION
  78 Infix "{-}" := Fminus (at level 50, left associativity).
  79 *)
  80
  81 (* From algebra/CLogic ****************************************************)
  82
  83 (* NOTATION
  84 Infix "IFF" := Iff (at level 60, right associativity).
  85 *)
  86
  87 (* NOTATION
  88 Infix "or" := COr (at level 85, right associativity).
  89 *)
  90
  91 (* NOTATION
  92 Infix "and" := CAnd (at level 80, right associativity).
  93 *)
  94
  95 (* NOTATION
  96 Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
  97   (at level 0, x at level 99) : type_scope.
  98 *)
  99
 100 (* NOTATION
 101 Notation "{ x : A  |  P  |  Q }" :=
 102   (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
 103   type_scope.
 104 *)
 105
 106 (* NOTATION
 107 Notation ProjT1 := (proj1_sigT _ _).
 108 *)
 109
 110 (* NOTATION
 111 Notation ProjT2 := (proj2_sigT _ _).
 112 *)
 113
 114 (* From algebra/CMonoids **************************************************)
 115
 116 coercion cic:/CoRN/algebra/CMonoids/cm_crr.con 0 (* compounds *).
 117
 118 (* NOTATION
 119 Notation Zero := (cm_unit _).
 120 *)
 121
 122 (* From algebra/COrdAbs ***************************************************)
 123
 124 (* NOTATION
 125 Notation ZeroR := (Zero:R).
 126 *)
 127
 128 (* NOTATION
 129 Notation AbsBig := (absBig _).
 130 *)
 131
 132 (* From algebra/COrdCauchy ************************************************)
 133
 134 coercion cic:/CoRN/algebra/COrdCauchy/CS_seq.con 0 (* compounds *).
 135
 136 (* From algebra/COrdFields ************************************************)
 137
 138 coercion cic:/CoRN/algebra/COrdFields/cof_crr.con 0 (* compounds *).
 139
 140 (* NOTATION
 141 Infix "[<]" := cof_less (at level 70, no associativity).
 142 *)
 143
 144 (* NOTATION
 145 Infix "[>]" := greater (at level 70, no associativity).
 146 *)
 147
 148 (* NOTATION
 149 Infix "[<=]" := leEq (at level 70, no associativity).
 150 *)
 151
 152 (* NOTATION
 153 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
 154 *)
 155
 156 (* NOTATION
 157 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
 158 *)
 159
 160 (* NOTATION
 161 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
 162 *)
 163
 164 (* NOTATION
 165 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
 166 *)
 167
 168 (* NOTATION
 169 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
 170 *)
 171
 172 (* NOTATION
 173 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
 174 *)
 175
 176 (* NOTATION
 177 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
 178 *)
 179
 180 (* NOTATION
 181 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
 182 *)
 183
 184 (* NOTATION
 185 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
 186 *)
 187
 188 (* NOTATION
 189 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
 190 *)
 191
 192 (* NOTATION
 193 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
 194 *)
 195
 196 (* NOTATION
 197 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
 198 *)
 199
 200 (* From algebra/COrdFields2 ***********************************************)
 201
 202 (* NOTATION
 203 Notation ZeroR := (Zero:R).
 204 *)
 205
 206 (* NOTATION
 207 Notation OneR := (One:R).
 208 *)
 209
 210 (* From algebra/CPoly_ApZero **********************************************)
 211
 212 (* NOTATION
 213 Notation RX := (cpoly_cring R).
 214 *)
 215
 216 (* NOTATION
 217 Notation RX := (cpoly_cring R).
 218 *)
 219
 220 (* NOTATION
 221 Notation RX := (cpoly_cring R).
 222 *)
 223
 224 (* From algebra/CPoly_Degree **********************************************)
 225
 226 (* NOTATION
 227 Notation RX := (cpoly_cring R).
 228 *)
 229
 230 (* NOTATION
 231 Notation RX := (cpoly_cring R).
 232 *)
 233
 234 (* NOTATION
 235 Notation FX := (cpoly_cring F).
 236 *)
 237
 238 (* From algebra/CPoly_NthCoeff ********************************************)
 239
 240 (* NOTATION
 241 Notation RX := (cpoly_cring R).
 242 *)
 243
 244 (* NOTATION
 245 Notation RX := (cpoly_cring R).
 246 *)
 247
 248 (* From algebra/CPolynomials **********************************************)
 249
 250 (* NOTATION
 251 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
 252 *)
 253
 254 (* NOTATION
 255 Notation RX := (cpoly_cring CR).
 256 *)
 257
 258 (* NOTATION
 259 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
 260 *)
 261
 262 (* NOTATION
 263 Notation RX := (cpoly_cring R).
 264 *)
 265
 266 (* NOTATION
 267 Notation Cpoly := (cpoly CR).
 268 *)
 269
 270 (* NOTATION
 271 Notation Cpoly_zero := (cpoly_zero CR).
 272 *)
 273
 274 (* NOTATION
 275 Notation Cpoly_linear := (cpoly_linear CR).
 276 *)
 277
 278 (* NOTATION
 279 Notation Cpoly_cring := (cpoly_cring CR).
 280 *)
 281
 282 (* From algebra/CRings ****************************************************)
 283
 284 coercion cic:/CoRN/algebra/CRings/cr_crr.con 0 (* compounds *).
 285
 286 (* NOTATION
 287 Notation One := (cr_one _).
 288 *)
 289
 290 (* NOTATION
 291 Infix "[*]" := cr_mult (at level 40, left associativity).
 292 *)
 293
 294 (* NOTATION
 295 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
 296 *)
 297
 298 (* NOTATION
 299 Notation Two := (nring 2).
 300 *)
 301
 302 (* NOTATION
 303 Notation Three := (nring 3).
 304 *)
 305
 306 (* NOTATION
 307 Notation Four := (nring 4).
 308 *)
 309
 310 (* NOTATION
 311 Notation Six := (nring 6).
 312 *)
 313
 314 (* NOTATION
 315 Notation Eight := (nring 8).
 316 *)
 317
 318 (* NOTATION
 319 Notation Twelve := (nring 12).
 320 *)
 321
 322 (* NOTATION
 323 Notation Sixteen := (nring 16).
 324 *)
 325
 326 (* NOTATION
 327 Notation Nine := (nring 9).
 328 *)
 329
 330 (* NOTATION
 331 Notation Eighteen := (nring 18).
 332 *)
 333
 334 (* NOTATION
 335 Notation TwentyFour := (nring 24).
 336 *)
 337
 338 (* NOTATION
 339 Notation FortyEight := (nring 48).
 340 *)
 341
 342 (* NOTATION
 343 Infix "{*}" := Fmult (at level 40, left associativity).
 344 *)
 345
 346 (* NOTATION
 347 Infix "{**}" := Fscalmult (at level 40, left associativity).
 348 *)
 349
 350 (* NOTATION
 351 Infix "{^}" := Fnth (at level 30, right associativity).
 352 *)
 353
 354 (* From algebra/CSemiGroups ***********************************************)
 355
 356 coercion cic:/CoRN/algebra/CSemiGroups/csg_crr.con 0 (* compounds *).
 357
 358 (* NOTATION
 359 Infix "[+]" := csg_op (at level 50, left associativity).
 360 *)
 361
 362 (* NOTATION
 363 Infix "{+}" := Fplus (at level 50, left associativity).
 364 *)
 365
 366 (* From algebra/CSetoidFun ************************************************)
 367
 368 (* NOTATION
 369 Notation Conj := (conjP _).
 370 *)
 371
 372 coercion cic:/CoRN/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *).
 373
 374 (* NOTATION
 375 Notation BDom := (bpfdom _ _).
 376 *)
 377
 378 coercion cic:/CoRN/algebra/CSetoidFun/pfpfun.con 0 (* compounds *).
 379
 380 (* NOTATION
 381 Notation Dom := (pfdom _).
 382 *)
 383
 384 (* NOTATION
 385 Notation Part := (pfpfun _).
 386 *)
 387
 388 (* NOTATION
 389 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
 390 *)
 391
 392 (* NOTATION
 393 Notation FId := (Fid _).
 394 *)
 395
 396 (* NOTATION
 397 Infix "[o]" := Fcomp (at level 65, no associativity).
 398 *)
 399
 400 (* NOTATION
 401 Notation Prj1 := (prj1 _ _ _ _).
 402 *)
 403
 404 (* NOTATION
 405 Notation Prj2 := (prj2 _ _ _ _).
 406 *)
 407
 408 (* From algebra/CSetoids **************************************************)
 409
 410 coercion cic:/CoRN/algebra/CSetoids/cs_crr.con 0 (* compounds *).
 411
 412 (* NOTATION
 413 Infix "[=]" := cs_eq (at level 70, no associativity).
 414 *)
 415
 416 (* NOTATION
 417 Infix "[#]" := cs_ap (at level 70, no associativity).
 418 *)
 419
 420 (* NOTATION
 421 Infix "[~=]" := cs_neq (at level 70, no associativity).
 422 *)
 423
 424 coercion cic:/CoRN/algebra/CSetoids/csp_pred.con 0 (* compounds *).
 425
 426 coercion cic:/CoRN/algebra/CSetoids/csp'_pred.con 0 (* compounds *).
 427
 428 coercion cic:/CoRN/algebra/CSetoids/csr_rel.con 0 (* compounds *).
 429
 430 coercion cic:/CoRN/algebra/CSetoids/Ccsr_rel.con 0 (* compounds *).
 431
 432 coercion cic:/CoRN/algebra/CSetoids/csf_fun.con 0 (* compounds *).
 433
 434 coercion cic:/CoRN/algebra/CSetoids/csbf_fun.con 0 (* compounds *).
 435
 436 coercion cic:/CoRN/algebra/CSetoids/un_op_fun.con 0 (* compounds *).
 437
 438 coercion cic:/CoRN/algebra/CSetoids/bin_op_bin_fun.con 0 (* compounds *).
 439
 440 coercion cic:/CoRN/algebra/CSetoids/outer_op_bin_fun.con 0 (* compounds *).
 441
 442 coercion cic:/CoRN/algebra/CSetoids/scs_elem.con 0 (* compounds *).
 443
 444 (* From algebra/CVectorSpace **********************************************)
 445
 446 coercion cic:/CoRN/algebra/CVectorSpace/vs_vs.con 0 (* compounds *).
 447
 448 (* NOTATION
 449 Infix "[']" := vs_op (at level 30, no associativity).
 450 *)
 451
 452 (* From algebra/Expon *****************************************************)
 453
 454 (* NOTATION
 455 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
 456 *)
 457
 458 (* From complex/CComplex **************************************************)
 459
 460 (* NOTATION
 461 Notation CCX := (cpoly_cring CC).
 462 *)
 463
 464 (* NOTATION
 465 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
 466 *)
 467
 468 (* From fta/CC_Props ******************************************************)
 469
 470 coercion cic:/CoRN/fta/CC_Props/CC_seq.con 0 (* compounds *).
 471
 472 (* From fta/FTAreg ********************************************************)
 473
 474 coercion cic:/CoRN/fta/FTAreg/z_el.con 0 (* compounds *).
 475
 476 coercion cic:/CoRN/fta/FTAreg/Kntup.con 0 (* compounds *).
 477
 478 (* From ftc/FTC ***********************************************************)
 479
 480 (* NOTATION
 481 Notation "[-S-] F" := (Fprim F) (at level 20).
 482 *)
 483
 484 (* From ftc/Integral ******************************************************)
 485
 486 (* NOTATION
 487 Notation Integral := (integral _ _ Hab).
 488 *)
 489
 490 (* From ftc/MoreIntervals *************************************************)
 491
 492 coercion cic:/CoRN/ftc/MoreIntervals/iprop.con 0 (* compounds *).
 493
 494 (* From ftc/Partitions ****************************************************)
 495
 496 coercion cic:/CoRN/ftc/Partitions/Pts.con 0 (* compounds *).
 497
 498 (* From ftc/RefLemma ******************************************************)
 499
 500 (* NOTATION
 501 Notation g := RL_g.
 502 *)
 503
 504 (* NOTATION
 505 Notation h := RL_h.
 506 *)
 507
 508 (* NOTATION
 509 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
 510 *)
 511
 512 (* NOTATION
 513 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
 514 *)
 515
 516 (* NOTATION
 517 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
 518 *)
 519
 520 (* From ftc/RefSeparated **************************************************)
 521
 522 (* NOTATION
 523 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
 524 *)
 525
 526 (* NOTATION
 527 Notation just2 :=
 528   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
 529 *)
 530
 531 (* From ftc/RefSeparating *************************************************)
 532
 533 (* NOTATION
 534 Notation m := RS'_m.
 535 *)
 536
 537 (* NOTATION
 538 Notation h := RS'_h.
 539 *)
 540
 541 (* NOTATION
 542 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
 543 *)
 544
 545 (* NOTATION
 546 Notation just2 :=
 547   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
 548 *)
 549
 550 (* From ftc/Rolle *********************************************************)
 551
 552 (* NOTATION
 553 Notation cp := (compact_part a b Hab' d Hd).
 554 *)
 555
 556 (* From ftc/TaylorLemma ***************************************************)
 557
 558 (* NOTATION
 559 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
 560 *)
 561
 562 (* NOTATION
 563 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
 564 *)
 565
 566 (* From ftc/WeakIVT *******************************************************)
 567
 568 (* NOTATION
 569 Infix "**" := prodT (at level 20).
 570 *)
 571
 572 (* From metrics/CMetricSpaces *********************************************)
 573
 574 coercion cic:/CoRN/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
 575
 576 (* From metrics/CPseudoMSpaces ********************************************)
 577
 578 coercion cic:/CoRN/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *).
 579
 580 (* NOTATION
 581 Infix "[-d]" := cms_d (at level 68, left associativity).
 582 *)
 583
 584 (* From model/structures/Nsec *********************************************)
 585
 586 (* NOTATION
 587 Infix "{#N}" := ap_nat (no associativity, at level 90).
 588 *)
 589
 590 (* From model/structures/Qsec *********************************************)
 591
 592 (* NOTATION
 593 Infix "{=Q}" := Qeq (no associativity, at level 90).
 594 *)
 595
 596 (* NOTATION
 597 Infix "{#Q}" := Qap (no associativity, at level 90).
 598 *)
 599
 600 (* NOTATION
 601 Infix "{<Q}" := Qlt (no associativity, at level 90).
 602 *)
 603
 604 (* NOTATION
 605 Infix "{+Q}" := Qplus (no associativity, at level 85).
 606 *)
 607
 608 (* NOTATION
 609 Infix "{*Q}" := Qmult (no associativity, at level 80).
 610 *)
 611
 612 (* NOTATION
 613 Notation "{-Q}" := Qopp (at level 1, left associativity).
 614 *)
 615
 616 coercion cic:/CoRN/model/structures/Qsec/inject_Z.con 0 (* compounds *).
 617
 618 (* From model/structures/Zsec *********************************************)
 619
 620 (* NOTATION
 621 Infix "{#Z}" := ap_Z (no associativity, at level 90).
 622 *)
 623
 624 coercion cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) 0 (* compounds *).
 625
 626 (* From reals/Bridges_LUB *************************************************)
 627
 628 (* NOTATION
 629 Notation "( p , q )" := (pairT p q).
 630 *)
 631
 632 (* From reals/CMetricFields ***********************************************)
 633
 634 coercion cic:/CoRN/reals/CMetricFields/cmf_crr.con 0 (* compounds *).
 635
 636 (* NOTATION
 637 Notation MAbs := (cmf_abs _).
 638 *)
 639
 640 coercion cic:/CoRN/reals/CMetricFields/MCS_seq.con 0 (* compounds *).
 641
 642 (* From reals/CReals ******************************************************)
 643
 644 coercion cic:/CoRN/reals/CReals/crl_crr.con 0 (* compounds *).
 645
 646 (* From reals/CauchySeq ***************************************************)
 647
 648 (* NOTATION
 649 Notation PartIR := (PartFunct IR).
 650 *)
 651
 652 (* NOTATION
 653 Notation ProjIR1 := (prj1 IR _ _ _).
 654 *)
 655
 656 (* NOTATION
 657 Notation ProjIR2 := (prj2 IR _ _ _).
 658 *)
 659
 660 (* NOTATION
 661 Notation ZeroR := (Zero:IR).
 662 *)
 663
 664 (* NOTATION
 665 Notation OneR := (One:IR).
 666 *)
 667
 668 (* From reals/Cauchy_CReals ***********************************************)
 669
 670 (* NOTATION
 671 Notation "'R_COrdField''" := (R_COrdField F).
 672 *)
 673
 674 (* From reals/Intervals ***************************************************)
 675
 676 (* NOTATION
 677 Notation Compact := (compact _ _).
 678 *)
 679
 680 (* NOTATION
 681 Notation FRestr := (Frestr (compact_wd _ _ _)).
 682 *)
 683
 684 (* From reals/Q_dense *****************************************************)
 685
 686 coercion cic:/CoRN/reals/Q_dense/pair_crr.con 0 (* compounds *).
 687
 688 (* NOTATION
 689 Notation "( A , B )" := (pairT A B).
 690 *)
 691
 692 (* From reals/Q_in_CReals *************************************************)
 693
 694 coercion cic:/Coq/NArith/BinPos/nat_of_P.con 0 (* compounds *).
 695
 696 (* From reals/R_morphism **************************************************)
 697
 698 coercion cic:/CoRN/reals/R_morphism/map.con 0 (* compounds *).
 699
 700 (* From tactics/FieldReflection *******************************************)
 701
 702 (* NOTATION
 703 Notation II := (interpF F val unop binop pfun).
 704 *)
 705
 706 (* From tactics/GroupReflection *******************************************)
 707
 708 (* NOTATION
 709 Notation II := (interpG G val unop binop pfun).
 710 *)
 711
 712 (* From tactics/RingReflection ********************************************)
 713
 714 (* NOTATION
 715 Notation II := (interpR R val unop binop pfun).
 716 *)
 717
 718 (* From transc/RealPowers *************************************************)
 719
 720 (* NOTATION
 721 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
 722 *)
 723
 724 (* NOTATION
 725 Notation "F {!} G" := (FPower F G) (at level 20).
 726 *)
 727
 728 (* From devel/loeb/per/lst2fun ********************************************)
 729
 730 coercion cic:/CoRN/devel/loeb/per/lst2fun/F_crr.con 0 (* compounds *).
 731
 732 coercion cic:/CoRN/devel/loeb/per/lst2fun/to_nat.con 0 (* compounds *).
 733