Reference · Algorithm guarantees

rainbow.algorithms.proofs.interval-arithmetic

Algorithm guaranteessrc/rainbow/algorithms/proofs/interval_arithmetic.clj4 definitions, 5 theorems

AHoF V40 Interval Arithmetic: the sound enclosure of a signed-rational value by a lower/upper bound pair, with the additive interval operation that underlies the reachability propagators (V40-V47). An interval is a pair [lo, hi] of signed rationals, and interval addition adds the bounds componentwise: [a, b] + [c, d] = [a + c, b + d] which is the sound enclosure of the sumset {x + y : x in [a,b], y in [c,d]}. Bounds are exact signed rationals (no floating rounding), so the enclosure is proved data. Addition reduces by reflexivity on concrete bounds; the containment/soundness predicate (x in [a,b] => lo <= x <= hi) uses the signed order and the width lo-hi lands on a non-canonical Grothendieck pair, so those stay executable/order-level concerns. What is proved here is the interval constructor with its projection laws and the componentwise additive law with worked instances. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 3 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.interval-arithmetic` prints this classification.

interval/make :
  (x₁ x₂ : ℚ)
  → data/Product ℚ ℚ

interval/lower :
  (x₁ : data/Product ℚ ℚ)
  → ℚ

interval/upper :
  (x₁ : data/Product ℚ ℚ)
  → ℚ

interval/add :
  (x₁ x₂ : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

interval/lower-of-make :
  (lo hi : ℚ)
  → interval/lower (interval/make lo hi) = lo

interval/upper-of-make :
  (lo hi : ℚ)
  → interval/upper (interval/make lo hi) = hi

interval/add-bounds :
  (a b c d : ℚ)
  → interval/add (interval/make a b) (interval/make c d) = interval/make (a + c) (b + d)

interval/add-1-3-example :
  → interval/add (make) (make₁) = interval/make (signed/from-nnrat 3) (signed/from-nnrat 7)
  where make := interval/make (signed/from-nnrat 1) (signed/from-nnrat 3)
  where make₁ := interval/make (signed/from-nnrat 2) (signed/from-nnrat 4)

interval/add-0-width-example :
  → interval/add (make) (make₁) = interval/make (signed/from-nnrat 0) (signed/from-nnrat 5)
  where make := interval/make (signed/from-nnrat 0) (signed/from-nnrat 2)
  where make₁ := interval/make (signed/from-nnrat 0) (signed/from-nnrat 3)