proof_inv.bend

minebender-game@1.0.0.0 · 840 lines · 58 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/solver.bend as S
14
15# The invariant of real games, and that every action keeps it.
16
17# Closure: every revealed zero has its neighbours revealed
18# ========================================================
19
20def shown_in(g: T.Grid(Bool), q: T.Pos) -> Bool:
21  B.at(Bool, False{}, g, q)
22
23type CL is Data:
24  CL{w: Nat, h: Nat, layout: T.Grid(Bool), g: T.Grid(Bool)}
25
26def cl_f.go(e: CL, +q: T.Pos) -> Bool:
27  match e:
28    case CL{+w, +h, layout, +g}:
29      Bool.not(B.at(Bool, False{}, g, q) && B.zero(w, h, layout, q))
30        || PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))
31
32def cl_f(e: CL, q: T.Pos) -> Bool:
33  cl_f.go(e, q)
34
35def closed(+w: Nat, +h: Nat, layout: T.Grid(Bool), g: T.Grid(Bool)) -> Bool:
36  PS.allp(~CL, ~cl_f, CL{w, h, layout, g}, B.cells(w, h))
37
38def closed_use.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: T.Grid(Bool), +q: T.Pos, +r: T.Pos,
39  f: {Bool.or(Bool.not(Bool.and(True{}, True{})),
40    PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool},
41  rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}) ->
42  {B.at(Bool, False{}, g, r) == True{} : Bool}:
43  PS.allp_member(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q), r, f, rm)
44
45# In a closed grid, a revealed zero's neighbours are revealed.
46law closed_use:
47  for +w: Nat
48  for +h: Nat
49  for +layout: T.Grid(Bool)
50  for +g: T.Grid(Bool)
51  for c: {closed(w, h, layout, g) == True{} : Bool}
52  for +q: T.Pos
53  for on: {B.on_board(w, h, q) == True{} : Bool}
54  for gq: {B.at(Bool, False{}, g, q) == True{} : Bool}
55  for z: {B.zero(w, h, layout, q) == True{} : Bool}
56  for +r: T.Pos
57  for rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}
58  {B.at(Bool, False{}, g, r) == True{} : Bool}
59
60def closed_use(w, h, layout, g, c, q, on, gq, z, r, rm):
61  +f = PS.allp_member(~CL, ~cl_f, CL{w, h, layout, g}, B.cells(w, h), q, c, PS.cells_member(w, h, q, on))
62  closed_use.go(w, h, layout, g, q, r,
63    %gq : {Bool.or(Bool.not(Bool.and(_, True{})),
64        PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool};
65    %z : {Bool.or(Bool.not(Bool.and(B.at(Bool, False{}, g, q), _)),
66        PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool};
67    f, rm)
68
69# After a flood
70# =============
71
72# The flood's one-cell closure fact: a revealed zero's neighbour is revealed.
73def flood_fact.go(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
74  +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
75  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat},
76  +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
77  after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool},
78  +z: {B.zero(w, h, layout, q) == True{} : Bool}, +r: T.Pos,
79  +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool},
80  +s: Bool, se: {B.at(Bool, False{}, shown, q) == s : Bool}) ->
81  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), r) == True{} : Bool}:
82  match s:
83    case True{}:
84      PF.flood_mono(n, work, hd, w, h, layout, shown, r, closed_use(w, h, layout, shown, cl, q, on, se, z, r, rm))
85    case False{}:
86      PF.flood_zero(n, work, hd, w, h, layout, shown, sh, cnt, he, q, se, after, z, r, rm)
87
88def closed_flood.nbrs(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
89  +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
90  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat},
91  +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool},
92  +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool},
93  +z: {B.zero(w, h, layout, q) == True{} : Bool}, ns: List<&2, T.Pos>,
94  +adj: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, ns) == True{} : Bool}) ->
95  {PS.allp(~T.Grid(Bool), ~shown_in, G.flood(n, work, hd, w, h, layout, shown), ns) == True{} : Bool}:
96  match ns:
97    case Nil{}:
98      {==}
99    case +r <> +t:
100      +ar = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj)
101      +rm = PS.neighbours_member(w, h, q, r, P.and_true_r(B.adjacent(q, r), B.on_board(w, h, r), ar),
102        P.and_true_l(B.adjacent(q, r), B.on_board(w, h, r), ar))
103      +F = G.flood(n, work, hd, w, h, layout, shown)
104      %Equal.sym(Bool, B.at(Bool, False{}, F, r), True{},
105        flood_fact.go(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, on, after, z, r, rm,
106          B.at(Bool, False{}, shown, q), {==})) :
107        {Bool.and(_, PS.allp(~T.Grid(Bool), ~shown_in, F, t)) == True{} : Bool}
108      closed_flood.nbrs(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, on, after, z, t,
109        PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj))
110
111def closed_flood.cell(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
112  +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
113  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat},
114  +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool},
115  +b: Bool, +be: {Bool.and(B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q), B.zero(w, h, layout, q)) == b : Bool}) ->
116  {cl_f(CL{w, h, layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}:
117  match b:
118    case False{}:
119      +F = G.flood(n, work, hd, w, h, layout, shown)
120      %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q)), False{}, be) :
121        {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, F, B.neighbours(w, h, q))) == True{} : Bool}
122      {==}
123    case True{}:
124      +F = G.flood(n, work, hd, w, h, layout, shown)
125      +fq = P.and_true_l(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q), be)
126      +zq = P.and_true_r(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q), be)
127      %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q)), True{}, be) :
128        {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, F, B.neighbours(w, h, q))) == True{} : Bool}
129      closed_flood.nbrs(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, on, fq, zq,
130        B.neighbours(w, h, q), PS.neighbours_all(w, h, q))
131
132def closed_flood.cells(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
133  +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
134  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat},
135  +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, ps: List<&2, T.Pos>,
136  +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
137  {PS.allp(~CL, ~cl_f, CL{w, h, layout, G.flood(n, work, hd, w, h, layout, shown)}, ps) == True{} : Bool}:
138  match ps:
139    case Nil{}:
140      {==}
141    case +q <> +t:
142      +F = G.flood(n, work, hd, w, h, layout, shown)
143      %Equal.sym(Bool, cl_f(CL{w, h, layout, F}, q), True{},
144        closed_flood.cell(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q,
145          PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
146          Bool.and(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q)), {==})) :
147        {Bool.and(_, PS.allp(~CL, ~cl_f, CL{w, h, layout, F}, t)) == True{} : Bool}
148      closed_flood.cells(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, t,
149        PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))
150
151# A flood from a closed grid leaves a closed grid.
152law closed_flood:
153  for +n: Nat
154  for +work: List<&2, G.Work>
155  for +hd: Bool
156  for +w: Nat
157  for +h: Nat
158  for +layout: T.Grid(Bool)
159  for +shown: T.Grid(Bool)
160  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
161  for +cl: {closed(w, h, layout, shown) == True{} : Bool}
162  for +cnt: {n == B.count_false(shown) : Nat}
163  for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
164  {closed(w, h, layout, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool}
165
166def closed_flood(n, work, hd, w, h, layout, shown, sh, cl, cnt, he):
167  closed_flood.cells(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, B.cells(w, h), PS.cells_on(w, h))
168
169# After an explosion
170# ==================
171
172def zero_not_mine(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos,
173  z: {B.zero(w, h, layout, q) == True{} : Bool}) -> {B.mine(layout, q) == False{} : Bool}:
174  +a = Bool.and(B.on_board(w, h, q), Bool.not(B.mine(layout, q)))
175  P.not_true(B.mine(layout, q),
176    P.and_true_r(B.on_board(w, h, q), Bool.not(B.mine(layout, q)),
177      P.and_true_l(a, Nat.is_eq(B.adj_mines(w, h, layout, q), 0n), z)))
178
179def explode_fact.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
180  mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool},
181  +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
182  after: {B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q) == True{} : Bool},
183  +z: {B.zero(w, h, layout, q) == True{} : Bool}, +r: T.Pos,
184  +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool},
185  +b: Bool, be: {B.same(p, q) == b : Bool}) ->
186  {B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), r) == True{} : Bool}:
187  match b:
188    case True{}:
189      PF.both_absurd({B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), r) == True{} : Bool},
190        B.mine(layout, q), zero_not_mine(w, h, layout, q, z),
191        %PG.same_sound(p, q, be) : {B.mine(layout, _) == True{} : Bool}; mp)
192    case False{}:
193      PF.at_set_mono(shown, p, r,
194        closed_use(w, h, layout, shown, cl, q, on,
195          %PL.at_set_ne(Bool, shown, p, q, True{}, False{}, be) : {_ == True{} : Bool}; after, z, r, rm))
196
197def closed_explode.nbrs(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
198  +mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool},
199  +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool},
200  +after: {B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q) == True{} : Bool},
201  +z: {B.zero(w, h, layout, q) == True{} : Bool}, ns: List<&2, T.Pos>,
202  +adj: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, ns) == True{} : Bool}) ->
203  {PS.allp(~T.Grid(Bool), ~shown_in, B.set_at(Bool, shown, p, True{}), ns) == True{} : Bool}:
204  match ns:
205    case Nil{}:
206      {==}
207    case +r <> +t:
208      +ar = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj)
209      +rm = PS.neighbours_member(w, h, q, r, P.and_true_r(B.adjacent(q, r), B.on_board(w, h, r), ar),
210        P.and_true_l(B.adjacent(q, r), B.on_board(w, h, r), ar))
211      +s2 = B.set_at(Bool, shown, p, True{})
212      %Equal.sym(Bool, B.at(Bool, False{}, s2, r), True{},
213        explode_fact.go(w, h, layout, shown, p, mp, cl, q, on, after, z, r, rm, B.same(p, q), {==})) :
214        {Bool.and(_, PS.allp(~T.Grid(Bool), ~shown_in, s2, t)) == True{} : Bool}
215      closed_explode.nbrs(w, h, layout, shown, p, mp, cl, q, on, after, z, t,
216        PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj))
217
218def closed_explode.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
219  +mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool},
220  +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}, +b: Bool,
221  +be: {Bool.and(B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q), B.zero(w, h, layout, q)) == b : Bool}) ->
222  {cl_f(CL{w, h, layout, B.set_at(Bool, shown, p, True{})}, q) == True{} : Bool}:
223  match b:
224    case False{}:
225      +s2 = B.set_at(Bool, shown, p, True{})
226      %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q)), False{}, be) :
227        {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, s2, B.neighbours(w, h, q))) == True{} : Bool}
228      {==}
229    case True{}:
230      +s2 = B.set_at(Bool, shown, p, True{})
231      %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q)), True{}, be) :
232        {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, s2, B.neighbours(w, h, q))) == True{} : Bool}
233      closed_explode.nbrs(w, h, layout, shown, p, mp, cl, q, on,
234        P.and_true_l(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q), be),
235        P.and_true_r(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q), be),
236        B.neighbours(w, h, q), PS.neighbours_all(w, h, q))
237
238def closed_explode.cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
239  +mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool},
240  ps: List<&2, T.Pos>, +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
241  {PS.allp(~CL, ~cl_f, CL{w, h, layout, B.set_at(Bool, shown, p, True{})}, ps) == True{} : Bool}:
242  match ps:
243    case Nil{}:
244      {==}
245    case +q <> +t:
246      +s2 = B.set_at(Bool, shown, p, True{})
247      %Equal.sym(Bool, cl_f(CL{w, h, layout, s2}, q), True{},
248        closed_explode.cell(w, h, layout, shown, p, mp, cl, q,
249          PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
250          Bool.and(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q)), {==})) :
251        {Bool.and(_, PS.allp(~CL, ~cl_f, CL{w, h, layout, s2}, t)) == True{} : Bool}
252      closed_explode.cells(w, h, layout, shown, p, mp, cl, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))
253
254law closed_explode:
255  for +w: Nat
256  for +h: Nat
257  for +layout: T.Grid(Bool)
258  for +shown: T.Grid(Bool)
259  for +p: T.Pos
260  for +mp: {B.mine(layout, p) == True{} : Bool}
261  for +cl: {closed(w, h, layout, shown) == True{} : Bool}
262  {closed(w, h, layout, B.set_at(Bool, shown, p, True{})) == True{} : Bool}
263
264def closed_explode(w, h, layout, shown, p, mp, cl):
265  closed_explode.cells(w, h, layout, shown, p, mp, cl, B.cells(w, h), PS.cells_on(w, h))
266
267# The blank grid is closed
268# ========================
269
270def closed_blank.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos) ->
271  {cl_f(CL{w, h, layout, B.blank(Bool, w, h, False{})}, q) == True{} : Bool}:
272  match q:
273    case T.Pos{x, y}:
274      +bl = B.blank(Bool, w, h, False{})
275      %Equal.sym(Bool, B.at(Bool, False{}, bl, T.Pos{x, y}), False{}, PL.blank_at(w, h, x, y)) :
276        {Bool.or(Bool.not(Bool.and(_, B.zero(w, h, layout, T.Pos{x, y}))),
277          PS.allp(~T.Grid(Bool), ~shown_in, bl, B.neighbours(w, h, T.Pos{x, y}))) == True{} : Bool}
278      {==}
279
280def closed_blank.cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), ps: List<&2, T.Pos>) ->
281  {PS.allp(~CL, ~cl_f, CL{w, h, layout, B.blank(Bool, w, h, False{})}, ps) == True{} : Bool}:
282  match ps:
283    case Nil{}:
284      {==}
285    case q <> t:
286      %Equal.sym(Bool, cl_f(CL{w, h, layout, B.blank(Bool, w, h, False{})}, q), True{},
287        closed_blank.cell(w, h, layout, q)) :
288        {Bool.and(_, PS.allp(~CL, ~cl_f, CL{w, h, layout, B.blank(Bool, w, h, False{})}, t)) == True{} : Bool}
289      closed_blank.cells(w, h, layout, t)
290
291law closed_blank:
292  for +w: Nat
293  for +h: Nat
294  for +layout: T.Grid(Bool)
295  {closed(w, h, layout, B.blank(Bool, w, h, False{})) == True{} : Bool}
296
297def closed_blank(w, h, layout):
298  closed_blank.cells(w, h, layout, B.cells(w, h))
299
300# No revealed mine
301# ================
302
303type LS is Data:
304  LS{layout: T.Grid(Bool), g: T.Grid(Bool)}
305
306def nsm_f.go(e: LS, +q: T.Pos) -> Bool:
307  match e:
308    case LS{layout, g}:
309      Bool.not(B.at(Bool, False{}, g, q) && B.mine(layout, q))
310
311def nsm_f(e: LS, q: T.Pos) -> Bool:
312  nsm_f.go(e, q)
313
314def nsm(w: Nat, h: Nat, layout: T.Grid(Bool), g: T.Grid(Bool)) -> Bool:
315  PS.allp(~LS, ~nsm_f, LS{layout, g}, B.cells(w, h))
316
317def nsm_use.go(+layout: T.Grid(Bool), +g: T.Grid(Bool), +q: T.Pos,
318  f: {Bool.not(Bool.and(B.at(Bool, False{}, g, q), True{})) == True{} : Bool}) ->
319  {B.at(Bool, False{}, g, q) == False{} : Bool}:
320  P.not_true(B.at(Bool, False{}, g, q),
321    %P.and_true_r_id(B.at(Bool, False{}, g, q)) : {Bool.not(_) == True{} : Bool}; f)
322
323# Without a revealed mine, a mine of the board is not revealed.
324law nsm_use:
325  for +w: Nat
326  for +h: Nat
327  for +layout: T.Grid(Bool)
328  for +g: T.Grid(Bool)
329  for n: {nsm(w, h, layout, g) == True{} : Bool}
330  for +q: T.Pos
331  for on: {B.on_board(w, h, q) == True{} : Bool}
332  for m: {B.mine(layout, q) == True{} : Bool}
333  {B.at(Bool, False{}, g, q) == False{} : Bool}
334
335def nsm_use(w, h, layout, g, n, q, on, m):
336  nsm_use.go(layout, g, q,
337    %m : {Bool.not(Bool.and(B.at(Bool, False{}, g, q), _)) == True{} : Bool};
338    PS.allp_member(~LS, ~nsm_f, LS{layout, g}, B.cells(w, h), q, n, PS.cells_member(w, h, q, on)))
339
340def nsm_flood.walk(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p0: T.Pos, +q: T.Pos,
341  safe: {L.mine(layout, p0) == False{} : Bool}, mq: {B.mine(layout, q) == True{} : Bool},
342  wk: PF.Walk(w, h, layout, p0, q), -A: Type) -> A:
343  match wk:
344    case (path, pw):
345      PF.both_absurd(A, L.mine(layout, q), PW.walk_safe(path, w, h, layout, p0, q, pw, safe),
346        %PC.mine_eq(layout, q) : {_ == True{} : Bool}; mq)
347
348def nsm_flood.new(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
349  +shown: T.Grid(Bool), +p0: T.Pos, +safe: {L.mine(layout, p0) == False{} : Bool},
350  +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool}, +q: T.Pos,
351  fq: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool},
352  mq: {B.mine(layout, q) == True{} : Bool}, before: {B.at(Bool, False{}, shown, q) == False{} : Bool}) ->
353  {nsm_f(LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}:
354  nsm_flood.walk(w, h, layout, p0, q, safe, mq,
355    PF.flood_path(n, work, hd, w, h, layout, shown, p0, ok, q, before, fq),
356    {nsm_f(LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool})
357
358def nsm_flood.cell(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
359  +shown: T.Grid(Bool), +p0: T.Pos, +safe: {L.mine(layout, p0) == False{} : Bool},
360  +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool},
361  +ns: {nsm(w, h, layout, shown) == True{} : Bool}, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool},
362  +b: Bool, +be: {Bool.and(B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q), B.mine(layout, q)) == b : Bool}) ->
363  {nsm_f(LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}:
364  match b:
365    case False{}:
366      +F = G.flood(n, work, hd, w, h, layout, shown)
367      %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, F, q), B.mine(layout, q)), False{}, be) :
368        {Bool.not(_) == True{} : Bool}
369      {==}
370    case True{}:
371      +F = G.flood(n, work, hd, w, h, layout, shown)
372      +fq = P.and_true_l(B.at(Bool, False{}, F, q), B.mine(layout, q), be)
373      +mq = P.and_true_r(B.at(Bool, False{}, F, q), B.mine(layout, q), be)
374      nsm_flood.new(n, work, hd, w, h, layout, shown, p0, safe, ok, q, fq, mq,
375        nsm_use(w, h, layout, shown, ns, q, on, mq))
376
377def nsm_flood.cells(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
378  +shown: T.Grid(Bool), +p0: T.Pos, +safe: {L.mine(layout, p0) == False{} : Bool},
379  +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool},
380  +ns: {nsm(w, h, layout, shown) == True{} : Bool}, ps: List<&2, T.Pos>,
381  +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
382  {PS.allp(~LS, ~nsm_f, LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, ps) == True{} : Bool}:
383  match ps:
384    case Nil{}:
385      {==}
386    case +q <> +t:
387      +F = G.flood(n, work, hd, w, h, layout, shown)
388      %Equal.sym(Bool, nsm_f(LS{layout, F}, q), True{},
389        nsm_flood.cell(n, work, hd, w, h, layout, shown, p0, safe, ok, ns, q,
390          PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons),
391          Bool.and(B.at(Bool, False{}, F, q), B.mine(layout, q)), {==})) :
392        {Bool.and(_, PS.allp(~LS, ~nsm_f, LS{layout, F}, t)) == True{} : Bool}
393      nsm_flood.cells(n, work, hd, w, h, layout, shown, p0, safe, ok, ns, t,
394        PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))
395
396# A flood from a safe cell reveals no mine.
397law nsm_flood:
398  for +n: Nat
399  for +work: List<&2, G.Work>
400  for +hd: Bool
401  for +w: Nat
402  for +h: Nat
403  for +layout: T.Grid(Bool)
404  for +shown: T.Grid(Bool)
405  for +p0: T.Pos
406  for +safe: {L.mine(layout, p0) == False{} : Bool}
407  for +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool}
408  for +ns: {nsm(w, h, layout, shown) == True{} : Bool}
409  {nsm(w, h, layout, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool}
410
411def nsm_flood(n, work, hd, w, h, layout, shown, p0, safe, ok, ns):
412  nsm_flood.cells(n, work, hd, w, h, layout, shown, p0, safe, ok, ns, B.cells(w, h), PS.cells_on(w, h))
413
414def nsm_blank.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos) ->
415  {nsm_f(LS{layout, B.blank(Bool, w, h, False{})}, q) == True{} : Bool}:
416  match q:
417    case T.Pos{x, y}:
418      %Equal.sym(Bool, B.at(Bool, False{}, B.blank(Bool, w, h, False{}), T.Pos{x, y}), False{}, PL.blank_at(w, h, x, y)) :
419        {Bool.not(Bool.and(_, B.mine(layout, T.Pos{x, y}))) == True{} : Bool}
420      {==}
421
422def nsm_blank.cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), ps: List<&2, T.Pos>) ->
423  {PS.allp(~LS, ~nsm_f, LS{layout, B.blank(Bool, w, h, False{})}, ps) == True{} : Bool}:
424  match ps:
425    case Nil{}:
426      {==}
427    case q <> t:
428      %Equal.sym(Bool, nsm_f(LS{layout, B.blank(Bool, w, h, False{})}, q), True{}, nsm_blank.cell(w, h, layout, q)) :
429        {Bool.and(_, PS.allp(~LS, ~nsm_f, LS{layout, B.blank(Bool, w, h, False{})}, t)) == True{} : Bool}
430      nsm_blank.cells(w, h, layout, t)
431
432law nsm_blank:
433  for +w: Nat
434  for +h: Nat
435  for +layout: T.Grid(Bool)
436  {nsm(w, h, layout, B.blank(Bool, w, h, False{})) == True{} : Bool}
437
438def nsm_blank(w, h, layout):
439  nsm_blank.cells(w, h, layout, B.cells(w, h))
440
441# Status
442# ======
443
444law won_or_playing_won:
445  for +b: Bool
446  {L.is_won(G.won_or_playing(b)) == b : Bool}
447
448def won_or_playing_won(b):
449  match b:
450    case True{}:
451      {==}
452    case False{}:
453      {==}
454
455law playing_is:
456  for +s: T.Status
457  for e: {G.is_playing(s) == True{} : Bool}
458  {s == T.Playing{} : T.Status}
459
460def playing_is(s, e):
461  match s:
462    case T.Playing{}:
463      {==}
464    case T.Won{}:
465      Empty.absurd({T.Won{} == T.Playing{} : T.Status}, P.false_ne_true(e))
466    case T.Lost{why}:
467      Empty.absurd({T.Lost{why} == T.Playing{} : T.Status}, P.false_ne_true(e))
468
469# The invariant
470# =============
471
472def calm(+status: T.Status, +w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool)) -> Bool:
473  Bool.or(Bool.not(G.is_playing(status)), nsm(w, h, layout, shown))
474
475def Facts(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +status: T.Status) -> Type:
476  {B.shaped(Bool, w, h, shown) == True{} : Bool} &
477  ({L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool} &
478  ({calm(status, w, h, layout, shown) == True{} : Bool} &
479   {closed(w, h, layout, shown) == True{} : Bool}))
480
481# What every real game satisfies: the board it was started with, a grid of
482# revealed cells of the board's shape, Won exactly when every safe cell is
483# revealed, no revealed mine during play, and every revealed zero's
484# neighbours revealed.
485def Inv(+w: Nat, +h: Nat, +layout: T.Grid(Bool), g: G.Game) -> Type:
486  match g:
487    case G.Game{gw, gh, gl, shown, flags, status}:
488      {gw == w : Nat} & ({gh == h : Nat} & ({gl == layout : T.Grid(Bool)} & Facts(w, h, layout, shown, status)))
489
490def all_safe_cell(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, +q: T.Pos,
491  mp: {B.mine(layout, p) == True{} : Bool}, +b: Bool, be: {B.same(p, q) == b : Bool}) ->
492  {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q))
493    == Bool.or(B.mine(layout, q), B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}:
494  match b:
495    case True{}:
496      +mq = {%PG.same_sound(p, q, be) : {B.mine(layout, _) == True{} : Bool}; mp : {B.mine(layout, q) == True{} : Bool}}
497      %Equal.sym(Bool, B.mine(layout, q), True{}, mq) :
498        {Bool.or(_, B.at(Bool, False{}, shown, q))
499          == Bool.or(_, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}
500      {==}
501    case False{}:
502      %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q), B.at(Bool, False{}, shown, q),
503        PL.at_set_ne(Bool, shown, p, q, True{}, False{}, be)) :
504        {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) == Bool.or(B.mine(layout, q), _) : Bool}
505      {==}
506
507def all_safe_set_mine.go(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
508  +mp: {B.mine(layout, p) == True{} : Bool}, ps: List<&2, T.Pos>) ->
509  {G.all_safe.go(layout, B.set_at(Bool, shown, p, True{}), ps) == G.all_safe.go(layout, shown, ps) : Bool}:
510  match ps:
511    case Nil{}:
512      {==}
513    case +q <> t:
514      +s2 = B.set_at(Bool, shown, p, True{})
515      %Equal.sym(Bool, G.all_safe.go(layout, s2, t), G.all_safe.go(layout, shown, t),
516        all_safe_set_mine.go(layout, shown, p, mp, t)) :
517        {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, s2, q)), _)
518          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
519      %all_safe_cell(layout, shown, p, q, mp, B.same(p, q), {==}) :
520        {Bool.and(_, G.all_safe.go(layout, shown, t))
521          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
522      {==}
523
524law all_safe_set_mine:
525  for +w: Nat
526  for +h: Nat
527  for +layout: T.Grid(Bool)
528  for +shown: T.Grid(Bool)
529  for +p: T.Pos
530  for +mp: {B.mine(layout, p) == True{} : Bool}
531  {G.all_safe(w, h, layout, B.set_at(Bool, shown, p, True{})) == G.all_safe(w, h, layout, shown) : Bool}
532
533def all_safe_set_mine(w, h, layout, shown, p, mp):
534  all_safe_set_mine.go(layout, shown, p, mp, B.cells(w, h))
535
536# Opening a cell keeps the invariant
537# ==================================
538
539def inv_open.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
540  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
541  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
542  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
543  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos,
544  +c: Bool, ce: {Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)) == c : Bool},
545  +m: Bool, +me: {B.mine(layout, p) == m : Bool}) ->
546  Inv(w, h, layout, G.open.go(c, m, G.Game{w, h, layout, shown, flags, status}, p)):
547  match c m:
548    case False{} _:
549      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
550    case True{} True{}:
551      +st = playing_is(status, P.and_true_l(G.is_playing(status), G.unrevealed(w, h, shown, p), ce))
552      +s2 = B.set_at(Bool, shown, p, True{})
553      +w0 = {%st : {L.is_won(_) == G.all_safe(w, h, layout, shown) : Bool};
554        won : {False{} == G.all_safe(w, h, layout, shown) : Bool}}
555      ({==}, ({==}, ({==}, (PL.shaped_set(Bool, w, h, shown, p, True{}, sh),
556        (Equal.trans(Bool, False{}, G.all_safe(w, h, layout, shown), G.all_safe(w, h, layout, s2), w0,
557          Equal.sym(Bool, G.all_safe(w, h, layout, s2), G.all_safe(w, h, layout, shown),
558            all_safe_set_mine(w, h, layout, shown, p, me))),
559        ({==}, closed_explode(w, h, layout, shown, p, me, cl)))))))
560    case True{} False{}:
561      +st = playing_is(status, P.and_true_l(G.is_playing(status), G.unrevealed(w, h, shown, p), ce))
562      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
563      +cf = B.count_false(shown)
564      +hh = G.head_hidden(w, h, shown, start)
565      +F = G.flood(cf, start, hh, w, h, layout, shown)
566      +ns = {%st : {Bool.or(Bool.not(G.is_playing(_)), nsm(w, h, layout, shown)) == True{} : Bool};
567        cm : {nsm(w, h, layout, shown) == True{} : Bool}}
568      +ok = {%Equal.sym(Bool, L.same(p, p), True{}, PW.lsame_refl(p)) : {Bool.and(_, True{}) == True{} : Bool};
569        {==} : {PF.works_ok(start, w, h, layout, p) == True{} : Bool}}
570      +safe = {%PC.mine_eq(layout, p) : {_ == False{} : Bool}; me : {L.mine(layout, p) == False{} : Bool}}
571      ({==}, ({==}, ({==}, (PF.flood_shaped(cf, start, hh, w, h, layout, shown, sh),
572        (won_or_playing_won(G.all_safe(w, h, layout, F)),
573        (%Equal.sym(Bool, nsm(w, h, layout, F), True{}, nsm_flood(cf, start, hh, w, h, layout, shown, p, safe, ok, ns)) :
574           {Bool.or(Bool.not(G.is_playing(G.won_or_playing(G.all_safe(w, h, layout, F)))), _) == True{} : Bool};
575           PS.or_true_r(Bool.not(G.is_playing(G.won_or_playing(G.all_safe(w, h, layout, F))))),
576         closed_flood(cf, start, hh, w, h, layout, shown, sh, cl, {==}, {==})))))))
577
578law inv_open:
579  for +w: Nat
580  for +h: Nat
581  for +layout: T.Grid(Bool)
582  for +shown: T.Grid(Bool)
583  for +flags: List<&2, T.Pos>
584  for +status: T.Status
585  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
586  for +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}
587  for +cm: {calm(status, w, h, layout, shown) == True{} : Bool}
588  for +cl: {closed(w, h, layout, shown) == True{} : Bool}
589  for +p: T.Pos
590  Inv(w, h, layout, G.open(G.Game{w, h, layout, shown, flags, status}, p))
591
592def inv_open(w, h, layout, shown, flags, status, sh, won, cm, cl, p):
593  inv_open.go(w, h, layout, shown, flags, status, sh, won, cm, cl, p,
594    Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)), {==}, B.mine(layout, p), {==})
595
596# Every action keeps the invariant
597# ================================
598
599def inv_reveal.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
600  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
601  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
602  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
603  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos, +f: Bool) ->
604  Inv(w, h, layout, G.reveal.go(f, G.Game{w, h, layout, shown, flags, status}, p)):
605  match f:
606    case True{}:
607      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
608    case False{}:
609      inv_open(w, h, layout, shown, flags, status, sh, won, cm, cl, p)
610
611def inv_flag.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
612  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
613  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
614  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
615  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos, +c: Bool) ->
616  Inv(w, h, layout, G.flag.go(c, G.Game{w, h, layout, shown, flags, status}, p)):
617  match c:
618    case False{}:
619      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
620    case True{}:
621      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
622
623def inv_assist.safe(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
624  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
625  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
626  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
627  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +m: Maybe<&2, T.Pos>) ->
628  Inv(w, h, layout, G.assist.safe(m, G.Game{w, h, layout, shown, flags, status})):
629  match m:
630    case None{}:
631      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
632    case Some{p}:
633      inv_open(w, h, layout, shown, flags, status, sh, won, cm, cl, p)
634
635def inv_assist.pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
636  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
637  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
638  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
639  +cl: {closed(w, h, layout, shown) == True{} : Bool},
640  +st: {status == T.Playing{} : T.Status}, +r: Maybe<&2, T.Pos>, +k: Nat) ->
641  Inv(w, h, layout, G.assist.pick(r, G.Game{w, h, layout, shown, flags, status}, k)):
642  match r:
643    case Some{q}:
644      ({==}, ({==}, ({==}, (sh,
645        ({%st : {L.is_won(_) == G.all_safe(w, h, layout, shown) : Bool};
646          won : {False{} == G.all_safe(w, h, layout, shown) : Bool}},
647        ({==}, cl))))))
648    case None{}:
649      inv_assist.safe(w, h, layout, shown, flags, status, sh, won, cm, cl,
650        G.safe_cell(G.Game{w, h, layout, shown, flags, status}, k))
651
652def inv_assist.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
653  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
654  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
655  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
656  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +c: Bool, ce: {G.is_playing(status) == c : Bool}, +k: Nat) ->
657  Inv(w, h, layout, G.assist.go(c, G.Game{w, h, layout, shown, flags, status}, k)):
658  match c:
659    case False{}:
660      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
661    case True{}:
662      +g0 = {G.Game{w, h, layout, shown, flags, status} : G.Game}
663      inv_assist.pick(w, h, layout, shown, flags, status, sh, won, cm, cl, playing_is(status, ce),
664        S.solve(G.knowledge(g0)), k)
665
666# Over a game in its general form.
667law inv_reveal:
668  for +w: Nat
669  for +h: Nat
670  for +layout: T.Grid(Bool)
671  for +g: G.Game
672  for inv: Inv(w, h, layout, g)
673  for +p: T.Pos
674  Inv(w, h, layout, G.reveal(g, p))
675
676def inv_reveal(w, h, layout, g, inv, p):
677  match g:
678    case G.Game{gw, gh, gl, shown, flags, status}:
679      match inv:
680        case (ew, rest):
681          match rest:
682            case (eh, rest2):
683              match rest2:
684                case (el, facts):
685                  match facts:
686                    case (sh, f2):
687                      match f2:
688                        case (won, f3):
689                          match f3:
690                            case (cm, cl):
691                              %Equal.sym(Nat, gw, w, ew) : Inv(w, h, layout, G.reveal(G.Game{_, gh, gl, shown, flags, status}, p))
692                              %Equal.sym(Nat, gh, h, eh) : Inv(w, h, layout, G.reveal(G.Game{w, _, gl, shown, flags, status}, p))
693                              %Equal.sym(T.Grid(Bool), gl, layout, el) :
694                                Inv(w, h, layout, G.reveal(G.Game{w, h, _, shown, flags, status}, p))
695                              inv_reveal.go(w, h, layout, shown, flags, status, sh, won, cm, cl, p,
696                                G.flagged(G.Game{w, h, layout, shown, flags, status}, p))
697
698law inv_flag:
699  for +w: Nat
700  for +h: Nat
701  for +layout: T.Grid(Bool)
702  for +g: G.Game
703  for inv: Inv(w, h, layout, g)
704  for +p: T.Pos
705  Inv(w, h, layout, G.flag(g, p))
706
707def inv_flag(w, h, layout, g, inv, p):
708  match g:
709    case G.Game{gw, gh, gl, shown, flags, status}:
710      match inv:
711        case (ew, rest):
712          match rest:
713            case (eh, rest2):
714              match rest2:
715                case (el, facts):
716                  match facts:
717                    case (sh, f2):
718                      match f2:
719                        case (won, f3):
720                          match f3:
721                            case (cm, cl):
722                              %Equal.sym(Nat, gw, w, ew) : Inv(w, h, layout, G.flag(G.Game{_, gh, gl, shown, flags, status}, p))
723                              %Equal.sym(Nat, gh, h, eh) : Inv(w, h, layout, G.flag(G.Game{w, _, gl, shown, flags, status}, p))
724                              %Equal.sym(T.Grid(Bool), gl, layout, el) :
725                                Inv(w, h, layout, G.flag(G.Game{w, h, _, shown, flags, status}, p))
726                              inv_flag.go(w, h, layout, shown, flags, status, sh, won, cm, cl, p,
727                                G.can_flag(G.Game{w, h, layout, shown, flags, status}, p))
728
729law inv_assist:
730  for +w: Nat
731  for +h: Nat
732  for +layout: T.Grid(Bool)
733  for +g: G.Game
734  for inv: Inv(w, h, layout, g)
735  for +k: Nat
736  Inv(w, h, layout, G.assist(g, k))
737
738def inv_assist(w, h, layout, g, inv, k):
739  match g:
740    case G.Game{gw, gh, gl, shown, flags, status}:
741      match inv:
742        case (ew, rest):
743          match rest:
744            case (eh, rest2):
745              match rest2:
746                case (el, facts):
747                  match facts:
748                    case (sh, f2):
749                      match f2:
750                        case (won, f3):
751                          match f3:
752                            case (cm, cl):
753                              %Equal.sym(Nat, gw, w, ew) : Inv(w, h, layout, G.assist(G.Game{_, gh, gl, shown, flags, status}, k))
754                              %Equal.sym(Nat, gh, h, eh) : Inv(w, h, layout, G.assist(G.Game{w, _, gl, shown, flags, status}, k))
755                              %Equal.sym(T.Grid(Bool), gl, layout, el) :
756                                Inv(w, h, layout, G.assist(G.Game{w, h, _, shown, flags, status}, k))
757                              inv_assist.go(w, h, layout, shown, flags, status, sh, won, cm, cl, G.is_playing(status), {==}, k)
758
759law inv_chord:
760  for +w: Nat
761  for +h: Nat
762  for +layout: T.Grid(Bool)
763  for +ts: List<&2, T.Pos>
764  for +g: G.Game
765  for inv: Inv(w, h, layout, g)
766  Inv(w, h, layout, G.chord_play(ts, g))
767
768def inv_chord(w, h, layout, ts, g, inv):
769  match ts:
770    case Nil{}:
771      inv
772    case q <> t:
773      inv_chord(w, h, layout, t, G.reveal(g, q), inv_reveal(w, h, layout, g, inv, q))
774
775law inv_step:
776  for +w: Nat
777  for +h: Nat
778  for +layout: T.Grid(Bool)
779  for +g: G.Game
780  for inv: Inv(w, h, layout, g)
781  for +a: T.Action
782  Inv(w, h, layout, G.step(g, a))
783
784def inv_step(w, h, layout, g, inv, a):
785  match a:
786    case T.Reveal{p}:
787      inv_reveal(w, h, layout, g, inv, p)
788    case T.Chord{p}:
789      inv_chord(w, h, layout, G.chord_targets(g, p), g, inv)
790    case T.Flag{p}:
791      inv_flag(w, h, layout, g, inv, p)
792    case T.Assist{k}:
793      inv_assist(w, h, layout, g, inv, k)
794
795law inv_play:
796  for +w: Nat
797  for +h: Nat
798  for +layout: T.Grid(Bool)
799  for +acts: List<&2, T.Action>
800  for +g: G.Game
801  for inv: Inv(w, h, layout, g)
802  Inv(w, h, layout, L.play(acts, g))
803
804def inv_play(w, h, layout, acts, g, inv):
805  match acts:
806    case Nil{}:
807      inv
808    case a <> t:
809      inv_play(w, h, layout, t, G.step(g, a), inv_step(w, h, layout, g, inv, a))
810
811law inv_fresh:
812  for +w: Nat
813  for +h: Nat
814  for +layout: T.Grid(Bool)
815  Inv(w, h, layout, G.fresh(w, h, layout))
816
817def inv_fresh(w, h, layout):
818  +bl = B.blank(Bool, w, h, False{})
819  +st = G.won_or_playing(G.all_safe(w, h, layout, bl))
820  ({==}, ({==}, ({==}, (PL.blank_shaped(Bool, w, h, False{}),
821    (won_or_playing_won(G.all_safe(w, h, layout, bl)),
822    (%Equal.sym(Bool, nsm(w, h, layout, bl), True{}, nsm_blank(w, h, layout)) :
823       {Bool.or(Bool.not(G.is_playing(st)), _) == True{} : Bool};
824       PS.or_true_r(Bool.not(G.is_playing(st))),
825     closed_blank(w, h, layout)))))))
826
827# Every real game satisfies the invariant.
828law inv_reach:
829  for +w: Nat
830  for +h: Nat
831  for +layout: T.Grid(Bool)
832  for +g: G.Game
833  for r: L.Reachable(w, h, layout, g)
834  Inv(w, h, layout, g)
835
836def inv_reach(w, h, layout, g, r):
837  match r:
838    case (acts, e):
839      %e : Inv(w, h, layout, _)
840      inv_play(w, h, layout, acts, G.fresh(w, h, layout), inv_fresh(w, h, layout))