CoRN.metric2.Complete

Require Export UniformContinuity.
Require Export QposInf.
Require Export Classification.
Require Import QposMinMax.
Require Import QMinMax.
Require Import Qauto.
Require Import Qordfield.
Require Import COrdFields2.
Require Import CornTac.

Open Local Scope Q_scope.
Open Local Scope uc_scope.

Complete metric space

Section RegularFunction.

Variable X:MetricSpace.

Regular functions

A regular function is one way of representing elements in a complete metric space. A regular function that take a given error e, and returns an approximation within e of the value it is representing. These approximations must be coherent and the definition belows state this property.

Definition is_RegularFunction (x:QposInf -> X) : Prop :=
forall (e1 e2:Qpos), ball (m:=X) (e1 +e2) (x e1) (x e2).

A regular function consists of an approximation function, and a proof that the approximations are coherent.

Record RegularFunction : Type :=
{approximate : QposInf -> X
;regFun_prf : is_RegularFunction approximate
}.

The value of the approximation function at infinity is irrelevant, so we make a smart constructor that just takes a Qpos->X.

Definition is_RegularFunction_noInf (x: Qpos -> X): Prop :=
  forall e1 e2 : Qpos, ball (e1 + e2) (x e1) (x e2).

Section mkRegularFunction.

  Variables (dummy: X).

  Let lift (f: Qpos -> X) (e: QposInf): X :=
    match e with
    | QposInfinity => dummy
    | Qpos2QposInf e' => f e'
    end.

  Let transport (f: Qpos -> X): is_RegularFunction_noInf f -> is_RegularFunction (lift f).

  Definition mkRegularFunction (f: Qpos -> X) (H: is_RegularFunction_noInf f): RegularFunction
    := Build_RegularFunction (transport H).

End mkRegularFunction.

Regular functions form a metric space

Definition regFunEq (f g : RegularFunction) :=
forall e1 e2, ball (m:=X) (e1 +e2) (approximate f e1) (approximate g e2).

Lemma regFunEq_e : forall (f g : RegularFunction), (forall e, ball (m:=X) (e +e) (approximate f e) (approximate g e)) -> (regFunEq f g).

Lemma regFunEq_e_small : forall (f g : RegularFunction) (E:Qpos), (forall (e:Qpos), e <= E -> ball (m:=X) (e +e) (approximate f e) (approximate g e)) -> (regFunEq f g).

Lemma regFun_is_setoid : Setoid_Theory RegularFunction regFunEq.

Definition regFun_Setoid := Build_RSetoid regFun_is_setoid.

Definition regFunBall e (f g : RegularFunction) :=
forall d1 d2, ball (m:=X) (d1 +e +d2)%Qpos (approximate f d1) (approximate g d2).

Lemma regFunBall_wd : forall (e1 e2:Qpos), (QposEq e1 e2) ->
            forall (x1 x2 : regFun_Setoid), (st_eq x1 x2) ->
            forall (y1 y2 : regFun_Setoid), (st_eq y1 y2) ->
            (regFunBall e1 x1 y1 <-> regFunBall e2 x2 y2).

Lemma regFun_is_MetricSpace : is_MetricSpace regFun_Setoid regFunBall.

We define the completion of a metric space to be the space of regular functions

Definition Complete : MetricSpace :=
Build_MetricSpace regFunBall_wd regFun_is_MetricSpace.

The ball of regular functions is related to the underlying ball in ways that you would expect.

Lemma regFunBall_ball : forall (x y:Complete) (e0 e1 e2:Qpos), ball e0 (approximate x e1) (approximate y e2) -> ball (e1 + e0 + e2) x y.

Lemma regFunBall_e : forall (x y:Complete) e, (forall d, ball (d + e + d) (approximate x d) (approximate y d)) -> ball e x y.

Cunit

There is an injection from the original space to the complete space given by the constant regular function.

Lemma Cunit_fun_prf (x:X) : is_RegularFunction (fun _ => x).

Definition Cunit_fun (x:X) : Complete :=
Build_RegularFunction (Cunit_fun_prf x).

Lemma Cunit_prf : is_UniformlyContinuousFunction Cunit_fun Qpos2QposInf.

Definition Cunit : X --> Complete :=
Build_UniformlyContinuousFunction Cunit_prf.

This injection preserves the metric

Lemma ball_Cunit : forall e a b, ball e (Cunit a) (Cunit b) <-> ball e a b.

Lemma Cunit_eq : forall a b, st_eq (Cunit a) (Cunit b) <-> st_eq a b.

Lemma ball_approx_r : forall (x:Complete) e, ball e x (Cunit (approximate x e)).

Lemma ball_approx_l : forall (x:Complete) e, ball e (Cunit (approximate x e)) x.

Lemma ball_ex_approx_r : forall (x:Complete) e, ball_ex e x (Cunit (approximate x e)).

Lemma ball_ex_approx_l : forall (x:Complete) e, ball_ex e (Cunit (approximate x e)) x.

