def first_safe.lift

minebender-game@1.0.0.0 · proof_assist.bend:35

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/proof_solver.bend as PV

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))))