helm/software/matita/contribs/CoRN-Procedural/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".
  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".
  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 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/I.var".
  89
  90 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/F.var".
  91
  92 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var".
  93
  94 (* begin hide *)
  95
  96 inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__".
  97
  98 inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__".
  99
 100 (* end hide *)
 101
 102 alias id "R" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/R.var".
 103
 104 (*#*
 105 We start with two lemmas which make it much easier to prove and use
 106 this definition:
 107 *)
 108
 109 inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con".
 110
 111 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con".
 112
 113 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con".
 114
 115 (* UNEXPORTED
 116 End Equality_Results
 117 *)
 118
 119 (* UNEXPORTED
 120 Hint Resolve included_IR : included.
 121 *)
 122
 123 (* UNEXPORTED
 124 Section Some_More
 125 *)
 126
 127 (*#*
 128 If two function coincide on a given subset then they coincide in any smaller subset.
 129 *)
 130
 131 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con".
 132
 133 (* UNEXPORTED
 134 End Some_More
 135 *)
 136
 137 (* UNEXPORTED
 138 Section Away_from_Zero
 139 *)
 140
 141 (* UNEXPORTED
 142 Section Definitions
 143 *)
 144
 145 (*#* **Away from Zero
 146
 147 Before we prove our main results about the equality we have to do some
 148 work on division.  A function is said to be bounded away from zero in
 149 a set if there exists a positive lower bound for the set of absolute
 150 values of its image of that set.
 151
 152 %\begin{convention}% Let [I : IR->CProp], [F : PartIR] and denote by [P]
 153 the domain of [F].
 154 %\end{convention}%
 155 *)
 156
 157 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/I.var".
 158
 159 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var".
 160
 161 (* begin hide *)
 162
 163 inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__".
 164
 165 (* end hide *)
 166
 167 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con".
 168
 169 (*#*
 170 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].
 171 *)
 172
 173 (* begin show *)
 174
 175 alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var".
 176
 177 (* end show *)
 178
 179 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con".
 180
 181 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con".
 182
 183 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con".
 184
 185 (* UNEXPORTED
 186 End Definitions
 187 *)
 188
 189 (*#*
 190 Boundedness away from zero is preserved through restriction of the set.
 191
 192 %\begin{convention}% Let [F] be a partial function and [P, Q] be predicates.
 193 %\end{convention}%
 194 *)
 195
 196 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/F.var".
 197
 198 alias id "P" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var".
 199
 200 alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var".
 201
 202 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con".
 203
 204 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con".
 205
 206 (*#*
 207 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.
 208 *)
 209
 210 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con".
 211
 212 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con".
 213
 214 (*#*
 215 An immediate consequence:
 216 *)
 217
 218 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con".
 219
 220 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con".
 221
 222 (* UNEXPORTED
 223 End Away_from_Zero
 224 *)
 225
 226 (* UNEXPORTED
 227 Hint Resolve bnd_imp_inc_recip bnd_imp_inc_div: included.
 228 *)
 229
 230 (* UNEXPORTED
 231 Hint Immediate bnd_in_P_imp_ap_zero: included.
 232 *)
 233
 234 (*#* ** The [FEQ] tactic
 235 This tactic splits a goal of the form [Feq I F G] into the three subgoals
 236 [included I (Dom F)], [included I (Dom G)] and [forall x, F x [=] G x]
 237 and applies [Included] to the first two and [rational] to the third.
 238 *)
 239
 240 (* begin hide *)
 241
 242 (* UNEXPORTED
 243 Ltac FEQ := apply eq_imp_Feq;
 244    [ Included | Included | intros; try (simpl in |- *; rational) ].
 245 *)
 246
 247 (* end hide *)
 248
 249 (* UNEXPORTED
 250 Section More_on_Equality
 251 *)
 252
 253 (*#* **Properties of Equality
 254
 255 We are now finally able to prove the main properties of the equality relation.  We begin by showing it to be an equivalence relation.
 256
 257 %\begin{convention}% Let [I] be a predicate and [F, F', G, G', H] be
 258 partial functions.
 259 %\end{convention}%
 260 *)
 261
 262 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/I.var".
 263
 264 (* UNEXPORTED
 265 Section Feq_Equivalence
 266 *)
 267
 268 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/F.var".
 269
 270 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G.var".
 271
 272 alias id "H" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var".
 273
 274 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con".
 275
 276 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con".
 277
 278 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con".
 279
 280 (* UNEXPORTED
 281 End Feq_Equivalence
 282 *)
 283
 284 (* UNEXPORTED
 285 Section Operations
 286 *)
 287
 288 (*#*
 289 Also it is preserved through application of functional constructors and restriction.
 290 *)
 291
 292 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F.var".
 293
 294 alias id "F'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F'.var".
 295
 296 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var".
 297
 298 alias id "G'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var".
 299
 300 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con".
 301
 302 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con".
 303
 304 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con".
 305
 306 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con".
 307
 308 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con".
 309
 310 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con".
 311
 312 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con".
 313
 314 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con".
 315
 316 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con".
 317
 318 (*#*
 319 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.
 320
 321 The restriction of a function is well defined.
 322 *)
 323
 324 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con".
 325
 326 (*#*
 327 The image of a set is extensional.
 328 *)
 329
 330 inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con".
 331
 332 (* UNEXPORTED
 333 End Operations
 334 *)
 335
 336 (* UNEXPORTED
 337 End More_on_Equality
 338 *)
 339
 340 (* UNEXPORTED
 341 Section Nth_Power
 342 *)
 343
 344 (*#* **Nth Power
 345
 346 We finish this group of lemmas with characterization results for the
 347 power function (similar to those already proved for arbitrary rings).
 348 The characterization is done at first pointwise and later using the
 349 equality relation.
 350
 351 %\begin{convention}% Let [F] be a partial function with domain [P] and
 352 [Q] be a predicate on the real numbers assumed to be included in [P].
 353 %\end{convention}%
 354 *)
 355
 356 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var".
 357
 358 (* begin hide *)
 359
 360 inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__".
 361
 362 (* end hide *)
 363
 364 alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Q.var".
 365
 366 alias id "H" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var".
 367
 368 alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var".
 369
 370 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con".
 371
 372 alias id "n" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var".
 373
 374 alias id "H'" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var".
 375
 376 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con".
 377
 378 (* UNEXPORTED
 379 End Nth_Power
 380 *)
 381
 382 (* UNEXPORTED
 383 Section Strong_Nth_Power
 384 *)
 385
 386 (*#*
 387 %\begin{convention}% Let [a,b] be real numbers such that [I := [a,b]]
 388 is included in the domain of [F].
 389 %\end{convention}%
 390 *)
 391
 392 alias id "a" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/a.var".
 393
 394 alias id "b" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/b.var".
 395
 396 alias id "Hab" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var".
 397
 398 (* begin hide *)
 399
 400 inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__".
 401
 402 (* end hide *)
 403
 404 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var".
 405
 406 alias id "incF" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var".
 407
 408 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con".
 409
 410 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con".
 411
 412 (* UNEXPORTED
 413 End Strong_Nth_Power
 414 *)
 415