proof_gen.bend

minebender-game@1.0.0.0 · 1,231 lines · 83 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
8
9# Lemmas about board generation.
10
11# Shape
12# =====
13
14law gen_row_len:
15  for +z: G.Zone
16  for +y: Nat
17  for +xs: List<&2, Nat>
18  for +st: G.GenState
19  {List.length(&2, Bool, G.gen.row(z, y, xs, st)) == List.length(&2, Nat, xs) : Nat}
20
21def gen_row_len(z, y, xs, st):
22  match xs:
23    case Nil{}:
24      {==}
25    case x <> t:
26      %gen_row_len(z, y, t, G.gen.next(z, T.Pos{x, y}, st)) :
27        {1n+List.length(&2, Bool, G.gen.row(z, y, t, G.gen.next(z, T.Pos{x, y}, st)))
28          == 1n+_ : Nat}
29      {==}
30
31law gen_rows_len:
32  for +z: G.Zone
33  for +w: Nat
34  for +ys: List<&2, Nat>
35  for +st: G.GenState
36  {List.length(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st)) == List.length(&2, Nat, ys) : Nat}
37
38def gen_rows_len(z, w, ys, st):
39  match ys:
40    case Nil{}:
41      {==}
42    case y <> t:
43      +st2 = G.gen.row_state(z, y, List.range(w), st)
44      %gen_rows_len(z, w, t, st2) :
45        {1n+List.length(&2, List<&2, Bool>, G.gen.rows(z, w, t, st2)) == 1n+_ : Nat}
46      {==}
47
48law gen_rows_wide:
49  for +z: G.Zone
50  for +w: Nat
51  for +ys: List<&2, Nat>
52  for +st: G.GenState
53  {L.rows_wide(Bool, w, G.gen.rows(z, w, ys, st)) == True{} : Bool}
54
55def gen_rows_wide(z, w, ys, st):
56  match ys:
57    case Nil{}:
58      {==}
59    case y <> t:
60      +row = G.gen.row(z, y, List.range(w), st)
61      +st2 = G.gen.row_state(z, y, List.range(w), st)
62      +len = Equal.trans(Nat, List.length(&2, Bool, row), List.length(&2, Nat, List.range(w)), w,
63        gen_row_len(z, y, List.range(w), st), P.range_length(w))
64      %Equal.sym(Nat, List.length(&2, Bool, row), w, len) :
65        {Bool.and(Nat.is_eq(_, w), L.rows_wide(Bool, w, G.gen.rows(z, w, t, st2))) == True{} : Bool}
66      %Equal.sym(Bool, Nat.is_eq(w, w), True{}, P.eq_refl(w)) :
67        {Bool.and(_, L.rows_wide(Bool, w, G.gen.rows(z, w, t, st2))) == True{} : Bool}
68      gen_rows_wide(z, w, t, st2)
69
70# The zone a board of n mines keeps free around the first click.
71def zone(+w: Nat, +h: Nat, +n: Nat, +first: T.Pos) -> G.Zone:
72  G.Zone{first, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h))}
73
74law gen_shape_:
75  for +w: Nat
76  for +h: Nat
77  for +n: Nat
78  for +first: T.Pos
79  for +rs: List<&2, U32>
80  {L.shaped(Bool, w, h, G.place_mines(w, h, n, first, rs)) == True{} : Bool}
81
82def gen_shape_(w, h, n, first, rs):
83  +z = zone(w, h, n, first)
84  +st = {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState}
85  +g = G.gen.rows(z, w, List.range(h), st)
86  +len = Equal.trans(Nat, List.length(&2, List<&2, Bool>, g), List.length(&2, Nat, List.range(h)), h,
87    gen_rows_len(z, w, List.range(h), st), P.range_length(h))
88  %Equal.sym(Nat, List.length(&2, List<&2, Bool>, g), h, len) :
89    {Bool.and(Nat.is_eq(_, h), L.rows_wide(Bool, w, g)) == True{} : Bool}
90  %Equal.sym(Bool, Nat.is_eq(h, h), True{}, P.eq_refl(h)) :
91    {Bool.and(_, L.rows_wide(Bool, w, g)) == True{} : Bool}
92  gen_rows_wide(z, w, List.range(h), st)
93
94# The first click
95# ===============
96
97def gen_bit_first(+z: G.Zone, +p: T.Pos, +st: G.GenState,
98  s: {G.gen.out(z, p) == True{} : Bool}) -> {G.gen.bit(z, p, st) == False{} : Bool}:
99  match st:
100    case G.GenState{need, left, rs}:
101      %Equal.sym(Bool, G.gen.out(z, p), True{}, s) :
102        {Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))
103          == False{} : Bool}
104      {==}
105
106# A cell of a generated row that is in the zone has no mine.
107law gen_row_first:
108  for +z: G.Zone
109  for +y: Nat
110  for +xs: List<&2, Nat>
111  for +j: Nat
112  for +x: Nat
113  for +st: G.GenState
114  for e: {List.get(&2, Nat, xs, j) == Some{x} : Maybe<&2, Nat>}
115  for +s: {G.gen.out(z, T.Pos{x, y}) == True{} : Bool}
116  {List.get(&2, Bool, G.gen.row(z, y, xs, st), j) == Some{False{}} : Maybe<&2, Bool>}
117
118def gen_row_first(z, y, xs, j, x, st, e, s):
119  match xs j:
120    case Nil{} _:
121      Empty.absurd({List.get(&2, Bool, G.gen.row(z, y, Nil{}, st), j) == Some{False{}}
122        : Maybe<&2, Bool>}, PG.know_row_get.none(Nat, x, e))
123    case a <> t 0n:
124      %Equal.sym(Nat, a, x, PG.know_row_get.some(Nat, a, x, e)) :
125        {Some{G.gen.bit(z, T.Pos{_, y}, st)} == Some{False{}} : Maybe<&2, Bool>}
126      %Equal.sym(Bool, G.gen.bit(z, T.Pos{x, y}, st), False{},
127        gen_bit_first(z, T.Pos{x, y}, st, s)) :
128        {Some{_} == Some{False{}} : Maybe<&2, Bool>}
129      {==}
130    case a <> t 1n+k:
131      gen_row_first(z, y, t, k, x, G.gen.next(z, T.Pos{a, y}, st), e, s)
132
133def Maybe.disc_some(-A: Data, m: Maybe<&2, A>) -> Type:
134  match m:
135    case None{}:
136      Empty
137    case Some{v}:
138      Unit
139
140def gen_some_ne_none(-A: Data, -a: A, e: {Some{a} == None{} : Maybe<&2, A>}) -> Empty:
141  %e : Maybe.disc_some(A, _)
142  Unit{}
143
144law gen_row_out:
145  for +z: G.Zone
146  for +y: Nat
147  for +xs: List<&2, Nat>
148  for +j: Nat
149  for +st: G.GenState
150  for e: {List.get(&2, Nat, xs, j) == None{} : Maybe<&2, Nat>}
151  {List.get(&2, Bool, G.gen.row(z, y, xs, st), j) == None{} : Maybe<&2, Bool>}
152
153def gen_row_out(z, y, xs, j, st, e):
154  match xs j:
155    case Nil{} _:
156      {==}
157    case a <> t 0n:
158      Empty.absurd({List.get(&2, Bool, G.gen.row(z, y, a <> t, st), 0n) == None{}
159        : Maybe<&2, Bool>}, gen_some_ne_none(Nat, a, e))
160    case a <> t 1n+k:
161      gen_row_out(z, y, t, k, G.gen.next(z, T.Pos{a, y}, st), e)
162
163law gen_rows_get:
164  for +z: G.Zone
165  for +w: Nat
166  for +ys: List<&2, Nat>
167  for +i: Nat
168  for +y: Nat
169  for +st: G.GenState
170  for e: {List.get(&2, Nat, ys, i) == Some{y} : Maybe<&2, Nat>}
171  exs st2: G.GenState
172  {List.get(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st), i)
173    == Some{G.gen.row(z, y, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>}
174
175def gen_rows_get(z, w, ys, i, y, st, e):
176  match ys i:
177    case Nil{} _:
178      Empty.absurd(Exists(G.GenState, st2 => {List.get(&2, List<&2, Bool>,
179        G.gen.rows(z, w, Nil{}, st), i) == Some{G.gen.row(z, y, List.range(w), st2)}
180        : Maybe<&2, List<&2, Bool>>}), PG.know_row_get.none(Nat, y, e))
181    case a <> t 0n:
182      %PG.know_row_get.some(Nat, a, y, e) :
183        Exists(G.GenState, st2 => {Some{G.gen.row(z, a, List.range(w), st)}
184          == Some{G.gen.row(z, _, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>})
185      (st, {==})
186    case a <> t 1n+k:
187      gen_rows_get(z, w, t, k, y, G.gen.row_state(z, a, List.range(w), st), e)
188
189law gen_rows_out:
190  for +z: G.Zone
191  for +w: Nat
192  for +ys: List<&2, Nat>
193  for +i: Nat
194  for +st: G.GenState
195  for e: {List.get(&2, Nat, ys, i) == None{} : Maybe<&2, Nat>}
196  {List.get(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st), i) == None{}
197    : Maybe<&2, List<&2, Bool>>}
198
199def gen_rows_out(z, w, ys, i, st, e):
200  match ys i:
201    case Nil{} _:
202      {==}
203    case a <> t 0n:
204      Empty.absurd({List.get(&2, List<&2, Bool>, G.gen.rows(z, w, a <> t, st), 0n) == None{}
205        : Maybe<&2, List<&2, Bool>>}, gen_some_ne_none(Nat, a, e))
206    case a <> t 1n+k:
207      gen_rows_out(z, w, t, k, G.gen.row_state(z, a, List.range(w), st), e)
208
209def gen_first.col(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +st2: G.GenState,
210  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool}, +b: Bool,
211  e: {Nat.is_lt(fx, w) == b : Bool}) ->
212  {Maybe.default(&2, Bool, List.get(&2, Bool, G.gen.row(z, fy, List.range(w), st2), fx), False{})
213    == False{} : Bool}:
214  match b:
215    case True{}:
216      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, G.gen.row(z, fy, List.range(w), st2), fx),
217        Some{False{}},
218        gen_row_first(z, fy, List.range(w), fx, fx, st2, P.range_get(w, fx, e), s)) :
219        {Maybe.default(&2, Bool, _, False{}) == False{} : Bool}
220      {==}
221    case False{}:
222      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, G.gen.row(z, fy, List.range(w), st2), fx),
223        None{}, gen_row_out(z, fy, List.range(w), fx, st2, P.range_get_out(w, fx, e))) :
224        {Maybe.default(&2, Bool, _, False{}) == False{} : Bool}
225      {==}
226
227def gen_first.found(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +g: T.Grid(Bool),
228  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool},
229  r: Exists(G.GenState, st2 => {List.get(&2, List<&2, Bool>, g, fy)
230    == Some{G.gen.row(z, fy, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>})) ->
231  {L.mine(g, T.Pos{fx, fy}) == False{} : Bool}:
232  match r:
233    case (st2, eq):
234      %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, g, fy),
235        Some{G.gen.row(z, fy, List.range(w), st2)}, eq) :
236        {Maybe.default(&2, Bool, List.get(&2, Bool,
237          Maybe.default(&2, List<&2, Bool>, _, Nil{}), fx), False{}) == False{} : Bool}
238      gen_first.col(z, fx, fy, w, st2, s, Nat.is_lt(fx, w), {==})
239
240def gen_first.row(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +h: Nat, +st: G.GenState,
241  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool}, +b: Bool,
242  e: {Nat.is_lt(fy, h) == b : Bool}) ->
243  {L.mine(G.gen.rows(z, w, List.range(h), st), T.Pos{fx, fy}) == False{} : Bool}:
244  match b:
245    case True{}:
246      gen_first.found(z, fx, fy, w, G.gen.rows(z, w, List.range(h), st), s,
247        gen_rows_get(z, w, List.range(h), fy, fy, st, P.range_get(h, fy, e)))
248    case False{}:
249      %Equal.sym(Maybe<&2, List<&2, Bool>>,
250        List.get(&2, List<&2, Bool>, G.gen.rows(z, w, List.range(h), st), fy), None{},
251        gen_rows_out(z, w, List.range(h), fy, st, P.range_get_out(h, fy, e))) :
252        {Maybe.default(&2, Bool, List.get(&2, Bool,
253          Maybe.default(&2, List<&2, Bool>, _, Nil{}), fx), False{}) == False{} : Bool}
254      {==}
255
256law sub_self:
257  for +a: Nat
258  {Nat.sub(a, a) == 0n : Nat}
259
260def sub_self(a):
261  match a:
262    case 0n:
263      {==}
264    case 1n+k:
265      sub_self(k)
266
267# A cell is within one step of itself.
268law within_self:
269  for +p: T.Pos
270  {B.within_one(p, p) == True{} : Bool}
271
272def within_self(p):
273  match p:
274    case T.Pos{x, y}:
275      %Equal.sym(Nat, Nat.sub(x, x), 0n, sub_self(x)) :
276        {Bool.and(Nat.is_le(Nat.add(_, _), 1n), Nat.is_le(Nat.add(Nat.sub(y, y), Nat.sub(y, y)), 1n)) == True{} : Bool}
277      %Equal.sym(Nat, Nat.sub(y, y), 0n, sub_self(y)) :
278        {Bool.and(Nat.is_le(Nat.add(0n, 0n), 1n), Nat.is_le(Nat.add(_, _), 1n)) == True{} : Bool}
279      {==}
280
281# The first click is always in its own zone.
282law out_first:
283  for +first: T.Pos
284  for +wide: Bool
285  {G.gen.out(G.Zone{first, wide}, first) == True{} : Bool}
286
287def out_first(first, wide):
288  match wide:
289    case True{}:
290      within_self(first)
291    case False{}:
292      PG.same_refl(first)
293
294law gen_first_safe_:
295  for +w: Nat
296  for +h: Nat
297  for +n: Nat
298  for +first: T.Pos
299  for +rs: List<&2, U32>
300  {L.mine(G.place_mines(w, h, n, first, rs), first) == False{} : Bool}
301
302def gen_first_safe_(w, h, n, first, rs):
303  match first:
304    case T.Pos{fx, fy}:
305      +p = {T.Pos{fx, fy} : T.Pos}
306      +z = zone(w, h, n, p)
307      gen_first.row(z, fx, fy, w, h,
308        {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState},
309        out_first(p, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h))), Nat.is_lt(fy, h), {==})
310
311law within_eq:
312  for +p: T.Pos
313  for +q: T.Pos
314  {B.within_one(p, q) == L.within_one(p, q) : Bool}
315
316def within_eq(p, q):
317  match p q:
318    case T.Pos{px, py} T.Pos{qx, qy}:
319      {==}
320
321# A wide zone holds every cell next to the first click.
322def opening_in(+first: T.Pos, +p: T.Pos, +wide: Bool, ew: {wide == True{} : Bool},
323  near: {L.within_one(first, p) == True{} : Bool}) -> {G.gen.out(G.Zone{first, wide}, p) == True{} : Bool}:
324  %Equal.sym(Bool, wide, True{}, ew) : {G.gen.out(G.Zone{first, _}, p) == True{} : Bool}
325  Equal.trans(Bool, B.within_one(first, p), L.within_one(first, p), True{}, within_eq(first, p), near)
326
327# With room, no cell next to the first click gets a mine.
328law gen_opening_:
329  for +w: Nat
330  for +h: Nat
331  for +n: Nat
332  for +first: T.Pos
333  for +rs: List<&2, U32>
334  for +room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
335  for +q: T.Pos
336  for +near: {L.within_one(first, q) == True{} : Bool}
337  {L.mine(G.place_mines(w, h, n, first, rs), q) == False{} : Bool}
338
339def gen_opening_(w, h, n, first, rs, room, q, near):
340  match q:
341    case T.Pos{qx, qy}:
342      +p = {T.Pos{qx, qy} : T.Pos}
343      +z = zone(w, h, n, first)
344      gen_first.row(z, qx, qy, w, h,
345        {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState},
346        opening_in(first, p, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)), room, near), Nat.is_lt(qy, h), {==})
347
348# Exactly n mines
349# ===============
350
351def st_need(st: G.GenState) -> Nat:
352  match st:
353    case G.GenState{need, left, rs}:
354      need
355
356def st_left(st: G.GenState) -> Nat:
357  match st:
358    case G.GenState{need, left, rs}:
359      left
360
361def one(b: Bool) -> Nat:
362  Bool.pick(Nat, b, 1n, 0n)
363
364# What one cell does to the state: the mines placed plus the mines still
365# needed stay the same, need <= left stays true, and left counts down for
366# every cell outside the zone.
367def GenStep(+z: G.Zone, +p: T.Pos, +st: G.GenState, +lp: Nat) -> Type:
368  {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat} &
369  {Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} &
370  {st_left(G.gen.next(z, p, st)) == lp : Nat}
371
372def gen_pick_false(+need: Nat, +left: Nat, +rs: List<&2, U32>,
373  e: {G.gen.pick(need, left, rs) == False{} : Bool}) -> {Nat.is_eq(need, left) == False{} : Bool}:
374  match rs:
375    case Nil{}:
376      e
377    case r <> t:
378      P.or_false_inv(Nat.is_eq(need, left), G.gen.coin(r, left, need), e)
379
380def gen_take(+z: G.Zone, +p: T.Pos, +m: Nat, +lp: Nat, +rs: List<&2, U32>,
381  inv: {Nat.is_le(1n+m, 1n+lp) == True{} : Bool}, +c: Bool,
382  ce: {G.gen.pick(1n+m, 1n+lp, rs) == c : Bool}) ->
383  {Nat.add(one(c), Nat.sub(1n+m, one(c))) == 1n+m : Nat} &
384  {Nat.is_le(Nat.sub(1n+m, one(c)), Nat.sub(1n+lp, 1n)) == True{} : Bool} &
385  {Nat.sub(1n+lp, 1n) == lp : Nat}:
386  match c:
387    case True{}:
388      %Equal.sym(Nat, Nat.sub(m, 0n), m, P.sub_zero(m)) :
389        {1n+_ == 1n+m : Nat} & {Nat.is_le(_, Nat.sub(lp, 0n)) == True{} : Bool} &
390        {Nat.sub(lp, 0n) == lp : Nat}
391      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
392        {1n+m == 1n+m : Nat} & {Nat.is_le(m, _) == True{} : Bool} & {_ == lp : Nat}
393      ({==}, (inv, {==}))
394    case False{}:
395      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
396        {1n+m == 1n+m : Nat} & {Nat.is_le(1n+m, _) == True{} : Bool} & {_ == lp : Nat}
397      ({==}, (P.le_ne(m, lp, inv, gen_pick_false(1n+m, 1n+lp, rs, ce)), {==}))
398
399def gen_cell.need(+z: G.Zone, +p: T.Pos, +need: Nat, +lp: Nat, +rs: List<&2, U32>,
400  inv: {Nat.is_le(need, 1n+lp) == True{} : Bool}) ->
401  {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))),
402     Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))))) == need : Nat} &
403  {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs)))),
404     Nat.sub(1n+lp, 1n)) == True{} : Bool} &
405  {Nat.sub(1n+lp, 1n) == lp : Nat}:
406  match need:
407    case 0n:
408      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
409        {0n == 0n : Nat} & {Nat.is_le(0n, _) == True{} : Bool} & {_ == lp : Nat}
410      ({==}, (P.le_zero_l(lp), {==}))
411    case 1n+m:
412      gen_take(z, p, m, lp, rs, inv, G.gen.pick(1n+m, 1n+lp, rs), {==})
413
414def gen_cell.go(+z: G.Zone, +p: T.Pos, +need: Nat, +left: Nat, +rs: List<&2, U32>, +lp: Nat,
415  inv: {Nat.is_le(need, left) == True{} : Bool}, +s: Bool, e: {G.gen.out(z, p) == s : Bool},
416  +lft: {left == Nat.add(Bool.pick(Nat, s, 0n, 1n), lp) : Nat}) ->
417  GenStep(z, p, G.GenState{need, left, rs}, lp):
418  match s:
419    case True{}:
420      %Equal.sym(Bool, G.gen.out(z, p), True{}, e) :
421        {Nat.add(one(Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))),
422          st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
423            G.gen.pick(need, left, rs)), need, left, rs))) == need : Nat} &
424        {Nat.is_le(st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
425            G.gen.pick(need, left, rs)), need, left, rs)),
426          st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
427            G.gen.pick(need, left, rs)), need, left, rs))) == True{} : Bool} &
428        {st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
429            G.gen.pick(need, left, rs)), need, left, rs)) == lp : Nat}
430      ({==}, (inv, lft))
431    case False{}:
432      %Equal.sym(Bool, G.gen.out(z, p), False{}, e) :
433        {Nat.add(one(Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)), G.gen.pick(need, left, rs))),
434          st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
435            G.gen.pick(need, left, rs)), need, left, rs))) == need : Nat} &
436        {Nat.is_le(st_need(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
437            G.gen.pick(need, left, rs)), need, left, rs)),
438          st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
439            G.gen.pick(need, left, rs)), need, left, rs))) == True{} : Bool} &
440        {st_left(G.gen.next.go(_, Bool.and(Bool.and(Bool.not(_), Nat.is_lt(0n, need)),
441            G.gen.pick(need, left, rs)), need, left, rs)) == lp : Nat}
442      %Equal.sym(Nat, left, 1n+lp, lft) :
443        {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs))),
444          Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs))))) == need : Nat} &
445        {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, _, rs)))),
446          Nat.sub(_, 1n)) == True{} : Bool} &
447        {Nat.sub(_, 1n) == lp : Nat}
448      gen_cell.need(z, p, need, lp, rs,
449        {%lft : {Nat.is_le(need, _) == True{} : Bool}; inv : {Nat.is_le(need, 1n+lp) == True{} : Bool}})
450
451
452law gen_cell:
453  for +z: G.Zone
454  for +p: T.Pos
455  for +st: G.GenState
456  for +lp: Nat
457  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
458  for lft: {st_left(st) == Nat.add(Bool.pick(Nat, G.gen.out(z, p), 0n, 1n), lp) : Nat}
459  GenStep(z, p, st, lp)
460
461def gen_cell(z, p, st, lp, inv, lft):
462  match st:
463    case G.GenState{need, left, rs}:
464      gen_cell.go(z, p, need, left, rs, lp, inv, G.gen.out(z, p), {==}, lft)
465
466def gen_row_count.step(+z: G.Zone, +p: T.Pos, +st: G.GenState, +rm: Nat, +nf: Nat,
467  s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
468  r1: {Nat.add(rm, nf) == st_need(G.gen.next(z, p, st)) : Nat}) ->
469  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf) == st_need(st) : Nat}:
470  %Equal.sym(Nat, Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf),
471    Nat.add(one(G.gen.bit(z, p, st)), Nat.add(rm, nf)),
472    P.add_assoc(one(G.gen.bit(z, p, st)), rm, nf)) : {_ == st_need(st) : Nat}
473  %Equal.sym(Nat, Nat.add(rm, nf), st_need(G.gen.next(z, p, st)), r1) :
474    {Nat.add(one(G.gen.bit(z, p, st)), _) == st_need(st) : Nat}
475  s1
476
477def gen_row_count.k2(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
478  +cs: List<&2, T.Pos>,
479  s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
480  r: {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
481       st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
482    {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
483       st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
484    {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}) ->
485  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st)))),
486     st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
487  {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
488     st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
489  {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
490  match r:
491    case (r1, rest):
492      (gen_row_count.step(z, p, st,
493        L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
494        st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))), s1, r1), rest)
495
496def gen_row_count.k(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
497  +cs: List<&2, T.Pos>,
498  step: GenStep(z, p, st, G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs))),
499  ih: ({Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} ->
500    {st_left(G.gen.next(z, p, st)) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs)) : Nat} ->
501    {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
502       st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
503    {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
504       st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
505    {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat})) ->
506  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st)))),
507     st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
508  {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
509     st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
510  {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
511  match step:
512    case (s1, rest):
513      match rest:
514        case (s2, s3):
515          gen_row_count.k2(z, y, t, p, st, cs, s1, ih(s2, s3))
516
517
518law gen_row_count:
519  for +z: G.Zone
520  for +y: Nat
521  for +xs: List<&2, Nat>
522  for +st: G.GenState
523  for +cs: List<&2, T.Pos>
524  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
525  for lft: {st_left(st) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, xs), cs)) : Nat}
526  {Nat.add(L.row_mines(G.gen.row(z, y, xs, st)), st_need(G.gen.row_state(z, y, xs, st)))
527    == st_need(st) : Nat} &
528  {Nat.is_le(st_need(G.gen.row_state(z, y, xs, st)), st_left(G.gen.row_state(z, y, xs, st)))
529    == True{} : Bool} &
530  {st_left(G.gen.row_state(z, y, xs, st)) == G.gen.left(z, cs) : Nat}
531
532def gen_row_count(z, y, xs, st, cs, inv, lft):
533  match xs:
534    case Nil{}:
535      ({==}, (inv, lft))
536    case x <> t:
537      +p = {T.Pos{x, y} : T.Pos}
538      +lp = G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs))
539      +nx = G.gen.next(z, p, st)
540      gen_row_count.k(z, y, t, p, st, cs, gen_cell(z, p, st, lp, inv, lft),
541        s => gen_row_count(z, y, t, nx, cs, s))
542
543
544def gen_rows_count.k(+z: G.Zone, +w: Nat, +y: Nat, +t: List<&2, Nat>, +st: G.GenState,
545  r: {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
546       st_need(G.gen.row_state(z, y, List.range(w), st))) == st_need(st) : Nat} &
547    {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
548       st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} &
549    {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat},
550  ih: {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
551       st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} ->
552    {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat} ->
553    {L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st)))
554      == st_need(G.gen.row_state(z, y, List.range(w), st)) : Nat}) ->
555  {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
556     L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))))
557    == st_need(st) : Nat}:
558  match r:
559    case (r1, rest):
560      match rest:
561        case (r2, r3):
562          %Equal.sym(Nat, L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))),
563            st_need(G.gen.row_state(z, y, List.range(w), st)), ih(r2, r3)) :
564            {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)), _) == st_need(st) : Nat}
565          r1
566
567law gen_rows_count:
568  for +z: G.Zone
569  for +w: Nat
570  for +ys: List<&2, Nat>
571  for +st: G.GenState
572  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
573  for lft: {st_left(st) == G.gen.left(z, B.cells.go(w, ys)) : Nat}
574  {L.total_mines(G.gen.rows(z, w, ys, st)) == st_need(st) : Nat}
575
576def gen_rows_count(z, w, ys, st, inv, lft):
577  match ys:
578    case Nil{}:
579      Equal.sym(Nat, st_need(st), 0n, P.le_zero(st_need(st),
580        {%lft : {Nat.is_le(st_need(st), _) == True{} : Bool};
581          inv : {Nat.is_le(st_need(st), 0n) == True{} : Bool}}))
582    case y <> t:
583      +rs2 = G.gen.row_state(z, y, List.range(w), st)
584      gen_rows_count.k(z, w, y, t, st,
585        gen_row_count(z, y, List.range(w), st, B.cells.go(w, t), inv, lft),
586        a => b => gen_rows_count(z, w, t, rs2, a, b))
587
588# Counting the candidates
589# =======================
590
591# How many cells of ps are in the zone.
592def outs(+z: G.Zone, ps: List<&2, T.Pos>) -> Nat:
593  match ps:
594    case Nil{}:
595      0n
596    case p <> t:
597      Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t))
598
599def gen_left_firsts.go(+z: G.Zone, +p: T.Pos, +t: List<&2, T.Pos>, +s: Bool,
600  ih: {Nat.add(G.gen.left(z, t), outs(z, t)) == List.length(&2, T.Pos, t) : Nat}) ->
601  {Nat.add(Nat.add(Bool.pick(Nat, s, 0n, 1n), G.gen.left(z, t)),
602     Nat.add(Bool.pick(Nat, s, 1n, 0n), outs(z, t))) == 1n+List.length(&2, T.Pos, t) : Nat}:
603  match s:
604    case True{}:
605      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), 1n+outs(z, t)),
606        1n+Nat.add(G.gen.left(z, t), outs(z, t)),
607        P.add_succ(G.gen.left(z, t), outs(z, t))) :
608        {_ == 1n+List.length(&2, T.Pos, t) : Nat}
609      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
610        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
611      {==}
612    case False{}:
613      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
614        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
615      {==}
616
617# Every cell is either a candidate or in the zone.
618law gen_left_firsts:
619  for +z: G.Zone
620  for +ps: List<&2, T.Pos>
621  {Nat.add(G.gen.left(z, ps), outs(z, ps)) == List.length(&2, T.Pos, ps) : Nat}
622
623def gen_left_firsts(z, ps):
624  match ps:
625    case Nil{}:
626      {==}
627    case p <> t:
628      gen_left_firsts.go(z, p, t, G.gen.out(z, p), gen_left_firsts(z, t))
629
630law firsts_append:
631  for +z: G.Zone
632  for +xs: List<&2, T.Pos>
633  for +ys: List<&2, T.Pos>
634  {outs(z, List.append(&2, T.Pos, xs, ys)) == Nat.add(outs(z, xs), outs(z, ys)) : Nat}
635
636def firsts_append(z, xs, ys):
637  match xs:
638    case Nil{}:
639      {==}
640    case p <> t:
641      %Equal.sym(Nat, outs(z, List.append(&2, T.Pos, t, ys)),
642        Nat.add(outs(z, t), outs(z, ys)), firsts_append(z, t, ys)) :
643        {Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), _)
644          == Nat.add(Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t)), outs(z, ys)) : Nat}
645      Equal.sym(Nat, Nat.add(Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t)), outs(z, ys)),
646        Nat.add(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), Nat.add(outs(z, t), outs(z, ys))),
647        P.add_assoc(Bool.pick(Nat, G.gen.out(z, p), 1n, 0n), outs(z, t), outs(z, ys)))
648
649# How many elements of xs are i.
650def cnt(+i: Nat, xs: List<&2, Nat>) -> Nat:
651  match xs:
652    case Nil{}:
653      0n
654    case x <> t:
655      Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t))
656
657law cnt_append:
658  for +i: Nat
659  for +xs: List<&2, Nat>
660  for +ys: List<&2, Nat>
661  {cnt(i, List.append(&2, Nat, xs, ys)) == Nat.add(cnt(i, xs), cnt(i, ys)) : Nat}
662
663def cnt_append(i, xs, ys):
664  match xs:
665    case Nil{}:
666      {==}
667    case x <> t:
668      %Equal.sym(Nat, cnt(i, List.append(&2, Nat, t, ys)), Nat.add(cnt(i, t), cnt(i, ys)), cnt_append(i, t, ys)) :
669        {Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), _)
670          == Nat.add(Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t)), cnt(i, ys)) : Nat}
671      Equal.sym(Nat, Nat.add(Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t)), cnt(i, ys)),
672        Nat.add(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), Nat.add(cnt(i, t), cnt(i, ys))),
673        P.add_assoc(Bool.pick(Nat, Nat.is_eq(x, i), 1n, 0n), cnt(i, t), cnt(i, ys)))
674
675law cnt_step:
676  for +i: Nat
677  for +p: Nat
678  {Nat.add(Bool.pick(Nat, Nat.is_lt(i, p), 1n, 0n), Nat.add(Bool.pick(Nat, Nat.is_eq(p, i), 1n, 0n), 0n))
679    == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
680
681def cnt_step(i, p):
682  match i p:
683    case 0n 0n:
684      {==}
685    case 0n 1n+q:
686      {==}
687    case 1n+j 0n:
688      %Equal.sym(Bool, Nat.is_lt(j, 0n), False{}, P.lt_zero(j)) :
689        {0n == Bool.pick(Nat, _, 1n, 0n) : Nat}
690      {==}
691    case 1n+j 1n+q:
692      cnt_step(j, q)
693
694# Each number below n appears in range(n) once.
695law cnt_range:
696  for +i: Nat
697  for +n: Nat
698  {cnt(i, List.range(n)) == Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n) : Nat}
699
700def cnt_range(i, n):
701  match n:
702    case 0n:
703      %Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, P.lt_zero(i)) :
704        {0n == Bool.pick(Nat, _, 1n, 0n) : Nat}
705      {==}
706    case 1n+p:
707      %Equal.sym(List<&2, Nat>, List.range(1n+p), List.append(&2, Nat, List.range(p), [p]), P.range_snoc(p)) :
708        {cnt(i, _) == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
709      %Equal.sym(Nat, cnt(i, List.append(&2, Nat, List.range(p), [p])),
710        Nat.add(cnt(i, List.range(p)), cnt(i, [p])), cnt_append(i, List.range(p), [p])) :
711        {_ == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
712      %Equal.sym(Nat, cnt(i, List.range(p)), Bool.pick(Nat, Nat.is_lt(i, p), 1n, 0n), cnt_range(i, p)) :
713        {Nat.add(_, cnt(i, [p])) == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}
714      cnt_step(i, p)
715
716def firsts_row.end(+a: Bool, +b: Bool, +c: Nat) ->
717  {Nat.add(Bool.pick(Nat, Bool.and(a, b), 1n, 0n), Bool.pick(Nat, b, c, 0n))
718    == Bool.pick(Nat, b, Nat.add(Bool.pick(Nat, a, 1n, 0n), c), 0n) : Nat}:
719  match a b:
720    case True{} True{}:
721      {==}
722    case True{} False{}:
723      {==}
724    case False{} True{}:
725      {==}
726    case False{} False{}:
727      {==}
728
729def firsts_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
730  +e: {Nat.is_eq(y, fy) == b : Bool}) ->
731  {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, cnt(fx, xs), 0n) : Nat}:
732  match xs:
733    case Nil{}:
734      match b:
735        case True{}:
736          {==}
737        case False{}:
738          {==}
739    case x <> t:
740      %Equal.sym(Bool, Nat.is_eq(y, fy), b, e) :
741        {Nat.add(Bool.pick(Nat, Bool.and(Nat.is_eq(x, fx), _), 1n, 0n), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, t)))
742          == Bool.pick(Nat, b, cnt(fx, x <> t), 0n) : Nat}
743      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, t)), Bool.pick(Nat, b, cnt(fx, t), 0n),
744        firsts_row.go(fx, fy, y, t, b, e)) :
745        {Nat.add(Bool.pick(Nat, Bool.and(Nat.is_eq(x, fx), b), 1n, 0n), _)
746          == Bool.pick(Nat, b, cnt(fx, x <> t), 0n) : Nat}
747      firsts_row.end(Nat.is_eq(x, fx), b, cnt(fx, t))
748
749def firsts_rows.go(+fx: Nat, +fy: Nat, +w: Nat, +y: Nat, +t: List<&2, Nat>,
750  c1: {cnt(fx, List.range(w)) == 1n : Nat},
751  ih: {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)) == cnt(fy, t) : Nat}) ->
752  {outs(G.Zone{T.Pos{fx, fy}, False{}}, List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t)))
753    == cnt(fy, y <> t) : Nat}:
754  +row = B.row_cells(y, List.range(w))
755  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, List.append(&2, T.Pos, row, B.cells.go(w, t))),
756    Nat.add(outs(G.Zone{T.Pos{fx, fy}, False{}}, row), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t))),
757    firsts_append(G.Zone{T.Pos{fx, fy}, False{}}, row, B.cells.go(w, t))) : {_ == cnt(fy, y <> t) : Nat}
758  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, row), Bool.pick(Nat, Nat.is_eq(y, fy), cnt(fx, List.range(w)), 0n),
759    firsts_row.go(fx, fy, y, List.range(w), Nat.is_eq(y, fy), {==})) :
760    {Nat.add(_, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t))) == cnt(fy, y <> t) : Nat}
761  %Equal.sym(Nat, cnt(fx, List.range(w)), 1n, c1) :
762    {Nat.add(Bool.pick(Nat, Nat.is_eq(y, fy), _, 0n), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)))
763      == cnt(fy, y <> t) : Nat}
764  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)), cnt(fy, t), ih) :
765    {Nat.add(Bool.pick(Nat, Nat.is_eq(y, fy), 1n, 0n), _) == cnt(fy, y <> t) : Nat}
766  {==}
767
768law firsts_rows:
769  for +fx: Nat
770  for +fy: Nat
771  for +w: Nat
772  for +ys: List<&2, Nat>
773  for +c1: {cnt(fx, List.range(w)) == 1n : Nat}
774  {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, ys)) == cnt(fy, ys) : Nat}
775
776def firsts_rows(fx, fy, w, ys, c1):
777  match ys:
778    case Nil{}:
779      {==}
780    case y <> t:
781      firsts_rows.go(fx, fy, w, y, t, c1, firsts_rows(fx, fy, w, t, c1))
782
783law row_cells_len:
784  for +y: Nat
785  for +xs: List<&2, Nat>
786  {List.length(&2, T.Pos, B.row_cells(y, xs)) == List.length(&2, Nat, xs) : Nat}
787
788def row_cells_len(y, xs):
789  match xs:
790    case Nil{}:
791      {==}
792    case x <> t:
793      %Equal.sym(Nat, List.length(&2, T.Pos, B.row_cells(y, t)), List.length(&2, Nat, t), row_cells_len(y, t)) :
794        {1n+_ == 1n+List.length(&2, Nat, t) : Nat}
795      {==}
796
797law cells_go_len:
798  for +w: Nat
799  for +ys: List<&2, Nat>
800  {List.length(&2, T.Pos, B.cells.go(w, ys)) == Nat.mul(List.length(&2, Nat, ys), w) : Nat}
801
802def cells_go_len(w, ys):
803  match ys:
804    case Nil{}:
805      {==}
806    case y <> t:
807      +row = B.row_cells(y, List.range(w))
808      %Equal.sym(Nat, List.length(&2, T.Pos, List.append(&2, T.Pos, row, B.cells.go(w, t))),
809        Nat.add(List.length(&2, T.Pos, row), List.length(&2, T.Pos, B.cells.go(w, t))),
810        P.length_append(T.Pos, row, B.cells.go(w, t))) :
811        {_ == Nat.add(w, Nat.mul(List.length(&2, Nat, t), w)) : Nat}
812      %Equal.sym(Nat, List.length(&2, T.Pos, row), w,
813        Equal.trans(Nat, List.length(&2, T.Pos, row), List.length(&2, Nat, List.range(w)), w,
814          row_cells_len(y, List.range(w)), P.range_length(w))) :
815        {Nat.add(_, List.length(&2, T.Pos, B.cells.go(w, t))) == Nat.add(w, Nat.mul(List.length(&2, Nat, t), w)) : Nat}
816      %Equal.sym(Nat, List.length(&2, T.Pos, B.cells.go(w, t)), Nat.mul(List.length(&2, Nat, t), w), cells_go_len(w, t)) :
817        {Nat.add(w, _) == Nat.add(w, Nat.mul(List.length(&2, Nat, t), w)) : Nat}
818      {==}
819
820def one_when(+i: Nat, +n: Nat, lt: {Nat.is_lt(i, n) == True{} : Bool}) -> {cnt(i, List.range(n)) == 1n : Nat}:
821  Equal.trans(Nat, cnt(i, List.range(n)), Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n), 1n,
822    cnt_range(i, n),
823    Equal.cong(Bool, Nat, b => Bool.pick(Nat, b, 1n, 0n), Nat.is_lt(i, n), True{}, lt))
824
825# Arithmetic
826# ==========
827
828law le_trans:
829  for +a: Nat
830  for +b: Nat
831  for +c: Nat
832  for e1: {Nat.is_le(a, b) == True{} : Bool}
833  for e2: {Nat.is_le(b, c) == True{} : Bool}
834  {Nat.is_le(a, c) == True{} : Bool}
835
836def le_trans.k(+a: Nat, +b: Nat, +c: Nat, r1: P.LeW(a, b), r2: P.LeW(b, c)) -> {Nat.is_le(a, c) == True{} : Bool}:
837  match r1:
838    case (+k1, e1):
839      match r2:
840        case (+k2, e2):
841          %Equal.sym(Nat, c, Nat.add(b, k2), e2) : {Nat.is_le(a, _) == True{} : Bool}
842          %Equal.sym(Nat, b, Nat.add(a, k1), e1) : {Nat.is_le(a, Nat.add(_, k2)) == True{} : Bool}
843          %Equal.sym(Nat, Nat.add(Nat.add(a, k1), k2), Nat.add(a, Nat.add(k1, k2)), P.add_assoc(a, k1, k2)) :
844            {Nat.is_le(a, _) == True{} : Bool}
845          P.le_of_add(a, Nat.add(k1, k2))
846
847def le_trans(a, b, c, e1, e2):
848  le_trans.k(a, b, c, P.le_witness(a, b, e1), P.le_witness(b, c, e2))
849
850law add_cancel_l:
851  for +c: Nat
852  for +a: Nat
853  for +b: Nat
854  for e: {Nat.add(c, a) == Nat.add(c, b) : Nat}
855  {a == b : Nat}
856
857def add_cancel_l(c, a, b, e):
858  match c:
859    case 0n:
860      e
861    case 1n+k:
862      add_cancel_l(k, a, b, P.succ_inj(Nat.add(k, a), Nat.add(k, b), e))
863
864# ((a+b)+c) + ((a'+b')+c') regrouped as ((a+a')+(b+b')) + (c+c').
865def swap3(+a: Nat, +b: Nat, +c: Nat, +a2: Nat, +b2: Nat, +c2: Nat) ->
866  {Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a2, b2), c2))
867    == Nat.add(Nat.add(Nat.add(a, a2), Nat.add(b, b2)), Nat.add(c, c2)) : Nat}:
868  %P.add_swap(a, b, a2, b2) : {Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a2, b2), c2))
869    == Nat.add(_, Nat.add(c, c2)) : Nat}
870  P.add_swap(Nat.add(a, b), c, Nat.add(a2, b2), c2)
871
872# Room for n mines and 9 more among the L + O cells, with O <= 9: n <= L.
873def room_left.k(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
874  wb: P.LeW(o, 9n), wr: P.LeW(Nat.add(n, 9n), m)) -> {Nat.is_le(n, l) == True{} : Bool}:
875  match wb:
876    case (+d, eb):
877      match wr:
878        case (+k, er):
879          +dk = Nat.add(d, k)
880          +t1 = Equal.trans(Nat, Nat.add(o, l), m, Nat.add(Nat.add(n, 9n), k),
881            Equal.trans(Nat, Nat.add(o, l), Nat.add(l, o), m, P.add_comm(o, l), e), er)
882          +t2 = Equal.cong(Nat, Nat, x => Nat.add(Nat.add(n, x), k), 9n, Nat.add(o, d), eb)
883          +t4 = Equal.cong(Nat, Nat, x => Nat.add(n, x), Nat.add(Nat.add(o, d), k), Nat.add(o, dk), P.add_assoc(o, d, k))
884          +t345 = Equal.trans(Nat, Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(n, Nat.add(Nat.add(o, d), k)),
885            Nat.add(o, Nat.add(n, dk)), P.add_assoc(n, Nat.add(o, d), k),
886            Equal.trans(Nat, Nat.add(n, Nat.add(Nat.add(o, d), k)), Nat.add(n, Nat.add(o, dk)), Nat.add(o, Nat.add(n, dk)),
887              t4, P.add_left_comm(n, o, dk)))
888          +e3 = Equal.trans(Nat, Nat.add(o, l), Nat.add(Nat.add(n, 9n), k), Nat.add(o, Nat.add(n, dk)), t1,
889            Equal.trans(Nat, Nat.add(Nat.add(n, 9n), k), Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(o, Nat.add(n, dk)),
890              t2, t345))
891          %Equal.sym(Nat, l, Nat.add(n, dk), add_cancel_l(o, l, Nat.add(n, dk), e3)) : {Nat.is_le(n, _) == True{} : Bool}
892          P.le_of_add(n, dk)
893
894def room_left(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
895  r: {Nat.is_le(Nat.add(n, 9n), m) == True{} : Bool}, b: {Nat.is_le(o, 9n) == True{} : Bool}) ->
896  {Nat.is_le(n, l) == True{} : Bool}:
897  room_left.k(l, o, m, n, e, P.le_witness(o, 9n, b), P.le_witness(Nat.add(n, 9n), m, r))
898
899# At most nine cells near the first click
900# =======================================
901
902# x is within one step of a.
903def nr(+a: Nat, +x: Nat) -> Bool:
904  Nat.is_le(B.dist(a, x), 1n)
905
906# How many elements of xs are within one step of a.
907def ncnt(+a: Nat, xs: List<&2, Nat>) -> Nat:
908  match xs:
909    case Nil{}:
910      0n
911    case x <> t:
912      Nat.add(one(nr(a, x)), ncnt(a, t))
913
914# How many elements of xs are one below a.
915def cnt1(+a: Nat, xs: List<&2, Nat>) -> Nat:
916  match xs:
917    case Nil{}:
918      0n
919    case x <> t:
920      Nat.add(one(Nat.is_eq(1n+x, a)), cnt1(a, t))
921
922# Within one step of a means a, a + 1 or a - 1.
923law near_pt:
924  for +a: Nat
925  for +x: Nat
926  {Nat.is_le(one(nr(a, x)), Nat.add(Nat.add(one(Nat.is_eq(x, a)), one(Nat.is_eq(x, 1n+a))), one(Nat.is_eq(1n+x, a))))
927    == True{} : Bool}
928
929def near_pt.zx(+j: Nat) ->
930  {Nat.is_le(one(nr(0n, 1n+j)), Nat.add(Nat.add(one(Nat.is_eq(1n+j, 0n)), one(Nat.is_eq(1n+j, 1n))), one(Nat.is_eq(2n+j, 0n))))
931    == True{} : Bool}:
932  match j:
933    case 0n:
934      {==}
935    case 1n+i:
936      P.le_zero_l(Nat.add(Nat.add(one(Nat.is_eq(2n+i, 0n)), one(Nat.is_eq(2n+i, 1n))), one(Nat.is_eq(3n+i, 0n))))
937
938def near_pt.xz(+k: Nat) ->
939  {Nat.is_le(one(nr(1n+k, 0n)), Nat.add(Nat.add(one(Nat.is_eq(0n, 1n+k)), one(Nat.is_eq(0n, 2n+k))), one(Nat.is_eq(1n, 1n+k))))
940    == True{} : Bool}:
941  match k:
942    case 0n:
943      {==}
944    case 1n+i:
945      P.le_zero_l(Nat.add(Nat.add(one(Nat.is_eq(0n, 2n+i)), one(Nat.is_eq(0n, 3n+i))), one(Nat.is_eq(1n, 2n+i))))
946
947def near_pt(a, x):
948  match a x:
949    case 0n 0n:
950      {==}
951    case 0n 1n+j:
952      near_pt.zx(j)
953    case 1n+k 0n:
954      near_pt.xz(k)
955    case 1n+k 1n+j:
956      near_pt(k, j)
957
958law near_cnt:
959  for +a: Nat
960  for +xs: List<&2, Nat>
961  {Nat.is_le(ncnt(a, xs), Nat.add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), cnt1(a, xs))) == True{} : Bool}
962
963def near_cnt(a, xs):
964  match xs:
965    case Nil{}:
966      {==}
967    case x <> t:
968      +o1 = one(Nat.is_eq(x, a))
969      +o2 = one(Nat.is_eq(x, 1n+a))
970      +o3 = one(Nat.is_eq(1n+x, a))
971      %swap3(o1, o2, o3, cnt(a, t), cnt(1n+a, t), cnt1(a, t)) :
972        {Nat.is_le(Nat.add(one(nr(a, x)), ncnt(a, t)), _) == True{} : Bool}
973      P.le_add(one(nr(a, x)), Nat.add(Nat.add(o1, o2), o3), ncnt(a, t), Nat.add(Nat.add(cnt(a, t), cnt(1n+a, t)), cnt1(a, t)),
974        near_pt(a, x), near_cnt(a, t))
975
976law cnt1_succ:
977  for +a: Nat
978  for +xs: List<&2, Nat>
979  {cnt1(1n+a, xs) == cnt(a, xs) : Nat}
980
981def cnt1_succ(a, xs):
982  match xs:
983    case Nil{}:
984      {==}
985    case x <> t:
986      %cnt1_succ(a, t) : {Nat.add(one(Nat.is_eq(1n+x, 1n+a)), cnt1(1n+a, t))
987        == Nat.add(one(Nat.is_eq(x, a)), _) : Nat}
988      {==}
989
990law cnt1_zero:
991  for +xs: List<&2, Nat>
992  {cnt1(0n, xs) == 0n : Nat}
993
994def cnt1_zero(xs):
995  match xs:
996    case Nil{}:
997      {==}
998    case x <> t:
999      cnt1_zero(t)
1000
1001def pick_le1(+b: Bool) -> {Nat.is_le(Bool.pick(Nat, b, 1n, 0n), 1n) == True{} : Bool}:
1002  match b:
1003    case True{}:
1004      {==}
1005    case False{}:
1006      {==}
1007
1008def cnt_le1(+i: Nat, +n: Nat) -> {Nat.is_le(cnt(i, List.range(n)), 1n) == True{} : Bool}:
1009  %Equal.sym(Nat, cnt(i, List.range(n)), Bool.pick(Nat, Nat.is_lt(i, n), 1n, 0n), cnt_range(i, n)) :
1010    {Nat.is_le(_, 1n) == True{} : Bool}
1011  pick_le1(Nat.is_lt(i, n))
1012
1013def cnt1_le1(+a: Nat, +n: Nat) -> {Nat.is_le(cnt1(a, List.range(n)), 1n) == True{} : Bool}:
1014  match a:
1015    case 0n:
1016      %Equal.sym(Nat, cnt1(0n, List.range(n)), 0n, cnt1_zero(List.range(n))) : {Nat.is_le(_, 1n) == True{} : Bool}
1017      {==}
1018    case 1n+k:
1019      %Equal.sym(Nat, cnt1(1n+k, List.range(n)), cnt(k, List.range(n)), cnt1_succ(k, List.range(n))) :
1020        {Nat.is_le(_, 1n) == True{} : Bool}
1021      cnt_le1(k, n)
1022
1023# At most three numbers below n are within one step of a.
1024law ncnt_le3:
1025  for +a: Nat
1026  for +n: Nat
1027  {Nat.is_le(ncnt(a, List.range(n)), 3n) == True{} : Bool}
1028
1029def ncnt_le3(a, n):
1030  +xs = List.range(n)
1031  le_trans(ncnt(a, xs), Nat.add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), cnt1(a, xs)), 3n,
1032    near_cnt(a, xs),
1033    P.le_add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), 2n, cnt1(a, xs), 1n,
1034      P.le_add(cnt(a, xs), 1n, cnt(1n+a, xs), 1n, cnt_le1(a, n), cnt_le1(1n+a, n)),
1035      cnt1_le1(a, n)))
1036
1037def wide_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
1038  +e: {nr(fy, y) == b : Bool}) ->
1039  {outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, ncnt(fx, xs), 0n) : Nat}:
1040  match xs:
1041    case Nil{}:
1042      match b:
1043        case True{}:
1044          {==}
1045        case False{}:
1046          {==}
1047    case x <> t:
1048      %Equal.sym(Bool, nr(fy, y), b, e) :
1049        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), _), 1n, 0n), outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)))
1050          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
1051      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)), Bool.pick(Nat, b, ncnt(fx, t), 0n),
1052        wide_row.go(fx, fy, y, t, b, e)) :
1053        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), b), 1n, 0n), _)
1054          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
1055      firsts_row.end(nr(fx, x), b, ncnt(fx, t))
1056
1057# Each row near the first click's row, counted c times.
1058def rsum(+fy: Nat, +c: Nat, ys: List<&2, Nat>) -> Nat:
1059  match ys:
1060    case Nil{}:
1061      0n
1062    case y <> t:
1063      Nat.add(Bool.pick(Nat, nr(fy, y), c, 0n), rsum(fy, c, t))
1064
1065law wide_rows:
1066  for +fx: Nat
1067  for +fy: Nat
1068  for +w: Nat
1069  for +ys: List<&2, Nat>
1070  {outs(G.Zone{T.Pos{fx, fy}, True{}}, B.cells.go(w, ys)) == rsum(fy, ncnt(fx, List.range(w)), ys) : Nat}
1071
1072def wide_rows(fx, fy, w, ys):
1073  match ys:
1074    case Nil{}:
1075      {==}
1076    case y <> t:
1077      +z = {G.Zone{T.Pos{fx, fy}, True{}} : G.Zone}
1078      +row = B.row_cells(y, List.range(w))
1079      +c = ncnt(fx, List.range(w))
1080      %Equal.sym(Nat, outs(z, List.append(&2, T.Pos, row, B.cells.go(w, t))),
1081        Nat.add(outs(z, row), outs(z, B.cells.go(w, t))), firsts_append(z, row, B.cells.go(w, t))) :
1082        {_ == rsum(fy, c, y <> t) : Nat}
1083      %Equal.sym(Nat, outs(z, row), Bool.pick(Nat, nr(fy, y), c, 0n), wide_row.go(fx, fy, y, List.range(w), nr(fy, y), {==})) :
1084        {Nat.add(_, outs(z, B.cells.go(w, t))) == rsum(fy, c, y <> t) : Nat}
1085      %Equal.sym(Nat, outs(z, B.cells.go(w, t)), rsum(fy, c, t), wide_rows(fx, fy, w, t)) :
1086        {Nat.add(Bool.pick(Nat, nr(fy, y), c, 0n), _) == rsum(fy, c, y <> t) : Nat}
1087      {==}
1088
1089def pick_le3(+b: Bool, +c: Nat, lc: {Nat.is_le(c, 3n) == True{} : Bool}) ->
1090  {Nat.is_le(Bool.pick(Nat, b, c, 0n), Nat.add(Nat.add(one(b), one(b)), one(b))) == True{} : Bool}:
1091  match b:
1092    case True{}:
1093      lc
1094    case False{}:
1095      {==}
1096
1097law rsum_le:
1098  for +fy: Nat
1099  for +c: Nat
1100  for +ys: List<&2, Nat>
1101  for +lc: {Nat.is_le(c, 3n) == True{} : Bool}
1102  {Nat.is_le(rsum(fy, c, ys), Nat.add(Nat.add(ncnt(fy, ys), ncnt(fy, ys)), ncnt(fy, ys))) == True{} : Bool}
1103
1104def rsum_le(fy, c, ys, lc):
1105  match ys:
1106    case Nil{}:
1107      {==}
1108    case y <> t:
1109      +o = one(nr(fy, y))
1110      +nt = ncnt(fy, t)
1111      %swap3(o, o, o, nt, nt, nt) :
1112        {Nat.is_le(rsum(fy, c, y <> t), _) == True{} : Bool}
1113      P.le_add(Bool.pick(Nat, nr(fy, y), c, 0n), Nat.add(Nat.add(o, o), o), rsum(fy, c, t), Nat.add(Nat.add(nt, nt), nt),
1114        pick_le3(nr(fy, y), c, lc), rsum_le(fy, c, t, lc))
1115
1116# The zone around a first click holds at most 9 cells of the board.
1117law wide_le9:
1118  for +fx: Nat
1119  for +fy: Nat
1120  for +w: Nat
1121  for +h: Nat
1122  {Nat.is_le(outs(G.Zone{T.Pos{fx, fy}, True{}}, B.cells(w, h)), 9n) == True{} : Bool}
1123
1124def wide_le9(fx, fy, w, h):
1125  +c = ncnt(fx, List.range(w))
1126  +ny = ncnt(fy, List.range(h))
1127  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, True{}}, B.cells(w, h)), rsum(fy, c, List.range(h)),
1128    wide_rows(fx, fy, w, List.range(h))) : {Nat.is_le(_, 9n) == True{} : Bool}
1129  le_trans(rsum(fy, c, List.range(h)), Nat.add(Nat.add(ny, ny), ny), 9n,
1130    rsum_le(fy, c, List.range(h), ncnt_le3(fx, w)),
1131    P.le_add(Nat.add(ny, ny), 6n, ny, 3n,
1132      P.le_add(ny, 3n, ny, 3n, ncnt_le3(fy, h), ncnt_le3(fy, h)), ncnt_le3(fy, h)))
1133
1134# Exactly n mines, again
1135# =====================
1136
1137def cells_len(+w: Nat, +h: Nat) -> {List.length(&2, T.Pos, B.cells(w, h)) == Nat.mul(w, h) : Nat}:
1138  Equal.trans(Nat, List.length(&2, T.Pos, B.cells(w, h)),
1139    Nat.mul(List.length(&2, Nat, List.range(h)), w), Nat.mul(w, h),
1140    cells_go_len(w, List.range(h)),
1141    %Equal.sym(Nat, List.length(&2, Nat, List.range(h)), h, P.range_length(h)) :
1142      {Nat.mul(_, w) == Nat.mul(w, h) : Nat};
1143      P.mul_comm(h, w))
1144
1145# With just the first click kept free, there are w*h - 1 candidates, so
1146# n < w*h mines fit among them.
1147law gen_inv_one:
1148  for +w: Nat
1149  for +h: Nat
1150  for +n: Nat
1151  for +fx: Nat
1152  for +fy: Nat
1153  for +on: {L.on_board(w, h, T.Pos{fx, fy}) == True{} : Bool}
1154  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1155  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, False{}}, B.cells(w, h))) == True{} : Bool}
1156
1157def gen_inv_one(w, h, n, fx, fy, on, fits):
1158  +z = {G.Zone{T.Pos{fx, fy}, False{}} : G.Zone}
1159  +gl = G.gen.left(z, B.cells(w, h))
1160  +xw = P.and_true_l(Nat.is_lt(fx, w), Nat.is_lt(fy, h), on)
1161  +yh = P.and_true_r(Nat.is_lt(fx, w), Nat.is_lt(fy, h), on)
1162  +f1 = Equal.trans(Nat, outs(z, B.cells(w, h)), cnt(fy, List.range(h)), 1n,
1163    firsts_rows(fx, fy, w, List.range(h), one_when(fx, w, xw)), one_when(fy, h, yh))
1164  +e1 = {%f1 : {Nat.add(gl, _) == List.length(&2, T.Pos, B.cells(w, h)) : Nat};
1165    gen_left_firsts(z, B.cells(w, h)) : {Nat.add(gl, 1n) == List.length(&2, T.Pos, B.cells(w, h)) : Nat}}
1166  +e2 = Equal.trans(Nat, 1n+gl, Nat.add(gl, 1n), Nat.mul(w, h),
1167    Equal.sym(Nat, Nat.add(gl, 1n), 1n+gl, P.add_one(gl)),
1168    Equal.trans(Nat, Nat.add(gl, 1n), List.length(&2, T.Pos, B.cells(w, h)), Nat.mul(w, h), e1, cells_len(w, h)))
1169  P.lt_succ_le(n, gl,
1170    {%Equal.sym(Nat, 1n+gl, Nat.mul(w, h), e2) : {Nat.is_lt(n, _) == True{} : Bool};
1171      fits : {Nat.is_lt(n, 1n+gl) == True{} : Bool}})
1172
1173# With room for 9 more, n mines fit outside the wider zone.
1174law gen_inv_wide:
1175  for +w: Nat
1176  for +h: Nat
1177  for +n: Nat
1178  for +fx: Nat
1179  for +fy: Nat
1180  for room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
1181  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, True{}}, B.cells(w, h))) == True{} : Bool}
1182
1183def gen_inv_wide(w, h, n, fx, fy, room):
1184  +z = {G.Zone{T.Pos{fx, fy}, True{}} : G.Zone}
1185  +gl = G.gen.left(z, B.cells(w, h))
1186  +o = outs(z, B.cells(w, h))
1187  room_left(gl, o, Nat.mul(w, h), n,
1188    Equal.trans(Nat, Nat.add(gl, o), List.length(&2, T.Pos, B.cells(w, h)), Nat.mul(w, h),
1189      gen_left_firsts(z, B.cells(w, h)), cells_len(w, h)),
1190    room, wide_le9(fx, fy, w, h))
1191
1192def gen_inv.k(+w: Nat, +h: Nat, +n: Nat, +fx: Nat, +fy: Nat,
1193  +on: {L.on_board(w, h, T.Pos{fx, fy}) == True{} : Bool}, fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool},
1194  +wide: Bool, ew: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == wide : Bool}) ->
1195  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, wide}, B.cells(w, h))) == True{} : Bool}:
1196  match wide:
1197    case False{}:
1198      gen_inv_one(w, h, n, fx, fy, on, fits)
1199    case True{}:
1200      gen_inv_wide(w, h, n, fx, fy, ew)
1201
1202# Whichever zone the board keeps free, the n mines fit outside it.
1203law gen_inv:
1204  for +w: Nat
1205  for +h: Nat
1206  for +n: Nat
1207  for +first: T.Pos
1208  for +on: {L.on_board(w, h, first) == True{} : Bool}
1209  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1210  {Nat.is_le(n, G.gen.left(zone(w, h, n, first), B.cells(w, h))) == True{} : Bool}
1211
1212def gen_inv(w, h, n, first, on, fits):
1213  match first:
1214    case T.Pos{fx, fy}:
1215      gen_inv.k(w, h, n, fx, fy, on, fits, Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)), {==})
1216
1217law gen_count_:
1218  for +w: Nat
1219  for +h: Nat
1220  for +n: Nat
1221  for +first: T.Pos
1222  for +rs: List<&2, U32>
1223  for on: {L.on_board(w, h, first) == True{} : Bool}
1224  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1225  {L.total_mines(G.place_mines(w, h, n, first, rs)) == n : Nat}
1226
1227def gen_count_(w, h, n, first, rs, on, fits):
1228  +z = zone(w, h, n, first)
1229  gen_rows_count(z, w, List.range(h),
1230    {G.GenState{n, G.gen.left(z, B.cells(w, h)), rs} : G.GenState},
1231    gen_inv(w, h, n, first, on, fits), {==})