proof_lists.bend

minebender-game@1.0.0.0 · 563 lines · 32 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/proof_base.bend as P
5
6# Lemmas about updating lists and grids.
7
8def Maybe.disc_n(-A: Data, m: Maybe<&2, A>) -> Type:
9  match m:
10    case None{}:
11      Unit
12    case Some{v}:
13      Empty
14
15def none_ne_some(-A: Data, -x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:
16  %e : Maybe.disc_n(A, _)
17  Unit{}
18
19def Maybe.val(-A: Data, +d: A, m: Maybe<&2, A>) -> A:
20  match m:
21    case None{}:
22      d
23    case Some{v}:
24      v
25
26def some_inj(-A: Data, +a: A, +x: A, e: {Some{a} == Some{x} : Maybe<&2, A>}) -> {a == x : A}:
27  Equal.cong(Maybe<&2, A>, A, m => Maybe.val(A, a, m), Some{a}, Some{x}, e)
28
29# List.set
30# ========
31
32law set_len:
33  for -A: Data
34  for +xs: List<&2, A>
35  for +i: Nat
36  for +v: A
37  {List.length(&2, A, List.set(&2, A, xs, i, v)) == List.length(&2, A, xs) : Nat}
38
39def set_len(A, xs, i, v):
40  match xs i:
41    case Nil{} _:
42      {==}
43    case h <> t 0n:
44      {==}
45    case h <> t 1n+k:
46      %Equal.sym(Nat, List.length(&2, A, List.set(&2, A, t, k, v)), List.length(&2, A, t), set_len(A, t, k, v)) :
47        {1n+_ == 1n+List.length(&2, A, t) : Nat}
48      {==}
49
50law get_set_eq:
51  for -A: Data
52  for +xs: List<&2, A>
53  for +i: Nat
54  for +v: A
55  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
56  {List.get(&2, A, List.set(&2, A, xs, i, v), i) == Some{v} : Maybe<&2, A>}
57
58def get_set_eq(A, xs, i, v, e):
59  match xs i:
60    case Nil{} _:
61      Empty.absurd({List.get(&2, A, List.set(&2, A, Nil{}, i, v), i) == Some{v} : Maybe<&2, A>},
62        P.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(i, 0n), True{},
63          Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, P.lt_zero(i)), e)))
64    case h <> t 0n:
65      {==}
66    case h <> t 1n+k:
67      get_set_eq(A, t, k, v, e)
68
69law get_set_ne:
70  for -A: Data
71  for +xs: List<&2, A>
72  for +i: Nat
73  for +j: Nat
74  for +v: A
75  for e: {Nat.is_eq(i, j) == False{} : Bool}
76  {List.get(&2, A, List.set(&2, A, xs, i, v), j) == List.get(&2, A, xs, j) : Maybe<&2, A>}
77
78def get_set_ne(A, xs, i, j, v, e):
79  match xs i j:
80    case Nil{} _ _:
81      {==}
82    case h <> t 0n 0n:
83      Empty.absurd({List.get(&2, A, v <> t, 0n) == List.get(&2, A, h <> t, 0n) : Maybe<&2, A>},
84        P.true_ne_false(e))
85    case h <> t 0n 1n+q:
86      {==}
87    case h <> t 1n+k 0n:
88      {==}
89    case h <> t 1n+k 1n+q:
90      get_set_ne(A, t, k, q, v, e)
91
92# Setting an index past the end changes nothing.
93law set_out:
94  for -A: Data
95  for +xs: List<&2, A>
96  for +i: Nat
97  for +v: A
98  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool}
99  {List.set(&2, A, xs, i, v) == xs : List<&2, A>}
100
101def set_out(A, xs, i, v, e):
102  match xs i:
103    case Nil{} _:
104      {==}
105    case h <> t 0n:
106      Empty.absurd({List.set(&2, A, h <> t, 0n, v) == h <> t : List<&2, A>}, P.true_ne_false(e))
107    case h <> t 1n+k:
108      %Equal.sym(List<&2, A>, List.set(&2, A, t, k, v), t, set_out(A, t, k, v, e)) :
109        {h <> _ == h <> t : List<&2, A>}
110      {==}
111
112# Inside a list, an index reads Some of its default.
113law get_in:
114  for -A: Data
115  for +xs: List<&2, A>
116  for +i: Nat
117  for +d: A
118  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
119  {List.get(&2, A, xs, i) == Some{Maybe.default(&2, A, List.get(&2, A, xs, i), d)} : Maybe<&2, A>}
120
121def get_in(A, xs, i, d, e):
122  match xs i:
123    case Nil{} _:
124      Empty.absurd({List.get(&2, A, Nil{}, i) == Some{Maybe.default(&2, A, List.get(&2, A, Nil{}, i), d)}
125        : Maybe<&2, A>},
126        P.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(i, 0n), True{},
127          Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, P.lt_zero(i)), e)))
128    case h <> t 0n:
129      {==}
130    case h <> t 1n+k:
131      get_in(A, t, k, d, e)
132
133# A row of a grid whose rows all have w cells has w cells.
134law rows_wide_get:
135  for -A: Data
136  for +w: Nat
137  for +g: T.Grid(A)
138  for +i: Nat
139  for +r: List<&2, A>
140  for wide: {B.rows_wide(A, w, g) == True{} : Bool}
141  for e: {List.get(&2, List<&2, A>, g, i) == Some{r} : Maybe<&2, List<&2, A>>}
142  {List.length(&2, A, r) == w : Nat}
143
144def rows_wide_get(A, w, g, i, r, wide, e):
145  match g i:
146    case Nil{} _:
147      Empty.absurd({List.length(&2, A, r) == w : Nat}, none_ne_some(List<&2, A>, r, e))
148    case row <> t 0n:
149      %some_inj(List<&2, A>, row, r, e) : {List.length(&2, A, _) == w : Nat}
150      P.eq_sound(List.length(&2, A, row), w,
151        P.and_true_l(Nat.is_eq(List.length(&2, A, row), w), B.rows_wide(A, w, t), wide))
152    case row <> t 1n+k:
153      rows_wide_get(A, w, t, k, r,
154        P.and_true_r(Nat.is_eq(List.length(&2, A, row), w), B.rows_wide(A, w, t), wide), e)
155
156
157# Grids
158# =====
159
160def row_of(-A: Data, +g: T.Grid(A), +y: Nat) -> List<&2, A>:
161  Maybe.default(&2, List<&2, A>, List.get(&2, List<&2, A>, g, y), Nil{})
162
163law shaped_len:
164  for -A: Data
165  for +w: Nat
166  for +h: Nat
167  for +g: T.Grid(A)
168  for sh: {B.shaped(A, w, h, g) == True{} : Bool}
169  {List.length(&2, List<&2, A>, g) == h : Nat}
170
171def shaped_len(A, w, h, g, sh):
172  P.eq_sound(List.length(&2, List<&2, A>, g), h,
173    P.and_true_l(Nat.is_eq(List.length(&2, List<&2, A>, g), h), B.rows_wide(A, w, g), sh))
174
175law shaped_wide:
176  for -A: Data
177  for +w: Nat
178  for +h: Nat
179  for +g: T.Grid(A)
180  for sh: {B.shaped(A, w, h, g) == True{} : Bool}
181  {B.rows_wide(A, w, g) == True{} : Bool}
182
183def shaped_wide(A, w, h, g, sh):
184  P.and_true_r(Nat.is_eq(List.length(&2, List<&2, A>, g), h), B.rows_wide(A, w, g), sh)
185
186# In a w-by-h grid, the row at y < h is its row and has w cells.
187law row_in:
188  for -A: Data
189  for +w: Nat
190  for +h: Nat
191  for +g: T.Grid(A)
192  for +y: Nat
193  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
194  for yh: {Nat.is_lt(y, h) == True{} : Bool}
195  {List.get(&2, List<&2, A>, g, y) == Some{row_of(A, g, y)} : Maybe<&2, List<&2, A>>} &
196  {List.length(&2, A, row_of(A, g, y)) == w : Nat}
197
198def row_in(A, w, h, g, y, sh, yh):
199  +yl = {%Equal.sym(Nat, List.length(&2, List<&2, A>, g), h, shaped_len(A, w, h, g, sh)) :
200    {Nat.is_lt(y, _) == True{} : Bool};
201    yh : {Nat.is_lt(y, List.length(&2, List<&2, A>, g)) == True{} : Bool}}
202  +gi = get_in(List<&2, A>, g, y, Nil{}, yl)
203  (gi, rows_wide_get(A, w, g, y, row_of(A, g, y), shaped_wide(A, w, h, g, sh), gi))
204
205law at_set_eq:
206  for -A: Data
207  for +w: Nat
208  for +h: Nat
209  for +g: T.Grid(A)
210  for +x: Nat
211  for +y: Nat
212  for +v: A
213  for +d: A
214  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
215  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
216  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{x, y}) == v : A}
217
218law row_in_get:
219  for -A: Data
220  for +w: Nat
221  for +h: Nat
222  for +g: T.Grid(A)
223  for +y: Nat
224  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
225  for yh: {Nat.is_lt(y, h) == True{} : Bool}
226  {List.get(&2, List<&2, A>, g, y) == Some{row_of(A, g, y)} : Maybe<&2, List<&2, A>>}
227
228def row_in_get(A, w, h, g, y, sh, yh):
229  get_in(List<&2, A>, g, y, Nil{},
230    {%Equal.sym(Nat, List.length(&2, List<&2, A>, g), h, shaped_len(A, w, h, g, sh)) :
231      {Nat.is_lt(y, _) == True{} : Bool};
232      yh : {Nat.is_lt(y, List.length(&2, List<&2, A>, g)) == True{} : Bool}})
233
234law row_in_len:
235  for -A: Data
236  for +w: Nat
237  for +h: Nat
238  for +g: T.Grid(A)
239  for +y: Nat
240  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
241  for yh: {Nat.is_lt(y, h) == True{} : Bool}
242  {List.length(&2, A, row_of(A, g, y)) == w : Nat}
243
244def row_in_len(A, w, h, g, y, sh, yh):
245  rows_wide_get(A, w, g, y, row_of(A, g, y), shaped_wide(A, w, h, g, sh), row_in_get(A, w, h, g, y, sh, yh))
246
247def at_set_eq(A, w, h, g, x, y, v, d, sh, on):
248  +xw = P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
249  +yh = P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
250  ri = row_in(A, w, h, g, y, sh, yh)
251  +row = row_of(A, g, y)
252  +yl = {%Equal.sym(Nat, List.length(&2, List<&2, A>, g), h, shaped_len(A, w, h, g, sh)) :
253    {Nat.is_lt(y, _) == True{} : Bool};
254    yh : {Nat.is_lt(y, List.length(&2, List<&2, A>, g)) == True{} : Bool}}
255  +xl = {%Equal.sym(Nat, List.length(&2, A, row), w,
256      Pair.snd({List.get(&2, List<&2, A>, g, y) == Some{row} : Maybe<&2, List<&2, A>>},
257      {List.length(&2, A, row) == w : Nat}, ri)) : {Nat.is_lt(x, _) == True{} : Bool};
258    xw : {Nat.is_lt(x, List.length(&2, A, row)) == True{} : Bool}}
259  +r2 = List.set(&2, A, row, x, v)
260  %Equal.sym(Maybe<&2, List<&2, A>>, List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, r2), y),
261    Some{r2}, get_set_eq(List<&2, A>, g, y, r2, yl)) :
262    {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), x), d) == v : A}
263  %Equal.sym(Maybe<&2, A>, List.get(&2, A, r2, x), Some{v}, get_set_eq(A, row, x, v, xl)) :
264    {Maybe.default(&2, A, _, d) == v : A}
265  {==}
266
267def at_set_ne.row(-A: Data, +g: T.Grid(A), +x: Nat, +y: Nat, +qx: Nat, +v: A, +d: A,
268  xne: {Nat.is_eq(x, qx) == False{} : Bool}, +c: Bool,
269  ce: {Nat.is_lt(y, List.length(&2, List<&2, A>, g)) == c : Bool}) ->
270  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, y}) == B.at(A, d, g, T.Pos{qx, y}) : A}:
271  match c:
272    case True{}:
273      +row = row_of(A, g, y)
274      +r2 = List.set(&2, A, row, x, v)
275      %Equal.sym(Maybe<&2, List<&2, A>>, List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, r2), y),
276        Some{r2}, get_set_eq(List<&2, A>, g, y, r2, ce)) :
277        {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), qx), d)
278          == B.at(A, d, g, T.Pos{qx, y}) : A}
279      %Equal.sym(Maybe<&2, A>, List.get(&2, A, r2, qx), List.get(&2, A, row, qx),
280        get_set_ne(A, row, x, qx, v, xne)) :
281        {Maybe.default(&2, A, _, d) == B.at(A, d, g, T.Pos{qx, y}) : A}
282      {==}
283    case False{}:
284      +r2 = List.set(&2, A, row_of(A, g, y), x, v)
285      %Equal.sym(T.Grid(A), List.set(&2, List<&2, A>, g, y, r2), g, set_out(List<&2, A>, g, y, r2, ce)) :
286        {B.at(A, d, _, T.Pos{qx, y}) == B.at(A, d, g, T.Pos{qx, y}) : A}
287      {==}
288
289def at_set_ne.go(-A: Data, +g: T.Grid(A), +x: Nat, +y: Nat, +qx: Nat, +qy: Nat, +v: A, +d: A,
290  ne: {B.same(T.Pos{x, y}, T.Pos{qx, qy}) == False{} : Bool}, +b: Bool,
291  +be: {Nat.is_eq(y, qy) == b : Bool}) ->
292  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, qy}) == B.at(A, d, g, T.Pos{qx, qy}) : A}:
293  match b:
294    case False{}:
295      %Equal.sym(Maybe<&2, List<&2, A>>,
296        List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, List.set(&2, A, row_of(A, g, y), x, v)), qy),
297        List.get(&2, List<&2, A>, g, qy),
298        get_set_ne(List<&2, A>, g, y, qy, List.set(&2, A, row_of(A, g, y), x, v), be)) :
299        {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), qx), d)
300          == B.at(A, d, g, T.Pos{qx, qy}) : A}
301      {==}
302    case True{}:
303      +yq = P.eq_sound(y, qy, be)
304      %yq : {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, _}) == B.at(A, d, g, T.Pos{qx, _}) : A}
305      at_set_ne.row(A, g, x, y, qx, v, d,
306        {%P.and_true_r_id(Nat.is_eq(x, qx)) : {_ == False{} : Bool};
307          %be : {Bool.and(Nat.is_eq(x, qx), _) == False{} : Bool};
308          ne : {Nat.is_eq(x, qx) == False{} : Bool}},
309        Nat.is_lt(y, List.length(&2, List<&2, A>, g)), {==})
310
311# Setting p leaves every other cell as it was.
312law at_set_ne:
313  for -A: Data
314  for +g: T.Grid(A)
315  for +p: T.Pos
316  for +q: T.Pos
317  for +v: A
318  for +d: A
319  for ne: {B.same(p, q) == False{} : Bool}
320  {B.at(A, d, B.set_at(A, g, p, v), q) == B.at(A, d, g, q) : A}
321
322def at_set_ne(A, g, p, q, v, d, ne):
323  match p q:
324    case T.Pos{x, y} T.Pos{qx, qy}:
325      at_set_ne.go(A, g, x, y, qx, qy, v, d, ne, Nat.is_eq(y, qy), {==})
326
327law rows_wide_set:
328  for -A: Data
329  for +w: Nat
330  for +g: T.Grid(A)
331  for +y: Nat
332  for +x: Nat
333  for +v: A
334  for +wide: {B.rows_wide(A, w, g) == True{} : Bool}
335  {B.rows_wide(A, w, List.set(&2, List<&2, A>, g, y, List.set(&2, A, row_of(A, g, y), x, v))) == True{} : Bool}
336
337def rows_wide_set(A, w, g, y, x, v, wide):
338  match g y:
339    case Nil{} _:
340      {==}
341    case r <> t 0n:
342      %Equal.sym(Nat, List.length(&2, A, List.set(&2, A, r, x, v)), List.length(&2, A, r), set_len(A, r, x, v)) :
343        {Bool.and(Nat.is_eq(_, w), B.rows_wide(A, w, t)) == True{} : Bool}
344      wide
345    case r <> t 1n+k:
346      %Equal.sym(Bool, B.rows_wide(A, w, List.set(&2, List<&2, A>, t, k, List.set(&2, A, row_of(A, t, k), x, v))),
347        True{}, rows_wide_set(A, w, t, k, x, v,
348          P.and_true_r(Nat.is_eq(List.length(&2, A, r), w), B.rows_wide(A, w, t), wide))) :
349        {Bool.and(Nat.is_eq(List.length(&2, A, r), w), _) == True{} : Bool}
350      %Equal.sym(Bool, Bool.and(Nat.is_eq(List.length(&2, A, r), w), True{}), Nat.is_eq(List.length(&2, A, r), w),
351        P.and_true_r_id(Nat.is_eq(List.length(&2, A, r), w))) : {_ == True{} : Bool}
352      P.and_true_l(Nat.is_eq(List.length(&2, A, r), w), B.rows_wide(A, w, t), wide)
353
354law shaped_set:
355  for -A: Data
356  for +w: Nat
357  for +h: Nat
358  for +g: T.Grid(A)
359  for +p: T.Pos
360  for +v: A
361  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
362  {B.shaped(A, w, h, B.set_at(A, g, p, v)) == True{} : Bool}
363
364def shaped_set(A, w, h, g, p, v, sh):
365  match p:
366    case T.Pos{x, y}:
367      +r2 = List.set(&2, A, row_of(A, g, y), x, v)
368      %Equal.sym(Nat, List.length(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, r2)),
369        List.length(&2, List<&2, A>, g), set_len(List<&2, A>, g, y, r2)) :
370        {Bool.and(Nat.is_eq(_, h), B.rows_wide(A, w, List.set(&2, List<&2, A>, g, y, r2))) == True{} : Bool}
371      %Equal.sym(Bool, B.rows_wide(A, w, List.set(&2, List<&2, A>, g, y, r2)), True{},
372        rows_wide_set(A, w, g, y, x, v, shaped_wide(A, w, h, g, sh))) :
373        {Bool.and(Nat.is_eq(List.length(&2, List<&2, A>, g), h), _) == True{} : Bool}
374      %Equal.sym(Bool, Bool.and(Nat.is_eq(List.length(&2, List<&2, A>, g), h), True{}),
375        Nat.is_eq(List.length(&2, List<&2, A>, g), h),
376        P.and_true_r_id(Nat.is_eq(List.length(&2, List<&2, A>, g), h))) : {_ == True{} : Bool}
377      P.and_true_l(Nat.is_eq(List.length(&2, List<&2, A>, g), h), B.rows_wide(A, w, g), sh)
378
379# The blank grid
380# ==============
381
382law rep_len:
383  for -A: Data
384  for +n: Nat
385  for +v: A
386  {List.length(&2, A, List.replicate(A, n, v)) == n : Nat}
387
388def rep_len(A, n, v):
389  match n:
390    case 0n:
391      {==}
392    case 1n+k:
393      %Equal.sym(Nat, List.length(&2, A, List.replicate(A, k, v)), k, rep_len(A, k, v)) :
394        {1n+_ == 1n+k : Nat}
395      {==}
396
397law rep_wide:
398  for -A: Data
399  for +w: Nat
400  for +h: Nat
401  for +v: A
402  {B.rows_wide(A, w, List.replicate(List<&2, A>, h, List.replicate(A, w, v))) == True{} : Bool}
403
404def rep_wide(A, w, h, v):
405  match h:
406    case 0n:
407      {==}
408    case 1n+k:
409      %Equal.sym(Nat, List.length(&2, A, List.replicate(A, w, v)), w, rep_len(A, w, v)) :
410        {Bool.and(Nat.is_eq(_, w), B.rows_wide(A, w, List.replicate(List<&2, A>, k, List.replicate(A, w, v))))
411          == True{} : Bool}
412      %Equal.sym(Bool, Nat.is_eq(w, w), True{}, P.eq_refl(w)) :
413        {Bool.and(_, B.rows_wide(A, w, List.replicate(List<&2, A>, k, List.replicate(A, w, v)))) == True{} : Bool}
414      rep_wide(A, w, k, v)
415
416law blank_shaped:
417  for -A: Data
418  for +w: Nat
419  for +h: Nat
420  for +v: A
421  {B.shaped(A, w, h, B.blank(A, w, h, v)) == True{} : Bool}
422
423def blank_shaped(A, w, h, v):
424  %Equal.sym(Nat, List.length(&2, List<&2, A>, List.replicate(List<&2, A>, h, List.replicate(A, w, v))), h,
425    rep_len(List<&2, A>, h, List.replicate(A, w, v))) :
426    {Bool.and(Nat.is_eq(_, h), B.rows_wide(A, w, B.blank(A, w, h, v))) == True{} : Bool}
427  %Equal.sym(Bool, Nat.is_eq(h, h), True{}, P.eq_refl(h)) :
428    {Bool.and(_, B.rows_wide(A, w, B.blank(A, w, h, v))) == True{} : Bool}
429  rep_wide(A, w, h, v)
430
431law rep_default:
432  for -A: Data
433  for +n: Nat
434  for +v: A
435  for +i: Nat
436  {Maybe.default(&2, A, List.get(&2, A, List.replicate(A, n, v), i), v) == v : A}
437
438def rep_default(A, n, v, i):
439  match n i:
440    case 0n _:
441      {==}
442    case 1n+k 0n:
443      {==}
444    case 1n+k 1n+j:
445      rep_default(A, k, v, j)
446
447law blank_at:
448  for +w: Nat
449  for +h: Nat
450  for +x: Nat
451  for +y: Nat
452  {B.at(Bool, False{}, B.blank(Bool, w, h, False{}), T.Pos{x, y}) == False{} : Bool}
453
454def blank_at(w, h, x, y):
455  match h y:
456    case 0n _:
457      {==}
458    case 1n+k 0n:
459      rep_default(Bool, w, False{}, x)
460    case 1n+k 1n+j:
461      blank_at(w, k, x, j)
462
463# Counting unrevealed cells
464# =========================
465
466law row_false_set:
467  for +r: List<&2, Bool>
468  for +x: Nat
469  for e: {List.get(&2, Bool, r, x) == Some{False{}} : Maybe<&2, Bool>}
470  {B.row_false(r) == 1n+B.row_false(List.set(&2, Bool, r, x, True{})) : Nat}
471
472def row_false_set(r, x, e):
473  match r x:
474    case Nil{} _:
475      Empty.absurd({0n == 1n+0n : Nat}, none_ne_some(Bool, False{}, e))
476    case b <> t 0n:
477      %Equal.sym(Bool, b, False{}, some_inj(Bool, b, False{}, e)) :
478        {Nat.add(Bool.pick(Nat, _, 0n, 1n), B.row_false(t)) == 1n+Nat.add(0n, B.row_false(t)) : Nat}
479      {==}
480    case b <> t 1n+k:
481      %Equal.sym(Nat, B.row_false(t), 1n+B.row_false(List.set(&2, Bool, t, k, True{})), row_false_set(t, k, e)) :
482        {Nat.add(Bool.pick(Nat, b, 0n, 1n), _)
483          == 1n+Nat.add(Bool.pick(Nat, b, 0n, 1n), B.row_false(List.set(&2, Bool, t, k, True{}))) : Nat}
484      P.add_succ(Bool.pick(Nat, b, 0n, 1n), B.row_false(List.set(&2, Bool, t, k, True{})))
485
486law count_false_set.go:
487  for +g: T.Grid(Bool)
488  for +y: Nat
489  for +r: List<&2, Bool>
490  for +r2: List<&2, Bool>
491  for e: {List.get(&2, List<&2, Bool>, g, y) == Some{r} : Maybe<&2, List<&2, Bool>>}
492  for rf: {B.row_false(r) == 1n+B.row_false(r2) : Nat}
493  {B.count_false(g) == 1n+B.count_false(List.set(&2, List<&2, Bool>, g, y, r2)) : Nat}
494
495def count_false_set.go(g, y, r, r2, e, rf):
496  match g y:
497    case Nil{} _:
498      Empty.absurd({0n == 1n+0n : Nat}, none_ne_some(List<&2, Bool>, r, e))
499    case row <> t 0n:
500      %Equal.sym(List<&2, Bool>, row, r, some_inj(List<&2, Bool>, row, r, e)) :
501        {Nat.add(B.row_false(_), B.count_false(t)) == 1n+Nat.add(B.row_false(r2), B.count_false(t)) : Nat}
502      %Equal.sym(Nat, B.row_false(r), 1n+B.row_false(r2), rf) :
503        {Nat.add(_, B.count_false(t)) == 1n+Nat.add(B.row_false(r2), B.count_false(t)) : Nat}
504      {==}
505    case row <> t 1n+k:
506      %Equal.sym(Nat, B.count_false(t), 1n+B.count_false(List.set(&2, List<&2, Bool>, t, k, r2)),
507        count_false_set.go(t, k, r, r2, e, rf)) :
508        {Nat.add(B.row_false(row), _)
509          == 1n+Nat.add(B.row_false(row), B.count_false(List.set(&2, List<&2, Bool>, t, k, r2))) : Nat}
510      P.add_succ(B.row_false(row), B.count_false(List.set(&2, List<&2, Bool>, t, k, r2)))
511
512# Revealing an unrevealed cell of the board uses up one count.
513law count_false_set:
514  for +w: Nat
515  for +h: Nat
516  for +g: T.Grid(Bool)
517  for +x: Nat
518  for +y: Nat
519  for +sh: {B.shaped(Bool, w, h, g) == True{} : Bool}
520  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
521  for hid: {B.at(Bool, False{}, g, T.Pos{x, y}) == False{} : Bool}
522  {B.count_false(g) == 1n+B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})) : Nat}
523
524def count_false_set(w, h, g, x, y, sh, on, hid):
525  +xw = P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
526  +yh = P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
527  +row = row_of(Bool, g, y)
528  +xl = {%Equal.sym(Nat, List.length(&2, Bool, row), w, row_in_len(Bool, w, h, g, y, sh, yh)) :
529    {Nat.is_lt(x, _) == True{} : Bool};
530    xw : {Nat.is_lt(x, List.length(&2, Bool, row)) == True{} : Bool}}
531  +cell = {%hid : {List.get(&2, Bool, row, x) == Some{_} : Maybe<&2, Bool>};
532    get_in(Bool, row, x, False{}, xl) : {List.get(&2, Bool, row, x) == Some{False{}} : Maybe<&2, Bool>}}
533  count_false_set.go(g, y, row, List.set(&2, Bool, row, x, True{}), row_in_get(Bool, w, h, g, y, sh, yh),
534    row_false_set(row, x, cell))
535
536# A grid with no unrevealed cell has every cell of the board revealed.
537law count_false_zero:
538  for +w: Nat
539  for +h: Nat
540  for +g: T.Grid(Bool)
541  for +x: Nat
542  for +y: Nat
543  for +sh: {B.shaped(Bool, w, h, g) == True{} : Bool}
544  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
545  for z: {B.count_false(g) == 0n : Nat}
546  {B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool}
547
548def count_false_zero.go(+w: Nat, +h: Nat, +g: T.Grid(Bool), +x: Nat, +y: Nat,
549  +sh: {B.shaped(Bool, w, h, g) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
550  z: {B.count_false(g) == 0n : Nat}, +b: Bool, e: {B.at(Bool, False{}, g, T.Pos{x, y}) == b : Bool}) ->
551  {B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool}:
552  match b:
553    case True{}:
554      e
555    case False{}:
556      Empty.absurd({B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool},
557        P.succ_ne_zero(B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})),
558          Equal.trans(Nat, 1n+B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})), B.count_false(g), 0n,
559            Equal.sym(Nat, B.count_false(g), 1n+B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})),
560              count_false_set(w, h, g, x, y, sh, on, e)), z)))
561
562def count_false_zero(w, h, g, x, y, sh, on, z):
563  count_false_zero.go(w, h, g, x, y, sh, on, z, B.at(Bool, False{}, g, T.Pos{x, y}), {==})