Functional induction

Alternating lists, the manual way

We begin with a function that picks elements from two alternating input lists:

It seems to be doing what it should:

["red", "apple", "green", "banana", "blue", "yellow"]

Now let us try to prove a simple theorem about alternatealternate.{u_1} {α : Type u_1} (xs ys : List α) : List α, namely that the length of the resulting list is the sum of the argument lists' lengths.

The alternatealternate.{u_1} {α : Type u_1} (xs ys : List α) : List α function is not structurally recursive, so using induction xs is not going to be helpful (try it if you are curious how it fails). Instead, we can attempt to write a recursive theorem: we use the theorem we are in the process of proving in the proof, and then rely on Lean's termination checker to check that this is actually ok.

So a first attempt at the proof might start by unfolding the definition of alternatealternate.{u_1} {α : Type u_1} (xs ys : List α) : List α. This exposes a match expression, and our Lean muscle memory tells us to proceed using split. The first case is now trivial. In the second case we use the next tactic to name the new variables. Then we call the theorem we are currently proving on the smaller lists ys and xs, following the pattern of alternatealternate.{u_1} {α : Type u_1} (xs ys : List α) : List α itself, and after some simplification and arithmetic, this goal is closed. Lean will tell us that it cannot prove termination of the recursive call, so we help it by giving the same termination argument as we gave to alternatealternate.{u_1} {α : Type u_1} (xs ys : List α) : List α itself.

This works, but is not quite satisfactory. The split tactic is rather powerful, but having to name the variables with next is tedious. A more elegant variant is to use the same pattern matching in the proof as we do in the function definition:

Note that we no longer unfold the function definition, but let the simplifier reduce the function application in the respective cases.

This style brings us closer to the function to be defined, but we still have to repeat the (possibly complex) pattern match of the original function, and the (possibly complex) termination argument and proof. Moreover, we have to explicitly instantiate the recursive invocation of the theorem, or hope that simp will only use it at the arguments that we want it to.

This is not very satisfying. The repetition makes the proof brittle, as a change to the function definition may require applying the same change to every single proof. We already explained the structure of the function to Lean once, we should not have to do it again!

Alternating lists, with functional induction

This is where the functional induction theorem comes in. For every recursive function, Lean defines a functional induction principle; just append .induct to the name. In our example, it has the following type:

Seeing an induction principle in its full glory can be a bit intimidating, so let us spell it out in prose:

• Given a property of two lists that we want to prove (the motive),

• if it holds when the first list is empty (the minor premise case1, corresponding to the first branch of alternate),

• and if it holds when the first list is non-empty (the minor premise case2, corresponding to the second branch of alternate), where we may assume that it holds for the second list and the tail of the first list (the induction hypothesis, corresponding to the recursive call in alternate),

• then given two arbitrary lists (the targets xs and xy, which correspond to the varying parameters of the function)

• the property holds for these lists.

An induction principle like this is used every time you use the induction tactic; for example induction on natural numbers uses Nat.recAuxNat.recAux.{u} {motive : Nat → Sort u} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (t : Nat) : motive tRecursor identical to `Nat.rec` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`. Used as the default `Nat` eliminator by the `induction` tactic. .

With this bespoke induction principle, we can now use the induction tactic in our proof:

This looks still quite similar to the previous iteration, but note the absence of a termination argument. Furthermore, just like with normal induction, we were provided the induction hypothesis already specialized at the right argument, as you can see in the proof state after case2.

With all this boilerplate out of the way, chances are good that we can now solve both cases with just proof automation tactics, leading to the following two-line proof:

The * in simp's argument list indicates that simp should also consider local assumptions for rewriting; this way it picks up the induction hypothesis.

In terms of proof automation, this is almost as good as it can get: We state the theorem and the induction and leave the rest to Lean's automation. However, just in case you prefer explicit readable and educational proofs, we can of course also spell it out explicitly:

Functions with fixed parameters

The above example demonstrates how to use functional induction in the common simple case. We now look into some more tricky aspects of it.

The first arises if the the recursive function has fixed parameters, as in the following function, which cuts up a list into sublists of length at most n:

Note that in all the recursive calls, the parameter n remains the same, whereas the parameter xs varies. Lean distinguishes between a prefix of fixed parameters, which are identical in all recursive calls, and then the varying parameters, which can change.

Let's first see the function in action:

[["😏", "😄", "😊"], ["😎", "😍", "😘"], ["🥰", "😃", "😉"], ["😋", "😆"]]

Joining these lists back together should give the original list. If we try to use functional induction in the same way as before, we find that we have more goals than we expect. In addition to the expected case1 and case2, we also get a subgoal called n:

unsolved goals
case n
α : Type u_1
n : Nat
⊢ Nat

case case1
α : Type u_1
n : Nat
⊢ (cutN n []).join = []

case case2
α : Type u_1
n : Nat
x✝ : α
xs✝ : List α
ih1✝ : (cutN n (List.drop (?n - 1) xs✝)).join = List.drop (?n - 1) xs✝
⊢ (cutN n (x✝ :: xs✝)).join = x✝ :: xs✝

This is not really a “case”, but the induction tactic does not know that. If we look at the type of cutN.induct, we see that – just like cutN itself - it has a parameter called n, which is hardly surprising:

Note that the motive depends only on the varying parameter of cutN, namely xs, whereas the fixed parameter of cutN, namely n, did not turn into a target of the induction principle, but merely a regular parameter.

So because n is not a target, we cannot write induction n, xs. Instead, we have to instantiate this parameter in the expression passed to using, and now the proof turns out rather nice:

We also could have used the syntax cutN.induct (n := n) if we prefer named arguments.

Overlapping patterns

So far we only defined functions with non-overlapping patterns. Lean also supports defining functions with overlapping patterns, and here functional induction can be particularly helpful.

Our (contrived) example function is one that removes repeated elements from a list of Boolean values:

The first three patterns of the function definition do not overlap, so they can be read as theorems that hold unconditionally. Lean generates such theorems, for use with rw and simp:

But the fourth equation is not a theorem. In general, it is not true that destutter (x :: xs) = x :: destutter xs holds. This equation is only true when the previous cases did not apply. Lean expresses this by preconditions on the equational lemma:

One rather annoying consequence is that if we try to construct a proof about destutter by repeating the same pattern matches, we cannot make progress: