PROOF.bend
bendtorch@1.1.1.0 · 812 lines · 0 definitions
1# The proofs of LAWS.bend. Every proof is plain Bend: no @unsafe, no ?TODO, no axioms. The arithmetic lemmas come
2# from bend-ml-nat-lemmas; the division lemmas behind gqa_head are llama.bend's (MIT, same author).
3
4import Base
5import bendtorch@1.1.1.0/main.bend as T
6import bendtorch@1.1.1.0/spec.bend as Spec
7import bendtorch@1.1.1.0/tensor.bend as TT
8import bendtorch@1.1.1.0/LAWS.bend as Laws
9import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL
10import bend-ml-tensor-array@0.1.14.0/main.bend as TA
11
12# =====================================================================================================
13# Dot products
14# =====================================================================================================
15
16# dot(a + b, v) == dot(a, v) + dot(b, v): induction on the three vectors; at each entry (x + y)·z splits into x·z + y·z
17# (distributivity) and add4 regroups the four terms
18def dot_vadd(a: List<&2, Nat>, b: List<&2, Nat>, v: List<&2, Nat>) -> {Spec.dotn(Spec.vadd(a, b), v) == Nat.add(Spec.dotn(a, v), Spec.dotn(b, v)) : Nat}:
19 match a b v:
20 case Nil{} _ _:
21 {==}
22 case Con{+x, +xt} Nil{} +v:
23 Equal.sym(Nat, Nat.add(Spec.dotn(Con{x, xt}, v), 0n), Spec.dotn(Con{x, xt}, v), NL.add_zero(Spec.dotn(Con{x, xt}, v)))
24 case Con{x, xt} Con{y, yt} Nil{}:
25 {==}
26 case Con{+x, +xt} Con{+y, +yt} Con{+z, +zt}:
27 +xz = Nat.mul(x, z)
28 +yz = Nat.mul(y, z)
29 +pa = Spec.dotn(xt, zt)
30 +pb = Spec.dotn(yt, zt)
31 Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(x, y), z), Spec.dotn(Spec.vadd(xt, yt), zt)), Nat.add(Nat.mul(Nat.add(x, y), z), Nat.add(pa, pb)), Nat.add(Nat.add(xz, pa), Nat.add(yz, pb)),
32 Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(Nat.add(x, y), z), s), Spec.dotn(Spec.vadd(xt, yt), zt), Nat.add(pa, pb), dot_vadd(xt, yt, zt)),
33 Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(x, y), z), Nat.add(pa, pb)), Nat.add(Nat.add(xz, yz), Nat.add(pa, pb)), Nat.add(Nat.add(xz, pa), Nat.add(yz, pb)),
34 Equal.cong(Nat, Nat, s => Nat.add(s, Nat.add(pa, pb)), Nat.mul(Nat.add(x, y), z), Nat.add(xz, yz), Equal.sym(Nat, Nat.add(xz, yz), Nat.mul(Nat.add(x, y), z), NL.mul_dist(x, y, z))),
35 NL.add4(xz, yz, pa, pb)))
36
37# dot(k·r, v) == k · dot(r, v): at each entry (k·x)·z == k·(x·z) (associativity), then k factors out of the sum
38def dot_scale(+k: Nat, r: List<&2, Nat>, v: List<&2, Nat>) -> {Spec.dotn(Spec.vscale(k, r), v) == Nat.mul(k, Spec.dotn(r, v)) : Nat}:
39 match r v:
40 case Nil{} _:
41 Equal.sym(Nat, Nat.mul(k, 0n), 0n, NL.mul_zero(k))
42 case Con{x, xt} Nil{}:
43 Equal.sym(Nat, Nat.mul(k, 0n), 0n, NL.mul_zero(k))
44 case Con{+x, +xt} Con{+z, +zt}:
45 +d = Spec.dotn(xt, zt)
46 Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(k, x), z), Spec.dotn(Spec.vscale(k, xt), zt)), Nat.add(Nat.mul(Nat.mul(k, x), z), Nat.mul(k, d)), Nat.mul(k, Nat.add(Nat.mul(x, z), d)),
47 Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(Nat.mul(k, x), z), s), Spec.dotn(Spec.vscale(k, xt), zt), Nat.mul(k, d), dot_scale(k, xt, zt)),
48 Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(k, x), z), Nat.mul(k, d)), Nat.add(Nat.mul(k, Nat.mul(x, z)), Nat.mul(k, d)), Nat.mul(k, Nat.add(Nat.mul(x, z), d)),
49 Equal.cong(Nat, Nat, s => Nat.add(s, Nat.mul(k, d)), Nat.mul(Nat.mul(k, x), z), Nat.mul(k, Nat.mul(x, z)), Equal.sym(Nat, Nat.mul(k, Nat.mul(x, z)), Nat.mul(Nat.mul(k, x), z), NL.mul_assoc(k, x, z))),
50 Equal.sym(Nat, Nat.mul(k, Nat.add(Nat.mul(x, z), d)), Nat.add(Nat.mul(k, Nat.mul(x, z)), Nat.mul(k, d)), NL.mul_dist_l(k, Nat.mul(x, z), d))))
51
52# dot(a, b) == dot(b, a)
53def dot_comm(a: List<&2, Nat>, b: List<&2, Nat>) -> {Spec.dotn(a, b) == Spec.dotn(b, a) : Nat}:
54 match a b:
55 case Nil{} Nil{}:
56 {==}
57 case Nil{} Con{y, yt}:
58 {==}
59 case Con{x, xt} Nil{}:
60 {==}
61 case Con{+x, +xt} Con{+y, +yt}:
62 Equal.trans(Nat, Nat.add(Nat.mul(x, y), Spec.dotn(xt, yt)), Nat.add(Nat.mul(y, x), Spec.dotn(xt, yt)), Nat.add(Nat.mul(y, x), Spec.dotn(yt, xt)),
63 Equal.cong(Nat, Nat, s => Nat.add(s, Spec.dotn(xt, yt)), Nat.mul(x, y), Nat.mul(y, x), NL.mul_comm(x, y)),
64 Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(y, x), s), Spec.dotn(xt, yt), Spec.dotn(yt, xt), dot_comm(xt, yt)))
65
66# =====================================================================================================
67# The linear laws
68# =====================================================================================================
69
70# PROOF (adjoint): induction on the rows of W and the entries of dy. Row r with weight g_i contributes g_i·(r·x) on the
71# left and (g_i·r)·x on the right (dot_scale); the right side's sum of weighted rows splits by dot_vadd.
72def Laws.adjoint(w, g, v):
73 match w g:
74 case Nil{} Nil{}:
75 {==}
76 case Nil{} Con{gi, gt}:
77 {==}
78 case Con{r, rt} Nil{}:
79 {==}
80 case Con{+r, +rt} Con{+gi, +gt}:
81 +a = Spec.dotn(Spec.vscale(gi, r), v)
82 +m = Spec.mtv(rt, gt)
83 Equal.trans(Nat, Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(gt, Spec.mv(rt, v))), Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(m, v)), Spec.dotn(Spec.vadd(Spec.vscale(gi, r), m), v),
84 Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(gi, Spec.dotn(r, v)), s), Spec.dotn(gt, Spec.mv(rt, v)), Spec.dotn(m, v), Laws.adjoint(rt, gt, v)),
85 Equal.trans(Nat, Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(m, v)), Nat.add(a, Spec.dotn(m, v)), Spec.dotn(Spec.vadd(Spec.vscale(gi, r), m), v),
86 Equal.cong(Nat, Nat, s => Nat.add(s, Spec.dotn(m, v)), Nat.mul(gi, Spec.dotn(r, v)), a, Equal.sym(Nat, a, Nat.mul(gi, Spec.dotn(r, v)), dot_scale(gi, r, v))),
87 Equal.sym(Nat, Spec.dotn(Spec.vadd(Spec.vscale(gi, r), m), v), Nat.add(a, Spec.dotn(m, v)), dot_vadd(Spec.vscale(gi, r), m, v))))
88
89# PROOF (weight_adjoint): row by row, g_i·(r·x) == (g_i·x)·r, by dot_comm and dot_scale.
90def Laws.weight_adjoint(w, g, v):
91 match w g:
92 case Nil{} Nil{}:
93 {==}
94 case Nil{} Con{gi, gt}:
95 {==}
96 case Con{r, rt} Nil{}:
97 {==}
98 case Con{+r, +rt} Con{+gi, +gt}:
99 +f = Spec.frob(Spec.outer(gt, v), rt)
100 Equal.trans(Nat, Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(gt, Spec.mv(rt, v))), Nat.add(Nat.mul(gi, Spec.dotn(r, v)), f), Nat.add(Spec.dotn(Spec.vscale(gi, v), r), f),
101 Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(gi, Spec.dotn(r, v)), s), Spec.dotn(gt, Spec.mv(rt, v)), f, Laws.weight_adjoint(rt, gt, v)),
102 Equal.cong(Nat, Nat, s => Nat.add(s, f), Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(Spec.vscale(gi, v), r),
103 Equal.trans(Nat, Nat.mul(gi, Spec.dotn(r, v)), Nat.mul(gi, Spec.dotn(v, r)), Spec.dotn(Spec.vscale(gi, v), r),
104 Equal.cong(Nat, Nat, s => Nat.mul(gi, s), Spec.dotn(r, v), Spec.dotn(v, r), dot_comm(r, v)),
105 Equal.sym(Nat, Spec.dotn(Spec.vscale(gi, v), r), Nat.mul(gi, Spec.dotn(v, r)), dot_scale(gi, v, r)))))
106
107# PROOF (adjoint_seq): adjoint once for W2 (with W1·x as the input), then once for W1.
108def Laws.adjoint_seq(w1, w2, g, v):
109 Equal.trans(Nat, Spec.dotn(g, Spec.mv(w2, Spec.mv(w1, v))), Spec.dotn(Spec.mtv(w2, g), Spec.mv(w1, v)), Spec.dotn(Spec.mtv(w1, Spec.mtv(w2, g)), v), Laws.adjoint(w2, g, Spec.mv(w1, v)), Laws.adjoint(w1, Spec.mtv(w2, g), v))
110
111# =====================================================================================================
112# Causal attention
113# =====================================================================================================
114
115# PROOF (seq_chain): Seq's forward pass computes W2·(W1·x) and saves x and W1·x; its backward pass computes
116# W1ᵀ·(W2ᵀ·dy). Every step of the combinator reduces, so this is adjoint_seq.
117def Laws.seq_chain(w1, w2, x, dy, g1, g2):
118 Laws.adjoint_seq(w1, w2, dy, x)
119
120# PROOF (fork_sum): Fork's backward pass is W1ᵀ·dy1 + W2ᵀ·dy2 (vadd, the add it was given); the dot of a sum is the sum
121# of the dots (dot_vadd), and each is its layer's adjoint law.
122def Laws.fork_sum(w1, w2, x, dy1, dy2, g1, g2):
123 Equal.trans(Nat, Nat.add(Spec.dotn(dy1, Spec.mv(w1, x)), Spec.dotn(dy2, Spec.mv(w2, x))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(Spec.mtv(w2, dy2), x)), Spec.dotn(Spec.vadd(Spec.mtv(w1, dy1), Spec.mtv(w2, dy2)), x),
124 Equal.trans(Nat, Nat.add(Spec.dotn(dy1, Spec.mv(w1, x)), Spec.dotn(dy2, Spec.mv(w2, x))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(dy2, Spec.mv(w2, x))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(Spec.mtv(w2, dy2), x)),
125 Equal.cong(Nat, Nat, z => Nat.add(z, Spec.dotn(dy2, Spec.mv(w2, x))), Spec.dotn(dy1, Spec.mv(w1, x)), Spec.dotn(Spec.mtv(w1, dy1), x), Laws.adjoint(w1, dy1, x)),
126 Equal.cong(Nat, Nat, z => Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), z), Spec.dotn(dy2, Spec.mv(w2, x)), Spec.dotn(Spec.mtv(w2, dy2), x), Laws.adjoint(w2, dy2, x))),
127 Equal.sym(Nat, Spec.dotn(Spec.vadd(Spec.mtv(w1, dy1), Spec.mtv(w2, dy2)), x), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(Spec.mtv(w2, dy2), x)), dot_vadd(Spec.mtv(w1, dy1), Spec.mtv(w2, dy2), x)))
128
129def disc(b: Bool) -> Type:
130 match b:
131 case True{}:
132 Unit
133 case False{}:
134 Empty
135
136# False == True is impossible: rewriting the goal Empty = disc(False) with it gives disc(True) = Unit
137def false_true(e: {False{} == True{} : Bool}) -> Empty:
138 %Equal.sym(Bool, False{}, True{}, e) : disc(_)
139 Unit{}
140
141# xs reversed onto acc has the length of both
142def len_rcat(+xs: List<&2, F32>, +acc: List<&2, F32>) -> {List.length(&2, F32, T.rcat(xs, acc)) == Nat.add(List.length(&2, F32, xs), List.length(&2, F32, acc)) : Nat}:
143 match xs:
144 case Nil{}:
145 {==}
146 case Con{+x, +t}:
147 Equal.trans(Nat, List.length(&2, F32, T.rcat(t, x <> acc)), Nat.add(List.length(&2, F32, t), 1n+List.length(&2, F32, acc)), 1n+Nat.add(List.length(&2, F32, t), List.length(&2, F32, acc)), len_rcat(t, x <> acc), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), List.length(&2, F32, acc)), Nat.add(List.length(&2, F32, t), 1n+List.length(&2, F32, acc)), NL.add_succ(List.length(&2, F32, t), List.length(&2, F32, acc))))
148
149# drow's row has the current dot, the m after it, and acc: 1 + m + |acc| numbers
150def len_drow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2) -> {List.length(&2, F32, T.dr_row(T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}:
151 match m r:
152 case 0n T.D2{a, b, +s}:
153 Equal.trans(Nat, List.length(&2, F32, T.rcat(s <> acc, Nil{})), Nat.add(1n+List.length(&2, F32, acc), 0n), 1n+List.length(&2, F32, acc), len_rcat(s <> acc, Nil{}), NL.add_zero(1n+List.length(&2, F32, acc)))
154 case 1n++p T.D2{a, b, +s}:
155 Equal.trans(Nat, List.length(&2, F32, T.dr_row(T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), len_drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc)))))
156
157# PROOF (causal_keys): qrow is drow(i, ..) from an empty accumulator, so its row has 1 + i + 0 numbers (len_drow).
158def Laws.causal_keys(i, hd, qs, qc, ks, kc, q, k):
159 Equal.trans(Nat, List.length(&2, F32, T.dr_row(T.qrow(i, hd, qs, qc, ks, kc, q, k))), Nat.add(1n+i, 0n), 1n+i, len_drow(i, hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, ks, Nil{}, T.dot0(hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, 1, 1, q, k)), NL.add_zero(1n+i))
160
161# n - 0 is n
162def sub0(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
163 match n:
164 case 0n:
165 {==}
166 case 1n+p:
167 {==}
168
169# the division loop of a softmax counts the 1 + k numbers it divides onto c (pr_of hands the count on as the row's)
170def cnt_div(q: Array<F32>, k: Array<F32>, kk: Nat, +idx: U32, +s: F32, +c: Nat, r: Array<F32> & F32) -> {T.pr_n(T.pr_of(q, k, T.pdiv(kk, idx, s, c, r))) == Nat.add(1n+kk, c) : Nat}:
171 match kk r:
172 case 0n Tuple{a, +x}:
173 {==}
174 case 1n++j Tuple{a, +x}:
175 Equal.trans(Nat, T.pr_n(T.pr_of(q, k, T.pdiv(j, (idx + 1 : U32), s, 1n+c, Array.get(F32, Array.set(F32, a, idx, (x / s : F32)), (idx + 1 : U32))))), Nat.add(1n+j, 1n+c), 2n+Nat.add(j, c), cnt_div(q, k, j, (idx + 1 : U32), s, 1n+c, Array.get(F32, Array.set(F32, a, idx, (x / s : F32)), (idx + 1 : U32))), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, 1n+c), 1n+Nat.add(j, c), Equal.sym(Nat, 1n+Nat.add(j, c), Nat.add(j, 1n+c), NL.add_succ(j, c))))
176
177# the whole softmax over 1 + kk numbers reports 1 + kk, whatever max and exp found (they are matched, not computed)
178def cnt_psm3(q: Array<F32>, k: Array<F32>, +kk: Nat, +off: U32, r: T.AS) -> {T.pr_n(T.pr_of(q, k, T.psm3(kk, off, r))) == 1n+kk : Nat}:
179 match r:
180 case T.AS{a, +s}:
181 Equal.trans(Nat, T.pr_n(T.pr_of(q, k, T.pdiv(kk, off, s, 0n, Array.get(F32, a, off)))), Nat.add(1n+kk, 0n), 1n+kk, cnt_div(q, k, kk, off, s, 0n, Array.get(F32, a, off)), NL.add_zero(1n+kk))
182
183def cnt_psm2(q: Array<F32>, k: Array<F32>, +kk: Nat, +off: U32, r: T.AS) -> {T.pr_n(T.pr_of(q, k, T.psm2(kk, off, r))) == 1n+kk : Nat}:
184 match r:
185 case T.AS{a, +m}:
186 cnt_psm3(q, k, kk, off, T.pexp(kk, off, m, 0.0, Array.get(F32, a, off)))
187
188# pw writes xs and counts them from n; the softmax prow3 runs on them reports 1 + (|xs| + n - 1)
189def cnt_pw(+xs: List<&2, F32>, +idx: U32, +sc: F32, +n: Nat, +off: U32, q: Array<F32>, k: Array<F32>, p: Array<F32>) -> {T.pr_n(T.prow3(off, q, k, T.pw(xs, idx, sc, n, p))) == 1n+Nat.sub(Nat.add(List.length(&2, F32, xs), n), 1n) : Nat}:
190 match xs:
191 case Nil{}:
192 cnt_psm2(q, k, Nat.sub(n, 1n), off, T.pmax0(Nat.sub(n, 1n), off, Array.get(F32, p, off)))
193 case Con{+x, +t}:
194 Equal.trans(Nat, T.pr_n(T.prow3(off, q, k, T.pw(t, (idx + 1 : U32), sc, 1n+n, Array.set(F32, p, idx, (x * sc : F32))))), 1n+Nat.sub(Nat.add(List.length(&2, F32, t), 1n+n), 1n), 1n+Nat.sub(1n+Nat.add(List.length(&2, F32, t), n), 1n), cnt_pw(t, (idx + 1 : U32), sc, 1n+n, off, q, k, Array.set(F32, p, idx, (x * sc : F32))), Equal.cong(Nat, Nat, z => 1n+Nat.sub(z, 1n), Nat.add(List.length(&2, F32, t), 1n+n), 1n+Nat.add(List.length(&2, F32, t), n), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), n), Nat.add(List.length(&2, F32, t), 1n+n), NL.add_succ(List.length(&2, F32, t), n))))
195
196# the count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw
197def cnt_drow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2, +sc: F32, +off: U32, pa: Array<F32>) -> {T.pr_n(T.prow2(sc, off, pa, T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}:
198 match m r:
199 case 0n T.D2{a, b, +s}:
200 +rw = T.rcat(s <> acc, Nil{})
201 +la = List.length(&2, F32, acc)
202 Equal.trans(Nat, T.pr_n(T.prow3(off, a, b, T.pw(rw, off, sc, 0n, pa))), 1n+Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), 1n+la, cnt_pw(rw, off, sc, 0n, off, a, b, pa),
203 Equal.cong(Nat, Nat, z => 1n+z, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), la,
204 Equal.trans(Nat, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), Nat.sub(1n+la, 1n), la,
205 Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(List.length(&2, F32, rw), 0n), 1n+la,
206 Equal.trans(Nat, Nat.add(List.length(&2, F32, rw), 0n), List.length(&2, F32, rw), 1n+la, NL.add_zero(List.length(&2, F32, rw)),
207 Equal.trans(Nat, List.length(&2, F32, rw), Nat.add(1n+la, 0n), 1n+la, len_rcat(s <> acc, Nil{}), NL.add_zero(1n+la)))),
208 sub0(la))))
209 case 1n++p T.D2{a, b, +s}:
210 Equal.trans(Nat, T.pr_n(T.prow2(sc, off, pa, T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), cnt_drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b), sc, off, pa), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc)))))
211
212# PROOF (causal): prow runs prow2 on qrow's row, drow(i, ..) from an empty accumulator, so the count it hands the
213# softmax is 1 + i + 0 (cnt_drow).
214def Laws.causal(i, t, hd, sc, qs, qc, ks, kc, q, k, p):
215 Equal.trans(Nat, T.pr_n(T.prow(i, t, hd, sc, qs, qc, ks, kc, q, k, p)), Nat.add(1n+i, 0n), 1n+i, cnt_drow(i, hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, ks, Nil{}, T.dot0(hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, 1, 1, q, k), sc, (U32.from_nat(i) * U32.from_nat(t) : U32), p), NL.add_zero(1n+i))
216
217# gw writes xs and counts them from n: gr3 hands on |xs| + n (as cnt_pw for the forward pass)
218def cnt_gw(+xs: List<&2, F32>, +idx: U32, +n: Nat, +sc: F32, +off: U32, d: Array<F32>, v: Array<F32>, p: Array<F32>, g: Array<F32>) -> {T.gr_n(T.gr3(sc, off, d, v, p, T.gw(xs, idx, n, g))) == Nat.add(List.length(&2, F32, xs), n) : Nat}:
219 match xs:
220 case Nil{}:
221 {==}
222 case Con{+x, +t}:
223 Equal.trans(Nat, T.gr_n(T.gr3(sc, off, d, v, p, T.gw(t, (idx + 1 : U32), 1n+n, Array.set(F32, g, idx, x)))), Nat.add(List.length(&2, F32, t), 1n+n), 1n+Nat.add(List.length(&2, F32, t), n), cnt_gw(t, (idx + 1 : U32), 1n+n, sc, off, d, v, p, Array.set(F32, g, idx, x)), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), n), Nat.add(List.length(&2, F32, t), 1n+n), NL.add_succ(List.length(&2, F32, t), n)))
224
225# the count gr2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_gw (cnt_drow's twin)
226def cnt_gdrow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2, +sc: F32, +off: U32, pa: Array<F32>, ga: Array<F32>) -> {T.gr_n(T.gr2(sc, off, pa, ga, T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}:
227 match m r:
228 case 0n T.D2{a, b, +s}:
229 +rw = T.rcat(s <> acc, Nil{})
230 Equal.trans(Nat, T.gr_n(T.gr3(sc, off, a, b, pa, T.gw(rw, off, 0n, ga))), Nat.add(List.length(&2, F32, rw), 0n), 1n+List.length(&2, F32, acc), cnt_gw(rw, off, 0n, sc, off, a, b, pa, ga),
231 Equal.trans(Nat, Nat.add(List.length(&2, F32, rw), 0n), List.length(&2, F32, rw), 1n+List.length(&2, F32, acc), NL.add_zero(List.length(&2, F32, rw)),
232 Equal.trans(Nat, List.length(&2, F32, rw), Nat.add(1n+List.length(&2, F32, acc), 0n), 1n+List.length(&2, F32, acc), len_rcat(s <> acc, Nil{}), NL.add_zero(1n+List.length(&2, F32, acc)))))
233 case 1n++p T.D2{a, b, +s}:
234 Equal.trans(Nat, T.gr_n(T.gr2(sc, off, pa, ga, T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), cnt_gdrow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b), sc, off, pa, ga), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc)))))
235
236# PROOF (causal_grad): grow runs gr2 on drow(i, ..) from an empty accumulator, so the count is 1 + i + 0 (cnt_gdrow).
237def Laws.causal_grad(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g):
238 Equal.trans(Nat, T.gr_n(T.grow(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g)), Nat.add(1n+i, 0n), 1n+i, cnt_gdrow(i, hd, ((U32.from_nat(i) * ds : U32) + dc : U32), vc, vs, Nil{}, T.dot0(hd, ((U32.from_nat(i) * ds : U32) + dc : U32), vc, 1, 1, d, v), sc, (U32.from_nat(i) * U32.from_nat(t) : U32), p, g), NL.add_zero(1n+i))
239
240# =====================================================================================================
241# Attention's trees of sequences: parallel = sequential
242# =====================================================================================================
243
244# a ++ b == a2 ++ b2 from a == a2 and b == b2
245def app2(-A: Type, -a: List<&1, A>, -a2: List<&1, A>, -b: List<&1, A>, -b2: List<&1, A>, ea: {a == a2 : List<&1, A>}, eb: {b == b2 : List<&1, A>}) -> {List.append(&1, A, a, b) == List.append(&1, A, a2, b2) : List<&1, A>}:
246 Equal.trans(List<&1, A>, List.append(&1, A, a, b), List.append(&1, A, a2, b), List.append(&1, A, a2, b2), Equal.cong(List<&1, A>, List<&1, A>, z => List.append(&1, A, z, b), a, a2, ea), Equal.cong(List<&1, A>, List<&1, A>, z => List.append(&1, A, a2, z), b, b2, eb))
247
248# ---- the sequential map the tree is compared with: f(x) = fs_o(fheads(h, 0, dm, x)) for each x, in order ----
249
250def fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array<F32>>:
251 match xs:
252 case Nil{}:
253 Nil{}
254 case Con{x, t}:
255 T.fs_o(T.fheads(h, 0n, dm, x)) <> fmap(h, dm, t)
256
257# ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ----
258
259type L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array<F32>>> is Type:
260 L1R{ys: List<&1, T.FS>, same: {ys == xs : List<&1, T.FS>}, fact: {T.fleaf(xs, h, dm, acc) == List.reverse.go(&1, Array<F32>, acc, fmap(h, dm, xs)) : List<&1, Array<F32>>}}
261
262def l1_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>, r: L1R<h, dm, t, T.fs_o(T.fheads(h, 0n, dm, x)) <> acc>) -> L1R<h, dm, x <> t, acc>:
263 match r:
264 case L1R{ys, same, fact}:
265 L1R{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact}
266
267def l1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>) -> L1R<h, dm, xs, acc>:
268 match xs:
269 case Nil{}:
270 L1R{Nil{}, {==}, {==}}
271 case Con{x, t}:
272 l1_con(x, t, h, dm, acc, l1(t, h, dm, T.fs_o(T.fheads(h, 0n, dm, x)) <> acc))
273
274# ---- the map of two lists appended is the two maps appended ----
275
276type MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type:
277 MAR{ys: List<&1, T.FS>, same: {ys == a : List<&1, T.FS>}, fact: {fmap(h, dm, List.append(&1, T.FS, a, b)) == List.append(&1, Array<F32>, fmap(h, dm, a), fmap(h, dm, b)) : List<&1, Array<F32>>}}
278
279def ma_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>, r: MAR<h, dm, t, b>) -> MAR<h, dm, x <> t, b>:
280 match r:
281 case MAR{ys, same, fact}:
282 MAR{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), Equal.cong(List<&1, Array<F32>>, List<&1, Array<F32>>, z => T.fs_o(T.fheads(h, 0n, dm, x)) <> z, fmap(h, dm, List.append(&1, T.FS, t, b)), List.append(&1, Array<F32>, fmap(h, dm, t), fmap(h, dm, b)), fact)}
283
284def map_app(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MAR<h, dm, a, b>:
285 match a:
286 case Nil{}:
287 MAR{Nil{}, {==}, {==}}
288 case Con{x, t}:
289 ma_con(x, t, h, dm, b, map_app(t, h, dm, b))
290
291# ---- a reversed onto b, then c appended: a reversed onto b ++ c ----
292
293type GAR<-a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>> is Type:
294 GAR{ys: List<&1, T.FS>, same: {ys == a : List<&1, T.FS>}, fact: {List.append(&1, T.FS, List.reverse.go(&1, T.FS, a, b), c) == List.reverse.go(&1, T.FS, a, List.append(&1, T.FS, b, c)) : List<&1, T.FS>}}
295
296def ga_con(x: T.FS, -t: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>, r: GAR<t, x <> b, c>) -> GAR<x <> t, b, c>:
297 match r:
298 case GAR{ys, same, fact}:
299 GAR{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact}
300
301def go_app(a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>) -> GAR<a, b, c>:
302 match a:
303 case Nil{}:
304 GAR{Nil{}, {==}, {==}}
305 case Con{x, t}:
306 ga_con(x, t, b, c, go_app(t, x <> b, c))
307
308# ---- cut gives two halves that, appended, are acc reversed onto xs ----
309
310type CGR<-k: Nat, -xs: List<&1, T.FS>, -acc: List<&1, T.FS>> is Type:
311 CGR{hh: T.Halves<T.FS>, same: {hh == T.cut(T.FS, k, xs, acc) : T.Halves<T.FS>}, cat: {T.hcat(T.FS, hh) == List.reverse.go(&1, T.FS, acc, xs) : List<&1, T.FS>}}
312
313def cg_base(-k: Nat, xs: List<&1, T.FS>, -acc: List<&1, T.FS>, e: {T.cut(T.FS, k, xs, acc) == T.Halves{List.reverse(&1, T.FS, acc), xs} : T.Halves<T.FS>}, r: GAR<acc, Nil{}, xs>) -> CGR<k, xs, acc>:
314 match r:
315 case GAR{ys, +same, fact}:
316 CGR{T.Halves{List.reverse(&1, T.FS, ys), xs},
317 Equal.trans(T.Halves<T.FS>, T.Halves{List.reverse(&1, T.FS, ys), xs}, T.Halves{List.reverse(&1, T.FS, acc), xs}, T.cut(T.FS, k, xs, acc), Equal.cong(List<&1, T.FS>, T.Halves<T.FS>, z => T.Halves{List.reverse(&1, T.FS, z), xs}, ys, acc, same), Equal.sym(T.Halves<T.FS>, T.cut(T.FS, k, xs, acc), T.Halves{List.reverse(&1, T.FS, acc), xs}, e)),
318 Equal.trans(List<&1, T.FS>, List.append(&1, T.FS, List.reverse.go(&1, T.FS, ys, Nil{}), xs), List.append(&1, T.FS, List.reverse.go(&1, T.FS, acc, Nil{}), xs), List.reverse.go(&1, T.FS, acc, xs), Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => List.append(&1, T.FS, List.reverse.go(&1, T.FS, z, Nil{}), xs), ys, acc, same), fact)}
319
320def cg_con(-m: Nat, -x: T.FS, -t: List<&1, T.FS>, -acc: List<&1, T.FS>, r: CGR<m, t, x <> acc>) -> CGR<1n+m, x <> t, acc>:
321 match r:
322 case CGR{hh, same, cat}:
323 CGR{hh, same, cat}
324
325def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR<k, xs, acc>:
326 match k xs:
327 case 1n+m Con{x, t}:
328 cg_con(m, x, t, acc, cg(m, t, x <> acc))
329 case 0n ys:
330 cg_base(0n, ys, acc, {==}, go_app(acc, Nil{}, ys))
331 case 1n+m Nil{}:
332 cg_base(1n+m, Nil{}, acc, {==}, go_app(acc, Nil{}, Nil{}))
333
334# ---- the tree: fpar at depth d on two halves is the map of the halves appended ----
335
336type MR<-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
337 MR{ys: List<&1, T.FS>, same: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, fact: {T.fpar(d, gs, n, h, dm) == fmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}}
338
339# depth 0: the two leaves' loops, appended
340def m0c(-l: List<&1, T.FS>, -r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.FS>, +sl: {l1y == l : List<&1, T.FS>}, fl: {T.fleaf(l, h, dm, Nil{}) == fmap(h, dm, l) : List<&1, Array<F32>>}, r1: List<&1, T.FS>, sr: {r1 == r : List<&1, T.FS>}, fr: {T.fleaf(r, h, dm, Nil{}) == fmap(h, dm, r) : List<&1, Array<F32>>}, c: MAR<h, dm, l1y, r>) -> MR<0n, T.Halves{l, r}, n, h, dm>:
341 match c:
342 case MAR{l2, s2, fa}:
343 MR{List.append(&1, T.FS, l2, r1), app2(T.FS, l2, l, r1, r, Equal.trans(List<&1, T.FS>, l2, l1y, l, s2, sl), sr),
344 Equal.trans(List<&1, Array<F32>>, List.append(&1, Array<F32>, T.fleaf(l, h, dm, Nil{}), T.fleaf(r, h, dm, Nil{})), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array<F32>, T.fleaf(l, h, dm, Nil{}), fmap(h, dm, l), T.fleaf(r, h, dm, Nil{}), fmap(h, dm, r), fl, fr),
345 Equal.sym(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)),
346 Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), fmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, List.append(&1, T.FS, z, r)), l, l1y, Equal.sym(List<&1, T.FS>, l1y, l, sl)),
347 Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array<F32>, fmap(h, dm, l1y), fmap(h, dm, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fa, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => List.append(&1, Array<F32>, fmap(h, dm, z), fmap(h, dm, r)), l1y, l, sl)))))}
348
349def m0b(-l: List<&1, T.FS>, -r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, l1y: List<&1, T.FS>, +sl: {l1y == l : List<&1, T.FS>}, fl: {T.fleaf(l, h, dm, Nil{}) == fmap(h, dm, l) : List<&1, Array<F32>>}, b: L1R<h, dm, r, Nil{}>) -> MR<0n, T.Halves{l, r}, n, h, dm>:
350 match b:
351 case L1R{r1, sr, fr}:
352 m0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, map_app(l1y, h, dm, r))
353
354def m0a(-l: List<&1, T.FS>, r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, a: L1R<h, dm, l, Nil{}>) -> MR<0n, T.Halves{l, r}, n, h, dm>:
355 match a:
356 case L1R{l1y, sl, fl}:
357 m0b(l, r, n, h, dm, l1y, sl, fl, l1(r, h, dm, Nil{}))
358
359# depth 1 + e: each half cut in two and its tree (the closures run main at depth e), then the two maps appended
360def m1c(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.FS>, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.FS>}, +cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves<T.FS>, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.FS>}, +cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, -y1: List<&1, T.FS>, sy1: {y1 == T.hcat(T.FS, hh1) : List<&1, T.FS>}, f1: {T.fpar(e, hh1, TA.half(n), h, dm) == fmap(h, dm, T.hcat(T.FS, hh1)) : List<&1, Array<F32>>}, y2: List<&1, T.FS>, sy2: {y2 == T.hcat(T.FS, hh2) : List<&1, T.FS>}, f2: {T.fpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == fmap(h, dm, T.hcat(T.FS, hh2)) : List<&1, Array<F32>>}, ma: MAR<h, dm, y1, y2>) -> MR<1n+e, T.Halves{l, r}, n, h, dm>:
361 match ma:
362 case MAR{y1b, sb, fa}:
363 +ly1 = Equal.trans(List<&1, T.FS>, y1, T.hcat(T.FS, hh1), l, sy1, cat1)
364 +ly2 = Equal.trans(List<&1, T.FS>, y2, T.hcat(T.FS, hh2), r, sy2, cat2)
365 +q1 = Equal.trans(List<&1, Array<F32>>, T.fpar(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar(e, hh1, TA.half(n), h, dm), fmap(h, dm, l), Equal.cong(T.Halves<T.FS>, List<&1, Array<F32>>, z => T.fpar(e, z, TA.half(n), h, dm), T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), hh1, Equal.sym(T.Halves<T.FS>, hh1, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, Array<F32>>, T.fpar(e, hh1, TA.half(n), h, dm), fmap(h, dm, T.hcat(T.FS, hh1)), fmap(h, dm, l), f1, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), T.hcat(T.FS, hh1), l, cat1)))
366 +q2 = Equal.trans(List<&1, Array<F32>>, T.fpar(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), T.fpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), fmap(h, dm, r), Equal.cong(T.Halves<T.FS>, List<&1, Array<F32>>, z => T.fpar(e, z, Nat.sub(n, TA.half(n)), h, dm), T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), hh2, Equal.sym(T.Halves<T.FS>, hh2, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, Array<F32>>, T.fpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), fmap(h, dm, T.hcat(T.FS, hh2)), fmap(h, dm, r), f2, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), T.hcat(T.FS, hh2), r, cat2)))
367 +bb = Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), fmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), List.append(&1, T.FS, l, r), List.append(&1, T.FS, y1, y2), app2(T.FS, l, y1, r, y2, Equal.sym(List<&1, T.FS>, y1, l, ly1), Equal.sym(List<&1, T.FS>, y2, r, ly2))), Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array<F32>, fmap(h, dm, y1), fmap(h, dm, y2)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fa, app2(Array<F32>, fmap(h, dm, y1), fmap(h, dm, l), fmap(h, dm, y2), fmap(h, dm, r), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), y2, r, ly2))))
368 MR{List.append(&1, T.FS, y1b, y2), app2(T.FS, y1b, l, y2, r, Equal.trans(List<&1, T.FS>, y1b, y1, l, sb, ly1), ly2),
369 Equal.trans(List<&1, Array<F32>>, List.append(&1, Array<F32>, T.fpar(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array<F32>, T.fpar(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), fmap(h, dm, l), T.fpar(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), fmap(h, dm, r), q1, q2), Equal.sym(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), bb))}
370
371def m1b(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.FS>, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.FS>}, cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves<T.FS>, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.FS>}, cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, r1: MR<e, hh1, TA.half(n), h, dm>, r2: MR<e, hh2, Nat.sub(n, TA.half(n)), h, dm>) -> MR<1n+e, T.Halves{l, r}, n, h, dm>:
372 match r1 r2:
373 case MR{y1, sy1, f1} MR{y2, sy2, f2}:
374 m1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, map_app(y1, h, dm, y2))
375
376def m1a(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, c1: CGR<TA.half(TA.half(n)), l, Nil{}>, c2: CGR<TA.half(Nat.sub(n, TA.half(n))), r, Nil{}>, k1: @g: T.Halves<T.FS> -> MR<e, g, TA.half(n), h, dm>, k2: @g: T.Halves<T.FS> -> MR<e, g, Nat.sub(n, TA.half(n)), h, dm>) -> MR<1n+e, T.Halves{l, r}, n, h, dm>:
377 match c1 c2:
378 case CGR{hh1, s1, cat1} CGR{hh2, s2, cat2}:
379 m1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2))
380
381def tree(d: Nat, gs: T.Halves<T.FS>, +n: Nat, +h: Nat, +dm: T.Dm) -> MR<d, gs, n, h, dm>:
382 match d gs:
383 case 0n T.Halves{l, r}:
384 m0a(l, r, n, h, dm, l1(l, h, dm, Nil{}))
385 case 1n++e T.Halves{l, r}:
386 m1a(e, l, r, n, h, dm, cg(TA.half(TA.half(n)), l, Nil{}), cg(TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), g1 => tree(e, g1, TA.half(n), h, dm), g2 => tree(e, g2, Nat.sub(n, TA.half(n)), h, dm))
387
388# the law: the tree gives what fleaf, the loop over the sequences one after another, gives
389def par_fin(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.FS>, +sy: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, f: {T.fpar(d, gs, n, h, dm) == fmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}, r: L1R<h, dm, ys, Nil{}>) -> {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
390 match r:
391 case L1R{ys2, s2, fl}:
392 Equal.trans(List<&1, Array<F32>>, T.fpar(d, gs, n, h, dm), fmap(h, dm, T.hcat(T.FS, gs)), T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), f,
393 Equal.sym(List<&1, Array<F32>>, T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), fmap(h, dm, T.hcat(T.FS, gs)),
394 Equal.trans(List<&1, Array<F32>>, T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), T.fleaf(ys, h, dm, Nil{}), fmap(h, dm, T.hcat(T.FS, gs)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => T.fleaf(z, h, dm, Nil{}), T.hcat(T.FS, gs), ys, Equal.sym(List<&1, T.FS>, ys, T.hcat(T.FS, gs), sy)),
395 Equal.trans(List<&1, Array<F32>>, T.fleaf(ys, h, dm, Nil{}), fmap(h, dm, ys), fmap(h, dm, T.hcat(T.FS, gs)), fl, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), ys, T.hcat(T.FS, gs), sy)))))
396
397def par_mid(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, r: MR<d, gs, n, h, dm>) -> {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
398 match r:
399 case MR{ys, sy, f}:
400 par_fin(d, gs, n, h, dm, ys, sy, f, l1(ys, h, dm, Nil{}))
401
402# PROOF (attn_par_fwd): by induction on the depth, each fact handing its list back (the lists hold arrays, so each is
403# used once): a leaf pair is fleaf twice, and fleaf is the map pushed onto its accumulator (l1); the map of two lists
404# appended is the two maps appended (map_app); cut's halves, appended, are the list it cut (cg); a deeper tree is two
405# trees on cut's halves (the closures).
406def Laws.attn_par_fwd(d, gs, n, h, dm):
407 par_mid(d, gs, n, h, dm, tree(d, gs, n, h, dm))
408
409# ---- the sequential map the b_tree is compared with: f(x) = fs_o(fheads(h, 0, dm, x)) for each x, in order ----
410
411def b_fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.BG>) -> List<&1, T.DB>:
412 match xs:
413 case Nil{}:
414 Nil{}
415 case Con{x, t}:
416 T.db_of(T.bgroups(h, 0n, dm, x)) <> b_fmap(h, dm, t)
417
418# ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ----
419
420type b_L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type:
421 b_L1R{ys: List<&1, T.BG>, same: {ys == xs : List<&1, T.BG>}, fact: {T.bleaf(xs, h, dm, acc) == List.reverse.go(&1, T.DB, acc, b_fmap(h, dm, xs)) : List<&1, T.DB>}}
422
423def b_l1_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>, r: b_L1R<h, dm, t, T.db_of(T.bgroups(h, 0n, dm, x)) <> acc>) -> b_L1R<h, dm, x <> t, acc>:
424 match r:
425 case b_L1R{ys, same, fact}:
426 b_L1R{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact}
427
428def b_l1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1R<h, dm, xs, acc>:
429 match xs:
430 case Nil{}:
431 b_L1R{Nil{}, {==}, {==}}
432 case Con{x, t}:
433 b_l1_con(x, t, h, dm, acc, b_l1(t, h, dm, T.db_of(T.bgroups(h, 0n, dm, x)) <> acc))
434
435# ---- the map of two lists appended is the two maps appended ----
436
437type b_MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type:
438 b_MAR{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {b_fmap(h, dm, List.append(&1, T.BG, a, b)) == List.append(&1, T.DB, b_fmap(h, dm, a), b_fmap(h, dm, b)) : List<&1, T.DB>}}
439
440def b_ma_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>, r: b_MAR<h, dm, t, b>) -> b_MAR<h, dm, x <> t, b>:
441 match r:
442 case b_MAR{ys, same, fact}:
443 b_MAR{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), Equal.cong(List<&1, T.DB>, List<&1, T.DB>, z => T.db_of(T.bgroups(h, 0n, dm, x)) <> z, b_fmap(h, dm, List.append(&1, T.BG, t, b)), List.append(&1, T.DB, b_fmap(h, dm, t), b_fmap(h, dm, b)), fact)}
444
445def b_map_app(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MAR<h, dm, a, b>:
446 match a:
447 case Nil{}:
448 b_MAR{Nil{}, {==}, {==}}
449 case Con{x, t}:
450 b_ma_con(x, t, h, dm, b, b_map_app(t, h, dm, b))
451
452# ---- a reversed onto b, then c appended: a reversed onto b ++ c ----
453
454type b_GAR<-a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>> is Type:
455 b_GAR{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {List.append(&1, T.BG, List.reverse.go(&1, T.BG, a, b), c) == List.reverse.go(&1, T.BG, a, List.append(&1, T.BG, b, c)) : List<&1, T.BG>}}
456
457def b_ga_con(x: T.BG, -t: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>, r: b_GAR<t, x <> b, c>) -> b_GAR<x <> t, b, c>:
458 match r:
459 case b_GAR{ys, same, fact}:
460 b_GAR{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact}
461
462def b_go_app(a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>) -> b_GAR<a, b, c>:
463 match a:
464 case Nil{}:
465 b_GAR{Nil{}, {==}, {==}}
466 case Con{x, t}:
467 b_ga_con(x, t, b, c, b_go_app(t, x <> b, c))
468
469# ---- cut gives two halves that, appended, are acc reversed onto xs ----
470
471type b_CGR<-k: Nat, -xs: List<&1, T.BG>, -acc: List<&1, T.BG>> is Type:
472 b_CGR{hh: T.Halves<T.BG>, same: {hh == T.cut(T.BG, k, xs, acc) : T.Halves<T.BG>}, cat: {T.hcat(T.BG, hh) == List.reverse.go(&1, T.BG, acc, xs) : List<&1, T.BG>}}
473
474def b_cg_base(-k: Nat, xs: List<&1, T.BG>, -acc: List<&1, T.BG>, e: {T.cut(T.BG, k, xs, acc) == T.Halves{List.reverse(&1, T.BG, acc), xs} : T.Halves<T.BG>}, r: b_GAR<acc, Nil{}, xs>) -> b_CGR<k, xs, acc>:
475 match r:
476 case b_GAR{ys, +same, fact}:
477 b_CGR{T.Halves{List.reverse(&1, T.BG, ys), xs},
478 Equal.trans(T.Halves<T.BG>, T.Halves{List.reverse(&1, T.BG, ys), xs}, T.Halves{List.reverse(&1, T.BG, acc), xs}, T.cut(T.BG, k, xs, acc), Equal.cong(List<&1, T.BG>, T.Halves<T.BG>, z => T.Halves{List.reverse(&1, T.BG, z), xs}, ys, acc, same), Equal.sym(T.Halves<T.BG>, T.cut(T.BG, k, xs, acc), T.Halves{List.reverse(&1, T.BG, acc), xs}, e)),
479 Equal.trans(List<&1, T.BG>, List.append(&1, T.BG, List.reverse.go(&1, T.BG, ys, Nil{}), xs), List.append(&1, T.BG, List.reverse.go(&1, T.BG, acc, Nil{}), xs), List.reverse.go(&1, T.BG, acc, xs), Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => List.append(&1, T.BG, List.reverse.go(&1, T.BG, z, Nil{}), xs), ys, acc, same), fact)}
480
481def b_cg_con(-m: Nat, -x: T.BG, -t: List<&1, T.BG>, -acc: List<&1, T.BG>, r: b_CGR<m, t, x <> acc>) -> b_CGR<1n+m, x <> t, acc>:
482 match r:
483 case b_CGR{hh, same, cat}:
484 b_CGR{hh, same, cat}
485
486def b_cg(k: Nat, xs: List<&1, T.BG>, acc: List<&1, T.BG>) -> b_CGR<k, xs, acc>:
487 match k xs:
488 case 1n+m Con{x, t}:
489 b_cg_con(m, x, t, acc, b_cg(m, t, x <> acc))
490 case 0n ys:
491 b_cg_base(0n, ys, acc, {==}, b_go_app(acc, Nil{}, ys))
492 case 1n+m Nil{}:
493 b_cg_base(1n+m, Nil{}, acc, {==}, b_go_app(acc, Nil{}, Nil{}))
494
495# ---- the b_tree: fpar at depth d on two halves is the map of the halves appended ----
496
497type b_MR<-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
498 b_MR{ys: List<&1, T.BG>, same: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, fact: {T.bpar(d, gs, n, h, dm) == b_fmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}}
499
500# depth 0: the two leaves' loops, appended
501def b_m0c(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf(l, h, dm, Nil{}) == b_fmap(h, dm, l) : List<&1, T.DB>}, r1: List<&1, T.BG>, sr: {r1 == r : List<&1, T.BG>}, fr: {T.bleaf(r, h, dm, Nil{}) == b_fmap(h, dm, r) : List<&1, T.DB>}, c: b_MAR<h, dm, l1y, r>) -> b_MR<0n, T.Halves{l, r}, n, h, dm>:
502 match c:
503 case b_MAR{l2, s2, fa}:
504 b_MR{List.append(&1, T.BG, l2, r1), app2(T.BG, l2, l, r1, r, Equal.trans(List<&1, T.BG>, l2, l1y, l, s2, sl), sr),
505 Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bleaf(l, h, dm, Nil{}), T.bleaf(r, h, dm, Nil{})), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), b_fmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bleaf(l, h, dm, Nil{}), b_fmap(h, dm, l), T.bleaf(r, h, dm, Nil{}), b_fmap(h, dm, r), fl, fr),
506 Equal.sym(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)),
507 Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), b_fmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, List.append(&1, T.BG, z, r)), l, l1y, Equal.sym(List<&1, T.BG>, l1y, l, sl)),
508 Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_fmap(h, dm, l1y), b_fmap(h, dm, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), fa, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => List.append(&1, T.DB, b_fmap(h, dm, z), b_fmap(h, dm, r)), l1y, l, sl)))))}
509
510def b_m0b(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf(l, h, dm, Nil{}) == b_fmap(h, dm, l) : List<&1, T.DB>}, b: b_L1R<h, dm, r, Nil{}>) -> b_MR<0n, T.Halves{l, r}, n, h, dm>:
511 match b:
512 case b_L1R{r1, sr, fr}:
513 b_m0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, b_map_app(l1y, h, dm, r))
514
515def b_m0a(-l: List<&1, T.BG>, r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, a: b_L1R<h, dm, l, Nil{}>) -> b_MR<0n, T.Halves{l, r}, n, h, dm>:
516 match a:
517 case b_L1R{l1y, sl, fl}:
518 b_m0b(l, r, n, h, dm, l1y, sl, fl, b_l1(r, h, dm, Nil{}))
519
520# depth 1 + e: each half cut in two and its b_tree (the closures run main at depth e), then the two maps appended
521def b_m1c(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.BG>, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.BG>}, +cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves<T.BG>, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.BG>}, +cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, -y1: List<&1, T.BG>, sy1: {y1 == T.hcat(T.BG, hh1) : List<&1, T.BG>}, f1: {T.bpar(e, hh1, TA.half(n), h, dm) == b_fmap(h, dm, T.hcat(T.BG, hh1)) : List<&1, T.DB>}, y2: List<&1, T.BG>, sy2: {y2 == T.hcat(T.BG, hh2) : List<&1, T.BG>}, f2: {T.bpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == b_fmap(h, dm, T.hcat(T.BG, hh2)) : List<&1, T.DB>}, ma: b_MAR<h, dm, y1, y2>) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>:
522 match ma:
523 case b_MAR{y1b, sb, fa}:
524 +ly1 = Equal.trans(List<&1, T.BG>, y1, T.hcat(T.BG, hh1), l, sy1, cat1)
525 +ly2 = Equal.trans(List<&1, T.BG>, y2, T.hcat(T.BG, hh2), r, sy2, cat2)
526 +q1 = Equal.trans(List<&1, T.DB>, T.bpar(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar(e, hh1, TA.half(n), h, dm), b_fmap(h, dm, l), Equal.cong(T.Halves<T.BG>, List<&1, T.DB>, z => T.bpar(e, z, TA.half(n), h, dm), T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), hh1, Equal.sym(T.Halves<T.BG>, hh1, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, T.DB>, T.bpar(e, hh1, TA.half(n), h, dm), b_fmap(h, dm, T.hcat(T.BG, hh1)), b_fmap(h, dm, l), f1, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), T.hcat(T.BG, hh1), l, cat1)))
527 +q2 = Equal.trans(List<&1, T.DB>, T.bpar(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), T.bpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_fmap(h, dm, r), Equal.cong(T.Halves<T.BG>, List<&1, T.DB>, z => T.bpar(e, z, Nat.sub(n, TA.half(n)), h, dm), T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), hh2, Equal.sym(T.Halves<T.BG>, hh2, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, T.DB>, T.bpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_fmap(h, dm, T.hcat(T.BG, hh2)), b_fmap(h, dm, r), f2, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), T.hcat(T.BG, hh2), r, cat2)))
528 +bb = Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), b_fmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), List.append(&1, T.BG, l, r), List.append(&1, T.BG, y1, y2), app2(T.BG, l, y1, r, y2, Equal.sym(List<&1, T.BG>, y1, l, ly1), Equal.sym(List<&1, T.BG>, y2, r, ly2))), Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_fmap(h, dm, y1), b_fmap(h, dm, y2)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), fa, app2(T.DB, b_fmap(h, dm, y1), b_fmap(h, dm, l), b_fmap(h, dm, y2), b_fmap(h, dm, r), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), y2, r, ly2))))
529 b_MR{List.append(&1, T.BG, y1b, y2), app2(T.BG, y1b, l, y2, r, Equal.trans(List<&1, T.BG>, y1b, y1, l, sb, ly1), ly2),
530 Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bpar(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), b_fmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bpar(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), b_fmap(h, dm, l), T.bpar(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), b_fmap(h, dm, r), q1, q2), Equal.sym(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), bb))}
531
532def b_m1b(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.BG>, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.BG>}, cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves<T.BG>, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.BG>}, cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, r1: b_MR<e, hh1, TA.half(n), h, dm>, r2: b_MR<e, hh2, Nat.sub(n, TA.half(n)), h, dm>) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>:
533 match r1 r2:
534 case b_MR{y1, sy1, f1} b_MR{y2, sy2, f2}:
535 b_m1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, b_map_app(y1, h, dm, y2))
536
537def b_m1a(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, c1: b_CGR<TA.half(TA.half(n)), l, Nil{}>, c2: b_CGR<TA.half(Nat.sub(n, TA.half(n))), r, Nil{}>, k1: @g: T.Halves<T.BG> -> b_MR<e, g, TA.half(n), h, dm>, k2: @g: T.Halves<T.BG> -> b_MR<e, g, Nat.sub(n, TA.half(n)), h, dm>) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>:
538 match c1 c2:
539 case b_CGR{hh1, s1, cat1} b_CGR{hh2, s2, cat2}:
540 b_m1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2))
541
542def b_tree(d: Nat, gs: T.Halves<T.BG>, +n: Nat, +h: Nat, +dm: T.Dm) -> b_MR<d, gs, n, h, dm>:
543 match d gs:
544 case 0n T.Halves{l, r}:
545 b_m0a(l, r, n, h, dm, b_l1(l, h, dm, Nil{}))
546 case 1n++e T.Halves{l, r}:
547 b_m1a(e, l, r, n, h, dm, b_cg(TA.half(TA.half(n)), l, Nil{}), b_cg(TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), g1 => b_tree(e, g1, TA.half(n), h, dm), g2 => b_tree(e, g2, Nat.sub(n, TA.half(n)), h, dm))
548
549# the law: the b_tree gives what fleaf, the loop over the sequences one after another, gives
550def b_par_fin(-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.BG>, +sy: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, f: {T.bpar(d, gs, n, h, dm) == b_fmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}, r: b_L1R<h, dm, ys, Nil{}>) -> {T.bpar(d, gs, n, h, dm) == T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}:
551 match r:
552 case b_L1R{ys2, s2, fl}:
553 Equal.trans(List<&1, T.DB>, T.bpar(d, gs, n, h, dm), b_fmap(h, dm, T.hcat(T.BG, gs)), T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}), f,
554 Equal.sym(List<&1, T.DB>, T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}), b_fmap(h, dm, T.hcat(T.BG, gs)),
555 Equal.trans(List<&1, T.DB>, T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}), T.bleaf(ys, h, dm, Nil{}), b_fmap(h, dm, T.hcat(T.BG, gs)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => T.bleaf(z, h, dm, Nil{}), T.hcat(T.BG, gs), ys, Equal.sym(List<&1, T.BG>, ys, T.hcat(T.BG, gs), sy)),
556 Equal.trans(List<&1, T.DB>, T.bleaf(ys, h, dm, Nil{}), b_fmap(h, dm, ys), b_fmap(h, dm, T.hcat(T.BG, gs)), fl, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), ys, T.hcat(T.BG, gs), sy)))))
557
558def b_par_mid(-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, r: b_MR<d, gs, n, h, dm>) -> {T.bpar(d, gs, n, h, dm) == T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}:
559 match r:
560 case b_MR{ys, sy, f}:
561 b_par_fin(d, gs, n, h, dm, ys, sy, f, b_l1(ys, h, dm, Nil{}))
562
563# PROOF (attn_par_bwd): attn_par_fwd's proof, for BG and bleaf.
564def Laws.attn_par_bwd(d, gs, n, h, dm):
565 b_par_mid(d, gs, n, h, dm, b_tree(d, gs, n, h, dm))
566
567# =====================================================================================================
568# Grouped-query heads (llama.bend's proof)
569# =====================================================================================================
570
571# one block of 1 + m numbers adds 1 to the quotient (Nat.divmod.go counts down the remainder from m)
572def div_block(+m: Nat, -n: Nat, -d: Nat, -r: Nat) -> {Nat.divmod.go(Nat.add(1n+m, n), m, d, r) == Nat.divmod.go(n, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}:
573 match m:
574 case 0n:
575 {==}
576 case 1n+p:
577 %Equal.sym(Nat, 1n+Nat.add(p, r), Nat.add(p, 1n+r), NL.add_succ(p, r)) : {Nat.divmod.go(Nat.add(1n+p, n), p, d, 1n+r) == Nat.divmod.go(n, _, 1n+d, 0n) : Nat & Nat}
578 div_block(p, n, d, 1n+r)
579
580# j whole blocks of 1 + s numbers add j to the quotient
581def div_blocks(+j: Nat, +s: Nat, +n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.add(Nat.mul(j, 1n+s), n), s, d, 0n) == Nat.divmod.go(n, s, Nat.add(j, d), 0n) : Nat & Nat}:
582 match j:
583 case 0n:
584 {==}
585 case 1n+jp:
586 %NL.add_assoc(1n+s, Nat.mul(jp, 1n+s), n) : {Nat.divmod.go(_, s, d, 0n) == Nat.divmod.go(n, s, Nat.add(1n+jp, d), 0n) : Nat & Nat}
587 %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(1n+s, Nat.add(Nat.mul(jp, 1n+s), n)), s, d, 0n), Nat.divmod.go(Nat.add(Nat.mul(jp, 1n+s), n), Nat.add(s, 0n), 1n+d, 0n), div_block(s, Nat.add(Nat.mul(jp, 1n+s), n), d, 0n)) : {_ == Nat.divmod.go(n, s, Nat.add(1n+jp, d), 0n) : Nat & Nat}
588 %Equal.sym(Nat, Nat.add(s, 0n), s, NL.add_zero(s)) : {Nat.divmod.go(Nat.add(Nat.mul(jp, 1n+s), n), _, 1n+d, 0n) == Nat.divmod.go(n, s, Nat.add(1n+jp, d), 0n) : Nat & Nat}
589 %Equal.sym(Nat, 1n+Nat.add(jp, d), Nat.add(jp, 1n+d), NL.add_succ(jp, d)) : {Nat.divmod.go(Nat.add(Nat.mul(jp, 1n+s), n), s, 1n+d, 0n) == Nat.divmod.go(n, s, _, 0n) : Nat & Nat}
590 div_blocks(jp, s, n, 1n+d)
591
592# fewer than 1 + s numbers after the last whole block leave the quotient alone
593def div_rest(+i: Nat, -k: Nat, -d: Nat, -r: Nat) -> {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), d, r)) == d : Nat}:
594 match i:
595 case 0n:
596 {==}
597 case 1n+p:
598 div_rest(p, k, d, 1n+r)
599
600# PROOF (gqa_head): Nat.div counts how many whole blocks of g numbers fit. j·g is j whole blocks (div_blocks), and
601# i < g numbers after them do not complete another one (div_rest).
602def Laws.gqa_head(j, i, k):
603 %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), Nat.add(i, k), 0n, 0n), Nat.divmod.go(i, Nat.add(i, k), Nat.add(j, 0n), 0n), div_blocks(j, Nat.add(i, k), i, 0n)) : {Pair.fst(Nat, Nat, _) == j : Nat}
604 %NL.add_zero(j) : {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), Nat.add(j, 0n), 0n)) == _ : Nat}
605 div_rest(i, k, Nat.add(j, 0n), 0n)
606
607# PROOF (kv_of_group): kv_of is Nat.div, so this is gqa_head.
608def Laws.kv_of_group(j, i, k):
609 Laws.gqa_head(j, i, k)
610
611# PROOF (kv_cols): head_cols' key column is kv_of(head, g)·hd; kv_of of a head of group j is j (kv_of_group).
612def Laws.kv_cols(t, hd, w, kvw, sc, j, i, k):
613 Equal.cong(Nat, U32, n => U32.from_nat(Nat.mul(n, hd)), T.kv_of(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), 1n+Nat.add(i, k)), j, Laws.kv_of_group(j, i, k))
614
615# =====================================================================================================
616# Tensors: shapes
617# =====================================================================================================
618
619# a || b == b || a, and a && b == b && a: every case computes
620def or_comm(+a: Bool, +b: Bool) -> {Bool.or(a, b) == Bool.or(b, a) : Bool}:
621 match a b:
622 case True{} True{}:
623 {==}
624 case True{} False{}:
625 {==}
626 case False{} True{}:
627 {==}
628 case False{} False{}:
629 {==}
630
631def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
632 match a b:
633 case True{} True{}:
634 {==}
635 case True{} False{}:
636 {==}
637 case False{} True{}:
638 {==}
639 case False{} False{}:
640 {==}
641
642# equal operands give equal conjunctions and disjunctions
643def and_cong(+p: Bool, +p2: Bool, +q: Bool, +q2: Bool, e: {p == p2 : Bool}, f: {q == q2 : Bool}) -> {Bool.and(p, q) == Bool.and(p2, q2) : Bool}:
644 Equal.trans(Bool, Bool.and(p, q), Bool.and(p2, q), Bool.and(p2, q2), Equal.cong(Bool, Bool, x => Bool.and(x, q), p, p2, e), Equal.cong(Bool, Bool, x => Bool.and(p2, x), q, q2, f))
645
646def or_cong(+p: Bool, +p2: Bool, +q: Bool, +q2: Bool, e: {p == p2 : Bool}, f: {q == q2 : Bool}) -> {Bool.or(p, q) == Bool.or(p2, q2) : Bool}:
647 Equal.trans(Bool, Bool.or(p, q), Bool.or(p2, q), Bool.or(p2, q2), Equal.cong(Bool, Bool, x => Bool.or(x, q), p, p2, e), Equal.cong(Bool, Bool, x => Bool.or(p2, x), q, q2, f))
648
649# one axis: bc_dim is written as pair(x, y) || pair(y, x), so swapping x and y only swaps the two sides of the ||
650def bc_dim_sym(+x: Nat, +y: Nat, +z: Nat) -> {TT.bc_dim(x, y, z) == TT.bc_dim(y, x, z) : Bool}:
651 or_comm(TT.bc_pair(x, y, z), TT.bc_pair(y, x, z))
652
653# axis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False
654# either way round
655def bc_eq_sym(a: List<&2, Nat>, b: List<&2, Nat>, o: List<&2, Nat>) -> {TT.bc_eq(a, b, o) == TT.bc_eq(b, a, o) : Bool}:
656 match a b o:
657 case Nil{} Nil{} Nil{}:
658 {==}
659 case Nil{} Nil{} Con{z, ro}:
660 {==}
661 case Nil{} Con{y, rb} Nil{}:
662 {==}
663 case Nil{} Con{y, rb} Con{z, ro}:
664 {==}
665 case Con{x, ra} Nil{} Nil{}:
666 {==}
667 case Con{x, ra} Nil{} Con{z, ro}:
668 {==}
669 case Con{x, ra} Con{y, rb} Nil{}:
670 {==}
671 case Con{+x, +ra} Con{+y, +rb} Con{+z, +ro}:
672 and_cong(TT.bc_dim(x, y, z), TT.bc_dim(y, x, z), TT.bc_eq(ra, rb, ro), TT.bc_eq(rb, ra, ro), bc_dim_sym(x, y, z), bc_eq_sym(ra, rb, ro))
673
674# the ranks: the same two comparisons and the same two equalities, in the other order
675def bc_rank_sym(+la: Nat, +lb: Nat, +lo: Nat) -> {TT.bc_rank(la, lb, lo) == TT.bc_rank(lb, la, lo) : Bool}:
676 and_cong(Bool.and(Nat.is_le(la, lo), Nat.is_le(lb, lo)), Bool.and(Nat.is_le(lb, lo), Nat.is_le(la, lo)), Bool.or(Nat.is_eq(la, lo), Nat.is_eq(lb, lo)), Bool.or(Nat.is_eq(lb, lo), Nat.is_eq(la, lo)),
677 and_comm(Nat.is_le(la, lo), Nat.is_le(lb, lo)), or_comm(Nat.is_eq(la, lo), Nat.is_eq(lb, lo)))
678
679def Laws.bc_sym(a, b, o):
680 and_cong(TT.bc_rank(List.length(&2, Nat, a), List.length(&2, Nat, b), List.length(&2, Nat, o)), TT.bc_rank(List.length(&2, Nat, b), List.length(&2, Nat, a), List.length(&2, Nat, o)),
681 TT.bc_eq(TT.pad(a, List.length(&2, Nat, o)), TT.pad(b, List.length(&2, Nat, o)), o), TT.bc_eq(TT.pad(b, List.length(&2, Nat, o)), TT.pad(a, List.length(&2, Nat, o)), o),
682 bc_rank_sym(List.length(&2, Nat, a), List.length(&2, Nat, b), List.length(&2, Nat, o)), bc_eq_sym(TT.pad(a, List.length(&2, Nat, o)), TT.pad(b, List.length(&2, Nat, o)), o))
683
684# h * (a * r) == a * (h * r): associativity, then commutativity of the first two factors, then associativity back
685def mul_swap(+h: Nat, +a: Nat, +r: Nat) -> {Nat.mul(h, Nat.mul(a, r)) == Nat.mul(a, Nat.mul(h, r)) : Nat}:
686 Equal.trans(Nat, Nat.mul(h, Nat.mul(a, r)), Nat.mul(Nat.mul(h, a), r), Nat.mul(a, Nat.mul(h, r)), NL.mul_assoc(h, a, r),
687 Equal.trans(Nat, Nat.mul(Nat.mul(h, a), r), Nat.mul(Nat.mul(a, h), r), Nat.mul(a, Nat.mul(h, r)),
688 Equal.cong(Nat, Nat, x => Nat.mul(x, r), Nat.mul(h, a), Nat.mul(a, h), NL.mul_comm(h, a)),
689 Equal.sym(Nat, Nat.mul(a, Nat.mul(h, r)), Nat.mul(Nat.mul(a, h), r), NL.mul_assoc(a, h, r))))
690
691# by induction on the shape and the axis: axis 0 computes; past it, the first size h stays in front on both sides, and
692# mul_swap moves it past size(k)
693def Laws.sum_numel(s, k):
694 match s k:
695 case Nil{} _:
696 {==}
697 case Con{h, t} 0n:
698 {==}
699 case Con{+h, +t} 1n+p:
700 Equal.trans(Nat, Nat.mul(h, NL.product(t)), Nat.mul(h, Nat.mul(TT.at1(t, p), NL.product(TT.remove(t, p)))), Nat.mul(TT.at1(t, p), Nat.mul(h, NL.product(TT.remove(t, p)))),
701 Equal.cong(Nat, Nat, x => Nat.mul(h, x), NL.product(t), Nat.mul(TT.at1(t, p), NL.product(TT.remove(t, p))), Laws.sum_numel(t, p)),
702 mul_swap(h, TT.at1(t, p), NL.product(TT.remove(t, p))))
703
704# =====================================================================================================
705# Tensors: narrow, cat, of_mat, permute
706# =====================================================================================================
707
708# by induction: axis 0 is replaced and then taken out; past it, the first size stays in front on both sides
709def Laws.narrow_rest(s, d, l):
710 match s d:
711 case Nil{} _:
712 {==}
713 case Con{h, t} 0n:
714 {==}
715 case Con{+h, +t} 1n+p:
716 Equal.cong(List<&2, Nat>, List<&2, Nat>, x => h <> x, TT.remove(TT.setd(t, p, l), p), TT.remove(t, p), Laws.narrow_rest(t, p, l))
717
718# a shape with no axis d contradicts the premise (d < rank is False); axis 0 is l; past it, the induction
719def Laws.narrow_axis(s, d, l, e):
720 match s d:
721 case Nil{} 0n:
722 Empty.absurd({TT.at1(TT.setd([], 0n, l), 0n) == l : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
723 case Nil{} 1n+p:
724 Empty.absurd({TT.at1(TT.setd([], 1n+p, l), 1n+p) == l : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
725 case Con{h, t} 0n:
726 {==}
727 case Con{h, +t} 1n+p:
728 Laws.narrow_axis(t, p, l, e)
729
730# axis 0: (x + y)·n == x·n + y·n (distributivity); past it, the induction and k·(a + b) == k·a + k·b
731def Laws.cat_numel(s, d, x, y, e):
732 match s d:
733 case Nil{} 0n:
734 Empty.absurd({TT.numel(TT.setd([], 0n, Nat.add(x, y))) == Nat.add(TT.numel(TT.setd([], 0n, x)), TT.numel(TT.setd([], 0n, y))) : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
735 case Nil{} 1n+p:
736 Empty.absurd({TT.numel(TT.setd([], 1n+p, Nat.add(x, y))) == Nat.add(TT.numel(TT.setd([], 1n+p, x)), TT.numel(TT.setd([], 1n+p, y))) : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
737 case Con{h, +t} 0n:
738 Equal.sym(Nat, Nat.add(Nat.mul(x, NL.product(t)), Nat.mul(y, NL.product(t))), Nat.mul(Nat.add(x, y), NL.product(t)), NL.mul_dist(x, y, NL.product(t)))
739 case Con{+h, +t} 1n+p:
740 Equal.trans(Nat, Nat.mul(h, NL.product(TT.setd(t, p, Nat.add(x, y)))), Nat.mul(h, Nat.add(NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y)))), Nat.add(Nat.mul(h, NL.product(TT.setd(t, p, x))), Nat.mul(h, NL.product(TT.setd(t, p, y)))),
741 Equal.cong(Nat, Nat, v => Nat.mul(h, v), NL.product(TT.setd(t, p, Nat.add(x, y))), Nat.add(NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y))), Laws.cat_numel(t, p, x, y, e)),
742 NL.mul_dist_l(h, NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y))))
743
744# r·(c·1) == r·c: c·1 == c
745def Laws.mat_numel(r, c):
746 Equal.cong(Nat, Nat, v => Nat.mul(r, v), Nat.mul(c, 1n), c, NL.mul_one_r(c))
747
748# one axis of the result per entry of p
749def Laws.permute_rank(s, p):
750 match p:
751 case Nil{}:
752 {==}
753 case Con{k, r}:
754 Equal.cong(Nat, Nat, v => 1n+v, TT.rank(TT.permuted(s, r)), List.length(&2, Nat, r), Laws.permute_rank(s, r))
755
756# =====================================================================================================
757# The order of a row's additions (block_sum)
758# =====================================================================================================
759
760# one pass over 2k blocks of 2^p cells gives the k blocks of 2^(p+1) cells: the pass adds blocks 2j and 2j+1, the two
761# halves bal puts under one node. Induction on k; add_succ turns k + (k + 1) into 2 + (k + k), and add_assoc moves the
762# next pair's start from (lo + 2^p) + 2^p to lo + 2^(p+1)
763def pass_pair(+p: Nat, +k: Nat, +lo: Nat) -> {Spec.spass(Spec.blocks(p, Nat.add(k, k), lo)) == Spec.blocks(1n+p, k, lo) : List<&2, Spec.Sum>}:
764 match k:
765 case 0n:
766 {==}
767 case 1n+j:
768 +a = Spec.pw(p)
769 +nx = Nat.add(Nat.add(lo, a), a)
770 %NL.add_succ(j, j) : {Spec.spass(Spec.blocks(p, 1n+_, lo)) == Spec.blocks(1n+p, 1n+j, lo) : List<&2, Spec.Sum>}
771 %Equal.sym(Nat, Nat.add(lo, Nat.add(a, a)), nx, NL.add_assoc(lo, a, a)) : {Spec.spass(Spec.blocks(p, 1n+1n+Nat.add(j, j), lo)) == Spec.SAdd{Spec.bal(p, lo), Spec.bal(p, Nat.add(lo, a))} <> Spec.blocks(1n+p, j, _) : List<&2, Spec.Sum>}
772 %pass_pair(p, j, nx) : {Spec.spass(Spec.blocks(p, 1n+1n+Nat.add(j, j), lo)) == Spec.SAdd{Spec.bal(p, lo), Spec.bal(p, Nat.add(lo, a))} <> _ : List<&2, Spec.Sum>}
773 {==}
774
775# 2^(p+1) · k cells are 2^p · 2k: (a + a)·k == a·k + a·k == a·(k + k)
776def cnt2(+p: Nat, +k: Nat) -> {Nat.mul(Spec.pw(1n+p), k) == Nat.mul(Spec.pw(p), Nat.add(k, k)) : Nat}:
777 +a = Spec.pw(p)
778 Equal.trans(Nat, Nat.mul(Nat.add(a, a), k), Nat.add(Nat.mul(a, k), Nat.mul(a, k)), Nat.mul(a, Nat.add(k, k)),
779 Equal.sym(Nat, Nat.add(Nat.mul(a, k), Nat.mul(a, k)), Nat.mul(Nat.add(a, a), k), NL.mul_dist(a, a, k)),
780 Equal.sym(Nat, Nat.mul(a, Nat.add(k, k)), Nat.add(Nat.mul(a, k), Nat.mul(a, k)), NL.mul_dist_l(a, k, k)))
781
782# the first p passes over a row of 2^p · k cells leave its k blocks, each summed as bal sums it. Induction on p: p
783# passes over 2^(p+1)·k cells (= 2^p·2k, cnt2) leave 2k blocks of 2^p, and one more pass pairs them (pass_pair)
784def blocks_passes(+p: Nat, +k: Nat, +lo: Nat) -> {Spec.passes(p, Spec.blocks(0n, Nat.mul(Spec.pw(p), k), lo)) == Spec.blocks(p, k, lo) : List<&2, Spec.Sum>}:
785 match p:
786 case 0n:
787 %NL.mul_one_l(k) : {Spec.blocks(0n, Nat.mul(1n, k), lo) == Spec.blocks(0n, _, lo) : List<&2, Spec.Sum>}
788 {==}
789 case 1n+q:
790 +kk = Nat.add(k, k)
791 %Equal.sym(Nat, Nat.mul(Spec.pw(1n+q), k), Nat.mul(Spec.pw(q), kk), cnt2(q, k)) : {Spec.spass(Spec.passes(q, Spec.blocks(0n, _, lo))) == Spec.blocks(1n+q, k, lo) : List<&2, Spec.Sum>}
792 %Equal.sym(List<&2, Spec.Sum>, Spec.passes(q, Spec.blocks(0n, Nat.mul(Spec.pw(q), kk), lo)), Spec.blocks(q, kk, lo), blocks_passes(q, kk, lo)) : {Spec.spass(_) == Spec.blocks(1n+q, k, lo) : List<&2, Spec.Sum>}
793 pass_pair(q, k, lo)
794
795# r + p passes are p passes, then r more
796def passes_add(r: Nat, +p: Nat, +xs: List<&2, Spec.Sum>) -> {Spec.passes(Nat.add(r, p), xs) == Spec.passes(r, Spec.passes(p, xs)) : List<&2, Spec.Sum>}:
797 match r:
798 case 0n:
799 {==}
800 case 1n+q:
801 Equal.cong(List<&2, Spec.Sum>, List<&2, Spec.Sum>, z => Spec.spass(z), Spec.passes(Nat.add(q, p), xs), Spec.passes(q, Spec.passes(p, xs)), passes_add(q, p, xs))
802
803# block_sum: r + p passes over the row are r passes over what its first p passes leave (passes_add), which is its k
804# blocks summed as bal sums them (blocks_passes)
805def Laws.block_sum(p, k, r):
806 +row = Spec.blocks(0n, Nat.mul(Spec.pw(p), k), 0n)
807 Equal.trans(List<&2, Spec.Sum>, Spec.passes(Nat.add(r, p), row), Spec.passes(r, Spec.passes(p, row)), Spec.passes(r, Spec.blocks(p, k, 0n)),
808 passes_add(r, p, row),
809 Equal.cong(List<&2, Spec.Sum>, List<&2, Spec.Sum>, z => Spec.passes(r, z), Spec.passes(p, row), Spec.blocks(p, k, 0n), blocks_passes(p, k, 0n)))
810
811def main() -> Unit:
812 Unit{}