def continue_inv

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

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

433def continue_inv(+remaining: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
434  result: Gradient.Step<shape>, -step: StepInv(shape, original, contribution, cursor, result),
435  -same: Totality.SameSource(contribution, step_owner(shape, result)),
436  -rec: @state: Gradient.State<shape> -> @-inv: Inv(shape, original, contribution, 1n+cursor, state_total(shape, state)) ->
437    @-same: Totality.SameSource(contribution, state_contribution(shape, state)) ->
438    Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))>) ->
439  Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor),
440    Gradient.continue_step(shape, state => Gradient.loop(remaining, shape, 1n+cursor, state), result))>:
441  match result:
442    case Gradient.Stop{owner, total, error}:
443      Holds{Unit{}}
444    case Gradient.Continue{state}:
445      Holds{{\{Holds: proof => proof} :
446        Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))> ->
447        LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))}(rec(state, step, same))}