(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *) (*#* printing Feq %\ensuremath{\approx}% #≈# *) include "reals/Intervals.ma". include "tactics/DiffTactics1.ma". (* UNEXPORTED Section Definitions *) (*#* *Equality of Partial Functions ** Definitions In some contexts (namely when quantifying over partial functions) we need to refer explicitly to the subsetoid of elements satisfying a given predicate rather than to the predicate itself. The following definition makes this possible. *) inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con" as definition. (*#* The core of our work will revolve around the following fundamental notion: two functions are equal in a given domain (predicate) iff they coincide on every point of that domain#. #%\footnote{%Notice that, according to our definition of partial function, it is equivalent to prove the equality for every proof or for a specific proof. Typically it is easier to consider a generic case%.}%. This file is concerned with proving the main properties of this equality relation. *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con" as definition. (*#* Notice that, because the quantification over the proofs is universal, we must require explicitly that the predicate be included in the domain of each function; otherwise the basic properties of equality (like, for example, transitivity) would fail to hold#. #%\footnote{%To see this it is enough to realize that the empty function would be equal to every other function in every domain.%}.% The way to circumvent this would be to quantify existentially over the proofs; this, however, would have two major disadvantages: first, proofs of equality would become very cumbersome and clumsy; secondly (and most important), we often need to prove the inclusions from an equality hypothesis, and this definition allows us to do it in a very easy way. Also, the pointwise equality is much nicer to use from this definition than in an existentially quantified one. *) (* UNEXPORTED End Definitions *) (* UNEXPORTED Section Equality_Results *) (*#* **Properties of Inclusion We will now prove the main properties of the equality relation. %\begin{convention}% Let [I,R:IR->CProp] and [F,G:PartIR], and denote by [P] and [Q], respectively, the domains of [F] and [G]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Equality_Results/I.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Equality_Results/F.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__" as definition. inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Equality_Results/R.var *) (*#* We start with two lemmas which make it much easier to prove and use this definition: *) inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con" as lemma. (* UNEXPORTED End Equality_Results *) (* UNEXPORTED Hint Resolve included_IR : included. *) (* UNEXPORTED Section Some_More *) (*#* If two function coincide on a given subset then they coincide in any smaller subset. *) inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con" as lemma. (* UNEXPORTED End Some_More *) (* UNEXPORTED Section Away_from_Zero *) (* UNEXPORTED Section Definitions *) (*#* **Away from Zero Before we prove our main results about the equality we have to do some work on division. A function is said to be bounded away from zero in a set if there exists a positive lower bound for the set of absolute values of its image of that set. %\begin{convention}% Let [I : IR->CProp], [F : PartIR] and denote by [P] the domain of [F]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/I.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__" as definition. (* end hide *) inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con" as definition. (*#* 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]. *) (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var *) (* end show *) inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con" as lemma. (* UNEXPORTED End Definitions *) (*#* Boundedness away from zero is preserved through restriction of the set. %\begin{convention}% Let [F] be a partial function and [P, Q] be predicates. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/F.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var *) inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con" as lemma. (*#* 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. *) inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con" as definition. inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con" as definition. (*#* An immediate consequence: *) inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con" as lemma. (* UNEXPORTED End Away_from_Zero *) (* UNEXPORTED Hint Resolve bnd_imp_inc_recip bnd_imp_inc_div: included. *) (* UNEXPORTED Hint Immediate bnd_in_P_imp_ap_zero: included. *) (*#* ** The [FEQ] tactic This tactic splits a goal of the form [Feq I F G] into the three subgoals [included I (Dom F)], [included I (Dom G)] and [forall x, F x [=] G x] and applies [Included] to the first two and [rational] to the third. *) (* begin hide *) (* UNEXPORTED Ltac FEQ := apply eq_imp_Feq; [ Included | Included | intros; try (simpl in |- *; rational) ]. *) (* end hide *) (* UNEXPORTED Section More_on_Equality *) (*#* **Properties of Equality We are now finally able to prove the main properties of the equality relation. We begin by showing it to be an equivalence relation. %\begin{convention}% Let [I] be a predicate and [F, F', G, G', H] be partial functions. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/I.var *) (* UNEXPORTED Section Feq_Equivalence *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/F.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con" as lemma. (* UNEXPORTED End Feq_Equivalence *) (* UNEXPORTED Section Operations *) (*#* Also it is preserved through application of functional constructors and restriction. *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F'.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con" as lemma. (*#* 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. The restriction of a function is well defined. *) inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con" as lemma. (*#* The image of a set is extensional. *) inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con" as lemma. (* UNEXPORTED End Operations *) (* UNEXPORTED End More_on_Equality *) (* UNEXPORTED Section Nth_Power *) (*#* **Nth Power We finish this group of lemmas with characterization results for the power function (similar to those already proved for arbitrary rings). The characterization is done at first pointwise and later using the equality relation. %\begin{convention}% Let [F] be a partial function with domain [P] and [Q] be a predicate on the real numbers assumed to be included in [P]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Nth_Power/Q.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var *) inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con" as lemma. (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var *) inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con" as lemma. (* UNEXPORTED End Nth_Power *) (* UNEXPORTED Section Strong_Nth_Power *) (*#* %\begin{convention}% Let [a,b] be real numbers such that [I := [a,b]] is included in the domain of [F]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/a.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/b.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var *) (* UNEXPORTED cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var *) inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con" as lemma. inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con" as lemma. (* UNEXPORTED End Strong_Nth_Power *)