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.18.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 # PROOF (both_sum): Both runs each layer on its own side, so both sides are pairs of linear passes; each half of the sum 130 # is its layer's adjoint law. 131 def Laws.both_sum(w1, w2, x1, x2, dy1, dy2, g1, g2): 132 Equal.trans(Nat, Nat.add(Spec.dotn(dy1, Spec.mv(w1, x1)), Spec.dotn(dy2, Spec.mv(w2, x2))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x1), Spec.dotn(dy2, Spec.mv(w2, x2))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x1), Spec.dotn(Spec.mtv(w2, dy2), x2)), 133 Equal.cong(Nat, Nat, z => Nat.add(z, Spec.dotn(dy2, Spec.mv(w2, x2))), Spec.dotn(dy1, Spec.mv(w1, x1)), Spec.dotn(Spec.mtv(w1, dy1), x1), Laws.adjoint(w1, dy1, x1)), 134 Equal.cong(Nat, Nat, z => Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x1), z), Spec.dotn(dy2, Spec.mv(w2, x2)), Spec.dotn(Spec.mtv(w2, dy2), x2), Laws.adjoint(w2, dy2, x2))) 135 136 # PROOF (residual): the forward pass gives x + W·x and the backward pass dy + Wᵀ·dy (Id hands dy back, the linear layer 137 # Wᵀ·dy, Fork adds them). Then dy·(x + W·x) = x·dy + (W·x)·dy (dot_comm, dot_vadd) = dy·x + dy·(W·x) (dot_comm twice) 138 # = dy·x + (Wᵀ·dy)·x (adjoint) = (dy + Wᵀ·dy)·x (dot_vadd). 139 def Laws.residual(w, x, dy, g): 140 +wx = Spec.mv(w, x) 141 +wd = Spec.mtv(w, dy) 142 Equal.trans(Nat, Spec.dotn(dy, Spec.vadd(x, wx)), Spec.dotn(Spec.vadd(x, wx), dy), Spec.dotn(Spec.vadd(dy, wd), x), 143 dot_comm(dy, Spec.vadd(x, wx)), 144 Equal.trans(Nat, Spec.dotn(Spec.vadd(x, wx), dy), Nat.add(Spec.dotn(x, dy), Spec.dotn(wx, dy)), Spec.dotn(Spec.vadd(dy, wd), x), 145 dot_vadd(x, wx, dy), 146 Equal.trans(Nat, Nat.add(Spec.dotn(x, dy), Spec.dotn(wx, dy)), Nat.add(Spec.dotn(dy, x), Spec.dotn(wx, dy)), Spec.dotn(Spec.vadd(dy, wd), x), 147 Equal.cong(Nat, Nat, z => Nat.add(z, Spec.dotn(wx, dy)), Spec.dotn(x, dy), Spec.dotn(dy, x), dot_comm(x, dy)), 148 Equal.trans(Nat, Nat.add(Spec.dotn(dy, x), Spec.dotn(wx, dy)), Nat.add(Spec.dotn(dy, x), Spec.dotn(wd, x)), Spec.dotn(Spec.vadd(dy, wd), x), 149 Equal.cong(Nat, Nat, z => Nat.add(Spec.dotn(dy, x), z), Spec.dotn(wx, dy), Spec.dotn(wd, x), 150 Equal.trans(Nat, Spec.dotn(wx, dy), Spec.dotn(dy, wx), Spec.dotn(wd, x), dot_comm(wx, dy), Laws.adjoint(w, dy, x))), 151 Equal.sym(Nat, Spec.dotn(Spec.vadd(dy, wd), x), Nat.add(Spec.dotn(dy, x), Spec.dotn(wd, x)), dot_vadd(dy, wd, x)))))) 152 153 def disc(b: Bool) -> Type: 154 match b: 155 case True{}: 156 Unit 157 case False{}: 158 Empty 159 160 # False == True is impossible: rewriting the goal Empty = disc(False) with it gives disc(True) = Unit 161 def false_true(e: {False{} == True{} : Bool}) -> Empty: 162 %Equal.sym(Bool, False{}, True{}, e) : disc(_) 163 Unit{} 164 165 # xs reversed onto acc has the length of both 166 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}: 167 match xs: 168 case Nil{}: 169 {==} 170 case Con{+x, +t}: 171 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)))) 172 173 # drow's row has the current dot, the m after it, and acc: 1 + m + |acc| numbers 174 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}: 175 match m r: 176 case 0n T.D2{a, b, +s}: 177 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))) 178 case 1n++p T.D2{a, b, +s}: 179 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))))) 180 181 # PROOF (causal_keys): qrow is drow(i, ..) from an empty accumulator, so its row has 1 + i + 0 numbers (len_drow). 182 def Laws.causal_keys(i, hd, qs, qc, ks, kc, q, k): 183 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)) 184 185 # n - 0 is n 186 def sub0(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}: 187 match n: 188 case 0n: 189 {==} 190 case 1n+p: 191 {==} 192 193 # 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) 194 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}: 195 match kk r: 196 case 0n Tuple{a, +x}: 197 {==} 198 case 1n++j Tuple{a, +x}: 199 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)))) 200 201 # the whole softmax over 1 + kk numbers reports 1 + kk, whatever max and exp found (they are matched, not computed) 202 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}: 203 match r: 204 case T.AS{a, +s}: 205 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)) 206 207 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}: 208 match r: 209 case T.AS{a, +m}: 210 cnt_psm3(q, k, kk, off, T.pexp(kk, off, m, 0.0, Array.get(F32, a, off))) 211 212 # pw writes xs and counts them from n; the softmax prow3 runs on them reports 1 + (|xs| + n - 1) 213 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}: 214 match xs: 215 case Nil{}: 216 cnt_psm2(q, k, Nat.sub(n, 1n), off, T.pmax0(Nat.sub(n, 1n), off, Array.get(F32, p, off))) 217 case Con{+x, +t}: 218 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)))) 219 220 # the count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw 221 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}: 222 match m r: 223 case 0n T.D2{a, b, +s}: 224 +rw = T.rcat(s <> acc, Nil{}) 225 +la = List.length(&2, F32, acc) 226 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), 227 Equal.cong(Nat, Nat, z => 1n+z, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), la, 228 Equal.trans(Nat, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), Nat.sub(1n+la, 1n), la, 229 Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(List.length(&2, F32, rw), 0n), 1n+la, 230 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)), 231 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)))), 232 sub0(la)))) 233 case 1n++p T.D2{a, b, +s}: 234 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))))) 235 236 # PROOF (causal): prow runs prow2 on qrow's row, drow(i, ..) from an empty accumulator, so the count it hands the 237 # softmax is 1 + i + 0 (cnt_drow). 238 def Laws.causal(i, t, hd, sc, qs, qc, ks, kc, q, k, p): 239 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)) 240 241 # gw writes xs and counts them from n: gr3 hands on |xs| + n (as cnt_pw for the forward pass) 242 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}: 243 match xs: 244 case Nil{}: 245 {==} 246 case Con{+x, +t}: 247 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))) 248 249 # the count gr2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_gw (cnt_drow's twin) 250 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}: 251 match m r: 252 case 0n T.D2{a, b, +s}: 253 +rw = T.rcat(s <> acc, Nil{}) 254 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), 255 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)), 256 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))))) 257 case 1n++p T.D2{a, b, +s}: 258 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))))) 259 260 # PROOF (causal_grad): grow runs gr2 on drow(i, ..) from an empty accumulator, so the count is 1 + i + 0 (cnt_gdrow). 261 def Laws.causal_grad(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g): 262 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)) 263 264 # PROOF (full_keys, full, full_grad): the causal proofs with m in place of i, because a full row reads every key 265 # 0..m; the row's count is then 1 + m from the same drow lemmas. 266 def Laws.full_keys(i, m, hd, qs, qc, ks, kc, q, k): 267 Equal.trans(Nat, List.length(&2, F32, T.dr_row(T.frow(i, m, hd, qs, qc, ks, kc, q, k))), Nat.add(1n+m, 0n), 1n+m, len_drow(m, 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+m)) 268 269 def Laws.full(i, m, hd, sc, qs, qc, ks, kc, q, k, pa): 270 Equal.trans(Nat, T.pr_n(T.fprow(i, m, hd, sc, qs, qc, ks, kc, q, k, pa)), Nat.add(1n+m, 0n), 1n+m, cnt_drow(m, 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(1n+m) : U32), pa), NL.add_zero(1n+m)) 271 272 def Laws.full_grad(i, m, hd, sc, ds, dc, vs, vc, d, v, pa, ga): 273 Equal.trans(Nat, T.gr_n(T.fgrow(i, m, hd, sc, ds, dc, vs, vc, d, v, pa, ga)), Nat.add(1n+m, 0n), 1n+m, cnt_gdrow(m, 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(1n+m) : U32), pa, ga), NL.add_zero(1n+m)) 274 275 # ===================================================================================================== 276 # Attention's trees of sequences: parallel = sequential 277 # ===================================================================================================== 278 279 # a ++ b == a2 ++ b2 from a == a2 and b == b2 280 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>}: 281 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)) 282 283 # ---- the sequential map the tree is compared with: f(x) = fs_o(fheads(h, 0, dm, x)) for each x, in order ---- 284 285 def fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array>: 286 match xs: 287 case Nil{}: 288 Nil{} 289 case Con{x, t}: 290 T.fs_o(T.fheads(h, 0n, dm, x)) <> fmap(h, dm, t) 291 292 # ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ---- 293 294 type L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array>> is Type: 295 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>}} 296 297 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>: 298 match r: 299 case L1R{ys, same, fact}: 300 L1R{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact} 301 302 def l1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array>) -> L1R: 303 match xs: 304 case Nil{}: 305 L1R{Nil{}, {==}, {==}} 306 case Con{x, t}: 307 l1_con(x, t, h, dm, acc, l1(t, h, dm, T.fs_o(T.fheads(h, 0n, dm, x)) <> acc)) 308 309 # ---- the map of two lists appended is the two maps appended ---- 310 311 type MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type: 312 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>}} 313 314 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>: 315 match r: 316 case MAR{ys, same, fact}: 317 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)} 318 319 def map_app(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MAR: 320 match a: 321 case Nil{}: 322 MAR{Nil{}, {==}, {==}} 323 case Con{x, t}: 324 ma_con(x, t, h, dm, b, map_app(t, h, dm, b)) 325 326 # ---- a reversed onto b, then c appended: a reversed onto b ++ c ---- 327 328 type GAR<-a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>> is Type: 329 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>}} 330 331 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>: 332 match r: 333 case GAR{ys, same, fact}: 334 GAR{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact} 335 336 def go_app(a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>) -> GAR: 337 match a: 338 case Nil{}: 339 GAR{Nil{}, {==}, {==}} 340 case Con{x, t}: 341 ga_con(x, t, b, c, go_app(t, x <> b, c)) 342 343 # ---- cut gives two halves that, appended, are acc reversed onto xs ---- 344 345 type CGR<-k: Nat, -xs: List<&1, T.FS>, -acc: List<&1, T.FS>> is Type: 346 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>}} 347 348 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: 349 match r: 350 case GAR{ys, +same, fact}: 351 CGR{T.Halves{List.reverse(&1, T.FS, ys), xs}, 352 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)), 353 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)} 354 355 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>: 356 match r: 357 case CGR{hh, same, cat}: 358 CGR{hh, same, cat} 359 360 def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR: 361 match k xs: 362 case 1n+m Con{x, t}: 363 cg_con(m, x, t, acc, cg(m, t, x <> acc)) 364 case 0n ys: 365 cg_base(0n, ys, acc, {==}, go_app(acc, Nil{}, ys)) 366 case 1n+m Nil{}: 367 cg_base(1n+m, Nil{}, acc, {==}, go_app(acc, Nil{}, Nil{})) 368 369 # ---- the tree: fpar at depth d on two halves is the map of the halves appended ---- 370 371 type MR<-d: Nat, -gs: T.Halves, -n: Nat, -h: Nat, -dm: T.Dm> is Type: 372 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>}} 373 374 # depth 0: the two leaves' loops, appended 375 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>: 376 match c: 377 case MAR{l2, s2, fa}: 378 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), 379 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), 380 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)), 381 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)), 382 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)))))} 383 384 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>: 385 match b: 386 case L1R{r1, sr, fr}: 387 m0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, map_app(l1y, h, dm, r)) 388 389 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>: 390 match a: 391 case L1R{l1y, sl, fl}: 392 m0b(l, r, n, h, dm, l1y, sl, fl, l1(r, h, dm, Nil{})) 393 394 # depth 1 + e: each half cut in two and its tree (the closures run main at depth e), then the two maps appended 395 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>: 396 match ma: 397 case MAR{y1b, sb, fa}: 398 +ly1 = Equal.trans(List<&1, T.FS>, y1, T.hcat(T.FS, hh1), l, sy1, cat1) 399 +ly2 = Equal.trans(List<&1, T.FS>, y2, T.hcat(T.FS, hh2), r, sy2, cat2) 400 +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))) 401 +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))) 402 +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)))) 403 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), 404 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))} 405 406 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>: 407 match r1 r2: 408 case MR{y1, sy1, f1} MR{y2, sy2, f2}: 409 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)) 410 411 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>: 412 match c1 c2: 413 case CGR{hh1, s1, cat1} CGR{hh2, s2, cat2}: 414 m1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2)) 415 416 def tree(d: Nat, gs: T.Halves, +n: Nat, +h: Nat, +dm: T.Dm) -> MR: 417 match d gs: 418 case 0n T.Halves{l, r}: 419 m0a(l, r, n, h, dm, l1(l, h, dm, Nil{})) 420 case 1n++e T.Halves{l, r}: 421 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)) 422 423 # the law: the tree gives what fleaf, the loop over the sequences one after another, gives 424 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>}: 425 match r: 426 case L1R{ys2, s2, fl}: 427 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, 428 Equal.sym(List<&1, Array>, T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), fmap(h, dm, T.hcat(T.FS, gs)), 429 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)), 430 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))))) 431 432 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>}: 433 match r: 434 case MR{ys, sy, f}: 435 par_fin(d, gs, n, h, dm, ys, sy, f, l1(ys, h, dm, Nil{})) 436 437 def ffmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array>: 438 match xs: 439 case Nil{}: 440 Nil{} 441 case Con{x, t}: 442 T.fs_o(T.fheads_full(h, 0n, dm, x)) <> ffmap(h, dm, t) 443 444 # ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ---- 445 446 type L1RF<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array>> is Type: 447 L1RF{ys: List<&1, T.FS>, same: {ys == xs : List<&1, T.FS>}, fact: {T.fleaf_full(xs, h, dm, acc) == List.reverse.go(&1, Array, acc, ffmap(h, dm, xs)) : List<&1, Array>}} 448 449 def lf_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array>, r: L1RF acc>) -> L1RF t, acc>: 450 match r: 451 case L1RF{ys, same, fact}: 452 L1RF{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact} 453 454 def lf1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array>) -> L1RF: 455 match xs: 456 case Nil{}: 457 L1RF{Nil{}, {==}, {==}} 458 case Con{x, t}: 459 lf_con(x, t, h, dm, acc, lf1(t, h, dm, T.fs_o(T.fheads_full(h, 0n, dm, x)) <> acc)) 460 461 # ---- the map of two lists appended is the two maps appended ---- 462 463 type MARF<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type: 464 MARF{ys: List<&1, T.FS>, same: {ys == a : List<&1, T.FS>}, fact: {ffmap(h, dm, List.append(&1, T.FS, a, b)) == List.append(&1, Array, ffmap(h, dm, a), ffmap(h, dm, b)) : List<&1, Array>}} 465 466 def ma_conf(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>, r: MARF) -> MARF t, b>: 467 match r: 468 case MARF{ys, same, fact}: 469 MARF{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_full(h, 0n, dm, x)) <> z, ffmap(h, dm, List.append(&1, T.FS, t, b)), List.append(&1, Array, ffmap(h, dm, t), ffmap(h, dm, b)), fact)} 470 471 def map_appf(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MARF: 472 match a: 473 case Nil{}: 474 MARF{Nil{}, {==}, {==}} 475 case Con{x, t}: 476 ma_conf(x, t, h, dm, b, map_appf(t, h, dm, b)) 477 478 # ---- a reversed onto b, then c appended: a reversed onto b ++ c ---- 479 480 type MRF<-d: Nat, -gs: T.Halves, -n: Nat, -h: Nat, -dm: T.Dm> is Type: 481 MRF{ys: List<&1, T.FS>, same: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, fact: {T.fpar_full(d, gs, n, h, dm) == ffmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array>}} 482 483 # depth 0: the two leaves' loops, appended 484 def fm0c(-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_full(l, h, dm, Nil{}) == ffmap(h, dm, l) : List<&1, Array>}, r1: List<&1, T.FS>, sr: {r1 == r : List<&1, T.FS>}, fr: {T.fleaf_full(r, h, dm, Nil{}) == ffmap(h, dm, r) : List<&1, Array>}, c: MARF) -> MRF<0n, T.Halves{l, r}, n, h, dm>: 485 match c: 486 case MARF{l2, s2, fa}: 487 MRF{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), 488 Equal.trans(List<&1, Array>, List.append(&1, Array, T.fleaf_full(l, h, dm, Nil{}), T.fleaf_full(r, h, dm, Nil{})), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), ffmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array, T.fleaf_full(l, h, dm, Nil{}), ffmap(h, dm, l), T.fleaf_full(r, h, dm, Nil{}), ffmap(h, dm, r), fl, fr), 489 Equal.sym(List<&1, Array>, ffmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), 490 Equal.trans(List<&1, Array>, ffmap(h, dm, List.append(&1, T.FS, l, r)), ffmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(h, dm, List.append(&1, T.FS, z, r)), l, l1y, Equal.sym(List<&1, T.FS>, l1y, l, sl)), 491 Equal.trans(List<&1, Array>, ffmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array, ffmap(h, dm, l1y), ffmap(h, dm, r)), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), fa, Equal.cong(List<&1, T.FS>, List<&1, Array>, z => List.append(&1, Array, ffmap(h, dm, z), ffmap(h, dm, r)), l1y, l, sl)))))} 492 493 def fm0b(-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_full(l, h, dm, Nil{}) == ffmap(h, dm, l) : List<&1, Array>}, b: L1RF) -> MRF<0n, T.Halves{l, r}, n, h, dm>: 494 match b: 495 case L1RF{r1, sr, fr}: 496 fm0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, map_appf(l1y, h, dm, r)) 497 498 def fm0a(-l: List<&1, T.FS>, r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, a: L1RF) -> MRF<0n, T.Halves{l, r}, n, h, dm>: 499 match a: 500 case L1RF{l1y, sl, fl}: 501 fm0b(l, r, n, h, dm, l1y, sl, fl, lf1(r, h, dm, Nil{})) 502 503 # depth 1 + e: each half cut in two and its treef (the closures run main at depth e), then the two maps appended 504 def fm1c(-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_full(e, hh1, TA.half(n), h, dm) == ffmap(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_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == ffmap(h, dm, T.hcat(T.FS, hh2)) : List<&1, Array>}, ma: MARF) -> MRF<1n+e, T.Halves{l, r}, n, h, dm>: 505 match ma: 506 case MARF{y1b, sb, fa}: 507 +ly1 = Equal.trans(List<&1, T.FS>, y1, T.hcat(T.FS, hh1), l, sy1, cat1) 508 +ly2 = Equal.trans(List<&1, T.FS>, y2, T.hcat(T.FS, hh2), r, sy2, cat2) 509 +q1 = Equal.trans(List<&1, Array>, T.fpar_full(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar_full(e, hh1, TA.half(n), h, dm), ffmap(h, dm, l), Equal.cong(T.Halves, List<&1, Array>, z => T.fpar_full(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_full(e, hh1, TA.half(n), h, dm), ffmap(h, dm, T.hcat(T.FS, hh1)), ffmap(h, dm, l), f1, Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(h, dm, z), T.hcat(T.FS, hh1), l, cat1))) 510 +q2 = Equal.trans(List<&1, Array>, T.fpar_full(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_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), ffmap(h, dm, r), Equal.cong(T.Halves, List<&1, Array>, z => T.fpar_full(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_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), ffmap(h, dm, T.hcat(T.FS, hh2)), ffmap(h, dm, r), f2, Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(h, dm, z), T.hcat(T.FS, hh2), r, cat2))) 511 +bb = Equal.trans(List<&1, Array>, ffmap(h, dm, List.append(&1, T.FS, l, r)), ffmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(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>, ffmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array, ffmap(h, dm, y1), ffmap(h, dm, y2)), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), fa, app2(Array, ffmap(h, dm, y1), ffmap(h, dm, l), ffmap(h, dm, y2), ffmap(h, dm, r), Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(h, dm, z), y2, r, ly2)))) 512 MRF{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), 513 Equal.trans(List<&1, Array>, List.append(&1, Array, T.fpar_full(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar_full(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, ffmap(h, dm, l), ffmap(h, dm, r)), ffmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array, T.fpar_full(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), ffmap(h, dm, l), T.fpar_full(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), ffmap(h, dm, r), q1, q2), Equal.sym(List<&1, Array>, ffmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array, ffmap(h, dm, l), ffmap(h, dm, r)), bb))} 514 515 def fm1b(-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: MRF, r2: MRF) -> MRF<1n+e, T.Halves{l, r}, n, h, dm>: 516 match r1 r2: 517 case MRF{y1, sy1, f1} MRF{y2, sy2, f2}: 518 fm1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, map_appf(y1, h, dm, y2)) 519 520 def fm1a(-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 -> MRF, k2: @g: T.Halves -> MRF) -> MRF<1n+e, T.Halves{l, r}, n, h, dm>: 521 match c1 c2: 522 case CGR{hh1, s1, cat1} CGR{hh2, s2, cat2}: 523 fm1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2)) 524 525 def treef(d: Nat, gs: T.Halves, +n: Nat, +h: Nat, +dm: T.Dm) -> MRF: 526 match d gs: 527 case 0n T.Halves{l, r}: 528 fm0a(l, r, n, h, dm, lf1(l, h, dm, Nil{})) 529 case 1n++e T.Halves{l, r}: 530 fm1a(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 => treef(e, g1, TA.half(n), h, dm), g2 => treef(e, g2, Nat.sub(n, TA.half(n)), h, dm)) 531 532 # the law: the treef gives what fleaf, the loop over the sequences one after another, gives 533 def par_fin_f(-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_full(d, gs, n, h, dm) == ffmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array>}, r: L1RF) -> {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array>}: 534 match r: 535 case L1RF{ys2, s2, fl}: 536 Equal.trans(List<&1, Array>, T.fpar_full(d, gs, n, h, dm), ffmap(h, dm, T.hcat(T.FS, gs)), T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), f, 537 Equal.sym(List<&1, Array>, T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), ffmap(h, dm, T.hcat(T.FS, gs)), 538 Equal.trans(List<&1, Array>, T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), T.fleaf_full(ys, h, dm, Nil{}), ffmap(h, dm, T.hcat(T.FS, gs)), Equal.cong(List<&1, T.FS>, List<&1, Array>, z => T.fleaf_full(z, h, dm, Nil{}), T.hcat(T.FS, gs), ys, Equal.sym(List<&1, T.FS>, ys, T.hcat(T.FS, gs), sy)), 539 Equal.trans(List<&1, Array>, T.fleaf_full(ys, h, dm, Nil{}), ffmap(h, dm, ys), ffmap(h, dm, T.hcat(T.FS, gs)), fl, Equal.cong(List<&1, T.FS>, List<&1, Array>, z => ffmap(h, dm, z), ys, T.hcat(T.FS, gs), sy))))) 540 541 def par_mid_f(-d: Nat, -gs: T.Halves, -n: Nat, +h: Nat, +dm: T.Dm, r: MRF) -> {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array>}: 542 match r: 543 case MRF{ys, sy, f}: 544 par_fin_f(d, gs, n, h, dm, ys, sy, f, lf1(ys, h, dm, Nil{})) 545 546 # PROOF (attn_par_fwd_full): attn_par_fwd's proof for the full-visible leaf; the depth induction, cut and append 547 # lemmas are the same, and cg (which is about cut and hcat, not about a leaf) is shared with it. 548 def Laws.attn_par_fwd_full(d, gs, n, h, dm): 549 par_mid_f(d, gs, n, h, dm, treef(d, gs, n, h, dm)) 550 551 # PROOF (attn_par_fwd): by induction on the depth, each fact handing its list back (the lists hold arrays, so each is 552 # used once): a leaf pair is fleaf twice, and fleaf is the map pushed onto its accumulator (l1); the map of two lists 553 # appended is the two maps appended (map_app); cut's halves, appended, are the list it cut (cg); a deeper tree is two 554 # trees on cut's halves (the closures). 555 def Laws.attn_par_fwd(d, gs, n, h, dm): 556 par_mid(d, gs, n, h, dm, tree(d, gs, n, h, dm)) 557 558 # ---- the sequential map the b_tree is compared with: f(x) = fs_o(fheads(h, 0, dm, x)) for each x, in order ---- 559 560 def b_fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.BG>) -> List<&1, T.DB>: 561 match xs: 562 case Nil{}: 563 Nil{} 564 case Con{x, t}: 565 T.db_of(T.bgroups(h, 0n, dm, x)) <> b_fmap(h, dm, t) 566 567 # ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ---- 568 569 type b_L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type: 570 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>}} 571 572 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>: 573 match r: 574 case b_L1R{ys, same, fact}: 575 b_L1R{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact} 576 577 def b_l1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1R: 578 match xs: 579 case Nil{}: 580 b_L1R{Nil{}, {==}, {==}} 581 case Con{x, t}: 582 b_l1_con(x, t, h, dm, acc, b_l1(t, h, dm, T.db_of(T.bgroups(h, 0n, dm, x)) <> acc)) 583 584 # ---- the map of two lists appended is the two maps appended ---- 585 586 type b_MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type: 587 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>}} 588 589 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>: 590 match r: 591 case b_MAR{ys, same, fact}: 592 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)} 593 594 def b_map_app(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MAR: 595 match a: 596 case Nil{}: 597 b_MAR{Nil{}, {==}, {==}} 598 case Con{x, t}: 599 b_ma_con(x, t, h, dm, b, b_map_app(t, h, dm, b)) 600 601 # ---- a reversed onto b, then c appended: a reversed onto b ++ c ---- 602 603 type b_GAR<-a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>> is Type: 604 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>}} 605 606 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>: 607 match r: 608 case b_GAR{ys, same, fact}: 609 b_GAR{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact} 610 611 def b_go_app(a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>) -> b_GAR: 612 match a: 613 case Nil{}: 614 b_GAR{Nil{}, {==}, {==}} 615 case Con{x, t}: 616 b_ga_con(x, t, b, c, b_go_app(t, x <> b, c)) 617 618 # ---- cut gives two halves that, appended, are acc reversed onto xs ---- 619 620 type b_CGR<-k: Nat, -xs: List<&1, T.BG>, -acc: List<&1, T.BG>> is Type: 621 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>}} 622 623 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: 624 match r: 625 case b_GAR{ys, +same, fact}: 626 b_CGR{T.Halves{List.reverse(&1, T.BG, ys), xs}, 627 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)), 628 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)} 629 630 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>: 631 match r: 632 case b_CGR{hh, same, cat}: 633 b_CGR{hh, same, cat} 634 635 def b_cg(k: Nat, xs: List<&1, T.BG>, acc: List<&1, T.BG>) -> b_CGR: 636 match k xs: 637 case 1n+m Con{x, t}: 638 b_cg_con(m, x, t, acc, b_cg(m, t, x <> acc)) 639 case 0n ys: 640 b_cg_base(0n, ys, acc, {==}, b_go_app(acc, Nil{}, ys)) 641 case 1n+m Nil{}: 642 b_cg_base(1n+m, Nil{}, acc, {==}, b_go_app(acc, Nil{}, Nil{})) 643 644 # ---- the b_tree: fpar at depth d on two halves is the map of the halves appended ---- 645 646 type b_MR<-d: Nat, -gs: T.Halves, -n: Nat, -h: Nat, -dm: T.Dm> is Type: 647 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>}} 648 649 # depth 0: the two leaves' loops, appended 650 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>: 651 match c: 652 case b_MAR{l2, s2, fa}: 653 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), 654 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), 655 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)), 656 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)), 657 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)))))} 658 659 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>: 660 match b: 661 case b_L1R{r1, sr, fr}: 662 b_m0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, b_map_app(l1y, h, dm, r)) 663 664 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>: 665 match a: 666 case b_L1R{l1y, sl, fl}: 667 b_m0b(l, r, n, h, dm, l1y, sl, fl, b_l1(r, h, dm, Nil{})) 668 669 # depth 1 + e: each half cut in two and its b_tree (the closures run main at depth e), then the two maps appended 670 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>: 671 match ma: 672 case b_MAR{y1b, sb, fa}: 673 +ly1 = Equal.trans(List<&1, T.BG>, y1, T.hcat(T.BG, hh1), l, sy1, cat1) 674 +ly2 = Equal.trans(List<&1, T.BG>, y2, T.hcat(T.BG, hh2), r, sy2, cat2) 675 +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))) 676 +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))) 677 +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)))) 678 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), 679 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))} 680 681 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>: 682 match r1 r2: 683 case b_MR{y1, sy1, f1} b_MR{y2, sy2, f2}: 684 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)) 685 686 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>: 687 match c1 c2: 688 case b_CGR{hh1, s1, cat1} b_CGR{hh2, s2, cat2}: 689 b_m1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2)) 690 691 def b_tree(d: Nat, gs: T.Halves, +n: Nat, +h: Nat, +dm: T.Dm) -> b_MR: 692 match d gs: 693 case 0n T.Halves{l, r}: 694 b_m0a(l, r, n, h, dm, b_l1(l, h, dm, Nil{})) 695 case 1n++e T.Halves{l, r}: 696 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)) 697 698 # the law: the b_tree gives what fleaf, the loop over the sequences one after another, gives 699 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>}: 700 match r: 701 case b_L1R{ys2, s2, fl}: 702 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, 703 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)), 704 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)), 705 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))))) 706 707 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>}: 708 match r: 709 case b_MR{ys, sy, f}: 710 b_par_fin(d, gs, n, h, dm, ys, sy, f, b_l1(ys, h, dm, Nil{})) 711 712 def b_ffmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.BG>) -> List<&1, T.DB>: 713 match xs: 714 case Nil{}: 715 Nil{} 716 case Con{x, t}: 717 T.db_of(T.bgroups_full(h, 0n, dm, x)) <> b_ffmap(h, dm, t) 718 719 # ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ---- 720 721 type b_L1RF<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type: 722 b_L1RF{ys: List<&1, T.BG>, same: {ys == xs : List<&1, T.BG>}, fact: {T.bleaf_full(xs, h, dm, acc) == List.reverse.go(&1, T.DB, acc, b_ffmap(h, dm, xs)) : List<&1, T.DB>}} 723 724 def b_lf_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>, r: b_L1RF acc>) -> b_L1RF t, acc>: 725 match r: 726 case b_L1RF{ys, same, fact}: 727 b_L1RF{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact} 728 729 def b_lf1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1RF: 730 match xs: 731 case Nil{}: 732 b_L1RF{Nil{}, {==}, {==}} 733 case Con{x, t}: 734 b_lf_con(x, t, h, dm, acc, b_lf1(t, h, dm, T.db_of(T.bgroups_full(h, 0n, dm, x)) <> acc)) 735 736 # ---- the map of two lists appended is the two maps appended ---- 737 738 type b_MARF<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type: 739 b_MARF{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {b_ffmap(h, dm, List.append(&1, T.BG, a, b)) == List.append(&1, T.DB, b_ffmap(h, dm, a), b_ffmap(h, dm, b)) : List<&1, T.DB>}} 740 741 def b_ma_conf(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>, r: b_MARF) -> b_MARF t, b>: 742 match r: 743 case b_MARF{ys, same, fact}: 744 b_MARF{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_full(h, 0n, dm, x)) <> z, b_ffmap(h, dm, List.append(&1, T.BG, t, b)), List.append(&1, T.DB, b_ffmap(h, dm, t), b_ffmap(h, dm, b)), fact)} 745 746 def b_map_appf(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MARF: 747 match a: 748 case Nil{}: 749 b_MARF{Nil{}, {==}, {==}} 750 case Con{x, t}: 751 b_ma_conf(x, t, h, dm, b, b_map_appf(t, h, dm, b)) 752 753 # ---- a reversed onto b, then c appended: a reversed onto b ++ c ---- 754 755 type b_MRF<-d: Nat, -gs: T.Halves, -n: Nat, -h: Nat, -dm: T.Dm> is Type: 756 b_MRF{ys: List<&1, T.BG>, same: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, fact: {T.bpar_full(d, gs, n, h, dm) == b_ffmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}} 757 758 # depth 0: the two leaves' loops, appended 759 def b_fm0c(-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_full(l, h, dm, Nil{}) == b_ffmap(h, dm, l) : List<&1, T.DB>}, r1: List<&1, T.BG>, sr: {r1 == r : List<&1, T.BG>}, fr: {T.bleaf_full(r, h, dm, Nil{}) == b_ffmap(h, dm, r) : List<&1, T.DB>}, c: b_MARF) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>: 760 match c: 761 case b_MARF{l2, s2, fa}: 762 b_MRF{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), 763 Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bleaf_full(l, h, dm, Nil{}), T.bleaf_full(r, h, dm, Nil{})), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), b_ffmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bleaf_full(l, h, dm, Nil{}), b_ffmap(h, dm, l), T.bleaf_full(r, h, dm, Nil{}), b_ffmap(h, dm, r), fl, fr), 764 Equal.sym(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), 765 Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), b_ffmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, List.append(&1, T.BG, z, r)), l, l1y, Equal.sym(List<&1, T.BG>, l1y, l, sl)), 766 Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_ffmap(h, dm, l1y), b_ffmap(h, dm, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), fa, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => List.append(&1, T.DB, b_ffmap(h, dm, z), b_ffmap(h, dm, r)), l1y, l, sl)))))} 767 768 def b_fm0b(-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_full(l, h, dm, Nil{}) == b_ffmap(h, dm, l) : List<&1, T.DB>}, b: b_L1RF) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>: 769 match b: 770 case b_L1RF{r1, sr, fr}: 771 b_fm0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, b_map_appf(l1y, h, dm, r)) 772 773 def b_fm0a(-l: List<&1, T.BG>, r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, a: b_L1RF) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>: 774 match a: 775 case b_L1RF{l1y, sl, fl}: 776 b_fm0b(l, r, n, h, dm, l1y, sl, fl, b_lf1(r, h, dm, Nil{})) 777 778 # depth 1 + e: each half cut in two and its b_treef (the closures run main at depth e), then the two maps appended 779 def b_fm1c(-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_full(e, hh1, TA.half(n), h, dm) == b_ffmap(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_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == b_ffmap(h, dm, T.hcat(T.BG, hh2)) : List<&1, T.DB>}, ma: b_MARF) -> b_MRF<1n+e, T.Halves{l, r}, n, h, dm>: 780 match ma: 781 case b_MARF{y1b, sb, fa}: 782 +ly1 = Equal.trans(List<&1, T.BG>, y1, T.hcat(T.BG, hh1), l, sy1, cat1) 783 +ly2 = Equal.trans(List<&1, T.BG>, y2, T.hcat(T.BG, hh2), r, sy2, cat2) 784 +q1 = Equal.trans(List<&1, T.DB>, T.bpar_full(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar_full(e, hh1, TA.half(n), h, dm), b_ffmap(h, dm, l), Equal.cong(T.Halves, List<&1, T.DB>, z => T.bpar_full(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_full(e, hh1, TA.half(n), h, dm), b_ffmap(h, dm, T.hcat(T.BG, hh1)), b_ffmap(h, dm, l), f1, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), T.hcat(T.BG, hh1), l, cat1))) 785 +q2 = Equal.trans(List<&1, T.DB>, T.bpar_full(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_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_ffmap(h, dm, r), Equal.cong(T.Halves, List<&1, T.DB>, z => T.bpar_full(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_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_ffmap(h, dm, T.hcat(T.BG, hh2)), b_ffmap(h, dm, r), f2, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), T.hcat(T.BG, hh2), r, cat2))) 786 +bb = Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), b_ffmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(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_ffmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_ffmap(h, dm, y1), b_ffmap(h, dm, y2)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), fa, app2(T.DB, b_ffmap(h, dm, y1), b_ffmap(h, dm, l), b_ffmap(h, dm, y2), b_ffmap(h, dm, r), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), y2, r, ly2)))) 787 b_MRF{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), 788 Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bpar_full(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar_full(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_ffmap(h, dm, l), b_ffmap(h, dm, r)), b_ffmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bpar_full(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), b_ffmap(h, dm, l), T.bpar_full(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), b_ffmap(h, dm, r), q1, q2), Equal.sym(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), bb))} 789 790 def b_fm1b(-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_MRF, r2: b_MRF) -> b_MRF<1n+e, T.Halves{l, r}, n, h, dm>: 791 match r1 r2: 792 case b_MRF{y1, sy1, f1} b_MRF{y2, sy2, f2}: 793 b_fm1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, b_map_appf(y1, h, dm, y2)) 794 795 def b_fm1a(-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_MRF, k2: @g: T.Halves -> b_MRF) -> b_MRF<1n+e, T.Halves{l, r}, n, h, dm>: 796 match c1 c2: 797 case b_CGR{hh1, s1, cat1} b_CGR{hh2, s2, cat2}: 798 b_fm1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2)) 799 800 def b_treef(d: Nat, gs: T.Halves, +n: Nat, +h: Nat, +dm: T.Dm) -> b_MRF: 801 match d gs: 802 case 0n T.Halves{l, r}: 803 b_fm0a(l, r, n, h, dm, b_lf1(l, h, dm, Nil{})) 804 case 1n++e T.Halves{l, r}: 805 b_fm1a(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_treef(e, g1, TA.half(n), h, dm), g2 => b_treef(e, g2, Nat.sub(n, TA.half(n)), h, dm)) 806 807 # the law: the b_treef gives what fleaf, the loop over the sequences one after another, gives 808 def b_par_fin_f(-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_full(d, gs, n, h, dm) == b_ffmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}, r: b_L1RF) -> {T.bpar_full(d, gs, n, h, dm) == T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}: 809 match r: 810 case b_L1RF{ys2, s2, fl}: 811 Equal.trans(List<&1, T.DB>, T.bpar_full(d, gs, n, h, dm), b_ffmap(h, dm, T.hcat(T.BG, gs)), T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}), f, 812 Equal.sym(List<&1, T.DB>, T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}), b_ffmap(h, dm, T.hcat(T.BG, gs)), 813 Equal.trans(List<&1, T.DB>, T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}), T.bleaf_full(ys, h, dm, Nil{}), b_ffmap(h, dm, T.hcat(T.BG, gs)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => T.bleaf_full(z, h, dm, Nil{}), T.hcat(T.BG, gs), ys, Equal.sym(List<&1, T.BG>, ys, T.hcat(T.BG, gs), sy)), 814 Equal.trans(List<&1, T.DB>, T.bleaf_full(ys, h, dm, Nil{}), b_ffmap(h, dm, ys), b_ffmap(h, dm, T.hcat(T.BG, gs)), fl, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), ys, T.hcat(T.BG, gs), sy))))) 815 816 def b_par_mid_f(-d: Nat, -gs: T.Halves, -n: Nat, +h: Nat, +dm: T.Dm, r: b_MRF) -> {T.bpar_full(d, gs, n, h, dm) == T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}: 817 match r: 818 case b_MRF{ys, sy, f}: 819 b_par_fin_f(d, gs, n, h, dm, ys, sy, f, b_lf1(ys, h, dm, Nil{})) 820 821 # PROOF (attn_par_bwd_full): attn_par_bwd's proof for the full-visible leaf; b_cg (cut and hcat, no leaf) is shared. 822 def Laws.attn_par_bwd_full(d, gs, n, h, dm): 823 b_par_mid_f(d, gs, n, h, dm, b_treef(d, gs, n, h, dm)) 824 825 # PROOF (attn_par_bwd): attn_par_fwd's proof, for BG and bleaf. 826 def Laws.attn_par_bwd(d, gs, n, h, dm): 827 b_par_mid(d, gs, n, h, dm, b_tree(d, gs, n, h, dm)) 828 829 # ===================================================================================================== 830 # Grouped-query heads (llama.bend's proof) 831 # ===================================================================================================== 832 833 # one block of 1 + m numbers adds 1 to the quotient (Nat.divmod.go counts down the remainder from m) 834 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}: 835 match m: 836 case 0n: 837 {==} 838 case 1n+p: 839 %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} 840 div_block(p, n, d, 1n+r) 841 842 # j whole blocks of 1 + s numbers add j to the quotient 843 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}: 844 match j: 845 case 0n: 846 {==} 847 case 1n+jp: 848 %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} 849 %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} 850 %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} 851 %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} 852 div_blocks(jp, s, n, 1n+d) 853 854 # fewer than 1 + s numbers after the last whole block leave the quotient alone 855 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}: 856 match i: 857 case 0n: 858 {==} 859 case 1n+p: 860 div_rest(p, k, d, 1n+r) 861 862 # PROOF (gqa_head): Nat.div counts how many whole blocks of g numbers fit. j·g is j whole blocks (div_blocks), and 863 # i < g numbers after them do not complete another one (div_rest). 864 def Laws.gqa_head(j, i, k): 865 %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} 866 %NL.add_zero(j) : {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), Nat.add(j, 0n), 0n)) == _ : Nat} 867 div_rest(i, k, Nat.add(j, 0n), 0n) 868 869 # PROOF (kv_of_group): kv_of is Nat.div, so this is gqa_head. 870 def Laws.kv_of_group(j, i, k): 871 Laws.gqa_head(j, i, k) 872 873 # 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). 874 def Laws.kv_cols(t, hd, w, kvw, sc, j, i, k): 875 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)) 876 877 # ===================================================================================================== 878 # Tensors: shapes 879 # ===================================================================================================== 880 881 # a || b == b || a, and a && b == b && a: every case computes 882 def or_comm(+a: Bool, +b: Bool) -> {Bool.or(a, b) == Bool.or(b, a) : Bool}: 883 match a b: 884 case True{} True{}: 885 {==} 886 case True{} False{}: 887 {==} 888 case False{} True{}: 889 {==} 890 case False{} False{}: 891 {==} 892 893 def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}: 894 match a b: 895 case True{} True{}: 896 {==} 897 case True{} False{}: 898 {==} 899 case False{} True{}: 900 {==} 901 case False{} False{}: 902 {==} 903 904 # equal operands give equal conjunctions and disjunctions 905 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}: 906 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)) 907 908 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}: 909 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)) 910 911 # 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 || 912 def bc_dim_sym(+x: Nat, +y: Nat, +z: Nat) -> {TT.bc_dim(x, y, z) == TT.bc_dim(y, x, z) : Bool}: 913 or_comm(TT.bc_pair(x, y, z), TT.bc_pair(y, x, z)) 914 915 # axis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False 916 # either way round 917 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}: 918 match a b o: 919 case Nil{} Nil{} Nil{}: 920 {==} 921 case Nil{} Nil{} Con{z, ro}: 922 {==} 923 case Nil{} Con{y, rb} Nil{}: 924 {==} 925 case Nil{} Con{y, rb} Con{z, ro}: 926 {==} 927 case Con{x, ra} Nil{} Nil{}: 928 {==} 929 case Con{x, ra} Nil{} Con{z, ro}: 930 {==} 931 case Con{x, ra} Con{y, rb} Nil{}: 932 {==} 933 case Con{+x, +ra} Con{+y, +rb} Con{+z, +ro}: 934 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)) 935 936 # the ranks: the same two comparisons and the same two equalities, in the other order 937 def bc_rank_sym(+la: Nat, +lb: Nat, +lo: Nat) -> {TT.bc_rank(la, lb, lo) == TT.bc_rank(lb, la, lo) : Bool}: 938 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)), 939 and_comm(Nat.is_le(la, lo), Nat.is_le(lb, lo)), or_comm(Nat.is_eq(la, lo), Nat.is_eq(lb, lo))) 940 941 def Laws.bc_sym(a, b, o): 942 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)), 943 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), 944 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)) 945 946 # h * (a * r) == a * (h * r): associativity, then commutativity of the first two factors, then associativity back 947 def mul_swap(+h: Nat, +a: Nat, +r: Nat) -> {Nat.mul(h, Nat.mul(a, r)) == Nat.mul(a, Nat.mul(h, r)) : Nat}: 948 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), 949 Equal.trans(Nat, Nat.mul(Nat.mul(h, a), r), Nat.mul(Nat.mul(a, h), r), Nat.mul(a, Nat.mul(h, r)), 950 Equal.cong(Nat, Nat, x => Nat.mul(x, r), Nat.mul(h, a), Nat.mul(a, h), NL.mul_comm(h, a)), 951 Equal.sym(Nat, Nat.mul(a, Nat.mul(h, r)), Nat.mul(Nat.mul(a, h), r), NL.mul_assoc(a, h, r)))) 952 953 # by induction on the shape and the axis: axis 0 computes; past it, the first size h stays in front on both sides, and 954 # mul_swap moves it past size(k) 955 def Laws.sum_numel(s, k): 956 match s k: 957 case Nil{} _: 958 {==} 959 case Con{h, t} 0n: 960 {==} 961 case Con{+h, +t} 1n+p: 962 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)))), 963 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)), 964 mul_swap(h, TT.at1(t, p), NL.product(TT.remove(t, p)))) 965 966 # ===================================================================================================== 967 # Tensors: narrow, cat, of_mat, permute 968 # ===================================================================================================== 969 970 # by induction: axis 0 is replaced and then taken out; past it, the first size stays in front on both sides 971 def Laws.narrow_rest(s, d, l): 972 match s d: 973 case Nil{} _: 974 {==} 975 case Con{h, t} 0n: 976 {==} 977 case Con{+h, +t} 1n+p: 978 # bend-lint: disable-next bend-lint-rules/performance/unused_result -- the binder of Equal.cong's motive, used in its body not-expected-because: a law, never run 979 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)) 980 981 # a shape with no axis d contradicts the premise (d < rank is False); axis 0 is l; past it, the induction 982 def Laws.narrow_axis(s, d, l, e): 983 match s d: 984 case Nil{} 0n: 985 Empty.absurd({TT.at1(TT.setd([], 0n, l), 0n) == l : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e))) 986 case Nil{} 1n+p: 987 Empty.absurd({TT.at1(TT.setd([], 1n+p, l), 1n+p) == l : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e))) 988 case Con{h, t} 0n: 989 {==} 990 case Con{h, +t} 1n+p: 991 Laws.narrow_axis(t, p, l, e) 992 993 # axis 0: (x + y)·n == x·n + y·n (distributivity); past it, the induction and k·(a + b) == k·a + k·b 994 def Laws.cat_numel(s, d, x, y, e): 995 match s d: 996 case Nil{} 0n: 997 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))) 998 case Nil{} 1n+p: 999 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))) 1000 case Con{h, +t} 0n: 1001 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))) 1002 case Con{+h, +t} 1n+p: 1003 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)))), 1004 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)), 1005 NL.mul_dist_l(h, NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y)))) 1006 1007 # r·(c·1) == r·c: c·1 == c 1008 def Laws.mat_numel(r, c): 1009 Equal.cong(Nat, Nat, v => Nat.mul(r, v), Nat.mul(c, 1n), c, NL.mul_one_r(c)) 1010 1011 # one axis of the result per entry of p 1012 def Laws.permute_rank(s, p): 1013 match p: 1014 case Nil{}: 1015 {==} 1016 case Con{k, r}: 1017 Equal.cong(Nat, Nat, v => 1n+v, TT.rank(TT.permuted(s, r)), List.length(&2, Nat, r), Laws.permute_rank(s, r)) 1018 1019 # ===================================================================================================== 1020 # The order of a row's additions (block_sum) 1021 # ===================================================================================================== 1022 1023 # 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 1024 # halves bal puts under one node. Induction on k; add_succ turns k + (k + 1) into 2 + (k + k), and add_assoc moves the 1025 # next pair's start from (lo + 2^p) + 2^p to lo + 2^(p+1) 1026 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>}: 1027 match k: 1028 case 0n: 1029 {==} 1030 case 1n+j: 1031 +a = Spec.pw(p) 1032 +nx = Nat.add(Nat.add(lo, a), a) 1033 %NL.add_succ(j, j) : {Spec.spass(Spec.blocks(p, 1n+_, lo)) == Spec.blocks(1n+p, 1n+j, lo) : List<&2, Spec.Sum>} 1034 %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>} 1035 %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>} 1036 {==} 1037 1038 # 2^(p+1) · k cells are 2^p · 2k: (a + a)·k == a·k + a·k == a·(k + k) 1039 def cnt2(+p: Nat, +k: Nat) -> {Nat.mul(Spec.pw(1n+p), k) == Nat.mul(Spec.pw(p), Nat.add(k, k)) : Nat}: 1040 +a = Spec.pw(p) 1041 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)), 1042 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)), 1043 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))) 1044 1045 # 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 1046 # 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) 1047 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>}: 1048 match p: 1049 case 0n: 1050 %NL.mul_one_l(k) : {Spec.blocks(0n, Nat.mul(1n, k), lo) == Spec.blocks(0n, _, lo) : List<&2, Spec.Sum>} 1051 {==} 1052 case 1n+q: 1053 +kk = Nat.add(k, k) 1054 %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>} 1055 %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>} 1056 pass_pair(q, k, lo) 1057 1058 # r + p passes are p passes, then r more 1059 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>}: 1060 match r: 1061 case 0n: 1062 {==} 1063 case 1n+q: 1064 # bend-lint: disable-next bend-lint-rules/performance/unused_result -- the binder of Equal.cong's motive, used in its body not-expected-because: a law, never run 1065 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)) 1066 1067 # block_sum: r + p passes over the row are r passes over what its first p passes leave (passes_add), which is its k 1068 # blocks summed as bal sums them (blocks_passes) 1069 def Laws.block_sum(p, k, r): 1070 +row = Spec.blocks(0n, Nat.mul(Spec.pw(p), k), 0n) 1071 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)), 1072 passes_add(r, p, row), 1073 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))) 1074 1075 def main() -> Unit: 1076 Unit{}