proof_flood.bend
minebender-game@1.0.0.0 · 637 lines · 34 definitions
1import Base
2import minebender-game@1.0.0.0/types.bend as T
3import minebender-game@1.0.0.0/board.bend as B
4import minebender-game@1.0.0.0/game.bend as G
5import minebender-game@1.0.0.0/LAWS.bend as L
6import minebender-game@1.0.0.0/proof_base.bend as P
7import minebender-game@1.0.0.0/proof_grid.bend as PG
8import minebender-game@1.0.0.0/proof_copy.bend as PC
9import minebender-game@1.0.0.0/proof_lists.bend as PL
10import minebender-game@1.0.0.0/proof_cells.bend as PS
11import minebender-game@1.0.0.0/proof_walk.bend as PW
12
13
14
15
16
17
18def at_true_self.col(+r: List<&2, Bool>, +x: Nat, +b: Bool,
19 be: {Nat.is_lt(x, List.length(&2, Bool, r)) == b : Bool},
20 e: {Maybe.default(&2, Bool, List.get(&2, Bool, r, x), False{}) == True{} : Bool}) ->
21 {Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool}:
22 match b:
23 case True{}:
24 %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), Some{True{}},
25 PL.get_set_eq(Bool, r, x, True{}, be)) : {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}
26 {==}
27 case False{}:
28 Empty.absurd({Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool},
29 P.false_ne_true(%P.get_out(Bool, r, x, be) :
30 {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; e))
31
32def at_true_self.row(+g: T.Grid(Bool), +x: Nat, +y: Nat, +b: Bool,
33 be: {Nat.is_lt(y, List.length(&2, List<&2, Bool>, g)) == b : Bool},
34 e: {B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool}) ->
35 {B.at(Bool, False{}, B.set_at(Bool, g, T.Pos{x, y}, True{}), T.Pos{x, y}) == True{} : Bool}:
36 match b:
37 case True{}:
38 +r = PL.row_of(Bool, g, y)
39 +r2 = List.set(&2, Bool, r, x, True{})
40 %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, List.set(&2, List<&2, Bool>, g, y, r2), y),
41 Some{r2}, PL.get_set_eq(List<&2, Bool>, g, y, r2, be)) :
42 {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
43 == True{} : Bool}
44 at_true_self.col(r, x, Nat.is_lt(x, List.length(&2, Bool, r)), {==}, e)
45 case False{}:
46 Empty.absurd({B.at(Bool, False{}, B.set_at(Bool, g, T.Pos{x, y}, True{}), T.Pos{x, y}) == True{} : Bool},
47 P.false_ne_true(%P.get_out(List<&2, Bool>, g, y, be) :
48 {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
49 == True{} : Bool}; e))
50
51law at_true_self:
52 for +g: T.Grid(Bool)
53 for +q: T.Pos
54 for e: {B.at(Bool, False{}, g, q) == True{} : Bool}
55 {B.at(Bool, False{}, B.set_at(Bool, g, q, True{}), q) == True{} : Bool}
56
57def at_true_self(g, q, e):
58 match q:
59 case T.Pos{x, y}:
60 at_true_self.row(g, x, y, Nat.is_lt(y, List.length(&2, List<&2, Bool>, g)), {==}, e)
61
62def at_set_mono.go(+g: T.Grid(Bool), +p: T.Pos, +q: T.Pos, e: {B.at(Bool, False{}, g, q) == True{} : Bool},
63 +b: Bool, be: {B.same(p, q) == b : Bool}) ->
64 {B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q) == True{} : Bool}:
65 match b:
66 case True{}:
67 %Equal.sym(T.Pos, p, q, PG.same_sound(p, q, be)) :
68 {B.at(Bool, False{}, B.set_at(Bool, g, _, True{}), q) == True{} : Bool}
69 at_true_self(g, q, e)
70 case False{}:
71 %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q), B.at(Bool, False{}, g, q),
72 PL.at_set_ne(Bool, g, p, q, True{}, False{}, be)) : {_ == True{} : Bool}
73 e
74
75
76law at_set_mono:
77 for +g: T.Grid(Bool)
78 for +p: T.Pos
79 for +q: T.Pos
80 for e: {B.at(Bool, False{}, g, q) == True{} : Bool}
81 {B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q) == True{} : Bool}
82
83def at_set_mono(g, p, q, e):
84 at_set_mono.go(g, p, q, e, B.same(p, q), {==})
85
86
87
88
89law flood_shaped:
90 for +n: Nat
91 for +work: List<&2, G.Work>
92 for +hd: Bool
93 for +w: Nat
94 for +h: Nat
95 for +layout: T.Grid(Bool)
96 for +shown: T.Grid(Bool)
97 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
98 {B.shaped(Bool, w, h, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool}
99
100def flood_shaped(n, work, hd, w, h, layout, shown, sh):
101 match n:
102 case 0n:
103 sh
104 case 1n+m:
105 match work:
106 case Nil{}:
107 sh
108 case G.Work{c, back} <> rest:
109 match hd:
110 case False{}:
111 flood_shaped(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, sh)
112 case True{}:
113 +s2 = B.set_at(Bool, shown, c, True{})
114 +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
115 flood_shaped(m, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
116 PL.shaped_set(Bool, w, h, shown, c, True{}, sh))
117
118law flood_mono:
119 for +n: Nat
120 for +work: List<&2, G.Work>
121 for +hd: Bool
122 for +w: Nat
123 for +h: Nat
124 for +layout: T.Grid(Bool)
125 for +shown: T.Grid(Bool)
126 for +q: T.Pos
127 for +s: {B.at(Bool, False{}, shown, q) == True{} : Bool}
128 {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
129
130def flood_mono(n, work, hd, w, h, layout, shown, q, s):
131 match n:
132 case 0n:
133 s
134 case 1n+m:
135 match work:
136 case Nil{}:
137 s
138 case G.Work{c, back} <> rest:
139 match hd:
140 case False{}:
141 flood_mono(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, q, s)
142 case True{}:
143 +s2 = B.set_at(Bool, shown, c, True{})
144 +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
145 flood_mono(m, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2, q,
146 at_set_mono(shown, c, q, s))
147
148
149
150
151
152def wcontains(ws: List<&2, G.Work>, +q: T.Pos) -> Bool:
153 match ws:
154 case Nil{}:
155 False{}
156 case G.Work{c, back} <> t:
157 B.same(c, q) || wcontains(t, q)
158
159def wcontains_append_r.go(+c: T.Pos, +xs: List<&2, G.Work>, +ys: List<&2, G.Work>, +q: T.Pos,
160 ih: {wcontains(List.append(&2, G.Work, xs, ys), q) == True{} : Bool}) ->
161 {Bool.or(B.same(c, q), wcontains(List.append(&2, G.Work, xs, ys), q)) == True{} : Bool}:
162 %Equal.sym(Bool, wcontains(List.append(&2, G.Work, xs, ys), q), True{}, ih) :
163 {Bool.or(B.same(c, q), _) == True{} : Bool}
164 PS.or_true_r(B.same(c, q))
165
166law wcontains_append_r:
167 for +xs: List<&2, G.Work>
168 for +ys: List<&2, G.Work>
169 for +q: T.Pos
170 for e: {wcontains(ys, q) == True{} : Bool}
171 {wcontains(List.append(&2, G.Work, xs, ys), q) == True{} : Bool}
172
173def wcontains_append_r(xs, ys, q, e):
174 match xs:
175 case Nil{}:
176 e
177 case G.Work{c, back} <> t:
178 wcontains_append_r.go(c, t, ys, q, wcontains_append_r(t, ys, q, e))
179
180def wcontains_append_l.go(+c: T.Pos, +t: List<&2, G.Work>, +ys: List<&2, G.Work>, +q: T.Pos, +b: Bool,
181 e: {Bool.or(b, wcontains(t, q)) == True{} : Bool},
182 ih: {wcontains(t, q) == True{} : Bool} -> {wcontains(List.append(&2, G.Work, t, ys), q) == True{} : Bool}) ->
183 {Bool.or(b, wcontains(List.append(&2, G.Work, t, ys), q)) == True{} : Bool}:
184 match b:
185 case True{}:
186 {==}
187 case False{}:
188 ih(e)
189
190law wcontains_append_l:
191 for +xs: List<&2, G.Work>
192 for +ys: List<&2, G.Work>
193 for +q: T.Pos
194 for e: {wcontains(xs, q) == True{} : Bool}
195 {wcontains(List.append(&2, G.Work, xs, ys), q) == True{} : Bool}
196
197def wcontains_append_l(xs, ys, q, e):
198 match xs:
199 case Nil{}:
200 Empty.absurd({wcontains(ys, q) == True{} : Bool}, P.false_ne_true(e))
201 case G.Work{c, back} <> t:
202 wcontains_append_l.go(c, t, ys, q, B.same(c, q), e, et => wcontains_append_l(t, ys, q, et))
203
204def wcontains_works.go(+r0: T.Pos, +t: List<&2, T.Pos>, +back: List<&2, T.Pos>, +q: T.Pos, +b: Bool,
205 e: {Bool.or(b, B.contains(t, q)) == True{} : Bool},
206 ih: {B.contains(t, q) == True{} : Bool} -> {wcontains(G.works(t, back), q) == True{} : Bool}) ->
207 {Bool.or(b, wcontains(G.works(t, back), q)) == True{} : Bool}:
208 match b:
209 case True{}:
210 {==}
211 case False{}:
212 ih(e)
213
214law wcontains_works:
215 for +ns: List<&2, T.Pos>
216 for +back: List<&2, T.Pos>
217 for +q: T.Pos
218 for e: {B.contains(ns, q) == True{} : Bool}
219 {wcontains(G.works(ns, back), q) == True{} : Bool}
220
221def wcontains_works(ns, back, q, e):
222 match ns:
223 case Nil{}:
224 Empty.absurd({wcontains(Nil{}, q) == True{} : Bool}, P.false_ne_true(e))
225 case r <> t:
226 wcontains_works.go(r, t, back, q, B.same(r, q), e, et => wcontains_works(t, back, q, et))
227
228law push_keeps:
229 for +z: Bool
230 for +ns: List<&2, T.Pos>
231 for +back: List<&2, T.Pos>
232 for +rest: List<&2, G.Work>
233 for +q: T.Pos
234 for e: {wcontains(rest, q) == True{} : Bool}
235 {wcontains(G.push(z, ns, back, rest), q) == True{} : Bool}
236
237def push_keeps(z, ns, back, rest, q, e):
238 match z:
239 case True{}:
240 wcontains_append_r(G.works(ns, back), rest, q, e)
241 case False{}:
242 e
243
244
245
246
247law unrev_on:
248 for +w: Nat
249 for +h: Nat
250 for +shown: T.Grid(Bool)
251 for +c: T.Pos
252 for e: {G.unrevealed(w, h, shown, c) == True{} : Bool}
253 {B.on_board(w, h, c) == True{} : Bool}
254
255def unrev_on(w, h, shown, c, e):
256 P.and_true_l(B.on_board(w, h, c), Bool.not(B.at(Bool, False{}, shown, c)), e)
257
258law unrev_hidden:
259 for +w: Nat
260 for +h: Nat
261 for +shown: T.Grid(Bool)
262 for +c: T.Pos
263 for e: {G.unrevealed(w, h, shown, c) == True{} : Bool}
264 {B.at(Bool, False{}, shown, c) == False{} : Bool}
265
266def unrev_hidden(w, h, shown, c, e):
267 P.not_true(B.at(Bool, False{}, shown, c),
268 P.and_true_r(B.on_board(w, h, c), Bool.not(B.at(Bool, False{}, shown, c)), e))
269
270law unrev_shown:
271 for +w: Nat
272 for +h: Nat
273 for +shown: T.Grid(Bool)
274 for +c: T.Pos
275 for e: {G.unrevealed(w, h, shown, c) == False{} : Bool}
276 for on: {B.on_board(w, h, c) == True{} : Bool}
277 {B.at(Bool, False{}, shown, c) == True{} : Bool}
278
279def unrev_shown(w, h, shown, c, e, on):
280 P.not_false(B.at(Bool, False{}, shown, c),
281 %on : {Bool.and(_, Bool.not(B.at(Bool, False{}, shown, c))) == False{} : Bool}; e)
282
283law count_after:
284 for +w: Nat
285 for +h: Nat
286 for +shown: T.Grid(Bool)
287 for +c: T.Pos
288 for +m: Nat
289 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
290 for +u: {G.unrevealed(w, h, shown, c) == True{} : Bool}
291 for cnt: {1n+m == B.count_false(shown) : Nat}
292 {m == B.count_false(B.set_at(Bool, shown, c, True{})) : Nat}
293
294def count_after(w, h, shown, c, m, sh, u, cnt):
295 match c:
296 case T.Pos{x, y}:
297 P.succ_inj(m, B.count_false(B.set_at(Bool, shown, T.Pos{x, y}, True{})),
298 Equal.trans(Nat, 1n+m, B.count_false(shown), 1n+B.count_false(B.set_at(Bool, shown, T.Pos{x, y}, True{})),
299 cnt, PL.count_false_set(w, h, shown, x, y, sh, unrev_on(w, h, shown, T.Pos{x, y}, u),
300 unrev_hidden(w, h, shown, T.Pos{x, y}, u))))
301
302law at_set_on:
303 for +w: Nat
304 for +h: Nat
305 for +shown: T.Grid(Bool)
306 for +c: T.Pos
307 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
308 for on: {B.on_board(w, h, c) == True{} : Bool}
309 {B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), c) == True{} : Bool}
310
311def at_set_on(w, h, shown, c, sh, on):
312 match c:
313 case T.Pos{x, y}:
314 PL.at_set_eq(Bool, w, h, shown, x, y, True{}, False{}, sh, on)
315
316law cf_zero:
317 for +w: Nat
318 for +h: Nat
319 for +shown: T.Grid(Bool)
320 for +q: T.Pos
321 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
322 for on: {B.on_board(w, h, q) == True{} : Bool}
323 for z: {0n == B.count_false(shown) : Nat}
324 {B.at(Bool, False{}, shown, q) == True{} : Bool}
325
326def cf_zero(w, h, shown, q, sh, on, z):
327 match q:
328 case T.Pos{x, y}:
329 PL.count_false_zero(w, h, shown, x, y, sh, on, Equal.sym(Nat, 0n, B.count_false(shown), z))
330
331
332
333
334def flood_work.skip(+n: Nat, +c: T.Pos, +rest: List<&2, G.Work>, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
335 +shown: T.Grid(Bool), +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
336 he: {G.unrevealed(w, h, shown, c) == False{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool},
337 m: {Bool.or(b, wcontains(rest, q)) == True{} : Bool},
338 ih: {wcontains(rest, q) == True{} : Bool} ->
339 {B.at(Bool, False{}, G.flood(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown), q) == True{} : Bool}) ->
340 {B.at(Bool, False{}, G.flood(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown), q) == True{} : Bool}:
341 match b:
342 case True{}:
343 +cq = PG.same_sound(c, q, be)
344 flood_mono(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, q,
345 unrev_shown(w, h, shown, q, %cq : {G.unrevealed(w, h, shown, _) == False{} : Bool}; he, on))
346 case False{}:
347 ih(m)
348
349def flood_work.take(+m: Nat, +c: T.Pos, +wk: List<&2, G.Work>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
350 +layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos,
351 +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
352 he: {G.unrevealed(w, h, shown, c) == True{} : Bool},
353 keep: {wcontains(rest, q) == True{} : Bool} -> {wcontains(wk, q) == True{} : Bool},
354 +b: Bool, be: {B.same(c, q) == b : Bool}, m2: {Bool.or(b, wcontains(rest, q)) == True{} : Bool},
355 ih: {wcontains(wk, q) == True{} : Bool} ->
356 {B.at(Bool, False{}, G.flood(m, wk, G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), wk), w, h, layout,
357 B.set_at(Bool, shown, c, True{})), q) == True{} : Bool}) ->
358 {B.at(Bool, False{}, G.flood(m, wk, G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), wk), w, h, layout,
359 B.set_at(Bool, shown, c, True{})), q) == True{} : Bool}:
360 match b:
361 case True{}:
362 +cq = PG.same_sound(c, q, be)
363 +s2 = B.set_at(Bool, shown, c, True{})
364 flood_mono(m, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2, q,
365 %cq : {B.at(Bool, False{}, s2, _) == True{} : Bool};
366 at_set_on(w, h, shown, c, sh, unrev_on(w, h, shown, c, he)))
367 case False{}:
368 ih(keep(m2))
369
370
371
372law flood_work:
373 for +n: Nat
374 for +work: List<&2, G.Work>
375 for +hd: Bool
376 for +w: Nat
377 for +h: Nat
378 for +layout: T.Grid(Bool)
379 for +shown: T.Grid(Bool)
380 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
381 for +cnt: {n == B.count_false(shown) : Nat}
382 for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
383 for +q: T.Pos
384 for +on: {B.on_board(w, h, q) == True{} : Bool}
385 for m: {wcontains(work, q) == True{} : Bool}
386 {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
387
388def flood_work(n, work, hd, w, h, layout, shown, sh, cnt, he, q, on, m):
389 match n:
390 case 0n:
391 cf_zero(w, h, shown, q, sh, on, cnt)
392 case 1n+k:
393 match work:
394 case Nil{}:
395 Empty.absurd({B.at(Bool, False{}, shown, q) == True{} : Bool}, P.false_ne_true(m))
396 case G.Work{c, back} <> rest:
397 match hd:
398 case False{}:
399 flood_work.skip(n, c, rest, w, h, layout, shown, q, on, he, B.same(c, q), {==}, m,
400 mr => flood_work(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, sh, cnt, {==},
401 q, on, mr))
402 case True{}:
403 +s2 = B.set_at(Bool, shown, c, True{})
404 +z = B.zero(w, h, layout, c)
405 +ns = B.neighbours(w, h, c)
406 +wk = G.push(z, ns, back, rest)
407 flood_work.take(k, c, wk, rest, w, h, layout, shown, q, sh, he,
408 mr => push_keeps(z, ns, back, rest, q, mr), B.same(c, q), {==}, m,
409 mw => flood_work(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
410 PL.shaped_set(Bool, w, h, shown, c, True{}, sh), count_after(w, h, shown, c, k, sh, he, cnt),
411 {==}, q, on, mw))
412
413
414
415
416def both_absurd(-A: Type, +a: Bool, e1: {a == False{} : Bool}, e2: {a == True{} : Bool}) -> A:
417 Empty.absurd(A, P.false_ne_true(Equal.trans(Bool, False{}, a, True{}, Equal.sym(Bool, a, False{}, e1), e2)))
418
419def flood_zero.take(+k: Nat, +c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
420 +layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +r: T.Pos,
421 +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
422 +cnt: {1n+k == B.count_false(shown) : Nat},
423 +he: {G.unrevealed(w, h, shown, c) == True{} : Bool},
424 before: {B.at(Bool, False{}, shown, q) == False{} : Bool},
425 z: {B.zero(w, h, layout, q) == True{} : Bool},
426 +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool},
427 +b: Bool, +be: {B.same(c, q) == b : Bool},
428 ih: {B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q) == False{} : Bool} ->
429 {B.at(Bool, False{}, G.flood(k, G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest),
430 G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)),
431 w, h, layout, B.set_at(Bool, shown, c, True{})), r) == True{} : Bool}) ->
432 {B.at(Bool, False{}, G.flood(k, G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest),
433 G.head_hidden(w, h, B.set_at(Bool, shown, c, True{}), G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)),
434 w, h, layout, B.set_at(Bool, shown, c, True{})), r) == True{} : Bool}:
435 match b:
436 case True{}:
437 %Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) :
438 {B.at(Bool, False{}, G.flood(k, G.push(B.zero(w, h, layout, _), B.neighbours(w, h, _), back, rest),
439 G.head_hidden(w, h, B.set_at(Bool, shown, _, True{}), G.push(B.zero(w, h, layout, _), B.neighbours(w, h, _), back, rest)),
440 w, h, layout, B.set_at(Bool, shown, _, True{})), r) == True{} : Bool}
441 %Equal.sym(Bool, B.zero(w, h, layout, q), True{}, z) :
442 {B.at(Bool, False{}, G.flood(k, G.push(_, B.neighbours(w, h, q), back, rest),
443 G.head_hidden(w, h, B.set_at(Bool, shown, q, True{}), G.push(_, B.neighbours(w, h, q), back, rest)),
444 w, h, layout, B.set_at(Bool, shown, q, True{})), r) == True{} : Bool}
445 +s2 = B.set_at(Bool, shown, q, True{})
446 +wk = List.append(&2, G.Work, G.works(B.neighbours(w, h, q), back), rest)
447 +hq = {%PG.same_sound(c, q, be) : {G.unrevealed(w, h, shown, _) == True{} : Bool};
448 he : {G.unrevealed(w, h, shown, q) == True{} : Bool}}
449 +ron = P.and_true_r(B.adjacent(q, r), B.on_board(w, h, r),
450 PS.allp_member(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, B.neighbours(w, h, q), r,
451 PS.neighbours_all(w, h, q), rm))
452 flood_work(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
453 PL.shaped_set(Bool, w, h, shown, q, True{}, sh), count_after(w, h, shown, q, k, sh, hq, cnt), {==}, r, ron,
454 wcontains_append_l(G.works(B.neighbours(w, h, q), back), rest, r,
455 wcontains_works(B.neighbours(w, h, q), back, r, rm)))
456 case False{}:
457 ih(%Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q), B.at(Bool, False{}, shown, q),
458 PL.at_set_ne(Bool, shown, c, q, True{}, False{}, be)) : {_ == False{} : Bool}; before)
459
460law flood_zero:
461 for +n: Nat
462 for +work: List<&2, G.Work>
463 for +hd: Bool
464 for +w: Nat
465 for +h: Nat
466 for +layout: T.Grid(Bool)
467 for +shown: T.Grid(Bool)
468 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
469 for +cnt: {n == B.count_false(shown) : Nat}
470 for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
471 for +q: T.Pos
472 for +before: {B.at(Bool, False{}, shown, q) == False{} : Bool}
473 for +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
474 for +z: {B.zero(w, h, layout, q) == True{} : Bool}
475 for +r: T.Pos
476 for +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}
477 {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), r) == True{} : Bool}
478
479def flood_zero(n, work, hd, w, h, layout, shown, sh, cnt, he, q, before, after, z, r, rm):
480 match n:
481 case 0n:
482 both_absurd({B.at(Bool, False{}, shown, r) == True{} : Bool}, B.at(Bool, False{}, shown, q), before, after)
483 case 1n+k:
484 match work:
485 case Nil{}:
486 both_absurd({B.at(Bool, False{}, shown, r) == True{} : Bool}, B.at(Bool, False{}, shown, q), before, after)
487 case G.Work{c, back} <> rest:
488 match hd:
489 case False{}:
490 flood_zero(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, sh, cnt, {==}, q,
491 before, after, z, r, rm)
492 case True{}:
493 +s2 = B.set_at(Bool, shown, c, True{})
494 +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
495 flood_zero.take(k, c, back, rest, w, h, layout, shown, q, r, sh, cnt, he, before, z, rm,
496 B.same(c, q), {==},
497 b2 => flood_zero(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2,
498 PL.shaped_set(Bool, w, h, shown, c, True{}, sh), count_after(w, h, shown, c, k, sh, he, cnt),
499 {==}, q, b2, after, z, r, rm))
500
501
502
503
504
505def works_ok(ws: List<&2, G.Work>, +w: Nat, +h: Nat, +layout: T.Grid(Bool), +p0: T.Pos) -> Bool:
506 match ws:
507 case Nil{}:
508 True{}
509 case G.Work{c, back} <> t:
510 L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) && works_ok(t, w, h, layout, p0)
511
512law works_ok_append:
513 for +xs: List<&2, G.Work>
514 for +ys: List<&2, G.Work>
515 for +w: Nat
516 for +h: Nat
517 for +layout: T.Grid(Bool)
518 for +p0: T.Pos
519 for +a: {works_ok(xs, w, h, layout, p0) == True{} : Bool}
520 for b: {works_ok(ys, w, h, layout, p0) == True{} : Bool}
521 {works_ok(List.append(&2, G.Work, xs, ys), w, h, layout, p0) == True{} : Bool}
522
523def works_ok_append(xs, ys, w, h, layout, p0, a, b):
524 match xs:
525 case Nil{}:
526 b
527 case G.Work{c, back} <> t:
528 +hd = L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c)
529 %Equal.sym(Bool, hd, True{}, P.and_true_l(hd, works_ok(t, w, h, layout, p0), a)) :
530 {Bool.and(_, works_ok(List.append(&2, G.Work, t, ys), w, h, layout, p0)) == True{} : Bool}
531 works_ok_append(t, ys, w, h, layout, p0, P.and_true_r(hd, works_ok(t, w, h, layout, p0), a), b)
532
533law works_ok_works:
534 for +ns: List<&2, T.Pos>
535 for +back: List<&2, T.Pos>
536 for +c: T.Pos
537 for +w: Nat
538 for +h: Nat
539 for +layout: T.Grid(Bool)
540 for +p0: T.Pos
541 for +okc: {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) == True{} : Bool}
542 for +zc: {L.zero(w, h, layout, c) == True{} : Bool}
543 for +adj: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, c}, ns) == True{} : Bool}
544 {works_ok(G.works(ns, back), w, h, layout, p0) == True{} : Bool}
545
546def works_ok_works(ns, back, c, w, h, layout, p0, okc, zc, adj):
547 match ns:
548 case Nil{}:
549 {==}
550 case r <> t:
551 +ar = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, c}, r, t, adj)
552 +a1 = P.and_true_l(B.adjacent(c, r), B.on_board(w, h, r), ar)
553 +a2 = P.and_true_r(B.adjacent(c, r), B.on_board(w, h, r), ar)
554 +wr = PW.walk_snoc(List.reverse(&2, T.Pos, back), w, h, layout, p0, c, r, okc, zc,
555 %PC.adjacent_eq(c, r) : {_ == True{} : Bool}; a1,
556 %PC.on_board_eq(w, h, r) : {_ == True{} : Bool}; a2)
557 %Equal.sym(Bool, L.zero_walk(List.reverse(&2, T.Pos, r <> back), w, h, layout, p0, r), True{},
558 %Equal.sym(List<&2, T.Pos>, List.reverse(&2, T.Pos, r <> back),
559 List.append(&2, T.Pos, List.reverse(&2, T.Pos, back), [r]), PW.rev_cons(T.Pos, r, back)) :
560 {L.zero_walk(_, w, h, layout, p0, r) == True{} : Bool}; wr) :
561 {Bool.and(_, works_ok(G.works(t, back), w, h, layout, p0)) == True{} : Bool}
562 works_ok_works(t, back, c, w, h, layout, p0, okc, zc,
563 PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, c}, r, t, adj))
564
565def works_ok_push(+z: Bool, +c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
566 +layout: T.Grid(Bool), +p0: T.Pos, ze: {B.zero(w, h, layout, c) == z : Bool},
567 okc: {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) == True{} : Bool},
568 okr: {works_ok(rest, w, h, layout, p0) == True{} : Bool}) ->
569 {works_ok(G.push(z, B.neighbours(w, h, c), back, rest), w, h, layout, p0) == True{} : Bool}:
570 match z:
571 case True{}:
572 works_ok_append(G.works(B.neighbours(w, h, c), back), rest, w, h, layout, p0,
573 works_ok_works(B.neighbours(w, h, c), back, c, w, h, layout, p0, okc,
574 %PC.zero_eq(w, h, layout, c) : {_ == True{} : Bool}; ze,
575 PS.neighbours_all(w, h, c)), okr)
576 case False{}:
577 okr
578
579def Walk(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p0: T.Pos, +q: T.Pos) -> Type:
580 Exists(List<&2, T.Pos>, path => {L.zero_walk(path, w, h, layout, p0, q) == True{} : Bool})
581
582def flood_path.take(+c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
583 +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p0: T.Pos, +q: T.Pos,
584 +ok: {Bool.and(L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c), works_ok(rest, w, h, layout, p0)) == True{} : Bool},
585 before: {B.at(Bool, False{}, shown, q) == False{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool},
586 ih: {works_ok(G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest), w, h, layout, p0) == True{} : Bool} ->
587 {B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q) == False{} : Bool} -> Walk(w, h, layout, p0, q)) ->
588 Walk(w, h, layout, p0, q):
589 match b:
590 case True{}:
591 +hd = L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c)
592 +okc = P.and_true_l(hd, works_ok(rest, w, h, layout, p0), ok)
593 (List.reverse(&2, T.Pos, back),
594 %PG.same_sound(c, q, be) : {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, _) == True{} : Bool};
595 okc)
596 case False{}:
597 +hd = L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c)
598 +okc = P.and_true_l(hd, works_ok(rest, w, h, layout, p0), ok)
599 ih(works_ok_push(B.zero(w, h, layout, c), c, back, rest, w, h, layout, p0, {==}, okc,
600 P.and_true_r(hd, works_ok(rest, w, h, layout, p0), ok)),
601 %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, c, True{}), q), B.at(Bool, False{}, shown, q),
602 PL.at_set_ne(Bool, shown, c, q, True{}, False{}, be)) : {_ == False{} : Bool}; before)
603
604law flood_path:
605 for +n: Nat
606 for +work: List<&2, G.Work>
607 for +hd: Bool
608 for +w: Nat
609 for +h: Nat
610 for +layout: T.Grid(Bool)
611 for +shown: T.Grid(Bool)
612 for +p0: T.Pos
613 for +ok: {works_ok(work, w, h, layout, p0) == True{} : Bool}
614 for +q: T.Pos
615 for +before: {B.at(Bool, False{}, shown, q) == False{} : Bool}
616 for +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
617 Walk(w, h, layout, p0, q)
618
619def flood_path(n, work, hd, w, h, layout, shown, p0, ok, q, before, after):
620 match n:
621 case 0n:
622 both_absurd(Walk(w, h, layout, p0, q), B.at(Bool, False{}, shown, q), before, after)
623 case 1n+k:
624 match work:
625 case Nil{}:
626 both_absurd(Walk(w, h, layout, p0, q), B.at(Bool, False{}, shown, q), before, after)
627 case G.Work{c, back} <> rest:
628 match hd:
629 case False{}:
630 flood_path(n, rest, G.head_hidden(w, h, shown, rest), w, h, layout, shown, p0,
631 P.and_true_r(L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c),
632 works_ok(rest, w, h, layout, p0), ok), q, before, after)
633 case True{}:
634 +s2 = B.set_at(Bool, shown, c, True{})
635 +wk = G.push(B.zero(w, h, layout, c), B.neighbours(w, h, c), back, rest)
636 flood_path.take(c, back, rest, w, h, layout, shown, p0, q, ok, before, B.same(c, q), {==},
637 okw => b2 => flood_path(k, wk, G.head_hidden(w, h, s2, wk), w, h, layout, s2, p0, okw, q, b2, after))