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