X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreIntervals.ma;fp=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreIntervals.ma;h=30bf4b4231c2c7d5133e3c5279d9c08eb9ad9658;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma b/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma new file mode 100644 index 000000000..30bf4b423 --- /dev/null +++ b/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma @@ -0,0 +1,460 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntervals". + +include "CoRN.ma". + +(* $Id: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *) + +include "ftc/NthDerivative.ma". + +(* UNEXPORTED +Opaque Min Max. +*) + +(* UNEXPORTED +Section Intervals +*) + +(*#* printing realline %\ensuremath{\RR}% #(-∞,+∞)# *) + +(*#* printing openl %\ensuremath{(\cdot,+\infty)}% #(⋅,+∞)# *) + +(*#* printing openr %\ensuremath{(-\infty,\cdot)}% #(-∞,⋅)# *) + +(*#* printing closel %\ensuremath{[\cdot,+\infty)}% #[⋅,+∞)# *) + +(*#* printing closer %\ensuremath{(-\infty,\cdot]}% #(-∞,⋅]# *) + +(*#* printing olor %\ensuremath{(\cdot,\cdot)}% #(⋅,⋅)# *) + +(*#* printing clor %\ensuremath{[\cdot,\cdot)}% #[⋅,⋅)# *) + +(*#* printing olcr %\ensuremath{(\cdot,\cdot]}% #(⋅,⋅]# *) + +(*#* printing clcr %\ensuremath{[\cdot,\cdot]}% #[⋅,⋅]# *) + +(*#* *Generalized Intervals + +At this stage we have enough material to begin generalizing our +concepts in preparation for the fundamental theorem of calculus and +the definition of the main (non-polynomial) functions of analysis. + +In order to define functions via power series (or any other kind of +series) we need to formalize a notion of convergence more general than +the one we already have on compact intervals. This is necessary for +practical reasons: we want to define a single exponential function +with domain [IR], not several exponential functions defined on compact +intervals which we prove to be the same wherever their domains +overlap. In a similar way, we want to define indefinite integrals on +infinite domains and not only on compact intervals. + +Unfortunately, proceeding in a way analogous to how we defined the +concept of global continuity will lead us nowhere; the concept turns +out to be to general, and the behaviour on too small domains +(typically intervals [[a,a']] where [a [=] a'] is neither +provably true nor provably false) will be unsatisfactory. + +There is a special family of sets, however, where this problems can be +avoided: intervals. Intervals have some nice properties that allow us +to prove good results, namely the facts that if [a] and [b] are +elements of an interval [I] then so are [Min(a,b)] and +[Max(a,b)] (which is in general not true) and also the +compact interval [[a,b]] is included in [I]. Furthermore, all +intervals are characterized by simple, well defined predicates, and +the nonempty and proper concepts become very easy to define. + +**Definitions and Basic Results + +We define an inductive type of intervals with nine constructors, +corresponding to the nine basic types of intervals. The reason why so +many constructors are needed is that we do not have a notion of real +line, for many reasons which we will not discuss here. Also it seems +simple to directly define finite intervals than to define then later +as intersections of infinite intervals, as it would only mess things +up. + +The compact interval which we will define here is obviously the same +that we have been working with all the way through; why, then, the +different formulation? The reason is simple: if we had worked with +intervals from the beginning we would have had case definitions at +every spot, and our lemmas and proofs would have been very awkward. +Also, it seems more natural to characterize a compact interval by two +real numbers (and a proof) than as a particular case of a more general +concept which doesn't have an intuitive interpretation. Finally, the +definitions we will make here will have the elegant consequence that +from this point on we can work with any kind of intervals in exactly +the same way. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/interval.ind". + +(*#* +To each interval a predicate (set) is assigned by the following map: +*) + +inline "cic:/CoRN/ftc/MoreIntervals/iprop.con". + +(* begin hide *) + +coercion cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con 0 (* compounds *). + +(* end hide *) + +(*#* +This map is made into a coercion, so that intervals +%\emph{%##are%}%## really subsets of reals. + +We now define what it means for an interval to be nonvoid, proper, +finite and compact in the obvious way. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/nonvoid.con". + +inline "cic:/CoRN/ftc/MoreIntervals/proper.con". + +inline "cic:/CoRN/ftc/MoreIntervals/finite.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_.con". + +(*#* Finite intervals have a left end and a right end. *) + +inline "cic:/CoRN/ftc/MoreIntervals/left_end.con". + +inline "cic:/CoRN/ftc/MoreIntervals/right_end.con". + +(*#* +Some trivia: compact intervals are finite; proper intervals are nonvoid; an interval is nonvoid iff it contains some point. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_finite.con". + +inline "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con". + +inline "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con". + +inline "cic:/CoRN/ftc/MoreIntervals/nonvoid_char.con". + +(*#* +For practical reasons it helps to define left end and right end of compact intervals. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/Lend.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Rend.con". + +(*#* In a compact interval, the left end is always less than or equal +to the right end. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con". + +(*#* +Some nice characterizations of inclusion: +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_included.con". + +inline "cic:/CoRN/ftc/MoreIntervals/included_interval'.con". + +inline "cic:/CoRN/ftc/MoreIntervals/included_interval.con". + +(*#* +A weirder inclusion result. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/included3_interval.con". + +(*#* +Finally, all intervals are characterized by well defined predicates. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con". + +(* UNEXPORTED +End Intervals +*) + +(* UNEXPORTED +Implicit Arguments Lend [I]. +*) + +(* UNEXPORTED +Implicit Arguments Rend [I]. +*) + +(* UNEXPORTED +Section Compact_Constructions +*) + +(* UNEXPORTED +Section Single_Compact_Interval +*) + +(*#* **Constructions with Compact Intervals + +Several important constructions are now discussed. + +We begin by defining the compact interval [[x,x]]. + +%\begin{convention}% Let [P:IR->CProp] be well defined, and [x:IR] +such that [P(x)] holds. +%\end{convention}% +*) + +alias id "P" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var". + +alias id "wdP" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var". + +alias id "x" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var". + +alias id "Hx" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_single.con". + +(*#* +This interval contains [x] and only (elements equal to) [x]; furthermore, for every (well-defined) [P], if $x\in P$#x∈P# then $[x,x]\subseteq P$#[x,x]⊆P#. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con". + +(* UNEXPORTED +End Single_Compact_Interval +*) + +(*#* +The special case of intervals is worth singling out, as one of the hypothesis becomes a theorem. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_single_iprop.con". + +(*#* +Now for more interesting and important results. + +Let [I] be a proper interval and [x] be a point of [I]. Then there is +a proper compact interval [[a,b]] such that $x\in[a,b]\subseteq +I$#x∈[a,b]⊆I#. +*) + +(* UNEXPORTED +Section Proper_Compact_with_One_or_Two_Points +*) + +(* begin hide *) + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". + +(* end hide *) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con". + +inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con". + +inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con". + +inline "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval'.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc2.con". + +(*#* +If [x [=] y] then the construction yields the same interval whether we +use [x] or [y] in its definition. This property is required at some +stage, which is why we formalized this result as a functional +definition rather than as an existential formula. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd2.con". + +(*#* +We can make an analogous construction for two points. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con". + +inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con". + +inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con". + +inline "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con". + +inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con". + +(* UNEXPORTED +End Proper_Compact_with_One_or_Two_Points +*) + +(*#* +Compact intervals are exactly compact intervals(!). +*) + +inline "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con". + +inline "cic:/CoRN/ftc/MoreIntervals/compact_interval_inc.con". + +(*#* +A generalization of the previous results: if $[a,b]\subseteq J$#[a,b]⊆J# +and [J] is proper, then we can find a proper interval [[a',b']] such that +$[a,b]\subseteq[a',b']\subseteq J$#[a,b]⊆[a',b']⊆J#. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con". + +(* UNEXPORTED +End Compact_Constructions +*) + +(* UNEXPORTED +Section Functions +*) + +(*#* **Properties of Functions in Intervals + +We now define notions of continuity, differentiability and so on on +arbitrary intervals. As expected, a function [F] has property [P] in +the (proper) interval [I] iff it has property [P] in every compact +interval included in [I]. We can formalize this in a nice way using +previously defined concepts. + +%\begin{convention}% Let [n:nat] and [I:interval]. +%\end{convention}% +*) + +alias id "n" = "cic:/CoRN/ftc/MoreIntervals/Functions/n.var". + +alias id "I" = "cic:/CoRN/ftc/MoreIntervals/Functions/I.var". + +inline "cic:/CoRN/ftc/MoreIntervals/Continuous.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Derivative.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Diffble.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con". + +(* UNEXPORTED +End Functions +*) + +(* UNEXPORTED +Section Reflexivity_Properties +*) + +(*#* +In the case of compact intervals, this definitions collapse to the old ones. +*) + +inline "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con". + +inline "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con". + +(* UNEXPORTED +End Reflexivity_Properties +*) + +(* UNEXPORTED +Section Lemmas +*) + +(*#* +Interestingly, inclusion and equality in an interval are also characterizable in a similar way: +*) + +inline "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con". + +inline "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con". + +inline "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con". + +(* UNEXPORTED +End Lemmas +*) + +(* UNEXPORTED +Hint Resolve included_interval included_interval' included3_interval + compact_single_inc compact_single_iprop included_compact_in_interval + iprop_compact_in_interval_inc1 iprop_compact_in_interval_inc2 + included_compact_in_interval2 iprop_compact_in_interval2_inc1 + iprop_compact_in_interval2_inc2 interval_compact_inc compact_interval_inc + iprop_wd: included. +*) +