def left_padding_equal

bendtorch-core@0.1.0.0 · src/shape/unique_proofs.bend:62

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

62def left_padding_equal(+lp1: Nat, +rp1: Nat, +lp2: Nat, +rp2: Nat, +left_rank: Nat, +right_rank: Nat, +m1: Shape.PadMinimal<lp1, rp1>, +m2: Shape.PadMinimal<lp2, rp2>, +first: {Nat.add(lp1, left_rank) == Nat.add(rp1, right_rank) : Nat}, +second: {Nat.add(lp2, left_rank) == Nat.add(rp2, right_rank) : Nat}) -> {lp1 == lp2 : Nat}:
63  match m1 m2:
64    case Shape.PLeftZero{z1} Shape.PLeftZero{z2}:
65      Equal.trans(Nat, lp1, 0n, lp2, Equal.sym(Nat, 0n, lp1, z1), z2)
66    case Shape.PRightZero{z1} Shape.PRightZero{z2}:
67      cancel_right(lp1, lp2, left_rank, Equal.trans(Nat, Nat.add(lp1, left_rank), right_rank, Nat.add(lp2, left_rank), unpadded(lp1, rp1, left_rank, right_rank, z1, first), Equal.sym(Nat, Nat.add(lp2, left_rank), right_rank, unpadded(lp2, rp2, left_rank, right_rank, z2, second))))
68    case Shape.PLeftZero{z1} Shape.PRightZero{z2}:
69      crossed(lp1, rp1, lp2, rp2, left_rank, right_rank, z1, z2, first, second)
70    case Shape.PRightZero{z1} Shape.PLeftZero{z2}:
71      Equal.sym(Nat, lp2, lp1, crossed(lp2, rp2, lp1, rp1, left_rank, right_rank, z2, z1, second, first))