def masked_base

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:591

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

591def masked_base(+n: Nat, +rows: List<&2, Shape.Row>, +target: Nat, +base: Nat, +cursor: Nat) ->
592  {masked(n, rows, target, base, cursor) == shift(base, masked(n, rows, target, 0n, cursor)) : List<&2, Nat>}:
593  match n:
594    case 0n:
595      {==}
596    case 1n+m:
597      +keep = Nat.is_eq(Shape.walk_left(rows, cursor), target)
598      +x = Shape.walk_right(rows, cursor)
599      Equal.trans(List<&2, Nat>, kept(keep, Nat.add(base, x), masked(m, rows, target, base, 1n+cursor)),
600        kept(keep, Nat.add(base, x), shift(base, masked(m, rows, target, 0n, 1n+cursor))),
601        shift(base, kept(keep, x, masked(m, rows, target, 0n, 1n+cursor))),
602        Equal.cong(List<&2, Nat>, List<&2, Nat>, tail => kept(keep, Nat.add(base, x), tail),
603          masked(m, rows, target, base, 1n+cursor), shift(base, masked(m, rows, target, 0n, 1n+cursor)), masked_base(m, rows, target, base, 1n+cursor)),
604        kept_shift(keep, base, x, masked(m, rows, target, 0n, 1n+cursor)))