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	# Lemmas about the knowledge the game builds.
9	
10	def 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	
17	def 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	
21	def 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	
28	def 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	
32	law 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	
45	def 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	
60	law 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	
72	def 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	# On the board, the knowledge shows what seen_at says.
87	law 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	
98	def 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	
115	law 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	
124	def 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	
133	def 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	# Hidden in the knowledge means on the board and not revealed in the game.
157	law 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	
168	def 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	# Cells and the flag list
174	# =======================
175	
176	law same_refl:
177	  for +p: T.Pos
178	  {B.same(p, p) == True{} : Bool}
179	
180	def 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	
187	law 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	
193	def 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	
202	def 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	
210	law 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	
216	def same_ne(p, q, ne):
217	  same_ne.go(p, q, ne, B.same(p, q), {==})
218	
219	law contains_cons_self:
220	  for +p: T.Pos
221	  for +xs: List<&2, T.Pos>
222	  {B.contains(p <> xs, p) == True{} : Bool}
223	
224	def 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	
229	def 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	
246	law 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	
251	def 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	
258	def 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	
281	law 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	
288	def 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	
296	def 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	# Toggling p flips whether p is in the list.
306	law 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	
311	def toggle_self(flags, p):
312	  toggle_self.go(flags, p, B.contains(flags, p), {==})
313	
314	def 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	# Toggling p leaves every other cell as it was.
326	law 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	
333	def toggle_other(flags, p, q, d):
334	  toggle_other.go(flags, p, q, d, B.contains(flags, p))