Correspondence
In this file we prove that there are mappings going in both ways between the set of partial functions whose domain contains [a,b] and the set of real-valued functions with domain on that interval. These mappings form an adjunction, and thus they have all the good properties for preservation results.
Mappings
We begin by defining the map from partial functions to setoid functions as simply being the restriction of the partial function to the interval [a,b].
Let F be a partial function and a,b:IR such that I = [a,b] is included in the domain of F.
Variable F : PartIR.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Hypothesis Hf : ⊆ I (Dom F).
Lemma IntPartIR_strext : fun_strext
(fun x : subset I => F (scs_elem _ _ x) (Hf _ (scs_prf _ _ x))).
Definition IntPartIR : CSetoid_fun (subset I) IR.
Defined.
End Conversion.
Section AntiConversion.
To go the other way around, we simply take a setoid function f with
domain [a,b] and build the corresponding partial function.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable f : CSetoid_fun (subset I) IR.
Lemma PartInt_strext : forall x y Hx Hy,
f (Build_subcsetoid_crr IR _ x Hx) [#] f (Build_subcsetoid_crr IR _ y Hy) -> x [#] y.
Definition PartInt : PartIR.
Defined.
End AntiConversion.
Section Inverses.
In one direction these operators are inverses.
Lemma int_part_int : forall a b Hab F (Hf : ⊆ (compact a b Hab) (Dom F)),
≈ (compact a b Hab) F (PartInt (IntPartIR Hf)).
End Inverses.
Section Equivalences.
Mappings Preserve Operations
We now prove that all the operations we have defined on both sets are preserved by PartInt.
Let F,G be partial functions and a,b:IR and denote by I the interval [a,b]. Let f,g be setoid functions of type I->IR equal respectively to F and G in I.
Variables F G : PartIR.
Variables a b c : IR.
Hypothesis Hab : a [<=] b.
Variables f g : CSetoid_fun (subset (compact a b Hab)) IR.
Hypothesis Ff : ≈ I F (PartInt f).
Hypothesis Gg : ≈ I G (PartInt g).
Lemma part_int_const : ≈ I [-C-]c (PartInt (IConst (Hab:=Hab) c)).
Lemma part_int_id : ≈ I FId (PartInt (IId (Hab:=Hab))).
Lemma part_int_plus : ≈ I (F{+}G) (PartInt (IPlus f g)).
Included.
Included.
Qed.
Lemma part_int_inv : ≈ I {--}F (PartInt (IInv f)).
Included.
Included.
Qed.
Lemma part_int_minus : ≈ I (F{-}G) (PartInt (IMinus f g)).
Included.
Included.
Qed.
Lemma part_int_mult : ≈ I (F{*}G) (PartInt (IMult f g)).
Included.
Included.
Qed.
Lemma part_int_nth : forall n : N, ≈ I (F{^}n) (PartInt (INth f n)).
Included.
Included.
Qed.
Hypothesis HG : bnd_away_zero I G.
Hypothesis Hg : forall x : subset I, g x [#] 0.
Lemma part_int_recip : ≈ I {1/}G (PartInt (IRecip g Hg)).
Included.
Included.
Qed.
Lemma part_int_div : ≈ I (F{/}G) (PartInt (IDiv f g Hg)).
Included.
Included.
Qed.
End Equivalences.