-
Notifications
You must be signed in to change notification settings - Fork 10
/
StateTransfThetaDens.v
154 lines (121 loc) · 4.78 KB
/
StateTransfThetaDens.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
From Coq Require Import RelationClasses.
From SSProve.Mon Require Import SPropBase.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect.
Set Warnings "notation-overridden,ambiguous-paths".
From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples.
From SSProve.Crypt Require Import ChoiceAsOrd OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples TransformingLaxMorph SubDistr Theta_dens LaxFunctorsAndTransf UniversalFreeMap FreeProbProg StateTransformingLaxMorph LaxComp.
Import SPropNotations.
(*
In this file we state transform this morphism
θdens : Frp → Sdistr
into
StT(θdens) : StT(Frp) → StT(SDistr)
We also subsequently make its domain free
θFstd : FrStP → StT(Frp) → stT(SDistr)
*)
Section GetDomainAndCodomain.
Context {C D1 D2 : ord_category} {J1 : ord_functor C D1} {J12 : ord_functor D1 D2} {J2 : ord_functor C D2}
{phi : natIso J2 (ord_functor_comp J1 J12)} (psi := ni_inv phi)
{M1 : ord_relativeMonad J1} {M2: ord_relativeMonad J2}.
Definition rlmm_domain (smTheta : relativeLaxMonadMorphism J12 phi M1 M2)
: ord_relativeMonad J1
:= M1.
Definition rlmm_codomain (smTheta : relativeLaxMonadMorphism J12 phi M1 M2)
: ord_relativeMonad J2
:= M2.
End GetDomainAndCodomain.
Section StT_unaryThetaDens.
Context {probE : Type -> Type}. (*an interface for probabilistic events*)
Context {choice_type : Type}
{chElement : choice_type -> choiceType}.
Context (prob_handler : forall (T:choiceType),
probE T -> SDistr T).
Context {S : choiceType}.
(*we wish to transform this monad morphism*)
Let θdens_filled :=
@unary_theta_dens.
(*domain and codomain*)
Let Frp := rlmm_domain θdens_filled.
(* Eval hnf in rlmm_codomain θdens_filled. (*SDistr*) *)
(*state transform the domain*)
Program Definition unaryStateTingAdj :
leftAdjunctionSituation choice_incl
(ord_functor_comp (unaryTimesS1 S) choice_incl)
(ToTheS S) :=
mkNatIso _ _ _ _ _ _ _.
Next Obligation.
move=> [A X]. unshelve econstructor.
simpl. move=> g a s. exact (g (a,s)).
move=> g g'. simpl in g. simpl in g'.
move=> Hg. unfold extract_ord. simpl.
move=> a.
unfold extract_ord in Hg. simpl in Hg.
apply boolp.funext. move=> s.
apply Hg.
Defined.
Next Obligation.
move=> [A X]. unshelve econstructor.
simpl. move=> g. move=> [a s]. exact (g a s).
simpl. move => g g'.
unfold extract_ord. simpl.
move=> Hg. move=> [a s].
specialize (Hg a). destruct Hg.
reflexivity.
Defined.
Next Obligation.
move=> [A X] [A' X']. move=> [fA fX]. simpl in *.
apply sig_eq. simpl. apply boolp.funext. move=> g.
apply boolp.funext. move=> a'. apply boolp.funext. move=> s.
simpl.
rewrite /OrderEnrichedRelativeAdjunctionsExamples.ToTheS_obligation_1.
reflexivity.
Qed.
Next Obligation.
move=> [A X].
apply sig_eq. simpl. apply boolp.funext. move=> g.
simpl. apply boolp.funext. move=> a. reflexivity.
Qed.
Next Obligation.
move=> [A X].
apply sig_eq. simpl. apply boolp.funext. move=> g.
simpl. apply boolp.funext. move=> [a s]. reflexivity.
Qed.
Program Definition unaryStateBeta' :
lnatTrans (lord_functor_comp
(strict2laxFunc (ToTheS S))
(strict2laxFunc (ord_functor_id TypeCat)))
(lord_functor_comp
(strict2laxFunc (ord_functor_id TypeCat))
(strict2laxFunc (ToTheS S))) :=
mkLnatTrans _ _.
Program Definition stT_thetaDens_adj :=
Transformed_lmla θdens_filled unaryStateTingAdj unaryStateTingAdj unaryStateBeta' _ _.
Next Obligation.
move=> A Y. move=> g.
apply boolp.funext. move=> [ a s]. cbv. reflexivity.
Qed.
Definition stT_thetaDens := rlmm_from_lmla stT_thetaDens_adj.
End StT_unaryThetaDens.
Section MakeTheDomainFree.
Context {probE : Type -> Type}. (*an interface for probabilistic events*)
Context {choice_type : Type}
{chElement : choice_type -> choiceType}.
Context {prob_handler : forall (T:choiceType),
probE T -> SDistr T}.
Context {S : choiceType}.
Let unaryIntState_filled :=
@unaryIntState S.
Let stT_thetaDens_filled :=
@stT_thetaDens S.
(*an auxiliary morphism to connect the dots*)
Program Definition bridgg :
relativeMonadMorphism (ord_functor_id _) (trivialChi)
(rlmm_codomain unaryIntState_filled)
(rlmm_domain stT_thetaDens_filled) :=
mkRelMonMorph _ _ _ _ _ _ _.
(*now... unaryIntState_filled ; bridgg = ppre*)
Let ppre := rlmm_comp _ _ _ _ _ _ _ (unaryIntState_filled) bridgg.
(*and then ppre ; stT_thetaDens_filled*)
Definition thetaFstd := rlmm_comp _ _ _ _ _ _ _ ppre stT_thetaDens_filled.
End MakeTheDomainFree.