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