def step_within

bendtorch-core@0.1.0.0 · src/shape/construct_proofs.bend:48

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

48def step_within(+p: Nat, +tail: List<&2, Nat>, +rest: Shape.Capacity<tail>, ih: {True{} == within(tail, rest) : Bool}, bound: Shape.LE(Nat.mul(1n+p, Shape.numel(tail)), 1048576n)) -> {True{} == within((1n+p) <> tail, Shape.capacity.step(1n+p, tail, rest)) : Bool}:
49  match rest:
50    case Shape.Beyond{}:
51      Empty.absurd({True{} == within((1n+p) <> tail, Shape.capacity.step(1n+p, tail, Shape.Beyond{})) : Bool}, Shape.clash(ih))
52    case Shape.Within{+size, +exact, fits}:
53      +scaled = Nats.le_rewrite(Nat.mul(1n+p, size), Nat.mul(1n+p, Shape.numel(tail)), 1048576n, Equal.cong(Nat, Nat, value => Nat.mul(1n+p, value), Shape.numel(tail), size, Equal.sym(Nat, size, Shape.numel(tail), exact)), bound)
54      scale_within(1n+p, tail, size, exact, Shape.bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(1n+p, 1048576n))), scale_fits(p, size, scaled), Nats.le_true(Nat.mul(1n+p, size), 1048576n, scaled))