helm/software/matita/contribs/procedural/CoRN/ftc/PartFunEquality.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: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *)
  20
  21 (*#* printing Feq %\ensuremath{\approx}% #&asymp;# *)
  22
  23 include "reals/Intervals.ma".
  24
  25 include "tactics/DiffTactics1.ma".
  26
  27 (* UNEXPORTED
  28 Section Definitions
  29 *)
  30
  31 (*#* *Equality of Partial Functions
  32
  33 ** Definitions
  34
  35 In some contexts (namely when quantifying over partial functions) we
  36 need to refer explicitly to the subsetoid of elements satisfying a
  37 given predicate rather than to the predicate itself.  The following
  38 definition makes this possible.
  39 *)
  40
  41 inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con" as definition.
  42
  43 (*#*
  44 The core of our work will revolve around the following fundamental
  45 notion: two functions are equal in a given domain (predicate) iff they
  46 coincide on every point of that domain#. #%\footnote{%Notice that,
  47 according to our definition of partial function, it is equivalent to
  48 prove the equality for every proof or for a specific proof.  Typically
  49 it is easier to consider a generic case%.}%.  This file is concerned
  50 with proving the main properties of this equality relation.
  51 *)
  52
  53 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con" as definition.
  54
  55 (*#*
  56 Notice that, because the quantification over the proofs is universal,
  57 we must require explicitly that the predicate be included in the
  58 domain of each function; otherwise the basic properties of equality
  59 (like, for example, transitivity) would fail to hold#. #%\footnote{%To
  60 see this it is enough to realize that the empty function would be
  61 equal to every other function in every domain.%}.% The way to
  62 circumvent this would be to quantify existentially over the proofs;
  63 this, however, would have two major disadvantages: first, proofs of
  64 equality would become very cumbersome and clumsy; secondly (and most
  65 important), we often need to prove the inclusions from an equality
  66 hypothesis, and this definition allows us to do it in a very easy way.
  67 Also, the pointwise equality is much nicer to use from this definition
  68 than in an existentially quantified one.
  69 *)
  70
  71 (* UNEXPORTED
  72 End Definitions
  73 *)
  74
  75 (* UNEXPORTED
  76 Section Equality_Results
  77 *)
  78
  79 (*#* **Properties of Inclusion
  80
  81 We will now prove the main properties of the equality relation.
  82
  83 %\begin{convention}% Let [I,R:IR->CProp] and [F,G:PartIR], and denote
  84 by [P] and [Q], respectively, the domains of [F] and [G].
  85 %\end{convention}%
  86 *)
  87
  88 (* UNEXPORTED
  89 cic:/CoRN/ftc/PartFunEquality/Equality_Results/I.var
  90 *)
  91
  92 (* UNEXPORTED
  93 cic:/CoRN/ftc/PartFunEquality/Equality_Results/F.var
  94 *)
  95
  96 (* UNEXPORTED
  97 cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var
  98 *)
  99
 100 (* begin hide *)
 101
 102 inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__" as definition.
 103
 104 inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__" as definition.
 105
 106 (* end hide *)
 107
 108 (* UNEXPORTED
 109 cic:/CoRN/ftc/PartFunEquality/Equality_Results/R.var
 110 *)
 111
 112 (*#*
 113 We start with two lemmas which make it much easier to prove and use
 114 this definition:
 115 *)
 116
 117 inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con" as lemma.
 120
 121 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con" as lemma.
 122
 123 (* UNEXPORTED
 124 End Equality_Results
 125 *)
 126
 127 (* UNEXPORTED
 128 Hint Resolve included_IR : included.
 129 *)
 130
 131 (* UNEXPORTED
 132 Section Some_More
 133 *)
 134
 135 (*#*
 136 If two function coincide on a given subset then they coincide in any smaller subset.
 137 *)
 138
 139 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con" as lemma.
 140
 141 (* UNEXPORTED
 142 End Some_More
 143 *)
 144
 145 (* UNEXPORTED
 146 Section Away_from_Zero
 147 *)
 148
 149 (* UNEXPORTED
 150 Section Definitions
 151 *)
 152
 153 (*#* **Away from Zero
 154
 155 Before we prove our main results about the equality we have to do some
 156 work on division.  A function is said to be bounded away from zero in
 157 a set if there exists a positive lower bound for the set of absolute
 158 values of its image of that set.
 159
 160 %\begin{convention}% Let [I : IR->CProp], [F : PartIR] and denote by [P]
 161 the domain of [F].
 162 %\end{convention}%
 163 *)
 164
 165 (* UNEXPORTED
 166 cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/I.var
 167 *)
 168
 169 (* UNEXPORTED
 170 cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var
 171 *)
 172
 173 (* begin hide *)
 174
 175 inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__" as definition.
 176
 177 (* end hide *)
 178
 179 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con" as definition.
 180
 181 (*#*
 182 If [F] is bounded away from zero in [I] then [F] is necessarily apart from zero in [I]; also this means that [I] is included in the domain of [{1/}F].
 183 *)
 184
 185 (* begin show *)
 186
 187 (* UNEXPORTED
 188 cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var
 189 *)
 190
 191 (* end show *)
 192
 193 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con" as lemma.
 194
 195 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con" as lemma.
 196
 197 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con" as lemma.
 198
 199 (* UNEXPORTED
 200 End Definitions
 201 *)
 202
 203 (*#*
 204 Boundedness away from zero is preserved through restriction of the set.
 205
 206 %\begin{convention}% Let [F] be a partial function and [P, Q] be predicates.
 207 %\end{convention}%
 208 *)
 209
 210 (* UNEXPORTED
 211 cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/F.var
 212 *)
 213
 214 (* UNEXPORTED
 215 cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var
 216 *)
 217
 218 (* UNEXPORTED
 219 cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var
 220 *)
 221
 222 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con" as lemma.
 223
 224 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con" as lemma.
 225
 226 (*#*
 227 A function is said to be bounded away from zero everywhere if it is bounded away from zero in every compact subinterval of its domain; a similar definition is made for arbitrary sets, which will be necessary for future work.
 228 *)
 229
 230 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con" as definition.
 231
 232 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con" as definition.
 233
 234 (*#*
 235 An immediate consequence:
 236 *)
 237
 238 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con" as lemma.
 239
 240 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con" as lemma.
 241
 242 (* UNEXPORTED
 243 End Away_from_Zero
 244 *)
 245
 246 (* UNEXPORTED
 247 Hint Resolve bnd_imp_inc_recip bnd_imp_inc_div: included.
 248 *)
 249
 250 (* UNEXPORTED
 251 Hint Immediate bnd_in_P_imp_ap_zero: included.
 252 *)
 253
 254 (*#* ** The [FEQ] tactic
 255 This tactic splits a goal of the form [Feq I F G] into the three subgoals
 256 [included I (Dom F)], [included I (Dom G)] and [forall x, F x [=] G x]
 257 and applies [Included] to the first two and [rational] to the third.
 258 *)
 259
 260 (* begin hide *)
 261
 262 (* UNEXPORTED
 263 Ltac FEQ := apply eq_imp_Feq;
 264    [ Included | Included | intros; try (simpl in |- *; rational) ].
 265 *)
 266
 267 (* end hide *)
 268
 269 (* UNEXPORTED
 270 Section More_on_Equality
 271 *)
 272
 273 (*#* **Properties of Equality
 274
 275 We are now finally able to prove the main properties of the equality relation.  We begin by showing it to be an equivalence relation.
 276
 277 %\begin{convention}% Let [I] be a predicate and [F, F', G, G', H] be
 278 partial functions.
 279 %\end{convention}%
 280 *)
 281
 282 (* UNEXPORTED
 283 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/I.var
 284 *)
 285
 286 (* UNEXPORTED
 287 Section Feq_Equivalence
 288 *)
 289
 290 (* UNEXPORTED
 291 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/F.var
 292 *)
 293
 294 (* UNEXPORTED
 295 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G.var
 296 *)
 297
 298 (* UNEXPORTED
 299 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var
 300 *)
 301
 302 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con" as lemma.
 303
 304 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con" as lemma.
 305
 306 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con" as lemma.
 307
 308 (* UNEXPORTED
 309 End Feq_Equivalence
 310 *)
 311
 312 (* UNEXPORTED
 313 Section Operations
 314 *)
 315
 316 (*#*
 317 Also it is preserved through application of functional constructors and restriction.
 318 *)
 319
 320 (* UNEXPORTED
 321 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F.var
 322 *)
 323
 324 (* UNEXPORTED
 325 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F'.var
 326 *)
 327
 328 (* UNEXPORTED
 329 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var
 330 *)
 331
 332 (* UNEXPORTED
 333 cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var
 334 *)
 335
 336 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con" as lemma.
 337
 338 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con" as lemma.
 339
 340 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con" as lemma.
 341
 342 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con" as lemma.
 343
 344 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con" as lemma.
 345
 346 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con" as lemma.
 347
 348 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con" as lemma.
 349
 350 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con" as lemma.
 351
 352 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con" as lemma.
 353
 354 (*#*
 355 Notice that in the case of division we only need to require boundedness away from zero for one of the functions (as they are equal); thus the two last lemmas are stated in two different ways, as according to the context one or the other condition may be easier to prove.
 356
 357 The restriction of a function is well defined.
 358 *)
 359
 360 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con" as lemma.
 361
 362 (*#*
 363 The image of a set is extensional.
 364 *)
 365
 366 inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con" as lemma.
 367
 368 (* UNEXPORTED
 369 End Operations
 370 *)
 371
 372 (* UNEXPORTED
 373 End More_on_Equality
 374 *)
 375
 376 (* UNEXPORTED
 377 Section Nth_Power
 378 *)
 379
 380 (*#* **Nth Power
 381
 382 We finish this group of lemmas with characterization results for the
 383 power function (similar to those already proved for arbitrary rings).
 384 The characterization is done at first pointwise and later using the
 385 equality relation.
 386
 387 %\begin{convention}% Let [F] be a partial function with domain [P] and
 388 [Q] be a predicate on the real numbers assumed to be included in [P].
 389 %\end{convention}%
 390 *)
 391
 392 (* UNEXPORTED
 393 cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var
 394 *)
 395
 396 (* begin hide *)
 397
 398 inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__" as definition.
 399
 400 (* end hide *)
 401
 402 (* UNEXPORTED
 403 cic:/CoRN/ftc/PartFunEquality/Nth_Power/Q.var
 404 *)
 405
 406 (* UNEXPORTED
 407 cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var
 408 *)
 409
 410 (* UNEXPORTED
 411 cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var
 412 *)
 413
 414 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con" as lemma.
 415
 416 (* UNEXPORTED
 417 cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var
 418 *)
 419
 420 (* UNEXPORTED
 421 cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var
 422 *)
 423
 424 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con" as lemma.
 425
 426 (* UNEXPORTED
 427 End Nth_Power
 428 *)
 429
 430 (* UNEXPORTED
 431 Section Strong_Nth_Power
 432 *)
 433
 434 (*#*
 435 %\begin{convention}% Let [a,b] be real numbers such that [I := [a,b]]
 436 is included in the domain of [F].
 437 %\end{convention}%
 438 *)
 439
 440 (* UNEXPORTED
 441 cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/a.var
 442 *)
 443
 444 (* UNEXPORTED
 445 cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/b.var
 446 *)
 447
 448 (* UNEXPORTED
 449 cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var
 450 *)
 451
 452 (* begin hide *)
 453
 454 inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__" as definition.
 455
 456 (* end hide *)
 457
 458 (* UNEXPORTED
 459 cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var
 460 *)
 461
 462 (* UNEXPORTED
 463 cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var
 464 *)
 465
 466 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con" as lemma.
 467
 468 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con" as lemma.
 469
 470 (* UNEXPORTED
 471 End Strong_Nth_Power
 472 *)
 473