proof_assist.bend

minebender-game@1.0.0.0 · 348 lines · 20 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/solver.bend as S
6import minebender-game@1.0.0.0/LAWS.bend as L
7import minebender-game@1.0.0.0/proof_base.bend as P
8import minebender-game@1.0.0.0/proof_grid.bend as PG
9import minebender-game@1.0.0.0/proof_copy.bend as PC
10import minebender-game@1.0.0.0/proof_cells.bend as PS
11import minebender-game@1.0.0.0/proof_inv.bend as PI
12import minebender-game@1.0.0.0/proof_laws.bend as PW
13import minebender-game@1.0.0.0/proof_solver.bend as PV
14
15# Proofs of the two assist laws.
16
17# A safe hidden cell, while one exists
18# ====================================
19
20def not_and_false(+a: Bool, +b: Bool, e: {Bool.and(Bool.not(a), Bool.not(b)) == False{} : Bool}) ->
21  {Bool.or(a, b) == True{} : Bool}:
22  match a b:
23    case True{} _:
24      {==}
25    case False{} True{}:
26      {==}
27    case False{} False{}:
28      Empty.absurd({False{} == True{} : Bool}, P.true_ne_false(e))
29
30def SafeAt(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +ps: List<&2, T.Pos>) -> Type:
31  Exists(T.Pos, p => {G.first_safe(layout, shown, ps) == Some{p} : Maybe<&2, T.Pos>} &
32    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
33     {B.contains(ps, p) == True{} : Bool}))
34
35def first_safe.lift(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>,
36  r: SafeAt(layout, shown, t), -hit: Bool, he: {hit == False{} : Bool}) ->
37  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
38    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
39     {B.contains(q <> t, p) == True{} : Bool})):
40  match r:
41    case (+p, pr):
42      match pr:
43        case (fe, rest):
44          match rest:
45            case (sf, m):
46              %Equal.sym(Bool, hit, False{}, he) :
47                Exists(T.Pos, p2 => {G.first_safe.go(q <> t, _, layout, shown) == Some{p2} : Maybe<&2, T.Pos>} &
48                  ({Bool.and(Bool.not(B.mine(layout, p2)), Bool.not(B.at(Bool, False{}, shown, p2))) == True{} : Bool} &
49                   {B.contains(q <> t, p2) == True{} : Bool}))
50              (p, (fe, (sf, PV.or_r(B.same(q, p), B.contains(t, p), m))))
51
52def first_safe.go2(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>, +hit: Bool,
53  he: {Bool.and(Bool.not(B.mine(layout, q)), Bool.not(B.at(Bool, False{}, shown, q))) == hit : Bool},
54  e: {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) == False{} : Bool},
55  ih: {G.all_safe.go(layout, shown, t) == False{} : Bool} -> SafeAt(layout, shown, t)) ->
56  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
57    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
58     {B.contains(q <> t, p) == True{} : Bool})):
59  match hit:
60    case True{}:
61      (q, ({==}, (he, PV.or_l(B.same(q, q), B.contains(t, q), PG.same_refl(q)))))
62    case False{}:
63      first_safe.lift(layout, shown, q, t,
64        ih(%not_and_false(B.mine(layout, q), B.at(Bool, False{}, shown, q), he) :
65            {Bool.and(_, G.all_safe.go(layout, shown, t)) == False{} : Bool}; e),
66        False{}, {==})
67
68# While some safe cell is unrevealed, first_safe finds one.
69law first_safe_some:
70  for +layout: T.Grid(Bool)
71  for +shown: T.Grid(Bool)
72  for +ps: List<&2, T.Pos>
73  for e: {G.all_safe.go(layout, shown, ps) == False{} : Bool}
74  SafeAt(layout, shown, ps)
75
76def first_safe_some(layout, shown, ps, e):
77  match ps:
78    case Nil{}:
79      Empty.absurd(SafeAt(layout, shown, Nil{}), P.true_ne_false(e))
80    case q <> t:
81      first_safe.go2(layout, shown, q, t,
82        Bool.and(Bool.not(B.mine(layout, q)), Bool.not(B.at(Bool, False{}, shown, q))), {==}, e,
83        et => first_safe_some(layout, shown, t, et))
84
85# Where the assist looks
86# ======================
87
88law all_safe_append:
89  for +layout: T.Grid(Bool)
90  for +shown: T.Grid(Bool)
91  for +xs: List<&2, T.Pos>
92  for +ys: List<&2, T.Pos>
93  for e: {G.all_safe.go(layout, shown, ys) == False{} : Bool}
94  {G.all_safe.go(layout, shown, List.append(&2, T.Pos, xs, ys)) == False{} : Bool}
95
96def all_safe_append(layout, shown, xs, ys, e):
97  match xs:
98    case Nil{}:
99      e
100    case +p <> t:
101      %Equal.sym(Bool, G.all_safe.go(layout, shown, List.append(&2, T.Pos, t, ys)), False{},
102        all_safe_append(layout, shown, t, ys, e)) :
103        {Bool.and(Bool.or(B.mine(layout, p), B.at(Bool, False{}, shown, p)), _) == False{} : Bool}
104      P.and_false_r(Bool.or(B.mine(layout, p), B.at(Bool, False{}, shown, p)))
105
106law on_drop:
107  for +w: Nat
108  for +h: Nat
109  for +ps: List<&2, T.Pos>
110  for +i: Nat
111  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
112  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.drop(&2, T.Pos, ps, i)) == True{} : Bool}
113
114def on_drop(w, h, ps, i, on):
115  match ps i:
116    case Nil{} _:
117      {==}
118    case q <> t 0n:
119      on
120    case q <> t 1n+j:
121      on_drop(w, h, t, j, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, on))
122
123law on_take:
124  for +w: Nat
125  for +h: Nat
126  for +ps: List<&2, T.Pos>
127  for +i: Nat
128  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
129  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.take(&2, T.Pos, ps, i)) == True{} : Bool}
130
131def on_take(w, h, ps, i, on):
132  match ps i:
133    case Nil{} _:
134      {==}
135    case q <> t 0n:
136      {==}
137    case q <> t 1n+j:
138      %Equal.sym(Bool, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.take(&2, T.Pos, t, j)), True{},
139        on_take(w, h, t, j, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, on))) :
140        {Bool.and(PS.onb(PS.WH{w, h}, q), _) == True{} : Bool}
141      %Equal.sym(Bool, PS.onb(PS.WH{w, h}, q), True{}, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, on)) :
142        {Bool.and(_, True{}) == True{} : Bool}
143      {==}
144
145def on_turn(+w: Nat, +h: Nat, +ps: List<&2, T.Pos>, +k: Nat,
146  +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
147  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(ps, k)) == True{} : Bool}:
148  +i = Nat.mod(k, Nat.add(List.length(&2, T.Pos, ps), 1n))
149  PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, List.drop(&2, T.Pos, ps, i), List.take(&2, T.Pos, ps, i),
150    on_drop(w, h, ps, i, on), on_take(w, h, ps, i, on))
151
152def on_put(+w: Nat, +h: Nat, +p: T.Pos, +t: List<&2, T.Pos>, +b: Bool,
153  hd: {PS.onb(PS.WH{w, h}, p) == True{} : Bool}, tl: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, t) == True{} : Bool}) ->
154  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, List.filter.put(T.Pos, p, t, b)) == True{} : Bool}:
155  match b:
156    case False{}:
157      tl
158    case True{}:
159      %Equal.sym(Bool, PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, t), True{}, tl) :
160        {Bool.and(PS.onb(PS.WH{w, h}, p), _) == True{} : Bool}
161      %Equal.sym(Bool, PS.onb(PS.WH{w, h}, p), True{}, hd) : {Bool.and(_, True{}) == True{} : Bool}
162      {==}
163
164law on_edges:
165  for +w: Nat
166  for +h: Nat
167  for +shown: T.Grid(Bool)
168  for +ps: List<&2, T.Pos>
169  for +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
170  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.edges(w, h, shown, ps)) == True{} : Bool}
171
172def on_edges(w, h, shown, ps, on):
173  match ps:
174    case Nil{}:
175      {==}
176    case +p <> +t:
177      on_put(w, h, p, G.edges(w, h, shown, t),
178        Bool.and(Bool.not(B.at(Bool, False{}, shown, p)), G.any_shown(shown, B.neighbours(w, h, p))),
179        PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, on),
180        on_edges(w, h, shown, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, p, t, on)))
181
182# Every cell the assist may look at is on the board.
183def on_list(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +k: Nat) ->
184  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, shown, k)) == True{} : Bool}:
185  +cs = B.cells(w, h)
186  +es = G.edges(w, h, shown, cs)
187  PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(es, k), List.append(&2, T.Pos, G.turn(cs, k), cs),
188    on_turn(w, h, es, k, on_edges(w, h, shown, cs, PS.cells_on(w, h))),
189    PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(cs, k), cs, on_turn(w, h, cs, k, PS.cells_on(w, h)), PS.cells_on(w, h)))
190
191# While a safe cell is hidden, the assist's list holds one.
192def nos_list(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +k: Nat,
193  nos: {G.all_safe(w, h, layout, shown) == False{} : Bool}) ->
194  {G.all_safe.go(layout, shown, G.safe_list(w, h, shown, k)) == False{} : Bool}:
195  +cs = B.cells(w, h)
196  all_safe_append(layout, shown, G.turn(G.edges(w, h, shown, cs), k), List.append(&2, T.Pos, G.turn(cs, k), cs),
197    all_safe_append(layout, shown, G.turn(cs, k), cs, nos))
198
199# Pressing the assist when stuck
200# ==============================
201
202def stuck_pick.none(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +k: Nat,
203  sa: SafeAt(layout, s, G.safe_list(w, h, s, k))) ->
204  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
205    ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) == True{} : Bool} &
206     {G.assist.safe(G.first_safe(layout, s, G.safe_list(w, h, s, k)), G.Game{w, h, layout, s, f, T.Playing{}})
207       == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})):
208  match sa:
209    case (+p, pr):
210      match pr:
211        case (+fe, rest):
212          match rest:
213            case (+sf, m):
214              +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
215              +nm = P.not_true(B.mine(layout, p), P.and_true_l(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf))
216              +onp = PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, s, k), p, on_list(w, h, s, k), m)
217              (p,
218                (%PC.mine_eq(layout, p) : {_ == False{} : Bool}; nm,
219                 (%Equal.sym(Bool, L.hidden(G.knowledge(g0), p), G.unrevealed(w, h, s, p),
220                    PG.know_hidden(w, h, layout, s, f, T.Playing{}, p)) : {_ == True{} : Bool};
221                    %Equal.sym(Bool, B.on_board(w, h, p), True{}, onp) :
222                      {Bool.and(_, Bool.not(B.at(Bool, False{}, s, p))) == True{} : Bool};
223                    P.and_true_r(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf),
224                  %Equal.sym(Maybe<&2, T.Pos>, G.first_safe(layout, s, G.safe_list(w, h, s, k)), Some{p}, fe) :
225                    {G.assist.safe(_, g0) == G.open(g0, p) : G.Game};
226                  {==})))
227
228def stuck_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
229  +nos: {G.all_safe(w, h, layout, s) == False{} : Bool},
230  stuck: L.Stuck(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})),
231  +r: Maybe<&2, T.Pos>, re: {S.solve(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})) == r : Maybe<&2, T.Pos>}, +k: Nat) ->
232  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
233    ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) == True{} : Bool} &
234     {G.assist.pick(r, G.Game{w, h, layout, s, f, T.Playing{}}, k) == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})):
235  match r:
236    case Some{q}:
237      +k0 = G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})
238      Empty.absurd(Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
239        ({L.hidden(k0, p) == True{} : Bool} &
240         {G.assist.pick(Some{q}, G.Game{w, h, layout, s, f, T.Playing{}}, k) == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})),
241        stuck(q, PV.solve_safe(k0, q, re)))
242    case None{}:
243      stuck_pick.none(w, h, layout, s, f, k, first_safe_some(layout, s, G.safe_list(w, h, s, k), nos_list(w, h, layout, s, k, nos)))
244
245def assist_stuck.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
246  +playing: {G.status(g) == T.Playing{} : T.Status}, stuck: L.Stuck(G.knowledge(g)), +k: Nat, c: PW.Canon(w, h, layout, g)) ->
247  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
248    ({L.hidden(G.knowledge(g), p) == True{} : Bool} & {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game})):
249  match c:
250    case (+eg, facts):
251      match facts:
252        case (sh, f2):
253          match f2:
254            case (won, f3):
255              +s = PW.shown_of(g)
256              +f = PW.flags_of(g)
257              +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
258              %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
259                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
260                  ({L.hidden(G.knowledge(_), p) == True{} : Bool} & {G.step(_, T.Assist{k}) == G.open(_, p) : G.Game}))
261              %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
262                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
263                  ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), p) == True{} : Bool} &
264                   {G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k}) == G.open(G.Game{w, h, layout, s, f, _}, p) : G.Game}))
265              stuck_pick(w, h, layout, s, f,
266                Equal.sym(Bool, False{}, G.all_safe(w, h, layout, s),
267                  %playing : {L.is_won(_) == G.all_safe(w, h, layout, s) : Bool}; won),
268                {%playing : L.Stuck(G.knowledge(G.Game{w, h, layout, s, f, _}));
269                  %eg : L.Stuck(G.knowledge(_)); stuck : L.Stuck(G.knowledge(gp))},
270                S.solve(G.knowledge(gp)), {==}, k)
271
272law assist_stuck_:
273  for +w: Nat
274  for +h: Nat
275  for +layout: T.Grid(Bool)
276  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
277  for +g: G.Game
278  for r: L.Reachable(w, h, layout, g)
279  for +playing: {G.status(g) == T.Playing{} : T.Status}
280  for stuck: L.Stuck(G.knowledge(g))
281  for +k: Nat
282  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
283    ({L.hidden(G.knowledge(g), p) == True{} : Bool} & {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game}))
284
285def assist_stuck_(w, h, layout, shape, g, r, playing, stuck, k):
286  assist_stuck.k(w, h, layout, g, playing, stuck, k, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))
287
288# Pressing the assist too early
289# =============================
290
291def early_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +q: T.Pos,
292  option: L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q),
293  +r: Maybe<&2, T.Pos>, re: {S.solve(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})) == r : Maybe<&2, T.Pos>}, +k: Nat) ->
294  Exists(T.Pos, p => L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) &
295    ({G.status(G.assist.pick(r, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
296     {G.knowledge(G.assist.pick(r, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}) : T.Knowledge})):
297  match r:
298    case Some{p}:
299      +k0 = G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})
300      (p, (PV.solve_safe(k0, p, re), ({==}, {==})))
301    case None{}:
302      +k0 = G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}})
303      Empty.absurd(Exists(T.Pos, p => L.ProvablySafe(k0, p) &
304        ({G.status(G.assist.pick(None{}, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
305         {G.knowledge(G.assist.pick(None{}, G.Game{w, h, layout, s, f, T.Playing{}}, k)) == k0 : T.Knowledge})),
306        PV.solve_stuck(k0, re)(q, option))
307
308def assist_early.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
309  +playing: {G.status(g) == T.Playing{} : T.Status}, +q: T.Pos, option: L.ProvablySafe(G.knowledge(g), q), +k: Nat,
310  c: PW.Canon(w, h, layout, g)) ->
311  Exists(T.Pos, p => L.ProvablySafe(G.knowledge(g), p) &
312    ({G.status(G.step(g, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
313     {G.knowledge(G.step(g, T.Assist{k})) == G.knowledge(g) : T.Knowledge})):
314  match c:
315    case (+eg, facts):
316      +s = PW.shown_of(g)
317      +f = PW.flags_of(g)
318      +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
319      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
320        Exists(T.Pos, p => L.ProvablySafe(G.knowledge(_), p) &
321          ({G.status(G.step(_, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
322           {G.knowledge(G.step(_, T.Assist{k})) == G.knowledge(_) : T.Knowledge}))
323      %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
324        Exists(T.Pos, p => L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, _}), p) &
325          ({G.status(G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
326           {G.knowledge(G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k})) == G.knowledge(G.Game{w, h, layout, s, f, _}) : T.Knowledge}))
327      early_pick(w, h, layout, s, f, q,
328        {%playing : L.ProvablySafe(G.knowledge(G.Game{w, h, layout, s, f, _}), q);
329          %eg : L.ProvablySafe(G.knowledge(_), q); option : L.ProvablySafe(G.knowledge(gp), q)},
330        S.solve(G.knowledge(gp)), {==}, k)
331
332law assist_too_early_:
333  for +w: Nat
334  for +h: Nat
335  for +layout: T.Grid(Bool)
336  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
337  for +g: G.Game
338  for r: L.Reachable(w, h, layout, g)
339  for +playing: {G.status(g) == T.Playing{} : T.Status}
340  for +q: T.Pos
341  for option: L.ProvablySafe(G.knowledge(g), q)
342  for +k: Nat
343  Exists(T.Pos, p => L.ProvablySafe(G.knowledge(g), p) &
344    ({G.status(G.step(g, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
345     {G.knowledge(G.step(g, T.Assist{k})) == G.knowledge(g) : T.Knowledge}))
346
347def assist_too_early_(w, h, layout, shape, g, r, playing, q, option, k):
348  assist_early.k(w, h, layout, g, playing, q, option, k, PW.canon(w, h, layout, g, PI.inv_reach(w, h, layout, g, r)))