Recursive definitions in Lean
Lean is a general purpose programming language. For example, the Lean compiler itself is written in Lean, and so is its language server, which provides those nice squiggly lines that you see when you edit a Lean file. As a Lean developer, you can rightfully expect to be able to write the kind of code you’d be writing in other programming languages.
Lean is also an interactive theorem prover that allows you to formalize mathematics or prove that the programs you wrote are actually correct with regard to their specification. Because Lean is both of these things, there are some possibly unfamiliar aspects that you have to pay attention to, even if you are just interested in Lean as a programming language.
One such aspect is termination  Lean is much pickier about whether programs ever actually return a result. This post explains why termination matters, how you can deal with it when you care, and how you you can avoid having to deal with it when you do not care.
Nontermination vs. soundness
To begin, let's briefly recapitulate why termination matters. Consider the following function search
that goes through the natural numbers until its argument f
returns a value (or keeps searching if f
always returns Option.none
):
def search {α} (f : Nat → Option α) (start : Nat) : α :=
match f start with
 .some x => x
 .none => search f (start + 1)
We could use this function as a blunt way to find the square root of 121
. For example, running
#eval search (fun n => if n * n ≥ 121 then .some n else .none) 0
will output
11
In a conventional programming language we can write this function without further ado, but Lean will not let us. And that is a good thing, because if it would, we could write a function that claims to calculate a value of any type α
:
def anything {α} : α := search (fun _ => .none) 0
The existence of this function is bad news for Leanthetheoremprover! In Lean, propositions (statements to prove) are represented as types, and a proof of a proposition is represented as a term of that type.
False propositions like 1 = 0
are therefore empty types, types that are not inhabited by any terms.
But our anything
function can have any type α
we want, and thus would allow us to prove anything:
theorem boom : 1 = 0 := ⊢ 1 = 0
element_of_empty_type:Empty⊢ 1 = 0
All goals completed! 🐙
We certainly don't want to be able to prove 1 = 0
, and so it is just for the better that Lean expects us to pay attention to termination.
Your options
As a Lean developer, you now have a few options when writing recursive definitions. On your menu are

writing structurally recursive functions

proving that your functions terminate, using wellfounded recursion

not worrying about recursion and mark your functions as partial or even unsafe.
Each of them have their respective advantages and disadvantages, which we’ll discuss now.
Structural recursion
It is often the case that your recursive functions follow the structure of a recursively defined data type. In these cases, Lean will see that your function definition is obviously terminating and nothing more needs to be done.
Consider a variant of our search
function from above, where we count down from the number start
:
def search {α} (f : Nat → Option α) (start : Nat) : Option α :=
match f start with
 .some x => .some x
 .none =>
match start with
 0 => .none
 n+1 => search f n
We have changed the result type of the function to Option α
so that search
can return Option.none
if nothing is found, and use pattern matching to try each number in sequence.
This follows the recursive structure of the Nat
type, which is defined as
inductive Nat where
 zero : Nat
 succ (n : Nat) : Nat
in the Lean Prelude, and 0
and n+1
are merely pretty syntax for the constructors Nat.zero
and Nat.succ n
. Because search
follows the recursive structure, Lean accepts the definition as is; no extra termination argument needed.
In general, if you plan to prove theorems about your functions, a structurally recursive definition is most pleasant to work with, for two reasons:

Since the definition follows the structure of the argument’s data type, you can use induction over that data type when proving theorems, as in this case:
theorem search_const_none {α} (start : Nat) : search (α := α) (fun _ => .none) start = .none := α:Type u_1start:Nat⊢ search (fun x => none) start = none α:Type u_1⊢ search (fun x => none) 0 = noneα:Type u_1n✝:Nata✝:search (fun x => none) n✝ = none⊢ search (fun x => none) (n✝ + 1) = none case zero α:Type u_1⊢ search (fun x => none) 0 = none All goals completed! 🐙 case succ _n IH α:Type u_1_n:NatIH:search (fun x => none) _n = none⊢ search (fun x => none) (_n + 1) = none All goals completed! 🐙

The defining equation of your function holds definitionally:
example : search (fun n => if n * n ≤ 121 then .some n else .none) 100 = .some 11 := rfl
This can be crucial if you use your function in types, and expect the type checker to calculate with your function. A full discussion of why and when that matters would takes us too far here, though.
Lean will automatically recognize structurally recursive functions, and even allows you to peel off more than one constructor at a time, as in the ubiquitous example of recursively calculating the Fibonacci numbers:
def fib : Nat → Nat
 0 => 0
 1 => 1
 .succ (.succ n) => fib n + fib (.succ n)
