def go_total

bendtorch-core@0.1.0.0 · src/tensor/elementwise_walk_proof.bend:28

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

28# The division loop keeps quotient * (1 + bp) + remainder + what is left to
29# count fixed, as long as the remainder and the countdown add up to bp.
30def go_total(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat, +fits: {Nat.add(m, r) == bp : Nat}) ->
31  {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r))) ==
32    Nat.add(Nat.add(Nat.mul(d, 1n+bp), r), n) : Nat}:
33  match n m:
34    case 0n m:
35      add_zero_left(Nat.add(Nat.mul(d, 1n+bp), r))
36    case 1n+np 0n:
37      +total = Nat.mul(d, 1n+bp)
38      Equal.trans(Nat,
39        Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))),
40        1n+Nat.add(Nat.add(Nat.add(bp, total), 0n), np),
41        Nat.add(Nat.add(total, r), 1n+np),
42        go_total(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, Equal.sym(Nat, r, Nat.add(r, 0n), add_zero_left(r)), fits)),
43        Equal.trans(Nat, 1n+Nat.add(Nat.add(Nat.add(bp, total), 0n), np), 1n+Nat.add(Nat.add(total, r), np), Nat.add(Nat.add(total, r), 1n+np),
44          Equal.cong(Nat, Nat, x => 1n+Nat.add(x, np), Nat.add(Nat.add(bp, total), 0n), Nat.add(total, r),
45            Equal.trans(Nat, Nat.add(Nat.add(bp, total), 0n), Nat.add(bp, total), Nat.add(total, r),
46              Equal.sym(Nat, Nat.add(bp, total), Nat.add(Nat.add(bp, total), 0n), add_zero_left(Nat.add(bp, total))),
47              Equal.trans(Nat, Nat.add(bp, total), Nat.add(total, bp), Nat.add(total, r), add_comm(bp, total),
48                Equal.cong(Nat, Nat, x => Nat.add(total, x), bp, r, Equal.sym(Nat, r, bp, fits))))),
49          Equal.sym(Nat, Nat.add(Nat.add(total, r), 1n+np), 1n+Nat.add(Nat.add(total, r), np), Arith.add_succ(Nat.add(total, r), np))))
50    case 1n+np 1n+mp:
51      +total = Nat.mul(d, 1n+bp)
52      Equal.trans(Nat,
53        Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))),
54        Nat.add(Nat.add(total, 1n+r), np),
55        Nat.add(Nat.add(total, r), 1n+np),
56        go_total(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, Arith.add_succ(mp, r), fits)),
57        Equal.trans(Nat, Nat.add(Nat.add(total, 1n+r), np), 1n+Nat.add(Nat.add(total, r), np), Nat.add(Nat.add(total, r), 1n+np),
58          Equal.cong(Nat, Nat, x => Nat.add(x, np), Nat.add(total, 1n+r), 1n+Nat.add(total, r), Arith.add_succ(total, r)),
59          Equal.sym(Nat, Nat.add(Nat.add(total, r), 1n+np), 1n+Nat.add(Nat.add(total, r), np), Arith.add_succ(Nat.add(total, r), np))))