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