If you want to know whether Lean is using structural recursion to implement your definition, run #print fib
and look for mentions of functions called brecOn
.
Wellfounded recursion
If your function happens to follow the recursive structure of its argument and it just works, great! But often your code just doesn't fit this pattern. Consider these popular algorithms:

Sorting algorithms like Quicksort and Mergesort split and reorder the input lists, rather than recursing on just the tail of the list.

Division, implemented as iterated subtraction, recurses not on the predecessor of the input number, but takes bigger steps.

With binary search sometimes one argument increases and sometimes the other argument decreases. However, their difference always decreases, and often by more than just one.
In such cases, you can still define your function, but now an explicit termination proof is needed.
To stick with our example, let us search counting up again, as originally, but define an upper bound (called to
), so that the search always terminates:
def search {α} (f : Nat → Option α) (start : Nat) (to : Nat) : Option α :=
match f start with
 .some x => .some x
 .none =>
if start < to then
search f (start + 1) to
else
.none
Notice the squiggly line beneath the recursive call search f (start + 1) to
. If you hover it, you will see that Lean complains rather verbosely:
fail to show termination for search with errors argument #3 was not used for structural recursion failed to eliminate recursive application search f✝ (start + 1) to argument #4 was not used for structural recursion failed to eliminate recursive application search f✝ (start + 1) to structural recursion cannot be used Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) start to 1) 16:2144 ? = Please use `termination_by` to specify a decreasing measure.
This message gives us a glimpse into the inner workings of Lean here. It first tries really hard to find structural recursion, but neither argument three (start
) nor argument four (to
) decreases structurally.
Then, it also tries to prove wellfounded termination automatically, but fails again. It displays in a small, mildly obscure matrix how the parameters (start
and to
) behave at the recursive calls (of which our function only has one). In the output above we see that Lean could not prove start
to be decreasing, and the parameter to
was proved to be equal, so certainly not decreasing.
Finally, it at least tells us what to do: Use termination_by
!
Proving termination
Taking a step back, let us consider our function definition and ask: Why does it terminate? It terminates because it keeps making recursive calls only as long as start < to
holds. Put differently, it makes at most to  start
recursive calls. This forms a decreasing measure on the function arguments, and we can tell Lean about it using the termination_by
annotation, which goes after the function definition:
def search {α} (f : Nat → Option α) (start : Nat) (to : Nat) : Option α :=
match f start with
 .some x => .some x
 .none =>
