]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/algebra/CLogic.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / CoRN / 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% #⇔# *)
26
27 (*#* printing CFalse %\ensuremath\bot% #⊥# *)
28
29 (*#* printing False %\ensuremath\bot% #⊥# *)
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" as definition.
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" as definition.
91
92 inline procedural "cic:/CoRN/algebra/CLogic/CAnd.ind".
93
94 inline procedural "cic:/CoRN/algebra/CLogic/Iff.con" as definition.
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" as definition.
101
102 inline procedural "cic:/CoRN/algebra/CLogic/proj2_sigT.con" as definition.
103
104 inline procedural "cic:/CoRN/algebra/CLogic/sig2T.ind".
105
106 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sig2T.con" as definition.
107
108 inline procedural "cic:/CoRN/algebra/CLogic/proj2a_sig2T.con" as definition.
109
110 inline procedural "cic:/CoRN/algebra/CLogic/proj2b_sig2T.con" as definition.
111
112 inline procedural "cic:/CoRN/algebra/CLogic/toCProp.ind".
113
114 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_e.con" as lemma.
115
116 inline procedural "cic:/CoRN/algebra/CLogic/CNot.con" as definition.
117
118 inline procedural "cic:/CoRN/algebra/CLogic/Ccontrapos'.con" as lemma.
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" as lemma.
131
132 inline procedural "cic:/CoRN/algebra/CLogic/Iff_right.con" as lemma.
133
134 inline procedural "cic:/CoRN/algebra/CLogic/Iff_refl.con" as lemma.
135
136 inline procedural "cic:/CoRN/algebra/CLogic/Iff_sym.con" as lemma.
137
138 inline procedural "cic:/CoRN/algebra/CLogic/Iff_trans.con" as lemma.
139
140 inline procedural "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con" as lemma.
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" as lemma.
171
172 inline procedural "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con" as lemma.
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 (* UNEXPORTED
219 cic:/CoRN/algebra/CLogic/Choice/P.var
220 *)
221
222 inline procedural "cic:/CoRN/algebra/CLogic/choice.con" as lemma.
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 procedural "cic:/CoRN/algebra/CLogic/CNot_Not_or.con" as lemma.
237
238 inline procedural "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con" as lemma.
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 (* UNEXPORTED
256 cic:/CoRN/algebra/CLogic/CRelation_Definition/A.var
257 *)
258
259 inline procedural "cic:/CoRN/algebra/CLogic/Crelation.con" as definition.
260
261 (* UNEXPORTED
262 cic:/CoRN/algebra/CLogic/CRelation_Definition/R.var
263 *)
264
265 inline procedural "cic:/CoRN/algebra/CLogic/Creflexive.con" as definition.
266
267 inline procedural "cic:/CoRN/algebra/CLogic/Ctransitive.con" as definition.
268
269 inline procedural "cic:/CoRN/algebra/CLogic/Csymmetric.con" as definition.
270
271 inline procedural "cic:/CoRN/algebra/CLogic/Cequiv.con" as definition.
272
273 (* UNEXPORTED
274 End CRelation_Definition
275 *)
276
277 (* UNEXPORTED
278 Section TRelation_Definition
279 *)
280
281 (*#* ** [Prop]-valued Relations
282 Analogous.
283
284 %\begin{convention}% Let [A:Type] and [R:Trelation].
285 %\end{convention}%
286 *)
287
288 (* UNEXPORTED
289 cic:/CoRN/algebra/CLogic/TRelation_Definition/A.var
290 *)
291
292 inline procedural "cic:/CoRN/algebra/CLogic/Trelation.con" as definition.
293
294 (* UNEXPORTED
295 cic:/CoRN/algebra/CLogic/TRelation_Definition/R.var
296 *)
297
298 inline procedural "cic:/CoRN/algebra/CLogic/Treflexive.con" as definition.
299
300 inline procedural "cic:/CoRN/algebra/CLogic/Ttransitive.con" as definition.
301
302 inline procedural "cic:/CoRN/algebra/CLogic/Tsymmetric.con" as definition.
303
304 inline procedural "cic:/CoRN/algebra/CLogic/Tequiv.con" as definition.
305
306 (* UNEXPORTED
307 End TRelation_Definition
308 *)
309
310 inline procedural "cic:/CoRN/algebra/CLogic/eqs.ind".
311
312 (* UNEXPORTED
313 Section le_odd
314 *)
315
316 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
317 *)
318
319 inline procedural "cic:/CoRN/algebra/CLogic/Cle.ind".
320
321 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con" as theorem.
322
323 inline procedural "cic:/CoRN/algebra/CLogic/my_Cle_ind.con" as theorem.
324
325 inline procedural "cic:/CoRN/algebra/CLogic/Cle_n_S.con" as theorem.
326
327 inline procedural "cic:/CoRN/algebra/CLogic/toCle.con" as lemma.
328
329 (* UNEXPORTED
330 Hint Resolve toCle.
331 *)
332
333 inline procedural "cic:/CoRN/algebra/CLogic/Cle_to.con" as lemma.
334
335 inline procedural "cic:/CoRN/algebra/CLogic/Clt.con" as definition.
336
337 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_lt.con" as lemma.
338
339 inline procedural "cic:/CoRN/algebra/CLogic/Clt_to.con" as lemma.
340
341 inline procedural "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con" as lemma.
342
343 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_total_order.con" as lemma.
344
345 inline procedural "cic:/CoRN/algebra/CLogic/Codd.ind".
346
347 inline procedural "cic:/CoRN/algebra/CLogic/Codd_even_to.con" as lemma.
348
349 inline procedural "cic:/CoRN/algebra/CLogic/Codd_to.con" as lemma.
350
351 inline procedural "cic:/CoRN/algebra/CLogic/Ceven_to.con" as lemma.
352
353 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd_even.con" as lemma.
354
355 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd.con" as lemma.
356
357 inline procedural "cic:/CoRN/algebra/CLogic/to_Ceven.con" as lemma.
358
359 (* UNEXPORTED
360 End le_odd
361 *)
362
363 (* UNEXPORTED
364 Section Misc
365 *)
366
367 (*#* **Miscellaneous
368 *)
369
370 inline procedural "cic:/CoRN/algebra/CLogic/CZ_exh.con" as lemma.
371
372 inline procedural "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con" as lemma.
373
374 inline procedural "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con" as lemma.
375
376 inline procedural "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con" as lemma.
377
378 inline procedural "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con" as lemma.
379
380 inline procedural "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con" as lemma.
381
382 (* UNEXPORTED
383 End Misc
384 *)
385
386 (*#* **Results about the natural numbers
387
388 We now define a class of predicates on a finite subset of natural
389 numbers that will be important throughout all our work.  Essentially,
390 these are simply setoid predicates, but for clarity we will never
391 write them in that form but we will single out the preservation of the
392 setoid equality.
393 *)
394
395 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con" as definition.
396
397 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con" as definition.
398
399 (* UNEXPORTED
400 Implicit Arguments nat_less_n_pred [n].
401 *)
402
403 (* UNEXPORTED
404 Implicit Arguments nat_less_n_pred' [n].
405 *)
406
407 (* UNEXPORTED
408 Section Odd_and_Even
409 *)
410
411 (*#*
412 For our work we will many times need to distinguish cases between even or odd numbers.
413 We begin by proving that this case distinction is decidable.
414 Next, we prove the usual results about sums of even and odd numbers:
415 *)
416
417 inline procedural "cic:/CoRN/algebra/CLogic/even_plus_n_n.con" as lemma.
418
419 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con" as lemma.
420
421 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
422 *)
423
424 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con" as lemma.
425
426 (* UNEXPORTED
427 End Odd_and_Even
428 *)
429
430 (* UNEXPORTED
431 Hint Resolve even_plus_n_n: arith.
432 *)
433
434 (* UNEXPORTED
435 Hint Resolve toCle: core.
436 *)
437
438 (* UNEXPORTED
439 Section Natural_Numbers
440 *)
441
442 (*#* **Algebraic Properties
443
444 We now present a series of trivial things proved with [Omega] that are
445 stated as lemmas to make proofs shorter and to aid in auxiliary
446 definitions.  Giving a name to these results allows us to use them in
447 definitions keeping conciseness.
448 *)
449
450 inline procedural "cic:/CoRN/algebra/CLogic/Clt_le_weak.con" as lemma.
451
452 inline procedural "cic:/CoRN/algebra/CLogic/lt_5.con" as lemma.
453
454 inline procedural "cic:/CoRN/algebra/CLogic/lt_8.con" as lemma.
455
456 inline procedural "cic:/CoRN/algebra/CLogic/pred_lt.con" as lemma.
457
458 inline procedural "cic:/CoRN/algebra/CLogic/lt_10.con" as lemma.
459
460 inline procedural "cic:/CoRN/algebra/CLogic/lt_pred'.con" as lemma.
461
462 inline procedural "cic:/CoRN/algebra/CLogic/le_1.con" as lemma.
463
464 inline procedural "cic:/CoRN/algebra/CLogic/le_2.con" as lemma.
465
466 inline procedural "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con" as lemma.
467
468 inline procedural "cic:/CoRN/algebra/CLogic/not_not_lt.con" as lemma.
469
470 inline procedural "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con" as lemma.
471
472 (*#* We now prove some properties of functions on the natural numbers.
473
474 %\begin{convention}% Let [H:nat->nat].
475 %\end{convention}%
476 *)
477
478 (* UNEXPORTED
479 cic:/CoRN/algebra/CLogic/Natural_Numbers/h.var
480 *)
481
482 (*#*
483 First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
484 for every natural number [n] then [h] is monotonous.  An analogous result
485 holds for weak monotonicity.
486 *)
487
488 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con" as lemma.
489
490 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con" as lemma.
491
492 (*#* A strictly increasing function is injective: *)
493
494 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con" as lemma.
495
496 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
497
498 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con" as lemma.
499
500 (*#*
501 The last lemmas in this section state that a monotonous function in the
502  natural numbers completely covers the natural numbers, that is, for every
503 natural number [n] there is an [i] such that [h(i) <= n<(n+1) <= h(i+1)].
504 These are useful for integration.
505 *)
506
507 inline procedural "cic:/CoRN/algebra/CLogic/mon_fun_covers.con" as lemma.
508
509 inline procedural "cic:/CoRN/algebra/CLogic/weird_mon_covers.con" as lemma.
510
511 (* UNEXPORTED
512 End Natural_Numbers
513 *)
514
515 (*#*
516 Useful for the Fundamental Theorem of Algebra.
517 *)
518
519 inline procedural "cic:/CoRN/algebra/CLogic/kseq_prop.con" as lemma.
520
521 (* UNEXPORTED
522 Section Predicates_to_CProp
523 *)
524
525 (*#* **Logical Properties
526
527 This section contains lemmas that aid in logical reasoning with
528 natural numbers.  First, we present some principles of induction, both
529 for [CProp]- and [Prop]-valued predicates.  We begin by presenting the
530 results for [CProp]-valued predicates:
531 *)
532
533 inline procedural "cic:/CoRN/algebra/CLogic/even_induction.con" as lemma.
534
535 inline procedural "cic:/CoRN/algebra/CLogic/odd_induction.con" as lemma.
536
537 inline procedural "cic:/CoRN/algebra/CLogic/four_induction.con" as lemma.
538
539 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con" as lemma.
540
541 inline procedural "cic:/CoRN/algebra/CLogic/odd_double_ind.con" as lemma.
542
543 (*#* For subsetoid predicates in the natural numbers we can eliminate
544 disjunction (and existential quantification) as follows.
545 *)
546
547 inline procedural "cic:/CoRN/algebra/CLogic/finite_or_elim.con" as lemma.
548
549 inline procedural "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con" as lemma.
550
551 (* UNEXPORTED
552 End Predicates_to_CProp
553 *)
554
555 (* UNEXPORTED
556 Section Predicates_to_Prop
557 *)
558
559 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
560 completeness's sake.
561 *)
562
563 inline procedural "cic:/CoRN/algebra/CLogic/even_ind.con" as lemma.
564
565 inline procedural "cic:/CoRN/algebra/CLogic/odd_ind.con" as lemma.
566
567 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con" as lemma.
568
569 inline procedural "cic:/CoRN/algebra/CLogic/four_ind.con" as lemma.
570
571 (* UNEXPORTED
572 End Predicates_to_Prop
573 *)
574
575 (*#* **Integers
576
577 Similar results for integers.
578 *)
579
580 (* begin hide *)
581
582 (* UNEXPORTED
583 Tactic Notation "ElimCompare" constr(c) constr(d) :=  elim_compare c d.
584 *)
585
586 (* end hide *)
587
588 inline procedural "cic:/CoRN/algebra/CLogic/Zlts.con" as definition.
589
590 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con" as lemma.
591
592 inline procedural "cic:/CoRN/algebra/CLogic/CZlt_to.con" as lemma.
593
594 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_1.con" as lemma.
595
596 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_2.con" as lemma.
597
598 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_3.con" as lemma.
599
600 (*#* The following have unusual names, in line with the series of lemmata in
601 fast_integers.v.
602 *)
603
604 inline procedural "cic:/CoRN/algebra/CLogic/ZL4'.con" as lemma.
605
606 inline procedural "cic:/CoRN/algebra/CLogic/ZL9.con" as lemma.
607
608 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_4.con" as theorem.
609
610 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_5.con" as theorem.
611
612 inline procedural "cic:/CoRN/algebra/CLogic/nat_nat_pos.con" as lemma.
613
614 inline procedural "cic:/CoRN/algebra/CLogic/S_predn.con" as theorem.
615
616 inline procedural "cic:/CoRN/algebra/CLogic/absolu_1.con" as lemma.
617
618 inline procedural "cic:/CoRN/algebra/CLogic/absolu_2.con" as lemma.
619
620 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con" as lemma.
621
622 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con" as lemma.
623
624 inline procedural "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con" as lemma.
625
626 (* NOTATION
627 Notation ProjT1 := (proj1_sigT _ _).
628 *)
629
630 (* NOTATION
631 Notation ProjT2 := (proj2_sigT _ _).
632 *)
633