1	import Base
2	import ./types.bend as T
3	import ./board.bend as B
4	import ./proof_base.bend as P
5	import ./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.
11	def 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	
18	law 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	
24	def 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.
36	law range_cons:
37	  for +n: Nat
38	  {List.range(1n+n) == 0n <> smap(List.range(n)) : List<&2, Nat>}
39	
40	def 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	
56	def 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.
64	def 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.
72	def 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	
79	def 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	
86	law 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	
95	def 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	
107	law 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	
116	def 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	
126	law 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	
136	def 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	
146	law 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	
156	def 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	
180	law 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	
189	def 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	
199	law 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	
206	def 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	
222	law 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	
231	def 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.
262	law 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	
272	def 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))