PROOF.bend
minebender-game@1.0.0.0 · 421 lines · 24 definitions
1import Base
2import minebender-game@1.0.0.0/types.bend as T
3import minebender-game@1.0.0.0/board.bend as B
4import minebender-game@1.0.0.0/game.bend as G
5import minebender-game@1.0.0.0/LAWS.bend as L
6import minebender-game@1.0.0.0/proof_base.bend as P
7import minebender-game@1.0.0.0/proof_grid.bend as PG
8import minebender-game@1.0.0.0/proof_copy.bend as PC
9import minebender-game@1.0.0.0/proof_gen.bend as PN
10import minebender-game@1.0.0.0/proof_laws.bend as PW
11import minebender-game@1.0.0.0/proof_assist.bend as PA
12import minebender-game@1.0.0.0/proof_display.bend as PD
13
14
15
16
17
18
19def L.level_beginner():
20 {==}
21
22def L.level_intermediate():
23 {==}
24
25def L.level_expert():
26 {==}
27
28def L.level_custom(w, h, m):
29 {==}
30
31
32
33
34def Bool.disc(b: Bool) -> Type:
35 match b:
36 case False{}:
37 Unit
38 case True{}:
39 Empty
40
41def Bool.false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
42 %e : Bool.disc(_)
43 Unit{}
44
45
46law open_over:
47 for +g: G.Game
48 for +p: T.Pos
49 for +over: {G.is_playing(G.status(g)) == False{} : Bool}
50 {G.open(g, p) == g : G.Game}
51
52def open_over(g, p, over):
53 match g:
54 case G.Game{w, h, layout, shown, flags, status}:
55 %Equal.sym(Bool, G.is_playing(status), False{}, over) :
56 {G.open.go(_ && G.unrevealed(w, h, shown, p), B.mine(layout, p),
57 G.Game{w, h, layout, shown, flags, status}, p)
58 == G.Game{w, h, layout, shown, flags, status} : G.Game}
59 {==}
60
61law not_playing:
62 for +s: T.Status
63 for ne: {s != T.Playing{} : T.Status}
64 {G.is_playing(s) == False{} : Bool}
65
66def not_playing(s, ne):
67 match s:
68 case T.Playing{}:
69 Empty.absurd({G.is_playing(T.Playing{}) == False{} : Bool}, ne({==}))
70 case T.Won{}:
71 {==}
72 case T.Lost{why}:
73 {==}
74
75law reveal_go_same:
76 for +b: Bool
77 for +g: G.Game
78 for +p: T.Pos
79 for +e: {G.open(g, p) == g : G.Game}
80 {G.reveal.go(b, g, p) == g : G.Game}
81
82def reveal_go_same(b, g, p, e):
83 match b:
84 case True{}:
85 {==}
86 case False{}:
87 e
88
89law reveal_over:
90 for +g: G.Game
91 for +p: T.Pos
92 for +over: {G.is_playing(G.status(g)) == False{} : Bool}
93 {G.reveal(g, p) == g : G.Game}
94
95def reveal_over(g, p, over):
96 reveal_go_same(G.flagged(g, p), g, p, open_over(g, p, over))
97
98law chord_over:
99 for +ts: List<&2, T.Pos>
100 for +g: G.Game
101 for +over: {G.is_playing(G.status(g)) == False{} : Bool}
102 {G.chord_play(ts, g) == g : G.Game}
103
104def chord_over(ts, g, over):
105 match ts:
106 case Nil{}:
107 {==}
108 case q <> t:
109 %Equal.sym(G.Game, G.reveal(g, q), g, reveal_over(g, q, over)) :
110 {G.chord_play(t, _) == g : G.Game}
111 chord_over(t, g, over)
112
113law flag_over:
114 for +g: G.Game
115 for +p: T.Pos
116 for +over: {G.is_playing(G.status(g)) == False{} : Bool}
117 {G.flag(g, p) == g : G.Game}
118
119def flag_over(g, p, over):
120 match g:
121 case G.Game{w, h, layout, shown, flags, status}:
122 %Equal.sym(Bool, G.is_playing(status), False{}, over) :
123 {G.flag.go(_ && G.unrevealed(w, h, shown, p),
124 G.Game{w, h, layout, shown, flags, status}, p)
125 == G.Game{w, h, layout, shown, flags, status} : G.Game}
126 {==}
127
128law assist_over:
129 for +g: G.Game
130 for +over: {G.is_playing(G.status(g)) == False{} : Bool}
131 for +k: Nat
132 {G.assist(g, k) == g : G.Game}
133
134def assist_over(g, over, k):
135 %Equal.sym(Bool, G.is_playing(G.status(g)), False{}, over) :
136 {G.assist.go(_, g, k) == g : G.Game}
137 {==}
138
139law frozen_:
140 for +g: G.Game
141 for over: {G.status(g) != T.Playing{} : T.Status}
142 for a: T.Action
143 {G.step(g, a) == g : G.Game}
144
145def frozen_(g, over, a):
146 match a:
147 case T.Reveal{p}:
148 reveal_over(g, p, not_playing(G.status(g), over))
149 case T.Chord{p}:
150 chord_over(G.chord_targets(g, p), g, not_playing(G.status(g), over))
151 case T.Flag{p}:
152 flag_over(g, p, not_playing(G.status(g), over))
153 case T.Assist{k}:
154 assist_over(g, not_playing(G.status(g), over), k)
155
156def L.frozen(g, over, a):
157 frozen_(g, over, a)
158
159
160
161
162law reveal_flagged_:
163 for +g: G.Game
164 for +p: T.Pos
165 for +flag: {G.flagged(g, p) == True{} : Bool}
166 {G.step(g, T.Reveal{p}) == g : G.Game}
167
168def reveal_flagged_(g, p, flag):
169 %Equal.sym(Bool, G.flagged(g, p), True{}, flag) : {G.reveal.go(_, g, p) == g : G.Game}
170 {==}
171
172def L.reveal_flagged(g, p, flag):
173 reveal_flagged_(g, p, flag)
174
175law reveal_unflagged_:
176 for +g: G.Game
177 for +p: T.Pos
178 for +flag: {G.flagged(g, p) == False{} : Bool}
179 {G.step(g, T.Reveal{p}) == G.open(g, p) : G.Game}
180
181def reveal_unflagged_(g, p, flag):
182 %Equal.sym(Bool, G.flagged(g, p), False{}, flag) :
183 {G.reveal.go(_, g, p) == G.open(g, p) : G.Game}
184 {==}
185
186def L.reveal_unflagged(g, p, flag):
187 reveal_unflagged_(g, p, flag)
188
189
190
191
192def flag_k.go(+b: Bool, +g: G.Game, +p: T.Pos) ->
193 {G.knowledge(G.flag.go(b, g, p)) == G.knowledge(g) : T.Knowledge}:
194 match b:
195 case False{}:
196 {==}
197 case True{}:
198 match g:
199 case G.Game{w, h, layout, shown, flags, status}:
200 {==}
201
202def flag_s.go(+b: Bool, +g: G.Game, +p: T.Pos) ->
203 {G.status(G.flag.go(b, g, p)) == G.status(g) : T.Status}:
204 match b:
205 case False{}:
206 {==}
207 case True{}:
208 match g:
209 case G.Game{w, h, layout, shown, flags, status}:
210 {==}
211
212law flag_no_knowledge_:
213 for +g: G.Game
214 for +p: T.Pos
215 {G.knowledge(G.step(g, T.Flag{p})) == G.knowledge(g) : T.Knowledge} &
216 {G.status(G.step(g, T.Flag{p})) == G.status(g) : T.Status}
217
218def flag_no_knowledge_(g, p):
219 (flag_k.go(G.can_flag(g, p), g, p), flag_s.go(G.can_flag(g, p), g, p))
220
221def L.flag_no_knowledge(g, p):
222 flag_no_knowledge_(g, p)
223
224def status_disc_playing(s: T.Status) -> Type:
225 match s:
226 case T.Playing{}:
227 Empty
228 case o:
229 Unit
230
231def won_ne_playing(e: {T.Won{} == T.Playing{} : T.Status}) -> Empty:
232 %e : status_disc_playing(_)
233 Unit{}
234
235def lost_ne_playing(-why: T.Loss, e: {T.Lost{why} == T.Playing{} : T.Status}) -> Empty:
236 %e : status_disc_playing(_)
237 Unit{}
238
239law flag_toggle_:
240 for +g: G.Game
241 for +playing: {G.status(g) == T.Playing{} : T.Status}
242 for +p: T.Pos
243 for +hid: {L.hidden(G.knowledge(g), p) == True{} : Bool}
244 {G.flagged(G.step(g, T.Flag{p}), p) == Bool.not(G.flagged(g, p)) : Bool}
245
246def flag_toggle_(g, playing, p, hid):
247 match g:
248 case G.Game{w, h, layout, shown, flags, status}:
249 match status:
250 case T.Playing{}:
251 +gg = {G.Game{w, h, layout, shown, flags, T.Playing{}} : G.Game}
252 +u = Equal.trans(Bool, G.unrevealed(w, h, shown, p),
253 L.hidden(G.knowledge(gg), p), True{},
254 Equal.sym(Bool, L.hidden(G.knowledge(gg), p), G.unrevealed(w, h, shown, p),
255 PG.know_hidden(w, h, layout, shown, flags, T.Playing{}, p)), hid)
256 %Equal.sym(Bool, G.unrevealed(w, h, shown, p), True{}, u) :
257 {G.flagged(G.flag.go(_, gg, p), p) == Bool.not(G.flagged(gg, p)) : Bool}
258 %Equal.sym(Bool, G.unrevealed(w, h, shown, p), True{}, u) :
259 {Bool.and(_, B.contains(G.toggle(flags, p), p))
260 == Bool.not(Bool.and(_, B.contains(flags, p))) : Bool}
261 PG.toggle_self(flags, p)
262 case T.Won{}:
263 Empty.absurd({G.flagged(G.step(G.Game{w, h, layout, shown, flags, T.Won{}}, T.Flag{p}), p)
264 == Bool.not(G.flagged(G.Game{w, h, layout, shown, flags, T.Won{}}, p)) : Bool},
265 won_ne_playing(playing))
266 case T.Lost{why}:
267 Empty.absurd({G.flagged(G.step(G.Game{w, h, layout, shown, flags, T.Lost{why}}, T.Flag{p}), p)
268 == Bool.not(G.flagged(G.Game{w, h, layout, shown, flags, T.Lost{why}}, p)) : Bool},
269 lost_ne_playing(why, playing))
270
271def L.flag_toggle(g, playing, p, hid):
272 flag_toggle_(g, playing, p, hid)
273
274def flag_others.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos,
275 d: {B.same(p, q) == False{} : Bool}) ->
276 {G.flagged(G.flag.go(c, g, p), q) == G.flagged(g, q) : Bool}:
277 match c:
278 case False{}:
279 {==}
280 case True{}:
281 match g:
282 case G.Game{w, h, layout, shown, flags, status}:
283 %Equal.sym(Bool, B.contains(G.toggle(flags, p), q), B.contains(flags, q),
284 PG.toggle_other(flags, p, q, d)) :
285 {Bool.and(G.unrevealed(w, h, shown, q), _)
286 == Bool.and(G.unrevealed(w, h, shown, q), B.contains(flags, q)) : Bool}
287 {==}
288
289law flag_others_:
290 for +g: G.Game
291 for +p: T.Pos
292 for +q: T.Pos
293 for diff: {p != q : T.Pos}
294 {G.flagged(G.step(g, T.Flag{p}), q) == G.flagged(g, q) : Bool}
295
296def flag_others_(g, p, q, diff):
297 flag_others.go(G.can_flag(g, p), g, p, q, PG.same_ne(p, q, diff))
298
299def L.flag_others(g, p, q, diff):
300 flag_others_(g, p, q, diff)
301
302law flag_revealed_:
303 for +g: G.Game
304 for +p: T.Pos
305 for +vis: {L.hidden(G.knowledge(g), p) == False{} : Bool}
306 {G.step(g, T.Flag{p}) == g : G.Game}
307
308def flag_revealed_(g, p, vis):
309 match g:
310 case G.Game{w, h, layout, shown, flags, status}:
311 +gg = {G.Game{w, h, layout, shown, flags, status} : G.Game}
312 +u = Equal.trans(Bool, G.unrevealed(w, h, shown, p),
313 L.hidden(G.knowledge(gg), p), False{},
314 Equal.sym(Bool, L.hidden(G.knowledge(gg), p), G.unrevealed(w, h, shown, p),
315 PG.know_hidden(w, h, layout, shown, flags, status, p)), vis)
316 %Equal.sym(Bool, G.unrevealed(w, h, shown, p), False{}, u) :
317 {G.flag.go(Bool.and(G.is_playing(status), _), gg, p) == gg : G.Game}
318 %Equal.sym(Bool, Bool.and(G.is_playing(status), False{}), False{},
319 P.and_false_r(G.is_playing(status))) :
320 {G.flag.go(_, gg, p) == gg : G.Game}
321 {==}
322
323def L.flag_revealed(g, p, vis):
324 flag_revealed_(g, p, vis)
325
326
327
328
329law play_reveals:
330 for +ts: List<&2, T.Pos>
331 for +g: G.Game
332 {G.chord_play(ts, g) == L.play(L.reveals(ts), g) : G.Game}
333
334def play_reveals(ts, g):
335 match ts:
336 case Nil{}:
337 {==}
338 case q <> t:
339 play_reveals(t, G.reveal(g, q))
340
341law chord_:
342 for +g: G.Game
343 for +p: T.Pos
344 {G.step(g, T.Chord{p}) == L.play(L.reveals(L.chord_targets(g, p)), g) : G.Game}
345
346def chord_(g, p):
347 %PC.chord_targets_eq(g, p) :
348 {G.chord_play(G.chord_targets(g, p), g) == L.play(L.reveals(_), g) : G.Game}
349 play_reveals(G.chord_targets(g, p), g)
350
351def L.chord(g, p):
352 chord_(g, p)
353
354
355
356
357def L.gen_shape(w, h, n, first, rs):
358 PN.gen_shape_(w, h, n, first, rs)
359
360def L.gen_count(w, h, n, first, rs, on, fits):
361 PN.gen_count_(w, h, n, first, rs, on, fits)
362
363def L.gen_first_safe(w, h, n, first, rs):
364 PN.gen_first_safe_(w, h, n, first, rs)
365
366def L.gen_opening(w, h, n, first, rs, room, q, near):
367 PN.gen_opening_(w, h, n, first, rs, room, q, near)
368
369
370
371
372def L.bridge(w, h, layout, shape, g, r):
373 PW.bridge_(w, h, layout, shape, g, r)
374
375def L.won_iff(w, h, layout, shape, g, r):
376 PW.won_iff_(w, h, layout, shape, g, r)
377
378def L.flags_hidden(w, h, layout, shape, g, r, q, flag):
379 PW.flags_hidden_(g, q, flag)
380
381def L.monotone(w, h, layout, shape, g, r, a, q, vis):
382 PW.monotone_(w, h, layout, shape, g, r, a, q, vis)
383
384
385
386
387def L.open_mine(w, h, layout, shape, g, r, playing, p, boom):
388 PW.open_mine_(w, h, layout, shape, g, r, playing, p, boom)
389
390def L.open_safe(w, h, layout, shape, g, r, playing, p, safe):
391 PW.open_safe_(w, h, layout, shape, g, r, playing, p, safe)
392
393def L.flood_complete(w, h, layout, shape, g, r, playing, p, on, q, path, walk):
394 PW.flood_complete_(w, h, layout, shape, g, r, playing, p, on, q, path, walk)
395
396def L.flood_exact(w, h, layout, shape, g, r, playing, p, q, before, after):
397 PW.flood_exact_(w, h, layout, shape, g, r, playing, p, q, before, after)
398
399
400
401
402def L.assist_stuck(w, h, layout, shape, g, r, playing, stuck, k):
403 PA.assist_stuck_(w, h, layout, shape, g, r, playing, stuck, k)
404
405def L.assist_too_early(w, h, layout, shape, g, r, playing, q, option, k):
406 PA.assist_too_early_(w, h, layout, shape, g, r, playing, q, option, k)
407
408
409
410
411def L.display_play(w, h, layout, shape, g, r, playing, p, on):
412 PD.display_play_(w, h, layout, shape, g, r, playing, p, on)
413
414def L.display_blast(w, h, layout, shape, g, r, p, lost, on):
415 PD.display_blast_(w, h, layout, shape, g, r, p, lost, on)
416
417def L.display_hint(w, h, layout, shape, g, r, s, lost, on):
418 PD.display_hint_(w, h, layout, shape, g, r, s, lost, on)
419
420def L.display_mines(w, h, layout, shape, g, r, over, q, on, m):
421 PD.display_mines_(w, h, layout, shape, g, r, over, q, on, m)