def step_inv

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:421

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_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient

421def step_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
422  -exact: {U32.to_nat(index) == cursor : Nat}, state: Gradient.State<shape>,
423  -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
424  -same: Totality.SameSource(contribution, state_contribution(shape, state))) ->
425  Holds<StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))>:
426  Gradient.State{current, total} = state
427  contribution_inv(shape, original, contribution, cursor, index, total, current, Core.read_dynamic(current, index), exact,
428    {\{Core.DynamicSourceRead: meaning => meaning} : Core.DynamicSourceRead<current, index> ->
429      {Core.dynamic_read_value(Core.read_dynamic(current, index)) == Core.checked_observe_dynamic(current, index) : Maybe<&2, F32>}}(
430      Core.dynamic_source_read_model(current, index)),
431    same, inv)