Reference · Logic

rainbow.math.logic.scan-length

Logicsrc/rainbow/math/logic/scan_length.clj1 definitions, 2 theorems

A GENERAL (for-all-inputs) correctness theorem about the prefix-sum scan: scanning a list preserves its length, length (cumulative-sum xs) = length xs for every list xs. Unlike the worked examples in prefix-sum (which check specific lists), this is proved by induction over ALL lists, with the induction hypothesis generalized over the running accumulator -- the essential move for reasoning about the higher-order scan fold (whose motive is nat -> list nat). It upgrades the scan from 'computes the right answer on examples' to 'proved structurally correct', the same jump the convergence capstone made for the geometric sequence. Requires prefix-sum/scan-from, algebra/nat-add, data/List.rec, equality/reflexive, equality/congruent-function (all in the D63 checkpoint plus the prefix-sum module).

Depends onalgorithms.proofs.prefix-sum

scan-length/length :
  (x₁ : List ℕ)
  → ℕ

scan-length/scan-from-preserves-length :
  (xs : List ℕ) (acc : ℕ)
  → scan-length/length (prefix-sum/scan-from xs acc) = scan-length/length xs

scan-length/cumulative-sum-preserves-length :
  (xs : List ℕ)
  → scan-length/length (prefix-sum/cumulative-sum xs) = scan-length/length xs