Proving Termination in Lean 4, pt. 1

You are filled with determination…

Doing proofs from the book Programming Language Foundations in Agda in the Lean 4 prover has really been a refreshing experience for me. However, things did get annoying sometimes for me, especially when I just couldn’t get pass the termination check.

Although I haven’t seen every piece of the puzzle yet, I do hope that by sharing what I have seen so far, this blog post could save you some time from bashing “lean termination” into your search box , which could potentially lead you to some random web pages about Lean Manufacturing.

Example: The Factorial

Let’s start with our old friend, the factorial function:

import Mathlib.Tactic

def fact : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * fact n

This definition should be quite self-explanatory even for those who are not so familiar with Lean.

We can add some “unit tests” to ensure that this is indeed the fact that we all know and love:

example : fact <$> [1, 2, 3, 4, 5, 6] = [1, 2, 6, 24, 120, 720] := rfl

If the <$> infix operator here looks strange to you, don’t worry! It is just another fancy way of writing your familiar array.map function.

Proof by Structural Recursion

In trivial cases (like this one), it’s quite possible that the termination proof is already done for you.

An intuitive way of seeing how this proof is possible might be the following:

1. fact has only one argument (let’s call it n : ℕ), so in order to prove that fact terminates, we need to prove that n decreases.

2. We search the function body for all call sites of fact, and it turns out there’s only one fact n which is required by fact (n + 1).

3. ∀ n : ℕ, n is smaller than n + 1, so n is indeed decreasing.

… wait a minute. Did I say decreasing? What is actually decreasing here?

According to the docs, we are using a structural recursion here, and thus it’s n’s structure that is decreasing. After all, ℕ is inductively defined:

So you can see the decrease in n’s structure as a decrease in the number of constructors (.zero/.succ) required to construct n.

Proof by WF Recursion and termination_by

What if the structural recursion doesn’t work, and we have to use a well-founded (WF) recursion ¹ instead?

Again, looking at the docs, it seems that this is as easy as adding a termination_by clause:

def factₜ : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * factₜ n
termination_by factₜ n => n

By explicitly pointing out the parameter n, we are actually doing the step 2. above manually: you can see this as a way of informing the compiler that we need to prove that n decreases in some sense later on.

The compiler will then try to perform step 3. automatically, by searching for an implicit instance wf : WellFounded ℕ, and trying to conclude that n is decreasing in terms of wf.rel.

Let’s say it has found Nat.lt_wfRel : WellFounded ℕ, which stands for the well-foundedness of Nat.lt (i.e. the < operator on ℕ):

Since n < n + 1 trivially holds, the termination proof is again completed.

In fact, it is according not to us, but to the compiler that n < n + 1 “trivially holds”. When a termination_by clause is not followed by a decreasing_by clause, a default one will be generated right beside it:

decreasing_by decreasing_tactic

decreasing_tactic, as the name suggests, is a tactic. This means that decreasing_by activates the tactic mode, just like the usual by keyword does.

This tactic is defined as follows:

… and the triviality of n < n + 1 (and many other similar arithmetic statements) is already included in decreasing_trivial:

Proof by WF Recursion and decreasing_by

What if we want to write a decreasing_by clause by ourselves?

In practice, you should try to benefit from the existing infrastructure by extending the decreasing_trivial macro with an extra macro_rules declaration, as stated in the doc comments below:

For the sake of the demo, let’s write a similar proof by hand, but this time with another instance, instWellFoundedRelation : WellFounded ℕ:

More details on this definition

sizeOfWFRel is defined as follows:

… and measure as follows:

… and invImage as follows:

All those definitions above give:

  instWellFoundedRelation
= sizeOfWFRel
= measure sizeOf
= invImage sizeOf Nat.lt_wfRel
= let f := InvImage WellFoundedRelation.rel sizeOf;
  { rel := f, wf := (_ : WellFounded f) }
= let f a b := sizeOf a < sizeOf b;
  { rel := f, wf := (_ : WellFounded f) }

We say a type α is sized if there is an instance of type SizeOf α. Here’s how the SizeOf typeclass and its sizeOf function are introduced in the doc comments:

In short, instWellFoundedRelation ensures that every sized type α (hence the implicit instance parameter [SizeOf α]) satisfies WellFoundedRelation α, in the sense that Nat.lt over its size is well-founded:

  instWellFoundedRelation.rel
= (let f a b := sizeOf a < sizeOf b; { rel := f, wf := (_ : WellFounded f) }).rel
= let f a b := sizeOf a < sizeOf b; f
= (sizeOf · < sizeOf ·)

Now we are ready to write our decreasing_by clause by hand (just to prove it is possible, please don’t try this at home).

As usual, let’s first copy the function declaration and the termination_by clause over:

def factₛ : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * factₛ n
termination_by
  _ n => n

A tiny syntax sugar here: in the termination_by clause, you can write _ instead of the name of the function factₛ.

… and here it is, the decreasing_by clause:

decreasing_by
  show instWellFoundedRelation.rel n n.succ;                  unfold instWellFoundedRelation
  show @WellFoundedRelation.rel ℕ sizeOfWFRel n n.succ;       unfold sizeOfWFRel
  show @WellFoundedRelation.rel ℕ (measure sizeOf) n n.succ;  unfold measure
  show invImage sizeOf Nat.lt_wfRel |>.rel n n.succ;          unfold Nat.lt_wfRel
  show sizeOf n < sizeOf n.succ;                              simp only [sizeOf_nat]
  show n < n.succ;                                            apply Nat.lt_succ_self

Don’t be scared by the snippet above! I have carefully formatted the tactics block (i.e. the block that follows decreasing_by) into two columns:

• The left column is composed entirely of uses of the show tactic. show is usually used to replace a goal’s target to its unified version, but here it’s used carefully as a no-op simply to illustrate the current state of the target on that line.

• The right column contains all the actual tactics that we have used to complete the proof.

As you can see, what we are doing in that snippet is basically replaying the equational reasoning above. The thing that the compiler really wants us to prove is in fact sizeOf n < sizeOf n.succ, but the statement is given in such a complicated way that a few times of definition unfolding turned out to be necessary for us to see it more clearly.

Also, this is the same as n < n + 1, since sizeOf n = n. This is called sizeOf_nat:

After applying that theorem to our goal, the termination proof is completed for the third time.

As a matter of fact, decreasing_with is defined as follows:

… and simp_wf as follows:

Thanks to these carefully-written definitions, many recursions can be automatically proven to be “decreasing” with just the default decreasing_tactic. Kudos to the Lean compiler! 🙌