You are filled with de

termination…

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:

`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.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)`

.`∀ 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 ^{1} 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 `unfold`

ing 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! 🙌

The notion of WF recursion won’t be explained in detail here. The key intuition in this notion, however, is that for a function

`f (v : α) : β`

to be total, it suffices that every`v`

should be mapped to a body in`β`

that…- Either has nothing to do with
`f`

(the base case); - Or depends on some
`f w`

where`w : α`

, and there exists a WF relation`≺`

(“smaller”) that ensures`w ≺ v`

, so that the body can be written in such a way that depends exclusively on some base cases. This prevents infinite recursions from ever happening.

- Either has nothing to do with