proof_grid.bend
minebender-game@1.0.0.0 · 334 lines · 23 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/LAWS.bend as L
6import minebender-game@1.0.0.0/proof_base.bend as P
7
8
9
10def Maybe.disc_none(-A: Data, m: Maybe<&2, A>) -> Type:
11 match m:
12 case None{}:
13 Unit
14 case Some{v}:
15 Empty
16
17def know_row_get.none(-A: Data, -x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:
18 %e : Maybe.disc_none(A, _)
19 Unit{}
20
21def Maybe.value(-A: Data, +d: A, m: Maybe<&2, A>) -> A:
22 match m:
23 case None{}:
24 d
25 case Some{v}:
26 v
27
28def know_row_get.some(-A: Data, +a: A, +x: A, e: {Some{a} == Some{x} : Maybe<&2, A>}) ->
29 {a == x : A}:
30 Equal.cong(Maybe<&2, A>, A, m => Maybe.value(A, a, m), Some{a}, Some{x}, e)
31
32law know_row_get:
33 for +w: Nat
34 for +h: Nat
35 for +layout: T.Grid(Bool)
36 for +shown: T.Grid(Bool)
37 for +y: Nat
38 for +xs: List<&2, Nat>
39 for +j: Nat
40 for +x: Nat
41 for e: {List.get(&2, Nat, xs, j) == Some{x} : Maybe<&2, Nat>}
42 {List.get(&2, T.Seen, G.know_row(w, h, layout, shown, y, xs), j)
43 == Some{G.seen_at(w, h, layout, shown, T.Pos{x, y})} : Maybe<&2, T.Seen>}
44
45def know_row_get(w, h, layout, shown, y, xs, j, x, e):
46 match xs j:
47 case Nil{} _:
48 Empty.absurd({List.get(&2, T.Seen, G.know_row(w, h, layout, shown, y, Nil{}), j)
49 == Some{G.seen_at(w, h, layout, shown, T.Pos{x, y})} : Maybe<&2, T.Seen>},
50 know_row_get.none(Nat, x, e))
51 case a <> t 0n:
52 %know_row_get.some(Nat, a, x, e) :
53 {Some{G.seen_at(w, h, layout, shown, T.Pos{a, y})}
54 == Some{G.seen_at(w, h, layout, shown, T.Pos{_, y})} : Maybe<&2, T.Seen>}
55 {==}
56 case a <> t 1n+k:
57 know_row_get(w, h, layout, shown, y, t, k, x, e)
58
59
60law know_rows_get:
61 for +w: Nat
62 for +h: Nat
63 for +layout: T.Grid(Bool)
64 for +shown: T.Grid(Bool)
65 for +ys: List<&2, Nat>
66 for +i: Nat
67 for +y: Nat
68 for e: {List.get(&2, Nat, ys, i) == Some{y} : Maybe<&2, Nat>}
69 {List.get(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, ys), i)
70 == Some{G.know_row(w, h, layout, shown, y, List.range(w))} : Maybe<&2, List<&2, T.Seen>>}
71
72def know_rows_get(w, h, layout, shown, ys, i, y, e):
73 match ys i:
74 case Nil{} _:
75 Empty.absurd({List.get(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, Nil{}), i)
76 == Some{G.know_row(w, h, layout, shown, y, List.range(w))} : Maybe<&2, List<&2, T.Seen>>},
77 know_row_get.none(Nat, y, e))
78 case a <> t 0n:
79 %know_row_get.some(Nat, a, y, e) :
80 {Some{G.know_row(w, h, layout, shown, a, List.range(w))}
81 == Some{G.know_row(w, h, layout, shown, _, List.range(w))} : Maybe<&2, List<&2, T.Seen>>}
82 {==}
83 case a <> t 1n+k:
84 know_rows_get(w, h, layout, shown, t, k, y, e)
85
86
87law know_at:
88 for +w: Nat
89 for +h: Nat
90 for +layout: T.Grid(Bool)
91 for +shown: T.Grid(Bool)
92 for +x: Nat
93 for +y: Nat
94 for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
95 {L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), T.Pos{x, y})
96 == G.seen_at(w, h, layout, shown, T.Pos{x, y}) : T.Seen}
97
98def know_at(w, h, layout, shown, x, y, on):
99 +xw = P.and_true_l(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
100 +yh = P.and_true_r(Nat.is_lt(x, w), Nat.is_lt(y, h), on)
101 +rows = G.know_rows(w, h, layout, shown, List.range(h))
102 +row = G.know_row(w, h, layout, shown, y, List.range(w))
103 %Equal.sym(Maybe<&2, List<&2, T.Seen>>, List.get(&2, List<&2, T.Seen>, rows, y), Some{row},
104 know_rows_get(w, h, layout, shown, List.range(h), y, y, P.range_get(h, y, yh))) :
105 {Maybe.default(&2, T.Seen, List.get(&2, T.Seen,
106 Maybe.default(&2, List<&2, T.Seen>, _, Nil{}), x), T.Hidden{})
107 == G.seen_at(w, h, layout, shown, T.Pos{x, y}) : T.Seen}
108 %Equal.sym(Maybe<&2, T.Seen>, List.get(&2, T.Seen, row, x),
109 Some{G.seen_at(w, h, layout, shown, T.Pos{x, y})},
110 know_row_get(w, h, layout, shown, y, List.range(w), x, x, P.range_get(w, x, xw))) :
111 {Maybe.default(&2, T.Seen, _, T.Hidden{})
112 == G.seen_at(w, h, layout, shown, T.Pos{x, y}) : T.Seen}
113 {==}
114
115law hidden_pick:
116 for +c: Bool
117 for +m: Bool
118 for +w: Nat
119 for +h: Nat
120 for +layout: T.Grid(Bool)
121 for +p: T.Pos
122 {L.is_hidden(G.seen_pick(c, m, w, h, layout, p)) == Bool.not(c) : Bool}
123
124def hidden_pick(c, m, w, h, layout, p):
125 match c m:
126 case False{} _:
127 {==}
128 case True{} True{}:
129 {==}
130 case True{} False{}:
131 {==}
132
133def know_hidden.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool),
134 +x: Nat, +y: Nat, +b: Bool, +e: {B.on_board(w, h, T.Pos{x, y}) == b : Bool}) ->
135 {Bool.and(B.on_board(w, h, T.Pos{x, y}),
136 L.is_hidden(L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), T.Pos{x, y})))
137 == Bool.and(B.on_board(w, h, T.Pos{x, y}), Bool.not(B.at(Bool, False{}, shown, T.Pos{x, y})))
138 : Bool}:
139 match b:
140 case False{}:
141 %Equal.sym(Bool, B.on_board(w, h, T.Pos{x, y}), False{}, e) :
142 {Bool.and(_, L.is_hidden(L.at(T.Seen, T.Hidden{}, G.know_rows(w, h, layout, shown, List.range(h)), T.Pos{x, y})))
143 == Bool.and(_, Bool.not(B.at(Bool, False{}, shown, T.Pos{x, y}))) : Bool}
144 {==}
145 case True{}:
146 +rows = G.know_rows(w, h, layout, shown, List.range(h))
147 +p = {T.Pos{x, y} : T.Pos}
148 %Equal.sym(Bool, B.on_board(w, h, p), True{}, e) :
149 {Bool.and(_, L.is_hidden(L.at(T.Seen, T.Hidden{}, rows, p)))
150 == Bool.and(_, Bool.not(B.at(Bool, False{}, shown, p))) : Bool}
151 %Equal.sym(T.Seen, L.at(T.Seen, T.Hidden{}, rows, p), G.seen_at(w, h, layout, shown, p),
152 know_at(w, h, layout, shown, x, y, e)) :
153 {L.is_hidden(_) == Bool.not(B.at(Bool, False{}, shown, p)) : Bool}
154 hidden_pick(B.at(Bool, False{}, shown, p), B.mine(layout, p), w, h, layout, p)
155
156
157law know_hidden:
158 for +w: Nat
159 for +h: Nat
160 for +layout: T.Grid(Bool)
161 for +shown: T.Grid(Bool)
162 for +flags: List<&2, T.Pos>
163 for +status: T.Status
164 for +p: T.Pos
165 {L.hidden(G.knowledge(G.Game{w, h, layout, shown, flags, status}), p)
166 == G.unrevealed(w, h, shown, p) : Bool}
167
168def know_hidden(w, h, layout, shown, flags, status, p):
169 match p:
170 case T.Pos{x, y}:
171 know_hidden.go(w, h, layout, shown, x, y, B.on_board(w, h, T.Pos{x, y}), {==})
172
173
174
175
176law same_refl:
177 for +p: T.Pos
178 {B.same(p, p) == True{} : Bool}
179
180def same_refl(p):
181 match p:
182 case T.Pos{x, y}:
183 %Equal.sym(Bool, Nat.is_eq(x, x), True{}, P.eq_refl(x)) :
184 {Bool.and(_, Nat.is_eq(y, y)) == True{} : Bool}
185 P.eq_refl(y)
186
187law same_sound:
188 for +p: T.Pos
189 for +q: T.Pos
190 for +e: {B.same(p, q) == True{} : Bool}
191 {p == q : T.Pos}
192
193def same_sound(p, q, e):
194 match p q:
195 case T.Pos{px, py} T.Pos{qx, qy}:
196 +ex = P.eq_sound(px, qx, P.and_true_l(Nat.is_eq(px, qx), Nat.is_eq(py, qy), e))
197 +ey = P.eq_sound(py, qy, P.and_true_r(Nat.is_eq(px, qx), Nat.is_eq(py, qy), e))
198 %ex : {T.Pos{px, py} == T.Pos{_, qy} : T.Pos}
199 %ey : {T.Pos{px, py} == T.Pos{px, _} : T.Pos}
200 {==}
201
202def same_ne.go(+p: T.Pos, +q: T.Pos, ne: {p != q : T.Pos}, b: Bool,
203 e: {B.same(p, q) == b : Bool}) -> {B.same(p, q) == False{} : Bool}:
204 match b:
205 case False{}:
206 e
207 case True{}:
208 Empty.absurd({B.same(p, q) == False{} : Bool}, ne(same_sound(p, q, e)))
209
210law same_ne:
211 for +p: T.Pos
212 for +q: T.Pos
213 for ne: {p != q : T.Pos}
214 {B.same(p, q) == False{} : Bool}
215
216def same_ne(p, q, ne):
217 same_ne.go(p, q, ne, B.same(p, q), {==})
218
219law contains_cons_self:
220 for +p: T.Pos
221 for +xs: List<&2, T.Pos>
222 {B.contains(p <> xs, p) == True{} : Bool}
223
224def contains_cons_self(p, xs):
225 %Equal.sym(Bool, B.same(p, p), True{}, same_refl(p)) :
226 {Bool.or(_, B.contains(xs, p)) == True{} : Bool}
227 {==}
228
229def contains_remove_self.go(+q: T.Pos, +t: List<&2, T.Pos>, +p: T.Pos, +b: Bool,
230 +e: {B.same(q, p) == b : Bool},
231 ih: {B.contains(B.remove(t, p), p) == False{} : Bool}) ->
232 {B.contains(List.filter.put(T.Pos, q, B.remove(t, p), Bool.not(B.same(q, p))), p)
233 == False{} : Bool}:
234 match b:
235 case True{}:
236 %Equal.sym(Bool, B.same(q, p), True{}, e) :
237 {B.contains(List.filter.put(T.Pos, q, B.remove(t, p), Bool.not(_)), p) == False{} : Bool}
238 ih
239 case False{}:
240 %Equal.sym(Bool, B.same(q, p), False{}, e) :
241 {B.contains(List.filter.put(T.Pos, q, B.remove(t, p), Bool.not(_)), p) == False{} : Bool}
242 %Equal.sym(Bool, B.same(q, p), False{}, e) :
243 {Bool.or(_, B.contains(B.remove(t, p), p)) == False{} : Bool}
244 ih
245
246law contains_remove_self:
247 for +xs: List<&2, T.Pos>
248 for +p: T.Pos
249 {B.contains(B.remove(xs, p), p) == False{} : Bool}
250
251def contains_remove_self(xs, p):
252 match xs:
253 case Nil{}:
254 {==}
255 case q <> t:
256 contains_remove_self.go(q, t, p, B.same(q, p), {==}, contains_remove_self(t, p))
257
258def contains_remove_other.go(+e0: T.Pos, +t: List<&2, T.Pos>, +p: T.Pos, +q: T.Pos,
259 d: {B.same(p, q) == False{} : Bool}, +b: Bool, +e: {B.same(e0, p) == b : Bool},
260 ih: {B.contains(B.remove(t, p), q) == B.contains(t, q) : Bool}) ->
261 {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(B.same(e0, p))), q)
262 == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}:
263 match b:
264 case True{}:
265 %Equal.sym(Bool, B.same(e0, p), True{}, e) :
266 {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(_)), q)
267 == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}
268 %Equal.sym(T.Pos, e0, p, same_sound(e0, p, e)) :
269 {B.contains(B.remove(t, p), q) == Bool.or(B.same(_, q), B.contains(t, q)) : Bool}
270 %Equal.sym(Bool, B.same(p, q), False{}, d) :
271 {B.contains(B.remove(t, p), q) == Bool.or(_, B.contains(t, q)) : Bool}
272 ih
273 case False{}:
274 %Equal.sym(Bool, B.same(e0, p), False{}, e) :
275 {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(_)), q)
276 == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}
277 %ih : {Bool.or(B.same(e0, q), B.contains(B.remove(t, p), q))
278 == Bool.or(B.same(e0, q), _) : Bool}
279 {==}
280
281law contains_remove_other:
282 for +xs: List<&2, T.Pos>
283 for +p: T.Pos
284 for +q: T.Pos
285 for +d: {B.same(p, q) == False{} : Bool}
286 {B.contains(B.remove(xs, p), q) == B.contains(xs, q) : Bool}
287
288def contains_remove_other(xs, p, q, d):
289 match xs:
290 case Nil{}:
291 {==}
292 case e0 <> t:
293 contains_remove_other.go(e0, t, p, q, d, B.same(e0, p), {==},
294 contains_remove_other(t, p, q, d))
295
296def toggle_self.go(+flags: List<&2, T.Pos>, +p: T.Pos, +c: Bool,
297 e: {B.contains(flags, p) == c : Bool}) ->
298 {B.contains(G.toggle.go(c, flags, p), p) == Bool.not(c) : Bool}:
299 match c:
300 case True{}:
301 contains_remove_self(flags, p)
302 case False{}:
303 contains_cons_self(p, flags)
304
305
306law toggle_self:
307 for +flags: List<&2, T.Pos>
308 for +p: T.Pos
309 {B.contains(G.toggle(flags, p), p) == Bool.not(B.contains(flags, p)) : Bool}
310
311def toggle_self(flags, p):
312 toggle_self.go(flags, p, B.contains(flags, p), {==})
313
314def toggle_other.go(+flags: List<&2, T.Pos>, +p: T.Pos, +q: T.Pos,
315 d: {B.same(p, q) == False{} : Bool}, +c: Bool) ->
316 {B.contains(G.toggle.go(c, flags, p), q) == B.contains(flags, q) : Bool}:
317 match c:
318 case True{}:
319 contains_remove_other(flags, p, q, d)
320 case False{}:
321 %Equal.sym(Bool, B.same(p, q), False{}, d) :
322 {Bool.or(_, B.contains(flags, q)) == B.contains(flags, q) : Bool}
323 {==}
324
325
326law toggle_other:
327 for +flags: List<&2, T.Pos>
328 for +p: T.Pos
329 for +q: T.Pos
330 for +d: {B.same(p, q) == False{} : Bool}
331 {B.contains(G.toggle(flags, p), q) == B.contains(flags, q) : Bool}
332
333def toggle_other(flags, p, q, d):
334 toggle_other.go(flags, p, q, d, B.contains(flags, p))