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
129 Infix "IFF" := Iff (at level 60, right associativity).
132 inline "cic:/CoRN/algebra/CLogic/Iff_left.con".
134 inline "cic:/CoRN/algebra/CLogic/Iff_right.con".
136 inline "cic:/CoRN/algebra/CLogic/Iff_refl.con".
138 inline "cic:/CoRN/algebra/CLogic/Iff_sym.con".
140 inline "cic:/CoRN/algebra/CLogic/Iff_trans.con".
142 inline "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con".
145 Declare Right Step Iff_right.
149 Declare Left Step Iff_left.
153 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
163 Infix "or" := COr (at level 85, right associativity).
167 Infix "and" := CAnd (at level 80, right associativity).
172 inline "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con".
174 inline "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con".
179 Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp)
180 (at level 0, x at level 99) : type_scope.
184 Notation "{ x : A | P | Q }" :=
185 (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
195 Variables P,Q:A->Prop.
196 Variables X,Y:A->CProp.
200 Check {x:A | (X x) | (Y x)}.
201 Check {x:A | (P x) | (Q x)}.
202 Check {x:A | (P x) | (X x)}.
203 Check {x:A | (X x) | (P x)}.
209 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
217 Let [P] be a predicate on $\NN^2$#N times N#.
220 inline "cic:/CoRN/algebra/CLogic/P.var".
222 inline "cic:/CoRN/algebra/CLogic/choice.con".
229 Section Logical_Remarks.
232 (*#* We prove a few logical results which are helpful to have as lemmas
233 when [A], [B] and [C] are non trivial.
236 inline "cic:/CoRN/algebra/CLogic/CNot_Not_or.con".
238 inline "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con".
245 Section CRelation_Definition.
248 (*#* ** [CProp]-valued Relations
249 Similar to Relations.v in Coq's standard library.
251 %\begin{convention}% Let [A:Type] and [R:Crelation].
255 inline "cic:/CoRN/algebra/CLogic/A.var".
257 inline "cic:/CoRN/algebra/CLogic/Crelation.con".
259 inline "cic:/CoRN/algebra/CLogic/R.var".
261 inline "cic:/CoRN/algebra/CLogic/Creflexive.con".
263 inline "cic:/CoRN/algebra/CLogic/Ctransitive.con".
265 inline "cic:/CoRN/algebra/CLogic/Csymmetric.con".
267 inline "cic:/CoRN/algebra/CLogic/Cequiv.con".
270 End CRelation_Definition.
274 Section TRelation_Definition.
277 (*#* ** [Prop]-valued Relations
280 %\begin{convention}% Let [A:Type] and [R:Trelation].
284 inline "cic:/CoRN/algebra/CLogic/A.var".
286 inline "cic:/CoRN/algebra/CLogic/Trelation.con".
288 inline "cic:/CoRN/algebra/CLogic/R.var".
290 inline "cic:/CoRN/algebra/CLogic/Treflexive.con".
292 inline "cic:/CoRN/algebra/CLogic/Ttransitive.con".
294 inline "cic:/CoRN/algebra/CLogic/Tsymmetric.con".
296 inline "cic:/CoRN/algebra/CLogic/Tequiv.con".
299 End TRelation_Definition.
302 inline "cic:/CoRN/algebra/CLogic/eqs.ind".
308 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
311 inline "cic:/CoRN/algebra/CLogic/Cle.ind".
313 inline "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con".
315 inline "cic:/CoRN/algebra/CLogic/my_Cle_ind.con".
317 inline "cic:/CoRN/algebra/CLogic/Cle_n_S.con".
319 inline "cic:/CoRN/algebra/CLogic/toCle.con".
325 inline "cic:/CoRN/algebra/CLogic/Cle_to.con".
327 inline "cic:/CoRN/algebra/CLogic/Clt.con".
329 inline "cic:/CoRN/algebra/CLogic/toCProp_lt.con".
331 inline "cic:/CoRN/algebra/CLogic/Clt_to.con".
333 inline "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con".
335 inline "cic:/CoRN/algebra/CLogic/Cnat_total_order.con".
337 inline "cic:/CoRN/algebra/CLogic/Codd.ind".
339 inline "cic:/CoRN/algebra/CLogic/Codd_even_to.con".
341 inline "cic:/CoRN/algebra/CLogic/Codd_to.con".
343 inline "cic:/CoRN/algebra/CLogic/Ceven_to.con".
345 inline "cic:/CoRN/algebra/CLogic/to_Codd_even.con".
347 inline "cic:/CoRN/algebra/CLogic/to_Codd.con".
349 inline "cic:/CoRN/algebra/CLogic/to_Ceven.con".
362 inline "cic:/CoRN/algebra/CLogic/CZ_exh.con".
364 inline "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con".
366 inline "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con".
368 inline "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con".
370 inline "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con".
372 inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
378 (*#* **Results about the natural numbers
380 We now define a class of predicates on a finite subset of natural
381 numbers that will be important throughout all our work. Essentially,
382 these are simply setoid predicates, but for clarity we will never
383 write them in that form but we will single out the preservation of the
387 inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con".
389 inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con".
392 Implicit Arguments nat_less_n_pred [n].
396 Implicit Arguments nat_less_n_pred' [n].
400 Section Odd_and_Even.
404 For our work we will many times need to distinguish cases between even or odd numbers.
405 We begin by proving that this case distinction is decidable.
406 Next, we prove the usual results about sums of even and odd numbers:
409 inline "cic:/CoRN/algebra/CLogic/even_plus_n_n.con".
411 inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con".
413 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
416 inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con".
423 Hint Resolve even_plus_n_n: arith.
427 Hint Resolve toCle: core.
431 Section Natural_Numbers.
434 (*#* **Algebraic Properties
436 We now present a series of trivial things proved with [Omega] that are
437 stated as lemmas to make proofs shorter and to aid in auxiliary
438 definitions. Giving a name to these results allows us to use them in
439 definitions keeping conciseness.
442 inline "cic:/CoRN/algebra/CLogic/Clt_le_weak.con".
444 inline "cic:/CoRN/algebra/CLogic/lt_5.con".
446 inline "cic:/CoRN/algebra/CLogic/lt_8.con".
448 inline "cic:/CoRN/algebra/CLogic/pred_lt.con".
450 inline "cic:/CoRN/algebra/CLogic/lt_10.con".
452 inline "cic:/CoRN/algebra/CLogic/lt_pred'.con".
454 inline "cic:/CoRN/algebra/CLogic/le_1.con".
456 inline "cic:/CoRN/algebra/CLogic/le_2.con".
458 inline "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con".
460 inline "cic:/CoRN/algebra/CLogic/not_not_lt.con".
462 inline "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con".
464 (*#* We now prove some properties of functions on the natural numbers.
466 %\begin{convention}% Let [H:nat->nat].
470 inline "cic:/CoRN/algebra/CLogic/h.var".
473 First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
474 for every natural number [n] then [h] is monotonous. An analogous result
475 holds for weak monotonicity.
478 inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con".
480 inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con".
482 (*#* A strictly increasing function is injective: *)
484 inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con".
486 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
488 inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con".
491 The last lemmas in this section state that a monotonous function in the
492 natural numbers completely covers the natural numbers, that is, for every
493 natural number [n] there is an [i] such that [h(i) <= n<(n+1) <= h(i+1)].
494 These are useful for integration.
497 inline "cic:/CoRN/algebra/CLogic/mon_fun_covers.con".
499 inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
506 Useful for the Fundamental Theorem of Algebra.
509 inline "cic:/CoRN/algebra/CLogic/kseq_prop.con".
512 Section Predicates_to_CProp.
515 (*#* **Logical Properties
517 This section contains lemmas that aid in logical reasoning with
518 natural numbers. First, we present some principles of induction, both
519 for [CProp]- and [Prop]-valued predicates. We begin by presenting the
520 results for [CProp]-valued predicates:
523 inline "cic:/CoRN/algebra/CLogic/even_induction.con".
525 inline "cic:/CoRN/algebra/CLogic/odd_induction.con".
527 inline "cic:/CoRN/algebra/CLogic/four_induction.con".
529 inline "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con".
531 inline "cic:/CoRN/algebra/CLogic/odd_double_ind.con".
533 (*#* For subsetoid predicates in the natural numbers we can eliminate
534 disjunction (and existential quantification) as follows.
537 inline "cic:/CoRN/algebra/CLogic/finite_or_elim.con".
539 inline "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con".
542 End Predicates_to_CProp.
546 Section Predicates_to_Prop.
549 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
553 inline "cic:/CoRN/algebra/CLogic/even_ind.con".
555 inline "cic:/CoRN/algebra/CLogic/odd_ind.con".
557 inline "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con".
559 inline "cic:/CoRN/algebra/CLogic/four_ind.con".
562 End Predicates_to_Prop.
567 Similar results for integers.
573 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
578 inline "cic:/CoRN/algebra/CLogic/Zlts.con".
580 inline "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con".
582 inline "cic:/CoRN/algebra/CLogic/CZlt_to.con".
584 inline "cic:/CoRN/algebra/CLogic/Zsgn_1.con".
586 inline "cic:/CoRN/algebra/CLogic/Zsgn_2.con".
588 inline "cic:/CoRN/algebra/CLogic/Zsgn_3.con".
590 (*#* The following have unusual names, in line with the series of lemmata in
594 inline "cic:/CoRN/algebra/CLogic/ZL4'.con".
596 inline "cic:/CoRN/algebra/CLogic/ZL9.con".
598 inline "cic:/CoRN/algebra/CLogic/Zsgn_4.con".
600 inline "cic:/CoRN/algebra/CLogic/Zsgn_5.con".
602 inline "cic:/CoRN/algebra/CLogic/nat_nat_pos.con".
604 inline "cic:/CoRN/algebra/CLogic/S_predn.con".
606 inline "cic:/CoRN/algebra/CLogic/absolu_1.con".
608 inline "cic:/CoRN/algebra/CLogic/absolu_2.con".
610 inline "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con".
612 inline "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con".
614 inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".
617 Notation ProjT1 := (proj1_sigT _ _).
621 Notation ProjT2 := (proj2_sigT _ _).