]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/IntervalFunct.mma
ground_2 released and permanently renamed as ground
[helm.git] / 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