def logical_keeps

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:49

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/reduction_LAWS.bend as Laws

49def logical_keeps(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
50  values: List<&2, F32>, logical: Laws.LogicalValues(fuel, shape, original, cursor, values),
51  -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
52  Laws.LogicalValues(fuel, shape, tensor, cursor, values):
53  match fuel values:
54    case 0n Nil{}:
55      Unit{}
56    case 1n+tail +value <> rest:
57      Laws.LogicalStep{exact, observed, remaining} = logical
58      Laws.LogicalStep{exact, Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, U32.from_nat(cursor)),
59        Core.checked_observe(shape, original, U32.from_nat(cursor)), Some{value}, kept(U32.from_nat(cursor)), observed),
60        logical_keeps(tail, shape, original, tensor, 1n+cursor, rest, remaining, kept)}
61    case 0n value <> rest:
62      Empty.absurd(Laws.LogicalValues(0n, shape, tensor, cursor, value <> rest), logical)
63    case 1n+tail Nil{}:
64      Empty.absurd(Laws.LogicalValues(1n+tail, shape, tensor, cursor, Nil{}), logical)