BendMlAutograd.nbwd_ok: def of bend-ml-autograd@0.1.1.0
Import: import bend-ml-autograd@0.1.1.0/main.bend as BendMlAutograd
Lines 94-108 of bend-ml-autograd@0.1.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-autograd@0.1.1.0/main.bend&start_line=94&end_line=108

import Base
import bend-ml-nat-lemmas@0.1.0.0/main.bend as NL

# The reverse mode returns g times the forward-mode derivative.
def nbwd_ok(e: NE, +x: Nat, +g: Nat) -> {nbwd(e, x, g) == Nat.mul(g, nfwd(e, x)) : Nat}:
  match e:
    case NCst{n}:
      Equal.sym(Nat, Nat.mul(g, 0n), 0n, NL.mul_zero(g))
    case NX{}:
      Equal.sym(Nat, Nat.mul(g, 1n), g, NL.mul_one_r(g))
    case NAdd{+a, +b}:
      Equal.trans(Nat, Nat.add(nbwd(a, x, g), nbwd(b, x, g)), Nat.add(Nat.mul(g, nfwd(a, x)), nbwd(b, x, g)), Nat.mul(g, Nat.add(nfwd(a, x), nfwd(b, x))),
        Equal.cong(Nat, Nat, k => Nat.add(k, nbwd(b, x, g)), nbwd(a, x, g), Nat.mul(g, nfwd(a, x)), nbwd_ok(a, x, g)),
        Equal.trans(Nat, Nat.add(Nat.mul(g, nfwd(a, x)), nbwd(b, x, g)), Nat.add(Nat.mul(g, nfwd(a, x)), Nat.mul(g, nfwd(b, x))), Nat.mul(g, Nat.add(nfwd(a, x), nfwd(b, x))),
          Equal.cong(Nat, Nat, k => Nat.add(Nat.mul(g, nfwd(a, x)), k), nbwd(b, x, g), Nat.mul(g, nfwd(b, x)), nbwd_ok(b, x, g)),
          Equal.sym(Nat, Nat.mul(g, Nat.add(nfwd(a, x), nfwd(b, x))), Nat.add(Nat.mul(g, nfwd(a, x)), Nat.mul(g, nfwd(b, x))), ndist_l(g, nfwd(a, x), nfwd(b, x)))))
    case NMul{+a, +b}:
      nmul_case(g, nfwd(a, x), nfwd(b, x), nval(a, x), nval(b, x), nbwd(a, x, Nat.mul(g, nval(b, x))), nbwd(b, x, Nat.mul(g, nval(a, x))), nbwd_ok(a, x, Nat.mul(g, nval(b, x))), nbwd_ok(b, x, Nat.mul(g, nval(a, x))))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=NE
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nbwd
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=ndist_l
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nfwd
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nmul_case
  https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nval
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_one_r
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_zero