def inv_open.go

minebender-game@1.0.0.0 · proof_inv.bend:539

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
import minebender-game@1.0.0.0/proof_lists.bend as PL
import minebender-game@1.0.0.0/proof_cells.bend as PS
import minebender-game@1.0.0.0/proof_walk.bend as PW
import minebender-game@1.0.0.0/proof_flood.bend as PF

539def inv_open.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
540  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
541  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
542  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
543  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos,
544  +c: Bool, ce: {Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)) == c : Bool},
545  +m: Bool, +me: {B.mine(layout, p) == m : Bool}) ->
546  Inv(w, h, layout, G.open.go(c, m, G.Game{w, h, layout, shown, flags, status}, p)):
547  match c m:
548    case False{} _:
549      ({==}, ({==}, ({==}, (sh, (won, (cm, cl))))))
550    case True{} True{}:
551      +st = playing_is(status, P.and_true_l(G.is_playing(status), G.unrevealed(w, h, shown, p), ce))
552      +s2 = B.set_at(Bool, shown, p, True{})
553      +w0 = {%st : {L.is_won(_) == G.all_safe(w, h, layout, shown) : Bool};
554        won : {False{} == G.all_safe(w, h, layout, shown) : Bool}}
555      ({==}, ({==}, ({==}, (PL.shaped_set(Bool, w, h, shown, p, True{}, sh),
556        (Equal.trans(Bool, False{}, G.all_safe(w, h, layout, shown), G.all_safe(w, h, layout, s2), w0,
557          Equal.sym(Bool, G.all_safe(w, h, layout, s2), G.all_safe(w, h, layout, shown),
558            all_safe_set_mine(w, h, layout, shown, p, me))),
559        ({==}, closed_explode(w, h, layout, shown, p, me, cl)))))))
560    case True{} False{}:
561      +st = playing_is(status, P.and_true_l(G.is_playing(status), G.unrevealed(w, h, shown, p), ce))
562      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
563      +cf = B.count_false(shown)
564      +hh = G.head_hidden(w, h, shown, start)
565      +F = G.flood(cf, start, hh, w, h, layout, shown)
566      +ns = {%st : {Bool.or(Bool.not(G.is_playing(_)), nsm(w, h, layout, shown)) == True{} : Bool};
567        cm : {nsm(w, h, layout, shown) == True{} : Bool}}
568      +ok = {%Equal.sym(Bool, L.same(p, p), True{}, PW.lsame_refl(p)) : {Bool.and(_, True{}) == True{} : Bool};
569        {==} : {PF.works_ok(start, w, h, layout, p) == True{} : Bool}}
570      +safe = {%PC.mine_eq(layout, p) : {_ == False{} : Bool}; me : {L.mine(layout, p) == False{} : Bool}}
571      ({==}, ({==}, ({==}, (PF.flood_shaped(cf, start, hh, w, h, layout, shown, sh),
572        (won_or_playing_won(G.all_safe(w, h, layout, F)),
573        (%Equal.sym(Bool, nsm(w, h, layout, F), True{}, nsm_flood(cf, start, hh, w, h, layout, shown, p, safe, ok, ns)) :
574           {Bool.or(Bool.not(G.is_playing(G.won_or_playing(G.all_safe(w, h, layout, F)))), _) == True{} : Bool};
575           PS.or_true_r(Bool.not(G.is_playing(G.won_or_playing(G.all_safe(w, h, layout, F))))),
576         closed_flood(cf, start, hh, w, h, layout, shown, sh, cl, {==}, {==})))))))