def observed_presence

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:551

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/transform_PROOF.bend as TransformProof

551def observed_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +source: U32, +inside: Bool,
552  -decision: {inside == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) ->
553  Holds<{TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == inside : Bool}>:
554  match inside:
555    case False{}:
556      Holds{Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Core.checked_observe(shape, tensor, source), None{},
557        {\{Holds: proof => proof} : Holds<{Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}> -> {Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}}(
558          absent_observation(shape, tensor, source, Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), decision))))}
559    case True{}:
560      Holds{{\{TransformProof.PresentObservation: value => equal =>
561        Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Core.checked_observe(shape, tensor, source), Some{value}, equal)} :
562        TransformProof.PresentObservation<shape, tensor, source> -> {TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == True{} : Bool}}(
563        TransformProof.present_observation(shape, tensor, source, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), decision)))}