def sweep_reach

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:207

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws

207def sweep_reach(nodes: List<&2, Backward.Node>, gradients: List<&2, Maybe<&2, F32>>, +count: Nat) ->
208  {Laws.somes(Backward.sweep(nodes, gradients, count)) == Laws.reach(nodes, Laws.somes(gradients), count) : List<&2, Bool>}:
209  match nodes gradients count:
210    case Nil{} gradients count:
211      {==}
212    case Con{node, rest} Nil{} count:
213      {==}
214    case Con{node, rest} Con{gradient, pending} 0n:
215      {==}
216    case Con{+node, rest} Con{+gradient, +pending} 1n+below:
217      %somes_contribute(node, gradient, below, pending) :
218        {Maybe.is_some(&2, F32, gradient) <> Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)) ==
219          Maybe.is_some(&2, F32, gradient) <> Laws.reach(rest, _, below) : List<&2, Bool>}
220      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, gradient) <> xs,
221        Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)),
222        Laws.reach(rest, Laws.somes(Backward.contribute(node, gradient, below, pending)), below),
223        sweep_reach(rest, Backward.contribute(node, gradient, below, pending), below))