if start < to then
search f (start + 1) to
else
.none
termination_by to  start
The termination_by
clause indicates an expression that gets smaller in each recursive call.
With this information, Lean will notice that to  (start + 1)
really is smaller than to  start
, and therefore this function definition terminates. Here Lean finds the proof automatically, but we can also do the proof manually, by writing a decreasing_by
clause with a tactic proof:
decreasing_by simp_wf apply Nat.sub_succ_lt_self assumption
After the simp_wf
tactic, which cleans up some internal technicalities, we have to solve the goal
start to : Nat h✝: start < to ⊢ to  (start + 1) < to  start
where we recognize the measure we specified in termination_by
. It is worth noting that Lean understands that the recursive call is in the then
branch of an if
, and helpfully added the condition start < to
as a hypothesis.
If you don't write a decreasing_by
clause, then by default Lean uses
decreasing_by decreasing_tactic
The decreasing_tactic
runs simp_wf
, applies lexicographic ordering lemmas and then tries to use the extensible decreasing_trivial
tactic to discharge the subgoals.
Often, the expression after termination_by
is of type Nat
. Then it is called a measure on the function arguments, and gives an upper bound on how often the function will make recursive calls. Generally, that expression can have any type α
with a WellFoundedRelation α
instance. This type class declares what it means for a value of α
to be “smaller” to another (like <
on Nat
) and provides a proof that that relation is wellfounded, meaning that starting from any value you can go to “smaller” values only a finite number of times.
Proofs about wellfounded recursion
Proving theorems about our structurally recursive search
variant was straightforward, because we could use induction on the parameter start
. With wellfounded recursion this is not so easy: Simple induction on start
or to
will lead the proof into a different direction than the function definition, and that is rarely productive. Maybe we could introduce a variable that’s equal to to  start
and perform induction on that, or use a suitable induction principle like Mathlib’s Nat.le_induction
. But more often that not it's easiest to write the proof itself as a recursive definition, following the same recursion structure as the function:
theorem search_const_none {α} (start to : Nat) :
search (α := α) (fun _ => .none) start to = .none := α:Type u_1start:Natto:Nat⊢ search (fun x => none) start to = none
α:Type u_1start:Natto:Nat⊢ (if start < to then search (fun x => none) (start + 1) to else none) = none
α:Type u_1start:Natto:Nath✝:start < to⊢ search (fun x => none) (start + 1) to = noneα:Type u_1start:Natto:Nath✝:¬start < to⊢ none = none
α:Type u_1start:Natto:Nath✝:start < to⊢ search (fun x => none) (start + 1) to = none All goals completed! 🐙
α:Type u_1start:Natto:Nath✝:¬start < to⊢ none = none All goals completed! 🐙
termination_by to  start
The unfold search
step exposes the function definition's if start < to then … else
, the split
then proceeds into the two branches, and in the first case we use the theorem we are currently defining. This seemingly circular reasoning is then justified by the termination checker, which we have to help out with termination_by
, just like above.
It is one of the perks of proving theorems in a system based on dependent type theory that the tools we have to define functions can also be used to prove theorems!
Nevertheless, it is a bit silly to repeat the whole termination argument at every proof about search
. In the future, Lean will generate a bespoke induction principle for each recursive function, which should simplify these proofs considerably.
As you prove more theorems about your function you might notice that you often have to explicitly unfold it (e.g., using unfold search
, rw [search]
or simp [search]
) where you may expect an equality to hold just by definition. This is one of the downsides of definitions using wellfounded recursion: the defining equation no longer holds by definition, but is merely a propositional equality proved by Lean for you, in a theorem named search._unfold
or search.eq_def
, depending on your version of Lean:
#check search.eq_def
search.eq_def.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) : search f start to = match f start with  some x => some x  none => if start < to then search f (start + 1) to else none
Nested recursion
Wellfounded recursion can handle nested recursion, where the recursive call is an argument to another higherorder function. A typical occurrence of that pattern is if you have an inductive type (here Tree
) whose definition includes a recursive occurrence of itself inside some other type (here List
):
inductive Tree (α : Type) where
 node : α → List (Tree α) → Tree α
A naive implementation of Tree.map
like
def Tree.map {α β} (f : α → β) : Tree α → Tree β
 node v ts => node (f v) (List.map (fun t => Tree.map f t) ts)
will not be accepted asis. Lean does not find a termination argument and suggests we use termination_by
. With
def Tree.map {α β} (f : α → β) : Tree α → Tree β
 node v ts => node (f v) (List.map (fun t => Tree.map f t) ts)
