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