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: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *)
21 (*#* printing Feq %\ensuremath{\approx}% #≈# *)
23 include "reals/Intervals.ma".
25 include "tactics/DiffTactics1.ma".
31 (*#* *Equality of Partial Functions
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.
41 inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con" as definition.
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.
53 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con" as definition.
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.
76 Section Equality_Results
79 (*#* **Properties of Inclusion
81 We will now prove the main properties of the equality relation.
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].
88 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/I.var".
90 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/F.var".
92 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var".
96 inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__" as definition.
98 inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__" as definition.
102 alias id "R" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/R.var".
105 We start with two lemmas which make it much easier to prove and use
109 inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con" as lemma.
111 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con" as lemma.
113 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con" as lemma.
120 Hint Resolve included_IR : included.
128 If two function coincide on a given subset then they coincide in any smaller subset.
131 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con" as lemma.
138 Section Away_from_Zero
145 (*#* **Away from Zero
147 Before we prove our main results about the equality we have to do some
148 work on division. A function is said to be bounded away from zero in
149 a set if there exists a positive lower bound for the set of absolute
150 values of its image of that set.
152 %\begin{convention}% Let [I : IR->CProp], [F : PartIR] and denote by [P]
157 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/I.var".
159 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var".
163 inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__" as definition.
167 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con" as definition.
170 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].
175 alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var".
179 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con" as lemma.
181 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con" as lemma.
183 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con" as lemma.
190 Boundedness away from zero is preserved through restriction of the set.
192 %\begin{convention}% Let [F] be a partial function and [P, Q] be predicates.
196 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/F.var".
198 alias id "P" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var".
200 alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var".
202 inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con" as lemma.
204 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con" as lemma.
207 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 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con" as definition.
212 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con" as definition.
215 An immediate consequence:
218 inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con" as lemma.
220 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con" as lemma.
227 Hint Resolve bnd_imp_inc_recip bnd_imp_inc_div: included.
231 Hint Immediate bnd_in_P_imp_ap_zero: included.
234 (*#* ** The [FEQ] tactic
235 This tactic splits a goal of the form [Feq I F G] into the three subgoals
236 [included I (Dom F)], [included I (Dom G)] and [forall x, F x [=] G x]
237 and applies [Included] to the first two and [rational] to the third.
243 Ltac FEQ := apply eq_imp_Feq;
244 [ Included | Included | intros; try (simpl in |- *; rational) ].
250 Section More_on_Equality
253 (*#* **Properties of Equality
255 We are now finally able to prove the main properties of the equality relation. We begin by showing it to be an equivalence relation.
257 %\begin{convention}% Let [I] be a predicate and [F, F', G, G', H] be
262 alias id "I" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/I.var".
265 Section Feq_Equivalence
268 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/F.var".
270 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G.var".
272 alias id "H" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var".
274 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con" as lemma.
276 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con" as lemma.
278 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con" as lemma.
289 Also it is preserved through application of functional constructors and restriction.
292 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F.var".
294 alias id "F'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F'.var".
296 alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var".
298 alias id "G'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var".
300 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con" as lemma.
302 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con" as lemma.
304 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con" as lemma.
306 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con" as lemma.
308 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con" as lemma.
310 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con" as lemma.
312 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con" as lemma.
314 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con" as lemma.
316 inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con" as lemma.
319 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.
321 The restriction of a function is well defined.
324 inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con" as lemma.
327 The image of a set is extensional.
330 inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con" as lemma.
346 We finish this group of lemmas with characterization results for the
347 power function (similar to those already proved for arbitrary rings).
348 The characterization is done at first pointwise and later using the
351 %\begin{convention}% Let [F] be a partial function with domain [P] and
352 [Q] be a predicate on the real numbers assumed to be included in [P].
356 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var".
360 inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__" as definition.
364 alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Q.var".
366 alias id "H" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var".
368 alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var".
370 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con" as lemma.
372 alias id "n" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var".
374 alias id "H'" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var".
376 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con" as lemma.
383 Section Strong_Nth_Power
387 %\begin{convention}% Let [a,b] be real numbers such that [I := [a,b]]
388 is included in the domain of [F].
392 alias id "a" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/a.var".
394 alias id "b" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/b.var".
396 alias id "Hab" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var".
400 inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__" as definition.
404 alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var".
406 alias id "incF" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var".
408 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con" as lemma.
410 inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con" as lemma.