helm/software/matita/contribs/CoRN-Procedural/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".
 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".
 127
 128 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper.con".
 129
 130 inline procedural "cic:/CoRN/ftc/MoreIntervals/finite.con".
 131
 132 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_.con".
 133
 134 (*#* Finite intervals have a left end and a right end. *)
 135
 136 inline procedural "cic:/CoRN/ftc/MoreIntervals/left_end.con".
 137
 138 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/compact_finite.con".
 145
 146 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con".
 147
 148 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con".
 149
 150 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/Lend.con".
 157
 158 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con".
 165
 166 (*#*
 167 Some nice characterizations of inclusion:
 168 *)
 169
 170 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_included.con".
 171
 172 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval'.con".
 173
 174 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval.con".
 175
 176 (*#*
 177 A weirder inclusion result.
 178 *)
 179
 180 inline procedural "cic:/CoRN/ftc/MoreIntervals/included3_interval.con".
 181
 182 (*#*
 183 Finally, all intervals are characterized by well defined predicates.
 184 *)
 185
 186 inline procedural "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 procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con".
 234
 235 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con".
 236
 237 inline procedural "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 procedural "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 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__".
 264
 265 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__".
 266
 267 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__".
 268
 269 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__".
 270
 271 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__".
 272
 273 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__".
 274
 275 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__".
 276
 277 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__".
 278
 279 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__".
 280
 281 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__".
 282
 283 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__".
 284
 285 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__".
 286
 287 (* end hide *)
 288
 289 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con".
 290
 291 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con".
 292
 293 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con".
 294
 295 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con".
 296
 297 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval.con".
 298
 299 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval.con".
 300
 301 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval'.con".
 302
 303 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con".
 304
 305 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con".
 315
 316 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con".
 323
 324 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con".
 325
 326 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con".
 327
 328 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con".
 329
 330 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con".
 331
 332 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con".
 333
 334 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con".
 335
 336 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con".
 337
 338 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con".
 339
 340 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con".
 341
 342 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con".
 343
 344 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con".
 345
 346 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con".
 347
 348 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con".
 349
 350 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con".
 361
 362 inline procedural "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 procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/Continuous.con".
 397
 398 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative.con".
 399
 400 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble.con".
 401
 402 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con".
 403
 404 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con".
 419
 420 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con".
 421
 422 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con".
 423
 424 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con".
 425
 426 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con".
 427
 428 inline procedural "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 procedural "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con".
 443
 444 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con".
 445
 446 inline procedural "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