Module 3 · Lesson 2

Recursion

Recursion is the primary looping mechanism in Lean. Unlike imperative loops, recursive functions must be provably terminating.

Structural Recursion

The simplest form of recursion follows the structure of the data:

lean

1-- Recursion on Nat
2def factorial : Nat → Nat
3  | 0 => 1
4  | n + 1 => (n + 1) * factorial n
5
6-- Recursion on List
7def length : List α → Nat
8  | [] => 0
9  | _ :: xs => 1 + length xs
10
11-- Recursion on custom type
12inductive Tree where
13  | leaf
14  | node (left : Tree) (value : Nat) (right : Tree)
15
16def Tree.size : Tree → Nat
17  | leaf => 0
18  | node left _ right => 1 + left.size + right.size
19
20#eval factorial 5  -- 120
21#eval length [1, 2, 3, 4]  -- 4

In each case, the recursive call is on a "smaller" value—a predecessor of a Nat, the tail of a List, or a subtree. This guarantees termination.

Termination Checking

Lean requires proof that all functions terminate. For structural recursion, this is automatic. But some patterns need help:

lean

1-- This works: clearly structural
2def sum : List Nat → Nat
3  | [] => 0
4  | x :: xs => x + sum xs
5
6-- This needs a hint: the argument shrinks, but not structurally
7def gcd (m n : Nat) : Nat :=
8  if h : n = 0 then m
9  else gcd n (m % n)
10termination_by n
11decreasing_by exact Nat.mod_lt _ (Nat.pos_of_ne_zero h)
12
13#eval gcd 12 18   -- 6

The two clauses do different jobs, and you usually need both:

termination_by n — what gets smaller. Here, the second argument.
decreasing_by … — why it gets smaller. Lean hands you a goal (m % n < n) and you prove it.

⚠

Note the if h : n = 0 rather than if n = 0. The dependent if is what puts h : ¬n = 0 into scope in the else branch — and without it there is no way to prove m % n < n, which is false when n = 0. Forgetting the h : is the single most common reason a termination proof looks impossible.

Sometimes termination is genuinely unknown to mathematics. The Collatz function is the classic example — no one has proved it terminates for every input:

lean

1-- Honest answer: mark it partial
2partial def collatz (n : Nat) : Nat :=
3  if n ≤ 1 then n
4  else if n % 2 == 0 then collatz (n / 2)
5  else collatz (3 * n + 1)
6
7#eval collatz 27   -- 1
8
9-- If you insist on a real def, you must admit the obligation.
10-- Note "all_goals": decreasing_by gets one goal PER recursive call,
11-- and a bare "sorry" would only close the first.
12def collatz' (n : Nat) : Nat :=
13  if n ≤ 1 then n
14  else if n % 2 == 0 then collatz' (n / 2)
15  else collatz' (3 * n + 1)
16termination_by n
17decreasing_by all_goals sorry   -- warning: declaration uses 'sorry'

Partial Functions

When you can't prove termination (or don't want to), use partial:

lean

1-- Reading user input until it is valid: may never terminate,
2-- and that is the intended behaviour
3partial def getValidInput : IO Nat := do
4  IO.println "Enter a positive number:"
5  let input ← (← IO.getStdin).getLine
6  match input.trimAscii.toString.toNat? with
7  | some n => return n
8  | none =>
9    IO.println "Invalid input, try again."
10    getValidInput
11
12-- A loop that runs until told to stop
13partial def countdown (n : Nat) : IO Unit := do
14  if n == 0 then
15    IO.println "liftoff"
16  else
17    IO.println s!"{n}..."
18    countdown (n - 1)
19
20#eval countdown 3

⚠

partial is not free. Lean marks the definition opaque: it compiles and runs, but you cannot unfold it in a proof, and rfl, decide, and simp [f] will not see through it. It also requires the return type to be Inhabited, since Lean needs a value to pretend the function returns.

lean

1partial def loop (n : Nat) : Nat := if n = 0 then 0 else loop (n - 1)
2
3#eval loop 5                       -- 0, runs fine
4-- example : loop 5 = 0 := rfl     -- fails: loop is opaque to the kernel
5
6-- The fuel pattern: a total function that is "partial enough".
7-- Structural on the fuel argument, so Lean accepts it with no proof obligation.
8def collatzFuel : Nat → Nat → Option Nat
9  | 0,        _ => none              -- ran out of fuel
10  | _,        1 => some 1
11  | fuel + 1, n =>
12    if n % 2 == 0 then collatzFuel fuel (n / 2)
13    else collatzFuel fuel (3 * n + 1)
14
15#eval collatzFuel 200 27   -- some 1
16#eval collatzFuel 5 27     -- none

💡

The fuel pattern is the standard way to keep a function total when you cannot prove termination but still want to reason about it. You trade "always gives an answer" for "gives an answer or admits it gave up" — and in exchange the function stays transparent to simp and rfl.

Key Takeaway

Use partialfor functions that intentionally don't terminate (servers, REPLs) or when proving termination is too complex. Regular defrequires termination proof.

