ReduceFiberProof.fiber_walk: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 846-870 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=846&end_line=870

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

# The fiber-walk lemma: for the index rows of an aligned broadcast and a
# cell below the left count, the offsets the walk reads, in order, are the
# masked positions.
def fiber_walk(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +aligned: Shape.Aligned(left, right, output),
  +target: Nat, +below: {Nat.is_lt(target, Shape.numel(left)) == True{} : Bool}) -> RowsWalk(left, right, output, target):
  match left right output:
    case Nil{} Nil{} Nil{}:
      %Arith.lt_one(target, below) : {kept(Nat.is_eq(0n, _), 0n, Nil{}) == [0n] : List<&2, Nat>}
      {==}
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      Shape.AStep{+axis, +tail} = aligned
      fiber_cons(lh, lt, rh, rt, oh, ot, axis, tail, target, below,
        inner => inside => fiber_walk(lt, rt, ot, tail, inner, inside))
    case Nil{} Nil{} +oh <> +ot:
      Empty.absurd(RowsWalk(Nil{}, Nil{}, oh <> ot, target), aligned)
    case Nil{} +rh <> +rt Nil{}:
      Empty.absurd(RowsWalk(Nil{}, rh <> rt, Nil{}, target), aligned)
    case +lh <> +lt Nil{} Nil{}:
      Empty.absurd(RowsWalk(lh <> lt, Nil{}, Nil{}, target), aligned)
    case Nil{} +rh <> +rt +oh <> +ot:
      Empty.absurd(RowsWalk(Nil{}, rh <> rt, oh <> ot, target), aligned)
    case +lh <> +lt Nil{} +oh <> +ot:
      Empty.absurd(RowsWalk(lh <> lt, Nil{}, oh <> ot, target), aligned)
    case +lh <> +lt +rh <> +rt Nil{}:
      Empty.absurd(RowsWalk(lh <> lt, rh <> rt, Nil{}, target), aligned)

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=RowsWalk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=fiber_cons
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_one