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_gen.bend as PN
10	import ./proof_laws.bend as PW
11	import ./proof_assist.bend as PA
12	import ./proof_display.bend as PD
13	
14	# Proofs of the laws in LAWS.bend: `def L.name` proves `law name`.
15	
16	# Levels
17	# ======
18	
19	def L.level_beginner():
20	  {==}
21	
22	def L.level_intermediate():
23	  {==}
24	
25	def L.level_expert():
26	  {==}
27	
28	def L.level_custom(w, h, m):
29	  {==}
30	
31	# Finished games
32	# ==============
33	
34	def Bool.disc(b: Bool) -> Type:
35	  match b:
36	    case False{}:
37	      Unit
38	    case True{}:
39	      Empty
40	
41	def Bool.false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
42	  %e : Bool.disc(_)
43	  Unit{}
44	
45	# In a finished game, opening a cell changes nothing.
46	law open_over:
47	  for +g: G.Game
48	  for +p: T.Pos
49	  for +over: {G.is_playing(G.status(g)) == False{} : Bool}
50	  {G.open(g, p) == g : G.Game}
51	
52	def open_over(g, p, over):
53	  match g:
54	    case G.Game{w, h, layout, shown, flags, status}:
55	      %Equal.sym(Bool, G.is_playing(status), False{}, over) :
56	        {G.open.go(_ && G.unrevealed(w, h, shown, p), B.mine(layout, p),
57	          G.Game{w, h, layout, shown, flags, status}, p)
58	          == G.Game{w, h, layout, shown, flags, status} : G.Game}
59	      {==}
60	
61	law not_playing:
62	  for +s: T.Status
63	  for ne: {s != T.Playing{} : T.Status}
64	  {G.is_playing(s) == False{} : Bool}
65	
66	def not_playing(s, ne):
67	  match s:
68	    case T.Playing{}:
69	      Empty.absurd({G.is_playing(T.Playing{}) == False{} : Bool}, ne({==}))
70	    case T.Won{}:
71	      {==}
72	    case T.Lost{why}:
73	      {==}
74	
75	law reveal_go_same:
76	  for +b: Bool
77	  for +g: G.Game
78	  for +p: T.Pos
79	  for +e: {G.open(g, p) == g : G.Game}
80	  {G.reveal.go(b, g, p) == g : G.Game}
81	
82	def reveal_go_same(b, g, p, e):
83	  match b:
84	    case True{}:
85	      {==}
86	    case False{}:
87	      e
88	
89	law reveal_over:
90	  for +g: G.Game
91	  for +p: T.Pos
92	  for +over: {G.is_playing(G.status(g)) == False{} : Bool}
93	  {G.reveal(g, p) == g : G.Game}
94	
95	def reveal_over(g, p, over):
96	  reveal_go_same(G.flagged(g, p), g, p, open_over(g, p, over))
97	
98	law chord_over:
99	  for +ts: List<&2, T.Pos>
100	  for +g: G.Game
101	  for +over: {G.is_playing(G.status(g)) == False{} : Bool}
102	  {G.chord_play(ts, g) == g : G.Game}
103	
104	def chord_over(ts, g, over):
105	  match ts:
106	    case Nil{}:
107	      {==}
108	    case q <> t:
109	      %Equal.sym(G.Game, G.reveal(g, q), g, reveal_over(g, q, over)) :
110	        {G.chord_play(t, _) == g : G.Game}
111	      chord_over(t, g, over)
112	
113	law flag_over:
114	  for +g: G.Game
115	  for +p: T.Pos
116	  for +over: {G.is_playing(G.status(g)) == False{} : Bool}
117	  {G.flag(g, p) == g : G.Game}
118	
119	def flag_over(g, p, over):
120	  match g:
121	    case G.Game{w, h, layout, shown, flags, status}:
122	      %Equal.sym(Bool, G.is_playing(status), False{}, over) :
123	        {G.flag.go(_ && G.unrevealed(w, h, shown, p),
124	          G.Game{w, h, layout, shown, flags, status}, p)
125	          == G.Game{w, h, layout, shown, flags, status} : G.Game}
126	      {==}
127	
128	law assist_over:
129	  for +g: G.Game
130	  for +over: {G.is_playing(G.status(g)) == False{} : Bool}
131	  for +k: Nat
132	  {G.assist(g, k) == g : G.Game}
133	
134	def assist_over(g, over, k):
135	  %Equal.sym(Bool, G.is_playing(G.status(g)), False{}, over) :
136	    {G.assist.go(_, g, k) == g : G.Game}
137	  {==}
138	
139	law frozen_:
140	  for +g: G.Game
141	  for over: {G.status(g) != T.Playing{} : T.Status}
142	  for a: T.Action
143	  {G.step(g, a) == g : G.Game}
144	
145	def frozen_(g, over, a):
146	  match a:
147	    case T.Reveal{p}:
148	      reveal_over(g, p, not_playing(G.status(g), over))
149	    case T.Chord{p}:
150	      chord_over(G.chord_targets(g, p), g, not_playing(G.status(g), over))
151	    case T.Flag{p}:
152	      flag_over(g, p, not_playing(G.status(g), over))
153	    case T.Assist{k}:
154	      assist_over(g, not_playing(G.status(g), over), k)
155	
156	def L.frozen(g, over, a):
157	  frozen_(g, over, a)
158	
159	# Clicks
160	# ======
161	
162	law reveal_flagged_:
163	  for +g: G.Game
164	  for +p: T.Pos
165	  for +flag: {G.flagged(g, p) == True{} : Bool}
166	  {G.step(g, T.Reveal{p}) == g : G.Game}
167	
168	def reveal_flagged_(g, p, flag):
169	  %Equal.sym(Bool, G.flagged(g, p), True{}, flag) : {G.reveal.go(_, g, p) == g : G.Game}
170	  {==}
171	
172	def L.reveal_flagged(g, p, flag):
173	  reveal_flagged_(g, p, flag)
174	
175	law reveal_unflagged_:
176	  for +g: G.Game
177	  for +p: T.Pos
178	  for +flag: {G.flagged(g, p) == False{} : Bool}
179	  {G.step(g, T.Reveal{p}) == G.open(g, p) : G.Game}
180	
181	def reveal_unflagged_(g, p, flag):
182	  %Equal.sym(Bool, G.flagged(g, p), False{}, flag) :
183	    {G.reveal.go(_, g, p) == G.open(g, p) : G.Game}
184	  {==}
185	
186	def L.reveal_unflagged(g, p, flag):
187	  reveal_unflagged_(g, p, flag)
188	
189	# Flags
190	# =====
191	
192	def flag_k.go(+b: Bool, +g: G.Game, +p: T.Pos) ->
193	  {G.knowledge(G.flag.go(b, g, p)) == G.knowledge(g) : T.Knowledge}:
194	  match b:
195	    case False{}:
196	      {==}
197	    case True{}:
198	      match g:
199	        case G.Game{w, h, layout, shown, flags, status}:
200	          {==}
201	
202	def flag_s.go(+b: Bool, +g: G.Game, +p: T.Pos) ->
203	  {G.status(G.flag.go(b, g, p)) == G.status(g) : T.Status}:
204	  match b:
205	    case False{}:
206	      {==}
207	    case True{}:
208	      match g:
209	        case G.Game{w, h, layout, shown, flags, status}:
210	          {==}
211	
212	law flag_no_knowledge_:
213	  for +g: G.Game
214	  for +p: T.Pos
215	  {G.knowledge(G.step(g, T.Flag{p})) == G.knowledge(g) : T.Knowledge} &
216	  {G.status(G.step(g, T.Flag{p})) == G.status(g) : T.Status}
217	
218	def flag_no_knowledge_(g, p):
219	  (flag_k.go(G.can_flag(g, p), g, p), flag_s.go(G.can_flag(g, p), g, p))
220	
221	def L.flag_no_knowledge(g, p):
222	  flag_no_knowledge_(g, p)
223	
224	def status_disc_playing(s: T.Status) -> Type:
225	  match s:
226	    case T.Playing{}:
227	      Empty
228	    case o:
229	      Unit
230	
231	def won_ne_playing(e: {T.Won{} == T.Playing{} : T.Status}) -> Empty:
232	  %e : status_disc_playing(_)
233	  Unit{}
234	
235	def lost_ne_playing(-why: T.Loss, e: {T.Lost{why} == T.Playing{} : T.Status}) -> Empty:
236	  %e : status_disc_playing(_)
237	  Unit{}
238	
239	law flag_toggle_:
240	  for +g: G.Game
241	  for +playing: {G.status(g) == T.Playing{} : T.Status}
242	  for +p: T.Pos
243	  for +hid: {L.hidden(G.knowledge(g), p) == True{} : Bool}
244	  {G.flagged(G.step(g, T.Flag{p}), p) == Bool.not(G.flagged(g, p)) : Bool}
245	
246	def flag_toggle_(g, playing, p, hid):
247	  match g:
248	    case G.Game{w, h, layout, shown, flags, status}:
249	      match status:
250	        case T.Playing{}:
251	          +gg = {G.Game{w, h, layout, shown, flags, T.Playing{}} : G.Game}
252	          +u = Equal.trans(Bool, G.unrevealed(w, h, shown, p),
253	            L.hidden(G.knowledge(gg), p), True{},
254	            Equal.sym(Bool, L.hidden(G.knowledge(gg), p), G.unrevealed(w, h, shown, p),
255	              PG.know_hidden(w, h, layout, shown, flags, T.Playing{}, p)), hid)
256	          %Equal.sym(Bool, G.unrevealed(w, h, shown, p), True{}, u) :
257	            {G.flagged(G.flag.go(_, gg, p), p) == Bool.not(G.flagged(gg, p)) : Bool}
258	          %Equal.sym(Bool, G.unrevealed(w, h, shown, p), True{}, u) :
259	            {Bool.and(_, B.contains(G.toggle(flags, p), p))
260	              == Bool.not(Bool.and(_, B.contains(flags, p))) : Bool}
261	          PG.toggle_self(flags, p)
262	        case T.Won{}:
263	          Empty.absurd({G.flagged(G.step(G.Game{w, h, layout, shown, flags, T.Won{}}, T.Flag{p}), p)
264	            == Bool.not(G.flagged(G.Game{w, h, layout, shown, flags, T.Won{}}, p)) : Bool},
265	            won_ne_playing(playing))
266	        case T.Lost{why}:
267	          Empty.absurd({G.flagged(G.step(G.Game{w, h, layout, shown, flags, T.Lost{why}}, T.Flag{p}), p)
268	            == Bool.not(G.flagged(G.Game{w, h, layout, shown, flags, T.Lost{why}}, p)) : Bool},
269	            lost_ne_playing(why, playing))
270	
271	def L.flag_toggle(g, playing, p, hid):
272	  flag_toggle_(g, playing, p, hid)
273	
274	def flag_others.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos,
275	  d: {B.same(p, q) == False{} : Bool}) ->
276	  {G.flagged(G.flag.go(c, g, p), q) == G.flagged(g, q) : Bool}:
277	  match c:
278	    case False{}:
279	      {==}
280	    case True{}:
281	      match g:
282	        case G.Game{w, h, layout, shown, flags, status}:
283	          %Equal.sym(Bool, B.contains(G.toggle(flags, p), q), B.contains(flags, q),
284	            PG.toggle_other(flags, p, q, d)) :
285	            {Bool.and(G.unrevealed(w, h, shown, q), _)
286	              == Bool.and(G.unrevealed(w, h, shown, q), B.contains(flags, q)) : Bool}
287	          {==}
288	
289	law flag_others_:
290	  for +g: G.Game
291	  for +p: T.Pos
292	  for +q: T.Pos
293	  for diff: {p != q : T.Pos}
294	  {G.flagged(G.step(g, T.Flag{p}), q) == G.flagged(g, q) : Bool}
295	
296	def flag_others_(g, p, q, diff):
297	  flag_others.go(G.can_flag(g, p), g, p, q, PG.same_ne(p, q, diff))
298	
299	def L.flag_others(g, p, q, diff):
300	  flag_others_(g, p, q, diff)
301	
302	law flag_revealed_:
303	  for +g: G.Game
304	  for +p: T.Pos
305	  for +vis: {L.hidden(G.knowledge(g), p) == False{} : Bool}
306	  {G.step(g, T.Flag{p}) == g : G.Game}
307	
308	def flag_revealed_(g, p, vis):
309	  match g:
310	    case G.Game{w, h, layout, shown, flags, status}:
311	      +gg = {G.Game{w, h, layout, shown, flags, status} : G.Game}
312	      +u = Equal.trans(Bool, G.unrevealed(w, h, shown, p),
313	        L.hidden(G.knowledge(gg), p), False{},
314	        Equal.sym(Bool, L.hidden(G.knowledge(gg), p), G.unrevealed(w, h, shown, p),
315	          PG.know_hidden(w, h, layout, shown, flags, status, p)), vis)
316	      %Equal.sym(Bool, G.unrevealed(w, h, shown, p), False{}, u) :
317	        {G.flag.go(Bool.and(G.is_playing(status), _), gg, p) == gg : G.Game}
318	      %Equal.sym(Bool, Bool.and(G.is_playing(status), False{}), False{},
319	        P.and_false_r(G.is_playing(status))) :
320	        {G.flag.go(_, gg, p) == gg : G.Game}
321	      {==}
322	
323	def L.flag_revealed(g, p, vis):
324	  flag_revealed_(g, p, vis)
325	
326	# Chording
327	# ========
328	
329	law play_reveals:
330	  for +ts: List<&2, T.Pos>
331	  for +g: G.Game
332	  {G.chord_play(ts, g) == L.play(L.reveals(ts), g) : G.Game}
333	
334	def play_reveals(ts, g):
335	  match ts:
336	    case Nil{}:
337	      {==}
338	    case q <> t:
339	      play_reveals(t, G.reveal(g, q))
340	
341	law chord_:
342	  for +g: G.Game
343	  for +p: T.Pos
344	  {G.step(g, T.Chord{p}) == L.play(L.reveals(L.chord_targets(g, p)), g) : G.Game}
345	
346	def chord_(g, p):
347	  %PC.chord_targets_eq(g, p) :
348	    {G.chord_play(G.chord_targets(g, p), g) == L.play(L.reveals(_), g) : G.Game}
349	  play_reveals(G.chord_targets(g, p), g)
350	
351	def L.chord(g, p):
352	  chord_(g, p)
353	
354	# Board generation
355	# ================
356	
357	def L.gen_shape(w, h, n, first, rs):
358	  PN.gen_shape_(w, h, n, first, rs)
359	
360	def L.gen_count(w, h, n, first, rs, on, fits):
361	  PN.gen_count_(w, h, n, first, rs, on, fits)
362	
363	def L.gen_first_safe(w, h, n, first, rs):
364	  PN.gen_first_safe_(w, h, n, first, rs)
365	
366	def L.gen_opening(w, h, n, first, rs, room, q, near):
367	  PN.gen_opening_(w, h, n, first, rs, room, q, near)
368	
369	# The real board, winning and flags
370	# =================================
371	
372	def L.bridge(w, h, layout, shape, g, r):
373	  PW.bridge_(w, h, layout, shape, g, r)
374	
375	def L.won_iff(w, h, layout, shape, g, r):
376	  PW.won_iff_(w, h, layout, shape, g, r)
377	
378	def L.flags_hidden(w, h, layout, shape, g, r, q, flag):
379	  PW.flags_hidden_(g, q, flag)
380	
381	def L.monotone(w, h, layout, shape, g, r, a, q, vis):
382	  PW.monotone_(w, h, layout, shape, g, r, a, q, vis)
383	
384	# Revealing
385	# =========
386	
387	def L.open_mine(w, h, layout, shape, g, r, playing, p, boom):
388	  PW.open_mine_(w, h, layout, shape, g, r, playing, p, boom)
389	
390	def L.open_safe(w, h, layout, shape, g, r, playing, p, safe):
391	  PW.open_safe_(w, h, layout, shape, g, r, playing, p, safe)
392	
393	def L.flood_complete(w, h, layout, shape, g, r, playing, p, on, q, path, walk):
394	  PW.flood_complete_(w, h, layout, shape, g, r, playing, p, on, q, path, walk)
395	
396	def L.flood_exact(w, h, layout, shape, g, r, playing, p, q, before, after):
397	  PW.flood_exact_(w, h, layout, shape, g, r, playing, p, q, before, after)
398	
399	# The no-guess assist
400	# ===================
401	
402	def L.assist_stuck(w, h, layout, shape, g, r, playing, stuck, k):
403	  PA.assist_stuck_(w, h, layout, shape, g, r, playing, stuck, k)
404	
405	def L.assist_too_early(w, h, layout, shape, g, r, playing, q, option, k):
406	  PA.assist_too_early_(w, h, layout, shape, g, r, playing, q, option, k)
407	
408	# The display
409	# ===========
410	
411	def L.display_play(w, h, layout, shape, g, r, playing, p, on):
412	  PD.display_play_(w, h, layout, shape, g, r, playing, p, on)
413	
414	def L.display_blast(w, h, layout, shape, g, r, p, lost, on):
415	  PD.display_blast_(w, h, layout, shape, g, r, p, lost, on)
416	
417	def L.display_hint(w, h, layout, shape, g, r, s, lost, on):
418	  PD.display_hint_(w, h, layout, shape, g, r, s, lost, on)
419	
420	def L.display_mines(w, h, layout, shape, g, r, over, q, on, m):
421	  PD.display_mines_(w, h, layout, shape, g, r, over, q, on, m)