helm/software/matita/contribs/procedural/CoRN/ftc/MoreIntervals.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
  20
  21 include "ftc/NthDerivative.ma".
  22
  23 (* UNEXPORTED
  24 Opaque Min Max.
  25 *)
  26
  27 (* UNEXPORTED
  28 Section Intervals
  29 *)
  30
  31 (*#* printing realline %\ensuremath{\RR}% #(-&infin;,+&infin;)# *)
  32
  33 (*#* printing openl %\ensuremath{(\cdot,+\infty)}% #(&sdot;,+&infin;)# *)
  34
  35 (*#* printing openr %\ensuremath{(-\infty,\cdot)}% #(-&infin;,&sdot;)# *)
  36
  37 (*#* printing closel %\ensuremath{[\cdot,+\infty)}% #[&sdot;,+&infin;)# *)
  38
  39 (*#* printing closer %\ensuremath{(-\infty,\cdot]}% #(-&infin;,&sdot;]# *)
  40
  41 (*#* printing olor %\ensuremath{(\cdot,\cdot)}% #(&sdot;,&sdot;)# *)
  42
  43 (*#* printing clor %\ensuremath{[\cdot,\cdot)}% #[&sdot;,&sdot;)# *)
  44
  45 (*#* printing olcr %\ensuremath{(\cdot,\cdot]}% #(&sdot;,&sdot;]# *)
  46
  47 (*#* printing clcr %\ensuremath{[\cdot,\cdot]}% #[&sdot;,&sdot;]# *)
  48
  49 (*#* *Generalized Intervals
  50
  51 At this stage we have enough material to begin generalizing our
  52 concepts in preparation for the fundamental theorem of calculus and
  53 the definition of the main (non-polynomial) functions of analysis.
  54
  55 In order to define functions via power series (or any other kind of
  56 series) we need to formalize a notion of convergence more general than
  57 the one we already have on compact intervals.  This is necessary for
  58 practical reasons: we want to define a single exponential function
  59 with domain [IR], not several exponential functions defined on compact
  60 intervals which we prove to be the same wherever their domains
  61 overlap.  In a similar way, we want to define indefinite integrals on
  62 infinite domains and not only on compact intervals.
  63
  64 Unfortunately, proceeding in a way analogous to how we defined the
  65 concept of global continuity will lead us nowhere; the concept turns
  66 out to be to general, and the behaviour on too small domains
  67 (typically intervals [[a,a']] where [a [=] a'] is neither
  68 provably true nor provably false) will be unsatisfactory.
  69
  70 There is a special family of sets, however, where this problems can be
  71 avoided: intervals.  Intervals have some nice properties that allow us
  72 to prove good results, namely the facts that if [a] and [b] are
  73 elements of an interval [I] then so are [Min(a,b)] and
  74 [Max(a,b)] (which is in general not true) and also the
  75 compact interval [[a,b]] is included in [I].  Furthermore, all
  76 intervals are characterized by simple, well defined predicates, and
  77 the nonempty and proper concepts become very easy to define.
  78
  79 **Definitions and Basic Results
  80
  81 We define an inductive type of intervals with nine constructors,
  82 corresponding to the nine basic types of intervals.  The reason why so
  83 many constructors are needed is that we do not have a notion of real
  84 line, for many reasons which we will not discuss here.  Also it seems
  85 simple to directly define finite intervals than to define then later
  86 as intersections of infinite intervals, as it would only mess things
  87 up.
  88
  89 The compact interval which we will define here is obviously the same
  90 that we have been working with all the way through; why, then, the
  91 different formulation?  The reason is simple: if we had worked with
  92 intervals from the beginning we would have had case definitions at
  93 every spot, and our lemmas and proofs would have been very awkward.
  94 Also, it seems more natural to characterize a compact interval by two
  95 real numbers (and a proof) than as a particular case of a more general
  96 concept which doesn't have an intuitive interpretation.  Finally, the
  97 definitions we will make here will have the elegant consequence that
  98 from this point on we can work with any kind of intervals in exactly
  99 the same way.
 100 *)
 101
 102 inline procedural "cic:/CoRN/ftc/MoreIntervals/interval.ind".
 103
 104 (*#*
 105 To each interval a predicate (set) is assigned by the following map:
 106 *)
 107
 108 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop.con" as definition.
 109
 110 (* begin hide *)
 111
 112 (* COERCION
 113 cic:/matita/CoRN-Procedural/ftc/MoreIntervals/iprop.con
 114 *)
 115
 116 (* end hide *)
 117
 118 (*#*
 119 This map is made into a coercion, so that intervals
 120 %\emph{%#<i>#are%}%#</i># really subsets of reals.
 121
 122 We now define what it means for an interval to be nonvoid, proper,
 123 finite and compact in the obvious way.
 124 *)
 125
 126 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid.con" as definition.
 127
 128 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper.con" as definition.
 129
 130 inline procedural "cic:/CoRN/ftc/MoreIntervals/finite.con" as definition.
 131
 132 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_.con" as definition.
 133
 134 (*#* Finite intervals have a left end and a right end. *)
 135
 136 inline procedural "cic:/CoRN/ftc/MoreIntervals/left_end.con" as definition.
 137
 138 inline procedural "cic:/CoRN/ftc/MoreIntervals/right_end.con" as definition.
 139
 140 (*#*
 141 Some trivia: compact intervals are finite; proper intervals are nonvoid; an interval is nonvoid iff it contains some point.
 142 *)
 143
 144 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_finite.con" as lemma.
 145
 146 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con" as lemma.
 147
 148 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con" as lemma.
 149
 150 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_char.con" as lemma.
 151
 152 (*#*
 153 For practical reasons it helps to define left end and right end of compact intervals.
 154 *)
 155
 156 inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend.con" as definition.
 157
 158 inline procedural "cic:/CoRN/ftc/MoreIntervals/Rend.con" as definition.
 159
 160 (*#* In a compact interval, the left end is always less than or equal
 161 to the right end.
 162 *)
 163
 164 inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con" as lemma.
 165
 166 (*#*
 167 Some nice characterizations of inclusion:
 168 *)
 169
 170 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_included.con" as lemma.
 171
 172 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval'.con" as lemma.
 173
 174 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval.con" as lemma.
 175
 176 (*#*
 177 A weirder inclusion result.
 178 *)
 179
 180 inline procedural "cic:/CoRN/ftc/MoreIntervals/included3_interval.con" as lemma.
 181
 182 (*#*
 183 Finally, all intervals are characterized by well defined predicates.
 184 *)
 185
 186 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con" as lemma.
 187
 188 (* UNEXPORTED
 189 End Intervals
 190 *)
 191
 192 (* UNEXPORTED
 193 Implicit Arguments Lend [I].
 194 *)
 195
 196 (* UNEXPORTED
 197 Implicit Arguments Rend [I].
 198 *)
 199
 200 (* UNEXPORTED
 201 Section Compact_Constructions
 202 *)
 203
 204 (* UNEXPORTED
 205 Section Single_Compact_Interval
 206 *)
 207
 208 (*#* **Constructions with Compact Intervals
 209
 210 Several important constructions are now discussed.
 211
 212 We begin by defining the compact interval [[x,x]].
 213
 214 %\begin{convention}% Let [P:IR->CProp] be well defined, and [x:IR]
 215 such that [P(x)] holds.
 216 %\end{convention}%
 217 *)
 218
 219 (* UNEXPORTED
 220 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var
 221 *)
 222
 223 (* UNEXPORTED
 224 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var
 225 *)
 226
 227 (* UNEXPORTED
 228 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var
 229 *)
 230
 231 (* UNEXPORTED
 232 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var
 233 *)
 234
 235 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single.con" as definition.
 236
 237 (*#*
 238 This interval contains [x] and only (elements equal to) [x]; furthermore, for every (well-defined) [P], if $x\in P$#x&isin;P# then $[x,x]\subseteq P$#[x,x]&sube;P#.
 239 *)
 240
 241 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con" as lemma.
 242
 243 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con" as lemma.
 244
 245 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con" as lemma.
 246
 247 (* UNEXPORTED
 248 End Single_Compact_Interval
 249 *)
 250
 251 (*#*
 252 The special case of intervals is worth singling out, as one of the hypothesis becomes a theorem.
 253 *)
 254
 255 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_iprop.con" as definition.
 256
 257 (*#*
 258 Now for more interesting and important results.
 259
 260 Let [I] be a proper interval and [x] be a point of [I].  Then there is
 261 a proper compact interval [[a,b]] such that $x\in[a,b]\subseteq
 262 I$#x&isin;[a,b]&sube;I#.
 263 *)
 264
 265 (* UNEXPORTED
 266 Section Proper_Compact_with_One_or_Two_Points
 267 *)
 268
 269 (* begin hide *)
 270
 271 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 272
 273 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 274
 275 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 276
 277 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 278
 279 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 280
 281 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 282
 283 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 284
 285 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 286
 287 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 288
 289 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 290
 291 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 292
 293 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
 294
 295 (* end hide *)
 296
 297 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con" as definition.
 298
 299 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con" as lemma.
 300
 301 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con" as lemma.
 302
 303 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con" as lemma.
 304
 305 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval.con" as lemma.
 306
 307 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval.con" as lemma.
 308
 309 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval'.con" as lemma.
 310
 311 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con" as lemma.
 312
 313 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc2.con" as lemma.
 314
 315 (*#*
 316 If [x [=] y] then the construction yields the same interval whether we
 317 use [x] or [y] in its definition.  This property is required at some
 318 stage, which is why we formalized this result as a functional
 319 definition rather than as an existential formula.
 320 *)
 321
 322 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con" as lemma.
 323
 324 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd2.con" as lemma.
 325
 326 (*#*
 327 We can make an analogous construction for two points.
 328 *)
 329
 330 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con" as definition.
 331
 332 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con" as lemma.
 333
 334 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con" as lemma.
 335
 336 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con" as lemma.
 337
 338 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con" as lemma.
 339
 340 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con" as lemma.
 341
 342 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con" as lemma.
 343
 344 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con" as lemma.
 345
 346 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con" as lemma.
 347
 348 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con" as lemma.
 349
 350 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con" as lemma.
 351
 352 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con" as lemma.
 353
 354 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con" as lemma.
 355
 356 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con" as lemma.
 357
 358 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con" as lemma.
 359
 360 (* UNEXPORTED
 361 End Proper_Compact_with_One_or_Two_Points
 362 *)
 363
 364 (*#*
 365 Compact intervals are exactly compact intervals(!).
 366 *)
 367
 368 inline procedural "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con" as lemma.
 369
 370 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_interval_inc.con" as lemma.
 371
 372 (*#*
 373 A generalization of the previous results: if $[a,b]\subseteq J$#[a,b]&sube;J#
 374 and [J] is proper, then we can find a proper interval [[a',b']] such that
 375 $[a,b]\subseteq[a',b']\subseteq J$#[a,b]&sube;[a',b']&sube;J#.
 376 *)
 377
 378 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con" as lemma.
 379
 380 (* UNEXPORTED
 381 End Compact_Constructions
 382 *)
 383
 384 (* UNEXPORTED
 385 Section Functions
 386 *)
 387
 388 (*#* **Properties of Functions in Intervals
 389
 390 We now define notions of continuity, differentiability and so on on
 391 arbitrary intervals.  As expected, a function [F] has property [P] in
 392 the (proper) interval [I] iff it has property [P] in every compact
 393 interval included in [I].  We can formalize this in a nice way using
 394 previously defined concepts.
 395
 396 %\begin{convention}% Let [n:nat] and [I:interval].
 397 %\end{convention}%
 398 *)
 399
 400 (* UNEXPORTED
 401 cic:/CoRN/ftc/MoreIntervals/Functions/n.var
 402 *)
 403
 404 (* UNEXPORTED
 405 cic:/CoRN/ftc/MoreIntervals/Functions/I.var
 406 *)
 407
 408 inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous.con" as definition.
 409
 410 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative.con" as definition.
 411
 412 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble.con" as definition.
 413
 414 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con" as definition.
 415
 416 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con" as definition.
 417
 418 (* UNEXPORTED
 419 End Functions
 420 *)
 421
 422 (* UNEXPORTED
 423 Section Reflexivity_Properties
 424 *)
 425
 426 (*#*
 427 In the case of compact intervals, this definitions collapse to the old ones.
 428 *)
 429
 430 inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con" as lemma.
 431
 432 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con" as lemma.
 433
 434 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con" as lemma.
 435
 436 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con" as lemma.
 437
 438 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con" as lemma.
 439
 440 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con" as lemma.
 441
 442 (* UNEXPORTED
 443 End Reflexivity_Properties
 444 *)
 445
 446 (* UNEXPORTED
 447 Section Lemmas
 448 *)
 449
 450 (*#*
 451 Interestingly, inclusion and equality in an interval are also characterizable in a similar way:
 452 *)
 453
 454 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con" as lemma.
 455
 456 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con" as lemma.
 457
 458 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con" as lemma.
 459
 460 (* UNEXPORTED
 461 End Lemmas
 462 *)
 463
 464 (* UNEXPORTED
 465 Hint Resolve included_interval included_interval' included3_interval
 466   compact_single_inc compact_single_iprop included_compact_in_interval
 467   iprop_compact_in_interval_inc1 iprop_compact_in_interval_inc2
 468   included_compact_in_interval2 iprop_compact_in_interval2_inc1
 469   iprop_compact_in_interval2_inc2 interval_compact_inc compact_interval_inc
 470   iprop_wd: included.
 471 *)
 472