Lemma regFunBall_Cunit (e: Qpos) (x: Complete) (y: X):
regFunBall e x (Cunit y) <-> (forall d: Qpos, ball (d + e) (approximate x d) y ).

Lemma regFun_prf_ex :
forall (r : Complete) (e1 e2 : QposInf),
ball_ex (e1 + e2) (approximate r e1) (approximate r e2).

End RegularFunction.

Section Faster.

Variable X : MetricSpace.
Variable x : Complete X.

A regular function is equivalent to the same function that returns a better approximation with a given error. One would not generally want to do this when doing computation; however it is quite a useful substitution to be able to make during reasoning.

Section FasterInGeneral.

Variable f : Qpos -> Qpos.
Hypothesis Hf : forall x, (f x ) <= x.

Lemma fasterIsRegular : is_RegularFunction (fun e => (approximate x (QposInf_bind f e))).

Definition faster : Complete X := Build_RegularFunction fasterIsRegular.

Lemma fasterIsEq : st_eq faster x.

End FasterInGeneral.

Lemma QreduceApprox_prf : forall (e:Qpos), QposRed e <= e.

Definition QreduceApprox := faster QposRed QreduceApprox_prf.

Lemma QreduceApprox_Eq : st_eq QreduceApprox x.

In particular, halving the error of the approximation is a common case.

