Advanced Lean · 12 min

Accumulators and invariants

A tail-recursive call is the final operation in its branch. Moving pending work into an accumulator allows Lean’s compiler to use a loop instead of a growing call stack.

Both sums in the related example perform linear work. The main benefit here is stack usage, not a guaranteed speedup for every input. Execution performance and proof-checking performance are separate measurements.

An accumulator changes on each recursive call. induction xs generalizing acc keeps the induction hypothesis valid for any accumulator. The resulting invariant states sumLoop xs acc = acc + sumRecursive xs.

The exercise gives a general accumulator invariant as a hypothesis. Specialize it at zero and simplify to obtain the user-facing correctness statement. The related example proves the invariant itself.

Exercise

Use h xs 0 to prove loop xs 0 = sum xs.

theorem from_invariant
    (loop : List Nat → Nat → Nat) (sum : List Nat → Nat)
    (h : ∀ xs acc, loop xs acc = acc + sum xs)
    (xs : List Nat) : loop xs 0 = sum xs := by
  sorry

theorem from_invariant
    (loop : List Nat → Nat → Nat) (sum : List Nat → Nat)
    (h : ∀ xs acc, loop xs acc = acc + sum xs)
    (xs : List Nat) : loop xs 0 = sum xs := by
  simpa only [Nat.zero_add] using h xs 0

Related example