proof_laws.bend
minebender-game@1.0.0.0 · 1,009 lines · 62 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_lists.bend as PL
10import minebender-game@1.0.0.0/proof_cells.bend as PS
11import minebender-game@1.0.0.0/proof_walk.bend as PW
12import minebender-game@1.0.0.0/proof_flood.bend as PF
13import minebender-game@1.0.0.0/proof_inv.bend as PI
14import minebender-game@1.0.0.0/solver.bend as S
15
16
17
18def shown_of(g: G.Game) -> T.Grid(Bool):
19 match g:
20 case G.Game{w, h, layout, shown, flags, status}:
21 shown
22
23def flags_of(g: G.Game) -> List<&2, T.Pos>:
24 match g:
25 case G.Game{w, h, layout, shown, flags, status}:
26 flags
27
28def Canon(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game) -> Type:
29 {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game} &
30 PI.Facts(w, h, layout, shown_of(g), G.status(g))
31
32
33law canon:
34 for +w: Nat
35 for +h: Nat
36 for +layout: T.Grid(Bool)
37 for +g: G.Game
38 for inv: PI.Inv(w, h, layout, g)
39 Canon(w, h, layout, g)
40
41def canon(w, h, layout, g, inv):
42 match g:
43 case G.Game{gw, gh, gl, shown, flags, status}:
44 match inv:
45 case (ew, rest):
46 match rest:
47 case (eh, rest2):
48 match rest2:
49 case (el, facts):
50 %Equal.sym(Nat, gw, w, ew) :
51 {G.Game{_, gh, gl, shown, flags, status} == G.Game{w, h, layout, shown, flags, status} : G.Game} &
52 PI.Facts(w, h, layout, shown, status)
53 %Equal.sym(Nat, gh, h, eh) :
54 {G.Game{w, _, gl, shown, flags, status} == G.Game{w, h, layout, shown, flags, status} : G.Game} &
55 PI.Facts(w, h, layout, shown, status)
56 %Equal.sym(T.Grid(Bool), gl, layout, el) :
57 {G.Game{w, h, _, shown, flags, status} == G.Game{w, h, layout, shown, flags, status} : G.Game} &
58 PI.Facts(w, h, layout, shown, status)
59 ({==}, facts)
60
61
62
63
64law know_seen:
65 for +w: Nat
66 for +h: Nat
67 for +layout: T.Grid(Bool)
68 for +shown: T.Grid(Bool)
69 for +flags: List<&2, T.Pos>
70 for +status: T.Status
71 for +q: T.Pos
72 for on: {B.on_board(w, h, q) == True{} : Bool}
73 {L.seen(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q) == G.seen_at(w, h, layout, shown, q) : T.Seen}
74
75def know_seen(w, h, layout, shown, flags, status, q, on):
76 match q:
77 case T.Pos{x, y}:
78 PG.know_at(w, h, layout, shown, x, y, on)
79
80law revealed_pick:
81 for +c: Bool
82 for +m: Bool
83 for +w: Nat
84 for +h: Nat
85 for +layout: T.Grid(Bool)
86 for +p: T.Pos
87 {Bool.not(L.is_hidden(G.seen_pick(c, m, w, h, layout, p))) == c : Bool}
88
89def revealed_pick(c, m, w, h, layout, p):
90 match c m:
91 case False{} _:
92 {==}
93 case True{} True{}:
94 {==}
95 case True{} False{}:
96 {==}
97
98
99law know_revealed:
100 for +w: Nat
101 for +h: Nat
102 for +layout: T.Grid(Bool)
103 for +shown: T.Grid(Bool)
104 for +flags: List<&2, T.Pos>
105 for +status: T.Status
106 for +q: T.Pos
107 for +on: {B.on_board(w, h, q) == True{} : Bool}
108 {L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q) == B.at(Bool, False{}, shown, q) : Bool}
109
110def know_revealed(w, h, layout, shown, flags, status, q, on):
111 match q:
112 case T.Pos{x, y}:
113 +rows = G.know_rows(w, h, layout, shown, List.range(h))
114 +p = {T.Pos{x, y} : T.Pos}
115 %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
116 {Bool.and(_, Bool.not(L.is_hidden(L.at(T.Seen, T.Hidden{}, rows, p)))) == B.at(Bool, False{}, shown, p) : Bool}
117 %Equal.sym(T.Seen, L.at(T.Seen, T.Hidden{}, rows, p), G.seen_at(w, h, layout, shown, p),
118 PG.know_at(w, h, layout, shown, x, y, on)) :
119 {Bool.not(L.is_hidden(_)) == B.at(Bool, False{}, shown, p) : Bool}
120 revealed_pick(B.at(Bool, False{}, shown, p), B.mine(layout, p), w, h, layout, p)
121
122
123
124
125law know_row_len:
126 for +w: Nat
127 for +h: Nat
128 for +layout: T.Grid(Bool)
129 for +shown: T.Grid(Bool)
130 for +y: Nat
131 for +xs: List<&2, Nat>
132 {List.length(&2, T.Seen, G.know_row(w, h, layout, shown, y, xs)) == List.length(&2, Nat, xs) : Nat}
133
134def know_row_len(w, h, layout, shown, y, xs):
135 match xs:
136 case Nil{}:
137 {==}
138 case x <> t:
139 %Equal.sym(Nat, List.length(&2, T.Seen, G.know_row(w, h, layout, shown, y, t)), List.length(&2, Nat, t),
140 know_row_len(w, h, layout, shown, y, t)) : {1n+_ == 1n+List.length(&2, Nat, t) : Nat}
141 {==}
142
143law know_rows_len:
144 for +w: Nat
145 for +h: Nat
146 for +layout: T.Grid(Bool)
147 for +shown: T.Grid(Bool)
148 for +ys: List<&2, Nat>
149 {List.length(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, ys)) == List.length(&2, Nat, ys) : Nat}
150
151def know_rows_len(w, h, layout, shown, ys):
152 match ys:
153 case Nil{}:
154 {==}
155 case y <> t:
156 %Equal.sym(Nat, List.length(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, t)), List.length(&2, Nat, t),
157 know_rows_len(w, h, layout, shown, t)) : {1n+_ == 1n+List.length(&2, Nat, t) : Nat}
158 {==}
159
160law know_rows_wide:
161 for +w: Nat
162 for +h: Nat
163 for +layout: T.Grid(Bool)
164 for +shown: T.Grid(Bool)
165 for +ys: List<&2, Nat>
166 {L.rows_wide(T.Seen, w, G.know_rows(w, h, layout, shown, ys)) == True{} : Bool}
167
168def know_rows_wide(w, h, layout, shown, ys):
169 match ys:
170 case Nil{}:
171 {==}
172 case y <> t:
173 +row = G.know_row(w, h, layout, shown, y, List.range(w))
174 %Equal.sym(Nat, List.length(&2, T.Seen, row), w,
175 Equal.trans(Nat, List.length(&2, T.Seen, row), List.length(&2, Nat, List.range(w)), w,
176 know_row_len(w, h, layout, shown, y, List.range(w)), P.range_length(w))) :
177 {Bool.and(Nat.is_eq(_, w), L.rows_wide(T.Seen, w, G.know_rows(w, h, layout, shown, t))) == True{} : Bool}
178 %Equal.sym(Bool, Nat.is_eq(w, w), True{}, P.eq_refl(w)) :
179 {Bool.and(_, L.rows_wide(T.Seen, w, G.know_rows(w, h, layout, shown, t))) == True{} : Bool}
180 know_rows_wide(w, h, layout, shown, t)
181
182law know_shaped:
183 for +w: Nat
184 for +h: Nat
185 for +layout: T.Grid(Bool)
186 for +shown: T.Grid(Bool)
187 {L.shaped(T.Seen, w, h, G.know_rows(w, h, layout, shown, List.range(h))) == True{} : Bool}
188
189def know_shaped(w, h, layout, shown):
190 +rows = G.know_rows(w, h, layout, shown, List.range(h))
191 %Equal.sym(Nat, List.length(&2, List<&2, T.Seen>, rows), h,
192 Equal.trans(Nat, List.length(&2, List<&2, T.Seen>, rows), List.length(&2, Nat, List.range(h)), h,
193 know_rows_len(w, h, layout, shown, List.range(h)), P.range_length(h))) :
194 {Bool.and(Nat.is_eq(_, h), L.rows_wide(T.Seen, w, rows)) == True{} : Bool}
195 %Equal.sym(Bool, Nat.is_eq(h, h), True{}, P.eq_refl(h)) : {Bool.and(_, L.rows_wide(T.Seen, w, rows)) == True{} : Bool}
196 know_rows_wide(w, h, layout, shown, List.range(h))
197
198def agrees_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos, +c: Bool, +m: Bool,
199 me: {B.mine(layout, p) == m : Bool}) ->
200 {L.agrees(w, h, layout, p, G.seen_pick(c, m, w, h, layout, p)) == True{} : Bool}:
201 match c m:
202 case False{} _:
203 {==}
204 case True{} True{}:
205 %PC.mine_eq(layout, p) : {_ == True{} : Bool}
206 me
207 case True{} False{}:
208 %PC.mine_eq(layout, p) :
209 {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
210 %Equal.sym(Bool, B.mine(layout, p), False{}, me) :
211 {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
212 %PC.adj_mines_eq(w, h, layout, p) :
213 {Bool.and(True{}, Nat.is_eq(_, B.adj_mines(w, h, layout, p))) == True{} : Bool}
214 P.eq_refl(B.adj_mines(w, h, layout, p))
215
216def agrees_cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
217 on: {B.on_board(w, h, p) == True{} : Bool}) ->
218 {L.agrees(w, h, layout, p, L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), p)) == True{} : Bool}:
219 match p:
220 case T.Pos{x, y}:
221 +q = {T.Pos{x, y} : T.Pos}
222 %Equal.sym(T.Seen, L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), q),
223 G.seen_at(w, h, layout, shown, q), PG.know_at(w, h, layout, shown, x, y, on)) :
224 {L.agrees(w, h, layout, q, _) == True{} : Bool}
225 agrees_pick(w, h, layout, q, B.at(Bool, False{}, shown, q), B.mine(layout, q), {==})
226
227def agrees_all_cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), ps: List<&2, T.Pos>,
228 +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
229 {L.agrees_all(w, h, G.know_rows(w, h, layout, shown, List.range(h)), layout, ps) == True{} : Bool}:
230 match ps:
231 case Nil{}:
232 {==}
233 case +q <> +t:
234 +rows = G.know_rows(w, h, layout, shown, List.range(h))
235 %Equal.sym(Bool, L.agrees(w, h, layout, q, L.at(T.Seen, T.Hidden{}, rows, q)), True{},
236 agrees_cell(w, h, layout, shown, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
237 {Bool.and(_, L.agrees_all(w, h, rows, layout, t)) == True{} : Bool}
238 agrees_all_cells(w, h, layout, shown, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))
239
240law bridge_canon:
241 for +w: Nat
242 for +h: Nat
243 for +layout: T.Grid(Bool)
244 for +shown: T.Grid(Bool)
245 for +flags: List<&2, T.Pos>
246 for +status: T.Status
247 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
248 {L.consistent(G.knowledge(G.Game{w, h, layout, shown, flags, status}), layout) == True{} : Bool}
249
250def bridge_canon(w, h, layout, shown, flags, status, shape):
251 +rows = G.know_rows(w, h, layout, shown, List.range(h))
252 PW.and4_intro(L.shaped(Bool, w, h, layout), L.shaped(T.Seen, w, h, rows),
253 Nat.is_eq(L.total_mines(layout), B.total_mines(layout)), L.agrees_all(w, h, rows, layout, L.cells(w, h)),
254 shape, know_shaped(w, h, layout, shown),
255 %PC.total_mines_eq(layout) : {Nat.is_eq(_, B.total_mines(layout)) == True{} : Bool};
256 P.eq_refl(B.total_mines(layout)),
257 %PC.cells_eq(w, h) : {L.agrees_all(w, h, rows, layout, _) == True{} : Bool};
258 agrees_all_cells(w, h, layout, shown, B.cells(w, h), PS.cells_on(w, h)))
259
260def bridge.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
261 shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}, c: Canon(w, h, layout, g)) ->
262 {L.consistent(G.knowledge(g), layout) == True{} : Bool}:
263 match c:
264 case (eg, facts):
265 %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
266 {L.consistent(G.knowledge(_), layout) == True{} : Bool}
267 bridge_canon(w, h, layout, shown_of(g), flags_of(g), G.status(g), shape)
268
269law bridge_:
270 for +w: Nat
271 for +h: Nat
272 for +layout: T.Grid(Bool)
273 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
274 for +g: G.Game
275 for r: L.Reachable(w, h, layout, g)
276 {L.consistent(G.knowledge(g), layout) == True{} : Bool}
277
278def bridge_(w, h, layout, shape, g, r):
279 bridge.k(w, h, layout, g, shape, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
280
281
282
283
284def safe_rev_cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
285 +status: T.Status, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}) ->
286 {Bool.or(L.mine(layout, q), L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q))
287 == Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) : Bool}:
288 %PC.mine_eq(layout, q) :
289 {Bool.or(_, L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q))
290 == Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) : Bool}
291 %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q), B.at(Bool, False{}, shown, q),
292 know_revealed(w, h, layout, shown, flags, status, q, on)) :
293 {Bool.or(B.mine(layout, q), _) == Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) : Bool}
294 {==}
295
296def safe_rev_all(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
297 +status: T.Status, ps: List<&2, T.Pos>, +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
298 {L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, shown, flags, status}), layout, ps)
299 == G.all_safe.go(layout, shown, ps) : Bool}:
300 match ps:
301 case Nil{}:
302 {==}
303 case +q <> +t:
304 +v = G.knowledge(G.Game{w, h, layout, shown, flags, status})
305 %Equal.sym(Bool, Bool.or(L.mine(layout, q), L.revealed(v, q)), Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)),
306 safe_rev_cell(w, h, layout, shown, flags, status, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
307 {Bool.and(_, L.all_safe_revealed.go(v, layout, t))
308 == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
309 %Equal.sym(Bool, L.all_safe_revealed.go(v, layout, t), G.all_safe.go(layout, shown, t),
310 safe_rev_all(w, h, layout, shown, flags, status, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
311 {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), _)
312 == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
313 {==}
314
315def won_iff.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, c: Canon(w, h, layout, g)) ->
316 {L.is_won(G.status(g)) == L.all_safe_revealed(G.knowledge(g), layout) : Bool}:
317 match c:
318 case (eg, facts):
319 match facts:
320 case (sh, f2):
321 match f2:
322 case (won, f3):
323 %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
324 {L.is_won(G.status(_)) == L.all_safe_revealed(G.knowledge(_), layout) : Bool}
325 +s = shown_of(g)
326 +f = flags_of(g)
327 +st = G.status(g)
328 %PC.cells_eq(w, h) :
329 {L.is_won(st) == L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, _) : Bool}
330 %Equal.sym(Bool, L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, B.cells(w, h)),
331 G.all_safe.go(layout, s, B.cells(w, h)), safe_rev_all(w, h, layout, s, f, st, B.cells(w, h), PS.cells_on(w, h))) :
332 {L.is_won(st) == _ : Bool}
333 won
334
335law won_iff_:
336 for +w: Nat
337 for +h: Nat
338 for +layout: T.Grid(Bool)
339 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
340 for +g: G.Game
341 for r: L.Reachable(w, h, layout, g)
342 {L.is_won(G.status(g)) == L.all_safe_revealed(G.knowledge(g), layout) : Bool}
343
344def won_iff_(w, h, layout, shape, g, r):
345 won_iff.k(w, h, layout, g, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
346
347
348
349
350law flags_hidden_:
351 for +g: G.Game
352 for +q: T.Pos
353 for flag: {G.flagged(g, q) == True{} : Bool}
354 {L.hidden(G.knowledge(g), q) == True{} : Bool}
355
356def flags_hidden_(g, q, flag):
357 match g:
358 case G.Game{w, h, layout, shown, flags, status}:
359 %Equal.sym(Bool, L.hidden(G.knowledge(G.Game{w, h, layout, shown, flags, status}), q), G.unrevealed(w, h, shown, q),
360 PG.know_hidden(w, h, layout, shown, flags, status, q)) : {_ == True{} : Bool}
361 P.and_true_l(G.unrevealed(w, h, shown, q), B.contains(flags, q), flag)
362
363
364
365
366def open_mono.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
367 +status: T.Status, +p: T.Pos, +q: T.Pos, s: {B.at(Bool, False{}, shown, q) == True{} : Bool}, +c: Bool, +m: Bool) ->
368 {B.at(Bool, False{}, shown_of(G.open.go(c, m, G.Game{w, h, layout, shown, flags, status}, p)), q) == True{} : Bool}:
369 match c m:
370 case False{} _:
371 s
372 case True{} True{}:
373 PF.at_set_mono(shown, p, q, s)
374 case True{} False{}:
375 +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
376 PF.flood_mono(B.count_false(shown), start, G.head_hidden(w, h, shown, start), w, h, layout, shown, q, s)
377
378law open_mono:
379 for +g: G.Game
380 for +p: T.Pos
381 for +q: T.Pos
382 for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
383 {B.at(Bool, False{}, shown_of(G.open(g, p)), q) == True{} : Bool}
384
385def open_mono(g, p, q, s):
386 match g:
387 case G.Game{w, h, layout, shown, flags, status}:
388 open_mono.go(w, h, layout, shown, flags, status, p, q, s,
389 Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)), B.mine(layout, p))
390
391def reveal_mono.go(+g: G.Game, +p: T.Pos, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}, +f: Bool) ->
392 {B.at(Bool, False{}, shown_of(G.reveal.go(f, g, p)), q) == True{} : Bool}:
393 match f:
394 case True{}:
395 s
396 case False{}:
397 open_mono(g, p, q, s)
398
399law reveal_mono:
400 for +g: G.Game
401 for +p: T.Pos
402 for +q: T.Pos
403 for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
404 {B.at(Bool, False{}, shown_of(G.reveal(g, p)), q) == True{} : Bool}
405
406def reveal_mono(g, p, q, s):
407 reveal_mono.go(g, p, q, s, G.flagged(g, p))
408
409law chord_mono:
410 for +ts: List<&2, T.Pos>
411 for +g: G.Game
412 for +q: T.Pos
413 for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
414 {B.at(Bool, False{}, shown_of(G.chord_play(ts, g)), q) == True{} : Bool}
415
416def chord_mono(ts, g, q, s):
417 match ts:
418 case Nil{}:
419 s
420 case p <> t:
421 chord_mono(t, G.reveal(g, p), q, reveal_mono(g, p, q, s))
422
423def flag_mono.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}) ->
424 {B.at(Bool, False{}, shown_of(G.flag.go(c, g, p)), q) == True{} : Bool}:
425 match c:
426 case False{}:
427 s
428 case True{}:
429 match g:
430 case G.Game{w, h, layout, shown, flags, status}:
431 s
432
433def assist_mono.safe(+g: G.Game, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool},
434 +m: Maybe<&2, T.Pos>) -> {B.at(Bool, False{}, shown_of(G.assist.safe(m, g)), q) == True{} : Bool}:
435 match m:
436 case None{}:
437 s
438 case Some{p}:
439 open_mono(g, p, q, s)
440
441def assist_mono.pick(+r: Maybe<&2, T.Pos>, +g: G.Game, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}, +k: Nat) ->
442 {B.at(Bool, False{}, shown_of(G.assist.pick(r, g, k)), q) == True{} : Bool}:
443 match r:
444 case Some{x}:
445 match g:
446 case G.Game{w, h, layout, shown, flags, status}:
447 s
448 case None{}:
449 assist_mono.safe(g, q, s, G.safe_cell(g, k))
450
451def assist_mono.go(+g: G.Game, +q: T.Pos, s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}, +c: Bool, +k: Nat) ->
452 {B.at(Bool, False{}, shown_of(G.assist.go(c, g, k)), q) == True{} : Bool}:
453 match c:
454 case False{}:
455 s
456 case True{}:
457 assist_mono.pick(S.solve(G.knowledge(g)), g, q, s, k)
458
459law step_mono:
460 for +g: G.Game
461 for +a: T.Action
462 for +q: T.Pos
463 for s: {B.at(Bool, False{}, shown_of(g), q) == True{} : Bool}
464 {B.at(Bool, False{}, shown_of(G.step(g, a)), q) == True{} : Bool}
465
466def step_mono(g, a, q, s):
467 match a:
468 case T.Reveal{p}:
469 reveal_mono(g, p, q, s)
470 case T.Chord{p}:
471 chord_mono(G.chord_targets(g, p), g, q, s)
472 case T.Flag{p}:
473 flag_mono.go(G.can_flag(g, p), g, p, q, s)
474 case T.Assist{k}:
475 assist_mono.go(g, q, s, G.is_playing(G.status(g)), k)
476
477law inv_of:
478 for +w: Nat
479 for +h: Nat
480 for +layout: T.Grid(Bool)
481 for +g: G.Game
482 for +acts: List<&2, T.Action>
483 for +e: {L.play(acts, G.fresh(w, h, layout)) == g : G.Game}
484 PI.Inv(w, h, layout, g)
485
486def inv_of(w, h, layout, g, acts, e):
487 %e : PI.Inv(w, h, layout, _)
488 PI.inv_play(w, h, layout, acts, G.fresh(w, h, layout), PI.inv_fresh(w, h, layout))
489
490
491def vis_parts(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +st: T.Status,
492 +q: T.Pos, vis: {L.revealed(G.knowledge(G.Game{w, h, layout, s, f, st}), q) == True{} : Bool}) ->
493 {B.on_board(w, h, q) == True{} : Bool}:
494 match q:
495 case T.Pos{x, y}:
496 P.and_true_l(L.on_board(w, h, T.Pos{x, y}),
497 Bool.not(L.is_hidden(L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, s, List.range(h)), T.Pos{x, y}))), vis)
498
499def monotone.k2(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
500 vis: {L.revealed(G.knowledge(g), q) == True{} : Bool},
501 +eg: {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game},
502 eg2: {G.step(g, a) == G.Game{w, h, layout, shown_of(G.step(g, a)), flags_of(G.step(g, a)), G.status(G.step(g, a))} : G.Game}) ->
503 {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
504 +s1 = shown_of(g)
505 +f1 = flags_of(g)
506 +t1 = G.status(g)
507 +g2 = G.step(g, a)
508 +s2 = shown_of(g2)
509 +f2 = flags_of(g2)
510 +t2 = G.status(g2)
511 +vis1 = {%eg : {L.revealed(G.knowledge(_), q) == True{} : Bool};
512 vis : {L.revealed(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) == True{} : Bool}}
513 +on = vis_parts(w, h, layout, s1, f1, t1, q, vis1)
514 +at1 = {%know_revealed(w, h, layout, s1, f1, t1, q, on) : {_ == True{} : Bool};
515 vis1 : {B.at(Bool, False{}, s1, q) == True{} : Bool}}
516 +at2 = step_mono(g, a, q, at1)
517 %Equal.sym(G.Game, g2, G.Game{w, h, layout, s2, f2, t2}, eg2) :
518 {L.seen(G.knowledge(_), q) == L.seen(G.knowledge(g), q) : T.Seen}
519 %Equal.sym(G.Game, g, G.Game{w, h, layout, s1, f1, t1}, eg) :
520 {L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q) == L.seen(G.knowledge(_), q) : T.Seen}
521 %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q), G.seen_at(w, h, layout, s2, q),
522 know_seen(w, h, layout, s2, f2, t2, q, on)) :
523 {_ == L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) : T.Seen}
524 %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q), G.seen_at(w, h, layout, s1, q),
525 know_seen(w, h, layout, s1, f1, t1, q, on)) :
526 {G.seen_at(w, h, layout, s2, q) == _ : T.Seen}
527 %Equal.sym(Bool, B.at(Bool, False{}, s2, q), True{}, at2) :
528 {G.seen_pick(_, B.mine(layout, q), w, h, layout, q) == G.seen_pick(B.at(Bool, False{}, s1, q), B.mine(layout, q), w, h, layout, q) : T.Seen}
529 %Equal.sym(Bool, B.at(Bool, False{}, s1, q), True{}, at1) :
530 {G.seen_pick(True{}, B.mine(layout, q), w, h, layout, q) == G.seen_pick(_, B.mine(layout, q), w, h, layout, q) : T.Seen}
531 {==}
532
533def monotone.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
534 vis: {L.revealed(G.knowledge(g), q) == True{} : Bool}, c1: Canon(w, h, layout, g),
535 c2: Canon(w, h, layout, G.step(g, a))) ->
536 {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
537 match c1:
538 case (eg, f1):
539 match c2:
540 case (eg2, f2):
541 monotone.k2(w, h, layout, g, a, q, vis, eg, eg2)
542
543def monotone.r(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
544 vis: {L.revealed(G.knowledge(g), q) == True{} : Bool}, +acts: List<&2, T.Action>,
545 +e: {L.play(acts, G.fresh(w, h, layout)) == g : G.Game}) ->
546 {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
547 monotone.k(w, h, layout, g, a, q, vis, canon(w, h, layout, g, inv_of(w, h, layout, g, acts, e)),
548 canon(w, h, layout, G.step(g, a), PI.inv_step(w, h, layout, g, inv_of(w, h, layout, g, acts, e), a)))
549
550law monotone_:
551 for +w: Nat
552 for +h: Nat
553 for +layout: T.Grid(Bool)
554 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
555 for +g: G.Game
556 for r: L.Reachable(w, h, layout, g)
557 for +a: T.Action
558 for +q: T.Pos
559 for vis: {L.revealed(G.knowledge(g), q) == True{} : Bool}
560 {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}
561
562def monotone_(w, h, layout, shape, g, r, a, q, vis):
563 match r:
564 case (acts, e):
565 monotone.r(w, h, layout, g, a, q, vis, acts, e)
566
567
568
569
570def mine_on.col(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +x: Nat, +y: Nat,
571 +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool}, yh: {Nat.is_lt(y, h) == True{} : Bool},
572 m: {Maybe.default(&2, Bool, List.get(&2, Bool, PL.row_of(Bool, layout, y), x), False{}) == True{} : Bool},
573 +b: Bool, be: {Nat.is_lt(x, w) == b : Bool}) -> {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}:
574 match b:
575 case True{}:
576 %Equal.sym(Bool, Nat.is_lt(x, w), True{}, be) : {Bool.and(_, Nat.is_lt(y, h)) == True{} : Bool}
577 yh
578 case False{}:
579 +row = PL.row_of(Bool, layout, y)
580 Empty.absurd({B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
581 P.false_ne_true(%P.get_out(Bool, row, x,
582 %Equal.sym(Nat, List.length(&2, Bool, row), w, PL.row_in_len(Bool, w, h, layout, y, sh, yh)) :
583 {Nat.is_lt(x, _) == False{} : Bool}; be) :
584 {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; m))
585
586def mine_on.row(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +x: Nat, +y: Nat,
587 +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool},
588 m: {B.mine(layout, T.Pos{x, y}) == True{} : Bool}, +b: Bool, +be: {Nat.is_lt(y, h) == b : Bool}) ->
589 {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}:
590 match b:
591 case True{}:
592 mine_on.col(w, h, layout, x, y, sh, be,
593 %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, layout, y), Some{PL.row_of(Bool, layout, y)},
594 PL.row_in_get(Bool, w, h, layout, y, sh, be)) :
595 {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{}) == True{} : Bool};
596 m, Nat.is_lt(x, w), {==})
597 case False{}:
598 Empty.absurd({B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
599 P.false_ne_true(%P.get_out(List<&2, Bool>, layout, y,
600 %Equal.sym(Nat, List.length(&2, List<&2, Bool>, layout), h, PL.shaped_len(Bool, w, h, layout, sh)) :
601 {Nat.is_lt(y, _) == False{} : Bool}; be) :
602 {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
603 == True{} : Bool}; m))
604
605
606law mine_on:
607 for +w: Nat
608 for +h: Nat
609 for +layout: T.Grid(Bool)
610 for +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool}
611 for +p: T.Pos
612 for m: {B.mine(layout, p) == True{} : Bool}
613 {B.on_board(w, h, p) == True{} : Bool}
614
615def mine_on(w, h, layout, sh, p, m):
616 match p:
617 case T.Pos{x, y}:
618 mine_on.row(w, h, layout, x, y, sh, m, Nat.is_lt(y, h), {==})
619
620
621law path_closed:
622 for +path: List<&2, T.Pos>
623 for +w: Nat
624 for +h: Nat
625 for +layout: T.Grid(Bool)
626 for +g: T.Grid(Bool)
627 for +cl: {PI.closed(w, h, layout, g) == True{} : Bool}
628 for +s: T.Pos
629 for +q: T.Pos
630 for gs: {B.at(Bool, False{}, g, s) == True{} : Bool}
631 for +wk: {L.zero_walk(path, w, h, layout, s, q) == True{} : Bool}
632 {B.at(Bool, False{}, g, q) == True{} : Bool}
633
634def path_closed(path, w, h, layout, g, cl, s, q, gs, wk):
635 match path:
636 case Nil{}:
637 %PW.lsame_sound(s, q, wk) : {B.at(Bool, False{}, g, _) == True{} : Bool}
638 gs
639 case r <> t:
640 +zs = L.zero(w, h, layout, s)
641 +sr = L.adjacent(s, r)
642 +orr = L.on_board(w, h, r)
643 +rest = L.zero_walk(t, w, h, layout, r, q)
644 +zsB = {%Equal.sym(Bool, B.zero(w, h, layout, s), L.zero(w, h, layout, s), PC.zero_eq(w, h, layout, s)) :
645 {_ == True{} : Bool}; PW.and4_a(zs, sr, orr, rest, wk) :
646 {B.zero(w, h, layout, s) == True{} : Bool}}
647 +onsB = P.and_true_l(B.on_board(w, h, s), Bool.not(B.mine(layout, s)),
648 P.and_true_l(Bool.and(B.on_board(w, h, s), Bool.not(B.mine(layout, s))),
649 Nat.is_eq(B.adj_mines(w, h, layout, s), 0n), zsB))
650 +rm = PS.neighbours_member(w, h, s, r,
651 %Equal.sym(Bool, B.on_board(w, h, r), L.on_board(w, h, r), PC.on_board_eq(w, h, r)) :
652 {_ == True{} : Bool}; PW.and4_c(zs, sr, orr, rest, wk),
653 %Equal.sym(Bool, B.adjacent(s, r), L.adjacent(s, r), PC.adjacent_eq(s, r)) :
654 {_ == True{} : Bool}; PW.and4_b(zs, sr, orr, rest, wk))
655 path_closed(t, w, h, layout, g, cl, r, q,
656 PI.closed_use(w, h, layout, g, cl, s, onsB, gs, zsB, r, rm), PW.and4_d(zs, sr, orr, rest, wk))
657
658def unrev_true(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +p: T.Pos, on: {B.on_board(w, h, p) == True{} : Bool},
659 hid: {B.at(Bool, False{}, shown, p) == False{} : Bool}) -> {G.unrevealed(w, h, shown, p) == True{} : Bool}:
660 %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
661 {Bool.and(_, Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool}
662 %Equal.sym(Bool, B.at(Bool, False{}, shown, p), False{}, hid) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
663 {==}
664
665def is_lost_wop(+b: Bool) -> {L.is_lost(G.won_or_playing(b)) == False{} : Bool}:
666 match b:
667 case True{}:
668 {==}
669 case False{}:
670 {==}
671
672def start_ok(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos) ->
673 {PF.works_ok({[G.Work{p, Nil{}}] : List<&2, G.Work>}, w, h, layout, p) == True{} : Bool}:
674 %Equal.sym(Bool, L.same(p, p), True{}, PW.lsame_refl(p)) : {Bool.and(_, True{}) == True{} : Bool}
675 {==}
676
677def start_has(+p: T.Pos) -> {PF.wcontains({[G.Work{p, Nil{}}] : List<&2, G.Work>}, p) == True{} : Bool}:
678 %Equal.sym(Bool, B.same(p, p), True{}, PG.same_refl(p)) : {Bool.or(_, False{}) == True{} : Bool}
679 {==}
680
681
682
683
684law open_mine_c:
685 for +w: Nat
686 for +h: Nat
687 for +layout: T.Grid(Bool)
688 for +s: T.Grid(Bool)
689 for +f: List<&2, T.Pos>
690 for +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}
691 for +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}
692 for +ns: {PI.nsm(w, h, layout, s) == True{} : Bool}
693 for +p: T.Pos
694 for +bm: {B.mine(layout, p) == True{} : Bool}
695 {G.status(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)) == T.Lost{T.Exploded{p}} : T.Status} &
696 {L.seen(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), p) == T.Boom{} : T.Seen}
697
698def open_mine_c(w, h, layout, s, f, shL, shS, ns, p, bm):
699 +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
700 +on = mine_on(w, h, layout, shL, p, bm)
701 +u = unrev_true(w, h, s, p, on, PI.nsm_use(w, h, layout, s, ns, p, on, bm))
702 +s2 = B.set_at(Bool, s, p, True{})
703 %Equal.sym(Bool, G.unrevealed(w, h, s, p), True{}, u) :
704 {G.status(G.open.go(_, B.mine(layout, p), g0, p)) == T.Lost{T.Exploded{p}} : T.Status} &
705 {L.seen(G.knowledge(G.open.go(_, B.mine(layout, p), g0, p)), p) == T.Boom{} : T.Seen}
706 %Equal.sym(Bool, B.mine(layout, p), True{}, bm) :
707 {G.status(G.open.go(True{}, _, g0, p)) == T.Lost{T.Exploded{p}} : T.Status} &
708 {L.seen(G.knowledge(G.open.go(True{}, _, g0, p)), p) == T.Boom{} : T.Seen}
709 ({==},
710 %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s2, f, T.Lost{T.Exploded{p}}}), p),
711 G.seen_at(w, h, layout, s2, p), know_seen(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, p, on)) :
712 {_ == T.Boom{} : T.Seen};
713 %Equal.sym(Bool, B.at(Bool, False{}, s2, p), True{}, PF.at_set_on(w, h, s, p, shS, on)) :
714 {G.seen_pick(_, B.mine(layout, p), w, h, layout, p) == T.Boom{} : T.Seen};
715 %Equal.sym(Bool, B.mine(layout, p), True{}, bm) :
716 {G.seen_pick(True{}, _, w, h, layout, p) == T.Boom{} : T.Seen};
717 {==})
718
719
720
721
722def open_safe_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +p: T.Pos,
723 bm: {B.mine(layout, p) == False{} : Bool}, +c: Bool) ->
724 {L.is_lost(G.status(G.open.go(c, B.mine(layout, p), G.Game{w, h, layout, s, f, T.Playing{}}, p))) == False{} : Bool}:
725 match c:
726 case False{}:
727 {==}
728 case True{}:
729 +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
730 %Equal.sym(Bool, B.mine(layout, p), False{}, bm) :
731 {L.is_lost(G.status(G.open.go(True{}, _, g0, p))) == False{} : Bool}
732 +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
733 is_lost_wop(G.all_safe(w, h, layout,
734 G.flood(B.count_false(s), start, G.head_hidden(w, h, s, start), w, h, layout, s)))
735
736law open_safe_c:
737 for +w: Nat
738 for +h: Nat
739 for +layout: T.Grid(Bool)
740 for +s: T.Grid(Bool)
741 for +f: List<&2, T.Pos>
742 for +p: T.Pos
743 for bm: {B.mine(layout, p) == False{} : Bool}
744 {L.is_lost(G.status(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p))) == False{} : Bool}
745
746def open_safe_c(w, h, layout, s, f, p, bm):
747 open_safe_c.go(w, h, layout, s, f, p, bm, G.unrevealed(w, h, s, p))
748
749
750
751
752def flood_complete_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
753 +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}, +cl: {PI.closed(w, h, layout, s) == True{} : Bool},
754 +p: T.Pos, +on: {B.on_board(w, h, p) == True{} : Bool}, +q: T.Pos, +onq: {B.on_board(w, h, q) == True{} : Bool},
755 +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
756 +c: Bool, ce: {G.unrevealed(w, h, s, p) == c : Bool}, +m: Bool, me: {B.mine(layout, p) == m : Bool}) ->
757 {L.revealed(G.knowledge(G.open.go(c, m, G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}:
758 match c m:
759 case False{} _:
760 %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q), B.at(Bool, False{}, s, q),
761 know_revealed(w, h, layout, s, f, T.Playing{}, q, onq)) : {_ == True{} : Bool}
762 path_closed(path, w, h, layout, s, cl, p, q, PF.unrev_shown(w, h, s, p, ce, on), wk)
763 case True{} True{}:
764 +s2 = B.set_at(Bool, s, p, True{})
765 %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s2, f, T.Lost{T.Exploded{p}}}), q), B.at(Bool, False{}, s2, q),
766 know_revealed(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, q, onq)) : {_ == True{} : Bool}
767 path_closed(path, w, h, layout, s2, PI.closed_explode(w, h, layout, s, p, me, cl), p, q,
768 PF.at_set_on(w, h, s, p, shS, on), wk)
769 case True{} False{}:
770 +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
771 +cf = B.count_false(s)
772 +hh = G.head_hidden(w, h, s, start)
773 +fl = G.flood(cf, start, hh, w, h, layout, s)
774 +st = G.won_or_playing(G.all_safe(w, h, layout, fl))
775 %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, fl, f, st}), q), B.at(Bool, False{}, fl, q),
776 know_revealed(w, h, layout, fl, f, st, q, onq)) : {_ == True{} : Bool}
777 path_closed(path, w, h, layout, fl, PI.closed_flood(cf, start, hh, w, h, layout, s, shS, cl, {==}, {==}), p, q,
778 PF.flood_work(cf, start, hh, w, h, layout, s, shS, {==}, {==}, p, on, start_has(p)), wk)
779
780law flood_complete_c:
781 for +w: Nat
782 for +h: Nat
783 for +layout: T.Grid(Bool)
784 for +s: T.Grid(Bool)
785 for +f: List<&2, T.Pos>
786 for +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}
787 for +cl: {PI.closed(w, h, layout, s) == True{} : Bool}
788 for +p: T.Pos
789 for +on: {L.on_board(w, h, p) == True{} : Bool}
790 for +q: T.Pos
791 for +path: List<&2, T.Pos>
792 for +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool}
793 {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}
794
795def flood_complete_c(w, h, layout, s, f, shS, cl, p, on, q, path, wk):
796 +onB = {%Equal.sym(Bool, B.on_board(w, h, p), L.on_board(w, h, p), PC.on_board_eq(w, h, p)) : {_ == True{} : Bool};
797 on : {B.on_board(w, h, p) == True{} : Bool}}
798 +onq = {%Equal.sym(Bool, B.on_board(w, h, q), L.on_board(w, h, q), PC.on_board_eq(w, h, q)) : {_ == True{} : Bool};
799 PW.walk_on(path, w, h, layout, p, q, wk, on) : {B.on_board(w, h, q) == True{} : Bool}}
800 flood_complete_c.go(w, h, layout, s, f, shS, cl, p, onB, q, onq, path, wk,
801 G.unrevealed(w, h, s, p), {==}, B.mine(layout, p), {==})
802
803def exact_explode(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +p: T.Pos, +q: T.Pos,
804 hidq: {B.at(Bool, False{}, s, q) == False{} : Bool},
805 after: {B.at(Bool, False{}, B.set_at(Bool, s, p, True{}), q) == True{} : Bool},
806 +b: Bool, be: {B.same(p, q) == b : Bool}) -> PF.Walk(w, h, layout, p, q):
807 match b:
808 case True{}:
809 (Nil{}, %PC.same_eq(p, q) : {_ == True{} : Bool}; be)
810 case False{}:
811 PF.both_absurd(PF.Walk(w, h, layout, p, q), B.at(Bool, False{}, s, q), hidq,
812 %PL.at_set_ne(Bool, s, p, q, True{}, False{}, be) : {_ == True{} : Bool}; after)
813
814def flood_exact_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
815 +p: T.Pos, +q: T.Pos, +onq: {B.on_board(w, h, q) == True{} : Bool},
816 +hidq: {B.at(Bool, False{}, s, q) == False{} : Bool},
817 +c: Bool, +m: Bool,
818 after: {L.revealed(G.knowledge(G.open.go(c, m, G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}) ->
819 PF.Walk(w, h, layout, p, q):
820 match c m:
821 case False{} _:
822 PF.both_absurd(PF.Walk(w, h, layout, p, q), B.at(Bool, False{}, s, q), hidq,
823 %know_revealed(w, h, layout, s, f, T.Playing{}, q, onq) : {_ == True{} : Bool}; after)
824 case True{} True{}:
825 +s2 = B.set_at(Bool, s, p, True{})
826 exact_explode(w, h, layout, s, p, q, hidq,
827 %know_revealed(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, q, onq) : {_ == True{} : Bool}; after,
828 B.same(p, q), {==})
829 case True{} False{}:
830 +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
831 +cf = B.count_false(s)
832 +hh = G.head_hidden(w, h, s, start)
833 +fl = G.flood(cf, start, hh, w, h, layout, s)
834 +st = G.won_or_playing(G.all_safe(w, h, layout, fl))
835 PF.flood_path(cf, start, hh, w, h, layout, s, p, start_ok(w, h, layout, p), q, hidq,
836 %know_revealed(w, h, layout, fl, f, st, q, onq) : {_ == True{} : Bool}; after)
837
838law flood_exact_c:
839 for +w: Nat
840 for +h: Nat
841 for +layout: T.Grid(Bool)
842 for +s: T.Grid(Bool)
843 for +f: List<&2, T.Pos>
844 for +p: T.Pos
845 for +q: T.Pos
846 for before: {L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q) == True{} : Bool}
847 for after: {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}
848 PF.Walk(w, h, layout, p, q)
849
850def flood_exact_c(w, h, layout, s, f, p, q, before, after):
851 +u = {%PG.know_hidden(w, h, layout, s, f, T.Playing{}, q) : {_ == True{} : Bool};
852 before : {G.unrevealed(w, h, s, q) == True{} : Bool}}
853 flood_exact_c.go(w, h, layout, s, f, p, q, PF.unrev_on(w, h, s, q, u), PF.unrev_hidden(w, h, s, q, u),
854 G.unrevealed(w, h, s, p), B.mine(layout, p), after)
855
856
857
858
859def open_mine.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
860 shape: {L.shaped(Bool, w, h, layout) == True{} : Bool},
861 +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, boom: {L.mine(layout, p) == True{} : Bool},
862 c: Canon(w, h, layout, g)) ->
863 {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
864 {L.seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}:
865 match c:
866 case (eg, facts):
867 match facts:
868 case (sh, f2):
869 match f2:
870 case (won, f3):
871 match f3:
872 case (cm, cl):
873 +s = shown_of(g)
874 +f = flags_of(g)
875 %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
876 {G.status(G.open(_, p)) == T.Lost{T.Exploded{p}} : T.Status} &
877 {L.seen(G.knowledge(G.open(_, p)), p) == T.Boom{} : T.Seen}
878 %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
879 {G.status(G.open(G.Game{w, h, layout, s, f, _}, p)) == T.Lost{T.Exploded{p}} : T.Status} &
880 {L.seen(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), p) == T.Boom{} : T.Seen}
881 open_mine_c(w, h, layout, s, f,
882 %Equal.sym(Bool, B.shaped(Bool, w, h, layout), L.shaped(Bool, w, h, layout), PC.shaped_eq(Bool, w, h, layout)) :
883 {_ == True{} : Bool}; shape,
884 sh,
885 %playing : {PI.calm(_, w, h, layout, s) == True{} : Bool}; cm,
886 p,
887 %Equal.sym(Bool, B.mine(layout, p), L.mine(layout, p), PC.mine_eq(layout, p)) :
888 {_ == True{} : Bool}; boom)
889
890law open_mine_:
891 for +w: Nat
892 for +h: Nat
893 for +layout: T.Grid(Bool)
894 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
895 for +g: G.Game
896 for r: L.Reachable(w, h, layout, g)
897 for +playing: {G.status(g) == T.Playing{} : T.Status}
898 for +p: T.Pos
899 for boom: {L.mine(layout, p) == True{} : Bool}
900 {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
901 {L.seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}
902
903def open_mine_(w, h, layout, shape, g, r, playing, p, boom):
904 open_mine.k(w, h, layout, g, shape, playing, p, boom, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
905
906def open_safe.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
907 +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, safe: {L.mine(layout, p) == False{} : Bool},
908 c: Canon(w, h, layout, g)) ->
909 {L.is_lost(G.status(G.open(g, p))) == False{} : Bool}:
910 match c:
911 case (eg, facts):
912 +s = shown_of(g)
913 +f = flags_of(g)
914 %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
915 {L.is_lost(G.status(G.open(_, p))) == False{} : Bool}
916 %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
917 {L.is_lost(G.status(G.open(G.Game{w, h, layout, s, f, _}, p))) == False{} : Bool}
918 open_safe_c(w, h, layout, s, f, p,
919 %Equal.sym(Bool, B.mine(layout, p), L.mine(layout, p), PC.mine_eq(layout, p)) :
920 {_ == False{} : Bool}; safe)
921
922law open_safe_:
923 for +w: Nat
924 for +h: Nat
925 for +layout: T.Grid(Bool)
926 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
927 for +g: G.Game
928 for r: L.Reachable(w, h, layout, g)
929 for +playing: {G.status(g) == T.Playing{} : T.Status}
930 for +p: T.Pos
931 for safe: {L.mine(layout, p) == False{} : Bool}
932 {L.is_lost(G.status(G.open(g, p))) == False{} : Bool}
933
934def open_safe_(w, h, layout, shape, g, r, playing, p, safe):
935 open_safe.k(w, h, layout, g, playing, p, safe, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
936
937def flood_complete.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
938 +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, +on: {L.on_board(w, h, p) == True{} : Bool},
939 +q: T.Pos, +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
940 c: Canon(w, h, layout, g)) ->
941 {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}:
942 match c:
943 case (eg, facts):
944 match facts:
945 case (sh, f2):
946 match f2:
947 case (won, f3):
948 match f3:
949 case (cm, cl):
950 +s = shown_of(g)
951 +f = flags_of(g)
952 %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
953 {L.revealed(G.knowledge(G.open(_, p)), q) == True{} : Bool}
954 %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
955 {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), q) == True{} : Bool}
956 flood_complete_c(w, h, layout, s, f, sh, cl, p, on, q, path, wk)
957
958law flood_complete_:
959 for +w: Nat
960 for +h: Nat
961 for +layout: T.Grid(Bool)
962 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
963 for +g: G.Game
964 for r: L.Reachable(w, h, layout, g)
965 for +playing: {G.status(g) == T.Playing{} : T.Status}
966 for +p: T.Pos
967 for +on: {L.on_board(w, h, p) == True{} : Bool}
968 for +q: T.Pos
969 for +path: List<&2, T.Pos>
970 for +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool}
971 {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
972
973def flood_complete_(w, h, layout, shape, g, r, playing, p, on, q, path, wk):
974 flood_complete.k(w, h, layout, g, playing, p, on, q, path, wk, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
975
976def flood_exact.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
977 +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, +q: T.Pos,
978 before: {L.hidden(G.knowledge(g), q) == True{} : Bool},
979 after: {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool},
980 c: Canon(w, h, layout, g)) -> PF.Walk(w, h, layout, p, q):
981 match c:
982 case (+eg, facts):
983 +s = shown_of(g)
984 +f = flags_of(g)
985 +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
986 flood_exact_c(w, h, layout, s, f, p, q,
987 {%playing : {L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), q) == True{} : Bool};
988 %eg : {L.hidden(G.knowledge(_), q) == True{} : Bool};
989 before : {L.hidden(G.knowledge(gp), q) == True{} : Bool}},
990 {%playing : {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), q) == True{} : Bool};
991 %eg : {L.revealed(G.knowledge(G.open(_, p)), q) == True{} : Bool};
992 after : {L.revealed(G.knowledge(G.open(gp, p)), q) == True{} : Bool}})
993
994law flood_exact_:
995 for +w: Nat
996 for +h: Nat
997 for +layout: T.Grid(Bool)
998 for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
999 for +g: G.Game
1000 for r: L.Reachable(w, h, layout, g)
1001 for +playing: {G.status(g) == T.Playing{} : T.Status}
1002 for +p: T.Pos
1003 for +q: T.Pos
1004 for before: {L.hidden(G.knowledge(g), q) == True{} : Bool}
1005 for after: {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
1006 PF.Walk(w, h, layout, p, q)
1007
1008def flood_exact_(w, h, layout, shape, g, r, playing, p, q, before, after):
1009 flood_exact.k(w, h, layout, g, playing, p, q, before, after, canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))