def periods

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:136

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

136def periods(+q: Nat, +b: Nat, +r: Nat, +d: Nat, bound: Shape.LE(r, b)) -> {Nat.divmod.go(Nat.add(Nat.mul(q, 1n+b), r), b, d, 0n) == (Nat.add(q, d), r) : Nat & Nat}:
137  match q:
138    case 0n:
139      %Equal.sym(Nat & Nat, Nat.divmod.go(r, b, d, 0n), (d, Nat.add(r, 0n)), remainder(r, b, d, 0n, bound)) : {_ == (d, r) : Nat & Nat}
140      %Equal.sym(Nat, Nat.add(r, 0n), r, Broadcast.add_zero(r)) : {(d, _) == (d, r) : Nat & Nat}
141      {==}
142    case 1n+p:
143      +rest = Nat.add(Nat.mul(p, 1n+b), r)
144      %Index.add_assoc(b, Nat.mul(p, 1n+b), r) : {Nat.divmod.go(1n+_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
145      %Equal.sym(Nat, 1n+Nat.add(b, rest), Nat.add(b, 1n+rest), Broadcast.add_succ(b, rest)) : {Nat.divmod.go(_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
146      %Broadcast.add_zero(b) : {Nat.divmod.go(Nat.add(b, 1n+rest), _, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
147      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(b, 1n+rest), Nat.add(b, 0n), d, 0n), Nat.divmod.go(1n+rest, 0n, d, Nat.add(b, 0n)), drain(b, 1n+rest, 0n, d, 0n)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
148      %Equal.sym(Nat, Nat.add(b, 0n), b, Broadcast.add_zero(b)) : {Nat.divmod.go(1n+rest, 0n, d, _) == (1n+Nat.add(p, d), r) : Nat & Nat}
149      %Equal.sym(Nat & Nat, Nat.divmod.go(rest, b, 1n+d, 0n), (Nat.add(p, 1n+d), r), periods(p, b, r, 1n+d, bound)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
150      %Broadcast.add_succ(p, d) : {(_, r) == (1n+Nat.add(p, d), r) : Nat & Nat}
151      {==}