proof_speed.bend

minebender-game@1.0.0.0 · 541 lines · 31 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/solver.bend as S
5import minebender-game@1.0.0.0/proof_base.bend as P
6import minebender-game@1.0.0.0/proof_lists.bend as PL
7import minebender-game@1.0.0.0/proof_cells.bend as PS
8
9# The counting search answers exactly as the plain one: dfs2, which carries
10# the mines and unassigned cells of the partial layout, returns what dfs
11# returns, as long as the counts start right and every cell it assigns is
12# on the board.
13
14# Counting after an assignment
15# ============================
16
17law row_none_set:
18  for +r: List<&2, Maybe<&2, Bool>>
19  for +x: Nat
20  for +b: Bool
21  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
22  {S.row_none(r) == 1n+S.row_none(List.set(&2, Maybe<&2, Bool>, r, x, Some{b})) : Nat}
23
24def row_none_set(r, x, b, e):
25  match r x:
26    case Nil{} _:
27      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(Maybe<&2, Bool>, None{}, e))
28    case m <> t 0n:
29      %Equal.sym(Maybe<&2, Bool>, m, None{}, PL.some_inj(Maybe<&2, Bool>, m, None{}, e)) :
30        {Nat.add(S.one_if(S.is_none(_)), S.row_none(t)) == 1n+Nat.add(S.one_if(S.is_none(Some{b})), S.row_none(t)) : Nat}
31      {==}
32    case m <> t 1n+k:
33      %Equal.sym(Nat, S.row_none(t), 1n+S.row_none(List.set(&2, Maybe<&2, Bool>, t, k, Some{b})), row_none_set(t, k, b, e)) :
34        {Nat.add(S.one_if(S.is_none(m)), _)
35          == 1n+Nat.add(S.one_if(S.is_none(m)), S.row_none(List.set(&2, Maybe<&2, Bool>, t, k, Some{b}))) : Nat}
36      P.add_succ(S.one_if(S.is_none(m)), S.row_none(List.set(&2, Maybe<&2, Bool>, t, k, Some{b})))
37
38law row_true_set_t:
39  for +r: List<&2, Maybe<&2, Bool>>
40  for +x: Nat
41  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
42  {S.row_true(List.set(&2, Maybe<&2, Bool>, r, x, Some{True{}})) == 1n+S.row_true(r) : Nat}
43
44def row_true_set_t(r, x, e):
45  match r x:
46    case Nil{} _:
47      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(Maybe<&2, Bool>, None{}, e))
48    case m <> t 0n:
49      %Equal.sym(Maybe<&2, Bool>, m, None{}, PL.some_inj(Maybe<&2, Bool>, m, None{}, e)) :
50        {Nat.add(S.one_if(S.is_true(Some{True{}})), S.row_true(t)) == 1n+Nat.add(S.one_if(S.is_true(_)), S.row_true(t)) : Nat}
51      {==}
52    case m <> t 1n+k:
53      %Equal.sym(Nat, S.row_true(List.set(&2, Maybe<&2, Bool>, t, k, Some{True{}})), 1n+S.row_true(t), row_true_set_t(t, k, e)) :
54        {Nat.add(S.one_if(S.is_true(m)), _) == 1n+Nat.add(S.one_if(S.is_true(m)), S.row_true(t)) : Nat}
55      P.add_succ(S.one_if(S.is_true(m)), S.row_true(t))
56
57law row_true_set_f:
58  for +r: List<&2, Maybe<&2, Bool>>
59  for +x: Nat
60  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
61  {S.row_true(List.set(&2, Maybe<&2, Bool>, r, x, Some{False{}})) == S.row_true(r) : Nat}
62
63def row_true_set_f(r, x, e):
64  match r x:
65    case Nil{} _:
66      Empty.absurd({0n == 0n : Nat}, PL.none_ne_some(Maybe<&2, Bool>, None{}, e))
67    case m <> t 0n:
68      %Equal.sym(Maybe<&2, Bool>, m, None{}, PL.some_inj(Maybe<&2, Bool>, m, None{}, e)) :
69        {Nat.add(S.one_if(S.is_true(Some{False{}})), S.row_true(t)) == Nat.add(S.one_if(S.is_true(_)), S.row_true(t)) : Nat}
70      {==}
71    case m <> t 1n+k:
72      %Equal.sym(Nat, S.row_true(List.set(&2, Maybe<&2, Bool>, t, k, Some{False{}})), S.row_true(t), row_true_set_f(t, k, e)) :
73        {Nat.add(S.one_if(S.is_true(m)), _) == Nat.add(S.one_if(S.is_true(m)), S.row_true(t)) : Nat}
74      {==}
75
76law none_go:
77  for +g: T.Grid(Maybe<&2, Bool>)
78  for +y: Nat
79  for +r: List<&2, Maybe<&2, Bool>>
80  for +r2: List<&2, Maybe<&2, Bool>>
81  for e: {List.get(&2, List<&2, Maybe<&2, Bool>>, g, y) == Some{r} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}
82  for rf: {S.row_none(r) == 1n+S.row_none(r2) : Nat}
83  {S.part_none(g) == 1n+S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, g, y, r2)) : Nat}
84
85def none_go(g, y, r, r2, e, rf):
86  match g y:
87    case Nil{} _:
88      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(List<&2, Maybe<&2, Bool>>, r, e))
89    case row <> t 0n:
90      %Equal.sym(List<&2, Maybe<&2, Bool>>, row, r, PL.some_inj(List<&2, Maybe<&2, Bool>>, row, r, e)) :
91        {Nat.add(S.row_none(_), S.part_none(t)) == 1n+Nat.add(S.row_none(r2), S.part_none(t)) : Nat}
92      %Equal.sym(Nat, S.row_none(r), 1n+S.row_none(r2), rf) :
93        {Nat.add(_, S.part_none(t)) == 1n+Nat.add(S.row_none(r2), S.part_none(t)) : Nat}
94      {==}
95    case row <> t 1n+k:
96      %Equal.sym(Nat, S.part_none(t), 1n+S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)), none_go(t, k, r, r2, e, rf)) :
97        {Nat.add(S.row_none(row), _)
98          == 1n+Nat.add(S.row_none(row), S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2))) : Nat}
99      P.add_succ(S.row_none(row), S.part_none(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)))
100
101law true_go_t:
102  for +g: T.Grid(Maybe<&2, Bool>)
103  for +y: Nat
104  for +r: List<&2, Maybe<&2, Bool>>
105  for +r2: List<&2, Maybe<&2, Bool>>
106  for e: {List.get(&2, List<&2, Maybe<&2, Bool>>, g, y) == Some{r} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}
107  for rf: {S.row_true(r2) == 1n+S.row_true(r) : Nat}
108  {S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, g, y, r2)) == 1n+S.part_true(g) : Nat}
109
110def true_go_t(g, y, r, r2, e, rf):
111  match g y:
112    case Nil{} _:
113      Empty.absurd({0n == 1n+0n : Nat}, PL.none_ne_some(List<&2, Maybe<&2, Bool>>, r, e))
114    case row <> t 0n:
115      %Equal.sym(List<&2, Maybe<&2, Bool>>, row, r, PL.some_inj(List<&2, Maybe<&2, Bool>>, row, r, e)) :
116        {Nat.add(S.row_true(r2), S.part_true(t)) == 1n+Nat.add(S.row_true(_), S.part_true(t)) : Nat}
117      %Equal.sym(Nat, S.row_true(r2), 1n+S.row_true(r), rf) :
118        {Nat.add(_, S.part_true(t)) == 1n+Nat.add(S.row_true(r), S.part_true(t)) : Nat}
119      {==}
120    case row <> t 1n+k:
121      %Equal.sym(Nat, S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)), 1n+S.part_true(t), true_go_t(t, k, r, r2, e, rf)) :
122        {Nat.add(S.row_true(row), _) == 1n+Nat.add(S.row_true(row), S.part_true(t)) : Nat}
123      P.add_succ(S.row_true(row), S.part_true(t))
124
125law true_go_f:
126  for +g: T.Grid(Maybe<&2, Bool>)
127  for +y: Nat
128  for +r: List<&2, Maybe<&2, Bool>>
129  for +r2: List<&2, Maybe<&2, Bool>>
130  for e: {List.get(&2, List<&2, Maybe<&2, Bool>>, g, y) == Some{r} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}
131  for rf: {S.row_true(r2) == S.row_true(r) : Nat}
132  {S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, g, y, r2)) == S.part_true(g) : Nat}
133
134def true_go_f(g, y, r, r2, e, rf):
135  match g y:
136    case Nil{} _:
137      Empty.absurd({0n == 0n : Nat}, PL.none_ne_some(List<&2, Maybe<&2, Bool>>, r, e))
138    case row <> t 0n:
139      %Equal.sym(List<&2, Maybe<&2, Bool>>, row, r, PL.some_inj(List<&2, Maybe<&2, Bool>>, row, r, e)) :
140        {Nat.add(S.row_true(r2), S.part_true(t)) == Nat.add(S.row_true(_), S.part_true(t)) : Nat}
141      %Equal.sym(Nat, S.row_true(r2), S.row_true(r), rf) :
142        {Nat.add(_, S.part_true(t)) == Nat.add(S.row_true(r), S.part_true(t)) : Nat}
143      {==}
144    case row <> t 1n+k:
145      %Equal.sym(Nat, S.part_true(List.set(&2, List<&2, Maybe<&2, Bool>>, t, k, r2)), S.part_true(t), true_go_f(t, k, r, r2, e, rf)) :
146        {Nat.add(S.row_true(row), _) == Nat.add(S.row_true(row), S.part_true(t)) : Nat}
147      {==}
148
149# The row of an unassigned cell, and the cell in it.
150def cell_none(+w: Nat, +h: Nat, +part: T.Grid(Maybe<&2, Bool>), +x: Nat, +y: Nat,
151  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
152  fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}) ->
153  {List.get(&2, Maybe<&2, Bool>, PL.row_of(Maybe<&2, Bool>, part, y), x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}:
154  +xw = P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
155  +yh = P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
156  +row = PL.row_of(Maybe<&2, Bool>, part, y)
157  +xl = {%Equal.sym(Nat, List.length(&2, Maybe<&2, Bool>, row), w, PL.row_in_len(Maybe<&2, Bool>, w, h, part, y, sh, yh)) :
158    {Nat.is_lt(x, _) == True{} : Bool};
159    xw : {Nat.is_lt(x, List.length(&2, Maybe<&2, Bool>, row)) == True{} : Bool}}
160  %fr : {List.get(&2, Maybe<&2, Bool>, row, x) == Some{_} : Maybe<&2, Maybe<&2, Bool>>}
161  PL.get_in(Maybe<&2, Bool>, row, x, None{}, xl)
162
163def row_get(+w: Nat, +h: Nat, +part: T.Grid(Maybe<&2, Bool>), +x: Nat, +y: Nat,
164  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}) ->
165  {List.get(&2, List<&2, Maybe<&2, Bool>>, part, y) == Some{PL.row_of(Maybe<&2, Bool>, part, y)} : Maybe<&2, List<&2, Maybe<&2, Bool>>>}:
166  PL.row_in_get(Maybe<&2, Bool>, w, h, part, y, sh, P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on))
167
168# Assigning an unassigned cell of the board uses up one unassigned cell...
169law none_set:
170  for +w: Nat
171  for +h: Nat
172  for +part: T.Grid(Maybe<&2, Bool>)
173  for +x: Nat
174  for +y: Nat
175  for +b: Bool
176  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
177  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
178  for +fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}
179  {S.part_none(part) == 1n+S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{b})) : Nat}
180
181def none_set(w, h, part, x, y, b, sh, on, fr):
182  +row = PL.row_of(Maybe<&2, Bool>, part, y)
183  none_go(part, y, row, List.set(&2, Maybe<&2, Bool>, row, x, Some{b}), row_get(w, h, part, x, y, sh, on),
184    row_none_set(row, x, b, cell_none(w, h, part, x, y, sh, on, fr)))
185
186# ... and adds a mine when it places one ...
187law true_set_t:
188  for +w: Nat
189  for +h: Nat
190  for +part: T.Grid(Maybe<&2, Bool>)
191  for +x: Nat
192  for +y: Nat
193  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
194  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
195  for +fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}
196  {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == 1n+S.part_true(part) : Nat}
197
198def true_set_t(w, h, part, x, y, sh, on, fr):
199  +row = PL.row_of(Maybe<&2, Bool>, part, y)
200  true_go_t(part, y, row, List.set(&2, Maybe<&2, Bool>, row, x, Some{True{}}), row_get(w, h, part, x, y, sh, on),
201    row_true_set_t(row, x, cell_none(w, h, part, x, y, sh, on, fr)))
202
203# ... and none otherwise.
204law true_set_f:
205  for +w: Nat
206  for +h: Nat
207  for +part: T.Grid(Maybe<&2, Bool>)
208  for +x: Nat
209  for +y: Nat
210  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
211  for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
212  for +fr: {S.look(part, T.Pos{x, y}) == None{} : Maybe<&2, Bool>}
213  {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == S.part_true(part) : Nat}
214
215def true_set_f(w, h, part, x, y, sh, on, fr):
216  +row = PL.row_of(Maybe<&2, Bool>, part, y)
217  true_go_f(part, y, row, List.set(&2, Maybe<&2, Bool>, row, x, Some{False{}}), row_get(w, h, part, x, y, sh, on),
218    row_true_set_f(row, x, cell_none(w, h, part, x, y, sh, on, fr)))
219
220# Lists of todos
221# ==============
222
223# Every todo of ts passes f (with e for f's context).
224def tall(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, ts: List<&2, S.Todo>) -> Bool:
225  match ts:
226    case Nil{}:
227      True{}
228    case t <> rest:
229      f(e, t) && tall(~E, ~f, e, rest)
230
231def tall_head(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +t: S.Todo, +rest: List<&2, S.Todo>,
232  h: {tall(~E, ~f, e, t <> rest) == True{} : Bool}) -> {f(e, t) == True{} : Bool}:
233  P.and_true_l(f(e, t), tall(~E, ~f, e, rest), h)
234
235def tall_tail(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +t: S.Todo, +rest: List<&2, S.Todo>,
236  h: {tall(~E, ~f, e, t <> rest) == True{} : Bool}) -> {tall(~E, ~f, e, rest) == True{} : Bool}:
237  P.and_true_r(f(e, t), tall(~E, ~f, e, rest), h)
238
239def tall_cons(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +t: S.Todo, +rest: List<&2, S.Todo>,
240  a: {f(e, t) == True{} : Bool}, b: {tall(~E, ~f, e, rest) == True{} : Bool}) ->
241  {tall(~E, ~f, e, t <> rest) == True{} : Bool}:
242  %Equal.sym(Bool, tall(~E, ~f, e, rest), True{}, b) : {Bool.and(f(e, t), _) == True{} : Bool}
243  %Equal.sym(Bool, f(e, t), True{}, a) : {Bool.and(_, True{}) == True{} : Bool}
244  {==}
245
246def tall_put(~E: Data, ~f: E -> S.Todo -> Bool, +e: E, +b: Bool, +t: S.Todo, +rest: List<&2, S.Todo>,
247  a: {f(e, t) == True{} : Bool}, r: {tall(~E, ~f, e, rest) == True{} : Bool}) ->
248  {tall(~E, ~f, e, List.filter.put(S.Todo, t, rest, b)) == True{} : Bool}:
249  match b:
250    case False{}:
251      r
252    case True{}:
253      tall_cons(~E, ~f, e, t, rest, a, r)
254
255law tall_append:
256  for ~E: Data
257  for ~f: E -> S.Todo -> Bool
258  for +e: E
259  for +xs: List<&2, S.Todo>
260  for +ys: List<&2, S.Todo>
261  for +a: {tall(~E, ~f, e, xs) == True{} : Bool}
262  for b: {tall(~E, ~f, e, ys) == True{} : Bool}
263  {tall(~E, ~f, e, List.append(&2, S.Todo, xs, ys)) == True{} : Bool}
264
265def tall_append(E, f, e, xs, ys, a, b):
266  match xs:
267    case Nil{}:
268      b
269    case t <> rest:
270      tall_cons(~E, ~f, e, t, List.append(&2, S.Todo, rest, ys), tall_head(~E, ~f, e, t, rest, a),
271        tall_append(~E, ~f, e, rest, ys, tall_tail(~E, ~f, e, t, rest, a), b))
272
273law tall_nears:
274  for ~E: Data
275  for ~f: E -> S.Todo -> Bool
276  for +e: E
277  for +ts: List<&2, S.Todo>
278  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
279  {tall(~E, ~f, e, S.nears(ts)) == True{} : Bool}
280
281def tall_nears(E, f, e, ts, a):
282  match ts:
283    case Nil{}:
284      {==}
285    case +t <> +rest:
286      tall_put(~E, ~f, e, S.has_rel(t), t, S.nears(rest), tall_head(~E, ~f, e, t, rest, a),
287        tall_nears(~E, ~f, e, rest, tall_tail(~E, ~f, e, t, rest, a)))
288
289law tall_fars:
290  for ~E: Data
291  for ~f: E -> S.Todo -> Bool
292  for +e: E
293  for +ts: List<&2, S.Todo>
294  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
295  {tall(~E, ~f, e, S.fars(ts)) == True{} : Bool}
296
297def tall_fars(E, f, e, ts, a):
298  match ts:
299    case Nil{}:
300      {==}
301    case +t <> +rest:
302      tall_put(~E, ~f, e, Bool.not(S.has_rel(t)), t, S.fars(rest), tall_head(~E, ~f, e, t, rest, a),
303        tall_fars(~E, ~f, e, rest, tall_tail(~E, ~f, e, t, rest, a)))
304
305law tall_with_c:
306  for ~E: Data
307  for ~f: E -> S.Todo -> Bool
308  for +e: E
309  for +ts: List<&2, S.Todo>
310  for +q: T.Pos
311  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
312  {tall(~E, ~f, e, S.with_c(ts, q)) == True{} : Bool}
313
314def tall_with_c(E, f, e, ts, q, a):
315  match ts:
316    case Nil{}:
317      {==}
318    case +t <> +rest:
319      tall_put(~E, ~f, e, B.same(S.todo_c(t), q), t, S.with_c(rest, q), tall_head(~E, ~f, e, t, rest, a),
320        tall_with_c(~E, ~f, e, rest, q, tall_tail(~E, ~f, e, t, rest, a)))
321
322law tall_gather:
323  for ~E: Data
324  for ~f: E -> S.Todo -> Bool
325  for +e: E
326  for +qs: List<&2, T.Pos>
327  for +ts: List<&2, S.Todo>
328  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
329  {tall(~E, ~f, e, S.gather(qs, ts)) == True{} : Bool}
330
331def tall_gather(E, f, e, qs, ts, a):
332  match qs:
333    case Nil{}:
334      {==}
335    case q <> t:
336      tall_append(~E, ~f, e, S.with_c(ts, q), S.gather(t, ts), tall_with_c(~E, ~f, e, ts, q, a),
337        tall_gather(~E, ~f, e, t, ts, a))
338
339law tall_drop:
340  for ~E: Data
341  for ~f: E -> S.Todo -> Bool
342  for +e: E
343  for +ts: List<&2, S.Todo>
344  for +k: Nat
345  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
346  {tall(~E, ~f, e, List.drop(&2, S.Todo, ts, k)) == True{} : Bool}
347
348def tall_drop(E, f, e, ts, k, a):
349  match ts k:
350    case Nil{} _:
351      {==}
352    case t <> rest 0n:
353      a
354    case t <> rest 1n+j:
355      tall_drop(~E, ~f, e, rest, j, tall_tail(~E, ~f, e, t, rest, a))
356
357law tall_take:
358  for ~E: Data
359  for ~f: E -> S.Todo -> Bool
360  for +e: E
361  for +ts: List<&2, S.Todo>
362  for +k: Nat
363  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
364  {tall(~E, ~f, e, List.take(&2, S.Todo, ts, k)) == True{} : Bool}
365
366def tall_take(E, f, e, ts, k, a):
367  match ts k:
368    case Nil{} _:
369      {==}
370    case t <> rest 0n:
371      {==}
372    case t <> rest 1n+j:
373      tall_cons(~E, ~f, e, t, List.take(&2, S.Todo, rest, j), tall_head(~E, ~f, e, t, rest, a),
374        tall_take(~E, ~f, e, rest, j, tall_tail(~E, ~f, e, t, rest, a)))
375
376# The order of every search passes whatever the cells of a solve pass.
377law tall_plan:
378  for ~E: Data
379  for ~f: E -> S.Todo -> Bool
380  for +e: E
381  for +ts: List<&2, S.Todo>
382  for +qs: List<&2, T.Pos>
383  for +k: Nat
384  for +a: {tall(~E, ~f, e, ts) == True{} : Bool}
385  {tall(~E, ~f, e, List.append(&2, S.Todo, S.gather(qs, S.nears(ts)),
386    List.append(&2, S.Todo, S.rot(S.fars(ts), k), S.order(ts)))) == True{} : Bool}
387
388def tall_plan(E, f, e, ts, qs, k, a):
389  +an = tall_nears(~E, ~f, e, ts, a)
390  +af = tall_fars(~E, ~f, e, ts, a)
391  +far = S.fars(ts)
392  tall_append(~E, ~f, e, S.gather(qs, S.nears(ts)), List.append(&2, S.Todo, S.rot(far, k), S.order(ts)),
393    tall_gather(~E, ~f, e, qs, S.nears(ts), an),
394    tall_append(~E, ~f, e, S.rot(far, k), S.order(ts),
395      tall_append(~E, ~f, e, List.drop(&2, S.Todo, far, k), List.take(&2, S.Todo, far, k),
396        tall_drop(~E, ~f, e, far, k, af), tall_take(~E, ~f, e, far, k, af)),
397      tall_append(~E, ~f, e, S.nears(ts), far, an, af)))
398
399# Todos on the board
400# ==================
401
402def con_f(e: PS.WH, t: S.Todo) -> Bool:
403  match t:
404    case S.Todo{c, rel}:
405      PS.onb(e, c)
406
407# The todos of cells on the board are on the board.
408law con_todos:
409  for +w: Nat
410  for +h: Nat
411  for +its: List<&2, S.Item>
412  for +cs: List<&2, T.Pos>
413  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, cs) == True{} : Bool}
414  {tall(~PS.WH, ~con_f, PS.WH{w, h}, S.todos(its, cs)) == True{} : Bool}
415
416def con_todos(w, h, its, cs, on):
417  match cs:
418    case Nil{}:
419      {==}
420    case +c <> +t:
421      tall_cons(~PS.WH, ~con_f, PS.WH{w, h}, S.Todo{c, S.around(its, c)}, S.todos(its, t),
422        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, c, t, on),
423        con_todos(w, h, its, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, c, t, on)))
424
425# The counting search
426# ===================
427
428def none_of(m: Maybe<&2, Bool>, e: {S.is_none(m) == True{} : Bool}) -> {m == None{} : Maybe<&2, Bool>}:
429  match m:
430    case Some{b}:
431      Empty.absurd({Some{b} == None{} : Maybe<&2, Bool>}, P.false_ne_true(e))
432    case None{}:
433      {==}
434
435def one_less(+a: Nat, +b: Nat, +f: Nat, e1: {a == f : Nat}, e2: {a == 1n+b : Nat}) -> {b == Nat.sub(f, 1n) : Nat}:
436  %e1 : {b == Nat.sub(_, 1n) : Nat}
437  %Equal.sym(Nat, a, 1n+b, e2) : {b == Nat.sub(_, 1n) : Nat}
438  Equal.sym(Nat, Nat.sub(b, 0n), b, P.sub_zero(b))
439
440def when_or_eq(+g0a: Bool, +g0b: Bool, eg0: {g0a == g0b : Bool},
441  +d0a: Maybe<&2, T.Grid(Bool)>, +d0b: Maybe<&2, T.Grid(Bool)>, ed0: {d0a == d0b : Maybe<&2, T.Grid(Bool)>},
442  +g1a: Bool, +g1b: Bool, eg1: {g1a == g1b : Bool},
443  +d1a: Maybe<&2, T.Grid(Bool)>, +d1b: Maybe<&2, T.Grid(Bool)>, ed1: {d1a == d1b : Maybe<&2, T.Grid(Bool)>}) ->
444  {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
445    == S.dfs.or(S.dfs.when(g0b, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}:
446  %eg0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
447    == S.dfs.or(S.dfs.when(_, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
448  %ed0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
449    == S.dfs.or(S.dfs.when(g0a, x => _), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
450  %eg1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
451    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(_, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
452  %ed1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
453    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => _)) : Maybe<&2, T.Grid(Bool)>}
454  {==}
455
456def dfs2_eq.node(+x: Nat, +y: Nat, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
457  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +t: Nat, +f: Nat,
458  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
459  +et: {S.part_true(part) == t : Nat}, +ef: {S.part_none(part) == f : Nat},
460  +fr: Bool, fre: {S.is_none(S.look(part, T.Pos{x, y})) == fr : Bool},
461  ks: {S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}) == S.dfs(rest, part, S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>},
462  k0: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == t : Nat} ->
463    {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == Nat.sub(f, 1n) : Nat} ->
464    {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})
465      == S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>},
466  k1: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == 1n+t : Nat} ->
467    {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == Nat.sub(f, 1n) : Nat} ->
468    {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), 1n+t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})
469      == S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}) ->
470  {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}),
471      v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), n),
472          S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel)),
473        x0 => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})),
474      y0 => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), n),
475          S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel)),
476        z0 => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), 1n+t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its}))))
477    == S.dfs.free(fr, u => S.dfs(rest, part, S.Ctx{w, h, n, rows, its}),
478      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel, n),
479        x0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its})),
480      y0 => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel, n),
481        z0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), S.Ctx{w, h, n, rows, its})))) : Maybe<&2, T.Grid(Bool)>}:
482  match fr:
483    case False{}:
484      ks
485    case True{}:
486      +q = {T.Pos{x, y} : T.Pos}
487      +p0 = B.set_at(Maybe<&2, Bool>, part, q, Some{False{}})
488      +p1 = B.set_at(Maybe<&2, Bool>, part, q, Some{True{}})
489      +lk = none_of(S.look(part, q), fre)
490      +e0f = one_less(S.part_none(part), S.part_none(p0), f, ef, none_set(w, h, part, x, y, False{}, sh, on, lk))
491      +e1f = one_less(S.part_none(part), S.part_none(p1), f, ef, none_set(w, h, part, x, y, True{}, sh, on, lk))
492      +e0t = Equal.trans(Nat, S.part_true(p0), S.part_true(part), t, true_set_f(w, h, part, x, y, sh, on, lk), et)
493      +e1t = {%et : {S.part_true(p1) == 1n+_ : Nat}; true_set_t(w, h, part, x, y, sh, on, lk) : {S.part_true(p1) == 1n+t : Nat}}
494      +eg0 = {%e0t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool};
495        %e0f : {Bool.and(S.between(S.part_true(p0), _, n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool};
496        {==} : {Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool}}
497      +eg1 = {%e1t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool};
498        %e1f : {Bool.and(S.between(S.part_true(p1), _, n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool};
499        {==} : {Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool}}
500      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
501      when_or_eq(Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)), S.open_ok(p0, rel, n), eg0,
502        S.dfs2(rest, p0, t, Nat.sub(f, 1n), ctx), S.dfs(rest, p0, ctx), k0(e0t, e0f),
503        Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)), S.open_ok(p1, rel, n), eg1,
504        S.dfs2(rest, p1, 1n+t, Nat.sub(f, 1n), ctx), S.dfs(rest, p1, ctx), k1(e1t, e1f))
505
506# With the counts right and every cell on the board, the counting search
507# answers exactly as the plain one.
508law dfs2_eq:
509  for +todo: List<&2, S.Todo>
510  for +part: T.Grid(Maybe<&2, Bool>)
511  for +w: Nat
512  for +h: Nat
513  for +n: Nat
514  for +rows: T.Grid(T.Seen)
515  for +its: List<&2, S.Item>
516  for +t: Nat
517  for +f: Nat
518  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
519  for +con: {tall(~PS.WH, ~con_f, PS.WH{w, h}, todo) == True{} : Bool}
520  for +et: {S.part_true(part) == t : Nat}
521  for +ef: {S.part_none(part) == f : Nat}
522  {S.dfs2(todo, part, t, f, S.Ctx{w, h, n, rows, its}) == S.dfs(todo, part, S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}
523
524def dfs2_eq(todo, part, w, h, n, rows, its, t, f, sh, con, et, ef):
525  match todo:
526    case Nil{}:
527      {==}
528    case S.Todo{c, rel} <> rest:
529      match c:
530        case T.Pos{x, y}:
531          +q = {T.Pos{x, y} : T.Pos}
532          +onc = tall_head(~PS.WH, ~con_f, PS.WH{w, h}, S.Todo{q, rel}, rest, con)
533          +conr = tall_tail(~PS.WH, ~con_f, PS.WH{w, h}, S.Todo{q, rel}, rest, con)
534          +p0 = B.set_at(Maybe<&2, Bool>, part, q, Some{False{}})
535          +p1 = B.set_at(Maybe<&2, Bool>, part, q, Some{True{}})
536          dfs2_eq.node(x, y, rel, rest, part, w, h, n, rows, its, t, f, sh, onc, et, ef, S.is_none(S.look(part, q)), {==},
537            dfs2_eq(rest, part, w, h, n, rows, its, t, f, sh, conr, et, ef),
538            e0t => e0f => dfs2_eq(rest, p0, w, h, n, rows, its, t, Nat.sub(f, 1n),
539              PL.shaped_set(Maybe<&2, Bool>, w, h, part, q, Some{False{}}, sh), conr, e0t, e0f),
540            e1t => e1f => dfs2_eq(rest, p1, w, h, n, rows, its, 1n+t, Nat.sub(f, 1n),
541              PL.shaped_set(Maybe<&2, Bool>, w, h, part, q, Some{True{}}, sh), conr, e1t, e1f))