termination_by t => t
we clarify that.
Since the Tree α
parameter of map
is bound in the body of Tree.map
, not in the declaration,
we bind it in the termination_by
clause as well.
Now the recursive call has a squiggly underline with the following error message:
failed to prove termination, possible solutions:  Use `have`expressions to prove the remaining goals  Use `termination_by` to specify a different wellfounded relation  Use `decreasing_by` to specify your own tactic for discharging this kind of goal α : Type v : α ts : List (Tree α) t : Tree α ⊢ sizeOf t < 1 + sizeOf ts
We recognize v
and ts
as the fields of our tree, t
as the tree in the argument to List.map
, and quite reasonably Lean tries to prove that t
is in some sense smaller than the argument to Tree.map
. The sizeOf : Tree α → Nat
function was automatically generated by Lean when we defined the Tree
inductive data type.
But note that nothing in this proof goal connects t
to ts
. The variable t
is an arbitrary Tree
! This is because Lean does not know that List.map f l
calls its argument only on elements on l
. So in this form, the proof goal is unsolvable.
The cure for this problem is called List.attach
, a function defined in the standard library (so import Std
if you haven't already) with type
List.attach.{u_1} {α : Type u_1} (l : List α) : List { x // x ∈ l }
It replaces each element x
in the list l
with a pair consisting of the element x
, and a proof x ∈ l
that the element is in the list. We can use this function before Lift.map
, ignore the proof in the argument to List.map
, and suddenly Lean accepts the definition:
def Tree.map {α β} (f : α → β) : Tree α → Tree β
 node v ts => node (f v) (List.map (fun ⟨t, h⟩ => Tree.map f t) ts.attach)
How does this work when we didn't even use the proof? To understand that, let us spell out the termination proof:
def Tree.map {α β} (f : α → β) : Tree α → Tree β
 node v ts => node (f v) (List.map (fun ⟨t, h⟩ => Tree.map f t) ts.attach)
termination_by t => t
decreasing_by
α:Typev:αts:List (Tree α)t:Tree αh:t ∈ ts⊢ sizeOf t < 1 + sizeOf ts
All goals completed! 🐙
After simp_wf
the proof goal reads
α: Type v: α ts: List (Tree α) t: Tree α h: t ∈ ts ⊢ sizeOf t < 1 + sizeOf ts
and we now see the crucial hypothesis t ∈ ts
that connects t
to ts
, and makes this proof obligation provable. The default tactic decreasing_trivial
recognizes this pattern and closes the proof for us.
So if you struggle defining a function with nested recursion, try List.attach
or search for a similar function for your data type.
Lexicographic orders
For some functions, the termination argument is not merely that a single measure (i.e. a function from the function arguments to Nat
) decreases, but we have two (or more) measures, and at each recursive call, either the first measure decreases, or the first stays the same and the second decreases. This combined order is called the lexicographic order, and is wellsupported by Lean, as in this example:
def ackermann : Nat → Nat → Nat
 0, m => m + 1
 n + 1, 0 => ackermann n 1
 n + 1, m + 1 => ackermann n (ackermann (n + 1) m)
termination_by n m => (n, m)
For tuples, Lean by default uses the lexicographic order, and here Lean figures out that in each recursive call, either n
gets smaller, or n
stays the same and m
gets smaller.
Mutual recursion
Wellfounded recursion can also be used to define mutuallyrecursive functions. Imagine we want to split our search
function into two functions, one that checks f n
and a second one that increases n
– maybe because we want to be able to call both variants. We can put the two functions into a mutual
block:
mutual
def search {α} (f : Nat → Option α) (start : Nat) (to : Nat) : Option α :=
match f start with
 .some x => .some x
 .none => searchAbove f start to
termination_by (to  start, 1)
def searchAbove {α} (f : Nat → Option α) (start : Nat) (to : Nat) : Option α :=
if start < to then
search f (start + 1) to
else
.none
termination_by (to  start, 0)
end
In this example the call from search
to searchAbove
does not change the parameters at all. How can we hope to prove this definition terminating? Since the calls from searchAbove
to search
have decreasing arguments, it suffices if calls from search
to searchAbove
are equal. We can express that using a lexicographic ordering, where the first component is our usual termination measure (to  start
) and the second component is simply the constant 1
for search
and 0
for searchAbove
. In this order, the call from search
to searchAbove
is decreasing, because the second component decreases.
Avoiding termination proofs
As we just saw, structural and wellfounded recursion are powerful tools to define recursive functions in a way that we can use them in proofs, but are sometimes nontrivial to use. When we just want to define functions for use in programs, but not in proofs, there is a way out.
We can declare that a function is partial
. If we do that, Lean will accept almost any function definition, like our nonterminating search:
partial def search {α} (f : Nat → Option α) (start : Nat) : Option α :=
match f start with
 .some x => .some x
 .none => search f (start + 1)
As a partial
function, it can be used in program just fine: the command
#eval search (fun n => if n * n ≥ 121 then .some n else .none) 0
prints
some 11
But for the purposes of proofs, search
is completely opaque. All we know is that it exists, but not how it behaves.
You might have spotted that this search
function returns an Option α
, unlike the example we started with, which simply returned an α
. That is because the type of a partial
function must be inhabited, or else allowing proofs to merely mention the function causes havoc, as we saw in the introduction.
If you need to define such a function, you can use the final technique presented in this post, namely the unsafe
keyword:
unsafe def search {α} (f : Nat → Option α) (start : Nat) : α :=
match f start with
 .some x => x
 .none => search f (start + 1)
Now Lean will accept, compile and run even this definition, just like a conventional programming language out there. Lean will, however, prevent you from using unsafe definitions in theorems and proofs, so that soundness is preserved.
Conclusion
We have come full circle: Starting with code that you might write in another functional programming language, we saw why this can't just go through in Lean. We learned how to convince Lean that a function definition is fine by using structural and wellfounded recursion, and saw that wellfounded recursion is very general and powerful, but also not necessarily easy to use. Luckily, we do not have to deal with any of that if we just want to write programs, as Lean lets us opt out of termination checking with partial
and unsafe
.
The Lean FRO has improvements to recursive definitions on its roadmap, and future versions of Lean will generate induction principles from recursive functions, support mutual structural recursion and more. And if there is something that Lean could do differently here to make your Lean programming experience more pleasant, please let us know!
Update: This post was slighly edited in February 2024 to adjust to the new termination_by
syntax introduced in Lean v4.6.