Std.Bounded

View source →

Bounded natural indices.

Bounded(n) is inhabited by values strictly less than n. It is the stdlib replacement for the traditional Fin(n) name and is used for length-safe indexing into Std.Vector.

Functions

  • # fn bounded_left_at(left: Nat, right: Nat, value: Bounded(left)) -> BoundedSum(left, right)
  • # fn bounded_right_at(left: Nat, right: Nat, value: Bounded(right)) -> BoundedSum(left, right)
  • # fn fold_sum(left: Nat, right: Nat, a: Type, side: BoundedSum(left, right), on_left: Function(Bounded(left), a), on_right: Function(Bounded(right), a)) -> a
  • # fn inject_left(n: Nat, m: Nat, value: Bounded(n)) -> Bounded(plus(n, m))

    Embed the left side of a disjoint n + m state space.

  • # fn inject_left_at(left: Nat, right: Nat, value: Bounded(left)) -> Bounded(plus(left, right))
  • # fn inject_right(n: Nat, m: Nat, value: Bounded(m)) -> Bounded(plus(n, m))

    Embed the right side of a disjoint n + m state space. Each constructor in the left bound shifts the right value once, making the two images disjoint by construction.

  • # fn inject_right_at(left: Nat, right: Nat, value: Bounded(right)) -> Bounded(plus(left, right))
  • # fn lift_bounded_sum(left: Nat, right: Nat, side: BoundedSum(left, right)) -> BoundedSum(S(left), right)
  • # fn lift_bounded_sum_equivalent(left: Nat, right: Nat, source: BoundedSum(left, right), target: BoundedSum(left, right), equality: Equivalent(BoundedSum(left, right), source, target)) -> Equivalent(BoundedSum(S(left), right), lift_bounded_sum(left, right, source), lift_bounded_sum(left, right, target))
  • # fn split_injected_left(left: Nat, right: Nat, value: Bounded(left)) -> Equivalent(BoundedSum(left, right), split_sum(left, inject_left_at(left, right, value)), bounded_left_at(left, right, value))

    The structural splitter is a left inverse of both disjoint injections. These equations are the elimination laws needed by dependent consumers: once a combined state is already known to come from one side, matching the proof reduces split_sum to that exact side and value.

  • # fn split_injected_left_at(left: Nat, right: Nat, value: Bounded(left)) -> Equivalent(BoundedSum(left, right), split_sum(left, inject_left_at(left, right, value)), bounded_left_at(left, right, value))
  • # fn split_injected_right(left: Nat, right: Nat, value: Bounded(right)) -> Equivalent(BoundedSum(left, right), split_sum(left, inject_right_at(left, right, value)), bounded_right_at(left, right, value))
  • # fn split_sum(left: Nat, right: Nat, value: Bounded(plus(left, right))) -> BoundedSum(left, right)
  • # fn widen(n: Nat, extra: Nat, value: Bounded(n)) -> Bounded(plus(n, extra))

    Preserve a bounded value while extending its upper bound on the right. The recursion follows the value itself, so no unchecked conversion from Nat is involved.