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 4 import Base 5 import ./main.bend as T 6 import ./spec.bend as Spec 7 import ./tensor.bend as TT 8 import ./LAWS.bend as Laws 9 import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL 10 import 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 18 def 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 38 def 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) 53 def 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. 72 def 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. 90 def 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. 108 def 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. 117 def 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. 122 def 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 129 def 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 137 def 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 142 def 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 150 def 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). 158 def 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 162 def 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) 170 def cnt_div(q: Array, k: Array, kk: Nat, +idx: U32, +s: F32, +c: Nat, r: Array & 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) 178 def cnt_psm3(q: Array, k: Array, +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 183 def cnt_psm2(q: Array, k: Array, +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) 189 def cnt_pw(+xs: List<&2, F32>, +idx: U32, +sc: F32, +n: Nat, +off: U32, q: Array, k: Array, p: Array) -> {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 197 def 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) -> {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). 214 def 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) 218 def cnt_gw(+xs: List<&2, F32>, +idx: U32, +n: Nat, +sc: F32, +off: U32, d: Array, v: Array, p: Array, g: Array) -> {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) 226 def 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, ga: Array) -> {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). 237 def 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 245 def 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 250 def fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array>: 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 259 type L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array>> 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, acc, fmap(h, dm, xs)) : List<&1, Array>}} 261 262 def l1_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array>, r: L1R acc>) -> L1R 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 267 def l1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array>) -> L1R: 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 276 type 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, fmap(h, dm, a), fmap(h, dm, b)) : List<&1, Array>}} 278 279 def ma_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>, r: MAR) -> MAR 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>, List<&1, Array>, 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, fmap(h, dm, t), fmap(h, dm, b)), fact)} 283 284 def map_app(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MAR: 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 293 type 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 296 def ga_con(x: T.FS, -t: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>, r: GAR b, c>) -> GAR 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 301 def go_app(a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>) -> GAR: 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 310 type CGR<-k: Nat, -xs: List<&1, T.FS>, -acc: List<&1, T.FS>> is Type: 311 CGR{hh: T.Halves, same: {hh == T.cut(T.FS, k, xs, acc) : T.Halves}, cat: {T.hcat(T.FS, hh) == List.reverse.go(&1, T.FS, acc, xs) : List<&1, T.FS>}} 312 313 def 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}, r: GAR) -> CGR: 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.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, z => T.Halves{List.reverse(&1, T.FS, z), xs}, ys, acc, same), Equal.sym(T.Halves, 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 320 def cg_con(-m: Nat, -x: T.FS, -t: List<&1, T.FS>, -acc: List<&1, T.FS>, r: CGR acc>) -> CGR<1n+m, x <> t, acc>: 321 match r: 322 case CGR{hh, same, cat}: 323 CGR{hh, same, cat} 324 325 def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR: 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 336 type MR<-d: Nat, -gs: T.Halves, -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>}} 338 339 # depth 0: the two leaves' loops, appended 340 def 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>}, 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>}, c: MAR) -> 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>, List.append(&1, Array, T.fleaf(l, h, dm, Nil{}), T.fleaf(r, h, dm, Nil{})), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), fmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array, 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>, fmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), 346 Equal.trans(List<&1, Array>, fmap(h, dm, List.append(&1, T.FS, l, r)), fmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array>, 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>, fmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array, fmap(h, dm, l1y), fmap(h, dm, r)), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), fa, Equal.cong(List<&1, T.FS>, List<&1, Array>, z => List.append(&1, Array, fmap(h, dm, z), fmap(h, dm, r)), l1y, l, sl)))))} 348 349 def 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>}, b: L1R) -> 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 354 def m0a(-l: List<&1, T.FS>, r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, a: L1R) -> 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 360 def m1c(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves}, +cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves}, +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>}, 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>}, ma: MAR) -> 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>, 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, List<&1, Array>, 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, hh1, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, Array>, 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>, z => fmap(h, dm, z), T.hcat(T.FS, hh1), l, cat1))) 366 +q2 = Equal.trans(List<&1, Array>, 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, List<&1, Array>, 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, hh2, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, Array>, 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>, z => fmap(h, dm, z), T.hcat(T.FS, hh2), r, cat2))) 367 +bb = Equal.trans(List<&1, Array>, fmap(h, dm, List.append(&1, T.FS, l, r)), fmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array>, 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>, fmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array, fmap(h, dm, y1), fmap(h, dm, y2)), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), fa, app2(Array, 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>, z => fmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.FS>, List<&1, Array>, 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>, List.append(&1, Array, 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, fmap(h, dm, l), fmap(h, dm, r)), fmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array, 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>, fmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array, fmap(h, dm, l), fmap(h, dm, r)), bb))} 370 371 def m1b(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves}, cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves}, cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, r1: MR, r2: MR) -> 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 376 def m1a(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, c1: CGR, c2: CGR, k1: @g: T.Halves -> MR, k2: @g: T.Halves -> MR) -> 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 381 def tree(d: Nat, gs: T.Halves, +n: Nat, +h: Nat, +dm: T.Dm) -> MR: 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 389 def par_fin(-d: Nat, -gs: T.Halves, -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>}, r: L1R) -> {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array>}: 390 match r: 391 case L1R{ys2, s2, fl}: 392 Equal.trans(List<&1, Array>, 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>, T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), fmap(h, dm, T.hcat(T.FS, gs)), 394 Equal.trans(List<&1, Array>, 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>, 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>, 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>, z => fmap(h, dm, z), ys, T.hcat(T.FS, gs), sy))))) 396 397 def par_mid(-d: Nat, -gs: T.Halves, -n: Nat, +h: Nat, +dm: T.Dm, r: MR) -> {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array>}: 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). 406 def 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 411 def 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 420 type 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 423 def b_l1_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>, r: b_L1R acc>) -> b_L1R 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 428 def b_l1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1R: 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 437 type 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 440 def b_ma_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>, r: b_MAR) -> b_MAR 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 445 def b_map_app(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MAR: 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 454 type 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 457 def b_ga_con(x: T.BG, -t: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>, r: b_GAR b, c>) -> b_GAR 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 462 def b_go_app(a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>) -> b_GAR: 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 471 type b_CGR<-k: Nat, -xs: List<&1, T.BG>, -acc: List<&1, T.BG>> is Type: 472 b_CGR{hh: T.Halves, same: {hh == T.cut(T.BG, k, xs, acc) : T.Halves}, cat: {T.hcat(T.BG, hh) == List.reverse.go(&1, T.BG, acc, xs) : List<&1, T.BG>}} 473 474 def 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}, r: b_GAR) -> b_CGR: 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.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, z => T.Halves{List.reverse(&1, T.BG, z), xs}, ys, acc, same), Equal.sym(T.Halves, 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 481 def b_cg_con(-m: Nat, -x: T.BG, -t: List<&1, T.BG>, -acc: List<&1, T.BG>, r: b_CGR 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 486 def b_cg(k: Nat, xs: List<&1, T.BG>, acc: List<&1, T.BG>) -> b_CGR: 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 497 type b_MR<-d: Nat, -gs: T.Halves, -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 501 def 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) -> 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 510 def 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) -> 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 515 def b_m0a(-l: List<&1, T.BG>, r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, a: b_L1R) -> 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 521 def b_m1c(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves}, +cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves}, +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) -> 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, 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, 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, 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, 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 532 def b_m1b(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves}, cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves}, cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, r1: b_MR, r2: b_MR) -> 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 537 def b_m1a(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, c1: b_CGR, c2: b_CGR, k1: @g: T.Halves -> b_MR, k2: @g: T.Halves -> b_MR) -> 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 542 def b_tree(d: Nat, gs: T.Halves, +n: Nat, +h: Nat, +dm: T.Dm) -> b_MR: 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 550 def b_par_fin(-d: Nat, -gs: T.Halves, -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) -> {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 558 def b_par_mid(-d: Nat, -gs: T.Halves, -n: Nat, +h: Nat, +dm: T.Dm, r: b_MR) -> {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. 564 def 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) 572 def 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 581 def 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 593 def 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). 602 def 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. 608 def 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). 612 def 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 620 def 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 631 def 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 643 def 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 646 def 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 || 650 def 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 655 def 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 675 def 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 679 def 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 685 def 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) 693 def 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 709 def 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 719 def 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 731 def 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 745 def 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 749 def 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) 763 def 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) 776 def 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) 784 def 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 796 def 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) 805 def 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 811 def main() -> Unit: 812 Unit{}