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