proof_sums.bend

minebender-game@1.0.0.0 · 274 lines · 15 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/proof_base.bend as P
5import minebender-game@1.0.0.0/proof_lists.bend as PL
6
7# Summing a value over a grid, row by row, equals summing it over the
8# board's cells, cell by cell.
9
10# Each element plus one.
11def smap(xs: List<&2, Nat>) -> List<&2, Nat>:
12  match xs:
13    case Nil{}:
14      Nil{}
15    case x <> t:
16      (1n+x) <> smap(t)
17
18law map_append:
19  for +xs: List<&2, Nat>
20  for +ys: List<&2, Nat>
21  {smap(List.append(&2, Nat, xs, ys))
22    == List.append(&2, Nat, smap(xs), smap(ys)) : List<&2, Nat>}
23
24def map_append(xs, ys):
25  match xs:
26    case Nil{}:
27      {==}
28    case x <> t:
29      %Equal.sym(List<&2, Nat>, smap(List.append(&2, Nat, t, ys)),
30        List.append(&2, Nat, smap(t), smap(ys)), map_append(t, ys)) :
31        {(1n+x) <> _ == (1n+x) <> List.append(&2, Nat, smap(t), smap(ys))
32          : List<&2, Nat>}
33      {==}
34
35# range(1+n) is 0 followed by 1..n.
36law range_cons:
37  for +n: Nat
38  {List.range(1n+n) == 0n <> smap(List.range(n)) : List<&2, Nat>}
39
40def range_cons(n):
41  match n:
42    case 0n:
43      {==}
44    case 1n+m:
45      %Equal.sym(List<&2, Nat>, List.range(2n+m), List.append(&2, Nat, List.range(1n+m), [1n+m]), P.range_snoc(1n+m)) :
46        {_ == 0n <> smap(List.range(1n+m)) : List<&2, Nat>}
47      %Equal.sym(List<&2, Nat>, List.range(1n+m), 0n <> smap(List.range(m)), range_cons(m)) :
48        {List.append(&2, Nat, _, [1n+m]) == 0n <> smap(List.range(1n+m)) : List<&2, Nat>}
49      %Equal.sym(List<&2, Nat>, List.range(1n+m), List.append(&2, Nat, List.range(m), [m]), P.range_snoc(m)) :
50        {List.append(&2, Nat, 0n <> smap(List.range(m)), [1n+m]) == 0n <> smap(_) : List<&2, Nat>}
51      %Equal.sym(List<&2, Nat>, smap(List.append(&2, Nat, List.range(m), [m])),
52        List.append(&2, Nat, smap(List.range(m)), smap([m])), map_append(List.range(m), [m])) :
53        {List.append(&2, Nat, 0n <> smap(List.range(m)), [1n+m]) == 0n <> _ : List<&2, Nat>}
54      {==}
55
56def rsum(~A: Data, ~f: A -> Nat, r: List<&2, A>) -> Nat:
57  match r:
58    case Nil{}:
59      0n
60    case a <> t:
61      Nat.add(f(a), rsum(~A, ~f, t))
62
63# The sum of f over the grid, row by row.
64def gsum(~A: Data, ~f: A -> Nat, g: T.Grid(A)) -> Nat:
65  match g:
66    case Nil{}:
67      0n
68    case r <> t:
69      Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, t))
70
71# The sum of f over the cells ps of the grid.
72def csum(~A: Data, ~f: A -> Nat, +d: A, +g: T.Grid(A), ps: List<&2, T.Pos>) -> Nat:
73  match ps:
74    case Nil{}:
75      0n
76    case q <> t:
77      Nat.add(f(B.at(A, d, g, q)), csum(~A, ~f, d, g, t))
78
79def rsum_at(~A: Data, ~f: A -> Nat, +d: A, +r: List<&2, A>, xs: List<&2, Nat>) -> Nat:
80  match xs:
81    case Nil{}:
82      0n
83    case x <> t:
84      Nat.add(f(Maybe.default(&2, A, List.get(&2, A, r, x), d)), rsum_at(~A, ~f, d, r, t))
85
86law csum_append:
87  for ~A: Data
88  for ~f: A -> Nat
89  for +d: A
90  for +g: T.Grid(A)
91  for +xs: List<&2, T.Pos>
92  for +ys: List<&2, T.Pos>
93  {csum(~A, ~f, d, g, List.append(&2, T.Pos, xs, ys)) == Nat.add(csum(~A, ~f, d, g, xs), csum(~A, ~f, d, g, ys)) : Nat}
94
95def csum_append(A, f, d, g, xs, ys):
96  match xs:
97    case Nil{}:
98      {==}
99    case q <> t:
100      %Equal.sym(Nat, csum(~A, ~f, d, g, List.append(&2, T.Pos, t, ys)),
101        Nat.add(csum(~A, ~f, d, g, t), csum(~A, ~f, d, g, ys)), csum_append(~A, ~f, d, g, t, ys)) :
102        {Nat.add(f(B.at(A, d, g, q)), _) == Nat.add(Nat.add(f(B.at(A, d, g, q)), csum(~A, ~f, d, g, t)), csum(~A, ~f, d, g, ys)) : Nat}
103      Equal.sym(Nat, Nat.add(Nat.add(f(B.at(A, d, g, q)), csum(~A, ~f, d, g, t)), csum(~A, ~f, d, g, ys)),
104        Nat.add(f(B.at(A, d, g, q)), Nat.add(csum(~A, ~f, d, g, t), csum(~A, ~f, d, g, ys))),
105        P.add_assoc(f(B.at(A, d, g, q)), csum(~A, ~f, d, g, t), csum(~A, ~f, d, g, ys)))
106
107law csum_row0:
108  for ~A: Data
109  for ~f: A -> Nat
110  for +d: A
111  for +r: List<&2, A>
112  for +rt: T.Grid(A)
113  for +xs: List<&2, Nat>
114  {csum(~A, ~f, d, r <> rt, B.row_cells(0n, xs)) == rsum_at(~A, ~f, d, r, xs) : Nat}
115
116def csum_row0(A, f, d, r, rt, xs):
117  match xs:
118    case Nil{}:
119      {==}
120    case x <> t:
121      %Equal.sym(Nat, csum(~A, ~f, d, r <> rt, B.row_cells(0n, t)), rsum_at(~A, ~f, d, r, t), csum_row0(~A, ~f, d, r, rt, t)) :
122        {Nat.add(f(Maybe.default(&2, A, List.get(&2, A, r, x), d)), _)
123          == Nat.add(f(Maybe.default(&2, A, List.get(&2, A, r, x), d)), rsum_at(~A, ~f, d, r, t)) : Nat}
124      {==}
125
126law csum_row_shift:
127  for ~A: Data
128  for ~f: A -> Nat
129  for +d: A
130  for +r: List<&2, A>
131  for +rt: T.Grid(A)
132  for +y: Nat
133  for +xs: List<&2, Nat>
134  {csum(~A, ~f, d, r <> rt, B.row_cells(1n+y, xs)) == csum(~A, ~f, d, rt, B.row_cells(y, xs)) : Nat}
135
136def csum_row_shift(A, f, d, r, rt, y, xs):
137  match xs:
138    case Nil{}:
139      {==}
140    case x <> t:
141      %Equal.sym(Nat, csum(~A, ~f, d, r <> rt, B.row_cells(1n+y, t)), csum(~A, ~f, d, rt, B.row_cells(y, t)),
142        csum_row_shift(~A, ~f, d, r, rt, y, t)) :
143        {Nat.add(f(B.at(A, d, rt, T.Pos{x, y})), _) == Nat.add(f(B.at(A, d, rt, T.Pos{x, y})), csum(~A, ~f, d, rt, B.row_cells(y, t))) : Nat}
144      {==}
145
146law csum_shift:
147  for ~A: Data
148  for ~f: A -> Nat
149  for +d: A
150  for +r: List<&2, A>
151  for +rt: T.Grid(A)
152  for +w: Nat
153  for +ys: List<&2, Nat>
154  {csum(~A, ~f, d, r <> rt, B.cells.go(w, smap(ys))) == csum(~A, ~f, d, rt, B.cells.go(w, ys)) : Nat}
155
156def csum_shift(A, f, d, r, rt, w, ys):
157  match ys:
158    case Nil{}:
159      {==}
160    case y <> t:
161      +g = {r <> rt : T.Grid(A)}
162      %Equal.sym(Nat, csum(~A, ~f, d, g, List.append(&2, T.Pos, B.row_cells(1n+y, List.range(w)), B.cells.go(w, smap(t)))),
163        Nat.add(csum(~A, ~f, d, g, B.row_cells(1n+y, List.range(w))), csum(~A, ~f, d, g, B.cells.go(w, smap(t)))),
164        csum_append(~A, ~f, d, g, B.row_cells(1n+y, List.range(w)), B.cells.go(w, smap(t)))) :
165        {_ == csum(~A, ~f, d, rt, List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t))) : Nat}
166      %Equal.sym(Nat, csum(~A, ~f, d, rt, List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t))),
167        Nat.add(csum(~A, ~f, d, rt, B.row_cells(y, List.range(w))), csum(~A, ~f, d, rt, B.cells.go(w, t))),
168        csum_append(~A, ~f, d, rt, B.row_cells(y, List.range(w)), B.cells.go(w, t))) :
169        {Nat.add(csum(~A, ~f, d, g, B.row_cells(1n+y, List.range(w))), csum(~A, ~f, d, g, B.cells.go(w, smap(t)))) == _ : Nat}
170      %Equal.sym(Nat, csum(~A, ~f, d, g, B.row_cells(1n+y, List.range(w))), csum(~A, ~f, d, rt, B.row_cells(y, List.range(w))),
171        csum_row_shift(~A, ~f, d, r, rt, y, List.range(w))) :
172        {Nat.add(_, csum(~A, ~f, d, g, B.cells.go(w, smap(t))))
173          == Nat.add(csum(~A, ~f, d, rt, B.row_cells(y, List.range(w))), csum(~A, ~f, d, rt, B.cells.go(w, t))) : Nat}
174      %Equal.sym(Nat, csum(~A, ~f, d, g, B.cells.go(w, smap(t))), csum(~A, ~f, d, rt, B.cells.go(w, t)),
175        csum_shift(~A, ~f, d, r, rt, w, t)) :
176        {Nat.add(csum(~A, ~f, d, rt, B.row_cells(y, List.range(w))), _)
177          == Nat.add(csum(~A, ~f, d, rt, B.row_cells(y, List.range(w))), csum(~A, ~f, d, rt, B.cells.go(w, t))) : Nat}
178      {==}
179
180law rsum_at_shift:
181  for ~A: Data
182  for ~f: A -> Nat
183  for +d: A
184  for +a: A
185  for +t: List<&2, A>
186  for +xs: List<&2, Nat>
187  {rsum_at(~A, ~f, d, a <> t, smap(xs)) == rsum_at(~A, ~f, d, t, xs) : Nat}
188
189def rsum_at_shift(A, f, d, a, t, xs):
190  match xs:
191    case Nil{}:
192      {==}
193    case x <> u:
194      %Equal.sym(Nat, rsum_at(~A, ~f, d, a <> t, smap(u)), rsum_at(~A, ~f, d, t, u), rsum_at_shift(~A, ~f, d, a, t, u)) :
195        {Nat.add(f(Maybe.default(&2, A, List.get(&2, A, t, x), d)), _)
196          == Nat.add(f(Maybe.default(&2, A, List.get(&2, A, t, x), d)), rsum_at(~A, ~f, d, t, u)) : Nat}
197      {==}
198
199law rsum_at_full:
200  for ~A: Data
201  for ~f: A -> Nat
202  for +d: A
203  for +r: List<&2, A>
204  {rsum_at(~A, ~f, d, r, List.range(List.length(&2, A, r))) == rsum(~A, ~f, r) : Nat}
205
206def rsum_at_full(A, f, d, r):
207  match r:
208    case Nil{}:
209      {==}
210    case a <> t:
211      %Equal.sym(List<&2, Nat>, List.range(1n+List.length(&2, A, t)), 0n <> smap(List.range(List.length(&2, A, t))),
212        range_cons(List.length(&2, A, t))) :
213        {rsum_at(~A, ~f, d, a <> t, _) == Nat.add(f(a), rsum(~A, ~f, t)) : Nat}
214      %Equal.sym(Nat, rsum_at(~A, ~f, d, a <> t, smap(List.range(List.length(&2, A, t)))),
215        rsum_at(~A, ~f, d, t, List.range(List.length(&2, A, t))),
216        rsum_at_shift(~A, ~f, d, a, t, List.range(List.length(&2, A, t)))) :
217        {Nat.add(f(a), _) == Nat.add(f(a), rsum(~A, ~f, t)) : Nat}
218      %Equal.sym(Nat, rsum_at(~A, ~f, d, t, List.range(List.length(&2, A, t))), rsum(~A, ~f, t), rsum_at_full(~A, ~f, d, t)) :
219        {Nat.add(f(a), _) == Nat.add(f(a), rsum(~A, ~f, t)) : Nat}
220      {==}
221
222law gsum_cells_go:
223  for ~A: Data
224  for ~f: A -> Nat
225  for +d: A
226  for +w: Nat
227  for +g: T.Grid(A)
228  for +wide: {B.rows_wide(A, w, g) == True{} : Bool}
229  {csum(~A, ~f, d, g, B.cells.go(w, List.range(List.length(&2, List<&2, A>, g)))) == gsum(~A, ~f, g) : Nat}
230
231def gsum_cells_go(A, f, d, w, g, wide):
232  match g:
233    case Nil{}:
234      {==}
235    case r <> rt:
236      +g2 = {r <> rt : T.Grid(A)}
237      +n = List.length(&2, List<&2, A>, rt)
238      +lr = P.eq_sound(List.length(&2, A, r), w,
239        P.and_true_l(Nat.is_eq(List.length(&2, A, r), w), B.rows_wide(A, w, rt), wide))
240      %Equal.sym(List<&2, Nat>, List.range(1n+n), 0n <> smap(List.range(n)), range_cons(n)) :
241        {csum(~A, ~f, d, g2, B.cells.go(w, _)) == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
242      %Equal.sym(Nat, csum(~A, ~f, d, g2, List.append(&2, T.Pos, B.row_cells(0n, List.range(w)), B.cells.go(w, smap(List.range(n))))),
243        Nat.add(csum(~A, ~f, d, g2, B.row_cells(0n, List.range(w))), csum(~A, ~f, d, g2, B.cells.go(w, smap(List.range(n))))),
244        csum_append(~A, ~f, d, g2, B.row_cells(0n, List.range(w)), B.cells.go(w, smap(List.range(n))))) :
245        {_ == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
246      %Equal.sym(Nat, csum(~A, ~f, d, g2, B.row_cells(0n, List.range(w))), rsum_at(~A, ~f, d, r, List.range(w)),
247        csum_row0(~A, ~f, d, r, rt, List.range(w))) :
248        {Nat.add(_, csum(~A, ~f, d, g2, B.cells.go(w, smap(List.range(n))))) == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
249      %lr : {Nat.add(rsum_at(~A, ~f, d, r, List.range(_)), csum(~A, ~f, d, g2, B.cells.go(w, smap(List.range(n)))))
250        == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
251      %Equal.sym(Nat, rsum_at(~A, ~f, d, r, List.range(List.length(&2, A, r))), rsum(~A, ~f, r), rsum_at_full(~A, ~f, d, r)) :
252        {Nat.add(_, csum(~A, ~f, d, g2, B.cells.go(w, smap(List.range(n))))) == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
253      %Equal.sym(Nat, csum(~A, ~f, d, g2, B.cells.go(w, smap(List.range(n)))), csum(~A, ~f, d, rt, B.cells.go(w, List.range(n))),
254        csum_shift(~A, ~f, d, r, rt, w, List.range(n))) :
255        {Nat.add(rsum(~A, ~f, r), _) == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
256      %Equal.sym(Nat, csum(~A, ~f, d, rt, B.cells.go(w, List.range(n))), gsum(~A, ~f, rt),
257        gsum_cells_go(~A, ~f, d, w, rt, P.and_true_r(Nat.is_eq(List.length(&2, A, r), w), B.rows_wide(A, w, rt), wide))) :
258        {Nat.add(rsum(~A, ~f, r), _) == Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, rt)) : Nat}
259      {==}
260
261# Summing over a w-by-h grid row by row equals summing over its cells.
262law grid_sum:
263  for ~A: Data
264  for ~f: A -> Nat
265  for +d: A
266  for +w: Nat
267  for +h: Nat
268  for +g: T.Grid(A)
269  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
270  {csum(~A, ~f, d, g, B.cells(w, h)) == gsum(~A, ~f, g) : Nat}
271
272def grid_sum(A, f, d, w, h, g, sh):
273  %PL.shaped_len(A, w, h, g, sh) : {csum(~A, ~f, d, g, B.cells.go(w, List.range(_))) == gsum(~A, ~f, g) : Nat}
274  gsum_cells_go(~A, ~f, d, w, g, PL.shaped_wide(A, w, h, g, sh))