Recursion

Recursive Functions

In Lean, functions can call themselves recursively. The key is having a base case that terminates the recursion:

def factorial (n : Nat) : Nat :=
  if n == 0 then 1 else n * factorial (n - 1)

#eval factorial 5    -- 120
#eval factorial 0    -- 1

The Fibonacci sequence is another classic recursive function:

def fibonacci (n : Nat) : Nat :=
  if n <= 1 then n
  else fibonacci (n - 1) + fibonacci (n - 2)

Lean verifies that recursive functions terminate (for Nat, each recursive call must use a smaller number).

Termination and Proofs

This termination checking is actually connected to Lean's role as a theorem prover. In Lean's type theory, every function must be total (defined for all inputs and guaranteed to terminate). For recursive functions on Nat, Lean automatically checks that the argument decreases on each call — this is called structural recursion. If Lean cannot verify termination automatically, you can provide a decreasing_by proof using tactics (Lean's proof language). Tactics like simp, omega, and exact let you guide the prover step by step. This is a taste of how programming and proving intertwine in Lean.

Your Turn

Define a recursive function sumTo that computes the sum 1 + 2 + ... + n.

Base case: sumTo 0 = 0 Recursive case: sumTo n = n + sumTo (n - 1)