def transposed_index_exact

bendtorch-core@0.1.0.0 · src/tensor/transpose_PROOF.bend:237

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

237# j * rows + l < rows * columns, so the output index is its own word.
238def transposed_index_exact(+input: Shape.Shape, +rows: U32, +columns: U32,
239  +matrix: {Shape.dimensions(input) == [rows, columns] : List<&2, U32>}, +j: Nat,
240  +j_below: {Nat.is_lt(j, U32.to_nat(columns)) == True{} : Bool}, +l: Nat,
241  +l_below: {Nat.is_lt(l, U32.to_nat(rows)) == True{} : Bool}) ->
242  {U32.to_nat(U32.from_nat(Nat.add(Nat.mul(j, U32.to_nat(rows)), l))) == Nat.add(Nat.mul(j, U32.to_nat(rows)), l) : Nat}:
243  +r = U32.to_nat(rows)
244  +c = U32.to_nat(columns)
245  MatrixIndex.word_exact(Nat.add(Nat.mul(j, r), l), input,
246    %Equal.sym(List<&2, U32>, Shape.dimensions(input), [rows, columns], matrix) :
247      {Nat.is_lt(Nat.add(Nat.mul(j, r), l), Shape.logical_numel(_)) == True{} : Bool}
248    %Equal.sym(Nat, Nat.mul(c, 1n), c, Nats.mul_one_right(c)) :
249      {Nat.is_lt(Nat.add(Nat.mul(j, r), l), Nat.mul(r, _)) == True{} : Bool}
250    %Nats.mul_comm(c, r) :
251      {Nat.is_lt(Nat.add(Nat.mul(j, r), l), _) == True{} : Bool}
252    MatrixIndex.lt_mul_add(j, c, l, r, j_below, l_below))