1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./LAWS.bend as L
5	import ./proof_base.bend as P
6	import ./proof_grid.bend as PG
7	import ./proof_copy.bend as PC
8	import ./proof_cells.bend as PS
9	
10	# Lemmas about zero walks (LAWS.bend's zero_walk).
11	
12	def and4(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> Bool:
13	  Bool.and(Bool.and(Bool.and(a, b), c), d)
14	
15	law and4_d:
16	  for +a: Bool
17	  for +b: Bool
18	  for +c: Bool
19	  for +d: Bool
20	  for e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}
21	  {d == True{} : Bool}
22	
23	def and4_d(a, b, c, d, e):
24	  P.and_true_r(Bool.and(Bool.and(a, b), c), d, e)
25	
26	law and4_c:
27	  for +a: Bool
28	  for +b: Bool
29	  for +c: Bool
30	  for +d: Bool
31	  for e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}
32	  {c == True{} : Bool}
33	
34	def and4_c(a, b, c, d, e):
35	  P.and_true_r(Bool.and(a, b), c, P.and_true_l(Bool.and(Bool.and(a, b), c), d, e))
36	
37	law and4_b:
38	  for +a: Bool
39	  for +b: Bool
40	  for +c: Bool
41	  for +d: Bool
42	  for e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}
43	  {b == True{} : Bool}
44	
45	def and4_b(a, b, c, d, e):
46	  P.and_true_r(a, b, P.and_true_l(Bool.and(a, b), c, P.and_true_l(Bool.and(Bool.and(a, b), c), d, e)))
47	
48	law and4_a:
49	  for +a: Bool
50	  for +b: Bool
51	  for +c: Bool
52	  for +d: Bool
53	  for e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}
54	  {a == True{} : Bool}
55	
56	def and4_a(a, b, c, d, e):
57	  P.and_true_l(a, b, P.and_true_l(Bool.and(a, b), c, P.and_true_l(Bool.and(Bool.and(a, b), c), d, e)))
58	
59	law and4_intro:
60	  for +a: Bool
61	  for +b: Bool
62	  for +c: Bool
63	  for +d: Bool
64	  for ea: {a == True{} : Bool}
65	  for eb: {b == True{} : Bool}
66	  for ec: {c == True{} : Bool}
67	  for ed: {d == True{} : Bool}
68	  {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}
69	
70	def and4_intro(a, b, c, d, ea, eb, ec, ed):
71	  %Equal.sym(Bool, a, True{}, ea) : {Bool.and(Bool.and(Bool.and(_, b), c), d) == True{} : Bool}
72	  %Equal.sym(Bool, b, True{}, eb) : {Bool.and(Bool.and(Bool.and(True{}, _), c), d) == True{} : Bool}
73	  %Equal.sym(Bool, c, True{}, ec) : {Bool.and(Bool.and(True{}, _), d) == True{} : Bool}
74	  ed
75	
76	law lsame_sound:
77	  for +p: T.Pos
78	  for +q: T.Pos
79	  for e: {L.same(p, q) == True{} : Bool}
80	  {p == q : T.Pos}
81	
82	def lsame_sound(p, q, e):
83	  PG.same_sound(p, q, %Equal.sym(Bool, B.same(p, q), L.same(p, q), PC.same_eq(p, q)) :
84	    {_ == True{} : Bool}; e)
85	
86	law lsame_refl:
87	  for +p: T.Pos
88	  {L.same(p, p) == True{} : Bool}
89	
90	def lsame_refl(p):
91	  %PC.same_eq(p, p) : {_ == True{} : Bool}
92	  PG.same_refl(p)
93	
94	# Extending a walk to c by one step from c (a zero) to r.
95	law walk_snoc:
96	  for +path: List<&2, T.Pos>
97	  for +w: Nat
98	  for +h: Nat
99	  for +layout: T.Grid(Bool)
100	  for +p: T.Pos
101	  for +c: T.Pos
102	  for +r: T.Pos
103	  for +wk: {L.zero_walk(path, w, h, layout, p, c) == True{} : Bool}
104	  for +z: {L.zero(w, h, layout, c) == True{} : Bool}
105	  for +a: {L.adjacent(c, r) == True{} : Bool}
106	  for +on: {L.on_board(w, h, r) == True{} : Bool}
107	  {L.zero_walk(List.append(&2, T.Pos, path, [r]), w, h, layout, p, r) == True{} : Bool}
108	
109	def walk_snoc(path, w, h, layout, p, c, r, wk, z, a, on):
110	  match path:
111	    case Nil{}:
112	      %Equal.sym(T.Pos, p, c, lsame_sound(p, c, wk)) :
113	        {Bool.and(Bool.and(Bool.and(L.zero(w, h, layout, _), L.adjacent(_, r)), L.on_board(w, h, r)),
114	          L.zero_walk(Nil{}, w, h, layout, r, r)) == True{} : Bool}
115	      and4_intro(L.zero(w, h, layout, c), L.adjacent(c, r), L.on_board(w, h, r), L.same(r, r),
116	        z, a, on, lsame_refl(r))
117	    case s <> t:
118	      +zp = L.zero(w, h, layout, p)
119	      +ps = L.adjacent(p, s)
120	      +os = L.on_board(w, h, s)
121	      +rest = L.zero_walk(t, w, h, layout, s, c)
122	      and4_intro(zp, ps, os, L.zero_walk(List.append(&2, T.Pos, t, [r]), w, h, layout, s, r),
123	        and4_a(zp, ps, os, rest, wk), and4_b(zp, ps, os, rest, wk), and4_c(zp, ps, os, rest, wk),
124	        walk_snoc(t, w, h, layout, s, c, r, and4_d(zp, ps, os, rest, wk), z, a, on))
125	
126	law rev_acc:
127	  for -A: Data
128	  for +xs: List<&2, A>
129	  for +acc: List<&2, A>
130	  {List.reverse.go(&2, A, xs, acc) == List.append(&2, A, List.reverse.go(&2, A, xs, Nil{}), acc) : List<&2, A>}
131	
132	def rev_acc(A, xs, acc):
133	  match xs:
134	    case Nil{}:
135	      {==}
136	    case x <> t:
137	      +r = List.reverse.go(&2, A, t, Nil{})
138	      %Equal.sym(List<&2, A>, List.reverse.go(&2, A, t, [x]), List.append(&2, A, r, [x]), rev_acc(A, t, [x])) :
139	        {List.reverse.go(&2, A, t, x <> acc) == List.append(&2, A, _, acc) : List<&2, A>}
140	      %Equal.sym(List<&2, A>, List.append(&2, A, List.append(&2, A, r, [x]), acc), List.append(&2, A, r, x <> acc),
141	        P.append_assoc(A, r, [x], acc)) :
142	        {List.reverse.go(&2, A, t, x <> acc) == _ : List<&2, A>}
143	      rev_acc(A, t, x <> acc)
144	
145	law rev_cons:
146	  for -A: Data
147	  for +r: A
148	  for +back: List<&2, A>
149	  {List.reverse(&2, A, r <> back) == List.append(&2, A, List.reverse(&2, A, back), [r]) : List<&2, A>}
150	
151	def rev_cons(A, r, back):
152	  rev_acc(A, back, [r])
153	
154	# A walk ends on the board when it starts there.
155	law walk_on:
156	  for +path: List<&2, T.Pos>
157	  for +w: Nat
158	  for +h: Nat
159	  for +layout: T.Grid(Bool)
160	  for +s: T.Pos
161	  for +q: T.Pos
162	  for +wk: {L.zero_walk(path, w, h, layout, s, q) == True{} : Bool}
163	  for +on: {L.on_board(w, h, s) == True{} : Bool}
164	  {L.on_board(w, h, q) == True{} : Bool}
165	
166	def walk_on(path, w, h, layout, s, q, wk, on):
167	  match path:
168	    case Nil{}:
169	      %lsame_sound(s, q, wk) : {L.on_board(w, h, _) == True{} : Bool}
170	      on
171	    case r <> t:
172	      +zs = L.zero(w, h, layout, s)
173	      +sr = L.adjacent(s, r)
174	      +orr = L.on_board(w, h, r)
175	      +rest = L.zero_walk(t, w, h, layout, r, q)
176	      walk_on(t, w, h, layout, r, q, and4_d(zs, sr, orr, rest, wk), and4_c(zs, sr, orr, rest, wk))
177	
178	# A walk from a safe cell only reaches safe cells.
179	law walk_safe:
180	  for +path: List<&2, T.Pos>
181	  for +w: Nat
182	  for +h: Nat
183	  for +layout: T.Grid(Bool)
184	  for +s: T.Pos
185	  for +q: T.Pos
186	  for +wk: {L.zero_walk(path, w, h, layout, s, q) == True{} : Bool}
187	  for +safe: {L.mine(layout, s) == False{} : Bool}
188	  {L.mine(layout, q) == False{} : Bool}
189	
190	def walk_safe(path, w, h, layout, s, q, wk, safe):
191	  match path:
192	    case Nil{}:
193	      %lsame_sound(s, q, wk) : {L.mine(layout, _) == False{} : Bool}
194	      safe
195	    case r <> t:
196	      +zs = L.zero(w, h, layout, s)
197	      +sr = L.adjacent(s, r)
198	      +orr = L.on_board(w, h, r)
199	      +rest = L.zero_walk(t, w, h, layout, r, q)
200	      +m = PS.neighbours_member(w, h, s, r,
201	        %Equal.sym(Bool, B.on_board(w, h, r), L.on_board(w, h, r), PC.on_board_eq(w, h, r)) :
202	          {_ == True{} : Bool}; and4_c(zs, sr, orr, rest, wk),
203	        %Equal.sym(Bool, B.adjacent(s, r), L.adjacent(s, r), PC.adjacent_eq(s, r)) :
204	          {_ == True{} : Bool}; and4_b(zs, sr, orr, rest, wk))
205	      +safe_r = PS.zero_nbr(w, h, layout, s, r,
206	        %Equal.sym(Bool, B.zero(w, h, layout, s), L.zero(w, h, layout, s), PC.zero_eq(w, h, layout, s)) :
207	          {_ == True{} : Bool}; and4_a(zs, sr, orr, rest, wk), m)
208	      walk_safe(t, w, h, layout, r, q, and4_d(zs, sr, orr, rest, wk),
209	        %PC.mine_eq(layout, r) : {_ == False{} : Bool}; safe_r)