Monad
Here we define bind and join for the step function monad, and prove that they satify the monad laws.
This version of StepF has type Setoid that carries its equivalence
relation with it.
We redefine several functions to return a setoid type.
Definition StFReturn (X:Setoid) : X-->(StepFS X).
Defined.
Definition SplitLS0(X:Setoid):OpenUnit->(StepFS X)->(StepFS X):=
(fun o x => SplitL x o).
Definition SplitLS(X:Setoid):OpenUnit->(StepFS X)-->(StepFS X).
Defined.
Definition SplitRS0(X:Setoid):OpenUnit->(StepFS X)->(StepFS X):=
(fun o x => SplitR x o).
Definition SplitRS(X:Setoid):OpenUnit->(StepFS X)-->(StepFS X).
Defined.
Definition MirrorS(X:Setoid):(StepFS X)-->(StepFS X).
Defined.
Definition of bind.
Definition StFBind00(X Y:Setoid) :
(StepFS X) -> (X --> (StepFS Y)) -> (StepFS Y).
Defined.
Lemma StFBind_wd1(X Y:Setoid):forall m, forall x1 x2 : X --> StepFS Y,
st_eq x1 x2 ->
st_eq (StFBind00 m x1) (StFBind00 m x2).
Definition StFBind1(X Y:Setoid) :
(StepFS X) -> (X --> (StepFS Y)) --> (StepFS Y).
Defined.
Lemma MirrorBind(X Y:Setoid):forall (x:StepF X) (f:X --> (StepFS Y)),
Mirror (StFBind00 x f)==(StFBind00 (Mirror x) (compose (MirrorS Y) f)).
Lemma SplitLBind (X Y:Setoid) : forall (y:(StepF X)) (o:OpenUnit) (f: (X-->(StepFS Y))),
SplitL (StFBind00 y f) o == StFBind00 (SplitL y o) (compose1 (SplitLS Y o) f).
Lemma SplitRBind (X Y:Setoid) : forall (y:(StepF X)) (o:OpenUnit) (f: (X-->(StepFS Y))),
SplitR (StFBind00 y f) o == StFBind00 (SplitR y o) (compose1 (SplitRS Y o) f).
Lemma StFBind_wd(X Y:Setoid): forall x1 x2 : StepFS X,
st_eq x1 x2 ->
st_eq (StFBind1 Y x1) (StFBind1 Y x2).
Definition StFBind(X Y:Setoid) :
(StepFS X) --> (X --> (StepFS Y)) --> (StepFS Y).
Defined.
Add Parametric Morphism X Y : (@StFBind00 X Y) with signature (@StepF_eq X ==> (@st_eq _) ==> @StepF_eq Y) as StFBind00_wd.
Qed.
Join is defined in terms of bind.
Definition StFJoin (X:Setoid):(StepFS (StepFS X))-->(StepFS X):=
(flip (@StFBind (StepFS X) X) (@id (StepFS X))).
Lemma JoinGlue(X:Setoid): forall o a b,
(StFJoin X (glue o a b))==(glue o (StFBind (StepFS X) _ a (SplitLS X o)) (StFBind (StepFS X) _ b (SplitRS X o))).
Section Monad_Laws.
Here we prove the monad laws.
Variable X Y:Setoid.
Lemma ReturnBind(x:X)(f:X-->StepFS Y): (StFBind X Y (StFReturn X x) f)==(f x).
Let Bind_compose(Z:Setoid)(f:X-->StepFS Y)(g:Y-->StepFS Z):=
(compose ((flip (StFBind Y Z)) g) f).
Lemma BindBind(Z:Setoid)(m:StepF X)(f:X-->StepFS Y)(g:Y-->StepFS Z):
(StFBind Y Z (StFBind X Y m f) g) == (StFBind X Z m (Bind_compose f g)).
Lemma BindReturn(m:StepF X): (StFBind X X m (StFReturn X)) == m.
End Monad_Laws.
Lemma ReturnBind(x:X)(f:X-->StepFS Y): (StFBind X Y (StFReturn X x) f)==(f x).
Let Bind_compose(Z:Setoid)(f:X-->StepFS Y)(g:Y-->StepFS Z):=
(compose ((flip (StFBind Y Z)) g) f).
Lemma BindBind(Z:Setoid)(m:StepF X)(f:X-->StepFS Y)(g:Y-->StepFS Z):
(StFBind Y Z (StFBind X Y m f) g) == (StFBind X Z m (Bind_compose f g)).
Lemma BindReturn(m:StepF X): (StFBind X X m (StFReturn X)) == m.
End Monad_Laws.
Lastly, we prove that the applicative functor is the canonical one
for this monad.