matitaB/matita/contribs/procedural/Coq/Coq.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 Arith/Compare *****************************************************)
  20
  21 (* NOTATION
  22 Notation not_eq_sym := sym_not_eq.
  23 *)
  24
  25 (* From Bool/Bool *********************************************************)
  26
  27 (* NOTATION
  28 Infix "||" := orb (at level 50, left associativity) : bool_scope.
  29 *)
  30
  31 (* NOTATION
  32 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
  33 *)
  34
  35 (* From Init/Datatypes ****************************************************)
  36
  37 (* NOTATION
  38 Add Printing If bool.
  39 *)
  40
  41 (* NOTATION
  42 Notation "x + y" := (sum x y) : type_scope.
  43 *)
  44
  45 (* NOTATION
  46 Add Printing Let prod.
  47 *)
  48
  49 (* NOTATION
  50 Notation "x * y" := (prod x y) : type_scope.
  51 *)
  52
  53 (* NOTATION
  54 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
  55 *)
  56
  57 (* From Init/Logic ********************************************************)
  58
  59 (* NOTATION
  60 Notation "~ x" := (not x) : type_scope.
  61 *)
  62
  63 (* NOTATION
  64 Notation "A <-> B" := (iff A B) : type_scope.
  65 *)
  66
  67 (* NOTATION
  68 Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
  69   (at level 200) : type_scope.
  70 *)
  71
  72 (* NOTATION
  73 Notation "'exists' x , p" := (ex (fun x => p))
  74   (at level 200, x ident) : type_scope.
  75 *)
  76
  77 (* NOTATION
  78 Notation "'exists' x : t , p" := (ex (fun x:t => p))
  79   (at level 200, x ident, format "'exists'  '/  ' x  :  t ,  '/  ' p")
  80   : type_scope.
  81 *)
  82
  83 (* NOTATION
  84 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
  85   (at level 200, x ident, p at level 200) : type_scope.
  86 *)
  87
  88 (* NOTATION
  89 Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
  90   (at level 200, x ident, t at level 200, p at level 200,
  91    format "'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']'")
  92   : type_scope.
  93 *)
  94
  95 (* NOTATION
  96 Notation "x = y" := (x = y :>_) : type_scope.
  97 *)
  98
  99 (* NOTATION
 100 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 101 *)
 102
 103 (* NOTATION
 104 Notation "x <> y" := (x <> y :>_) : type_scope.
 105 *)
 106
 107 (* From Init/Notations ****************************************************)
 108
 109 (* NOTATION
 110 Reserved Notation "x <-> y" (at level 95, no associativity).
 111 *)
 112
 113 (* NOTATION
 114 Reserved Notation "x /\ y" (at level 80, right associativity).
 115 *)
 116
 117 (* NOTATION
 118 Reserved Notation "x \/ y" (at level 85, right associativity).
 119 *)
 120
 121 (* NOTATION
 122 Reserved Notation "~ x" (at level 75, right associativity).
 123 *)
 124
 125 (* NOTATION
 126 Reserved Notation "x = y  :> T"
 127 (at level 70, y at next level, no associativity).
 128 *)
 129
 130 (* NOTATION
 131 Reserved Notation "x = y" (at level 70, no associativity).
 132 *)
 133
 134 (* NOTATION
 135 Reserved Notation "x = y = z"
 136 (at level 70, no associativity, y at next level).
 137 *)
 138
 139 (* NOTATION
 140 Reserved Notation "x <> y  :> T"
 141 (at level 70, y at next level, no associativity).
 142 *)
 143
 144 (* NOTATION
 145 Reserved Notation "x <> y" (at level 70, no associativity).
 146 *)
 147
 148 (* NOTATION
 149 Reserved Notation "x <= y" (at level 70, no associativity).
 150 *)
 151
 152 (* NOTATION
 153 Reserved Notation "x < y" (at level 70, no associativity).
 154 *)
 155
 156 (* NOTATION
 157 Reserved Notation "x >= y" (at level 70, no associativity).
 158 *)
 159
 160 (* NOTATION
 161 Reserved Notation "x > y" (at level 70, no associativity).
 162 *)
 163
 164 (* NOTATION
 165 Reserved Notation "x <= y <= z" (at level 70, y at next level).
 166 *)
 167
 168 (* NOTATION
 169 Reserved Notation "x <= y < z" (at level 70, y at next level).
 170 *)
 171
 172 (* NOTATION
 173 Reserved Notation "x < y < z" (at level 70, y at next level).
 174 *)
 175
 176 (* NOTATION
 177 Reserved Notation "x < y <= z" (at level 70, y at next level).
 178 *)
 179
 180 (* NOTATION
 181 Reserved Notation "x + y" (at level 50, left associativity).
 182 *)
 183
 184 (* NOTATION
 185 Reserved Notation "x - y" (at level 50, left associativity).
 186 *)
 187
 188 (* NOTATION
 189 Reserved Notation "x * y" (at level 40, left associativity).
 190 *)
 191
 192 (* NOTATION
 193 Reserved Notation "x / y" (at level 40, left associativity).
 194 *)
 195
 196 (* NOTATION
 197 Reserved Notation "- x" (at level 35, right associativity).
 198 *)
 199
 200 (* NOTATION
 201 Reserved Notation "/ x" (at level 35, right associativity).
 202 *)
 203
 204 (* NOTATION
 205 Reserved Notation "x ^ y" (at level 30, right associativity).
 206 *)
 207
 208 (* NOTATION
 209 Reserved Notation "( x , y , .. , z )" (at level 0).
 210 *)
 211
 212 (* NOTATION
 213 Reserved Notation "{ x }" (at level 0, x at level 99).
 214 *)
 215
 216 (* NOTATION
 217 Reserved Notation "{ A } + { B }" (at level 50, left associativity).
 218 *)
 219
 220 (* NOTATION
 221 Reserved Notation "A + { B }" (at level 50, left associativity).
 222 *)
 223
 224 (* NOTATION
 225 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
 226 *)
 227
 228 (* NOTATION
 229 Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
 230 *)
 231
 232 (* NOTATION
 233 Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
 234 *)
 235
 236 (* NOTATION
 237 Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
 238 *)
 239
 240 (* From Init/Peano ********************************************************)
 241
 242 (* NOTATION
 243 Infix "+" := plus : nat_scope.
 244 *)
 245
 246 (* NOTATION
 247 Infix "*" := mult : nat_scope.
 248 *)
 249
 250 (* NOTATION
 251 Infix "-" := minus : nat_scope.
 252 *)
 253
 254 (* NOTATION
 255 Infix "<=" := le : nat_scope.
 256 *)
 257
 258 (* NOTATION
 259 Infix "<" := lt : nat_scope.
 260 *)
 261
 262 (* NOTATION
 263 Infix ">=" := ge : nat_scope.
 264 *)
 265
 266 (* NOTATION
 267 Infix ">" := gt : nat_scope.
 268 *)
 269
 270 (* NOTATION
 271 Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
 272 *)
 273
 274 (* NOTATION
 275 Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 276 *)
 277
 278 (* NOTATION
 279 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 280 *)
 281
 282 (* NOTATION
 283 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 284 *)
 285
 286 (* From Init/Specif *******************************************************)
 287
 288 (* NOTATION
 289 Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
 290 *)
 291
 292 (* NOTATION
 293 Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
 294   type_scope.
 295 *)
 296
 297 (* NOTATION
 298 Notation "{ x : A  &  P }" := (sigS (fun x:A => P)) : type_scope.
 299 *)
 300
 301 (* NOTATION
 302 Notation "{ x : A  &  P  &  Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
 303   type_scope.
 304 *)
 305
 306 (* NOTATION
 307 Add Printing Let sig.
 308 *)
 309
 310 (* NOTATION
 311 Add Printing Let sig2.
 312 *)
 313
 314 (* NOTATION
 315 Add Printing Let sigS.
 316 *)
 317
 318 (* NOTATION
 319 Add Printing Let sigS2.
 320 *)
 321
 322 (* NOTATION
 323 Add Printing If sumbool.
 324 *)
 325
 326 (* NOTATION
 327 Add Printing If sumor.
 328 *)
 329
 330 (* From Lists/List ********************************************************)
 331
 332 (* NOTATION
 333 Infix "::" := cons (at level 60, right associativity) : list_scope.
 334 *)
 335
 336 (* NOTATION
 337 Infix "++" := app (right associativity, at level 60) : list_scope.
 338 *)
 339
 340 (* NOTATION
 341 Infix "::" := cons (at level 60, right associativity) : list_scope.
 342 *)
 343
 344 (* NOTATION
 345 Infix "++" := app (right associativity, at level 60) : list_scope.
 346 *)
 347
 348 (* From NArith/BinNat *****************************************************)
 349
 350 (* NOTATION
 351 Infix "+" := Nplus : N_scope.
 352 *)
 353
 354 (* NOTATION
 355 Infix "*" := Nmult : N_scope.
 356 *)
 357
 358 (* NOTATION
 359 Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
 360 *)
 361
 362 (* From NArith/BinPos *****************************************************)
 363
 364 (* NOTATION
 365 Infix "+" := Pplus : positive_scope.
 366 *)
 367
 368 (* NOTATION
 369 Infix "-" := Pminus : positive_scope.
 370 *)
 371
 372 (* NOTATION
 373 Infix "*" := Pmult : positive_scope.
 374 *)
 375
 376 (* NOTATION
 377 Infix "/" := Pdiv2 : positive_scope.
 378 *)
 379
 380 (* NOTATION
 381 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
 382 *)
 383
 384 (* From Reals/RIneq *******************************************************)
 385
 386 (* NOTATION
 387 Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
 388  with minus := Rminus div := Rdiv.
 389 *)
 390
 391 (* From Reals/Ranalysis1 **************************************************)
 392
 393 (* NOTATION
 394 Infix "+" := plus_fct : Rfun_scope.
 395 *)
 396
 397 (* NOTATION
 398 Notation "- x" := (opp_fct x) : Rfun_scope.
 399 *)
 400
 401 (* NOTATION
 402 Infix "*" := mult_fct : Rfun_scope.
 403 *)
 404
 405 (* NOTATION
 406 Infix "-" := minus_fct : Rfun_scope.
 407 *)
 408
 409 (* NOTATION
 410 Infix "/" := div_fct : Rfun_scope.
 411 *)
 412
 413 (* NOTATION
 414 Notation Local "f1 'o' f2" := (comp f1 f2)
 415   (at level 20, right associativity) : Rfun_scope.
 416 *)
 417
 418 (* NOTATION
 419 Notation "/ x" := (inv_fct x) : Rfun_scope.
 420 *)
 421
 422 (* From Reals/Rdefinitions ************************************************)
 423
 424 (* NOTATION
 425 Infix "+" := Rplus : R_scope.
 426 *)
 427
 428 (* NOTATION
 429 Infix "*" := Rmult : R_scope.
 430 *)
 431
 432 (* NOTATION
 433 Notation "- x" := (Ropp x) : R_scope.
 434 *)
 435
 436 (* NOTATION
 437 Notation "/ x" := (Rinv x) : R_scope.
 438 *)
 439
 440 (* NOTATION
 441 Infix "<" := Rlt : R_scope.
 442 *)
 443
 444 (* NOTATION
 445 Infix "-" := Rminus : R_scope.
 446 *)
 447
 448 (* NOTATION
 449 Infix "/" := Rdiv : R_scope.
 450 *)
 451
 452 (* NOTATION
 453 Infix "<=" := Rle : R_scope.
 454 *)
 455
 456 (* NOTATION
 457 Infix ">=" := Rge : R_scope.
 458 *)
 459
 460 (* NOTATION
 461 Infix ">" := Rgt : R_scope.
 462 *)
 463
 464 (* NOTATION
 465 Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
 466 *)
 467
 468 (* NOTATION
 469 Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
 470 *)
 471
 472 (* NOTATION
 473 Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
 474 *)
 475
 476 (* NOTATION
 477 Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.
 478 *)
 479
 480 (* From Reals/Rfunctions **************************************************)
 481
 482 (* NOTATION
 483 Infix "^" := pow : R_scope.
 484 *)
 485
 486 (* NOTATION
 487 Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
 488 *)
 489
 490 (* From Reals/Rpower ******************************************************)
 491
 492 (* NOTATION
 493 Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 494 *)
 495
 496 (* From Reals/Rtopology ***************************************************)
 497
 498 (* NOTATION
 499 Infix "=_D" := eq_Dom (at level 70, no associativity).
 500 *)
 501
 502 (* From Setoids/Setoid ****************************************************)
 503
 504 (* NOTATION
 505 Add Setoid Prop iff Prop_S.
 506 *)
 507
 508 (* From Wellfounded/Disjoint_Union ****************************************)
 509
 510 (* NOTATION
 511 Notation Le_AsB := (le_AsB A B leA leB).
 512 *)
 513
 514 (* From Wellfounded/Lexicographic_Exponentiation **************************)
 515
 516 (* NOTATION
 517 Notation Power := (Pow A leA).
 518 *)
 519
 520 (* NOTATION
 521 Notation Lex_Exp := (lex_exp A leA).
 522 *)
 523
 524 (* NOTATION
 525 Notation ltl := (Ltl A leA).
 526 *)
 527
 528 (* NOTATION
 529 Notation Descl := (Desc A leA).
 530 *)
 531
 532 (* NOTATION
 533 Notation List := (list A).
 534 *)
 535
 536 (* NOTATION
 537 Notation Nil := (nil (A:=A)).
 538 *)
 539
 540 (* NOTATION
 541 Notation Cons := (cons (A:=A)).
 542 *)
 543
 544 (* NOTATION
 545 Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
 546 *)
 547
 548 (* From Wellfounded/Lexicographic_Product *********************************)
 549
 550 (* NOTATION
 551 Notation LexProd := (lexprod A B leA leB).
 552 *)
 553
 554 (* NOTATION
 555 Notation Symprod := (symprod A B leA leB).
 556 *)
 557
 558 (* NOTATION
 559 Notation SwapProd := (swapprod A R).
 560 *)
 561
 562 (* From Wellfounded/Transitive_Closure ************************************)
 563
 564 (* NOTATION
 565 Notation trans_clos := (clos_trans A R).
 566 *)
 567
 568 (* From Wellfounded/Union *************************************************)
 569
 570 (* NOTATION
 571 Notation Union := (union A R1 R2).
 572 *)
 573
 574 (* From ZArith/BinInt *****************************************************)
 575
 576 (* NOTATION
 577 Infix "+" := Zplus : Z_scope.
 578 *)
 579
 580 (* NOTATION
 581 Notation "- x" := (Zopp x) : Z_scope.
 582 *)
 583
 584 (* NOTATION
 585 Infix "-" := Zminus : Z_scope.
 586 *)
 587
 588 (* NOTATION
 589 Infix "*" := Zmult : Z_scope.
 590 *)
 591
 592 (* NOTATION
 593 Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
 594 *)
 595
 596 (* NOTATION
 597 Infix "<=" := Zle : Z_scope.
 598 *)
 599
 600 (* NOTATION
 601 Infix "<" := Zlt : Z_scope.
 602 *)
 603
 604 (* NOTATION
 605 Infix ">=" := Zge : Z_scope.
 606 *)
 607
 608 (* NOTATION
 609 Infix ">" := Zgt : Z_scope.
 610 *)
 611
 612 (* NOTATION
 613 Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
 614 *)
 615
 616 (* NOTATION
 617 Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
 618 *)
 619
 620 (* NOTATION
 621 Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 622 *)
 623
 624 (* NOTATION
 625 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 626 *)
 627
 628 (* From ZArith/Zdiv *******************************************************)
 629
 630 (* NOTATION
 631 Infix "/" := Zdiv : Z_scope.
 632 *)
 633
 634 (* NOTATION
 635 Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
 636 *)
 637
 638 (* From ZArith/Znumtheory *************************************************)
 639
 640 (* NOTATION
 641 Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
 642 *)
 643
 644 (* From ZArith/Zpower *****************************************************)
 645
 646 (* NOTATION
 647 Infix "^" := Zpower : Z_scope.
 648 *)
 649
 650 (* NOTATION
 651 Infix "^" := Zpower : Z_scope.
 652 *)
 653