helm/software/matita/contribs/CoRN-Procedural/algebra/CLogic.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: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *)
  20
  21 (*#* printing Not %\ensuremath\neg% #~# *)
  22
  23 (*#* printing CNot %\ensuremath\neg% #~# *)
  24
  25 (*#* printing Iff %\ensuremath\Leftrightarrow% #&hArr;# *)
  26
  27 (*#* printing CFalse %\ensuremath\bot% #&perp;# *)
  28
  29 (*#* printing False %\ensuremath\bot% #&perp;# *)
  30
  31 (*#* printing CTrue %\ensuremath\top% *)
  32
  33 (*#* printing True %\ensuremath\top% *)
  34
  35 (*#* printing or %\ensuremath{\mathrel\vee}% *)
  36
  37 (*#* printing and %\ensuremath{\mathrel\wedge}% *)
  38
  39 include "algebra/Basics.ma".
  40
  41 (*#* *Extending the Coq Logic
  42 Because notions of apartness and order have computational meaning, we
  43 will have to define logical connectives in [Type].  In order to
  44 keep a syntactic distinction between types of terms, we define [CProp]
  45 as an alias for [Type], to be used as type of (computationally meaningful)
  46 propositions.
  47
  48 Falsehood and negation will typically not be needed in [CProp], as
  49 they are used to refer to negative statements, which carry no
  50 computational meaning.  Therefore, we will simply define a negation
  51 operator from [Type] to [Prop] .
  52
  53 Conjunction, disjunction and existential quantification will have to come in
  54 multiple varieties.  For conjunction, we will need four operators of type
  55 [s1->s2->s3], where [s3] is [Prop] if both [s1] and [s2]
  56 are [Prop] and [CProp] otherwise.
  57 We here take advantage of the inclusion of [Prop] in [Type].
  58
  59 Disjunction is slightly different, as it will always return a value in [CProp] even
  60 if both arguments are propositions.  This is because in general
  61 it may be computationally important to know which of the two branches of the
  62 disjunction actually holds.
  63
  64 Existential quantification will similarly always return a value in [CProp].
  65
  66 - [CProp]-valued conjuction will be denoted as [and];
  67 - [Crop]-valued conjuction will be denoted as [or];
  68 - Existential quantification will be written as [{x:A & B}] or [{x:A | B}],
  69 according to whether [B] is respectively of type [CProp] or [Prop].
  70
  71 In a few specific situations we do need truth, false and negation in [CProp],
  72 so we will also introduce them; this should be a temporary option.
  73
  74 Finally, for other formulae that might occur in our [CProp]-valued
  75 propositions, such as [(le m n)], we have to introduce a [CProp]-valued
  76 version.
  77 *)
  78
  79 inline procedural "cic:/CoRN/algebra/CLogic/CProp.con".
  80
  81 (* UNEXPORTED
  82 Section Basics
  83 *)
  84
  85 (*#* ** Basics
  86 Here we treat conversion from [Prop] to [CProp] and vice versa,
  87 and some basic connectives in [CProp].
  88 *)
  89
  90 inline procedural "cic:/CoRN/algebra/CLogic/Not.con".
  91
  92 inline procedural "cic:/CoRN/algebra/CLogic/CAnd.ind".
  93
  94 inline procedural "cic:/CoRN/algebra/CLogic/Iff.con".
  95
  96 inline procedural "cic:/CoRN/algebra/CLogic/CFalse.ind".
  97
  98 inline procedural "cic:/CoRN/algebra/CLogic/CTrue.ind".
  99
 100 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sigT.con".
 101
 102 inline procedural "cic:/CoRN/algebra/CLogic/proj2_sigT.con".
 103
 104 inline procedural "cic:/CoRN/algebra/CLogic/sig2T.ind".
 105
 106 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sig2T.con".
 107
 108 inline procedural "cic:/CoRN/algebra/CLogic/proj2a_sig2T.con".
 109
 110 inline procedural "cic:/CoRN/algebra/CLogic/proj2b_sig2T.con".
 111
 112 inline procedural "cic:/CoRN/algebra/CLogic/toCProp.ind".
 113
 114 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_e.con".
 115
 116 inline procedural "cic:/CoRN/algebra/CLogic/CNot.con".
 117
 118 inline procedural "cic:/CoRN/algebra/CLogic/Ccontrapos'.con".
 119
 120 inline procedural "cic:/CoRN/algebra/CLogic/COr.ind".
 121
 122 (*#*
 123 Some lemmas to make it possible to use [Step] when reasoning with
 124 biimplications.*)
 125
 126 (* NOTATION
 127 Infix "IFF" := Iff (at level 60, right associativity).
 128 *)
 129
 130 inline procedural "cic:/CoRN/algebra/CLogic/Iff_left.con".
 131
 132 inline procedural "cic:/CoRN/algebra/CLogic/Iff_right.con".
 133
 134 inline procedural "cic:/CoRN/algebra/CLogic/Iff_refl.con".
 135
 136 inline procedural "cic:/CoRN/algebra/CLogic/Iff_sym.con".
 137
 138 inline procedural "cic:/CoRN/algebra/CLogic/Iff_trans.con".
 139
 140 inline procedural "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con".
 141
 142 (* UNEXPORTED
 143 Declare Right Step Iff_right.
 144 *)
 145
 146 (* UNEXPORTED
 147 Declare Left Step Iff_left.
 148 *)
 149
 150 (* UNEXPORTED
 151 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
 152 *)
 153
 154 (* UNEXPORTED
 155 End Basics
 156 *)
 157
 158 (* begin hide *)
 159
 160 (* NOTATION
 161 Infix "or" := COr (at level 85, right associativity).
 162 *)
 163
 164 (* NOTATION
 165 Infix "and" := CAnd (at level 80, right associativity).
 166 *)
 167
 168 (* end hide *)
 169
 170 inline procedural "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con".
 171
 172 inline procedural "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con".
 173
 174 (* begin hide *)
 175
 176 (* NOTATION
 177 Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
 178   (at level 0, x at level 99) : type_scope.
 179 *)
 180
 181 (* NOTATION
 182 Notation "{ x : A  |  P  |  Q }" :=
 183   (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
 184   type_scope.
 185 *)
 186
 187 (* end hide *)
 188
 189 (*
 190 Section test.
 191
 192 Variable A:Type.
 193 Variables P,Q:A->Prop.
 194 Variables X,Y:A->CProp.
 195
 196 Check {x:A | (P x)}.
 197 Check {x:A |(X x)}.
 198 Check {x:A | (X x) | (Y x)}.
 199 Check {x:A | (P x) | (Q x)}.
 200 Check {x:A | (P x) | (X x)}.
 201 Check {x:A | (X x) | (P x)}.
 202
 203 End test.
 204 *)
 205
 206 (* UNEXPORTED
 207 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
 208 *)
 209
 210 (* UNEXPORTED
 211 Section Choice
 212 *)
 213
 214 (* **Choice
 215 Let [P] be a predicate on $\NN^2$#N times N#.
 216 *)
 217
 218 alias id "P" = "cic:/CoRN/algebra/CLogic/Choice/P.var".
 219
 220 inline procedural "cic:/CoRN/algebra/CLogic/choice.con".
 221
 222 (* UNEXPORTED
 223 End Choice
 224 *)
 225
 226 (* UNEXPORTED
 227 Section Logical_Remarks
 228 *)
 229
 230 (*#* We prove a few logical results which are helpful to have as lemmas
 231 when [A], [B] and [C] are non trivial.
 232 *)
 233
 234 inline procedural "cic:/CoRN/algebra/CLogic/CNot_Not_or.con".
 235
 236 inline procedural "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con".
 237
 238 (* UNEXPORTED
 239 End Logical_Remarks
 240 *)
 241
 242 (* UNEXPORTED
 243 Section CRelation_Definition
 244 *)
 245
 246 (*#* ** [CProp]-valued Relations
 247 Similar to Relations.v in Coq's standard library.
 248
 249 %\begin{convention}% Let [A:Type] and [R:Crelation].
 250 %\end{convention}%
 251 *)
 252
 253 alias id "A" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/A.var".
 254
 255 inline procedural "cic:/CoRN/algebra/CLogic/Crelation.con".
 256
 257 alias id "R" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/R.var".
 258
 259 inline procedural "cic:/CoRN/algebra/CLogic/Creflexive.con".
 260
 261 inline procedural "cic:/CoRN/algebra/CLogic/Ctransitive.con".
 262
 263 inline procedural "cic:/CoRN/algebra/CLogic/Csymmetric.con".
 264
 265 inline procedural "cic:/CoRN/algebra/CLogic/Cequiv.con".
 266
 267 (* UNEXPORTED
 268 End CRelation_Definition
 269 *)
 270
 271 (* UNEXPORTED
 272 Section TRelation_Definition
 273 *)
 274
 275 (*#* ** [Prop]-valued Relations
 276 Analogous.
 277
 278 %\begin{convention}% Let [A:Type] and [R:Trelation].
 279 %\end{convention}%
 280 *)
 281
 282 alias id "A" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/A.var".
 283
 284 inline procedural "cic:/CoRN/algebra/CLogic/Trelation.con".
 285
 286 alias id "R" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/R.var".
 287
 288 inline procedural "cic:/CoRN/algebra/CLogic/Treflexive.con".
 289
 290 inline procedural "cic:/CoRN/algebra/CLogic/Ttransitive.con".
 291
 292 inline procedural "cic:/CoRN/algebra/CLogic/Tsymmetric.con".
 293
 294 inline procedural "cic:/CoRN/algebra/CLogic/Tequiv.con".
 295
 296 (* UNEXPORTED
 297 End TRelation_Definition
 298 *)
 299
 300 inline procedural "cic:/CoRN/algebra/CLogic/eqs.ind".
 301
 302 (* UNEXPORTED
 303 Section le_odd
 304 *)
 305
 306 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
 307 *)
 308
 309 inline procedural "cic:/CoRN/algebra/CLogic/Cle.ind".
 310
 311 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con".
 312
 313 inline procedural "cic:/CoRN/algebra/CLogic/my_Cle_ind.con".
 314
 315 inline procedural "cic:/CoRN/algebra/CLogic/Cle_n_S.con".
 316
 317 inline procedural "cic:/CoRN/algebra/CLogic/toCle.con".
 318
 319 (* UNEXPORTED
 320 Hint Resolve toCle.
 321 *)
 322
 323 inline procedural "cic:/CoRN/algebra/CLogic/Cle_to.con".
 324
 325 inline procedural "cic:/CoRN/algebra/CLogic/Clt.con".
 326
 327 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_lt.con".
 328
 329 inline procedural "cic:/CoRN/algebra/CLogic/Clt_to.con".
 330
 331 inline procedural "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con".
 332
 333 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_total_order.con".
 334
 335 inline procedural "cic:/CoRN/algebra/CLogic/Codd.ind".
 336
 337 inline procedural "cic:/CoRN/algebra/CLogic/Codd_even_to.con".
 338
 339 inline procedural "cic:/CoRN/algebra/CLogic/Codd_to.con".
 340
 341 inline procedural "cic:/CoRN/algebra/CLogic/Ceven_to.con".
 342
 343 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd_even.con".
 344
 345 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd.con".
 346
 347 inline procedural "cic:/CoRN/algebra/CLogic/to_Ceven.con".
 348
 349 (* UNEXPORTED
 350 End le_odd
 351 *)
 352
 353 (* UNEXPORTED
 354 Section Misc
 355 *)
 356
 357 (*#* **Miscellaneous
 358 *)
 359
 360 inline procedural "cic:/CoRN/algebra/CLogic/CZ_exh.con".
 361
 362 inline procedural "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con".
 363
 364 inline procedural "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con".
 365
 366 inline procedural "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con".
 367
 368 inline procedural "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con".
 369
 370 inline procedural "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
 371
 372 (* UNEXPORTED
 373 End Misc
 374 *)
 375
 376 (*#* **Results about the natural numbers
 377
 378 We now define a class of predicates on a finite subset of natural
 379 numbers that will be important throughout all our work.  Essentially,
 380 these are simply setoid predicates, but for clarity we will never
 381 write them in that form but we will single out the preservation of the
 382 setoid equality.
 383 *)
 384
 385 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con".
 386
 387 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con".
 388
 389 (* UNEXPORTED
 390 Implicit Arguments nat_less_n_pred [n].
 391 *)
 392
 393 (* UNEXPORTED
 394 Implicit Arguments nat_less_n_pred' [n].
 395 *)
 396
 397 (* UNEXPORTED
 398 Section Odd_and_Even
 399 *)
 400
 401 (*#*
 402 For our work we will many times need to distinguish cases between even or odd numbers.
 403 We begin by proving that this case distinction is decidable.
 404 Next, we prove the usual results about sums of even and odd numbers:
 405 *)
 406
 407 inline procedural "cic:/CoRN/algebra/CLogic/even_plus_n_n.con".
 408
 409 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con".
 410
 411 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
 412 *)
 413
 414 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con".
 415
 416 (* UNEXPORTED
 417 End Odd_and_Even
 418 *)
 419
 420 (* UNEXPORTED
 421 Hint Resolve even_plus_n_n: arith.
 422 *)
 423
 424 (* UNEXPORTED
 425 Hint Resolve toCle: core.
 426 *)
 427
 428 (* UNEXPORTED
 429 Section Natural_Numbers
 430 *)
 431
 432 (*#* **Algebraic Properties
 433
 434 We now present a series of trivial things proved with [Omega] that are
 435 stated as lemmas to make proofs shorter and to aid in auxiliary
 436 definitions.  Giving a name to these results allows us to use them in
 437 definitions keeping conciseness.
 438 *)
 439
 440 inline procedural "cic:/CoRN/algebra/CLogic/Clt_le_weak.con".
 441
 442 inline procedural "cic:/CoRN/algebra/CLogic/lt_5.con".
 443
 444 inline procedural "cic:/CoRN/algebra/CLogic/lt_8.con".
 445
 446 inline procedural "cic:/CoRN/algebra/CLogic/pred_lt.con".
 447
 448 inline procedural "cic:/CoRN/algebra/CLogic/lt_10.con".
 449
 450 inline procedural "cic:/CoRN/algebra/CLogic/lt_pred'.con".
 451
 452 inline procedural "cic:/CoRN/algebra/CLogic/le_1.con".
 453
 454 inline procedural "cic:/CoRN/algebra/CLogic/le_2.con".
 455
 456 inline procedural "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con".
 457
 458 inline procedural "cic:/CoRN/algebra/CLogic/not_not_lt.con".
 459
 460 inline procedural "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con".
 461
 462 (*#* We now prove some properties of functions on the natural numbers.
 463
 464 %\begin{convention}% Let [H:nat->nat].
 465 %\end{convention}%
 466 *)
 467
 468 alias id "h" = "cic:/CoRN/algebra/CLogic/Natural_Numbers/h.var".
 469
 470 (*#*
 471 First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
 472 for every natural number [n] then [h] is monotonous.  An analogous result
 473 holds for weak monotonicity.
 474 *)
 475
 476 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con".
 477
 478 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con".
 479
 480 (*#* A strictly increasing function is injective: *)
 481
 482 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con".
 483
 484 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
 485
 486 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con".
 487
 488 (*#*
 489 The last lemmas in this section state that a monotonous function in the
 490  natural numbers completely covers the natural numbers, that is, for every
 491 natural number [n] there is an [i] such that [h(i) <= n<(n+1) <= h(i+1)].
 492 These are useful for integration.
 493 *)
 494
 495 inline procedural "cic:/CoRN/algebra/CLogic/mon_fun_covers.con".
 496
 497 inline procedural "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
 498
 499 (* UNEXPORTED
 500 End Natural_Numbers
 501 *)
 502
 503 (*#*
 504 Useful for the Fundamental Theorem of Algebra.
 505 *)
 506
 507 inline procedural "cic:/CoRN/algebra/CLogic/kseq_prop.con".
 508
 509 (* UNEXPORTED
 510 Section Predicates_to_CProp
 511 *)
 512
 513 (*#* **Logical Properties
 514
 515 This section contains lemmas that aid in logical reasoning with
 516 natural numbers.  First, we present some principles of induction, both
 517 for [CProp]- and [Prop]-valued predicates.  We begin by presenting the
 518 results for [CProp]-valued predicates:
 519 *)
 520
 521 inline procedural "cic:/CoRN/algebra/CLogic/even_induction.con".
 522
 523 inline procedural "cic:/CoRN/algebra/CLogic/odd_induction.con".
 524
 525 inline procedural "cic:/CoRN/algebra/CLogic/four_induction.con".
 526
 527 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con".
 528
 529 inline procedural "cic:/CoRN/algebra/CLogic/odd_double_ind.con".
 530
 531 (*#* For subsetoid predicates in the natural numbers we can eliminate
 532 disjunction (and existential quantification) as follows.
 533 *)
 534
 535 inline procedural "cic:/CoRN/algebra/CLogic/finite_or_elim.con".
 536
 537 inline procedural "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con".
 538
 539 (* UNEXPORTED
 540 End Predicates_to_CProp
 541 *)
 542
 543 (* UNEXPORTED
 544 Section Predicates_to_Prop
 545 *)
 546
 547 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
 548 completeness's sake.
 549 *)
 550
 551 inline procedural "cic:/CoRN/algebra/CLogic/even_ind.con".
 552
 553 inline procedural "cic:/CoRN/algebra/CLogic/odd_ind.con".
 554
 555 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con".
 556
 557 inline procedural "cic:/CoRN/algebra/CLogic/four_ind.con".
 558
 559 (* UNEXPORTED
 560 End Predicates_to_Prop
 561 *)
 562
 563 (*#* **Integers
 564
 565 Similar results for integers.
 566 *)
 567
 568 (* begin hide *)
 569
 570 (* UNEXPORTED
 571 Tactic Notation "ElimCompare" constr(c) constr(d) :=  elim_compare c d.
 572 *)
 573
 574 (* end hide *)
 575
 576 inline procedural "cic:/CoRN/algebra/CLogic/Zlts.con".
 577
 578 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con".
 579
 580 inline procedural "cic:/CoRN/algebra/CLogic/CZlt_to.con".
 581
 582 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_1.con".
 583
 584 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_2.con".
 585
 586 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_3.con".
 587
 588 (*#* The following have unusual names, in line with the series of lemmata in
 589 fast_integers.v.
 590 *)
 591
 592 inline procedural "cic:/CoRN/algebra/CLogic/ZL4'.con".
 593
 594 inline procedural "cic:/CoRN/algebra/CLogic/ZL9.con".
 595
 596 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_4.con".
 597
 598 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_5.con".
 599
 600 inline procedural "cic:/CoRN/algebra/CLogic/nat_nat_pos.con".
 601
 602 inline procedural "cic:/CoRN/algebra/CLogic/S_predn.con".
 603
 604 inline procedural "cic:/CoRN/algebra/CLogic/absolu_1.con".
 605
 606 inline procedural "cic:/CoRN/algebra/CLogic/absolu_2.con".
 607
 608 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con".
 609
 610 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con".
 611
 612 inline procedural "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".
 613
 614 (* NOTATION
 615 Notation ProjT1 := (proj1_sigT _ _).
 616 *)
 617
 618 (* NOTATION
 619 Notation ProjT2 := (proj2_sigT _ _).
 620 *)
 621