# 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.
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
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.
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.
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.

### 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.
Cbind can be defined in terms of map and join
The completion operation, along with the map functor from a monad in the catagory of metric spaces.

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.

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)).