def decided_inv

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

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/lifecycle.bend as Lifecycle
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

454def decided_inv(+remaining: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
455  state: Gradient.State<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
456  -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
457  -same: Totality.SameSource(contribution, state_contribution(shape, state)),
458  -rec: @state: Gradient.State<shape> -> @-inv: Inv(shape, original, contribution, 1n+cursor, state_total(shape, state)) ->
459    @-same: Totality.SameSource(contribution, state_contribution(shape, state)) ->
460    Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))>) ->
461  Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.decided(shape, cursor, index, state,
462    state => Gradient.loop(remaining, shape, 1n+cursor, state), decision))>:
463  match decision:
464    case Shape.BFalse{equal}:
465      conversion_inv(shape, original, contribution, Nat.add(remaining, 1n+cursor), state)
466    case Shape.BTrue{equal}:
467      continue_inv(remaining, shape, original, contribution, cursor, Gradient.step(shape, index, state),
468        {\{Holds: proof => proof} : Holds<StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))> ->
469          StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))}(
470          step_inv(shape, original, contribution, cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), state, inv, same)),
471        {\{Holds: proof => proof} : Holds<Totality.SameSource(contribution, step_owner(shape, Gradient.step(shape, index, state)))> ->
472          Totality.SameSource(contribution, step_owner(shape, Gradient.step(shape, index, state)))}(
473          same_trans(contribution, state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)), same,
474            {\{Holds: proof => proof} : Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))> ->
475              Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))}(
476              step_retains(shape, index, state)))),
477        rec)