def keep_left_source

bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:82

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

82def keep_left_source(+plan: Shape.BroadcastPlan, +index: U32, -input: Core.Dynamic, -right: Core.Dynamic,
83  -left_index: U32, -right_index: U32, -value: F32,
84  -exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
85  -present: {Some{value} == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) ->
86  Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, right, index) ==
87    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}>:
88  Holds{Equal.trans(Maybe<&2, F32>, Elementwise.expected(Elementwise.KeepLeft{}, plan, input, right, index),
89    Projection.specified_expected(Elementwise.KeepLeft{}, input, right, Projection.offset_spec(plan, U32.to_nat(index))),
90    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))),
91    Projection.expected_projection_refines(Elementwise.KeepLeft{}, plan, input, right, index),
92    %Equal.trans(Maybe<&1, U32 & U32>, Some{(left_index, right_index)}, Projection.indices_result(Elementwise.input_indices(plan, index)),
93      Projection.offset_spec(plan, U32.to_nat(index)),
94      Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Maybe<&1, U32 & U32>, Projection.indices_result,
95        Done{(left_index, right_index)}, Elementwise.input_indices(plan, index), exact),
96      Projection.input_indices_refines(plan, index)) :
97      {Projection.specified_expected(Elementwise.KeepLeft{}, input, right, _) == Laws.source_value(input, _) : Maybe<&2, F32>}
98    {\{Holds: proof => proof} : Holds<{Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, Core.checked_observe_dynamic(input, left_index)) ==
99      Core.checked_observe_dynamic(input, left_index) : Maybe<&2, F32>}> ->
100      {Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, Core.checked_observe_dynamic(input, left_index)) ==
101        Core.checked_observe_dynamic(input, left_index) : Maybe<&2, F32>}}(
102      keep_left_expected(right, right_index, Core.checked_observe_dynamic(input, left_index), value, present)))}