λleanlab

Advanced Lean

Efficiency: tail recursion

Write two equivalent sums and prove the accumulator invariant.

Open TailRecursion.lean in editor
def sumRecursive : List Nat → Nat
  | [] => 0
  | x :: xs => x + sumRecursive xs

def sumLoop : List Nat → Nat → Nat
  | [], acc => acc
  | x :: xs, acc => sumLoop xs (acc + x)

def sumTail (xs : List Nat) : Nat := sumLoop xs 0

-- Generalize the accumulator: each recursive call changes it.
theorem sumLoop_spec (xs : List Nat) (acc : Nat) :
    sumLoop xs acc = acc + sumRecursive xs := by
  induction xs generalizing acc with
  | nil => simp [sumLoop, sumRecursive]
  | cons x xs ih => simp [sumLoop, sumRecursive, ih, Nat.add_assoc]

-- This proves agreement for every list, not just the test below.
theorem same_sum (xs : List Nat) : sumTail xs = sumRecursive xs := by
  simp [sumTail, sumLoop_spec]

def main : IO Unit := do
  let values := List.range 101
  IO.println s!"Recursive: {sumRecursive values}"
  IO.println s!"Tail recursive: {sumTail values}"

Explanation

x + sumRecursive xs

The recursive call leaves an addition to perform afterward. Both algorithms do linear work, but this version builds a chain of pending calls.

sumLoop xs (acc + x)

The recursive call is the final operation. Lean’s compiler can use a loop and avoid a growing call stack. Small inputs may not show a measurable time difference.

induction xs generalizing acc

Keeps the accumulator arbitrary in the induction hypothesis so it applies to acc + x in the recursive case.

same_sum

Proves equality for all lists. Running main checks two concrete computations; the theorem establishes the general relationship.

Expected output

Reference only. Run the file to check its actual result.

Recursive: 5050
Tail recursive: 5050

Exercise

Use List.range 10 and verify the sum is 45. Read the accumulator proof before changing the algorithm.

Related examples

Further reading