Lemma doubleSpeed_prf : forall (e:Qpos), ((1#2)*e)%Qpos <= e.

Definition doubleSpeed := faster (Qpos_mult (1#2)) doubleSpeed_prf.

Lemma doubleSpeed_Eq : st_eq doubleSpeed x.
End Faster.

Section Cjoin.

Variable X : MetricSpace.

Cjoin

There is an injection from a twice completed space into a once completed space. This injection along with Cunit forms an isomorphism between a twice completed space and a once completed space. This proves that a complete metric space is complete.

Definition Cjoin_raw (x:Complete (Complete X)) (e:QposInf) :=
(approximate (approximate x (QposInf_mult (1#2) e)) (QposInf_mult (1#2) e))%Qpos.

Lemma Cjoin_fun_prf (x:Complete (Complete X)) : is_RegularFunction (Cjoin_raw x).

Definition Cjoin_fun (x:Complete (Complete X)) : Complete X :=
Build_RegularFunction (Cjoin_fun_prf x).

Lemma Cjoin_prf : is_UniformlyContinuousFunction Cjoin_fun Qpos2QposInf.

Definition Cjoin : (Complete (Complete X)) --> (Complete X ) :=
Build_UniformlyContinuousFunction Cjoin_prf.

End Cjoin.

Implicit Arguments Cjoin [X].

Section Cmap.

Variable X Y : MetricSpace.
Variable f : X --> Y.

Cmap (slow)

Uniformly continuous functions can be lifted to the completion of metric spaces. A faster version that works under some mild assumptions will be given later. But first the most generic version that we call Cmap_slow.

Definition Cmap_slow_raw (x:Complete X) (e:QposInf) :=
f (approximate x (QposInf_mult (1#2)%Qpos (QposInf_bind (mu f) e))).

Lemma Cmap_slow_raw_strongInf : forall (x:Complete X) (d:QposInf) (e:QposInf), QposInf_le d (QposInf_mult (1#2)%Qpos (QposInf_bind (mu f) e)) ->
ball_ex e (f (approximate x d)) (Cmap_slow_raw x e).

Lemma Cmap_slow_raw_strong : forall (x:Complete X) (d:QposInf) (e:Qpos), QposInf_le d (QposInf_mult (1#2)%Qpos (mu f e)) ->
ball e (f (approximate x d)) (Cmap_slow_raw x e).

Lemma Cmap_slow_fun_prf (x:Complete X) : is_RegularFunction (Cmap_slow_raw x).

Definition Cmap_slow_fun (x:Complete X) : Complete Y :=
Build_RegularFunction (Cmap_slow_fun_prf x).

Definition Cmap_slow_prf : is_UniformlyContinuousFunction Cmap_slow_fun (fun e => (QposInf_mult (1#2)(mu f e))%Qpos).

Definition Cmap_slow : (Complete X ) --> (Complete Y ) :=
Build_UniformlyContinuousFunction Cmap_slow_prf.

End Cmap.

Cbind can be defined in terms of map and join

Definition Cbind_slow (X Y:MetricSpace) (f:X -->Complete Y) := uc_compose Cjoin (Cmap_slow f).

The completion operation, along with the map functor from a monad in the catagory of metric spaces.

Section Monad_Laws.

Variable X Y Z : MetricSpace.

Notation "a =m b" := (st_eq a b) (at level 70, no associativity).

Lemma MonadLaw1 : forall a, Cmap_slow_fun (uc_id X) a =m a.

Lemma MonadLaw2 : forall (f:Y --> Z) (g:X --> Y) a, Cmap_slow_fun (uc_compose f g) a =m (Cmap_slow_fun f (Cmap_slow_fun g a)).

Lemma MonadLaw3 : forall (f:X --> Y) a, (Cmap_slow_fun f (Cunit_fun _ a)) =m (Cunit_fun _ (f a)).

Lemma MonadLaw4 : forall (f:X --> Y) a, (Cmap_slow_fun f (Cjoin_fun a)) =m (Cjoin_fun ((Cmap_slow_fun (Cmap_slow f)) a)).

Lemma MonadLaw5 : forall a, (Cjoin_fun (X:=X) (Cunit_fun _ a)) =m a.

Lemma MonadLaw6 : forall a, Cjoin_fun ((Cmap_slow_fun (X:=X) Cunit) a) =m a.

Lemma MonadLaw7 : forall a, Cjoin_fun ((Cmap_slow_fun (X:=Complete (Complete X)) Cjoin) a) =m Cjoin_fun (Cjoin_fun a).

This final law isn't a monad law, rather it completes the isomorphism between a twice completed metric space and a one completed metric space.

Lemma CunitCjoin : forall a, (Cunit_fun _ (Cjoin_fun (X:=X) a)) =m a.

End Monad_Laws.

The monad laws are sometimes expressed in terms of bind and unit.

Lemma BindLaw1 : forall X Y (f:X --> Complete Y) a, (st_eq (Cbind_slow f (Cunit_fun _ a)) (f a)).

Lemma BindLaw2 : forall X a, (st_eq (Cbind_slow (Cunit:X --> Complete X) a) a).

Lemma BindLaw3 : forall X Y Z (a:Complete X) (f:X --> Complete Y) (g:Y -->Complete Z), (st_eq (Cbind_slow g (Cbind_slow f a)) (Cbind_slow (uc_compose (Cbind_slow g) f) a)).

Strong Monad

The monad is a strong monad because the map function itself is a uniformly continuous function.

Section Strong_Monad.

Variable X Y : MetricSpace.
Let X_Y := UniformlyContinuousSpace X Y.
Let CX_CY := UniformlyContinuousSpace (Complete X) (Complete Y).

Lemma Cmap_strong_slow_prf : is_UniformlyContinuousFunction ((Cmap_slow (Y:=Y)):(X_Y -> CX_CY)) Qpos2QposInf.

Definition Cmap_strong_slow : (X --> Y ) --> (Complete X --> Complete Y ) :=
Build_UniformlyContinuousFunction Cmap_strong_slow_prf.

Using strength we can show that Complete forms an applicative functor. The ap function is useful for making multiple argument maps.

Definition Cap_slow_raw (f:Complete (X --> Y)) (x:Complete X) (e:QposInf) :=
approximate (Cmap_slow (approximate f ((1#2)%Qpos*e)%QposInf) x) ((1#2)%Qpos*e)%QposInf.

Lemma Cap_slow_fun_prf (f:Complete (X --> Y)) (x:Complete X) : is_RegularFunction (Cap_slow_raw f x).

Definition Cap_slow_fun (f:Complete (X --> Y)) (x:Complete X) : Complete Y :=
Build_RegularFunction (Cap_slow_fun_prf f x).

Lemma Cap_slow_help (f:Complete (X --> Y)) (x:Complete X) (e:Qpos) :
ball e (Cap_slow_fun f x) (Cmap_slow (approximate f e) x).

Definition Cap_slow_modulus (f:Complete (X --> Y)) (e:Qpos) : QposInf := ((1#2)%Qpos*(mu (approximate f ((1#3)*e)%Qpos) ((1#3)*e)))%QposInf.

Lemma Cap_weak_slow_prf (f:Complete (X --> Y)) : is_UniformlyContinuousFunction (Cap_slow_fun f) (Cap_slow_modulus f).

Definition Cap_weak_slow (f:Complete (X --> Y)) : Complete X --> Complete Y :=
Build_UniformlyContinuousFunction (Cap_weak_slow_prf f).

Lemma Cap_slow_prf : is_UniformlyContinuousFunction Cap_weak_slow Qpos2QposInf.

Definition Cap_slow : Complete (X --> Y) --> Complete X --> Complete Y :=
Build_UniformlyContinuousFunction Cap_slow_prf.

Lemma StrongMonadLaw1 : forall a b, st_eq (Cap_slow_fun (Cunit_fun _ a) b) (Cmap_strong_slow a b).

End Strong_Monad.

A binary version of map

Definition Cmap2_slow (X Y Z:MetricSpace) (f:X --> Y --> Z) := uc_compose (@Cap_slow Y Z) (Cmap_slow f).

Completion and Classification

The completion operations preserve stability and locatedness, but it does not preserve the decidability.

Lemma Complete_stable : forall X, stableMetric X -> stableMetric (Complete X).

Lemma Complete_located : forall X, locatedMetric X -> locatedMetric (Complete X).