helm/software/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 inline "cic:/CoRN/algebra/CLogic/Iff_left.con".
 129
 130 inline "cic:/CoRN/algebra/CLogic/Iff_right.con".
 131
 132 inline "cic:/CoRN/algebra/CLogic/Iff_refl.con".
 133
 134 inline "cic:/CoRN/algebra/CLogic/Iff_sym.con".
 135
 136 inline "cic:/CoRN/algebra/CLogic/Iff_trans.con".
 137
 138 inline "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con".
 139
 140 (* UNEXPORTED
 141 Declare Right Step Iff_right.
 142 *)
 143
 144 (* UNEXPORTED
 145 Declare Left Step Iff_left.
 146 *)
 147
 148 (* UNEXPORTED
 149 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
 150 *)
 151
 152 (* UNEXPORTED
 153 End Basics.
 154 *)
 155
 156 (* begin hide *)
 157
 158 (* end hide *)
 159
 160 inline "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con".
 161
 162 inline "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con".
 163
 164 (* begin hide *)
 165
 166 (* end hide *)
 167
 168 (*
 169 Section test.
 170
 171 Variable A:Type.
 172 Variables P,Q:A->Prop.
 173 Variables X,Y:A->CProp.
 174
 175 Check {x:A | (P x)}.
 176 Check {x:A |(X x)}.
 177 Check {x:A | (X x) | (Y x)}.
 178 Check {x:A | (P x) | (Q x)}.
 179 Check {x:A | (P x) | (X x)}.
 180 Check {x:A | (X x) | (P x)}.
 181
 182 End test.
 183 *)
 184
 185 (* UNEXPORTED
 186 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
 187 *)
 188
 189 (* UNEXPORTED
 190 Section Choice.
 191 *)
 192
 193 (* **Choice
 194 Let [P] be a predicate on $\NN^2$#N times N#.
 195 *)
 196
 197 inline "cic:/CoRN/algebra/CLogic/P.var".
 198
 199 inline "cic:/CoRN/algebra/CLogic/choice.con".
 200
 201 (* UNEXPORTED
 202 End Choice.
 203 *)
 204
 205 (* UNEXPORTED
 206 Section Logical_Remarks.
 207 *)
 208
 209 (*#* We prove a few logical results which are helpful to have as lemmas
 210 when [A], [B] and [C] are non trivial.
 211 *)
 212
 213 inline "cic:/CoRN/algebra/CLogic/CNot_Not_or.con".
 214
 215 inline "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con".
 216
 217 (* UNEXPORTED
 218 End Logical_Remarks.
 219 *)
 220
 221 (* UNEXPORTED
 222 Section CRelation_Definition.
 223 *)
 224
 225 (*#* ** [CProp]-valued Relations
 226 Similar to Relations.v in Coq's standard library.
 227
 228 %\begin{convention}% Let [A:Type] and [R:Crelation].
 229 %\end{convention}%
 230 *)
 231
 232 inline "cic:/CoRN/algebra/CLogic/A.var".
 233
 234 inline "cic:/CoRN/algebra/CLogic/Crelation.con".
 235
 236 inline "cic:/CoRN/algebra/CLogic/R.var".
 237
 238 inline "cic:/CoRN/algebra/CLogic/Creflexive.con".
 239
 240 inline "cic:/CoRN/algebra/CLogic/Ctransitive.con".
 241
 242 inline "cic:/CoRN/algebra/CLogic/Csymmetric.con".
 243
 244 inline "cic:/CoRN/algebra/CLogic/Cequiv.con".
 245
 246 (* UNEXPORTED
 247 End CRelation_Definition.
 248 *)
 249
 250 (* UNEXPORTED
 251 Section TRelation_Definition.
 252 *)
 253
 254 (*#* ** [Prop]-valued Relations
 255 Analogous.
 256
 257 %\begin{convention}% Let [A:Type] and [R:Trelation].
 258 %\end{convention}%
 259 *)
 260
 261 inline "cic:/CoRN/algebra/CLogic/A.var".
 262
 263 inline "cic:/CoRN/algebra/CLogic/Trelation.con".
 264
 265 inline "cic:/CoRN/algebra/CLogic/R.var".
 266
 267 inline "cic:/CoRN/algebra/CLogic/Treflexive.con".
 268
 269 inline "cic:/CoRN/algebra/CLogic/Ttransitive.con".
 270
 271 inline "cic:/CoRN/algebra/CLogic/Tsymmetric.con".
 272
 273 inline "cic:/CoRN/algebra/CLogic/Tequiv.con".
 274
 275 (* UNEXPORTED
 276 End TRelation_Definition.
 277 *)
 278
 279 inline "cic:/CoRN/algebra/CLogic/eqs.ind".
 280
 281 (* UNEXPORTED
 282 Section le_odd.
 283 *)
 284
 285 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
 286 *)
 287
 288 inline "cic:/CoRN/algebra/CLogic/Cle.ind".
 289
 290 inline "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con".
 291
 292 inline "cic:/CoRN/algebra/CLogic/my_Cle_ind.con".
 293
 294 inline "cic:/CoRN/algebra/CLogic/Cle_n_S.con".
 295
 296 inline "cic:/CoRN/algebra/CLogic/toCle.con".
 297
 298 (* UNEXPORTED
 299 Hint Resolve toCle.
 300 *)
 301
 302 inline "cic:/CoRN/algebra/CLogic/Cle_to.con".
 303
 304 inline "cic:/CoRN/algebra/CLogic/Clt.con".
 305
 306 inline "cic:/CoRN/algebra/CLogic/toCProp_lt.con".
 307
 308 inline "cic:/CoRN/algebra/CLogic/Clt_to.con".
 309
 310 inline "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con".
 311
 312 inline "cic:/CoRN/algebra/CLogic/Cnat_total_order.con".
 313
 314 inline "cic:/CoRN/algebra/CLogic/Codd.ind".
 315
 316 inline "cic:/CoRN/algebra/CLogic/Codd_even_to.con".
 317
 318 inline "cic:/CoRN/algebra/CLogic/Codd_to.con".
 319
 320 inline "cic:/CoRN/algebra/CLogic/Ceven_to.con".
 321
 322 inline "cic:/CoRN/algebra/CLogic/to_Codd_even.con".
 323
 324 inline "cic:/CoRN/algebra/CLogic/to_Codd.con".
 325
 326 inline "cic:/CoRN/algebra/CLogic/to_Ceven.con".
 327
 328 (* UNEXPORTED
 329 End le_odd.
 330 *)
 331
 332 (* UNEXPORTED
 333 Section Misc.
 334 *)
 335
 336 (*#* **Miscellaneous
 337 *)
 338
 339 inline "cic:/CoRN/algebra/CLogic/CZ_exh.con".
 340
 341 inline "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con".
 342
 343 inline "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con".
 344
 345 inline "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con".
 346
 347 inline "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con".
 348
 349 inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
 350
 351 (* UNEXPORTED
 352 End Misc.
 353 *)
 354
 355 (*#* **Results about the natural numbers
 356
 357 We now define a class of predicates on a finite subset of natural
 358 numbers that will be important throughout all our work.  Essentially,
 359 these are simply setoid predicates, but for clarity we will never
 360 write them in that form but we will single out the preservation of the
 361 setoid equality.
 362 *)
 363
 364 inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con".
 365
 366 inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con".
 367
 368 (* UNEXPORTED
 369 Implicit Arguments nat_less_n_pred [n].
 370 *)
 371
 372 (* UNEXPORTED
 373 Implicit Arguments nat_less_n_pred' [n].
 374 *)
 375
 376 (* UNEXPORTED
 377 Section Odd_and_Even.
 378 *)
 379
 380 (*#*
 381 For our work we will many times need to distinguish cases between even or odd numbers.
 382 We begin by proving that this case distinction is decidable.
 383 Next, we prove the usual results about sums of even and odd numbers:
 384 *)
 385
 386 inline "cic:/CoRN/algebra/CLogic/even_plus_n_n.con".
 387
 388 inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con".
 389
 390 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
 391 *)
 392
 393 inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con".
 394
 395 (* UNEXPORTED
 396 End Odd_and_Even.
 397 *)
 398
 399 (* UNEXPORTED
 400 Hint Resolve even_plus_n_n: arith.
 401 *)
 402
 403 (* UNEXPORTED
 404 Hint Resolve toCle: core.
 405 *)
 406
 407 (* UNEXPORTED
 408 Section Natural_Numbers.
 409 *)
 410
 411 (*#* **Algebraic Properties
 412
 413 We now present a series of trivial things proved with [Omega] that are
 414 stated as lemmas to make proofs shorter and to aid in auxiliary
 415 definitions.  Giving a name to these results allows us to use them in
 416 definitions keeping conciseness.
 417 *)
 418
 419 inline "cic:/CoRN/algebra/CLogic/Clt_le_weak.con".
 420
 421 inline "cic:/CoRN/algebra/CLogic/lt_5.con".
 422
 423 inline "cic:/CoRN/algebra/CLogic/lt_8.con".
 424
 425 inline "cic:/CoRN/algebra/CLogic/pred_lt.con".
 426
 427 inline "cic:/CoRN/algebra/CLogic/lt_10.con".
 428
 429 inline "cic:/CoRN/algebra/CLogic/lt_pred'.con".
 430
 431 inline "cic:/CoRN/algebra/CLogic/le_1.con".
 432
 433 inline "cic:/CoRN/algebra/CLogic/le_2.con".
 434
 435 inline "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con".
 436
 437 inline "cic:/CoRN/algebra/CLogic/not_not_lt.con".
 438
 439 inline "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con".
 440
 441 (*#* We now prove some properties of functions on the natural numbers.
 442
 443 %\begin{convention}% Let [H:nat->nat].
 444 %\end{convention}%
 445 *)
 446
 447 inline "cic:/CoRN/algebra/CLogic/h.var".
 448
 449 (*#*
 450 First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
 451 for every natural number [n] then [h] is monotonous.  An analogous result
 452 holds for weak monotonicity.
 453 *)
 454
 455 inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con".
 456
 457 inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con".
 458
 459 (*#* A strictly increasing function is injective: *)
 460
 461 inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con".
 462
 463 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
 464
 465 inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con".
 466
 467 (*#*
 468 The last lemmas in this section state that a monotonous function in the
 469  natural numbers completely covers the natural numbers, that is, for every
 470 natural number [n] there is an [i] such that [h(i) <= n<(n+1) <= h(i+1)].
 471 These are useful for integration.
 472 *)
 473
 474 inline "cic:/CoRN/algebra/CLogic/mon_fun_covers.con".
 475
 476 inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
 477
 478 (* UNEXPORTED
 479 End Natural_Numbers.
 480 *)
 481
 482 (*#*
 483 Useful for the Fundamental Theorem of Algebra.
 484 *)
 485
 486 inline "cic:/CoRN/algebra/CLogic/kseq_prop.con".
 487
 488 (* UNEXPORTED
 489 Section Predicates_to_CProp.
 490 *)
 491
 492 (*#* **Logical Properties
 493
 494 This section contains lemmas that aid in logical reasoning with
 495 natural numbers.  First, we present some principles of induction, both
 496 for [CProp]- and [Prop]-valued predicates.  We begin by presenting the
 497 results for [CProp]-valued predicates:
 498 *)
 499
 500 inline "cic:/CoRN/algebra/CLogic/even_induction.con".
 501
 502 inline "cic:/CoRN/algebra/CLogic/odd_induction.con".
 503
 504 inline "cic:/CoRN/algebra/CLogic/four_induction.con".
 505
 506 inline "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con".
 507
 508 inline "cic:/CoRN/algebra/CLogic/odd_double_ind.con".
 509
 510 (*#* For subsetoid predicates in the natural numbers we can eliminate
 511 disjunction (and existential quantification) as follows.
 512 *)
 513
 514 inline "cic:/CoRN/algebra/CLogic/finite_or_elim.con".
 515
 516 inline "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con".
 517
 518 (* UNEXPORTED
 519 End Predicates_to_CProp.
 520 *)
 521
 522 (* UNEXPORTED
 523 Section Predicates_to_Prop.
 524 *)
 525
 526 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
 527 completeness's sake.
 528 *)
 529
 530 inline "cic:/CoRN/algebra/CLogic/even_ind.con".
 531
 532 inline "cic:/CoRN/algebra/CLogic/odd_ind.con".
 533
 534 inline "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con".
 535
 536 inline "cic:/CoRN/algebra/CLogic/four_ind.con".
 537
 538 (* UNEXPORTED
 539 End Predicates_to_Prop.
 540 *)
 541
 542 (*#* **Integers
 543
 544 Similar results for integers.
 545 *)
 546
 547 (* begin hide *)
 548
 549 (* UNEXPORTED
 550 Tactic Notation "ElimCompare" constr(c) constr(d) :=  elim_compare c d.
 551 *)
 552
 553 (* end hide *)
 554
 555 inline "cic:/CoRN/algebra/CLogic/Zlts.con".
 556
 557 inline "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con".
 558
 559 inline "cic:/CoRN/algebra/CLogic/CZlt_to.con".
 560
 561 inline "cic:/CoRN/algebra/CLogic/Zsgn_1.con".
 562
 563 inline "cic:/CoRN/algebra/CLogic/Zsgn_2.con".
 564
 565 inline "cic:/CoRN/algebra/CLogic/Zsgn_3.con".
 566
 567 (*#* The following have unusual names, in line with the series of lemmata in
 568 fast_integers.v.
 569 *)
 570
 571 inline "cic:/CoRN/algebra/CLogic/ZL4'.con".
 572
 573 inline "cic:/CoRN/algebra/CLogic/ZL9.con".
 574
 575 inline "cic:/CoRN/algebra/CLogic/Zsgn_4.con".
 576
 577 inline "cic:/CoRN/algebra/CLogic/Zsgn_5.con".
 578
 579 inline "cic:/CoRN/algebra/CLogic/nat_nat_pos.con".
 580
 581 inline "cic:/CoRN/algebra/CLogic/S_predn.con".
 582
 583 inline "cic:/CoRN/algebra/CLogic/absolu_1.con".
 584
 585 inline "cic:/CoRN/algebra/CLogic/absolu_2.con".
 586
 587 inline "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con".
 588
 589 inline "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con".
 590
 591 inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".
 592