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