Tail Recursion

Tail-recursive functions are optimized to use constant stack space:

lean

1-- NOT tail recursive: has pending work after recursive call
2def factorialBad : Nat → Nat
3  | 0 => 1
4  | n + 1 => (n + 1) * factorialBad n  -- Must multiply AFTER the call
5
6-- Tail recursive: uses an accumulator
7def factorialGood (n : Nat) : Nat :=
8  go n 1
9where
10  go : Nat → Nat → Nat
11  | 0, acc => acc
12  | n + 1, acc => go n ((n + 1) * acc)  -- Recursive call is last
13
14-- Both compute the same result
15#eval factorialBad 10   -- 3628800
16#eval factorialGood 10  -- 3628800

The tail-recursive version won't overflow the stack even for large inputs.

Tracing Recursive Calls

When a recursive function misbehaves, add a small trace to see the call pattern. This is a practical debugging trick.

lean

1def traceSum : List Nat → Nat
2  | [] => dbg_trace "base case"; 0
3  | x :: xs =>
4    dbg_trace s!"visiting {x}, remaining {xs.length}"
5    x + traceSum xs
6
7#eval traceSum [1, 2, 3]
8-- visiting 1, remaining 2
9-- visiting 2, remaining 1
10-- visiting 3, remaining 0
11-- base case
12-- 6

ℹ

The order of the trace lines tells you something real: all three visiting lines print before base case, because each call must recurse fully before it can do its addition. That is exactly what "not tail recursive" looks like — three pending additions stacked up. Compare this with the accumulator version in the next lesson, where the work happens on the way down.

Common Recursive Patterns

Map: Transform Each Element

The map pattern applies a function to each element, building a new list with the transformed values. The recursive call processes the tail, and we prepend the transformed head.

lean

1def map (f : α → β) : List α → List β
2  | [] => []
3  | x :: xs => f x :: map f xs
4
5#eval map (· * 2) [1, 2, 3]  -- [2, 4, 6]

Filter: Keep Matching Elements

The filter pattern tests each element against a predicate. If the element passes, we include it in the result; otherwise, we skip it. The recursion handles the remaining elements.

lean

1def filter (p : α → Bool) : List α → List α
2  | [] => []
3  | x :: xs => if p x then x :: filter p xs else filter p xs
4
5#eval filter (· > 2) [1, 2, 3, 4, 5]  -- [3, 4, 5]

Fold: Accumulate a Result

The fold pattern combines all elements into a single value using an accumulator. Each step updates the accumulator with the next element until the list is exhausted.

lean

1def foldl (f : β → α → β) (init : β) : List α → β
2  | [] => init
3  | x :: xs => foldl f (f init x) xs
4
5#eval foldl (· + ·) 0 [1, 2, 3, 4, 5]  -- 15

Deep Dive: Why Structural vs Well-Founded Matters

The distinction is not just about which incantation you write. Lean compiles the two kinds of recursion differently, and that difference shows up in your proofs.

A structurally recursivefunction compiles to the type's recursor. Its defining equations hold by definition, so rfl and decide can unfold it and simp uses its equations freely.

A well-founded function (one with termination_by) compiles through WellFounded.fix. Its equations are theorems, not definitional truths, so rfl often fails where you expect it to work. You unfold with the generated f.eq_def or simp [f] instead.

lean

1-- Structural: this holds by rfl
2def len : List α → Nat
3  | []      => 0
4  | _ :: xs => len xs + 1
5
6example : len [1, 2] = 2 := rfl   -- ✓
7
8-- Well-founded: prefer the equation lemmas over rfl
9def gcd' (m n : Nat) : Nat :=
10  if h : n = 0 then m else gcd' n (m % n)
11termination_by n
12decreasing_by exact Nat.mod_lt _ (Nat.pos_of_ne_zero h)
13
14example : gcd' 12 18 = 6 := by simp [gcd']   -- or: by decide, or by native_decide

Practical advice: prefer structural recursion when you can restructure the function to get it, especially for anything you plan to prove things about. Reach for termination_by when the natural definition genuinely is not structural.

Mutual Recursion

Functions that call each other use mutual:

lean

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 4  -- true
12#eval isOdd 7   -- true

Recursion vs Iteration

Lean provides for loops in the donotation, but they're syntactic sugar for recursion:

lean

1-- Imperative-looking but actually recursive
2def sumArray (arr : Array Nat) : Nat := Id.run do
3  let mut total := 0
4  for x in arr do
5    total := total + x
6  return total
7
8-- Equivalent explicit recursion
9def sumArray' (arr : Array Nat) : Nat :=
10  arr.foldl (· + ·) 0
11
12#eval sumArray #[1, 2, 3, 4, 5]  -- 15

Exercise: Recursive Power

Implement exponentiation for natural numbers using recursion.

lean

1def pow : Nat → Nat → Nat
2  | _, 0 => 1
3  | x, n + 1 => x * pow x n
4
5#eval pow 2 10  -- 1024

Pattern Matching Next: Tail Recursion