helm/software/matita/contribs/procedural/CoRN/ftc/IntervalFunct.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: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *)
  20
  21 include "ftc/PartFunEquality.ma".
  22
  23 (* UNEXPORTED
  24 Section Operations
  25 *)
  26
  27 (*#* * Functions with compact domain
  28
  29 In this section we concern ourselves with defining operations on the
  30 set of functions from an arbitrary interval [[a,b]] to [IR].
  31 Although these are a particular kind of partial function, they have
  32 the advantage that, given [a] and [b], they have type [Set] and can
  33 thus be quantified over and extracted from existential hypothesis.
  34 This will be important when we want to define concepts like
  35 differentiability, which involve the existence of an object satisfying
  36 some given properties.
  37
  38 Throughout this section we will focus on a compact interval and define
  39 operators analogous to those we already have for arbitrary partial
  40 functions.
  41
  42 %\begin{convention}% Let [a,b] be real numbers and denote by [I] the
  43 compact interval [[a,b]].  Let [f, g] be setoid functions of
  44 type [I -> IR].
  45 %\end{convention}%
  46 *)
  47
  48 (* UNEXPORTED
  49 cic:/CoRN/ftc/IntervalFunct/Operations/a.var
  50 *)
  51
  52 (* UNEXPORTED
  53 cic:/CoRN/ftc/IntervalFunct/Operations/b.var
  54 *)
  55
  56 (* UNEXPORTED
  57 cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var
  58 *)
  59
  60 (* begin hide *)
  61
  62 inline procedural "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__" as definition.
  63
  64 (* end hide *)
  65
  66 (* UNEXPORTED
  67 cic:/CoRN/ftc/IntervalFunct/Operations/f.var
  68 *)
  69
  70 (* UNEXPORTED
  71 cic:/CoRN/ftc/IntervalFunct/Operations/g.var
  72 *)
  73
  74 (* UNEXPORTED
  75 Section Const
  76 *)
  77
  78 (*#*
  79 Constant and identity functions are defined.
  80
  81 %\begin{convention}% Let [c:IR].
  82 %\end{convention}%
  83 *)
  84
  85 (* UNEXPORTED
  86 cic:/CoRN/ftc/IntervalFunct/Operations/Const/c.var
  87 *)
  88
  89 inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst_strext.con" as lemma.
  90
  91 inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst.con" as definition.
  92
  93 (* UNEXPORTED
  94 End Const
  95 *)
  96
  97 inline procedural "cic:/CoRN/ftc/IntervalFunct/IId_strext.con" as lemma.
  98
  99 inline procedural "cic:/CoRN/ftc/IntervalFunct/IId.con" as definition.
 100
 101 (*#*
 102 Next, we define addition, algebraic inverse, subtraction and product of functions.
 103 *)
 104
 105 inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus_strext.con" as lemma.
 106
 107 inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus.con" as definition.
 108
 109 inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv_strext.con" as lemma.
 110
 111 inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv.con" as definition.
 112
 113 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus_strext.con" as lemma.
 114
 115 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus.con" as definition.
 116
 117 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult_strext.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult.con" as definition.
 120
 121 (* UNEXPORTED
 122 Section Nth_Power
 123 *)
 124
 125 (*#*
 126 Exponentiation to a natural power [n] is also useful.
 127 *)
 128
 129 (* UNEXPORTED
 130 cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/n.var
 131 *)
 132
 133 inline procedural "cic:/CoRN/ftc/IntervalFunct/INth_strext.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/ftc/IntervalFunct/INth.con" as definition.
 136
 137 (* UNEXPORTED
 138 End Nth_Power
 139 *)
 140
 141 (*#*
 142 If a function is non-zero in all the interval then we can define its multiplicative inverse.
 143 *)
 144
 145 (* UNEXPORTED
 146 Section Recip_Div
 147 *)
 148
 149 (* begin show *)
 150
 151 (* UNEXPORTED
 152 cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/Hg.var
 153 *)
 154
 155 (* end show *)
 156
 157 inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip_strext.con" as lemma.
 158
 159 inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip.con" as definition.
 160
 161 inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con" as lemma.
 162
 163 inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv.con" as definition.
 164
 165 (* UNEXPORTED
 166 End Recip_Div
 167 *)
 168
 169 (*#*
 170 Absolute value will also be needed at some point.
 171 *)
 172
 173 inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con" as lemma.
 174
 175 inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs.con" as definition.
 176
 177 (* UNEXPORTED
 178 End Operations
 179 *)
 180
 181 (*#*
 182 The set of these functions form a ring with relation to the operations
 183 of sum and multiplication.  As they actually form a set, this fact can
 184 be proved in Coq for this class of functions; unfortunately, due to a
 185 problem with the coercions, we are not able to use it (Coq will not
 186 recognize the elements of that ring as functions which can be applied
 187 to elements of [[a,b]]), so we merely state this fact here as a
 188 curiosity.
 189
 190 Finally, we define composition; for this we need two functions with
 191 different domains.
 192
 193 %\begin{convention}% [a',b'] be real numbers and denote by [I'] the
 194 compact interval [[a',b']], and let [g] be a setoid function of type
 195 [I' -> IR].
 196 %\end{convention}%
 197 *)
 198
 199 (* UNEXPORTED
 200 Section Composition
 201 *)
 202
 203 (* UNEXPORTED
 204 cic:/CoRN/ftc/IntervalFunct/Composition/a.var
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/ftc/IntervalFunct/Composition/b.var
 209 *)
 210
 211 (* UNEXPORTED
 212 cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var
 213 *)
 214
 215 (* begin hide *)
 216
 217 inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__" as definition.
 218
 219 (* end hide *)
 220
 221 (* UNEXPORTED
 222 cic:/CoRN/ftc/IntervalFunct/Composition/a'.var
 223 *)
 224
 225 (* UNEXPORTED
 226 cic:/CoRN/ftc/IntervalFunct/Composition/b'.var
 227 *)
 228
 229 (* UNEXPORTED
 230 cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var
 231 *)
 232
 233 (* begin hide *)
 234
 235 inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__" as definition.
 236
 237 (* end hide *)
 238
 239 (* UNEXPORTED
 240 cic:/CoRN/ftc/IntervalFunct/Composition/f.var
 241 *)
 242
 243 (* UNEXPORTED
 244 cic:/CoRN/ftc/IntervalFunct/Composition/g.var
 245 *)
 246
 247 (* UNEXPORTED
 248 cic:/CoRN/ftc/IntervalFunct/Composition/Hfg.var
 249 *)
 250
 251 inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp_strext.con" as lemma.
 252
 253 inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp.con" as definition.
 254
 255 (* UNEXPORTED
 256 End Composition
 257 *)
 258
 259 (* UNEXPORTED
 260 Implicit Arguments IConst [a b Hab].
 261 *)
 262
 263 (* UNEXPORTED
 264 Implicit Arguments IId [a b Hab].
 265 *)
 266
 267 (* UNEXPORTED
 268 Implicit Arguments IPlus [a b Hab].
 269 *)
 270
 271 (* UNEXPORTED
 272 Implicit Arguments IInv [a b Hab].
 273 *)
 274
 275 (* UNEXPORTED
 276 Implicit Arguments IMinus [a b Hab].
 277 *)
 278
 279 (* UNEXPORTED
 280 Implicit Arguments IMult [a b Hab].
 281 *)
 282
 283 (* UNEXPORTED
 284 Implicit Arguments INth [a b Hab].
 285 *)
 286
 287 (* UNEXPORTED
 288 Implicit Arguments IRecip [a b Hab].
 289 *)
 290
 291 (* UNEXPORTED
 292 Implicit Arguments IDiv [a b Hab].
 293 *)
 294
 295 (* UNEXPORTED
 296 Implicit Arguments IAbs [a b Hab].
 297 *)
 298
 299 (* UNEXPORTED
 300 Implicit Arguments IComp [a b Hab a' b' Hab'].
 301 *)
 302