def left_certificate

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:216

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend as Laws

216def left_certificate(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
217  +row: U32, +column: U32, +cursor: Nat, +accumulator: F32,
218  -rec: @a: Core.Tensor<left> -> @b: Core.Tensor<right> -> @+value: F32 ->
219    Laws.SourceDot<fuel, left, right, a, b, row, column, 1n+cursor, value, Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value)>,
220  -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
221  certificate: CoordinateRead<left, a, [row, U32.from_nat(cursor)]>) ->
222  Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
223    a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator,
224    Core.read_coordinate(left, a, [row, U32.from_nat(cursor)]))>:
225  CoordinateRead{ra, +result, +exact, meaning, left_kept} = certificate
226  Laws.SourceDot{unit =>
227    claim : @certificate: Laws.SourceDot<1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
228      a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, (ra, result))> ->
229      Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
230        a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, (ra, result))) =
231      \{Laws.SourceDot: proof => proof(Unit{})}
232    %exact : Laws.DotResultMeaning(1n+fuel, left, right, a, b, row, column, cursor, accumulator, Matrix.left_read(left, right,
233      a => b => value => Matrix.natural_dot(fuel, left, right, a, b, row, column, 1n+cursor, value), b, [U32.from_nat(cursor), column], accumulator, _))
234    claim(left_pair(fuel, left, right, a, b, ra, result, row, column, cursor, accumulator, rec, exact_cursor, meaning, left_kept))}