Recursive definitions in Lean

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:

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 well-founded, meaning that starting from any value you can go to “smaller” values only a finite number of times.

Proofs about well-founded recursion

Proving theorems about our structurally recursive search variant was straight-forward, because we could use induction on the parameter start. With well-founded 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:

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 well-founded 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:

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

Well-founded recursion can handle nested recursion, where the recursive call is an argument to another higher-order 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):

A naive implementation of Tree.map like

will not be accepted as-is. Lean does not find a termination argument and suggests we use termination_by. With

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 well-founded 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:

How does this work when we didn't even use the proof? To understand that, let us spell out the termination proof:

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 well-supported by Lean, as in this example:

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

Well-founded recursion can also be used to define mutually-recursive 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:

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.