def unpack_pack

bendtorch-core@0.1.0.0 · src/shape/index_proofs.bend:84

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

84def unpack_pack(+a: Nat, +b: Nat, +first: Shape.Fin(a), +last: Shape.Fin(b)) -> {Shape.Fin.unpack(a, b, Shape.Fin.pack(a, b, (first, last))) == (first, last) : Shape.Fin(a) & Shape.Fin(b)}:
85  match a:
86    case 0n:
87      match first:
88    case 1n+p:
89      match first:
90        case Shape.FZero{}:
91          %split_left(b, Nat.mul(p, b), last) : {Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), Shape.Fin.split(b, Nat.mul(p, b), Shape.Fin.left(b, Nat.mul(p, b), last))) == Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), _) : Shape.Fin(1n+p) & Shape.Fin(b)}
92          {==}
93        case Shape.FNext{+previous}:
94          %unpack_pack(p, b, previous, last) : {Shape.Fin.unpack(1n+p, b, Shape.Fin.pack(1n+p, b, (Shape.FNext{previous}, last))) == Shape.Fin.unpack.lift(p, b, _) : Shape.Fin(1n+p) & Shape.Fin(b)}
95          %split_shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last))) : {Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), Shape.Fin.split(b, Nat.mul(p, b), Shape.Fin.shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last))))) == Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), _) : Shape.Fin(1n+p) & Shape.Fin(b)}
96          {==}