1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CLogic".
21 (* $Id: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *)
23 (*#* printing Not %\ensuremath\neg% #~# *)
25 (*#* printing CNot %\ensuremath\neg% #~# *)
27 (*#* printing Iff %\ensuremath\Leftrightarrow% #⇔# *)
29 (*#* printing CFalse %\ensuremath\bot% #⊥# *)
31 (*#* printing False %\ensuremath\bot% #⊥# *)
33 (*#* printing CTrue %\ensuremath\top% *)
35 (*#* printing True %\ensuremath\top% *)
37 (*#* printing or %\ensuremath{\mathrel\vee}% *)
39 (*#* printing and %\ensuremath{\mathrel\wedge}% *)
41 include "algebra/Basics.ma".
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)
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] .
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].
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.
66 Existential quantification will similarly always return a value in [CProp].
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].
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.
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
81 inline "cic:/CoRN/algebra/CLogic/CProp.con".
88 Here we treat conversion from [Prop] to [CProp] and vice versa,
89 and some basic connectives in [CProp].
92 inline "cic:/CoRN/algebra/CLogic/Not.con".
94 inline "cic:/CoRN/algebra/CLogic/CAnd.ind".
96 inline "cic:/CoRN/algebra/CLogic/Iff.con".
98 inline "cic:/CoRN/algebra/CLogic/CFalse.ind".
100 inline "cic:/CoRN/algebra/CLogic/CTrue.ind".
102 inline "cic:/CoRN/algebra/CLogic/proj1_sigT.con".
104 inline "cic:/CoRN/algebra/CLogic/proj2_sigT.con".
106 inline "cic:/CoRN/algebra/CLogic/sig2T.ind".
108 inline "cic:/CoRN/algebra/CLogic/proj1_sig2T.con".
110 inline "cic:/CoRN/algebra/CLogic/proj2a_sig2T.con".
112 inline "cic:/CoRN/algebra/CLogic/proj2b_sig2T.con".
114 inline "cic:/CoRN/algebra/CLogic/toCProp.ind".
116 inline "cic:/CoRN/algebra/CLogic/toCProp_e.con".
118 inline "cic:/CoRN/algebra/CLogic/CNot.con".
120 inline "cic:/CoRN/algebra/CLogic/Ccontrapos'.con".
122 inline "cic:/CoRN/algebra/CLogic/COr.ind".
125 Some lemmas to make it possible to use [Step] when reasoning with
128 inline "cic:/CoRN/algebra/CLogic/Iff_left.con".
130 inline "cic:/CoRN/algebra/CLogic/Iff_right.con".
132 inline "cic:/CoRN/algebra/CLogic/Iff_refl.con".
134 inline "cic:/CoRN/algebra/CLogic/Iff_sym.con".
136 inline "cic:/CoRN/algebra/CLogic/Iff_trans.con".
138 inline "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con".
141 Declare Right Step Iff_right.
145 Declare Left Step Iff_left.
149 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
160 inline "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con".
162 inline "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con".
172 Variables P,Q:A->Prop.
173 Variables X,Y:A->CProp.
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)}.
186 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
194 Let [P] be a predicate on $\NN^2$#N times N#.
197 inline "cic:/CoRN/algebra/CLogic/P.var".
199 inline "cic:/CoRN/algebra/CLogic/choice.con".
206 Section Logical_Remarks.
209 (*#* We prove a few logical results which are helpful to have as lemmas
210 when [A], [B] and [C] are non trivial.
213 inline "cic:/CoRN/algebra/CLogic/CNot_Not_or.con".
215 inline "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con".
222 Section CRelation_Definition.
225 (*#* ** [CProp]-valued Relations
226 Similar to Relations.v in Coq's standard library.
228 %\begin{convention}% Let [A:Type] and [R:Crelation].
232 inline "cic:/CoRN/algebra/CLogic/A.var".
234 inline "cic:/CoRN/algebra/CLogic/Crelation.con".
236 inline "cic:/CoRN/algebra/CLogic/R.var".
238 inline "cic:/CoRN/algebra/CLogic/Creflexive.con".
240 inline "cic:/CoRN/algebra/CLogic/Ctransitive.con".
242 inline "cic:/CoRN/algebra/CLogic/Csymmetric.con".
244 inline "cic:/CoRN/algebra/CLogic/Cequiv.con".
247 End CRelation_Definition.
251 Section TRelation_Definition.
254 (*#* ** [Prop]-valued Relations
257 %\begin{convention}% Let [A:Type] and [R:Trelation].
261 inline "cic:/CoRN/algebra/CLogic/A.var".
263 inline "cic:/CoRN/algebra/CLogic/Trelation.con".
265 inline "cic:/CoRN/algebra/CLogic/R.var".
267 inline "cic:/CoRN/algebra/CLogic/Treflexive.con".
269 inline "cic:/CoRN/algebra/CLogic/Ttransitive.con".
271 inline "cic:/CoRN/algebra/CLogic/Tsymmetric.con".
273 inline "cic:/CoRN/algebra/CLogic/Tequiv.con".
276 End TRelation_Definition.
279 inline "cic:/CoRN/algebra/CLogic/eqs.ind".
285 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
288 inline "cic:/CoRN/algebra/CLogic/Cle.ind".
290 inline "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con".
292 inline "cic:/CoRN/algebra/CLogic/my_Cle_ind.con".
294 inline "cic:/CoRN/algebra/CLogic/Cle_n_S.con".
296 inline "cic:/CoRN/algebra/CLogic/toCle.con".
302 inline "cic:/CoRN/algebra/CLogic/Cle_to.con".
304 inline "cic:/CoRN/algebra/CLogic/Clt.con".
306 inline "cic:/CoRN/algebra/CLogic/toCProp_lt.con".
308 inline "cic:/CoRN/algebra/CLogic/Clt_to.con".
310 inline "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con".
312 inline "cic:/CoRN/algebra/CLogic/Cnat_total_order.con".
314 inline "cic:/CoRN/algebra/CLogic/Codd.ind".
316 inline "cic:/CoRN/algebra/CLogic/Codd_even_to.con".
318 inline "cic:/CoRN/algebra/CLogic/Codd_to.con".
320 inline "cic:/CoRN/algebra/CLogic/Ceven_to.con".
322 inline "cic:/CoRN/algebra/CLogic/to_Codd_even.con".
324 inline "cic:/CoRN/algebra/CLogic/to_Codd.con".
326 inline "cic:/CoRN/algebra/CLogic/to_Ceven.con".
339 inline "cic:/CoRN/algebra/CLogic/CZ_exh.con".
341 inline "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con".
343 inline "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con".
345 inline "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con".
347 inline "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con".
349 inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
355 (*#* **Results about the natural numbers
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
364 inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con".
366 inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con".
369 Implicit Arguments nat_less_n_pred [n].
373 Implicit Arguments nat_less_n_pred' [n].
377 Section Odd_and_Even.
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:
386 inline "cic:/CoRN/algebra/CLogic/even_plus_n_n.con".
388 inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con".
390 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
393 inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con".
400 Hint Resolve even_plus_n_n: arith.
404 Hint Resolve toCle: core.
408 Section Natural_Numbers.
411 (*#* **Algebraic Properties
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.
419 inline "cic:/CoRN/algebra/CLogic/Clt_le_weak.con".
421 inline "cic:/CoRN/algebra/CLogic/lt_5.con".
423 inline "cic:/CoRN/algebra/CLogic/lt_8.con".
425 inline "cic:/CoRN/algebra/CLogic/pred_lt.con".
427 inline "cic:/CoRN/algebra/CLogic/lt_10.con".
429 inline "cic:/CoRN/algebra/CLogic/lt_pred'.con".
431 inline "cic:/CoRN/algebra/CLogic/le_1.con".
433 inline "cic:/CoRN/algebra/CLogic/le_2.con".
435 inline "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con".
437 inline "cic:/CoRN/algebra/CLogic/not_not_lt.con".
439 inline "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con".
441 (*#* We now prove some properties of functions on the natural numbers.
443 %\begin{convention}% Let [H:nat->nat].
447 inline "cic:/CoRN/algebra/CLogic/h.var".
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.
455 inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con".
457 inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con".
459 (*#* A strictly increasing function is injective: *)
461 inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con".
463 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
465 inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con".
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.
474 inline "cic:/CoRN/algebra/CLogic/mon_fun_covers.con".
476 inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
483 Useful for the Fundamental Theorem of Algebra.
486 inline "cic:/CoRN/algebra/CLogic/kseq_prop.con".
489 Section Predicates_to_CProp.
492 (*#* **Logical Properties
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:
500 inline "cic:/CoRN/algebra/CLogic/even_induction.con".
502 inline "cic:/CoRN/algebra/CLogic/odd_induction.con".
504 inline "cic:/CoRN/algebra/CLogic/four_induction.con".
506 inline "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con".
508 inline "cic:/CoRN/algebra/CLogic/odd_double_ind.con".
510 (*#* For subsetoid predicates in the natural numbers we can eliminate
511 disjunction (and existential quantification) as follows.
514 inline "cic:/CoRN/algebra/CLogic/finite_or_elim.con".
516 inline "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con".
519 End Predicates_to_CProp.
523 Section Predicates_to_Prop.
526 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
530 inline "cic:/CoRN/algebra/CLogic/even_ind.con".
532 inline "cic:/CoRN/algebra/CLogic/odd_ind.con".
534 inline "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con".
536 inline "cic:/CoRN/algebra/CLogic/four_ind.con".
539 End Predicates_to_Prop.
544 Similar results for integers.
550 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
555 inline "cic:/CoRN/algebra/CLogic/Zlts.con".
557 inline "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con".
559 inline "cic:/CoRN/algebra/CLogic/CZlt_to.con".
561 inline "cic:/CoRN/algebra/CLogic/Zsgn_1.con".
563 inline "cic:/CoRN/algebra/CLogic/Zsgn_2.con".
565 inline "cic:/CoRN/algebra/CLogic/Zsgn_3.con".
567 (*#* The following have unusual names, in line with the series of lemmata in
571 inline "cic:/CoRN/algebra/CLogic/ZL4'.con".
573 inline "cic:/CoRN/algebra/CLogic/ZL9.con".
575 inline "cic:/CoRN/algebra/CLogic/Zsgn_4.con".
577 inline "cic:/CoRN/algebra/CLogic/Zsgn_5.con".
579 inline "cic:/CoRN/algebra/CLogic/nat_nat_pos.con".
581 inline "cic:/CoRN/algebra/CLogic/S_predn.con".
583 inline "cic:/CoRN/algebra/CLogic/absolu_1.con".
585 inline "cic:/CoRN/algebra/CLogic/absolu_2.con".
587 inline "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con".
589 inline "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con".
591 inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".