1 import Base 2 import ./types.bend as T 3 import ./board.bend as B 4 import ./game.bend as G 5 import ./LAWS.bend as L 6 import ./proof_base.bend as P 7 import ./proof_grid.bend as PG 8 import ./proof_copy.bend as PC 9 import ./proof_lists.bend as PL 10 import ./proof_cells.bend as PS 11 import ./proof_walk.bend as PW 12 import ./proof_flood.bend as PF 13 import ./solver.bend as S 14 15 # The invariant of real games, and that every action keeps it. 16 17 # Closure: every revealed zero has its neighbours revealed 18 # ======================================================== 19 20 def shown_in(g: T.Grid(Bool), q: T.Pos) -> Bool: 21 B.at(Bool, False{}, g, q) 22 23 type CL is Data: 24 CL{w: Nat, h: Nat, layout: T.Grid(Bool), g: T.Grid(Bool)} 25 26 def cl_f.go(e: CL, +q: T.Pos) -> Bool: 27 match e: 28 case CL{+w, +h, layout, +g}: 29 Bool.not(B.at(Bool, False{}, g, q) && B.zero(w, h, layout, q)) 30 || PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q)) 31 32 def cl_f(e: CL, q: T.Pos) -> Bool: 33 cl_f.go(e, q) 34 35 def closed(+w: Nat, +h: Nat, layout: T.Grid(Bool), g: T.Grid(Bool)) -> Bool: 36 PS.allp(~CL, ~cl_f, CL{w, h, layout, g}, B.cells(w, h)) 37 38 def closed_use.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: T.Grid(Bool), +q: T.Pos, +r: T.Pos, 39 f: {Bool.or(Bool.not(Bool.and(True{}, True{})), 40 PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool}, 41 rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}) -> 42 {B.at(Bool, False{}, g, r) == True{} : Bool}: 43 PS.allp_member(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q), r, f, rm) 44 45 # In a closed grid, a revealed zero's neighbours are revealed. 46 law closed_use: 47 for +w: Nat 48 for +h: Nat 49 for +layout: T.Grid(Bool) 50 for +g: T.Grid(Bool) 51 for c: {closed(w, h, layout, g) == True{} : Bool} 52 for +q: T.Pos 53 for on: {B.on_board(w, h, q) == True{} : Bool} 54 for gq: {B.at(Bool, False{}, g, q) == True{} : Bool} 55 for z: {B.zero(w, h, layout, q) == True{} : Bool} 56 for +r: T.Pos 57 for rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool} 58 {B.at(Bool, False{}, g, r) == True{} : Bool} 59 60 def closed_use(w, h, layout, g, c, q, on, gq, z, r, rm): 61 +f = PS.allp_member(~CL, ~cl_f, CL{w, h, layout, g}, B.cells(w, h), q, c, PS.cells_member(w, h, q, on)) 62 closed_use.go(w, h, layout, g, q, r, 63 %gq : {Bool.or(Bool.not(Bool.and(_, True{})), 64 PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool}; 65 %z : {Bool.or(Bool.not(Bool.and(B.at(Bool, False{}, g, q), _)), 66 PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool}; 67 f, rm) 68 69 # After a flood 70 # ============= 71 72 # The flood's one-cell closure fact: a revealed zero's neighbour is revealed. 73 def flood_fact.go(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 74 +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 75 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat}, 76 +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool}, 77 after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}, 78 +z: {B.zero(w, h, layout, q) == True{} : Bool}, +r: T.Pos, 79 +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}, 80 +s: Bool, se: {B.at(Bool, False{}, shown, q) == s : Bool}) -> 81 {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), r) == True{} : Bool}: 82 match s: 83 case True{}: 84 PF.flood_mono(n, work, hd, w, h, layout, shown, r, closed_use(w, h, layout, shown, cl, q, on, se, z, r, rm)) 85 case False{}: 86 PF.flood_zero(n, work, hd, w, h, layout, shown, sh, cnt, he, q, se, after, z, r, rm) 87 88 def closed_flood.nbrs(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 89 +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 90 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat}, 91 +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}, 92 +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}, 93 +z: {B.zero(w, h, layout, q) == True{} : Bool}, ns: List<&2, T.Pos>, 94 +adj: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, ns) == True{} : Bool}) -> 95 {PS.allp(~T.Grid(Bool), ~shown_in, G.flood(n, work, hd, w, h, layout, shown), ns) == True{} : Bool}: 96 match ns: 97 case Nil{}: 98 {==} 99 case +r <> +t: 100 +ar = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj) 101 +rm = PS.neighbours_member(w, h, q, r, P.and_true_r(B.adjacent(q, r), B.on_board(w, h, r), ar), 102 P.and_true_l(B.adjacent(q, r), B.on_board(w, h, r), ar)) 103 +F = G.flood(n, work, hd, w, h, layout, shown) 104 %Equal.sym(Bool, B.at(Bool, False{}, F, r), True{}, 105 flood_fact.go(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, on, after, z, r, rm, 106 B.at(Bool, False{}, shown, q), {==})) : 107 {Bool.and(_, PS.allp(~T.Grid(Bool), ~shown_in, F, t)) == True{} : Bool} 108 closed_flood.nbrs(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, on, after, z, t, 109 PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj)) 110 111 def closed_flood.cell(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 112 +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 113 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat}, 114 +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}, 115 +b: Bool, +be: {Bool.and(B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q), B.zero(w, h, layout, q)) == b : Bool}) -> 116 {cl_f(CL{w, h, layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}: 117 match b: 118 case False{}: 119 +F = G.flood(n, work, hd, w, h, layout, shown) 120 %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q)), False{}, be) : 121 {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, F, B.neighbours(w, h, q))) == True{} : Bool} 122 {==} 123 case True{}: 124 +F = G.flood(n, work, hd, w, h, layout, shown) 125 +fq = P.and_true_l(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q), be) 126 +zq = P.and_true_r(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q), be) 127 %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q)), True{}, be) : 128 {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, F, B.neighbours(w, h, q))) == True{} : Bool} 129 closed_flood.nbrs(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, on, fq, zq, 130 B.neighbours(w, h, q), PS.neighbours_all(w, h, q)) 131 132 def closed_flood.cells(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 133 +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 134 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat}, 135 +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, ps: List<&2, T.Pos>, 136 +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) -> 137 {PS.allp(~CL, ~cl_f, CL{w, h, layout, G.flood(n, work, hd, w, h, layout, shown)}, ps) == True{} : Bool}: 138 match ps: 139 case Nil{}: 140 {==} 141 case +q <> +t: 142 +F = G.flood(n, work, hd, w, h, layout, shown) 143 %Equal.sym(Bool, cl_f(CL{w, h, layout, F}, q), True{}, 144 closed_flood.cell(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, q, 145 PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons), 146 Bool.and(B.at(Bool, False{}, F, q), B.zero(w, h, layout, q)), {==})) : 147 {Bool.and(_, PS.allp(~CL, ~cl_f, CL{w, h, layout, F}, t)) == True{} : Bool} 148 closed_flood.cells(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, t, 149 PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons)) 150 151 # A flood from a closed grid leaves a closed grid. 152 law closed_flood: 153 for +n: Nat 154 for +work: List<&2, G.Work> 155 for +hd: Bool 156 for +w: Nat 157 for +h: Nat 158 for +layout: T.Grid(Bool) 159 for +shown: T.Grid(Bool) 160 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool} 161 for +cl: {closed(w, h, layout, shown) == True{} : Bool} 162 for +cnt: {n == B.count_false(shown) : Nat} 163 for +he: {G.head_hidden(w, h, shown, work) == hd : Bool} 164 {closed(w, h, layout, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool} 165 166 def closed_flood(n, work, hd, w, h, layout, shown, sh, cl, cnt, he): 167 closed_flood.cells(n, work, hd, w, h, layout, shown, sh, cl, cnt, he, B.cells(w, h), PS.cells_on(w, h)) 168 169 # After an explosion 170 # ================== 171 172 def zero_not_mine(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos, 173 z: {B.zero(w, h, layout, q) == True{} : Bool}) -> {B.mine(layout, q) == False{} : Bool}: 174 +a = Bool.and(B.on_board(w, h, q), Bool.not(B.mine(layout, q))) 175 P.not_true(B.mine(layout, q), 176 P.and_true_r(B.on_board(w, h, q), Bool.not(B.mine(layout, q)), 177 P.and_true_l(a, Nat.is_eq(B.adj_mines(w, h, layout, q), 0n), z))) 178 179 def explode_fact.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, 180 mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool}, 181 +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool}, 182 after: {B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q) == True{} : Bool}, 183 +z: {B.zero(w, h, layout, q) == True{} : Bool}, +r: T.Pos, 184 +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}, 185 +b: Bool, be: {B.same(p, q) == b : Bool}) -> 186 {B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), r) == True{} : Bool}: 187 match b: 188 case True{}: 189 PF.both_absurd({B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), r) == True{} : Bool}, 190 B.mine(layout, q), zero_not_mine(w, h, layout, q, z), 191 %PG.same_sound(p, q, be) : {B.mine(layout, _) == True{} : Bool}; mp) 192 case False{}: 193 PF.at_set_mono(shown, p, r, 194 closed_use(w, h, layout, shown, cl, q, on, 195 %PL.at_set_ne(Bool, shown, p, q, True{}, False{}, be) : {_ == True{} : Bool}; after, z, r, rm)) 196 197 def closed_explode.nbrs(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, 198 +mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool}, 199 +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}, 200 +after: {B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q) == True{} : Bool}, 201 +z: {B.zero(w, h, layout, q) == True{} : Bool}, ns: List<&2, T.Pos>, 202 +adj: {PS.allp(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, ns) == True{} : Bool}) -> 203 {PS.allp(~T.Grid(Bool), ~shown_in, B.set_at(Bool, shown, p, True{}), ns) == True{} : Bool}: 204 match ns: 205 case Nil{}: 206 {==} 207 case +r <> +t: 208 +ar = PS.allp_head(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj) 209 +rm = PS.neighbours_member(w, h, q, r, P.and_true_r(B.adjacent(q, r), B.on_board(w, h, r), ar), 210 P.and_true_l(B.adjacent(q, r), B.on_board(w, h, r), ar)) 211 +s2 = B.set_at(Bool, shown, p, True{}) 212 %Equal.sym(Bool, B.at(Bool, False{}, s2, r), True{}, 213 explode_fact.go(w, h, layout, shown, p, mp, cl, q, on, after, z, r, rm, B.same(p, q), {==})) : 214 {Bool.and(_, PS.allp(~T.Grid(Bool), ~shown_in, s2, t)) == True{} : Bool} 215 closed_explode.nbrs(w, h, layout, shown, p, mp, cl, q, on, after, z, t, 216 PS.allp_tail(~PS.WHS, ~PS.adj_on, PS.WHS{w, h, q}, r, t, adj)) 217 218 def closed_explode.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, 219 +mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool}, 220 +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}, +b: Bool, 221 +be: {Bool.and(B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q), B.zero(w, h, layout, q)) == b : Bool}) -> 222 {cl_f(CL{w, h, layout, B.set_at(Bool, shown, p, True{})}, q) == True{} : Bool}: 223 match b: 224 case False{}: 225 +s2 = B.set_at(Bool, shown, p, True{}) 226 %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q)), False{}, be) : 227 {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, s2, B.neighbours(w, h, q))) == True{} : Bool} 228 {==} 229 case True{}: 230 +s2 = B.set_at(Bool, shown, p, True{}) 231 %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q)), True{}, be) : 232 {Bool.or(Bool.not(_), PS.allp(~T.Grid(Bool), ~shown_in, s2, B.neighbours(w, h, q))) == True{} : Bool} 233 closed_explode.nbrs(w, h, layout, shown, p, mp, cl, q, on, 234 P.and_true_l(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q), be), 235 P.and_true_r(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q), be), 236 B.neighbours(w, h, q), PS.neighbours_all(w, h, q)) 237 238 def closed_explode.cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, 239 +mp: {B.mine(layout, p) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool}, 240 ps: List<&2, T.Pos>, +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) -> 241 {PS.allp(~CL, ~cl_f, CL{w, h, layout, B.set_at(Bool, shown, p, True{})}, ps) == True{} : Bool}: 242 match ps: 243 case Nil{}: 244 {==} 245 case +q <> +t: 246 +s2 = B.set_at(Bool, shown, p, True{}) 247 %Equal.sym(Bool, cl_f(CL{w, h, layout, s2}, q), True{}, 248 closed_explode.cell(w, h, layout, shown, p, mp, cl, q, 249 PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons), 250 Bool.and(B.at(Bool, False{}, s2, q), B.zero(w, h, layout, q)), {==})) : 251 {Bool.and(_, PS.allp(~CL, ~cl_f, CL{w, h, layout, s2}, t)) == True{} : Bool} 252 closed_explode.cells(w, h, layout, shown, p, mp, cl, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons)) 253 254 law closed_explode: 255 for +w: Nat 256 for +h: Nat 257 for +layout: T.Grid(Bool) 258 for +shown: T.Grid(Bool) 259 for +p: T.Pos 260 for +mp: {B.mine(layout, p) == True{} : Bool} 261 for +cl: {closed(w, h, layout, shown) == True{} : Bool} 262 {closed(w, h, layout, B.set_at(Bool, shown, p, True{})) == True{} : Bool} 263 264 def closed_explode(w, h, layout, shown, p, mp, cl): 265 closed_explode.cells(w, h, layout, shown, p, mp, cl, B.cells(w, h), PS.cells_on(w, h)) 266 267 # The blank grid is closed 268 # ======================== 269 270 def closed_blank.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos) -> 271 {cl_f(CL{w, h, layout, B.blank(Bool, w, h, False{})}, q) == True{} : Bool}: 272 match q: 273 case T.Pos{x, y}: 274 +bl = B.blank(Bool, w, h, False{}) 275 %Equal.sym(Bool, B.at(Bool, False{}, bl, T.Pos{x, y}), False{}, PL.blank_at(w, h, x, y)) : 276 {Bool.or(Bool.not(Bool.and(_, B.zero(w, h, layout, T.Pos{x, y}))), 277 PS.allp(~T.Grid(Bool), ~shown_in, bl, B.neighbours(w, h, T.Pos{x, y}))) == True{} : Bool} 278 {==} 279 280 def closed_blank.cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> 281 {PS.allp(~CL, ~cl_f, CL{w, h, layout, B.blank(Bool, w, h, False{})}, ps) == True{} : Bool}: 282 match ps: 283 case Nil{}: 284 {==} 285 case q <> t: 286 %Equal.sym(Bool, cl_f(CL{w, h, layout, B.blank(Bool, w, h, False{})}, q), True{}, 287 closed_blank.cell(w, h, layout, q)) : 288 {Bool.and(_, PS.allp(~CL, ~cl_f, CL{w, h, layout, B.blank(Bool, w, h, False{})}, t)) == True{} : Bool} 289 closed_blank.cells(w, h, layout, t) 290 291 law closed_blank: 292 for +w: Nat 293 for +h: Nat 294 for +layout: T.Grid(Bool) 295 {closed(w, h, layout, B.blank(Bool, w, h, False{})) == True{} : Bool} 296 297 def closed_blank(w, h, layout): 298 closed_blank.cells(w, h, layout, B.cells(w, h)) 299 300 # No revealed mine 301 # ================ 302 303 type LS is Data: 304 LS{layout: T.Grid(Bool), g: T.Grid(Bool)} 305 306 def nsm_f.go(e: LS, +q: T.Pos) -> Bool: 307 match e: 308 case LS{layout, g}: 309 Bool.not(B.at(Bool, False{}, g, q) && B.mine(layout, q)) 310 311 def nsm_f(e: LS, q: T.Pos) -> Bool: 312 nsm_f.go(e, q) 313 314 def nsm(w: Nat, h: Nat, layout: T.Grid(Bool), g: T.Grid(Bool)) -> Bool: 315 PS.allp(~LS, ~nsm_f, LS{layout, g}, B.cells(w, h)) 316 317 def nsm_use.go(+layout: T.Grid(Bool), +g: T.Grid(Bool), +q: T.Pos, 318 f: {Bool.not(Bool.and(B.at(Bool, False{}, g, q), True{})) == True{} : Bool}) -> 319 {B.at(Bool, False{}, g, q) == False{} : Bool}: 320 P.not_true(B.at(Bool, False{}, g, q), 321 %P.and_true_r_id(B.at(Bool, False{}, g, q)) : {Bool.not(_) == True{} : Bool}; f) 322 323 # Without a revealed mine, a mine of the board is not revealed. 324 law nsm_use: 325 for +w: Nat 326 for +h: Nat 327 for +layout: T.Grid(Bool) 328 for +g: T.Grid(Bool) 329 for n: {nsm(w, h, layout, g) == True{} : Bool} 330 for +q: T.Pos 331 for on: {B.on_board(w, h, q) == True{} : Bool} 332 for m: {B.mine(layout, q) == True{} : Bool} 333 {B.at(Bool, False{}, g, q) == False{} : Bool} 334 335 def nsm_use(w, h, layout, g, n, q, on, m): 336 nsm_use.go(layout, g, q, 337 %m : {Bool.not(Bool.and(B.at(Bool, False{}, g, q), _)) == True{} : Bool}; 338 PS.allp_member(~LS, ~nsm_f, LS{layout, g}, B.cells(w, h), q, n, PS.cells_member(w, h, q, on))) 339 340 def nsm_flood.walk(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p0: T.Pos, +q: T.Pos, 341 safe: {L.mine(layout, p0) == False{} : Bool}, mq: {B.mine(layout, q) == True{} : Bool}, 342 wk: PF.Walk(w, h, layout, p0, q), -A: Type) -> A: 343 match wk: 344 case (path, pw): 345 PF.both_absurd(A, L.mine(layout, q), PW.walk_safe(path, w, h, layout, p0, q, pw, safe), 346 %PC.mine_eq(layout, q) : {_ == True{} : Bool}; mq) 347 348 def nsm_flood.new(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 349 +shown: T.Grid(Bool), +p0: T.Pos, +safe: {L.mine(layout, p0) == False{} : Bool}, 350 +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool}, +q: T.Pos, 351 fq: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}, 352 mq: {B.mine(layout, q) == True{} : Bool}, before: {B.at(Bool, False{}, shown, q) == False{} : Bool}) -> 353 {nsm_f(LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}: 354 nsm_flood.walk(w, h, layout, p0, q, safe, mq, 355 PF.flood_path(n, work, hd, w, h, layout, shown, p0, ok, q, before, fq), 356 {nsm_f(LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}) 357 358 def nsm_flood.cell(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 359 +shown: T.Grid(Bool), +p0: T.Pos, +safe: {L.mine(layout, p0) == False{} : Bool}, 360 +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool}, 361 +ns: {nsm(w, h, layout, shown) == True{} : Bool}, +q: T.Pos, +on: {B.on_board(w, h, q) == True{} : Bool}, 362 +b: Bool, +be: {Bool.and(B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q), B.mine(layout, q)) == b : Bool}) -> 363 {nsm_f(LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, q) == True{} : Bool}: 364 match b: 365 case False{}: 366 +F = G.flood(n, work, hd, w, h, layout, shown) 367 %Equal.sym(Bool, Bool.and(B.at(Bool, False{}, F, q), B.mine(layout, q)), False{}, be) : 368 {Bool.not(_) == True{} : Bool} 369 {==} 370 case True{}: 371 +F = G.flood(n, work, hd, w, h, layout, shown) 372 +fq = P.and_true_l(B.at(Bool, False{}, F, q), B.mine(layout, q), be) 373 +mq = P.and_true_r(B.at(Bool, False{}, F, q), B.mine(layout, q), be) 374 nsm_flood.new(n, work, hd, w, h, layout, shown, p0, safe, ok, q, fq, mq, 375 nsm_use(w, h, layout, shown, ns, q, on, mq)) 376 377 def nsm_flood.cells(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool), 378 +shown: T.Grid(Bool), +p0: T.Pos, +safe: {L.mine(layout, p0) == False{} : Bool}, 379 +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool}, 380 +ns: {nsm(w, h, layout, shown) == True{} : Bool}, ps: List<&2, T.Pos>, 381 +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) -> 382 {PS.allp(~LS, ~nsm_f, LS{layout, G.flood(n, work, hd, w, h, layout, shown)}, ps) == True{} : Bool}: 383 match ps: 384 case Nil{}: 385 {==} 386 case +q <> +t: 387 +F = G.flood(n, work, hd, w, h, layout, shown) 388 %Equal.sym(Bool, nsm_f(LS{layout, F}, q), True{}, 389 nsm_flood.cell(n, work, hd, w, h, layout, shown, p0, safe, ok, ns, q, 390 PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons), 391 Bool.and(B.at(Bool, False{}, F, q), B.mine(layout, q)), {==})) : 392 {Bool.and(_, PS.allp(~LS, ~nsm_f, LS{layout, F}, t)) == True{} : Bool} 393 nsm_flood.cells(n, work, hd, w, h, layout, shown, p0, safe, ok, ns, t, 394 PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons)) 395 396 # A flood from a safe cell reveals no mine. 397 law nsm_flood: 398 for +n: Nat 399 for +work: List<&2, G.Work> 400 for +hd: Bool 401 for +w: Nat 402 for +h: Nat 403 for +layout: T.Grid(Bool) 404 for +shown: T.Grid(Bool) 405 for +p0: T.Pos 406 for +safe: {L.mine(layout, p0) == False{} : Bool} 407 for +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool} 408 for +ns: {nsm(w, h, layout, shown) == True{} : Bool} 409 {nsm(w, h, layout, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool} 410 411 def nsm_flood(n, work, hd, w, h, layout, shown, p0, safe, ok, ns): 412 nsm_flood.cells(n, work, hd, w, h, layout, shown, p0, safe, ok, ns, B.cells(w, h), PS.cells_on(w, h)) 413 414 def nsm_blank.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos) -> 415 {nsm_f(LS{layout, B.blank(Bool, w, h, False{})}, q) == True{} : Bool}: 416 match q: 417 case T.Pos{x, y}: 418 %Equal.sym(Bool, B.at(Bool, False{}, B.blank(Bool, w, h, False{}), T.Pos{x, y}), False{}, PL.blank_at(w, h, x, y)) : 419 {Bool.not(Bool.and(_, B.mine(layout, T.Pos{x, y}))) == True{} : Bool} 420 {==} 421 422 def nsm_blank.cells(+w: Nat, +h: Nat, +layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> 423 {PS.allp(~LS, ~nsm_f, LS{layout, B.blank(Bool, w, h, False{})}, ps) == True{} : Bool}: 424 match ps: 425 case Nil{}: 426 {==} 427 case q <> t: 428 %Equal.sym(Bool, nsm_f(LS{layout, B.blank(Bool, w, h, False{})}, q), True{}, nsm_blank.cell(w, h, layout, q)) : 429 {Bool.and(_, PS.allp(~LS, ~nsm_f, LS{layout, B.blank(Bool, w, h, False{})}, t)) == True{} : Bool} 430 nsm_blank.cells(w, h, layout, t) 431 432 law nsm_blank: 433 for +w: Nat 434 for +h: Nat 435 for +layout: T.Grid(Bool) 436 {nsm(w, h, layout, B.blank(Bool, w, h, False{})) == True{} : Bool} 437 438 def nsm_blank(w, h, layout): 439 nsm_blank.cells(w, h, layout, B.cells(w, h)) 440 441 # Status 442 # ====== 443 444 law won_or_playing_won: 445 for +b: Bool 446 {L.is_won(G.won_or_playing(b)) == b : Bool} 447 448 def won_or_playing_won(b): 449 match b: 450 case True{}: 451 {==} 452 case False{}: 453 {==} 454 455 law playing_is: 456 for +s: T.Status 457 for e: {G.is_playing(s) == True{} : Bool} 458 {s == T.Playing{} : T.Status} 459 460 def playing_is(s, e): 461 match s: 462 case T.Playing{}: 463 {==} 464 case T.Won{}: 465 Empty.absurd({T.Won{} == T.Playing{} : T.Status}, P.false_ne_true(e)) 466 case T.Lost{why}: 467 Empty.absurd({T.Lost{why} == T.Playing{} : T.Status}, P.false_ne_true(e)) 468 469 # The invariant 470 # ============= 471 472 def calm(+status: T.Status, +w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool)) -> Bool: 473 Bool.or(Bool.not(G.is_playing(status)), nsm(w, h, layout, shown)) 474 475 def Facts(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +status: T.Status) -> Type: 476 {B.shaped(Bool, w, h, shown) == True{} : Bool} & 477 ({L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool} & 478 ({calm(status, w, h, layout, shown) == True{} : Bool} & 479 {closed(w, h, layout, shown) == True{} : Bool})) 480 481 # What every real game satisfies: the board it was started with, a grid of 482 # revealed cells of the board's shape, Won exactly when every safe cell is 483 # revealed, no revealed mine during play, and every revealed zero's 484 # neighbours revealed. 485 def Inv(+w: Nat, +h: Nat, +layout: T.Grid(Bool), g: G.Game) -> Type: 486 match g: 487 case G.Game{gw, gh, gl, shown, flags, status}: 488 {gw == w : Nat} & ({gh == h : Nat} & ({gl == layout : T.Grid(Bool)} & Facts(w, h, layout, shown, status))) 489 490 def all_safe_cell(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, +q: T.Pos, 491 mp: {B.mine(layout, p) == True{} : Bool}, +b: Bool, be: {B.same(p, q) == b : Bool}) -> 492 {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) 493 == Bool.or(B.mine(layout, q), B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}: 494 match b: 495 case True{}: 496 +mq = {%PG.same_sound(p, q, be) : {B.mine(layout, _) == True{} : Bool}; mp : {B.mine(layout, q) == True{} : Bool}} 497 %Equal.sym(Bool, B.mine(layout, q), True{}, mq) : 498 {Bool.or(_, B.at(Bool, False{}, shown, q)) 499 == Bool.or(_, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool} 500 {==} 501 case False{}: 502 %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q), B.at(Bool, False{}, shown, q), 503 PL.at_set_ne(Bool, shown, p, q, True{}, False{}, be)) : 504 {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) == Bool.or(B.mine(layout, q), _) : Bool} 505 {==} 506 507 def all_safe_set_mine.go(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, 508 +mp: {B.mine(layout, p) == True{} : Bool}, ps: List<&2, T.Pos>) -> 509 {G.all_safe.go(layout, B.set_at(Bool, shown, p, True{}), ps) == G.all_safe.go(layout, shown, ps) : Bool}: 510 match ps: 511 case Nil{}: 512 {==} 513 case +q <> t: 514 +s2 = B.set_at(Bool, shown, p, True{}) 515 %Equal.sym(Bool, G.all_safe.go(layout, s2, t), G.all_safe.go(layout, shown, t), 516 all_safe_set_mine.go(layout, shown, p, mp, t)) : 517 {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, s2, q)), _) 518 == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool} 519 %all_safe_cell(layout, shown, p, q, mp, B.same(p, q), {==}) : 520 {Bool.and(_, G.all_safe.go(layout, shown, t)) 521 == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool} 522 {==} 523 524 law all_safe_set_mine: 525 for +w: Nat 526 for +h: Nat 527 for +layout: T.Grid(Bool) 528 for +shown: T.Grid(Bool) 529 for +p: T.Pos 530 for +mp: {B.mine(layout, p) == True{} : Bool} 531 {G.all_safe(w, h, layout, B.set_at(Bool, shown, p, True{})) == G.all_safe(w, h, layout, shown) : Bool} 532 533 def all_safe_set_mine(w, h, layout, shown, p, mp): 534 all_safe_set_mine.go(layout, shown, p, mp, B.cells(w, h)) 535 536 # Opening a cell keeps the invariant 537 # ================================== 538 539 def 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, {==}, {==}))))))) 577 578 law inv_open: 579 for +w: Nat 580 for +h: Nat 581 for +layout: T.Grid(Bool) 582 for +shown: T.Grid(Bool) 583 for +flags: List<&2, T.Pos> 584 for +status: T.Status 585 for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool} 586 for +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool} 587 for +cm: {calm(status, w, h, layout, shown) == True{} : Bool} 588 for +cl: {closed(w, h, layout, shown) == True{} : Bool} 589 for +p: T.Pos 590 Inv(w, h, layout, G.open(G.Game{w, h, layout, shown, flags, status}, p)) 591 592 def inv_open(w, h, layout, shown, flags, status, sh, won, cm, cl, p): 593 inv_open.go(w, h, layout, shown, flags, status, sh, won, cm, cl, p, 594 Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)), {==}, B.mine(layout, p), {==}) 595 596 # Every action keeps the invariant 597 # ================================ 598 599 def inv_reveal.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>, 600 +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 601 +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}, 602 +cm: {calm(status, w, h, layout, shown) == True{} : Bool}, 603 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos, +f: Bool) -> 604 Inv(w, h, layout, G.reveal.go(f, G.Game{w, h, layout, shown, flags, status}, p)): 605 match f: 606 case True{}: 607 ({==}, ({==}, ({==}, (sh, (won, (cm, cl)))))) 608 case False{}: 609 inv_open(w, h, layout, shown, flags, status, sh, won, cm, cl, p) 610 611 def inv_flag.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>, 612 +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 613 +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}, 614 +cm: {calm(status, w, h, layout, shown) == True{} : Bool}, 615 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos, +c: Bool) -> 616 Inv(w, h, layout, G.flag.go(c, G.Game{w, h, layout, shown, flags, status}, p)): 617 match c: 618 case False{}: 619 ({==}, ({==}, ({==}, (sh, (won, (cm, cl)))))) 620 case True{}: 621 ({==}, ({==}, ({==}, (sh, (won, (cm, cl)))))) 622 623 def inv_assist.safe(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>, 624 +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 625 +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}, 626 +cm: {calm(status, w, h, layout, shown) == True{} : Bool}, 627 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +m: Maybe<&2, T.Pos>) -> 628 Inv(w, h, layout, G.assist.safe(m, G.Game{w, h, layout, shown, flags, status})): 629 match m: 630 case None{}: 631 ({==}, ({==}, ({==}, (sh, (won, (cm, cl)))))) 632 case Some{p}: 633 inv_open(w, h, layout, shown, flags, status, sh, won, cm, cl, p) 634 635 def inv_assist.pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>, 636 +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 637 +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}, 638 +cm: {calm(status, w, h, layout, shown) == True{} : Bool}, 639 +cl: {closed(w, h, layout, shown) == True{} : Bool}, 640 +st: {status == T.Playing{} : T.Status}, +r: Maybe<&2, T.Pos>, +k: Nat) -> 641 Inv(w, h, layout, G.assist.pick(r, G.Game{w, h, layout, shown, flags, status}, k)): 642 match r: 643 case Some{q}: 644 ({==}, ({==}, ({==}, (sh, 645 ({%st : {L.is_won(_) == G.all_safe(w, h, layout, shown) : Bool}; 646 won : {False{} == G.all_safe(w, h, layout, shown) : Bool}}, 647 ({==}, cl)))))) 648 case None{}: 649 inv_assist.safe(w, h, layout, shown, flags, status, sh, won, cm, cl, 650 G.safe_cell(G.Game{w, h, layout, shown, flags, status}, k)) 651 652 def inv_assist.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>, 653 +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, 654 +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}, 655 +cm: {calm(status, w, h, layout, shown) == True{} : Bool}, 656 +cl: {closed(w, h, layout, shown) == True{} : Bool}, +c: Bool, ce: {G.is_playing(status) == c : Bool}, +k: Nat) -> 657 Inv(w, h, layout, G.assist.go(c, G.Game{w, h, layout, shown, flags, status}, k)): 658 match c: 659 case False{}: 660 ({==}, ({==}, ({==}, (sh, (won, (cm, cl)))))) 661 case True{}: 662 +g0 = {G.Game{w, h, layout, shown, flags, status} : G.Game} 663 inv_assist.pick(w, h, layout, shown, flags, status, sh, won, cm, cl, playing_is(status, ce), 664 S.solve(G.knowledge(g0)), k) 665 666 # Over a game in its general form. 667 law inv_reveal: 668 for +w: Nat 669 for +h: Nat 670 for +layout: T.Grid(Bool) 671 for +g: G.Game 672 for inv: Inv(w, h, layout, g) 673 for +p: T.Pos 674 Inv(w, h, layout, G.reveal(g, p)) 675 676 def inv_reveal(w, h, layout, g, inv, p): 677 match g: 678 case G.Game{gw, gh, gl, shown, flags, status}: 679 match inv: 680 case (ew, rest): 681 match rest: 682 case (eh, rest2): 683 match rest2: 684 case (el, facts): 685 match facts: 686 case (sh, f2): 687 match f2: 688 case (won, f3): 689 match f3: 690 case (cm, cl): 691 %Equal.sym(Nat, gw, w, ew) : Inv(w, h, layout, G.reveal(G.Game{_, gh, gl, shown, flags, status}, p)) 692 %Equal.sym(Nat, gh, h, eh) : Inv(w, h, layout, G.reveal(G.Game{w, _, gl, shown, flags, status}, p)) 693 %Equal.sym(T.Grid(Bool), gl, layout, el) : 694 Inv(w, h, layout, G.reveal(G.Game{w, h, _, shown, flags, status}, p)) 695 inv_reveal.go(w, h, layout, shown, flags, status, sh, won, cm, cl, p, 696 G.flagged(G.Game{w, h, layout, shown, flags, status}, p)) 697 698 law inv_flag: 699 for +w: Nat 700 for +h: Nat 701 for +layout: T.Grid(Bool) 702 for +g: G.Game 703 for inv: Inv(w, h, layout, g) 704 for +p: T.Pos 705 Inv(w, h, layout, G.flag(g, p)) 706 707 def inv_flag(w, h, layout, g, inv, p): 708 match g: 709 case G.Game{gw, gh, gl, shown, flags, status}: 710 match inv: 711 case (ew, rest): 712 match rest: 713 case (eh, rest2): 714 match rest2: 715 case (el, facts): 716 match facts: 717 case (sh, f2): 718 match f2: 719 case (won, f3): 720 match f3: 721 case (cm, cl): 722 %Equal.sym(Nat, gw, w, ew) : Inv(w, h, layout, G.flag(G.Game{_, gh, gl, shown, flags, status}, p)) 723 %Equal.sym(Nat, gh, h, eh) : Inv(w, h, layout, G.flag(G.Game{w, _, gl, shown, flags, status}, p)) 724 %Equal.sym(T.Grid(Bool), gl, layout, el) : 725 Inv(w, h, layout, G.flag(G.Game{w, h, _, shown, flags, status}, p)) 726 inv_flag.go(w, h, layout, shown, flags, status, sh, won, cm, cl, p, 727 G.can_flag(G.Game{w, h, layout, shown, flags, status}, p)) 728 729 law inv_assist: 730 for +w: Nat 731 for +h: Nat 732 for +layout: T.Grid(Bool) 733 for +g: G.Game 734 for inv: Inv(w, h, layout, g) 735 for +k: Nat 736 Inv(w, h, layout, G.assist(g, k)) 737 738 def inv_assist(w, h, layout, g, inv, k): 739 match g: 740 case G.Game{gw, gh, gl, shown, flags, status}: 741 match inv: 742 case (ew, rest): 743 match rest: 744 case (eh, rest2): 745 match rest2: 746 case (el, facts): 747 match facts: 748 case (sh, f2): 749 match f2: 750 case (won, f3): 751 match f3: 752 case (cm, cl): 753 %Equal.sym(Nat, gw, w, ew) : Inv(w, h, layout, G.assist(G.Game{_, gh, gl, shown, flags, status}, k)) 754 %Equal.sym(Nat, gh, h, eh) : Inv(w, h, layout, G.assist(G.Game{w, _, gl, shown, flags, status}, k)) 755 %Equal.sym(T.Grid(Bool), gl, layout, el) : 756 Inv(w, h, layout, G.assist(G.Game{w, h, _, shown, flags, status}, k)) 757 inv_assist.go(w, h, layout, shown, flags, status, sh, won, cm, cl, G.is_playing(status), {==}, k) 758 759 law inv_chord: 760 for +w: Nat 761 for +h: Nat 762 for +layout: T.Grid(Bool) 763 for +ts: List<&2, T.Pos> 764 for +g: G.Game 765 for inv: Inv(w, h, layout, g) 766 Inv(w, h, layout, G.chord_play(ts, g)) 767 768 def inv_chord(w, h, layout, ts, g, inv): 769 match ts: 770 case Nil{}: 771 inv 772 case q <> t: 773 inv_chord(w, h, layout, t, G.reveal(g, q), inv_reveal(w, h, layout, g, inv, q)) 774 775 law inv_step: 776 for +w: Nat 777 for +h: Nat 778 for +layout: T.Grid(Bool) 779 for +g: G.Game 780 for inv: Inv(w, h, layout, g) 781 for +a: T.Action 782 Inv(w, h, layout, G.step(g, a)) 783 784 def inv_step(w, h, layout, g, inv, a): 785 match a: 786 case T.Reveal{p}: 787 inv_reveal(w, h, layout, g, inv, p) 788 case T.Chord{p}: 789 inv_chord(w, h, layout, G.chord_targets(g, p), g, inv) 790 case T.Flag{p}: 791 inv_flag(w, h, layout, g, inv, p) 792 case T.Assist{k}: 793 inv_assist(w, h, layout, g, inv, k) 794 795 law inv_play: 796 for +w: Nat 797 for +h: Nat 798 for +layout: T.Grid(Bool) 799 for +acts: List<&2, T.Action> 800 for +g: G.Game 801 for inv: Inv(w, h, layout, g) 802 Inv(w, h, layout, L.play(acts, g)) 803 804 def inv_play(w, h, layout, acts, g, inv): 805 match acts: 806 case Nil{}: 807 inv 808 case a <> t: 809 inv_play(w, h, layout, t, G.step(g, a), inv_step(w, h, layout, g, inv, a)) 810 811 law inv_fresh: 812 for +w: Nat 813 for +h: Nat 814 for +layout: T.Grid(Bool) 815 Inv(w, h, layout, G.fresh(w, h, layout)) 816 817 def inv_fresh(w, h, layout): 818 +bl = B.blank(Bool, w, h, False{}) 819 +st = G.won_or_playing(G.all_safe(w, h, layout, bl)) 820 ({==}, ({==}, ({==}, (PL.blank_shaped(Bool, w, h, False{}), 821 (won_or_playing_won(G.all_safe(w, h, layout, bl)), 822 (%Equal.sym(Bool, nsm(w, h, layout, bl), True{}, nsm_blank(w, h, layout)) : 823 {Bool.or(Bool.not(G.is_playing(st)), _) == True{} : Bool}; 824 PS.or_true_r(Bool.not(G.is_playing(st))), 825 closed_blank(w, h, layout))))))) 826 827 # Every real game satisfies the invariant. 828 law inv_reach: 829 for +w: Nat 830 for +h: Nat 831 for +layout: T.Grid(Bool) 832 for +g: G.Game 833 for r: L.Reachable(w, h, layout, g) 834 Inv(w, h, layout, g) 835 836 def inv_reach(w, h, layout, g, r): 837 match r: 838 case (acts, e): 839 %e : Inv(w, h, layout, _) 840 inv_play(w, h, layout, acts, G.fresh(w, h, layout), inv_fresh(w, h, layout))