def walk_left_row

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex

377def walk_left_row(+lh: Nat, +rh: Nat, +oh: Nat, axis: Shape.Axis<lh, rh, oh>, +size: Nat, +d: Nat, +w: Nat,
378  d_below: {Nat.is_lt(d, oh) == True{} : Bool}, w_below: {Nat.is_lt(w, size) == True{} : Bool}) ->
379  {Nat.is_lt(Nat.add(Nat.mul(Shape.broadcast_index(lh, size), d), w), Nat.mul(lh, size)) == True{} : Bool}:
380  match lh:
381    case 0n:
382      Empty.absurd({Nat.is_lt(Nat.add(Nat.mul(size, d), w), 0n) == True{} : Bool},
383        Arith.lt_zero(d,
384          %axis_zero(rh, oh, axis) : {Nat.is_lt(d, _) == True{} : Bool}
385          d_below))
386    case 1n+k:
387      match k:
388        case 0n:
389          %Equal.sym(Nat, Nat.add(size, 0n), size, Broadcast.add_zero(size)) : {Nat.is_lt(w, _) == True{} : Bool}
390          w_below
391        case 1n+j:
392          %Nats.mul_comm(d, size) : {Nat.is_lt(Nat.add(_, w), Nat.mul(2n+j, size)) == True{} : Bool}
393          MatrixIndex.lt_mul_add(d, 2n+j, w, size,
394            %axis_kept(j, rh, oh, axis) : {Nat.is_lt(d, _) == True{} : Bool}
395            d_below,
396            w_below)