Completion distributes over Step Functions
We prove the that StepF distributes over Complete using the function swap (which we call dist) as in Jones, Duponcheel - composing monads
The dist function exchanges StepF (under the infinity metric) and Complete monads
Definition dist_raw (x:StepFSup (Complete X)) (e:QposInf): (StepFSup X):=
(Map (fun z=> approximate z e) x).
Lemma dist_prf : forall (x:StepFSup (Complete X)),
is_RegularFunction (dist_raw x).
Definition dist1 (x:StepFSup (Complete X)): (Complete (StepFSup X)).
Defined.
Add Morphism dist1 with signature (@st_eq _)
==> (@st_eq _) as dist1_wd.
Qed.
Lemma dist1_uc : is_UniformlyContinuousFunction dist1 Qpos2QposInf.
Definition dist: (StepFSup (Complete X))-->(Complete (StepFSup X)).
Defined.
End Dist.
Definition distconst(X : MetricSpace):(Complete X)->Complete (StepFSup X).
Defined.
Lemma distConst(X : MetricSpace):forall (x:Complete X),
(st_eq (dist (constStepF x)) (distconst x)).
Lemma dist_glue(X:MetricSpace)(o:OpenUnit): forall (x y:(StepFSup (Complete X))),
(st_eq (dist (glue o x y)) (Cmap2_slow (glue_uc _ o) (dist x) (dist y))).
Section DistributionLaws.
Now we show the laws for dist are satified, except for the last one
which we have not completed yet.
Let prod(X:MetricSpace):= (uc_compose (Cmap_slow (StFJoinSup X))
(@dist (StepFSup X))).
Let dorp(X:MetricSpace):= (uc_compose Cjoin
(Cmap_slow (@dist X))).
Lemma distmapmap: forall X Y (f : UniformlyContinuousSpace X Y), (ucEq
(uc_compose (dist) (Map_uc (@Cmap_slow _ _ f)))
(uc_compose (Cmap_slow (Map_uc f)) (dist))).
Lemma distreturn: forall X,
(ucEq
(uc_compose dist (StFReturn_uc _))
(@Cmap_slow _ _ (StFReturn_uc X))).
Lemma distmapret: forall X, (ucEq
(uc_compose dist
(@Map_uc _ _ (@Cunit X)))
(@Cunit (StepFSup X))).
End DistributionLaws.