-
Notifications
You must be signed in to change notification settings - Fork 11
/
altprob_model.v
211 lines (175 loc) · 7.35 KB
/
altprob_model.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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
Require Import Reals.
From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import reals Rstruct.
From infotheo Require Import classical_sets_ext Reals_ext ssrR fdist.
From infotheo Require Import ssrR Reals_ext proba.
From infotheo Require Import Reals_ext realType_ext.
From infotheo Require Import fsdist convex necset.
Require category.
From HB Require Import structures.
Require Import preamble hierarchy monad_lib proba_lib monad_model gcm_model.
Require Import category.
(******************************************************************************)
(* Model of the monad type altProbMonad *)
(* *)
(* gcmAP == model of a monad that combines non-deterministic choice and *)
(* probability, built on top of the geometrically convex monad *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope proba_scope.
Local Open Scope category_scope.
Section P_delta_altProbMonad.
Local Open Scope R_scope.
Local Open Scope reals_ext_scope.
Local Open Scope classical_set_scope.
Local Open Scope convex_scope.
Local Open Scope latt_scope.
Local Open Scope monae_scope.
Definition alt A (x y : gcm A) : gcm A := x [+] y.
Definition choice p A (x y : gcm A) : gcm A := x <| p |> y.
Lemma altA A : ssrfun.associative (@alt A).
Proof. by move=> x y z; rewrite /alt lubA. Qed.
Lemma image_fsdistmap A B (x : gcm A) (k : choice_of_Type A -> gcm B) :
fsdistmap k @` x = (gcm # k) x.
Proof.
rewrite /hierarchy.actm/= /actm 5!FCompE /category.actm/=.
by rewrite /free_semiCompSemiLattConvType_mor/=; unlock.
Qed.
Section funalt_funchoice.
Import category.
Import comps_notation.
Local Notation F1 := free_semiCompSemiLattConvType.
Local Notation F0 := free_convType.
Local Notation FC := free_choiceType.
Local Notation UC := forget_choiceType.
Local Notation U0 := forget_convType.
Local Notation U1 := forget_semiCompSemiLattConvType.
Lemma FunaltDr (A B : Type) (x y : gcm A) (k : A -> gcm B) :
(gcm # k) (x [+] y) = (gcm # k) x [+] (gcm # k) y.
Proof.
rewrite /hierarchy.actm /= /Monad_of_category_monad.actm /=.
by rewrite scsl_hom_is_lubmorph.
Qed.
Lemma FunpchoiceDr (A B : Type) (x y : gcm A) (k : A -> gcm B) p :
(gcm # k) (x <|p|> y) = (gcm # k) x <|p|> (gcm # k) y.
Proof.
rewrite /hierarchy.actm /= /Monad_of_category_monad.actm /=.
by rewrite scsl_hom_is_affine.
Qed.
End funalt_funchoice.
Section bindaltDl.
Import category.
Import comps_notation.
Local Notation F1 := free_semiCompSemiLattConvType.
Local Notation F0 := free_convType.
Local Notation FC := free_choiceType.
Local Notation UC := forget_choiceType.
Local Notation U0 := forget_convType.
Local Notation U1 := forget_semiCompSemiLattConvType.
Lemma affine_F1e0U1PD_alt T (u v : gcm (gcm T)) :
(F1 # eps0 (U1 (P_delta_left T)))%category (u [+] v) =
(F1 # eps0 (U1 (P_delta_left T)))%category u [+]
(F1 # eps0 (U1 (P_delta_left T)))%category v.
Proof. exact: scsl_hom_is_lubmorph. Qed.
Lemma affine_e1PD_alt T (x y : el (F1 (FId (U1 (P_delta_left T))))) :
(eps1 (P_delta_left T)) (x [+] y) =
(eps1 (P_delta_left T)) x [+] (eps1 (P_delta_left T)) y.
Proof. exact: scsl_hom_is_lubmorph. Qed.
(*
Local Notation F1o := necset_semiCompSemiLattConvType.
*)
Local Notation F0o := FSDist.t. (*FSDist_t__canonical__isConvexSpace__ConvexSpace. (* FIXME *)*)
Local Notation FCo := choice_of_Type.
Local Notation F1m := free_semiCompSemiLattConvType_mor.
Local Notation F0m := free_convType_mor.
Lemma bindaltDl : BindLaws.left_distributive (@hierarchy.bind gcm) alt.
Proof.
move=> A B x y k.
rewrite hierarchy.bindE /= /join_ -category.bindE.
by rewrite scsl_hom_is_lubmorph.
Qed.
End bindaltDl.
HB.instance Definition _ :=
@isMonadAlt.Build (Monad_of_category_monad.acto Mgcm) alt altA bindaltDl.
Lemma altxx A : idempotent (@alt A).
Proof. by move=> x; rewrite /= /alt lubxx. Qed.
Lemma altC A : commutative (@alt A).
Proof. by move=> a b; rewrite /= /alt /= lubC. Qed.
HB.instance Definition _ :=
@isMonadAltCI.Build (Monad_of_category_monad.acto Mgcm) altxx altC.
Definition gcmACI := [the altCIMonad of gcm].
Lemma choice1 A (x y : gcm A) : x <| 1%:pr |> y = x.
Proof. by rewrite conv1. Qed.
Lemma choiceC A p (x y : gcm A) : x <|p|> y = y <|(Prob.p p).~%:pr|> x.
Proof. by rewrite convC. Qed.
Lemma choicemm A p : idempotent (@choice p A).
Proof. by move=> m; rewrite /choice convmm. Qed.
Let choiceA A (p q r s : {prob R}) (x y z : gcm A) :
x <| p |> (y <| q |> z) = (x <| [r_of p, q] |> y) <| [s_of p, q] |> z.
Proof. exact: convA. Qed.
Section bindchoiceDl.
Import category.
Import comps_notation.
Local Notation F1 := free_semiCompSemiLattConvType.
Local Notation F0 := free_convType.
Local Notation FC := free_choiceType.
Local Notation UC := forget_choiceType.
Local Notation U0 := forget_convType.
Local Notation U1 := forget_semiCompSemiLattConvType.
Lemma affine_F1e0U1PD_conv T (u v : gcm (gcm T)) p :
((F1 # eps0 (U1 (P_delta_left T))) (u <|p|> v) =
(F1 # eps0 (U1 (P_delta_left T))) u <|p|>
(F1 # eps0 (U1 (P_delta_left T))) v)%category.
Proof. exact: scsl_hom_is_affine. Qed.
Lemma affine_e1PD_conv T (x y : el (F1 (FId (U1 (P_delta_left T))))) p :
(eps1 (P_delta_left T)) (x <|p|> y) =
(eps1 (P_delta_left T)) x <|p|> (eps1 (P_delta_left T)) y.
Proof. exact: scsl_hom_is_affine. Qed.
(*Local Notation F1o := necset_semiCompSemiLattConvType.*)
Local Notation F0o := FSDist.t.
Local Notation FCo := choice_of_Type.
Local Notation F1m := free_semiCompSemiLattConvType_mor.
Local Notation F0m := free_convType_mor.
Lemma bindchoiceDl p :
BindLaws.left_distributive (@hierarchy.bind gcm) (@choice p).
Proof.
move=> A B x y k.
rewrite hierarchy.bindE /= /join_ -category.bindE.
exact: scsl_hom_is_affine.
Qed.
End bindchoiceDl.
HB.instance Definition _ :=
isMonadConvex.Build R (Monad_of_category_monad.acto Mgcm)
choice1 choiceC choicemm choiceA.
HB.instance Definition _ :=
isMonadProb.Build R (Monad_of_category_monad.acto Mgcm) bindchoiceDl.
Lemma choicealtDr A (p : {prob R}) :
right_distributive (fun x y : Mgcm A => x <| p |> y) (@alt A).
Proof. by move=> x y z; rewrite /choice lubDr. Qed.
HB.instance Definition _ :=
@isMonadAltProb.Build R (Monad_of_category_monad.acto Mgcm) choicealtDr.
Definition gcmAP := [the altProbMonad R of gcm].
End P_delta_altProbMonad.
Section probabilisctic_choice_not_trivial.
Local Open Scope proba_monad_scope.
(* An example that probabilistic choice in this model is not trivial:
we can distinguish different probabilities. *)
Example gcmAP_choice_nontrivial (p q : {prob R}) :
p <> q ->
(* Ret = hierarchy.ret *)
Ret true <|p|> Ret false <>
Ret true <|q|> Ret false :> (Monad_of_category_monad.acto Mgcm) bool.
Proof.
apply contra_not.
rewrite !gcm_retE /hierarchy.choice => /(congr1 (@NECSet.sort _)).
rewrite /= !necset_convType.convE !conv_cset1 /=.
move/(@set1_inj _ (conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true).
rewrite !fsdist_convE !fsdist1xx !fsdist10//; last exact/eqP. (*TODO: we should not need that*)
by rewrite !avgRE !mulR1 ?mulR0 ?addR0 => /val_inj.
Qed.
End probabilisctic_choice_not_trivial.