proof_display.bend

minebender-game@1.0.0.0 · 414 lines · 22 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_inv.bend as PI
10import minebender-game@1.0.0.0/proof_laws.bend as PW
11
12# Proofs of the display laws.
13
14law disp_row_get:
15  for +w: Nat
16  for +h: Nat
17  for +layout: T.Grid(Bool)
18  for +shown: T.Grid(Bool)
19  for +flags: List<&2, T.Pos>
20  for +st: T.Status
21  for +y: Nat
22  for +xs: List<&2, Nat>
23  for +j: Nat
24  for +x: Nat
25  for e: {List.get(&2, Nat, xs, j) == Some{x} : Maybe<&2, Nat>}
26  {List.get(&2, T.Tile, G.disp_row(w, h, layout, shown, flags, st, y, xs), j)
27    == Some{G.tile_at(w, h, layout, shown, flags, st, T.Pos{x, y})} : Maybe<&2, T.Tile>}
28
29def disp_row_get(w, h, layout, shown, flags, st, y, xs, j, x, e):
30  match xs j:
31    case Nil{} _:
32      Empty.absurd({List.get(&2, T.Tile, G.disp_row(w, h, layout, shown, flags, st, y, Nil{}), j)
33        == Some{G.tile_at(w, h, layout, shown, flags, st, T.Pos{x, y})} : Maybe<&2, T.Tile>},
34        PG.know_row_get.none(Nat, x, e))
35    case a <> t 0n:
36      %PG.know_row_get.some(Nat, a, x, e) :
37        {Some{G.tile_at(w, h, layout, shown, flags, st, T.Pos{a, y})}
38          == Some{G.tile_at(w, h, layout, shown, flags, st, T.Pos{_, y})} : Maybe<&2, T.Tile>}
39      {==}
40    case a <> t 1n+k:
41      disp_row_get(w, h, layout, shown, flags, st, y, t, k, x, e)
42
43law disp_rows_get:
44  for +w: Nat
45  for +h: Nat
46  for +layout: T.Grid(Bool)
47  for +shown: T.Grid(Bool)
48  for +flags: List<&2, T.Pos>
49  for +st: T.Status
50  for +ys: List<&2, Nat>
51  for +i: Nat
52  for +y: Nat
53  for e: {List.get(&2, Nat, ys, i) == Some{y} : Maybe<&2, Nat>}
54  {List.get(&2, List<&2, T.Tile>, G.disp_rows(w, h, layout, shown, flags, st, ys), i)
55    == Some{G.disp_row(w, h, layout, shown, flags, st, y, List.range(w))} : Maybe<&2, List<&2, T.Tile>>}
56
57def disp_rows_get(w, h, layout, shown, flags, st, ys, i, y, e):
58  match ys i:
59    case Nil{} _:
60      Empty.absurd({List.get(&2, List<&2, T.Tile>, G.disp_rows(w, h, layout, shown, flags, st, Nil{}), i)
61        == Some{G.disp_row(w, h, layout, shown, flags, st, y, List.range(w))} : Maybe<&2, List<&2, T.Tile>>},
62        PG.know_row_get.none(Nat, y, e))
63    case a <> t 0n:
64      %PG.know_row_get.some(Nat, a, y, e) :
65        {Some{G.disp_row(w, h, layout, shown, flags, st, a, List.range(w))}
66          == Some{G.disp_row(w, h, layout, shown, flags, st, _, List.range(w))} : Maybe<&2, List<&2, T.Tile>>}
67      {==}
68    case a <> t 1n+k:
69      disp_rows_get(w, h, layout, shown, flags, st, t, k, y, e)
70
71# On the board, the screen shows what tile_at says.
72law disp_at:
73  for +w: Nat
74  for +h: Nat
75  for +layout: T.Grid(Bool)
76  for +shown: T.Grid(Bool)
77  for +flags: List<&2, T.Pos>
78  for +st: T.Status
79  for +x: Nat
80  for +y: Nat
81  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
82  {L.tile(G.Game{w, h, layout, shown, flags, st}, T.Pos{x, y}) == G.tile_at(w, h, layout, shown, flags, st, T.Pos{x, y}) : T.Tile}
83
84def disp_at(w, h, layout, shown, flags, st, x, y, on):
85  +xw = P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
86  +yh = P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
87  +rows = G.disp_rows(w, h, layout, shown, flags, st, List.range(h))
88  +row = G.disp_row(w, h, layout, shown, flags, st, y, List.range(w))
89  %Equal.sym(Maybe<&2, List<&2, T.Tile>>, List.get(&2, List<&2, T.Tile>, rows, y), Some{row},
90    disp_rows_get(w, h, layout, shown, flags, st, List.range(h), y, y, P.range_get(h, y, yh))) :
91    {Maybe.default(&2, T.Tile, List.get(&2, T.Tile, Maybe.default(&2, List<&2, T.Tile>, _, Nil{}), x), T.Covered{})
92      == G.tile_at(w, h, layout, shown, flags, st, T.Pos{x, y}) : T.Tile}
93  %Equal.sym(Maybe<&2, T.Tile>, List.get(&2, T.Tile, row, x), Some{G.tile_at(w, h, layout, shown, flags, st, T.Pos{x, y})},
94    disp_row_get(w, h, layout, shown, flags, st, y, List.range(w), x, x, P.range_get(w, x, xw))) :
95    {Maybe.default(&2, T.Tile, _, T.Covered{}) == G.tile_at(w, h, layout, shown, flags, st, T.Pos{x, y}) : T.Tile}
96  {==}
97
98# During play
99# ===========
100
101law play_cell:
102  for +c: Bool
103  for +m: Bool
104  for +fl: Bool
105  for +w: Nat
106  for +h: Nat
107  for +layout: T.Grid(Bool)
108  for +p: T.Pos
109  {G.tile.go(None{}, c, m, fl, T.Playing{}, w, h, layout, p)
110    == L.tile_of(G.seen_pick(c, m, w, h, layout, p), Bool.and(Bool.and(True{}, Bool.not(c)), fl)) : T.Tile}
111
112def play_cell(c, m, fl, w, h, layout, p):
113  match c m:
114    case True{} True{}:
115      {==}
116    case True{} False{}:
117      {==}
118    case False{} _:
119      {==}
120
121law display_play_c:
122  for +w: Nat
123  for +h: Nat
124  for +layout: T.Grid(Bool)
125  for +s: T.Grid(Bool)
126  for +f: List<&2, T.Pos>
127  for +p: T.Pos
128  for +on: {B.on_board(w, h, p) == True{} : Bool}
129  {L.tile(G.Game{w, h, layout, s, f, T.Playing{}}, p)
130    == L.tile_of(L.seen(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p), G.flagged(G.Game{w, h, layout, s, f, T.Playing{}}, p)) : T.Tile}
131
132def display_play_c(w, h, layout, s, f, p, on):
133  match p:
134    case T.Pos{x, y}:
135      +q = {T.Pos{x, y} : T.Pos}
136      +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
137      %Equal.sym(T.Tile, L.tile(g0, q), G.tile_at(w, h, layout, s, f, T.Playing{}, q),
138        disp_at(w, h, layout, s, f, T.Playing{}, x, y, on)) :
139        {_ == L.tile_of(L.seen(G.knowledge(g0), q), G.flagged(g0, q)) : T.Tile}
140      %Equal.sym(T.Seen, L.seen(G.knowledge(g0), q), G.seen_at(w, h, layout, s, q),
141        PW.know_seen(w, h, layout, s, f, T.Playing{}, q, on)) :
142        {G.tile_at(w, h, layout, s, f, T.Playing{}, q) == L.tile_of(_, G.flagged(g0, q)) : T.Tile}
143      %Equal.sym(Bool, B.on_board(w, h, q), True{}, on) :
144        {G.tile_at(w, h, layout, s, f, T.Playing{}, q)
145          == L.tile_of(G.seen_at(w, h, layout, s, q), Bool.and(Bool.and(_, Bool.not(B.at(Bool, False{}, s, q))), B.contains(f, q))) : T.Tile}
146      play_cell(B.at(Bool, False{}, s, q), B.mine(layout, q), B.contains(f, q), w, h, layout, q)
147
148# After the game
149# ==============
150
151law display_blast_c:
152  for +w: Nat
153  for +h: Nat
154  for +layout: T.Grid(Bool)
155  for +s: T.Grid(Bool)
156  for +f: List<&2, T.Pos>
157  for +p: T.Pos
158  for +on: {B.on_board(w, h, p) == True{} : Bool}
159  {L.tile(G.Game{w, h, layout, s, f, T.Lost{T.Exploded{p}}}, p) == T.Blast{} : T.Tile}
160
161def display_blast_c(w, h, layout, s, f, p, on):
162  match p:
163    case T.Pos{x, y}:
164      +q = {T.Pos{x, y} : T.Pos}
165      %Equal.sym(T.Tile, L.tile(G.Game{w, h, layout, s, f, T.Lost{T.Exploded{q}}}, q),
166        G.tile_at(w, h, layout, s, f, T.Lost{T.Exploded{q}}, q), disp_at(w, h, layout, s, f, T.Lost{T.Exploded{q}}, x, y, on)) :
167        {_ == T.Blast{} : T.Tile}
168      %Equal.sym(Bool, B.same(q, q), True{}, PG.same_refl(q)) :
169        {G.tile.go(Bool.pick(Maybe<&2, T.Tile>, _, Some{T.Blast{}}, None{}), B.at(Bool, False{}, s, q), B.mine(layout, q),
170          B.contains(f, q), T.Lost{T.Exploded{q}}, w, h, layout, q) == T.Blast{} : T.Tile}
171      {==}
172
173law display_hint_c:
174  for +w: Nat
175  for +h: Nat
176  for +layout: T.Grid(Bool)
177  for +s: T.Grid(Bool)
178  for +f: List<&2, T.Pos>
179  for +p: T.Pos
180  for +on: {B.on_board(w, h, p) == True{} : Bool}
181  {L.tile(G.Game{w, h, layout, s, f, T.Lost{T.AssistTooEarly{p}}}, p) == T.Hint{} : T.Tile}
182
183def display_hint_c(w, h, layout, s, f, p, on):
184  match p:
185    case T.Pos{x, y}:
186      +q = {T.Pos{x, y} : T.Pos}
187      %Equal.sym(T.Tile, L.tile(G.Game{w, h, layout, s, f, T.Lost{T.AssistTooEarly{q}}}, q),
188        G.tile_at(w, h, layout, s, f, T.Lost{T.AssistTooEarly{q}}, q), disp_at(w, h, layout, s, f, T.Lost{T.AssistTooEarly{q}}, x, y, on)) :
189        {_ == T.Hint{} : T.Tile}
190      %Equal.sym(Bool, B.same(q, q), True{}, PG.same_refl(q)) :
191        {G.tile.go(Bool.pick(Maybe<&2, T.Tile>, _, Some{T.Hint{}}, None{}), B.at(Bool, False{}, s, q), B.mine(layout, q),
192          B.contains(f, q), T.Lost{T.AssistTooEarly{q}}, w, h, layout, q) == T.Hint{} : T.Tile}
193      {==}
194
195# A mine, once the game is over, under each way the cell might be marked.
196law over_cell:
197  for +c: Bool
198  for +st: T.Status
199  for over: {st != T.Playing{} : T.Status}
200  for +fl: Bool
201  for +w: Nat
202  for +h: Nat
203  for +layout: T.Grid(Bool)
204  for +p: T.Pos
205  {L.is_covered(G.tile.go(None{}, c, True{}, fl, st, w, h, layout, p)) == False{} : Bool}
206
207def over_cell(c, st, over, fl, w, h, layout, p):
208  match c:
209    case True{}:
210      {==}
211    case False{}:
212      match st:
213        case T.Playing{}:
214          Empty.absurd({L.is_covered(G.tile_hidden(T.Playing{}, True{}, fl)) == False{} : Bool}, over({==}))
215        case T.Won{}:
216          {==}
217        case T.Lost{why}:
218          match fl:
219            case True{}:
220              {==}
221            case False{}:
222              {==}
223
224def mark_cell(+mk: Maybe<&2, T.Tile>, +c: Bool, +fl: Bool, +st: T.Status, over: {st != T.Playing{} : T.Status},
225  +w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos,
226  ok: {Maybe.default(&2, Bool, Maybe.map(&2, T.Tile, Bool, t => L.is_covered(t), mk), False{}) == False{} : Bool}) ->
227  {L.is_covered(G.tile.go(mk, c, True{}, fl, st, w, h, layout, p)) == False{} : Bool}:
228  match mk:
229    case Some{t}:
230      ok
231    case None{}:
232      over_cell(c, st, over, fl, w, h, layout, p)
233
234def mark_ok.pick(+b: Bool, +t: T.Tile, ct: {L.is_covered(t) == False{} : Bool}) ->
235  {Maybe.default(&2, Bool, Maybe.map(&2, T.Tile, Bool, x => L.is_covered(x), Bool.pick(Maybe<&2, T.Tile>, b, Some{t}, None{})), False{})
236    == False{} : Bool}:
237  match b:
238    case True{}:
239      ct
240    case False{}:
241      {==}
242
243def mark_ok.why(+why: T.Loss, +p: T.Pos) ->
244  {Maybe.default(&2, Bool, Maybe.map(&2, T.Tile, Bool, t => L.is_covered(t), G.mark.why(why, p)), False{}) == False{} : Bool}:
245  match why:
246    case T.Exploded{e}:
247      mark_ok.pick(B.same(e, p), T.Blast{}, {==})
248    case T.AssistTooEarly{s}:
249      mark_ok.pick(B.same(s, p), T.Hint{}, {==})
250
251# What the end of the game singles out is never covered.
252law mark_ok:
253  for +st: T.Status
254  for +p: T.Pos
255  {Maybe.default(&2, Bool, Maybe.map(&2, T.Tile, Bool, t => L.is_covered(t), G.mark(st, p)), False{}) == False{} : Bool}
256
257def mark_ok(st, p):
258  match st:
259    case T.Playing{}:
260      {==}
261    case T.Won{}:
262      {==}
263    case T.Lost{why}:
264      mark_ok.why(why, p)
265
266law display_mines_c:
267  for +w: Nat
268  for +h: Nat
269  for +layout: T.Grid(Bool)
270  for +s: T.Grid(Bool)
271  for +f: List<&2, T.Pos>
272  for +st: T.Status
273  for over: {st != T.Playing{} : T.Status}
274  for +q: T.Pos
275  for +on: {B.on_board(w, h, q) == True{} : Bool}
276  for +m: {B.mine(layout, q) == True{} : Bool}
277  {L.is_covered(L.tile(G.Game{w, h, layout, s, f, st}, q)) == False{} : Bool}
278
279def display_mines_c(w, h, layout, s, f, st, over, q, on, m):
280  match q:
281    case T.Pos{x, y}:
282      +p = {T.Pos{x, y} : T.Pos}
283      %Equal.sym(T.Tile, L.tile(G.Game{w, h, layout, s, f, st}, p), G.tile_at(w, h, layout, s, f, st, p),
284        disp_at(w, h, layout, s, f, st, x, y, on)) :
285        {L.is_covered(_) == False{} : Bool}
286      %Equal.sym(Bool, B.mine(layout, p), True{}, m) :
287        {L.is_covered(G.tile.go(G.mark(st, p), B.at(Bool, False{}, s, p), _, B.contains(f, p), st, w, h, layout, p)) == False{} : Bool}
288      mark_cell(G.mark(st, p), B.at(Bool, False{}, s, p), B.contains(f, p), st, over, w, h, layout, p, mark_ok(st, p))
289
290# On real games
291# =============
292
293def on_conv(+w: Nat, +h: Nat, +p: T.Pos, on: {L.on_board(w, h, p) == True{} : Bool}) ->
294  {B.on_board(w, h, p) == True{} : Bool}:
295  %Equal.sym(Bool, B.on_board(w, h, p), L.on_board(w, h, p), PC.on_board_eq(w, h, p)) :
296    {_ == True{} : Bool}; on
297
298def display_play.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
299  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, on: {L.on_board(w, h, p) == True{} : Bool},
300  c: PW.Canon(w, h, layout, g)) ->
301  {L.tile(g, p) == L.tile_of(L.seen(G.knowledge(g), p), G.flagged(g, p)) : T.Tile}:
302  match c:
303    case (eg, facts):
304      +s = PW.shown_of(g)
305      +f = PW.flags_of(g)
306      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
307        {L.tile(_, p) == L.tile_of(L.seen(G.knowledge(_), p), G.flagged(_, p)) : T.Tile}
308      %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
309        {L.tile(G.Game{w, h, layout, s, f, _}, p)
310          == L.tile_of(L.seen(G.knowledge(G.Game{w, h, layout, s, f, _}), p), G.flagged(G.Game{w, h, layout, s, f, _}, p)) : T.Tile}
311      display_play_c(w, h, layout, s, f, p, on_conv(w, h, p, on))
312
313law display_play_:
314  for +w: Nat
315  for +h: Nat
316  for +layout: T.Grid(Bool)
317  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
318  for +g: G.Game
319  for r: L.Reachable(w, h, layout, g)
320  for +playing: {G.status(g) == T.Playing{} : T.Status}
321  for +p: T.Pos
322  for on: {L.on_board(w, h, p) == True{} : Bool}
323  {L.tile(g, p) == L.tile_of(L.seen(G.knowledge(g), p), G.flagged(g, p)) : T.Tile}
324
325def display_play_(w, h, layout, shape, g, r, playing, p, on):
326  display_play.k(w, h, layout, g, playing, p, on, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
327
328def display_blast.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +p: T.Pos,
329  +lost: {G.status(g) == T.Lost{T.Exploded{p}} : T.Status}, on: {L.on_board(w, h, p) == True{} : Bool},
330  c: PW.Canon(w, h, layout, g)) ->
331  {L.tile(g, p) == T.Blast{} : T.Tile}:
332  match c:
333    case (eg, facts):
334      +s = PW.shown_of(g)
335      +f = PW.flags_of(g)
336      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
337        {L.tile(_, p) == T.Blast{} : T.Tile}
338      %Equal.sym(T.Status, G.status(g), T.Lost{T.Exploded{p}}, lost) :
339        {L.tile(G.Game{w, h, layout, s, f, _}, p) == T.Blast{} : T.Tile}
340      display_blast_c(w, h, layout, s, f, p, on_conv(w, h, p, on))
341
342law display_blast_:
343  for +w: Nat
344  for +h: Nat
345  for +layout: T.Grid(Bool)
346  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
347  for +g: G.Game
348  for r: L.Reachable(w, h, layout, g)
349  for +p: T.Pos
350  for +lost: {G.status(g) == T.Lost{T.Exploded{p}} : T.Status}
351  for on: {L.on_board(w, h, p) == True{} : Bool}
352  {L.tile(g, p) == T.Blast{} : T.Tile}
353
354def display_blast_(w, h, layout, shape, g, r, p, lost, on):
355  display_blast.k(w, h, layout, g, p, lost, on, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
356
357def display_hint.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +p: T.Pos,
358  +lost: {G.status(g) == T.Lost{T.AssistTooEarly{p}} : T.Status}, on: {L.on_board(w, h, p) == True{} : Bool},
359  c: PW.Canon(w, h, layout, g)) ->
360  {L.tile(g, p) == T.Hint{} : T.Tile}:
361  match c:
362    case (eg, facts):
363      +s = PW.shown_of(g)
364      +f = PW.flags_of(g)
365      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
366        {L.tile(_, p) == T.Hint{} : T.Tile}
367      %Equal.sym(T.Status, G.status(g), T.Lost{T.AssistTooEarly{p}}, lost) :
368        {L.tile(G.Game{w, h, layout, s, f, _}, p) == T.Hint{} : T.Tile}
369      display_hint_c(w, h, layout, s, f, p, on_conv(w, h, p, on))
370
371law display_hint_:
372  for +w: Nat
373  for +h: Nat
374  for +layout: T.Grid(Bool)
375  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
376  for +g: G.Game
377  for r: L.Reachable(w, h, layout, g)
378  for +s: T.Pos
379  for +lost: {G.status(g) == T.Lost{T.AssistTooEarly{s}} : T.Status}
380  for on: {L.on_board(w, h, s) == True{} : Bool}
381  {L.tile(g, s) == T.Hint{} : T.Tile}
382
383def display_hint_(w, h, layout, shape, g, r, s, lost, on):
384  display_hint.k(w, h, layout, g, s, lost, on, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
385
386def display_mines.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
387  over: {G.status(g) != T.Playing{} : T.Status}, +q: T.Pos, on: {L.on_board(w, h, q) == True{} : Bool},
388  m: {L.mine(layout, q) == True{} : Bool}, c: PW.Canon(w, h, layout, g)) ->
389  {L.is_covered(L.tile(g, q)) == False{} : Bool}:
390  match c:
391    case (eg, facts):
392      +s = PW.shown_of(g)
393      +f = PW.flags_of(g)
394      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
395        {L.is_covered(L.tile(_, q)) == False{} : Bool}
396      display_mines_c(w, h, layout, s, f, G.status(g), over, q, on_conv(w, h, q, on),
397        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) :
398          {_ == True{} : Bool}; m)
399
400law display_mines_:
401  for +w: Nat
402  for +h: Nat
403  for +layout: T.Grid(Bool)
404  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
405  for +g: G.Game
406  for r: L.Reachable(w, h, layout, g)
407  for over: {G.status(g) != T.Playing{} : T.Status}
408  for +q: T.Pos
409  for on: {L.on_board(w, h, q) == True{} : Bool}
410  for m: {L.mine(layout, q) == True{} : Bool}
411  {L.is_covered(L.tile(g, q)) == False{} : Bool}
412
413def display_mines_(w, h, layout, shape, g, r, over, q, on, m):
414  display_mines.k(w, h, layout, g, over, q, on, m, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))