matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma

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