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 include "CoRN.ma".
  20
  21 (* $Id: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *)
  22
  23 include "ftc/PartFunEquality.ma".
  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 alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Operations/a.var".
  51
  52 alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Operations/b.var".
  53
  54 alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var".
  55
  56 (* begin hide *)
  57
  58 inline "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__".
  59
  60 (* end hide *)
  61
  62 alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Operations/f.var".
  63
  64 alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Operations/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 alias id "c" = "cic:/CoRN/ftc/IntervalFunct/Operations/Const/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 alias id "n" = "cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/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 alias id "Hg" = "cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/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 alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Composition/a.var".
 190
 191 alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Composition/b.var".
 192
 193 alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var".
 194
 195 (* begin hide *)
 196
 197 inline "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__".
 198
 199 (* end hide *)
 200
 201 alias id "a'" = "cic:/CoRN/ftc/IntervalFunct/Composition/a'.var".
 202
 203 alias id "b'" = "cic:/CoRN/ftc/IntervalFunct/Composition/b'.var".
 204
 205 alias id "Hab'" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var".
 206
 207 (* begin hide *)
 208
 209 inline "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__".
 210
 211 (* end hide *)
 212
 213 alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Composition/f.var".
 214
 215 alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Composition/g.var".
 216
 217 alias id "Hfg" = "cic:/CoRN/ftc/IntervalFunct/Composition/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