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	
8	# The game's copies of definitions in LAWS.bend equal the originals.
9	
10	law 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	
17	def at_eq(A, d, g, p):
18	  match p:
19	    case T.Pos{x, y}:
20	      {==}
21	
22	law mine_eq:
23	  for +layout: T.Grid(Bool)
24	  for +p: T.Pos
25	  {B.mine(layout, p) == L.mine(layout, p) : Bool}
26	
27	def mine_eq(layout, p):
28	  match p:
29	    case T.Pos{x, y}:
30	      {==}
31	
32	law 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	
38	def on_board_eq(w, h, p):
39	  match p:
40	    case T.Pos{x, y}:
41	      {==}
42	
43	law same_eq:
44	  for +p: T.Pos
45	  for +q: T.Pos
46	  {B.same(p, q) == L.same(p, q) : Bool}
47	
48	def same_eq(p, q):
49	  match p q:
50	    case T.Pos{px, py} T.Pos{qx, qy}:
51	      {==}
52	
53	law adjacent_eq:
54	  for +p: T.Pos
55	  for +q: T.Pos
56	  {B.adjacent(p, q) == L.adjacent(p, q) : Bool}
57	
58	def adjacent_eq(p, q):
59	  match p q:
60	    case T.Pos{px, py} T.Pos{qx, qy}:
61	      {==}
62	
63	law 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	
68	def 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	
76	law 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	
81	def 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	
94	law cells_eq:
95	  for +w: Nat
96	  for +h: Nat
97	  {B.cells(w, h) == L.cells(w, h) : List<&2, T.Pos>}
98	
99	def cells_eq(w, h):
100	  cells_go_eq(w, List.range(h))
101	
102	law 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	
107	def 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	
120	law 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	
126	def 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	
130	law 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	
135	def 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	
148	law 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	
155	def 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	
160	law row_mines_eq:
161	  for +row: List<&2, Bool>
162	  {B.row_mines(row) == L.row_mines(row) : Nat}
163	
164	def 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	
174	law total_mines_eq:
175	  for +layout: T.Grid(Bool)
176	  {B.total_mines(layout) == L.total_mines(layout) : Nat}
177	
178	def 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	
189	law 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	
195	def 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	
205	law 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	
212	def 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	
218	law 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	
225	def 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	
244	law is_hidden_eq:
245	  for +s: T.Seen
246	  {G.is_hidden(s) == L.is_hidden(s) : Bool}
247	
248	def is_hidden_eq(s):
249	  match s:
250	    case T.Hidden{}:
251	      {==}
252	    case T.Shown{k}:
253	      {==}
254	    case T.Boom{}:
255	      {==}
256	
257	law seen_eq:
258	  for +v: T.Knowledge
259	  for +p: T.Pos
260	  {G.seen(v, p) == L.seen(v, p) : T.Seen}
261	
262	def 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	
267	law hidden_eq:
268	  for +v: T.Knowledge
269	  for +p: T.Pos
270	  {G.hidden(v, p) == L.hidden(v, p) : Bool}
271	
272	def 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	
280	law 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	
285	def 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	
295	law 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	
301	def 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	
318	law 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	
325	def 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	
344	def 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	
357	law 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	
362	def chord_targets_eq(g, p):
363	  chord_targets_eq.go(g, G.knowledge(g), p)
364