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 *********************)
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}% *)
39 include "algebra/Basics.ma".
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)
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] .
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].
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.
64 Existential quantification will similarly always return a value in [CProp].
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].
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.
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
79 inline procedural "cic:/CoRN/algebra/CLogic/CProp.con" as definition.
86 Here we treat conversion from [Prop] to [CProp] and vice versa,
87 and some basic connectives in [CProp].
90 inline procedural "cic:/CoRN/algebra/CLogic/Not.con" as definition.
92 inline procedural "cic:/CoRN/algebra/CLogic/CAnd.ind".
94 inline procedural "cic:/CoRN/algebra/CLogic/Iff.con" as definition.
96 inline procedural "cic:/CoRN/algebra/CLogic/CFalse.ind".
98 inline procedural "cic:/CoRN/algebra/CLogic/CTrue.ind".
100 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sigT.con" as definition.
102 inline procedural "cic:/CoRN/algebra/CLogic/proj2_sigT.con" as definition.
104 inline procedural "cic:/CoRN/algebra/CLogic/sig2T.ind".
106 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sig2T.con" as definition.
108 inline procedural "cic:/CoRN/algebra/CLogic/proj2a_sig2T.con" as definition.
110 inline procedural "cic:/CoRN/algebra/CLogic/proj2b_sig2T.con" as definition.
112 inline procedural "cic:/CoRN/algebra/CLogic/toCProp.ind".
114 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_e.con" as lemma.
116 inline procedural "cic:/CoRN/algebra/CLogic/CNot.con" as definition.
118 inline procedural "cic:/CoRN/algebra/CLogic/Ccontrapos'.con" as lemma.
120 inline procedural "cic:/CoRN/algebra/CLogic/COr.ind".
123 Some lemmas to make it possible to use [Step] when reasoning with
127 Infix "IFF" := Iff (at level 60, right associativity).
130 inline procedural "cic:/CoRN/algebra/CLogic/Iff_left.con" as lemma.
132 inline procedural "cic:/CoRN/algebra/CLogic/Iff_right.con" as lemma.
134 inline procedural "cic:/CoRN/algebra/CLogic/Iff_refl.con" as lemma.
136 inline procedural "cic:/CoRN/algebra/CLogic/Iff_sym.con" as lemma.
138 inline procedural "cic:/CoRN/algebra/CLogic/Iff_trans.con" as lemma.
140 inline procedural "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con" as lemma.
143 Declare Right Step Iff_right.
147 Declare Left Step Iff_left.
151 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
161 Infix "or" := COr (at level 85, right associativity).
165 Infix "and" := CAnd (at level 80, right associativity).
170 inline procedural "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con" as lemma.
172 inline procedural "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con" as lemma.
177 Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp)
178 (at level 0, x at level 99) : type_scope.
182 Notation "{ x : A | P | Q }" :=
183 (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
193 Variables P,Q:A->Prop.
194 Variables X,Y:A->CProp.
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)}.
207 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
215 Let [P] be a predicate on $\NN^2$#N times N#.
218 alias id "P" = "cic:/CoRN/algebra/CLogic/Choice/P.var".
220 inline procedural "cic:/CoRN/algebra/CLogic/choice.con" as lemma.
227 Section Logical_Remarks
230 (*#* We prove a few logical results which are helpful to have as lemmas
231 when [A], [B] and [C] are non trivial.
234 inline procedural "cic:/CoRN/algebra/CLogic/CNot_Not_or.con" as lemma.
236 inline procedural "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con" as lemma.
243 Section CRelation_Definition
246 (*#* ** [CProp]-valued Relations
247 Similar to Relations.v in Coq's standard library.
249 %\begin{convention}% Let [A:Type] and [R:Crelation].
253 alias id "A" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/A.var".
255 inline procedural "cic:/CoRN/algebra/CLogic/Crelation.con" as definition.
257 alias id "R" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/R.var".
259 inline procedural "cic:/CoRN/algebra/CLogic/Creflexive.con" as definition.
261 inline procedural "cic:/CoRN/algebra/CLogic/Ctransitive.con" as definition.
263 inline procedural "cic:/CoRN/algebra/CLogic/Csymmetric.con" as definition.
265 inline procedural "cic:/CoRN/algebra/CLogic/Cequiv.con" as definition.
268 End CRelation_Definition
272 Section TRelation_Definition
275 (*#* ** [Prop]-valued Relations
278 %\begin{convention}% Let [A:Type] and [R:Trelation].
282 alias id "A" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/A.var".
284 inline procedural "cic:/CoRN/algebra/CLogic/Trelation.con" as definition.
286 alias id "R" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/R.var".
288 inline procedural "cic:/CoRN/algebra/CLogic/Treflexive.con" as definition.
290 inline procedural "cic:/CoRN/algebra/CLogic/Ttransitive.con" as definition.
292 inline procedural "cic:/CoRN/algebra/CLogic/Tsymmetric.con" as definition.
294 inline procedural "cic:/CoRN/algebra/CLogic/Tequiv.con" as definition.
297 End TRelation_Definition
300 inline procedural "cic:/CoRN/algebra/CLogic/eqs.ind".
306 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
309 inline procedural "cic:/CoRN/algebra/CLogic/Cle.ind".
311 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con" as theorem.
313 inline procedural "cic:/CoRN/algebra/CLogic/my_Cle_ind.con" as theorem.
315 inline procedural "cic:/CoRN/algebra/CLogic/Cle_n_S.con" as theorem.
317 inline procedural "cic:/CoRN/algebra/CLogic/toCle.con" as lemma.
323 inline procedural "cic:/CoRN/algebra/CLogic/Cle_to.con" as lemma.
325 inline procedural "cic:/CoRN/algebra/CLogic/Clt.con" as definition.
327 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_lt.con" as lemma.
329 inline procedural "cic:/CoRN/algebra/CLogic/Clt_to.con" as lemma.
331 inline procedural "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con" as lemma.
333 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_total_order.con" as lemma.
335 inline procedural "cic:/CoRN/algebra/CLogic/Codd.ind".
337 inline procedural "cic:/CoRN/algebra/CLogic/Codd_even_to.con" as lemma.
339 inline procedural "cic:/CoRN/algebra/CLogic/Codd_to.con" as lemma.
341 inline procedural "cic:/CoRN/algebra/CLogic/Ceven_to.con" as lemma.
343 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd_even.con" as lemma.
345 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd.con" as lemma.
347 inline procedural "cic:/CoRN/algebra/CLogic/to_Ceven.con" as lemma.
360 inline procedural "cic:/CoRN/algebra/CLogic/CZ_exh.con" as lemma.
362 inline procedural "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con" as lemma.
364 inline procedural "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con" as lemma.
366 inline procedural "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con" as lemma.
368 inline procedural "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con" as lemma.
370 inline procedural "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con" as lemma.
376 (*#* **Results about the natural numbers
378 We now define a class of predicates on a finite subset of natural
379 numbers that will be important throughout all our work. Essentially,
380 these are simply setoid predicates, but for clarity we will never
381 write them in that form but we will single out the preservation of the
385 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con" as definition.
387 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con" as definition.
390 Implicit Arguments nat_less_n_pred [n].
394 Implicit Arguments nat_less_n_pred' [n].
402 For our work we will many times need to distinguish cases between even or odd numbers.
403 We begin by proving that this case distinction is decidable.
404 Next, we prove the usual results about sums of even and odd numbers:
407 inline procedural "cic:/CoRN/algebra/CLogic/even_plus_n_n.con" as lemma.
409 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con" as lemma.
411 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
414 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con" as lemma.
421 Hint Resolve even_plus_n_n: arith.
425 Hint Resolve toCle: core.
429 Section Natural_Numbers
432 (*#* **Algebraic Properties
434 We now present a series of trivial things proved with [Omega] that are
435 stated as lemmas to make proofs shorter and to aid in auxiliary
436 definitions. Giving a name to these results allows us to use them in
437 definitions keeping conciseness.
440 inline procedural "cic:/CoRN/algebra/CLogic/Clt_le_weak.con" as lemma.
442 inline procedural "cic:/CoRN/algebra/CLogic/lt_5.con" as lemma.
444 inline procedural "cic:/CoRN/algebra/CLogic/lt_8.con" as lemma.
446 inline procedural "cic:/CoRN/algebra/CLogic/pred_lt.con" as lemma.
448 inline procedural "cic:/CoRN/algebra/CLogic/lt_10.con" as lemma.
450 inline procedural "cic:/CoRN/algebra/CLogic/lt_pred'.con" as lemma.
452 inline procedural "cic:/CoRN/algebra/CLogic/le_1.con" as lemma.
454 inline procedural "cic:/CoRN/algebra/CLogic/le_2.con" as lemma.
456 inline procedural "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con" as lemma.
458 inline procedural "cic:/CoRN/algebra/CLogic/not_not_lt.con" as lemma.
460 inline procedural "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con" as lemma.
462 (*#* We now prove some properties of functions on the natural numbers.
464 %\begin{convention}% Let [H:nat->nat].
468 alias id "h" = "cic:/CoRN/algebra/CLogic/Natural_Numbers/h.var".
471 First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
472 for every natural number [n] then [h] is monotonous. An analogous result
473 holds for weak monotonicity.
476 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con" as lemma.
478 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con" as lemma.
480 (*#* A strictly increasing function is injective: *)
482 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con" as lemma.
484 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
486 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con" as lemma.
489 The last lemmas in this section state that a monotonous function in the
490 natural numbers completely covers the natural numbers, that is, for every
491 natural number [n] there is an [i] such that [h(i) <= n<(n+1) <= h(i+1)].
492 These are useful for integration.
495 inline procedural "cic:/CoRN/algebra/CLogic/mon_fun_covers.con" as lemma.
497 inline procedural "cic:/CoRN/algebra/CLogic/weird_mon_covers.con" as lemma.
504 Useful for the Fundamental Theorem of Algebra.
507 inline procedural "cic:/CoRN/algebra/CLogic/kseq_prop.con" as lemma.
510 Section Predicates_to_CProp
513 (*#* **Logical Properties
515 This section contains lemmas that aid in logical reasoning with
516 natural numbers. First, we present some principles of induction, both
517 for [CProp]- and [Prop]-valued predicates. We begin by presenting the
518 results for [CProp]-valued predicates:
521 inline procedural "cic:/CoRN/algebra/CLogic/even_induction.con" as lemma.
523 inline procedural "cic:/CoRN/algebra/CLogic/odd_induction.con" as lemma.
525 inline procedural "cic:/CoRN/algebra/CLogic/four_induction.con" as lemma.
527 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con" as lemma.
529 inline procedural "cic:/CoRN/algebra/CLogic/odd_double_ind.con" as lemma.
531 (*#* For subsetoid predicates in the natural numbers we can eliminate
532 disjunction (and existential quantification) as follows.
535 inline procedural "cic:/CoRN/algebra/CLogic/finite_or_elim.con" as lemma.
537 inline procedural "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con" as lemma.
540 End Predicates_to_CProp
544 Section Predicates_to_Prop
547 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
551 inline procedural "cic:/CoRN/algebra/CLogic/even_ind.con" as lemma.
553 inline procedural "cic:/CoRN/algebra/CLogic/odd_ind.con" as lemma.
555 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con" as lemma.
557 inline procedural "cic:/CoRN/algebra/CLogic/four_ind.con" as lemma.
560 End Predicates_to_Prop
565 Similar results for integers.
571 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
576 inline procedural "cic:/CoRN/algebra/CLogic/Zlts.con" as definition.
578 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con" as lemma.
580 inline procedural "cic:/CoRN/algebra/CLogic/CZlt_to.con" as lemma.
582 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_1.con" as lemma.
584 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_2.con" as lemma.
586 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_3.con" as lemma.
588 (*#* The following have unusual names, in line with the series of lemmata in
592 inline procedural "cic:/CoRN/algebra/CLogic/ZL4'.con" as lemma.
594 inline procedural "cic:/CoRN/algebra/CLogic/ZL9.con" as lemma.
596 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_4.con" as theorem.
598 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_5.con" as theorem.
600 inline procedural "cic:/CoRN/algebra/CLogic/nat_nat_pos.con" as lemma.
602 inline procedural "cic:/CoRN/algebra/CLogic/S_predn.con" as theorem.
604 inline procedural "cic:/CoRN/algebra/CLogic/absolu_1.con" as lemma.
606 inline procedural "cic:/CoRN/algebra/CLogic/absolu_2.con" as lemma.
608 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con" as lemma.
610 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con" as lemma.
612 inline procedural "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con" as lemma.
615 Notation ProjT1 := (proj1_sigT _ _).
619 Notation ProjT2 := (proj2_sigT _ _).