-
Notifications
You must be signed in to change notification settings - Fork 11
/
example_spark.v
299 lines (252 loc) · 9.94 KB
/
example_spark.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
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
Require Import preamble hierarchy monad_lib fail_lib.
(******************************************************************************)
(* Spark example *)
(* *)
(* see Shin-Cheng Mu, Equational Reasoning for Non-deterministic Monad: A *)
(* Case study of Spark Aggregation, TR-IIS-19-002 *)
(* *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section spark_aggregation.
Local Open Scope mprog.
Section definitions.
Variable M : altMonad.
Variables (A B : Type).
Definition deterministic A B (f : A -> M B) := exists g : A -> B, f = Ret \o g.
Variables (b : B) (mul : B -> A -> B) (add : B -> B -> B).
Let Partition A := seq A.
Let RDD A := seq (Partition A).
Definition aggregate : RDD A -> M B :=
foldl add b (o) (iperm \o map (foldl mul b)).
End definitions.
Arguments aggregate {M A B}.
Section aggregate_deterministic.
Section foldl_perm_deterministic.
Variable M : altCIMonad.
Variables (A B : Type) (op : B -> A -> B) (b : B).
Local Notation "x (.) y" := (op x y) (at level 11).
Hypothesis opP : forall (x y : A) (w : seq A),
(foldl op b w (.) x) (.) y = (foldl op b w (.) y) (.) x.
Lemma lemma32 a :
foldl op b (o) insert a = Ret \o foldl op b \o (rcons^~ a) :> (_ -> M _).
Proof.
rewrite boolp.funeqE; elim/last_ind => [/=|xs y IH].
by rewrite fcompE insertE fmapE bindretf.
rewrite fcompE.
rewrite insert_rcons.
rewrite alt_fmapDr fmapE bindretf.
rewrite -fmap_oE.
have H : forall w, foldl op b \o rcons^~ w = op^~ w \o foldl op b.
by move=> w; rewrite boolp.funeqE => ws /=; rewrite -cats1 foldl_cat.
rewrite (H y).
rewrite fmap_oE.
rewrite fcompE in IH.
rewrite IH.
rewrite -[in X in _ [~] X]bindretf.
rewrite bindretf.
rewrite -{1}compA.
rewrite fmapE bindretf.
rewrite (H a).
rewrite [in X in _ [~] X]/=.
rewrite opP.
rewrite /= -!cats1 -catA /=.
rewrite foldl_cat /=.
by rewrite altmm.
Qed.
End foldl_perm_deterministic.
Section foldl_perm_deterministic_contd.
Variable M : altCIMonad.
Variables (A B : Type) (op : B -> A -> B).
Local Notation "x (.) y" := (op x y) (at level 11).
Hypothesis opP : forall (x y : A) (w : B), (w (.) x) (.) y = (w (.) y) (.) x.
Lemma lemma31 b : foldl op b (o) iperm = Ret \o foldl op b :> (_ -> M _).
Proof.
rewrite boolp.funeqE => xs; move: xs b; elim => [/=|x xs IH] b.
by rewrite fcompE fmapE bindretf.
rewrite fcompE fmap_bind.
have opP' : forall (x y : A) (w : seq A), (foldl op b w (.) x) (.) y = (foldl op b w (.) y) (.) x.
move=> ? ? ?.
by rewrite opP.
under eq_bind do rewrite (lemma32 M opP').
transitivity ((Ret \o foldl op (b (.) x)) xs : M _); last by [].
rewrite -IH.
rewrite [in RHS]fcompE.
rewrite fmapE.
bind_ext => ys.
rewrite /= -cats1 foldl_cat /=.
congr (Ret _ : M _).
elim: ys b opP' => // y ys ih /= b opP'.
rewrite ih //=.
rewrite -/(foldl op b [::]).
by rewrite opP'.
Qed.
End foldl_perm_deterministic_contd.
Section theorem43.
Variable M : altCIMonad.
Variables (A B : Type) (b : B) (mul : B -> A -> B) (add : B -> B -> B).
Hypotheses (addA : associative add) (addC : commutative add).
Lemma aggregateE :
aggregate b mul add = Ret \o foldl add b \o map (foldl mul b) :> (_ -> M _).
Proof.
rewrite -lemma31; last by move=> x ??; rewrite -addA (addC x) addA.
by rewrite /aggregate 2!fcomp_def -compA.
Qed.
Lemma deter_aggregate : deterministic (aggregate b mul add : _ -> M _).
Proof. rewrite /deterministic aggregateE //; eexists; reflexivity. Qed.
End theorem43.
(* TODO: corollary 4.4 *)
End aggregate_deterministic.
Section determinism_implies_homomorphism.
Section homomorphism.
Variables (A B : Type) (add : B -> B -> B) (k : A -> B) (z : B).
Definition is_hom (h : seq A -> B) :=
h nil = z /\ (forall x : A, h [:: x] = k x) /\
{morph h : xs ys / xs ++ ys >-> add xs ys}.
End homomorphism.
Section lemma45.
Variable M : nondetMonad.
Variables (A B : Type) (b : B) (mul : B -> A -> B) (add : B -> B -> B).
(* TODO(rei): integrate this into a (new?) monad *)
Hypothesis idempotent_converse :
forall C m1 m2 x, m1 [~] m2 = Ret x :> M C -> m1 = ret _ x /\ m2 = ret _ x.
Hypothesis injective_return : forall C x1 x2,
Ret x1 = Ret x2 :> M C -> x1 = x2.
Hypothesis H : aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _).
Lemma lemma45a (xss : seq (seq A)) :
foldl mul b (flatten xss) = foldl add b (map (foldl mul b) xss).
Proof.
case: (@iperm_is_alt_ret M _ xss) => m Hm.
have step1 : (Ret \o foldl mul b \o flatten) xss =
(Ret \o foldl add b \o map (foldl mul b)) xss [~]
fmap (foldl add b \o map (foldl mul b)) (m : M _).
rewrite -H /aggregate iperm_o_map -fcomp_comp.
by rewrite fcompE Hm alt_fmapDr fmapE /= bindretf.
apply esym, idempotent_converse in step1.
case: step1 => step11 step12.
apply injective_return in step11.
by rewrite -step11.
Qed.
Lemma lemma45b (m : M _) (xss yss : seq (seq A)) : iperm xss = Ret yss [~] m ->
foldl add b (map (foldl mul b) xss) = foldl add b (map (foldl mul b) yss).
Proof.
move=> K.
have step1 : (Ret \o foldl mul b \o flatten) xss =
(Ret \o foldl add b \o map (foldl mul b)) yss [~]
fmap (foldl add b \o map (foldl mul b)) m.
rewrite -H /aggregate iperm_o_map -fcomp_comp.
by rewrite fcompE K alt_fmapDr fmapE /= bindretf.
have step2 : (foldl mul b \o flatten) xss =
(foldl add b \o map (foldl mul b)) yss.
apply esym, idempotent_converse in step1.
case: step1 => step11 step12.
apply injective_return in step11.
by rewrite compE -step11.
by rewrite -lemma45a.
Qed.
End lemma45.
Section theorem46.
Variable M : nondetMonad.
Variables (A B : Type) (b : B) (mul : B -> A -> B) (add : B -> B -> B).
Hypothesis idempotent_converse :
forall C m1 m2 x, m1 [~] m2 = Ret x :> M C -> m1 = ret _ x /\ m2 = ret _ x.
Hypothesis injective_return : forall C x1 x2,
Ret x1 = Ret x2 :> M C -> x1 = x2.
Lemma theorem46lid z zs : z = foldl mul b zs ->
aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) ->
z = add b z.
Proof.
move=> zzs H.
transitivity (foldl mul b (flatten [:: zs])).
by rewrite /= cats0.
transitivity (foldl add b (map (foldl mul b) [:: zs])).
have Hm : iperm [:: zs] = Ret [:: zs] [~] fail :> M _.
by rewrite /= bindretf insertE altmfail.
by rewrite (lemma45a idempotent_converse injective_return H).
by rewrite /= -zzs.
Qed.
Lemma theorem46rid z zs : z = foldl mul b zs ->
aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) ->
z = add z b.
Proof.
move=> zzs H.
transitivity (foldl mul b (flatten [:: zs; [::]])).
by rewrite /= cats0.
transitivity (foldl add b (map (foldl mul b) [:: zs; [::]])).
have [m Hm] : exists m : M _, iperm [:: zs; [::]] = Ret [:: zs; [::]] [~] m.
exact: iperm_is_alt_ret.
by rewrite (lemma45a idempotent_converse injective_return H).
rewrite /= -zzs.
by rewrite -(@theorem46lid _ zs).
Qed.
End theorem46.
Section theorem46_contd.
Variable M : nondetCIMonad.
Variables (A B : Type) (b : B) (mul : B -> A -> B) (add : B -> B -> B).
Hypothesis idempotent_converse :
forall C m1 m2 x, m1 [~] m2 = Ret x :> M C -> m1 = ret _ x /\ m2 = ret _ x.
Hypothesis injective_return : forall C x1 x2,
Ret x1 = Ret x2 :> M C -> x1 = x2.
Lemma theorem46C x xs y ys :
x = foldl mul b xs -> y = foldl mul b ys ->
aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) ->
add x y = add y x.
Proof.
move=> xxs yys.
transitivity (add x (add y b)).
by rewrite -(theorem46rid idempotent_converse injective_return yys).
transitivity (foldl add b (map (foldl mul b) [:: xs; ys])).
rewrite /= -xxs -yys.
rewrite -(theorem46rid idempotent_converse injective_return yys) //.
by rewrite -(theorem46lid idempotent_converse injective_return xxs).
transitivity (foldl add b (map (foldl mul b) [:: ys; xs])).
have [m Hm] : exists m : M _, iperm [:: xs; ys] = Ret [:: ys; xs] [~] m.
have [m Hm] := @iperm_is_alt_ret M _ [:: ys; xs].
by exists m; rewrite -Hm /= !bindretf !insertE !fmapE !bindretf /= altC.
by rewrite (lemma45b idempotent_converse injective_return H Hm).
by rewrite /= -xxs -yys -(theorem46lid idempotent_converse injective_return yys).
Qed.
(* TODO *)
Lemma theorem46A x xs y ys z zs :
x = foldl mul b xs -> y = foldl mul b ys -> z = foldl mul b zs ->
aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) ->
add x (add y z) = add (add x y) z.
Proof.
move=> xxs yys zzs H.
rewrite {1}(theorem46rid (add := add) idempotent_converse injective_return zzs) //.
Abort.
End theorem46_contd.
Section theorem47.
Variable M : nondetCIMonad.
Variables (A B : Type) (b : B) (mul : B -> A -> B) (add : B -> B -> B).
Hypothesis idempotent_converse :
forall C m1 m2 x, m1 [~] m2 = Ret x :> M C -> m1 = ret _ x /\ m2 = ret _ x.
Hypothesis injective_return : forall C x1 x2,
Ret x1 = Ret x2 :> M C -> x1 = x2.
Lemma theorem47 :
aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) ->
is_hom add (mul b) b (foldl mul b).
Proof.
move=> H.
split; first by [].
split; first by [].
move=> xs ys.
rewrite (_ : xs ++ ys = flatten [:: xs; ys]); last by rewrite /= cats0.
transitivity (foldl add b (map (foldl mul b) [:: xs; ys])).
case: (@iperm_is_alt_ret M _ [:: xs; ys]) => m Hm.
by rewrite (lemma45a idempotent_converse injective_return H).
transitivity (add (foldl mul b xs) (add (foldl mul b ys) b)).
rewrite /=.
rewrite /= -(theorem46lid (zs := xs) (mul := mul) idempotent_converse injective_return _ H) //.
by rewrite /= -(theorem46rid (zs := ys) (mul := mul) idempotent_converse injective_return _ H).
by rewrite /= -(theorem46rid (zs := ys) (mul := mul) idempotent_converse injective_return _ H).
Qed.
End theorem47.
(* TODO: corollary 4.8 *)
End determinism_implies_homomorphism.
End spark_aggregation.