SgdLAWS.sgd_update_reaches_target: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/sgd_LAWS.bend as SgdLAWS
Lines 95-106 of bendtorch-core@0.1.0.0/src/autograd/sgd_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd_LAWS.bend&start_line=95&end_line=106

import Base
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/sgd.bend as Sgd

# The update of parameter id reaches exactly the entry with id older entries
# below it, and keeps every other entry, whatever the list holds.
law sgd_update_reaches_target:
  for +lr: F32
  for newer: List<&1, Backward.Entry>
  for entry: Backward.Entry
  for rest: List<&1, Backward.Entry>
  for +older: Nat
  for fits: {List.length(&1, Backward.Entry, rest) == older : Nat}
  {Sgd.descend_at(lr, List.append(&1, Backward.Entry, newer, entry <> rest), 1n+Nat.add(older, List.length(&1, Backward.Entry, newer)),
      older, Backward.at_head(1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older)) ==
    newer_kept(newer, Sgd.placed(rest, Sgd.descend(lr, entry))) : Sgd.Walked()}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd.bend&name=Walked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd.bend&name=descend
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd.bend&name=descend_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd.bend&name=kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd.bend&name=placed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sgd_LAWS.bend&name=newer_kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Entry
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=at_head
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&name=eq_refl
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&name=older_ne