def agrees_pick

minebender-game@1.0.0.0 · proof_laws.bend:198

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/LAWS.bend as L
import minebender-game@1.0.0.0/proof_base.bend as P
import minebender-game@1.0.0.0/proof_copy.bend as PC

198def agrees_pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos, +c: Bool, +m: Bool,
199  me: {B.mine(layout, p) == m : Bool}) ->
200  {L.agrees(w, h, layout, p, G.seen_pick(c, m, w, h, layout, p)) == True{} : Bool}:
201  match c m:
202    case False{} _:
203      {==}
204    case True{} True{}:
205      %PC.mine_eq(layout, p) : {_ == True{} : Bool}
206      me
207    case True{} False{}:
208      %PC.mine_eq(layout, p) :
209        {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
210      %Equal.sym(Bool, B.mine(layout, p), False{}, me) :
211        {Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), B.adj_mines(w, h, layout, p))) == True{} : Bool}
212      %PC.adj_mines_eq(w, h, layout, p) :
213        {Bool.and(True{}, Nat.is_eq(_, B.adj_mines(w, h, layout, p))) == True{} : Bool}
214      P.eq_refl(B.adj_mines(w, h, layout, p))