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