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