def decided_success

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
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
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

667def decided_success(+remaining: Nat, +shape: Shape.Shape, +cursor: Nat, +index: U32,
668  state: Gradient.State<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
669  -exact: {U32.to_nat(index) == cursor : Nat},
670  -fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>},
671  -inside: {Nat.is_lt(cursor, Shape.elements(shape)) == True{} : Bool},
672  -rec: @state: Gradient.State<shape> -> @-fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>} ->
673    Holds<{Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}>) ->
674  Holds<{Laws.accumulated(Gradient.decided(shape, cursor, index, state,
675    state => Gradient.loop(remaining, shape, 1n+cursor, state), decision)) == True{} : Bool}>:
676  match decision:
677    case Shape.BFalse{equal}:
678      Holds{Empty.absurd({Laws.accumulated(Gradient.conversion_error(shape, state)) == True{} : Bool},
679        Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor), PlanProof.eq_true(U32.to_nat(index), cursor, exact), equal))}
680    case Shape.BTrue{equal}:
681      continue_success(remaining, shape, cursor, Gradient.step(shape, index, state),
682        {\{Holds: proof => proof} : Holds<{step_continued(shape, Gradient.step(shape, index, state)) == True{} : Bool}> ->
683          {step_continued(shape, Gradient.step(shape, index, state)) == True{} : Bool}}(
684          step_success(shape, index, state, fits,
685            %Shape.elements_exact(shape) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
686            %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, Shape.elements(shape)) == True{} : Bool}
687            inside)),
688        Equal.trans(List<&2, U32>, Totality.dimensions(step_owner(shape, Gradient.step(shape, index, state))),
689          Totality.dimensions(state_contribution(shape, state)), Shape.dimensions(shape),
690          {\{Holds: proof => proof} : Holds<{Totality.dimensions(step_owner(shape, Gradient.step(shape, index, state))) == Totality.dimensions(state_contribution(shape, state)) : List<&2, U32>}> ->
691            {Totality.dimensions(step_owner(shape, Gradient.step(shape, index, state))) == Totality.dimensions(state_contribution(shape, state)) : List<&2, U32>}}(
692            same_dimensions(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)),
693              {\{Holds: proof => proof} : Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))> ->
694                Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))}(
695                step_retains(shape, index, state)))),
696          fits),
697        rec)