proof_walk.bend
minebender-game@1.0.0.0 · 209 lines · 13 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/LAWS.bend as L
5import minebender-game@1.0.0.0/proof_base.bend as P
6import minebender-game@1.0.0.0/proof_grid.bend as PG
7import minebender-game@1.0.0.0/proof_copy.bend as PC
8import minebender-game@1.0.0.0/proof_cells.bend as PS
9
10
11
12def and4(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> Bool:
13 Bool.and(Bool.and(Bool.and(a, b), c), d)
14
15law 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
23def and4_d(a, b, c, d, e):
24 P.and_true_r(Bool.and(Bool.and(a, b), c), d, e)
25
26law 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
34def 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
37law 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
45def 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
48law 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
56def 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
59law 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
70def 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
76law 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
82def 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
86law lsame_refl:
87 for +p: T.Pos
88 {L.same(p, p) == True{} : Bool}
89
90def lsame_refl(p):
91 %PC.same_eq(p, p) : {_ == True{} : Bool}
92 PG.same_refl(p)
93
94
95law 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
109def 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
126law 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
132def 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
145law 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
151def rev_cons(A, r, back):
152 rev_acc(A, back, [r])
153
154
155law 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
166def 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
179law 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
190def 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)