BroadcastPROOF.keep_left_source: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend as BroadcastPROOF
Lines 82-102 of bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend&start_line=82&end_line=102

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/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
import bendtorch-core@0.1.0.0/src/autograd/broadcast_LAWS.bend as Laws

def keep_left_source(+plan: Shape.BroadcastPlan, +index: U32, -input: Core.Dynamic, -right: Core.Dynamic,
  -left_index: U32, -right_index: U32, -value: F32,
  -exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
  -present: {Some{value} == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) ->
  Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, right, index) ==
    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}>:
  Holds{Equal.trans(Maybe<&2, F32>, Elementwise.expected(Elementwise.KeepLeft{}, plan, input, right, index),
    Projection.specified_expected(Elementwise.KeepLeft{}, input, right, Projection.offset_spec(plan, U32.to_nat(index))),
    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))),
    Projection.expected_projection_refines(Elementwise.KeepLeft{}, plan, input, right, index),
    %Equal.trans(Maybe<&1, U32 & U32>, Some{(left_index, right_index)}, Projection.indices_result(Elementwise.input_indices(plan, index)),
      Projection.offset_spec(plan, U32.to_nat(index)),
      Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Maybe<&1, U32 & U32>, Projection.indices_result,
        Done{(left_index, right_index)}, Elementwise.input_indices(plan, index), exact),
      Projection.input_indices_refines(plan, index)) :
      {Projection.specified_expected(Elementwise.KeepLeft{}, input, right, _) == Laws.source_value(input, _) : Maybe<&2, F32>}
    {\{Holds: proof => proof} : Holds<{Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, Core.checked_observe_dynamic(input, left_index)) ==
      Core.checked_observe_dynamic(input, left_index) : Maybe<&2, F32>}> ->
      {Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, Core.checked_observe_dynamic(input, left_index)) ==
        Core.checked_observe_dynamic(input, left_index) : Maybe<&2, F32>}}(
      keep_left_expected(right, right_index, Core.checked_observe_dynamic(input, left_index), value, present)))}

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_LAWS.bend&name=source_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend&name=keep_left_expected
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe_dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=input_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=expected_projection_refines
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=indices_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=input_indices_refines
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=offset_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=specified_expected