Reference · Logic

rainbow.math.logic.scan-correctness

Logicsrc/rainbow/math/logic/scan_correctness.clj0 definitions, 3 theorems

GENERAL (abstract-element) correctness theorems for the prefix-sum scan: for arbitrary list elements a, b, c the running totals are exactly the prefix sums, cumulative-sum [a] = [a] cumulative-sum [a, b] = [a, a + b] cumulative-sum [a, b, c] = [a, a + b, a + b + c]. Unlike the numeric worked examples in prefix-sum, these are universally quantified over the elements (proved for ALL a, b, c), so they certify the scan's meaning, not just specific outputs. Each holds by reflexivity: the higher-order scan fold unfolds and the leading accumulator offset 0 + a reduces definitionally to a (nat-add recurses on its left argument), leaving exactly the prefix-sum list. Requires prefix-sum/cumulative-sum, algebra/nat-add, data/cons/nil (D63 checkpoint plus the prefix-sum module).

Depends onalgorithms.proofs.prefix-sum

scan-correctness/singleton :
  (a : ℕ)
  → prefix-sum/cumulative-sum [a] = [a]

scan-correctness/pair :
  (a b : ℕ)
  → prefix-sum/cumulative-sum [a, b] = [a, algebra/nat-add a b]

scan-correctness/triple :
  (a b c : ℕ)
  → prefix-sum/cumulative-sum [a, b, c] = [a, algebra/nat-add a b, algebra/nat-add (algebra/nat-add a b) c]