proof_copy.bend
minebender-game@1.0.0.0 · 364 lines · 25 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
10law at_eq:
11 for -A: Data
12 for +d: A
13 for +g: T.Grid(A)
14 for +p: T.Pos
15 {B.at(A, d, g, p) == L.at(A, d, g, p) : A}
16
17def at_eq(A, d, g, p):
18 match p:
19 case T.Pos{x, y}:
20 {==}
21
22law mine_eq:
23 for +layout: T.Grid(Bool)
24 for +p: T.Pos
25 {B.mine(layout, p) == L.mine(layout, p) : Bool}
26
27def mine_eq(layout, p):
28 match p:
29 case T.Pos{x, y}:
30 {==}
31
32law on_board_eq:
33 for +w: Nat
34 for +h: Nat
35 for +p: T.Pos
36 {B.on_board(w, h, p) == L.on_board(w, h, p) : Bool}
37
38def on_board_eq(w, h, p):
39 match p:
40 case T.Pos{x, y}:
41 {==}
42
43law same_eq:
44 for +p: T.Pos
45 for +q: T.Pos
46 {B.same(p, q) == L.same(p, q) : Bool}
47
48def same_eq(p, q):
49 match p q:
50 case T.Pos{px, py} T.Pos{qx, qy}:
51 {==}
52
53law adjacent_eq:
54 for +p: T.Pos
55 for +q: T.Pos
56 {B.adjacent(p, q) == L.adjacent(p, q) : Bool}
57
58def adjacent_eq(p, q):
59 match p q:
60 case T.Pos{px, py} T.Pos{qx, qy}:
61 {==}
62
63law row_cells_eq:
64 for +y: Nat
65 for +xs: List<&2, Nat>
66 {B.row_cells(y, xs) == L.row_cells(y, xs) : List<&2, T.Pos>}
67
68def row_cells_eq(y, xs):
69 match xs:
70 case Nil{}:
71 {==}
72 case x <> t:
73 %row_cells_eq(y, t) : {T.Pos{x, y} <> B.row_cells(y, t) == T.Pos{x, y} <> _ : List<&2, T.Pos>}
74 {==}
75
76law cells_go_eq:
77 for +w: Nat
78 for +ys: List<&2, Nat>
79 {B.cells.go(w, ys) == L.cells.go(w, ys) : List<&2, T.Pos>}
80
81def cells_go_eq(w, ys):
82 match ys:
83 case Nil{}:
84 {==}
85 case y <> t:
86 %row_cells_eq(y, List.range(w)) :
87 {List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t))
88 == List.append(&2, T.Pos, _, L.cells.go(w, t)) : List<&2, T.Pos>}
89 %cells_go_eq(w, t) :
90 {List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t))
91 == List.append(&2, T.Pos, B.row_cells(y, List.range(w)), _) : List<&2, T.Pos>}
92 {==}
93
94law cells_eq:
95 for +w: Nat
96 for +h: Nat
97 {B.cells(w, h) == L.cells(w, h) : List<&2, T.Pos>}
98
99def cells_eq(w, h):
100 cells_go_eq(w, List.range(h))
101
102law touching_eq:
103 for +p: T.Pos
104 for +qs: List<&2, T.Pos>
105 {B.touching(p, qs) == L.touching(p, qs) : List<&2, T.Pos>}
106
107def touching_eq(p, qs):
108 match qs:
109 case Nil{}:
110 {==}
111 case q <> t:
112 %adjacent_eq(p, q) :
113 {List.filter.put(T.Pos, q, B.touching(p, t), B.adjacent(p, q))
114 == List.filter.put(T.Pos, q, L.touching(p, t), _) : List<&2, T.Pos>}
115 %touching_eq(p, t) :
116 {List.filter.put(T.Pos, q, B.touching(p, t), B.adjacent(p, q))
117 == List.filter.put(T.Pos, q, _, B.adjacent(p, q)) : List<&2, T.Pos>}
118 {==}
119
120law neighbours_eq:
121 for +w: Nat
122 for +h: Nat
123 for +p: T.Pos
124 {B.neighbours(w, h, p) == L.neighbours(w, h, p) : List<&2, T.Pos>}
125
126def neighbours_eq(w, h, p):
127 %cells_eq(w, h) : {B.touching(p, B.cells(w, h)) == L.touching(p, _) : List<&2, T.Pos>}
128 touching_eq(p, B.cells(w, h))
129
130law count_mines_eq:
131 for +layout: T.Grid(Bool)
132 for +ps: List<&2, T.Pos>
133 {B.count_mines(layout, ps) == L.count_mines(layout, ps) : Nat}
134
135def count_mines_eq(layout, ps):
136 match ps:
137 case Nil{}:
138 {==}
139 case q <> t:
140 %mine_eq(layout, q) :
141 {Nat.add(Bool.pick(Nat, B.mine(layout, q), 1n, 0n), B.count_mines(layout, t))
142 == Nat.add(Bool.pick(Nat, _, 1n, 0n), L.count_mines(layout, t)) : Nat}
143 %count_mines_eq(layout, t) :
144 {Nat.add(Bool.pick(Nat, B.mine(layout, q), 1n, 0n), B.count_mines(layout, t))
145 == Nat.add(Bool.pick(Nat, B.mine(layout, q), 1n, 0n), _) : Nat}
146 {==}
147
148law adj_mines_eq:
149 for +w: Nat
150 for +h: Nat
151 for +layout: T.Grid(Bool)
152 for +p: T.Pos
153 {B.adj_mines(w, h, layout, p) == L.adj_mines(w, h, layout, p) : Nat}
154
155def adj_mines_eq(w, h, layout, p):
156 %neighbours_eq(w, h, p) :
157 {B.count_mines(layout, B.neighbours(w, h, p)) == L.count_mines(layout, _) : Nat}
158 count_mines_eq(layout, B.neighbours(w, h, p))
159
160law row_mines_eq:
161 for +row: List<&2, Bool>
162 {B.row_mines(row) == L.row_mines(row) : Nat}
163
164def row_mines_eq(row):
165 match row:
166 case Nil{}:
167 {==}
168 case b <> t:
169 %row_mines_eq(t) :
170 {Nat.add(Bool.pick(Nat, b, 1n, 0n), B.row_mines(t))
171 == Nat.add(Bool.pick(Nat, b, 1n, 0n), _) : Nat}
172 {==}
173
174law total_mines_eq:
175 for +layout: T.Grid(Bool)
176 {B.total_mines(layout) == L.total_mines(layout) : Nat}
177
178def total_mines_eq(layout):
179 match layout:
180 case Nil{}:
181 {==}
182 case r <> t:
183 %row_mines_eq(r) :
184 {Nat.add(B.row_mines(r), B.total_mines(t)) == Nat.add(_, L.total_mines(t)) : Nat}
185 %total_mines_eq(t) :
186 {Nat.add(B.row_mines(r), B.total_mines(t)) == Nat.add(B.row_mines(r), _) : Nat}
187 {==}
188
189law rows_wide_eq:
190 for -A: Data
191 for +w: Nat
192 for +g: T.Grid(A)
193 {B.rows_wide(A, w, g) == L.rows_wide(A, w, g) : Bool}
194
195def rows_wide_eq(A, w, g):
196 match g:
197 case Nil{}:
198 {==}
199 case r <> t:
200 %rows_wide_eq(A, w, t) :
201 {Bool.and(Nat.is_eq(List.length(&2, A, r), w), B.rows_wide(A, w, t))
202 == Bool.and(Nat.is_eq(List.length(&2, A, r), w), _) : Bool}
203 {==}
204
205law shaped_eq:
206 for -A: Data
207 for +w: Nat
208 for +h: Nat
209 for +g: T.Grid(A)
210 {B.shaped(A, w, h, g) == L.shaped(A, w, h, g) : Bool}
211
212def shaped_eq(A, w, h, g):
213 %rows_wide_eq(A, w, g) :
214 {Bool.and(Nat.is_eq(List.length(&2, List<&2, A>, g), h), B.rows_wide(A, w, g))
215 == Bool.and(Nat.is_eq(List.length(&2, List<&2, A>, g), h), _) : Bool}
216 {==}
217
218law zero_eq:
219 for +w: Nat
220 for +h: Nat
221 for +layout: T.Grid(Bool)
222 for +p: T.Pos
223 {B.zero(w, h, layout, p) == L.zero(w, h, layout, p) : Bool}
224
225def zero_eq(w, h, layout, p):
226 +nz = Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), 0n))
227 %on_board_eq(w, h, p) :
228 {Bool.and(Bool.and(B.on_board(w, h, p), Bool.not(B.mine(layout, p))),
229 Nat.is_eq(B.adj_mines(w, h, layout, p), 0n))
230 == Bool.and(Bool.and(_, Bool.not(L.mine(layout, p))),
231 Nat.is_eq(L.adj_mines(w, h, layout, p), 0n)) : Bool}
232 %mine_eq(layout, p) :
233 {Bool.and(Bool.and(B.on_board(w, h, p), Bool.not(B.mine(layout, p))),
234 Nat.is_eq(B.adj_mines(w, h, layout, p), 0n))
235 == Bool.and(Bool.and(B.on_board(w, h, p), Bool.not(_)),
236 Nat.is_eq(L.adj_mines(w, h, layout, p), 0n)) : Bool}
237 %adj_mines_eq(w, h, layout, p) :
238 {Bool.and(Bool.and(B.on_board(w, h, p), Bool.not(B.mine(layout, p))),
239 Nat.is_eq(B.adj_mines(w, h, layout, p), 0n))
240 == Bool.and(Bool.and(B.on_board(w, h, p), Bool.not(B.mine(layout, p))),
241 Nat.is_eq(_, 0n)) : Bool}
242 {==}
243
244law is_hidden_eq:
245 for +s: T.Seen
246 {G.is_hidden(s) == L.is_hidden(s) : Bool}
247
248def is_hidden_eq(s):
249 match s:
250 case T.Hidden{}:
251 {==}
252 case T.Shown{k}:
253 {==}
254 case T.Boom{}:
255 {==}
256
257law seen_eq:
258 for +v: T.Knowledge
259 for +p: T.Pos
260 {G.seen(v, p) == L.seen(v, p) : T.Seen}
261
262def seen_eq(v, p):
263 match v:
264 case T.Knowledge{w, h, n, rows}:
265 at_eq(T.Seen, T.Hidden{}, rows, p)
266
267law hidden_eq:
268 for +v: T.Knowledge
269 for +p: T.Pos
270 {G.hidden(v, p) == L.hidden(v, p) : Bool}
271
272def hidden_eq(v, p):
273 match v p:
274 case T.Knowledge{w, h, n, rows} T.Pos{x, y}:
275 %is_hidden_eq(B.at(T.Seen, T.Hidden{}, rows, T.Pos{x, y})) :
276 {G.hidden(T.Knowledge{w, h, n, rows}, T.Pos{x, y})
277 == Bool.and(B.on_board(w, h, T.Pos{x, y}), _) : Bool}
278 {==}
279
280law flags_among_eq:
281 for +g: G.Game
282 for +qs: List<&2, T.Pos>
283 {G.flags_among(g, qs) == L.flags_among(g, qs) : Nat}
284
285def flags_among_eq(g, qs):
286 match qs:
287 case Nil{}:
288 {==}
289 case q <> t:
290 %flags_among_eq(g, t) :
291 {Nat.add(Bool.pick(Nat, G.flagged(g, q), 1n, 0n), G.flags_among(g, t))
292 == Nat.add(Bool.pick(Nat, G.flagged(g, q), 1n, 0n), _) : Nat}
293 {==}
294
295law hidden_unflagged_eq:
296 for +g: G.Game
297 for +v: T.Knowledge
298 for +qs: List<&2, T.Pos>
299 {G.hidden_unflagged(g, v, qs) == L.hidden_unflagged(g, v, qs) : List<&2, T.Pos>}
300
301def hidden_unflagged_eq(g, v, qs):
302 match qs:
303 case Nil{}:
304 {==}
305 case q <> t:
306 %hidden_eq(v, q) :
307 {List.filter.put(T.Pos, q, G.hidden_unflagged(g, v, t),
308 Bool.and(G.hidden(v, q), Bool.not(G.flagged(g, q))))
309 == List.filter.put(T.Pos, q, L.hidden_unflagged(g, v, t),
310 Bool.and(_, Bool.not(G.flagged(g, q)))) : List<&2, T.Pos>}
311 %hidden_unflagged_eq(g, v, t) :
312 {List.filter.put(T.Pos, q, G.hidden_unflagged(g, v, t),
313 Bool.and(G.hidden(v, q), Bool.not(G.flagged(g, q))))
314 == List.filter.put(T.Pos, q, _,
315 Bool.and(G.hidden(v, q), Bool.not(G.flagged(g, q)))) : List<&2, T.Pos>}
316 {==}
317
318law chord_pick_eq:
319 for +g: G.Game
320 for +v: T.Knowledge
321 for +ns: List<&2, T.Pos>
322 for +s: T.Seen
323 {G.chord_targets.pick(g, v, ns, s) == L.chord_targets.pick(g, v, ns, s) : List<&2, T.Pos>}
324
325def chord_pick_eq(g, v, ns, s):
326 match s:
327 case T.Shown{k}:
328 %flags_among_eq(g, ns) :
329 {Bool.pick(List<&2, T.Pos>, Nat.is_eq(G.flags_among(g, ns), k),
330 G.hidden_unflagged(g, v, ns), Nil{})
331 == Bool.pick(List<&2, T.Pos>, Nat.is_eq(_, k),
332 L.hidden_unflagged(g, v, ns), Nil{}) : List<&2, T.Pos>}
333 %hidden_unflagged_eq(g, v, ns) :
334 {Bool.pick(List<&2, T.Pos>, Nat.is_eq(G.flags_among(g, ns), k),
335 G.hidden_unflagged(g, v, ns), Nil{})
336 == Bool.pick(List<&2, T.Pos>, Nat.is_eq(G.flags_among(g, ns), k),
337 _, Nil{}) : List<&2, T.Pos>}
338 {==}
339 case T.Hidden{}:
340 {==}
341 case T.Boom{}:
342 {==}
343
344def chord_targets_eq.go(+g: G.Game, +v: T.Knowledge, +p: T.Pos) ->
345 {G.chord_targets.go(g, v, p) == L.chord_targets.go(g, v, p) : List<&2, T.Pos>}:
346 match v:
347 case T.Knowledge{w, h, n, rows}:
348 +k = {T.Knowledge{w, h, n, rows} : T.Knowledge}
349 %neighbours_eq(w, h, p) :
350 {G.chord_targets.pick(g, k, B.neighbours(w, h, p), G.seen(k, p))
351 == L.chord_targets.pick(g, k, _, L.seen(k, p)) : List<&2, T.Pos>}
352 %seen_eq(k, p) :
353 {G.chord_targets.pick(g, k, B.neighbours(w, h, p), G.seen(k, p))
354 == L.chord_targets.pick(g, k, B.neighbours(w, h, p), _) : List<&2, T.Pos>}
355 chord_pick_eq(g, k, B.neighbours(w, h, p), G.seen(k, p))
356
357law chord_targets_eq:
358 for +g: G.Game
359 for +p: T.Pos
360 {G.chord_targets(g, p) == L.chord_targets(g, p) : List<&2, T.Pos>}
361
362def chord_targets_eq(g, p):
363 chord_targets_eq.go(g, G.knowledge(g), p)
364