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