matita/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 include "CoRN.ma".
  20
  21 (* $Id: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
  22
  23 include "ftc/NthDerivative.ma".
  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 coercion cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con 0 (* compounds *).
 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 "cic:/CoRN/ftc/MoreIntervals/nonvoid.con".
 127
 128 inline "cic:/CoRN/ftc/MoreIntervals/proper.con".
 129
 130 inline "cic:/CoRN/ftc/MoreIntervals/finite.con".
 131
 132 inline "cic:/CoRN/ftc/MoreIntervals/compact_.con".
 133
 134 (*#* Finite intervals have a left end and a right end. *)
 135
 136 inline "cic:/CoRN/ftc/MoreIntervals/left_end.con".
 137
 138 inline "cic:/CoRN/ftc/MoreIntervals/right_end.con".
 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 "cic:/CoRN/ftc/MoreIntervals/compact_finite.con".
 145
 146 inline "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con".
 147
 148 inline "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con".
 149
 150 inline "cic:/CoRN/ftc/MoreIntervals/nonvoid_char.con".
 151
 152 (*#*
 153 For practical reasons it helps to define left end and right end of compact intervals.
 154 *)
 155
 156 inline "cic:/CoRN/ftc/MoreIntervals/Lend.con".
 157
 158 inline "cic:/CoRN/ftc/MoreIntervals/Rend.con".
 159
 160 (*#* In a compact interval, the left end is always less than or equal
 161 to the right end.
 162 *)
 163
 164 inline "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con".
 165
 166 (*#*
 167 Some nice characterizations of inclusion:
 168 *)
 169
 170 inline "cic:/CoRN/ftc/MoreIntervals/compact_included.con".
 171
 172 inline "cic:/CoRN/ftc/MoreIntervals/included_interval'.con".
 173
 174 inline "cic:/CoRN/ftc/MoreIntervals/included_interval.con".
 175
 176 (*#*
 177 A weirder inclusion result.
 178 *)
 179
 180 inline "cic:/CoRN/ftc/MoreIntervals/included3_interval.con".
 181
 182 (*#*
 183 Finally, all intervals are characterized by well defined predicates.
 184 *)
 185
 186 inline "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con".
 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 alias id "P" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var".
 220
 221 alias id "wdP" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var".
 222
 223 alias id "x" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var".
 224
 225 alias id "Hx" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var".
 226
 227 inline "cic:/CoRN/ftc/MoreIntervals/compact_single.con".
 228
 229 (*#*
 230 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#.
 231 *)
 232
 233 inline "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con".
 234
 235 inline "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con".
 236
 237 inline "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con".
 238
 239 (* UNEXPORTED
 240 End Single_Compact_Interval
 241 *)
 242
 243 (*#*
 244 The special case of intervals is worth singling out, as one of the hypothesis becomes a theorem.
 245 *)
 246
 247 inline "cic:/CoRN/ftc/MoreIntervals/compact_single_iprop.con".
 248
 249 (*#*
 250 Now for more interesting and important results.
 251
 252 Let [I] be a proper interval and [x] be a point of [I].  Then there is
 253 a proper compact interval [[a,b]] such that $x\in[a,b]\subseteq
 254 I$#x&isin;[a,b]&sube;I#.
 255 *)
 256
 257 (* UNEXPORTED
 258 Section Proper_Compact_with_One_or_Two_Points
 259 *)
 260
 261 (* begin hide *)
 262
 263 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__".
 264
 265 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__".
 266
 267 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__".
 268
 269 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__".
 270
 271 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__".
 272
 273 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__".
 274
 275 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__".
 276
 277 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__".
 278
 279 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__".
 280
 281 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__".
 282
 283 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__".
 284
 285 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__".
 286
 287 (* end hide *)
 288
 289 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con".
 290
 291 inline "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con".
 292
 293 inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con".
 294
 295 inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con".
 296
 297 inline "cic:/CoRN/ftc/MoreIntervals/included_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'.con".
 302
 303 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con".
 304
 305 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc2.con".
 306
 307 (*#*
 308 If [x [=] y] then the construction yields the same interval whether we
 309 use [x] or [y] in its definition.  This property is required at some
 310 stage, which is why we formalized this result as a functional
 311 definition rather than as an existential formula.
 312 *)
 313
 314 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con".
 315
 316 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd2.con".
 317
 318 (*#*
 319 We can make an analogous construction for two points.
 320 *)
 321
 322 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con".
 323
 324 inline "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con".
 325
 326 inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con".
 327
 328 inline "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con".
 329
 330 inline "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con".
 331
 332 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con".
 333
 334 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con".
 335
 336 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con".
 337
 338 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con".
 339
 340 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con".
 341
 342 inline "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con".
 343
 344 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con".
 345
 346 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con".
 347
 348 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con".
 349
 350 inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con".
 351
 352 (* UNEXPORTED
 353 End Proper_Compact_with_One_or_Two_Points
 354 *)
 355
 356 (*#*
 357 Compact intervals are exactly compact intervals(!).
 358 *)
 359
 360 inline "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con".
 361
 362 inline "cic:/CoRN/ftc/MoreIntervals/compact_interval_inc.con".
 363
 364 (*#*
 365 A generalization of the previous results: if $[a,b]\subseteq J$#[a,b]&sube;J#
 366 and [J] is proper, then we can find a proper interval [[a',b']] such that
 367 $[a,b]\subseteq[a',b']\subseteq J$#[a,b]&sube;[a',b']&sube;J#.
 368 *)
 369
 370 inline "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con".
 371
 372 (* UNEXPORTED
 373 End Compact_Constructions
 374 *)
 375
 376 (* UNEXPORTED
 377 Section Functions
 378 *)
 379
 380 (*#* **Properties of Functions in Intervals
 381
 382 We now define notions of continuity, differentiability and so on on
 383 arbitrary intervals.  As expected, a function [F] has property [P] in
 384 the (proper) interval [I] iff it has property [P] in every compact
 385 interval included in [I].  We can formalize this in a nice way using
 386 previously defined concepts.
 387
 388 %\begin{convention}% Let [n:nat] and [I:interval].
 389 %\end{convention}%
 390 *)
 391
 392 alias id "n" = "cic:/CoRN/ftc/MoreIntervals/Functions/n.var".
 393
 394 alias id "I" = "cic:/CoRN/ftc/MoreIntervals/Functions/I.var".
 395
 396 inline "cic:/CoRN/ftc/MoreIntervals/Continuous.con".
 397
 398 inline "cic:/CoRN/ftc/MoreIntervals/Derivative.con".
 399
 400 inline "cic:/CoRN/ftc/MoreIntervals/Diffble.con".
 401
 402 inline "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con".
 403
 404 inline "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con".
 405
 406 (* UNEXPORTED
 407 End Functions
 408 *)
 409
 410 (* UNEXPORTED
 411 Section Reflexivity_Properties
 412 *)
 413
 414 (*#*
 415 In the case of compact intervals, this definitions collapse to the old ones.
 416 *)
 417
 418 inline "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con".
 419
 420 inline "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con".
 421
 422 inline "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con".
 423
 424 inline "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con".
 425
 426 inline "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con".
 427
 428 inline "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con".
 429
 430 (* UNEXPORTED
 431 End Reflexivity_Properties
 432 *)
 433
 434 (* UNEXPORTED
 435 Section Lemmas
 436 *)
 437
 438 (*#*
 439 Interestingly, inclusion and equality in an interval are also characterizable in a similar way:
 440 *)
 441
 442 inline "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con".
 443
 444 inline "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con".
 445
 446 inline "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con".
 447
 448 (* UNEXPORTED
 449 End Lemmas
 450 *)
 451
 452 (* UNEXPORTED
 453 Hint Resolve included_interval included_interval' included3_interval
 454   compact_single_inc compact_single_iprop included_compact_in_interval
 455   iprop_compact_in_interval_inc1 iprop_compact_in_interval_inc2
 456   included_compact_in_interval2 iprop_compact_in_interval2_inc1
 457   iprop_compact_in_interval2_inc2 interval_compact_inc compact_interval_inc
 458   iprop_wd: included.
 459 *)
 460