]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / PartFunEquality.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/PartFunEquality".
18
19 include "CoRN.ma".
20
21 (* $Id: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *)
22
23 (*#* printing Feq %\ensuremath{\approx}% #≈# *)
24
25 include "reals/Intervals.ma".
26
27 include "tactics/DiffTactics1.ma".
28
29 (* UNEXPORTED
30 Section Definitions
31 *)
32
33 (*#* *Equality of Partial Functions
34
35 ** Definitions
36
37 In some contexts (namely when quantifying over partial functions) we
38 need to refer explicitly to the subsetoid of elements satisfying a
39 given predicate rather than to the predicate itself.  The following
40 definition makes this possible.
41 *)
42
43 inline "cic:/CoRN/ftc/PartFunEquality/subset.con".
44
45 (*#*
46 The core of our work will revolve around the following fundamental
47 notion: two functions are equal in a given domain (predicate) iff they
48 coincide on every point of that domain#. #%\footnote{%Notice that,
49 according to our definition of partial function, it is equivalent to
50 prove the equality for every proof or for a specific proof.  Typically
51 it is easier to consider a generic case%.}%.  This file is concerned
52 with proving the main properties of this equality relation.
53 *)
54
55 inline "cic:/CoRN/ftc/PartFunEquality/Feq.con".
56
57 (*#*
58 Notice that, because the quantification over the proofs is universal,
59 we must require explicitly that the predicate be included in the
60 domain of each function; otherwise the basic properties of equality
61 (like, for example, transitivity) would fail to hold#. #%\footnote{%To
62 see this it is enough to realize that the empty function would be
63 equal to every other function in every domain.%}.% The way to
64 circumvent this would be to quantify existentially over the proofs;
65 this, however, would have two major disadvantages: first, proofs of
66 equality would become very cumbersome and clumsy; secondly (and most
67 important), we often need to prove the inclusions from an equality
68 hypothesis, and this definition allows us to do it in a very easy way.
69 Also, the pointwise equality is much nicer to use from this definition
70 than in an existentially quantified one.
71 *)
72
73 (* UNEXPORTED
74 End Definitions
75 *)
76
77 (* UNEXPORTED
78 Section Equality_Results
79 *)
80
81 (*#* **Properties of Inclusion
82
83 We will now prove the main properties of the equality relation.
84
85 %\begin{convention}% Let [I,R:IR->CProp] and [F,G:PartIR], and denote
86 by [P] and [Q], respectively, the domains of [F] and [G].
87 %\end{convention}%
88 *)
89
90 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/I.var".
91
92 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/F.var".
93
94 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var".
95
96 (* begin hide *)
97
98 inline "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__".
99
100 inline "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__".
101
102 (* end hide *)
103
104 alias id "R" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/R.var".
105
106 (*#*
107 We start with two lemmas which make it much easier to prove and use
108 this definition:
109 *)
110
111 inline "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con".
112
113 inline "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con".
114
115 inline "cic:/CoRN/ftc/PartFunEquality/included_IR.con".
116
117 (* UNEXPORTED
118 End Equality_Results
119 *)
120
121 (* UNEXPORTED
122 Hint Resolve included_IR : included.
123 *)
124
125 (* UNEXPORTED
126 Section Some_More
127 *)
128
129 (*#*
130 If two function coincide on a given subset then they coincide in any smaller subset.
131 *)
132
133 inline "cic:/CoRN/ftc/PartFunEquality/included_Feq.con".
134
135 (* UNEXPORTED
136 End Some_More
137 *)
138
139 (* UNEXPORTED
140 Section Away_from_Zero
141 *)
142
143 (* UNEXPORTED
144 Section Definitions
145 *)
146
147 (*#* **Away from Zero
148
149 Before we prove our main results about the equality we have to do some
150 work on division.  A function is said to be bounded away from zero in
151 a set if there exists a positive lower bound for the set of absolute
152 values of its image of that set.
153
154 %\begin{convention}% Let [I : IR->CProp], [F : PartIR] and denote by [P]
155 the domain of [F].
156 %\end{convention}%
157 *)
158
159 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/I.var".
160
161 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var".
162
163 (* begin hide *)
164
165 inline "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__".
166
167 (* end hide *)
168
169 inline "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con".
170
171 (*#*
172 If [F] is bounded away from zero in [I] then [F] is necessarily apart from zero in [I]; also this means that [I] is included in the domain of [{1/}F].
173 *)
174
175 (* begin show *)
176
177 alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var".
178
179 (* end show *)
180
181 inline "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con".
182
183 inline "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con".
184
185 inline "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con".
186
187 (* UNEXPORTED
188 End Definitions
189 *)
190
191 (*#*
192 Boundedness away from zero is preserved through restriction of the set.
193
194 %\begin{convention}% Let [F] be a partial function and [P, Q] be predicates.
195 %\end{convention}%
196 *)
197
198 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/F.var".
199
200 alias id "P" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var".
201
202 alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var".
203
204 inline "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con".
205
206 inline "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con".
207
208 (*#*
209 A function is said to be bounded away from zero everywhere if it is bounded away from zero in every compact subinterval of its domain; a similar definition is made for arbitrary sets, which will be necessary for future work.
210 *)
211
212 inline "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con".
213
214 inline "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con".
215
216 (*#*
217 An immediate consequence:
218 *)
219
220 inline "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con".
221
222 inline "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con".
223
224 (* UNEXPORTED
225 End Away_from_Zero
226 *)
227
228 (* UNEXPORTED
229 Hint Resolve bnd_imp_inc_recip bnd_imp_inc_div: included.
230 *)
231
232 (* UNEXPORTED
233 Hint Immediate bnd_in_P_imp_ap_zero: included.
234 *)
235
236 (*#* ** The [FEQ] tactic
237 This tactic splits a goal of the form [Feq I F G] into the three subgoals
238 [included I (Dom F)], [included I (Dom G)] and [forall x, F x [=] G x]
239 and applies [Included] to the first two and [rational] to the third.
240 *)
241
242 (* begin hide *)
243
244 (* UNEXPORTED
245 Ltac FEQ := apply eq_imp_Feq;
246    [ Included | Included | intros; try (simpl in |- *; rational) ].
247 *)
248
249 (* end hide *)
250
251 (* UNEXPORTED
252 Section More_on_Equality
253 *)
254
255 (*#* **Properties of Equality
256
257 We are now finally able to prove the main properties of the equality relation.  We begin by showing it to be an equivalence relation.
258
259 %\begin{convention}% Let [I] be a predicate and [F, F', G, G', H] be
260 partial functions.
261 %\end{convention}%
262 *)
263
264 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/I.var".
265
266 (* UNEXPORTED
267 Section Feq_Equivalence
268 *)
269
270 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/F.var".
271
272 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G.var".
273
274 alias id "H" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var".
275
276 inline "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con".
277
278 inline "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con".
279
280 inline "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con".
281
282 (* UNEXPORTED
283 End Feq_Equivalence
284 *)
285
286 (* UNEXPORTED
287 Section Operations
288 *)
289
290 (*#*
291 Also it is preserved through application of functional constructors and restriction.
292 *)
293
294 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F.var".
295
296 alias id "F'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F'.var".
297
298 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var".
299
300 alias id "G'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var".
301
302 inline "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con".
303
304 inline "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con".
305
306 inline "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con".
307
308 inline "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con".
309
310 inline "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con".
311
312 inline "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con".
313
314 inline "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con".
315
316 inline "cic:/CoRN/ftc/PartFunEquality/Feq_div.con".
317
318 inline "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con".
319
320 (*#*
321 Notice that in the case of division we only need to require boundedness away from zero for one of the functions (as they are equal); thus the two last lemmas are stated in two different ways, as according to the context one or the other condition may be easier to prove.
322
323 The restriction of a function is well defined.
324 *)
325
326 inline "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con".
327
328 (*#*
329 The image of a set is extensional.
330 *)
331
332 inline "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con".
333
334 (* UNEXPORTED
335 End Operations
336 *)
337
338 (* UNEXPORTED
339 End More_on_Equality
340 *)
341
342 (* UNEXPORTED
343 Section Nth_Power
344 *)
345
346 (*#* **Nth Power
347
348 We finish this group of lemmas with characterization results for the
349 power function (similar to those already proved for arbitrary rings).
350 The characterization is done at first pointwise and later using the
351 equality relation.
352
353 %\begin{convention}% Let [F] be a partial function with domain [P] and
354 [Q] be a predicate on the real numbers assumed to be included in [P].
355 %\end{convention}%
356 *)
357
358 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var".
359
360 (* begin hide *)
361
362 inline "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__".
363
364 (* end hide *)
365
366 alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Q.var".
367
368 alias id "H" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var".
369
370 alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var".
371
372 inline "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con".
373
374 alias id "n" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var".
375
376 alias id "H'" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var".
377
378 inline "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con".
379
380 (* UNEXPORTED
381 End Nth_Power
382 *)
383
384 (* UNEXPORTED
385 Section Strong_Nth_Power
386 *)
387
388 (*#*
389 %\begin{convention}% Let [a,b] be real numbers such that [I := [a,b]]
390 is included in the domain of [F].
391 %\end{convention}%
392 *)
393
394 alias id "a" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/a.var".
395
396 alias id "b" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/b.var".
397
398 alias id "Hab" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var".
399
400 (* begin hide *)
401
402 inline "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__".
403
404 (* end hide *)
405
406 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var".
407
408 alias id "incF" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var".
409
410 inline "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con".
411
412 inline "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con".
413
414 (* UNEXPORTED
415 End Strong_Nth_Power
416 *)
417