def join_len

bend-ml-tensor-array@0.1.19.0 · main.bend:1865

import Base

1865# joining two halves of h1 and h2 numbers gives h1 + h2 numbers. (The statement for the whole tree,
1866# "Bands.matvec_l gives r numbers", would apply this to the results of the two recursive calls and
1867# to the induction hypotheses about the same calls; that uses each band's Array twice, which Bend's
1868# affine rules refuse. It stays open, covered by tests: NOTES.md, v3.1.)
1869def join_len(-r: Nat, -c: Nat, -h1: Nat, -h2: Nat, p: BL<half(r), c>, q: BL<Nat.sub(r, half(r)), c>, hp: {bl_len(half(r), c, p) == h1 : Nat}, hq: {bl_len(Nat.sub(r, half(r)), c, q) == h2 : Nat}) -> {bl_len(r, c, bv_join(r, c, p, q)) == Nat.add(h1, h2) : Nat}:
1870  match p q:
1871    case BL{bx, +yx} BL{by, +yy}:
1872      %hp : {List.length(&2, F32, List.append(&2, F32, yx, yy)) == Nat.add(_, h2) : Nat}
1873      %hq : {List.length(&2, F32, List.append(&2, F32, yx, yy)) == Nat.add(List.length(&2, F32, yx), _) : Nat}
1874      app_len(yx, yy)