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".
19 (* $Id: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *)
21 (*#* printing Not %\ensuremath\neg% #~# *)
23 (*#* printing CNot %\ensuremath\neg% #~# *)
25 (*#* printing Iff %\ensuremath\Leftrightarrow% #⇔# *)
27 (*#* printing CFalse %\ensuremath\bot% #⊥# *)
29 (*#* printing False %\ensuremath\bot% #⊥# *)
31 (*#* printing CTrue %\ensuremath\top% *)
33 (*#* printing True %\ensuremath\top% *)
35 (*#* printing or %\ensuremath{\mathrel\vee}% *)
37 (*#* printing and %\ensuremath{\mathrel\wedge}% *)
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)
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] .
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].
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.
86 Existential quantification will similarly always return a value in [CProp].
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].
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.
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
101 inline cic:/CoRN/algebra/CLogic/CProp.con.
108 Here we treat conversion from [Prop] to [CProp] and vice versa,
109 and some basic connectives in [CProp].
112 inline cic:/CoRN/algebra/CLogic/Not.con.
114 inline cic:/CoRN/algebra/CLogic/CAnd.ind.
116 inline cic:/CoRN/algebra/CLogic/Iff.con.
118 inline cic:/CoRN/algebra/CLogic/CFalse.ind.
120 inline cic:/CoRN/algebra/CLogic/CTrue.ind.
122 inline cic:/CoRN/algebra/CLogic/proj1_sigT.con.
124 inline cic:/CoRN/algebra/CLogic/proj2_sigT.con.
126 inline cic:/CoRN/algebra/CLogic/sig2T.ind.
128 inline cic:/CoRN/algebra/CLogic/proj1_sig2T.con.
130 inline cic:/CoRN/algebra/CLogic/proj2a_sig2T.con.
132 inline cic:/CoRN/algebra/CLogic/proj2b_sig2T.con.
134 inline cic:/CoRN/algebra/CLogic/toCProp.ind.
136 inline cic:/CoRN/algebra/CLogic/toCProp_e.con.
138 inline cic:/CoRN/algebra/CLogic/CNot.con.
140 inline cic:/CoRN/algebra/CLogic/Ccontrapos'.con.
142 inline cic:/CoRN/algebra/CLogic/COr.ind.
145 Some lemmas to make it possible to use [Step] when reasoning with
148 inline cic:/CoRN/algebra/CLogic/Iff_left.con.
150 inline cic:/CoRN/algebra/CLogic/Iff_right.con.
152 inline cic:/CoRN/algebra/CLogic/Iff_refl.con.
154 inline cic:/CoRN/algebra/CLogic/Iff_sym.con.
156 inline cic:/CoRN/algebra/CLogic/Iff_trans.con.
158 inline cic:/CoRN/algebra/CLogic/Iff_imp_imp.con.
161 Declare Right Step Iff_right.
165 Declare Left Step Iff_left.
169 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
180 inline cic:/CoRN/algebra/CLogic/not_r_cor_rect.con.
182 inline cic:/CoRN/algebra/CLogic/not_l_cor_rect.con.
192 Variables P,Q:A->Prop.
193 Variables X,Y:A->CProp.
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)}.
206 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
214 Let [P] be a predicate on $\NN^2$#N times N#.
217 inline cic:/CoRN/algebra/CLogic/P.var.
219 inline cic:/CoRN/algebra/CLogic/choice.con.
226 Section Logical_Remarks.
229 (*#* We prove a few logical results which are helpful to have as lemmas
230 when [A], [B] and [C] are non trivial.
233 inline cic:/CoRN/algebra/CLogic/CNot_Not_or.con.
235 inline cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con.
242 Section CRelation_Definition.
245 (*#* ** [CProp]-valued Relations
246 Similar to Relations.v in Coq's standard library.
248 %\begin{convention}% Let [A:Type] and [R:Crelation].
252 inline cic:/CoRN/algebra/CLogic/A.var.
254 inline cic:/CoRN/algebra/CLogic/Crelation.con.
256 inline cic:/CoRN/algebra/CLogic/R.var.
258 inline cic:/CoRN/algebra/CLogic/Creflexive.con.
260 inline cic:/CoRN/algebra/CLogic/Ctransitive.con.
262 inline cic:/CoRN/algebra/CLogic/Csymmetric.con.
264 inline cic:/CoRN/algebra/CLogic/Cequiv.con.
267 End CRelation_Definition.
271 Section TRelation_Definition.
274 (*#* ** [Prop]-valued Relations
277 %\begin{convention}% Let [A:Type] and [R:Trelation].
281 inline cic:/CoRN/algebra/CLogic/A.var.
283 inline cic:/CoRN/algebra/CLogic/Trelation.con.
285 inline cic:/CoRN/algebra/CLogic/R.var.
287 inline cic:/CoRN/algebra/CLogic/Treflexive.con.
289 inline cic:/CoRN/algebra/CLogic/Ttransitive.con.
291 inline cic:/CoRN/algebra/CLogic/Tsymmetric.con.
293 inline cic:/CoRN/algebra/CLogic/Tequiv.con.
296 End TRelation_Definition.
299 inline cic:/CoRN/algebra/CLogic/eqs.ind.
305 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
308 inline cic:/CoRN/algebra/CLogic/Cle.ind.
310 inline cic:/CoRN/algebra/CLogic/Cnat_double_ind.con.
312 inline cic:/CoRN/algebra/CLogic/my_Cle_ind.con.
314 inline cic:/CoRN/algebra/CLogic/Cle_n_S.con.
316 inline cic:/CoRN/algebra/CLogic/toCle.con.
322 inline cic:/CoRN/algebra/CLogic/Cle_to.con.
324 inline cic:/CoRN/algebra/CLogic/Clt.con.
326 inline cic:/CoRN/algebra/CLogic/toCProp_lt.con.
328 inline cic:/CoRN/algebra/CLogic/Clt_to.con.
330 inline cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con.
332 inline cic:/CoRN/algebra/CLogic/Cnat_total_order.con.
334 inline cic:/CoRN/algebra/CLogic/Codd.ind.
336 inline cic:/CoRN/algebra/CLogic/Codd_even_to.con.
338 inline cic:/CoRN/algebra/CLogic/Codd_to.con.
340 inline cic:/CoRN/algebra/CLogic/Ceven_to.con.
342 inline cic:/CoRN/algebra/CLogic/to_Codd_even.con.
344 inline cic:/CoRN/algebra/CLogic/to_Codd.con.
346 inline cic:/CoRN/algebra/CLogic/to_Ceven.con.
359 inline cic:/CoRN/algebra/CLogic/CZ_exh.con.
361 inline cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con.
363 inline cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con.
365 inline cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con.
367 inline cic:/CoRN/algebra/CLogic/not_r_sum_rec.con.
369 inline cic:/CoRN/algebra/CLogic/not_l_sum_rec.con.
375 (*#* **Results about the natural numbers
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
384 inline cic:/CoRN/algebra/CLogic/nat_less_n_pred.con.
386 inline cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con.
389 Implicit Arguments nat_less_n_pred [n].
393 Implicit Arguments nat_less_n_pred' [n].
397 Section Odd_and_Even.
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:
406 inline cic:/CoRN/algebra/CLogic/even_plus_n_n.con.
408 inline cic:/CoRN/algebra/CLogic/even_or_odd_plus.con.
410 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
413 inline cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con.
420 Hint Resolve even_plus_n_n: arith.
424 Hint Resolve toCle: core.
428 Section Natural_Numbers.
431 (*#* **Algebraic Properties
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.
439 inline cic:/CoRN/algebra/CLogic/Clt_le_weak.con.
441 inline cic:/CoRN/algebra/CLogic/lt_5.con.
443 inline cic:/CoRN/algebra/CLogic/lt_8.con.
445 inline cic:/CoRN/algebra/CLogic/pred_lt.con.
447 inline cic:/CoRN/algebra/CLogic/lt_10.con.
449 inline cic:/CoRN/algebra/CLogic/lt_pred'.con.
451 inline cic:/CoRN/algebra/CLogic/le_1.con.
453 inline cic:/CoRN/algebra/CLogic/le_2.con.
455 inline cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con.
457 inline cic:/CoRN/algebra/CLogic/not_not_lt.con.
459 inline cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con.
461 (*#* We now prove some properties of functions on the natural numbers.
463 %\begin{convention}% Let [H:nat->nat].
467 inline cic:/CoRN/algebra/CLogic/h.var.
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.
475 inline cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con.
477 inline cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con.
479 (*#* A strictly increasing function is injective: *)
481 inline cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con.
483 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
485 inline cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con.
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.
494 inline cic:/CoRN/algebra/CLogic/mon_fun_covers.con.
496 inline cic:/CoRN/algebra/CLogic/weird_mon_covers.con.
503 Useful for the Fundamental Theorem of Algebra.
506 inline cic:/CoRN/algebra/CLogic/kseq_prop.con.
509 Section Predicates_to_CProp.
512 (*#* **Logical Properties
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:
520 inline cic:/CoRN/algebra/CLogic/even_induction.con.
522 inline cic:/CoRN/algebra/CLogic/odd_induction.con.
524 inline cic:/CoRN/algebra/CLogic/four_induction.con.
526 inline cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con.
528 inline cic:/CoRN/algebra/CLogic/odd_double_ind.con.
530 (*#* For subsetoid predicates in the natural numbers we can eliminate
531 disjunction (and existential quantification) as follows.
534 inline cic:/CoRN/algebra/CLogic/finite_or_elim.con.
536 inline cic:/CoRN/algebra/CLogic/str_finite_or_elim.con.
539 End Predicates_to_CProp.
543 Section Predicates_to_Prop.
546 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
550 inline cic:/CoRN/algebra/CLogic/even_ind.con.
552 inline cic:/CoRN/algebra/CLogic/odd_ind.con.
554 inline cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con.
556 inline cic:/CoRN/algebra/CLogic/four_ind.con.
559 End Predicates_to_Prop.
564 Similar results for integers.
570 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
575 inline cic:/CoRN/algebra/CLogic/Zlts.con.
577 inline cic:/CoRN/algebra/CLogic/toCProp_Zlt.con.
579 inline cic:/CoRN/algebra/CLogic/CZlt_to.con.
581 inline cic:/CoRN/algebra/CLogic/Zsgn_1.con.
583 inline cic:/CoRN/algebra/CLogic/Zsgn_2.con.
585 inline cic:/CoRN/algebra/CLogic/Zsgn_3.con.
587 (*#* The following have unusual names, in line with the series of lemmata in
591 inline cic:/CoRN/algebra/CLogic/ZL4'.con.
593 inline cic:/CoRN/algebra/CLogic/ZL9.con.
595 inline cic:/CoRN/algebra/CLogic/Zsgn_4.con.
597 inline cic:/CoRN/algebra/CLogic/Zsgn_5.con.
599 inline cic:/CoRN/algebra/CLogic/nat_nat_pos.con.
601 inline cic:/CoRN/algebra/CLogic/S_predn.con.
603 inline cic:/CoRN/algebra/CLogic/absolu_1.con.
605 inline cic:/CoRN/algebra/CLogic/absolu_2.con.
607 inline cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con.
609 inline cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con.
611 inline cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con.