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.
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. 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.
Definition ≈ P (F G : PartIR) := ⊆ P (Dom F) and ⊆ P (Dom G) and
(forall x, P x -> forall Hx Hx', F x Hx [=] G x Hx').
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. 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.
Properties of Inclusion
We will now prove the main properties of the equality relation.
Let I,R:IR->CProp and F,G:PartIR, and denote by P and Q, respectively, the domains of F and G.
We start with two lemmas which make it much easier to prove and use
this definition:
Lemma eq_imp_Feq : ⊆ I P -> ⊆ I Q ->
(forall x, I x -> forall Hx Hx', F x Hx [=] G x Hx') -> ≈ I F G.
Lemma Feq_imp_eq : ≈ I F G -> forall x, I x -> forall Hx Hx', F x Hx [=] G x Hx'.
Lemma included_IR : ⊆ I (fun x : IR => CTrue).
End Equality_Results.
Section Some_More.
If two function coincide on a given subset then they coincide in any smaller subset.
Lemma included_Feq : forall P Q F G, ⊆ P Q -> ≈ Q F G -> ≈ P F G.
End Some_More.
Section Away_from_Zero.
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.
Let I : IR->CProp, F : PartIR and denote by P the domain of F.
Variable I : IR -> CProp.
Variable F : PartIR.
Definition bnd_away_zero := ⊆ I P and {c : IR | 0 [<] c |
forall y Hy, (I y) -> c [<=] AbsIR (F y Hy)}.
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.
Hypothesis Hf : bnd_away_zero.
Lemma bnd_imp_ap_zero : forall x Hx, (I x) -> F x Hx [#] 0.
Lemma bnd_imp_inc_recip : ⊆ I (Dom {1/}F).
Lemma bnd_imp_inc_div : forall G, ⊆ I (Dom G) -> ⊆ I (Dom (G{/}F)).
End Definitions.
Boundedness away from zero is preserved through restriction of the set.
Let F be a partial function and P, Q be predicates.
Let F be a partial function and P, Q be predicates.
Variable F : PartIR.
Variables P Q : IR -> CProp.
Lemma included_imp_bnd : ⊆ Q P -> bnd_away_zero P F -> bnd_away_zero Q F.
Lemma FRestr_bnd : forall (HP : pred_wd _ P) (H : ⊆ P (Dom F)),
⊆ Q P -> bnd_away_zero Q F -> bnd_away_zero Q (Frestr HP H).
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.
Definition bnd_away_zero_everywhere G := forall a b Hab,
⊆ (compact a b Hab) (Dom G) -> bnd_away_zero (compact a b Hab) G.
Definition bnd_away_zero_in_P := forall a b Hab,
⊆ (compact a b Hab) P -> bnd_away_zero (compact a b Hab) F.
An immediate consequence:
Lemma bnd_in_P_imp_ap_zero : pred_wd _ P -> bnd_away_zero_in_P ->
forall x, P x -> forall Hx, F x Hx [#] 0.
Lemma FRestr_bnd' : forall (HP : pred_wd _ P) (H : ⊆ P (Dom F)),
bnd_away_zero_everywhere F -> bnd_away_zero_everywhere (Frestr HP H).
End Away_from_Zero.
The FEQ tactic
This tactic splits a goal of the form ≈ I F G into the three subgoals ⊆ I (Dom F), ⊆ I (Dom G) and forall x, F x = G x and applies Included to the first two and rational to the third.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.
Let I be a predicate and F, F', G, G', H be partial functions.
Variable I : IR -> CProp.
Section Feq_Equivalence.
Variables F G H : PartIR.
Lemma Feq_reflexive : ⊆ I (Dom F) -> ≈ I F F.
Lemma Feq_symmetric : ≈ I F G -> ≈ I G F.
Lemma Feq_transitive : ≈ I F G -> ≈ I G H -> ≈ I F H.
End Feq_Equivalence.
Section Operations.
Also it is preserved through application of functional constructors and restriction.
Variables F F' G G' : PartIR.
Lemma Feq_plus : ≈ I F F' -> ≈ I G G' -> ≈ I (F{+}G) (F'{+}G').
Lemma Feq_inv : ≈ I F F' -> ≈ I {--}F {--}F'.
Lemma Feq_minus : ≈ I F F' -> ≈ I G G' -> ≈ I (F{-}G) (F'{-}G').
Lemma Feq_mult : ≈ I F F' -> ≈ I G G' -> ≈ I (F{*}G) (F'{*}G').
Lemma Feq_nth : forall n : N, ≈ I F F' -> ≈ I (F{^}n) (F'{^}n).
Lemma Feq_recip : bnd_away_zero I F -> ≈ I F F' -> ≈ I {1/}F {1/}F'.
Lemma Feq_recip' : bnd_away_zero I F -> ≈ I F' F -> ≈ I {1/}F' {1/}F.
Lemma Feq_div : bnd_away_zero I G ->
≈ I F F' -> ≈ I G G' -> ≈ I (F{/}G) (F'{/}G').
Lemma Feq_div' : bnd_away_zero I G ->
≈ I F' F -> ≈ I G' G -> ≈ I (F'{/}G') (F{/}G).
Lemma Feq_comp : forall (J : IR -> CProp),
(forall x Hx, I x -> J (F x Hx)) -> (forall x Hx, I x -> J (F' x Hx)) ->
≈ I F F' -> ≈ J G G' -> ≈ I (G[o]F) (G'[o]F').
Included.
Included.
Qed.
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.
The restriction of a function is well defined.
The image of a set is extensional.
Lemma fun_image_wd : ≈ I F G -> forall x, fun_image F I x -> fun_image G I x.
End Operations.
End More_on_Equality.
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.
Let F be a partial function with domain P and Q be a predicate on the real numbers assumed to be included in P.
Variable F : PartIR.
Variable Q : IR -> CProp.
Hypothesis H : ⊆ Q (fun x : IR => CTrue).
Hypothesis Hf : ⊆ Q (Dom F).
Lemma FNth_zero : forall x, Q x -> forall Hx Hx', [-C-]1 x Hx [=] (F{^}0) x Hx'.
Variable n : N.
Hypothesis H' : ⊆ Q (Dom (F{*}F{^}n)).
Lemma FNth_mult : forall x, Q x -> forall Hx Hx', (F{*}F{^}n) x Hx [=] (F{^}S n) x Hx'.
End Nth_Power.
Section Strong_Nth_Power.
Let a,b be real numbers such that I := [a,b]
is included in the domain of F.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable F : PartIR.
Hypothesis incF : ⊆ I (Dom F).
Lemma FNth_zero' : ≈ I [-C-]1 (F{^}0).
Lemma FNth_mult' : forall n, ≈ I (F{*}F{^}n) (F{^}S n).
End Strong_Nth_Power.