Recursion

Recursion is Lean's core looping mechanism. If you can define a function by structural recursion, Lean guarantees it terminates — and when you cannot, Lean asks you to prove it, which is a conversation worth learning how to have.

Learning Goals

• Write structurally recursive functions over Nat and List.
• Explain why Lean insists every function terminates.
• Convert a naive recursion into an accumulator-passing one, and know when it matters.
• Use termination_by and decreasing_by when the recursion is not structural.
• Know what partial def buys you and what it costs.

Recursive Functions on Nat

A structurally recursive function calls itself on a strictly smaller piece of its input. For Nat, that means the n + 1 pattern from Level 6: match on it, and recurse on n.

1def factorial : Nat → Nat
2  | 0 => 1
3  | n + 1 => (n + 1) * factorial n
4
5#eval factorial 5    -- 120
6#eval factorial 10   -- 3628800

Two base cases are just as easy. fib peels off two at a time, so it needs a rule for 0 and one for 1.

1def fib : Nat → Nat
2  | 0 => 0
3  | 1 => 1
4  | n + 2 => fib n + fib (n + 1)
5
6#eval fib 10                    -- 55
7#eval (List.range 10).map fib   -- [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

Recursive Functions on Lists

Lists are recursive by nature, so the shape of the function mirrors the shape of the data: one branch for [], one for x :: xs that recurses on xs.

1def sumList : List Nat → Nat
2  | [] => 0
3  | x :: xs => x + sumList xs
4
5#eval sumList [1, 2, 3]   -- 6
6
7def myLength : List α → Nat
8  | [] => 0
9  | _ :: xs => 1 + myLength xs
10
11def myMap (f : α → β) : List α → List β
12  | [] => []
13  | x :: xs => f x :: myMap f xs
14
15#eval myMap (· * 2) [1, 2, 3]   -- [2, 4, 6]

Why Lean Insists on Termination

Lean will reject a recursive definition it cannot see terminating. This is not fussiness. In Lean, definitions and proofs are the same thing, and a non-terminating definition would let you prove anything at all:

1-- If this were allowed, it would "prove" any proposition P
2-- def bad (P : Prop) : P := bad P

A function that never returns could claim any type, including False. Rejecting non-termination is what keeps the whole logic sound. When Lean complains about termination it is protecting the thing that makes it worth using.

Accumulators and Tail Recursion

The naive definitions above build up work on the way out of the recursion. Passing an accumulator instead does the work on the way in, so the recursive call is the very last thing that happens — a tail call, which Lean compiles into a loop with no stack growth.

1def sumAcc : List Nat → Nat → Nat
2  | [], acc => acc
3  | x :: xs, acc => sumAcc xs (acc + x)
4
5#eval sumAcc [1, 2, 3] 0   -- 6
6
7-- A helper defined with "where" keeps the clean signature on the outside
8def fastReverse (xs : List α) : List α :=
9  go xs []
10where
11  go : List α → List α → List α
12  | [], acc => acc
13  | x :: xs, acc => go xs (x :: acc)
14
15#eval fastReverse [1, 2, 3, 4]   -- [4, 3, 2, 1]

Sometimes the rewrite changes the complexity class, not just the constant factor. Naive fib recomputes the same values exponentially many times; fib 90 would not finish in your lifetime. Carrying the last two values along makes it linear.

1def fibFast (n : Nat) : Nat :=
2  go n 0 1
3where
4  go : Nat → Nat → Nat → Nat
5  | 0, a, _ => a
6  | k + 1, a, b => go k b (a + b)
7
8#eval fibFast 10   -- 55
9#eval fibFast 90   -- 2880067194370816120   (instant)

Mutual Recursion

Two functions can call each other if you group them in a mutual block. Lean checks that the pair together makes progress.

1mutual
2  def isEven : Nat → Bool
3    | 0 => true
4    | n + 1 => isOdd n
5
6  def isOdd : Nat → Bool
7    | 0 => false
8    | n + 1 => isEven n
9end
10
11#eval isEven 10   -- true
12#eval isOdd 10    -- false

When Recursion Is Not Structural

Euclid's algorithm recurses on a % b, which is not a “peel one off” sub-term of anything. Lean cannot see the decrease by itself, and says so clearly:

1def gcd' (a b : Nat) : Nat :=
2  if _h : b = 0 then a
3  else gcd' b (a % b)
4termination_by b
5
6-- error: failed to prove termination
7-- a b : Nat
8-- _h : ¬b = 0
9-- ⊢ a % b < b

Read that carefully, because it is a good error. termination_by b told Lean which quantity to watch, and Lean worked out the exact obligation that remains: show a % b < b. It even put the hypothesis you need in scope. decreasing_by is where you discharge it.

1def gcd' (a b : Nat) : Nat :=
2  if _h : b = 0 then a
3  else gcd' b (a % b)
4termination_by b
5decreasing_by exact Nat.mod_lt _ (Nat.pos_of_ne_zero _h)
6
7#eval gcd' 12 18   -- 6
8#eval gcd' 48 18   -- 6
9#eval gcd' 7 13    -- 1

partial def: The Escape Hatch

Some functions really might not terminate, or the proof is more trouble than it is worth. partial def tells Lean to compile the function without a termination proof.

1partial def collatzLen (n : Nat) : Nat :=
2  if n <= 1 then 0
3  else if n % 2 == 0 then 1 + collatzLen (n / 2)
4  else 1 + collatzLen (3 * n + 1)
5
6#eval collatzLen 27   -- 111

Nobody knows whether the Collatz sequence always reaches 1, so no termination proof is available — that is a genuine open problem in mathematics. partial is the honest answer here.

Practice

1def countStrings : List String → Nat
2  | [] => 0
3  | _ :: xs => 1 + countStrings xs
4
5#eval countStrings ["a", "b", "c"]   -- 3

1def power (base : Nat) : Nat → Nat
2  | 0 => 1
3  | n + 1 => base * power base n
4
5#eval power 2 10   -- 1024

1def maximum : List Nat → Nat
2  | [] => 0
3  | x :: xs => max x (maximum xs)
4
5#eval maximum [3, 9, 2, 7]   -- 9

1def flatten : List (List Nat) → List Nat
2  | [] => []
3  | xs :: rest => xs ++ flatten rest
4
5#eval flatten [[1, 2], [3], [4, 5]]   -- [1, 2, 3, 4, 5]

Common Mistakes

• Recursing on the wrong argument. In power, the exponent shrinks and the base does not.
• Forgetting the base case.You will get a “Missing cases” error from Level 6, not an infinite loop — Lean catches it first.
• Using plain if where you need the hypothesis. decreasing_by often needs if h : cond.
• Reaching for partial too early. It makes the function unprovable forever. Try termination_by first.

Check Yourself

• Why would allowing non-terminating definitions make Lean unsound?
• What makes sumAcc tail-recursive but sumList not?
• What does termination_by b tell Lean, and what does it leave you to prove?
• Name one thing you can no longer do with a partial def.