1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: IntervalFunct.v,v 1.5 2004/04/08 15:28:06 lcf Exp $ *)
21 include "ftc/PartFunEquality.ma".
27 (*#* * Functions with compact domain
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.
38 Throughout this section we will focus on a compact interval and define
39 operators analogous to those we already have for arbitrary partial
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
48 alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Operations/a.var".
50 alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Operations/b.var".
52 alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Operations/Hab.var".
56 inline procedural "cic:/CoRN/ftc/IntervalFunct/Operations/I.con" "Operations__" as definition.
60 alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Operations/f.var".
62 alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Operations/g.var".
69 Constant and identity functions are defined.
71 %\begin{convention}% Let [c:IR].
75 alias id "c" = "cic:/CoRN/ftc/IntervalFunct/Operations/Const/c.var".
77 inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst_strext.con" as lemma.
79 inline procedural "cic:/CoRN/ftc/IntervalFunct/IConst.con" as definition.
85 inline procedural "cic:/CoRN/ftc/IntervalFunct/IId_strext.con" as lemma.
87 inline procedural "cic:/CoRN/ftc/IntervalFunct/IId.con" as definition.
90 Next, we define addition, algebraic inverse, subtraction and product of functions.
93 inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus_strext.con" as lemma.
95 inline procedural "cic:/CoRN/ftc/IntervalFunct/IPlus.con" as definition.
97 inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv_strext.con" as lemma.
99 inline procedural "cic:/CoRN/ftc/IntervalFunct/IInv.con" as definition.
101 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus_strext.con" as lemma.
103 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMinus.con" as definition.
105 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult_strext.con" as lemma.
107 inline procedural "cic:/CoRN/ftc/IntervalFunct/IMult.con" as definition.
114 Exponentiation to a natural power [n] is also useful.
117 alias id "n" = "cic:/CoRN/ftc/IntervalFunct/Operations/Nth_Power/n.var".
119 inline procedural "cic:/CoRN/ftc/IntervalFunct/INth_strext.con" as lemma.
121 inline procedural "cic:/CoRN/ftc/IntervalFunct/INth.con" as definition.
128 If a function is non-zero in all the interval then we can define its multiplicative inverse.
137 alias id "Hg" = "cic:/CoRN/ftc/IntervalFunct/Operations/Recip_Div/Hg.var".
141 inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip_strext.con" as lemma.
143 inline procedural "cic:/CoRN/ftc/IntervalFunct/IRecip.con" as definition.
145 inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv_strext.con" as lemma.
147 inline procedural "cic:/CoRN/ftc/IntervalFunct/IDiv.con" as definition.
154 Absolute value will also be needed at some point.
157 inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs_strext.con" as lemma.
159 inline procedural "cic:/CoRN/ftc/IntervalFunct/IAbs.con" as definition.
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
174 Finally, we define composition; for this we need two functions with
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
187 alias id "a" = "cic:/CoRN/ftc/IntervalFunct/Composition/a.var".
189 alias id "b" = "cic:/CoRN/ftc/IntervalFunct/Composition/b.var".
191 alias id "Hab" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab.var".
195 inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I.con" "Composition__" as definition.
199 alias id "a'" = "cic:/CoRN/ftc/IntervalFunct/Composition/a'.var".
201 alias id "b'" = "cic:/CoRN/ftc/IntervalFunct/Composition/b'.var".
203 alias id "Hab'" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hab'.var".
207 inline procedural "cic:/CoRN/ftc/IntervalFunct/Composition/I'.con" "Composition__" as definition.
211 alias id "f" = "cic:/CoRN/ftc/IntervalFunct/Composition/f.var".
213 alias id "g" = "cic:/CoRN/ftc/IntervalFunct/Composition/g.var".
215 alias id "Hfg" = "cic:/CoRN/ftc/IntervalFunct/Composition/Hfg.var".
217 inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp_strext.con" as lemma.
219 inline procedural "cic:/CoRN/ftc/IntervalFunct/IComp.con" as definition.
226 Implicit Arguments IConst [a b Hab].
230 Implicit Arguments IId [a b Hab].
234 Implicit Arguments IPlus [a b Hab].
238 Implicit Arguments IInv [a b Hab].
242 Implicit Arguments IMinus [a b Hab].
246 Implicit Arguments IMult [a b Hab].
250 Implicit Arguments INth [a b Hab].
254 Implicit Arguments IRecip [a b Hab].
258 Implicit Arguments IDiv [a b Hab].
262 Implicit Arguments IAbs [a b Hab].
266 Implicit Arguments IComp [a b Hab a' b' Hab'].