def logical_dot_original

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

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_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold

100def logical_dot_original(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
101  -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, +row: U32, +column: U32, +cursor: Nat, values: List<&2, DotFold.Factors>,
102  logical: Laws.LogicalDot(fuel, left, right, ra, rb, row, column, cursor, values),
103  -left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
104  -right_kept: @+other: U32 -> {Core.checked_observe(right, rb, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>}) ->
105  Laws.LogicalDot(fuel, left, right, a, b, row, column, cursor, values):
106  match fuel values:
107    case 0n Nil{}:
108      Unit{}
109    case 1n+tail DotFold.Factors{+lv, +rv} <> rest:
110      Laws.DotStep{exact, lo, ro, remaining} = logical
111      Laws.DotStep{exact,
112        Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]),
113          Laws.coordinate_observe(left, ra, [row, U32.from_nat(cursor)]), Some{lv},
114          Equal.sym(Maybe<&2, F32>, Laws.coordinate_observe(left, ra, [row, U32.from_nat(cursor)]),
115            Laws.coordinate_observe(left, a, [row, U32.from_nat(cursor)]), coordinate_keeps(left, a, ra, [row, U32.from_nat(cursor)], left_kept)), lo),
116        Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]),
117          Laws.coordinate_observe(right, rb, [U32.from_nat(cursor), column]), Some{rv},
118          Equal.sym(Maybe<&2, F32>, Laws.coordinate_observe(right, rb, [U32.from_nat(cursor), column]),
119            Laws.coordinate_observe(right, b, [U32.from_nat(cursor), column]), coordinate_keeps(right, b, rb, [U32.from_nat(cursor), column], right_kept)), ro),
120        logical_dot_original(tail, left, right, a, b, ra, rb, row, column, 1n+cursor, rest, remaining, left_kept, right_kept)}
121    case 0n DotFold.Factors{lv, rv} <> rest:
122      Empty.absurd(Laws.LogicalDot(0n, left, right, a, b, row, column, cursor, DotFold.Factors{lv, rv} <> rest), logical)
123    case 1n+tail Nil{}:
124      Empty.absurd(Laws.LogicalDot(1n+tail, left, right, a, b, row, column, cursor, Nil{}), logical)