proof_cells.bend

minebender-game@1.0.0.0 · 613 lines · 48 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/LAWS.bend as L
5import minebender-game@1.0.0.0/proof_base.bend as P
6import minebender-game@1.0.0.0/proof_grid.bend as PG
7import minebender-game@1.0.0.0/proof_copy.bend as PC
8
9# Lemmas about lists of cells: membership, the board's cells, neighbours.
10
11# Every cell of ps passes f (with e for f's context).
12def allp(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, ps: List<&2, T.Pos>) -> Bool:
13  match ps:
14    case Nil{}:
15      True{}
16    case q <> t:
17      f(e, q) && allp(~E, ~f, e, t)
18
19def allp_head(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, +q: T.Pos, +t: List<&2, T.Pos>,
20  h: {allp(~E, ~f, e, q <> t) == True{} : Bool}) -> {f(e, q) == True{} : Bool}:
21  P.and_true_l(f(e, q), allp(~E, ~f, e, t), h)
22
23def allp_tail(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, +q: T.Pos, +t: List<&2, T.Pos>,
24  h: {allp(~E, ~f, e, q <> t) == True{} : Bool}) -> {allp(~E, ~f, e, t) == True{} : Bool}:
25  P.and_true_r(f(e, q), allp(~E, ~f, e, t), h)
26
27def allp_member.go(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, +p: T.Pos, +t: List<&2, T.Pos>, +q: T.Pos,
28  +hd: {f(e, p) == True{} : Bool}, +b: Bool, be: {B.same(p, q) == b : Bool},
29  m: {Bool.or(b, B.contains(t, q)) == True{} : Bool},
30  ih: {B.contains(t, q) == True{} : Bool} -> {f(e, q) == True{} : Bool}) -> {f(e, q) == True{} : Bool}:
31  match b:
32    case True{}:
33      %PG.same_sound(p, q, be) : {f(e, _) == True{} : Bool}
34      hd
35    case False{}:
36      ih(m)
37
38# A cell of a list whose cells all pass f passes f.
39def allp_member(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, ps: List<&2, T.Pos>, +q: T.Pos,
40  +h: {allp(~E, ~f, e, ps) == True{} : Bool}, m: {B.contains(ps, q) == True{} : Bool}) ->
41  {f(e, q) == True{} : Bool}:
42  match ps:
43    case Nil{}:
44      Empty.absurd({f(e, q) == True{} : Bool}, P.false_ne_true(m))
45    case +p <> +t:
46      allp_member.go(~E, ~f, e, p, t, q, allp_head(~E, ~f, e, p, t, h), B.same(p, q), {==}, m,
47        mt => allp_member(~E, ~f, e, t, q, allp_tail(~E, ~f, e, p, t, h), mt))
48
49# Membership
50# ==========
51
52def contains_append.or(+a: Bool, +b: Bool, +c: Bool) ->
53  {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}:
54  match a:
55    case True{}:
56      {==}
57    case False{}:
58      {==}
59
60law contains_append:
61  for +xs: List<&2, T.Pos>
62  for +ys: List<&2, T.Pos>
63  for +q: T.Pos
64  {B.contains(List.append(&2, T.Pos, xs, ys), q) == Bool.or(B.contains(xs, q), B.contains(ys, q)) : Bool}
65
66def contains_append(xs, ys, q):
67  match xs:
68    case Nil{}:
69      {==}
70    case p <> t:
71      %Equal.sym(Bool, B.contains(List.append(&2, T.Pos, t, ys), q), Bool.or(B.contains(t, q), B.contains(ys, q)),
72        contains_append(t, ys, q)) :
73        {Bool.or(B.same(p, q), _) == Bool.or(Bool.or(B.same(p, q), B.contains(t, q)), B.contains(ys, q)) : Bool}
74      contains_append.or(B.same(p, q), B.contains(t, q), B.contains(ys, q))
75
76# A Nat list contains i.
77def memn(xs: List<&2, Nat>, +i: Nat) -> Bool:
78  match xs:
79    case Nil{}:
80      False{}
81    case x <> t:
82      Nat.is_eq(x, i) || memn(t, i)
83
84def or_true_r(+a: Bool) -> {Bool.or(a, True{}) == True{} : Bool}:
85  match a:
86    case True{}:
87      {==}
88    case False{}:
89      {==}
90
91law memn_append_r:
92  for +xs: List<&2, Nat>
93  for +ys: List<&2, Nat>
94  for +i: Nat
95  for e: {memn(ys, i) == True{} : Bool}
96  {memn(List.append(&2, Nat, xs, ys), i) == True{} : Bool}
97
98def memn_append_r(xs, ys, i, e):
99  match xs:
100    case Nil{}:
101      e
102    case x <> t:
103      %Equal.sym(Bool, memn(List.append(&2, Nat, t, ys), i), True{}, memn_append_r(t, ys, i, e)) :
104        {Bool.or(Nat.is_eq(x, i), _) == True{} : Bool}
105      or_true_r(Nat.is_eq(x, i))
106
107law memn_append_l:
108  for +xs: List<&2, Nat>
109  for +ys: List<&2, Nat>
110  for +i: Nat
111  for e: {memn(xs, i) == True{} : Bool}
112  {memn(List.append(&2, Nat, xs, ys), i) == True{} : Bool}
113
114def memn_append_l.go(+x: Nat, +t: List<&2, Nat>, +ys: List<&2, Nat>, +i: Nat, +b: Bool,
115  e: {Bool.or(b, memn(t, i)) == True{} : Bool},
116  ih: {memn(t, i) == True{} : Bool} -> {memn(List.append(&2, Nat, t, ys), i) == True{} : Bool}) ->
117  {Bool.or(b, memn(List.append(&2, Nat, t, ys), i)) == True{} : Bool}:
118  match b:
119    case True{}:
120      {==}
121    case False{}:
122      ih(e)
123
124def memn_append_l(xs, ys, i, e):
125  match xs:
126    case Nil{}:
127      Empty.absurd({memn(ys, i) == True{} : Bool}, P.false_ne_true(e))
128    case x <> t:
129      memn_append_l.go(x, t, ys, i, Nat.is_eq(x, i), e, et => memn_append_l(t, ys, i, et))
130
131def memn_range.cases(+p: Nat, +i: Nat, r: Or({Nat.is_lt(i, p) == True{} : Bool}, {i == p : Nat}),
132  ih: {Nat.is_lt(i, p) == True{} : Bool} -> {memn(List.range(p), i) == True{} : Bool}) ->
133  {memn(List.append(&2, Nat, List.range(p), [p]), i) == True{} : Bool}:
134  match r:
135    case Inl{lt}:
136      memn_append_l(List.range(p), [p], i, ih(lt))
137    case Inr{eq}:
138      memn_append_r(List.range(p), [p], i,
139        %Equal.sym(Nat, i, p, eq) : {Bool.or(Nat.is_eq(p, _), False{}) == True{} : Bool};
140        %Equal.sym(Bool, Nat.is_eq(p, p), True{}, P.eq_refl(p)) : {Bool.or(_, False{}) == True{} : Bool};
141        {==})
142
143law memn_range:
144  for +n: Nat
145  for +i: Nat
146  for e: {Nat.is_lt(i, n) == True{} : Bool}
147  {memn(List.range(n), i) == True{} : Bool}
148
149def memn_range(n, i, e):
150  match n:
151    case 0n:
152      Empty.absurd({memn(List.range(0n), i) == True{} : Bool},
153        P.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(i, 0n), True{},
154          Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, P.lt_zero(i)), e)))
155    case 1n+p:
156      %Equal.sym(List<&2, Nat>, List.range(1n+p), List.append(&2, Nat, List.range(p), [p]), P.range_snoc(p)) :
157        {memn(_, i) == True{} : Bool}
158      memn_range.cases(p, i, P.lt_succ(i, p, e), lt => memn_range(p, i, lt))
159
160def contains_row.go(+y: Nat, +a: Nat, +t: List<&2, Nat>, +x: Nat, +b: Bool,
161  e: {Bool.or(b, memn(t, x)) == True{} : Bool}, be: {Nat.is_eq(a, x) == b : Bool},
162  ih: {memn(t, x) == True{} : Bool} -> {B.contains(B.row_cells(y, t), T.Pos{x, y}) == True{} : Bool}) ->
163  {Bool.or(B.same(T.Pos{a, y}, T.Pos{x, y}), B.contains(B.row_cells(y, t), T.Pos{x, y})) == True{} : Bool}:
164  match b:
165    case True{}:
166      %Equal.sym(Bool, Nat.is_eq(a, x), True{}, be) :
167        {Bool.or(Bool.and(_, Nat.is_eq(y, y)), B.contains(B.row_cells(y, t), T.Pos{x, y})) == True{} : Bool}
168      %Equal.sym(Bool, Nat.is_eq(y, y), True{}, P.eq_refl(y)) :
169        {Bool.or(Bool.and(True{}, _), B.contains(B.row_cells(y, t), T.Pos{x, y})) == True{} : Bool}
170      {==}
171    case False{}:
172      %Equal.sym(Bool, B.contains(B.row_cells(y, t), T.Pos{x, y}), True{}, ih(e)) :
173        {Bool.or(B.same(T.Pos{a, y}, T.Pos{x, y}), _) == True{} : Bool}
174      or_true_r(B.same(T.Pos{a, y}, T.Pos{x, y}))
175
176law contains_row:
177  for +y: Nat
178  for +xs: List<&2, Nat>
179  for +x: Nat
180  for e: {memn(xs, x) == True{} : Bool}
181  {B.contains(B.row_cells(y, xs), T.Pos{x, y}) == True{} : Bool}
182
183def contains_row(y, xs, x, e):
184  match xs:
185    case Nil{}:
186      Empty.absurd({B.contains(Nil{}, T.Pos{x, y}) == True{} : Bool}, P.false_ne_true(e))
187    case a <> t:
188      contains_row.go(y, a, t, x, Nat.is_eq(a, x), e, {==}, et => contains_row(y, t, x, et))
189
190def contains_cells.k(+w: Nat, +a: Nat, +t: List<&2, Nat>, +x: Nat, +y: Nat,
191  xm: {memn(List.range(w), x) == True{} : Bool}, +b: Bool,
192  e: {Bool.or(b, memn(t, y)) == True{} : Bool}, be: {Nat.is_eq(a, y) == b : Bool},
193  ih: {memn(t, y) == True{} : Bool} -> {B.contains(B.cells.go(w, t), T.Pos{x, y}) == True{} : Bool}) ->
194  {Bool.or(B.contains(B.row_cells(a, List.range(w)), T.Pos{x, y}), B.contains(B.cells.go(w, t), T.Pos{x, y}))
195    == True{} : Bool}:
196  match b:
197    case True{}:
198      %P.eq_sound(a, y, be) :
199        {Bool.or(B.contains(B.row_cells(a, List.range(w)), T.Pos{x, _}), B.contains(B.cells.go(w, t), T.Pos{x, y}))
200          == True{} : Bool}
201      %Equal.sym(Bool, B.contains(B.row_cells(a, List.range(w)), T.Pos{x, a}), True{},
202        contains_row(a, List.range(w), x, xm)) :
203        {Bool.or(_, B.contains(B.cells.go(w, t), T.Pos{x, y})) == True{} : Bool}
204      {==}
205    case False{}:
206      %Equal.sym(Bool, B.contains(B.cells.go(w, t), T.Pos{x, y}), True{}, ih(e)) :
207        {Bool.or(B.contains(B.row_cells(a, List.range(w)), T.Pos{x, y}), _) == True{} : Bool}
208      or_true_r(B.contains(B.row_cells(a, List.range(w)), T.Pos{x, y}))
209
210def contains_cells.go(+w: Nat, +a: Nat, +t: List<&2, Nat>, +x: Nat, +y: Nat,
211  xm: {memn(List.range(w), x) == True{} : Bool}, +b: Bool,
212  e: {Bool.or(b, memn(t, y)) == True{} : Bool}, be: {Nat.is_eq(a, y) == b : Bool},
213  ih: {memn(t, y) == True{} : Bool} -> {B.contains(B.cells.go(w, t), T.Pos{x, y}) == True{} : Bool}) ->
214  {B.contains(List.append(&2, T.Pos, B.row_cells(a, List.range(w)), B.cells.go(w, t)), T.Pos{x, y}) == True{} : Bool}:
215  +row = B.row_cells(a, List.range(w))
216  %Equal.sym(Bool, B.contains(List.append(&2, T.Pos, row, B.cells.go(w, t)), T.Pos{x, y}),
217    Bool.or(B.contains(row, T.Pos{x, y}), B.contains(B.cells.go(w, t), T.Pos{x, y})),
218    contains_append(row, B.cells.go(w, t), T.Pos{x, y})) : {_ == True{} : Bool}
219  contains_cells.k(w, a, t, x, y, xm, b, e, be, ih)
220
221law contains_cells:
222  for +w: Nat
223  for +ys: List<&2, Nat>
224  for +x: Nat
225  for +y: Nat
226  for +xm: {memn(List.range(w), x) == True{} : Bool}
227  for e: {memn(ys, y) == True{} : Bool}
228  {B.contains(B.cells.go(w, ys), T.Pos{x, y}) == True{} : Bool}
229
230def contains_cells(w, ys, x, y, xm, e):
231  match ys:
232    case Nil{}:
233      Empty.absurd({B.contains(Nil{}, T.Pos{x, y}) == True{} : Bool}, P.false_ne_true(e))
234    case a <> t:
235      contains_cells.go(w, a, t, x, y, xm, Nat.is_eq(a, y), e, {==}, et => contains_cells(w, t, x, y, xm, et))
236
237# Every cell of the board is one of its cells.
238law cells_member:
239  for +w: Nat
240  for +h: Nat
241  for +q: T.Pos
242  for +on: {B.on_board(w, h, q) == True{} : Bool}
243  {B.contains(B.cells(w, h), q) == True{} : Bool}
244
245def cells_member(w, h, q, on):
246  match q:
247    case T.Pos{x, y}:
248      contains_cells(w, List.range(h), x, y,
249        memn_range(w, x, P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)),
250        memn_range(h, y, P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)))
251
252# The board's cells are on the board
253# ==================================
254
255type WH is Data:
256  WH{w: Nat, h: Nat}
257
258def onb(e: WH, q: T.Pos) -> Bool:
259  match e:
260    case WH{w, h}:
261      B.on_board(w, h, q)
262
263law allp_append:
264  for ~E: Data
265  for ~f: E -> T.Pos -> Bool
266  for +e: E
267  for +xs: List<&2, T.Pos>
268  for +ys: List<&2, T.Pos>
269  for +a: {allp(~E, ~f, e, xs) == True{} : Bool}
270  for b: {allp(~E, ~f, e, ys) == True{} : Bool}
271  {allp(~E, ~f, e, List.append(&2, T.Pos, xs, ys)) == True{} : Bool}
272
273def allp_append(E, f, e, xs, ys, a, b):
274  match xs:
275    case Nil{}:
276      b
277    case q <> t:
278      %Equal.sym(Bool, allp(~E, ~f, e, List.append(&2, T.Pos, t, ys)), True{},
279        allp_append(~E, ~f, e, t, ys, allp_tail(~E, ~f, e, q, t, a), b)) :
280        {Bool.and(f(e, q), _) == True{} : Bool}
281      %Equal.sym(Bool, f(e, q), True{}, allp_head(~E, ~f, e, q, t, a)) :
282        {Bool.and(_, True{}) == True{} : Bool}
283      {==}
284
285# Every element of xs is below n.
286def alln(xs: List<&2, Nat>, +n: Nat) -> Bool:
287  match xs:
288    case Nil{}:
289      True{}
290    case x <> t:
291      Nat.is_lt(x, n) && alln(t, n)
292
293law lt_mono:
294  for +i: Nat
295  for +n: Nat
296  for e: {Nat.is_lt(i, n) == True{} : Bool}
297  {Nat.is_lt(i, 1n+n) == True{} : Bool}
298
299def lt_mono(i, n, e):
300  match i n:
301    case 0n _:
302      {==}
303    case 1n+j 0n:
304      Empty.absurd({Nat.is_lt(1n+j, 1n) == True{} : Bool}, P.false_ne_true(e))
305    case 1n+j 1n+m:
306      lt_mono(j, m, e)
307
308law lt_succ_self:
309  for +n: Nat
310  {Nat.is_lt(n, 1n+n) == True{} : Bool}
311
312def lt_succ_self(n):
313  match n:
314    case 0n:
315      {==}
316    case 1n+p:
317      lt_succ_self(p)
318
319law alln_mono:
320  for +xs: List<&2, Nat>
321  for +n: Nat
322  for +e: {alln(xs, n) == True{} : Bool}
323  {alln(xs, 1n+n) == True{} : Bool}
324
325def alln_mono(xs, n, e):
326  match xs:
327    case Nil{}:
328      {==}
329    case x <> t:
330      %Equal.sym(Bool, Nat.is_lt(x, 1n+n), True{},
331        lt_mono(x, n, P.and_true_l(Nat.is_lt(x, n), alln(t, n), e))) :
332        {Bool.and(_, alln(t, 1n+n)) == True{} : Bool}
333      alln_mono(t, n, P.and_true_r(Nat.is_lt(x, n), alln(t, n), e))
334
335law alln_append:
336  for +xs: List<&2, Nat>
337  for +ys: List<&2, Nat>
338  for +n: Nat
339  for +a: {alln(xs, n) == True{} : Bool}
340  for b: {alln(ys, n) == True{} : Bool}
341  {alln(List.append(&2, Nat, xs, ys), n) == True{} : Bool}
342
343def alln_append(xs, ys, n, a, b):
344  match xs:
345    case Nil{}:
346      b
347    case x <> t:
348      %Equal.sym(Bool, Nat.is_lt(x, n), True{}, P.and_true_l(Nat.is_lt(x, n), alln(t, n), a)) :
349        {Bool.and(_, alln(List.append(&2, Nat, t, ys), n)) == True{} : Bool}
350      alln_append(t, ys, n, P.and_true_r(Nat.is_lt(x, n), alln(t, n), a), b)
351
352law alln_range:
353  for +n: Nat
354  {alln(List.range(n), n) == True{} : Bool}
355
356def alln_range(n):
357  match n:
358    case 0n:
359      {==}
360    case 1n+p:
361      %Equal.sym(List<&2, Nat>, List.range(1n+p), List.append(&2, Nat, List.range(p), [p]), P.range_snoc(p)) :
362        {alln(_, 1n+p) == True{} : Bool}
363      alln_append(List.range(p), [p], 1n+p, alln_mono(List.range(p), p, alln_range(p)),
364        %Equal.sym(Bool, Nat.is_lt(p, 1n+p), True{}, lt_succ_self(p)) :
365          {Bool.and(_, True{}) == True{} : Bool}; {==})
366
367law row_on:
368  for +w: Nat
369  for +h: Nat
370  for +y: Nat
371  for +xs: List<&2, Nat>
372  for +yh: {Nat.is_lt(y, h) == True{} : Bool}
373  for +xw: {alln(xs, w) == True{} : Bool}
374  {allp(~WH, ~onb, WH{w, h}, B.row_cells(y, xs)) == True{} : Bool}
375
376def row_on(w, h, y, xs, yh, xw):
377  match xs:
378    case Nil{}:
379      {==}
380    case x <> t:
381      %Equal.sym(Bool, Nat.is_lt(x, w), True{}, P.and_true_l(Nat.is_lt(x, w), alln(t, w), xw)) :
382        {Bool.and(Bool.and(_, Nat.is_lt(y, h)), allp(~WH, ~onb, WH{w, h}, B.row_cells(y, t))) == True{} : Bool}
383      %Equal.sym(Bool, Nat.is_lt(y, h), True{}, yh) :
384        {Bool.and(Bool.and(True{}, _), allp(~WH, ~onb, WH{w, h}, B.row_cells(y, t))) == True{} : Bool}
385      row_on(w, h, y, t, yh, P.and_true_r(Nat.is_lt(x, w), alln(t, w), xw))
386
387law cells_on.go:
388  for +w: Nat
389  for +h: Nat
390  for +ys: List<&2, Nat>
391  for +yh: {alln(ys, h) == True{} : Bool}
392  {allp(~WH, ~onb, WH{w, h}, B.cells.go(w, ys)) == True{} : Bool}
393
394def cells_on.go(w, h, ys, yh):
395  match ys:
396    case Nil{}:
397      {==}
398    case y <> t:
399      allp_append(~WH, ~onb, WH{w, h}, B.row_cells(y, List.range(w)), B.cells.go(w, t),
400        row_on(w, h, y, List.range(w), P.and_true_l(Nat.is_lt(y, h), alln(t, h), yh), alln_range(w)),
401        cells_on.go(w, h, t, P.and_true_r(Nat.is_lt(y, h), alln(t, h), yh)))
402
403# Every cell of cells(w, h) is on the board.
404law cells_on:
405  for +w: Nat
406  for +h: Nat
407  {allp(~WH, ~onb, WH{w, h}, B.cells(w, h)) == True{} : Bool}
408
409def cells_on(w, h):
410  cells_on.go(w, h, List.range(h), alln_range(h))
411
412# Neighbours
413# ==========
414
415law put_keeps:
416  for +e0: T.Pos
417  for +xs: List<&2, T.Pos>
418  for +c: Bool
419  for +r: T.Pos
420  for m: {B.contains(xs, r) == True{} : Bool}
421  {B.contains(List.filter.put(T.Pos, e0, xs, c), r) == True{} : Bool}
422
423def put_keeps(e0, xs, c, r, m):
424  match c:
425    case True{}:
426      %Equal.sym(Bool, B.contains(xs, r), True{}, m) : {Bool.or(B.same(e0, r), _) == True{} : Bool}
427      or_true_r(B.same(e0, r))
428    case False{}:
429      m
430
431def touching_member.go(+s: T.Pos, +e0: T.Pos, +t: List<&2, T.Pos>, +r: T.Pos,
432  a: {B.adjacent(s, r) == True{} : Bool}, +b: Bool, be: {B.same(e0, r) == b : Bool},
433  m: {Bool.or(b, B.contains(t, r)) == True{} : Bool},
434  ih: {B.contains(t, r) == True{} : Bool} -> {B.contains(B.touching(s, t), r) == True{} : Bool}) ->
435  {B.contains(List.filter.put(T.Pos, e0, B.touching(s, t), B.adjacent(s, e0)), r) == True{} : Bool}:
436  match b:
437    case True{}:
438      %Equal.sym(T.Pos, e0, r, PG.same_sound(e0, r, be)) :
439        {B.contains(List.filter.put(T.Pos, _, B.touching(s, t), B.adjacent(s, _)), r) == True{} : Bool}
440      %Equal.sym(Bool, B.adjacent(s, r), True{}, a) :
441        {B.contains(List.filter.put(T.Pos, r, B.touching(s, t), _), r) == True{} : Bool}
442      PG.contains_cons_self(r, B.touching(s, t))
443    case False{}:
444      put_keeps(e0, B.touching(s, t), B.adjacent(s, e0), r, ih(m))
445
446law touching_member:
447  for +s: T.Pos
448  for +xs: List<&2, T.Pos>
449  for +r: T.Pos
450  for +a: {B.adjacent(s, r) == True{} : Bool}
451  for m: {B.contains(xs, r) == True{} : Bool}
452  {B.contains(B.touching(s, xs), r) == True{} : Bool}
453
454def touching_member(s, xs, r, a, m):
455  match xs:
456    case Nil{}:
457      Empty.absurd({B.contains(Nil{}, r) == True{} : Bool}, P.false_ne_true(m))
458    case e0 <> t:
459      touching_member.go(s, e0, t, r, a, B.same(e0, r), {==}, m, mt => touching_member(s, t, r, a, mt))
460
461# An adjacent cell of the board is a neighbour.
462law neighbours_member:
463  for +w: Nat
464  for +h: Nat
465  for +s: T.Pos
466  for +r: T.Pos
467  for on: {B.on_board(w, h, r) == True{} : Bool}
468  for a: {B.adjacent(s, r) == True{} : Bool}
469  {B.contains(B.neighbours(w, h, s), r) == True{} : Bool}
470
471def neighbours_member(w, h, s, r, on, a):
472  touching_member(s, B.cells(w, h), r, a, cells_member(w, h, r, on))
473
474type WHS is Data:
475  WHS{w: Nat, h: Nat, s: T.Pos}
476
477def adj_on.go(e: WHS, +q: T.Pos) -> Bool:
478  match e:
479    case WHS{w, h, s}:
480      B.adjacent(s, q) && B.on_board(w, h, q)
481
482def adj_on(e: WHS, q: T.Pos) -> Bool:
483  adj_on.go(e, q)
484
485def touching_all.go(+w: Nat, +h: Nat, +s: T.Pos, +q: T.Pos, +t: List<&2, T.Pos>,
486  qon: {B.on_board(w, h, q) == True{} : Bool}, +c: Bool, ce: {B.adjacent(s, q) == c : Bool},
487  ih: {allp(~WHS, ~adj_on, WHS{w, h, s}, B.touching(s, t)) == True{} : Bool}) ->
488  {allp(~WHS, ~adj_on, WHS{w, h, s}, List.filter.put(T.Pos, q, B.touching(s, t), c)) == True{} : Bool}:
489  match c:
490    case True{}:
491      %Equal.sym(Bool, B.adjacent(s, q), True{}, ce) :
492        {Bool.and(Bool.and(_, B.on_board(w, h, q)), allp(~WHS, ~adj_on, WHS{w, h, s}, B.touching(s, t))) == True{} : Bool}
493      %Equal.sym(Bool, B.on_board(w, h, q), True{}, qon) :
494        {Bool.and(Bool.and(True{}, _), allp(~WHS, ~adj_on, WHS{w, h, s}, B.touching(s, t))) == True{} : Bool}
495      ih
496    case False{}:
497      ih
498
499law touching_all:
500  for +w: Nat
501  for +h: Nat
502  for +s: T.Pos
503  for +xs: List<&2, T.Pos>
504  for +on: {allp(~WH, ~onb, WH{w, h}, xs) == True{} : Bool}
505  {allp(~WHS, ~adj_on, WHS{w, h, s}, B.touching(s, xs)) == True{} : Bool}
506
507def touching_all(w, h, s, xs, on):
508  match xs:
509    case Nil{}:
510      {==}
511    case q <> t:
512      touching_all.go(w, h, s, q, t, allp_head(~WH, ~onb, WH{w, h}, q, t, on), B.adjacent(s, q), {==},
513        touching_all(w, h, s, t, allp_tail(~WH, ~onb, WH{w, h}, q, t, on)))
514
515# Every neighbour of s is adjacent to s and on the board.
516law neighbours_all:
517  for +w: Nat
518  for +h: Nat
519  for +s: T.Pos
520  {allp(~WHS, ~adj_on, WHS{w, h, s}, B.neighbours(w, h, s)) == True{} : Bool}
521
522def neighbours_all(w, h, s):
523  touching_all(w, h, s, B.cells(w, h), cells_on(w, h))
524
525# Zeros
526# =====
527
528law add_zero_l:
529  for +a: Nat
530  for +b: Nat
531  for e: {Nat.add(a, b) == 0n : Nat}
532  {a == 0n : Nat}
533
534def add_zero_l(a, b, e):
535  match a:
536    case 0n:
537      {==}
538    case 1n+p:
539      Empty.absurd({1n+p == 0n : Nat}, P.succ_ne_zero(Nat.add(p, b), e))
540
541law add_zero_r:
542  for +a: Nat
543  for +b: Nat
544  for e: {Nat.add(a, b) == 0n : Nat}
545  {b == 0n : Nat}
546
547def add_zero_r(a, b, e):
548  match a:
549    case 0n:
550      e
551    case 1n+p:
552      Empty.absurd({b == 0n : Nat}, P.succ_ne_zero(Nat.add(p, b), e))
553
554law one_zero:
555  for +b: Bool
556  for e: {Bool.pick(Nat, b, 1n, 0n) == 0n : Nat}
557  {b == False{} : Bool}
558
559def one_zero(b, e):
560  match b:
561    case False{}:
562      {==}
563    case True{}:
564      Empty.absurd({True{} == False{} : Bool}, P.succ_ne_zero(0n, e))
565
566def count_zero_member.go(+layout: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>, +r: T.Pos,
567  mq: {B.mine(layout, q) == False{} : Bool}, +b: Bool, be: {B.same(q, r) == b : Bool},
568  m: {Bool.or(b, B.contains(t, r)) == True{} : Bool},
569  ih: {B.contains(t, r) == True{} : Bool} -> {B.mine(layout, r) == False{} : Bool}) ->
570  {B.mine(layout, r) == False{} : Bool}:
571  match b:
572    case True{}:
573      %PG.same_sound(q, r, be) : {B.mine(layout, _) == False{} : Bool}
574      mq
575    case False{}:
576      ih(m)
577
578# A list with no mines has no mine on any of its cells.
579law count_zero_member:
580  for +layout: T.Grid(Bool)
581  for +ns: List<&2, T.Pos>
582  for +r: T.Pos
583  for +z: {B.count_mines(layout, ns) == 0n : Nat}
584  for m: {B.contains(ns, r) == True{} : Bool}
585  {B.mine(layout, r) == False{} : Bool}
586
587def count_zero_member(layout, ns, r, z, m):
588  match ns:
589    case Nil{}:
590      Empty.absurd({B.mine(layout, r) == False{} : Bool}, P.false_ne_true(m))
591    case q <> t:
592      +c = B.count_mines(layout, t)
593      count_zero_member.go(layout, q, t, r,
594        one_zero(B.mine(layout, q), add_zero_l(Bool.pick(Nat, B.mine(layout, q), 1n, 0n), c, z)),
595        B.same(q, r), {==}, m,
596        mt => count_zero_member(layout, t, r, add_zero_r(Bool.pick(Nat, B.mine(layout, q), 1n, 0n), c, z), mt))
597
598# The neighbours of a zero have no mines.
599law zero_nbr:
600  for +w: Nat
601  for +h: Nat
602  for +layout: T.Grid(Bool)
603  for +s: T.Pos
604  for +r: T.Pos
605  for z: {B.zero(w, h, layout, s) == True{} : Bool}
606  for m: {B.contains(B.neighbours(w, h, s), r) == True{} : Bool}
607  {B.mine(layout, r) == False{} : Bool}
608
609def zero_nbr(w, h, layout, s, r, z, m):
610  +a = Bool.and(B.on_board(w, h, s), Bool.not(B.mine(layout, s)))
611  +adj = B.adj_mines(w, h, layout, s)
612  count_zero_member(layout, B.neighbours(w, h, s), r,
613    P.eq_sound(adj, 0n, P.and_true_r(a, Nat.is_eq(adj, 0n), z)), m)