Functional induction
Proving properties of recursive functions is usually easiest when the proof follows the structure of the function that is being verified – same case splitting, same recursion pattern. To avoid having to spell this out in every proof, the upcoming 4.8 release of Lean provides a functional induction principle for recursive functions. Used with the induction
tactic, this takes care of the repetitive parts of the proof.
In this blog post we will look at examples of recursive functions where this feature can be convenient, how to use it, and where its limits lie. In particular, we look at functions with fixed parameters and overlapping patterns and mutually recursive functions, where this feature is especially useful. Because some recursive functions can cause the simp
tactic to loop, as it tries to unfold the definition infinitely many times, we also examine techniques for avoiding infinite simplification.
The examples in this post are short, in order to demonstrate the feature. If the gain does not seem to be very great, keep in mind that we are looking at particularly simple examples here. More realistic applications may have more cases or explicit termination proofs, and in these cases, functional induction can lead to shorter, more maintainable proofs.
Alternating lists, the manual way
We begin with a function that picks elements from two alternating input lists:
def alternate : (xs ys : List α) → List α
 [], ys => ys
 x::xs, ys => x :: alternate ys xs
termination_by xs ys => xs.length + ys.length
It seems to be doing what it should:
#eval alternate ["red", "green", "blue", "yellow"] ["apple", "banana"]
["red", "apple", "green", "banana", "blue", "yellow"]
Now let us try to prove a simple theorem about alternate
, namely that the length of the resulting list is the sum of the argument lists' lengths.
The alternate
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 alternate
. 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 alternate
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 alternate
itself.
theorem length_alternate1 (xs ys : List α) :
(alternate xs ys).length = xs.length + ys.length := α:Type u_1xs:List αys:List α⊢ (alternate xs ys).length = xs.length + ys.length
α:Type u_1xs:List αys:List α⊢ (match xs, ys with
 [], ys => ys
 x :: xs, ys => x :: alternate ys xs).length =
xs.length + ys.length
α:Type u_1ys:List αx✝¹:List αx✝:List α⊢ ys.length = [].length + ys.lengthα:Type u_1ys:List αx✝²:List αx✝¹:List αx✝:αxs✝:List α⊢ (x✝ :: alternate ys xs✝).length = (x✝ :: xs✝).length + ys.length
next α:Type u_1ys:List αx✝¹:List αx✝:List α⊢ ys.length = [].length + ys.length All goals completed! 🐙
next x xs α:Type u_1ys:List αx✝¹:List αx✝:List αx:αxs:List α⊢ (x :: alternate ys xs).length = (x :: xs).length + ys.length
α:Type u_1ys:List αx✝¹:List αx✝:List αx:αxs:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (x :: alternate ys xs).length = (x :: xs).length + ys.length
α:Type u_1ys:List αx✝¹:List αx✝:List αx:αxs:List αih:(alternate ys xs).length = ys.length + xs.length⊢ ys.length + xs.length + 1 = xs.length + 1 + ys.length
All goals completed! 🐙
termination_by xs.length + ys.length
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:
theorem length_alternate2 : (xs ys : List α) →
(alternate xs ys).length = xs.length + ys.length
 [], ys => α:Type u_1ys:List α⊢ (alternate [] ys).length = [].length + ys.length All goals completed! 🐙
 x::xs, ys => α:Type u_1x:αxs:List αys:List α⊢ (alternate (x :: xs) ys).length = (x :: xs).length + ys.length
α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (alternate (x :: xs) ys).length = (x :: xs).length + ys.length
α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ ys.length + xs.length + 1 = xs.length + 1 + ys.length
All goals completed! 🐙
termination_by xs ys => xs.length + ys.length
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:
alternate.induct {α : Type _}
(motive : List α → List α → Prop)
(case1 : ∀ (ys : List α), motive [] ys)
(case2 : ∀ (x : α) (xs ys : List α), motive ys xs → motive (x :: xs) ys)
(xs ys : List α) :
motive xs ys
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 ofalternate
), 
and if it holds when the first list is nonempty (the minor premise
case2
, corresponding to the second branch ofalternate
), 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 inalternate
), 
then given two arbitrary lists (the targets
xs
andxy
, 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.recAux
.
With this bespoke induction principle, we can now use the induction
tactic in our proof:
theorem length_alternate3 (xs ys : List α) :
(alternate xs ys).length = xs.length + ys.length := α:Type u_1xs:List αys:List α⊢ (alternate xs ys).length = xs.length + ys.length
induction xs, ys using alternate.induct with
 case1 ys α:Type u_1ys:List α⊢ (alternate [] ys).length = [].length + ys.length All goals completed! 🐙
 case2 x xs ys ih α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (alternate (x :: xs) ys).length = (x :: xs).length + ys.length
α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ ys.length + xs.length + 1 = xs.length + 1 + ys.length
All goals completed! 🐙
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 twoline proof:
theorem length_alternate4 (xs ys : List α) :
(alternate xs ys).length = xs.length + ys.length := α:Type u_1xs:List αys:List α⊢ (alternate xs ys).length = xs.length + ys.length
α:Type u_1ys✝:List α⊢ (alternate [] ys✝).length = [].length + ys✝.lengthα:Type u_1x✝:αxs✝:List αys✝:List αih1✝:(alternate ys✝ xs✝).length = ys✝.length + xs✝.length⊢ (alternate (x✝ :: xs✝) ys✝).length = (x✝ :: xs✝).length + ys✝.length
all_goals α:Type u_1x✝:αxs✝:List αys✝:List αih1✝:(alternate ys✝ xs✝).length = ys✝.length + xs✝.length⊢ ys✝.length + xs✝.length + 1 = xs✝.length + 1 + ys✝.length; try All goals completed! 🐙
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:
theorem length_alternate5 (xs ys : List α) :
(alternate xs ys).length = xs.length + ys.length := α:Type u_1xs:List αys:List α⊢ (alternate xs ys).length = xs.length + ys.length
induction xs, ys using alternate.induct with
 case1 ys α:Type u_1ys:List α⊢ (alternate [] ys).length = [].length + ys.length calc
(alternate [] ys).length
_ = ys.length := α:Type u_1ys:List α⊢ (alternate [] ys).length = ys.length All goals completed! 🐙
_ = [].length + ys.length := α:Type u_1ys:List α⊢ ys.length = [].length + ys.length All goals completed! 🐙
 case2 x xs ys ih α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (alternate (x :: xs) ys).length = (x :: xs).length + ys.length calc
(alternate (x :: xs) ys).length
_ = (x :: alternate ys xs).length := α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (alternate (x :: xs) ys).length = (x :: alternate ys xs).length All goals completed! 🐙
_ = (alternate ys xs).length + 1 := α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (x :: alternate ys xs).length = (alternate ys xs).length + 1 All goals completed! 🐙
_ = (ys.length + xs.length) + 1 := α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ (alternate ys xs).length + 1 = ys.length + xs.length + 1 All goals completed! 🐙
_ = (x :: xs).length + ys.length := α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ ys.length + xs.length + 1 = (x :: xs).length + ys.length α:Type u_1x:αxs:List αys:List αih:(alternate ys xs).length = ys.length + xs.length⊢ ys.length + xs.length + 1 = xs.length + 1 + ys.length; All goals completed! 🐙
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
:
def cutN (n : Nat) : (xs : List α) → List (List α)
 [] => []
 x::xs => (x::xs.take (n1)) :: cutN n (xs.drop (n1))
termination_by xs => xs.length
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:
#eval cutN 3 ["😏", "😄", "😊", "😎", "😍", "😘", "🥰", "😃", "😉", "😋", "😆"]
[["😏", "😄", "😊"], ["😎", "😍", "😘"], ["🥰", "😃", "😉"], ["😋", "😆"]]
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
:
theorem cutNJoin1 (n : Nat) (xs : List α) : List.join (cutN n xs) = xs := α:Type u_1n:Natxs:List α⊢ (cutN n xs).join = xs
α:Type u_1n:Nat⊢ Natα:Type u_1n:Nat⊢ (cutN n []).join = []α:Type u_1n:Natx✝:αxs✝:List αih1✝:(cutN n (List.drop (?n  1) xs✝)).join = List.drop (?n  1) xs✝⊢ (cutN n (x✝ :: xs✝)).join = x✝ :: xs✝
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:
cutN.induct {α : Type _} (n : Nat)
(motive : List α → Prop)
(case1 : motive [])
(case2 : ∀ (x : α) (xs : List α), motive (List.drop (n  1) xs) → motive (x :: xs))
(xs : List α) :
motive xs
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:
theorem cutNJoin2 (n : Nat) (xs : List α) : List.join (cutN n xs) = xs := α:Type u_1n:Natxs:List α⊢ (cutN n xs).join = xs
α:Type u_1n:Nat⊢ (cutN n []).join = []α:Type u_1n:Natx✝:αxs✝:List αih1✝:(cutN n (List.drop (n  1) xs✝)).join = List.drop (n  1) xs✝⊢ (cutN n (x✝ :: xs✝)).join = x✝ :: xs✝ α:Type u_1n:Nat⊢ (cutN n []).join = []α:Type u_1n:Natx✝:αxs✝:List αih1✝:(cutN n (List.drop (n  1) xs✝)).join = List.drop (n  1) xs✝⊢ (cutN n (x✝ :: xs✝)).join = x✝ :: xs✝ All goals completed! 🐙
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 nonoverlapping 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:
def destutter : (xs : List Bool) → List Bool
 [] => []
 true :: true :: xs => destutter (true :: xs)
 false :: false :: xs => destutter (false :: xs)
 x :: xs => x :: destutter xs
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
:
destutter.eq_3 (xs : List Bool) :
destutter (false :: false :: xs) = destutter (false :: xs)
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:
destutter.eq_4 (x_1 : Bool) (xs : List Bool)
(x_2 : ∀ (xs_1 : List Bool), x_1 = true → xs = true :: xs_1 → False)
(x_3 : ∀ (xs_1 : List Bool), x_1 = false → xs = false :: xs_1 → False) :
destutter (x_1 :: xs) = x_1 :: destutter xs
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:
theorem length_destutter : (xs : List Bool) → (destutter xs).length ≤ xs.length
 [] => ⊢ (destutter []).length ≤ [].length All goals completed! 🐙
 true :: true :: xs => xs:List Bool⊢ (destutter (true :: true :: xs)).length ≤ (true :: true :: xs).length
xs:List Boolthis:(destutter (true :: xs)).length ≤ (true :: xs).length⊢ (destutter (true :: true :: xs)).length ≤ (true :: true :: xs).length; xs:List Boolthis:(destutter (true :: xs)).length ≤ xs.length + 1⊢ (destutter (true :: xs)).length ≤ xs.length + 1 + 1; All goals completed! 🐙
 false :: false :: xs => xs:List Bool⊢ (destutter (false :: false :: xs)).length ≤ (false :: false :: xs).length
xs:List Boolthis:(destutter (false :: xs)).length ≤ (false :: xs).length⊢ (destutter (false :: false :: xs)).length ≤ (false :: false :: xs).length; xs:List Boolthis:(destutter (false :: xs)).length ≤ xs.length + 1⊢ (destutter (false :: xs)).length ≤ xs.length + 1 + 1; All goals completed! 🐙
 x :: xs => x:Boolxs:List Bool⊢ (destutter (x :: xs)).length ≤ (x :: xs).length
x:Boolxs:List Bool⊢ (destutter (x :: xs)).length ≤ (x :: xs).length  simp made no progress
In the last case of the match, Lean does not know that the previous cases did not apply, so it cannot use destutter.eq_4
and thus cannot simplify the goal.
One way out is to resort to the unfold destutter; split
idiom. Functional induction also covers this case. The induction theorem produced by Lean provides the assumptions needed by the equational theorem in the appropriate case:
destutter.induct
(motive : List Bool → Prop)
(case1 : motive [])
(case2 : ∀ (xs : List Bool), motive (true :: xs) → motive (true :: true :: xs))
(case3 : ∀ (xs : List Bool), motive (false :: xs) → motive (false :: false :: xs))
(case4 :
∀ (x : Bool) (xs : List Bool),
(∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → False) →
(∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → False) →
motive xs →
motive (x :: xs))
(xs : List Bool) :
motive xs
With these assumptions in the context, simp
makes progress, and the proof becomes quite short:
theorem length_destutter2 : (destutter xs).length ≤ xs.length := xs:List Bool⊢ (destutter xs).length ≤ xs.length
⊢ (destutter []).length ≤ [].lengthxs✝:List Boolih1✝:(destutter (true :: xs✝)).length ≤ (true :: xs✝).length⊢ (destutter (true :: true :: xs✝)).length ≤ (true :: true :: xs✝).lengthxs✝:List Boolih1✝:(destutter (false :: xs✝)).length ≤ (false :: xs✝).length⊢ (destutter (false :: false :: xs✝)).length ≤ (false :: false :: xs✝).lengthx✝²:Boolxs✝:List Boolx✝¹:∀ (xs_1 : List Bool), x✝² = true → xs✝ = true :: xs_1 → Falsex✝:∀ (xs_1 : List Bool), x✝² = false → xs✝ = false :: xs_1 → Falseih1✝:(destutter xs✝).length ≤ xs✝.length⊢ (destutter (x✝² :: xs✝)).length ≤ (x✝² :: xs✝).length ⊢ (destutter []).length ≤ [].lengthxs✝:List Boolih1✝:(destutter (true :: xs✝)).length ≤ (true :: xs✝).length⊢ (destutter (true :: true :: xs✝)).length ≤ (true :: true :: xs✝).lengthxs✝:List Boolih1✝:(destutter (false :: xs✝)).length ≤ (false :: xs✝).length⊢ (destutter (false :: false :: xs✝)).length ≤ (false :: false :: xs✝).lengthx✝²:Boolxs✝:List Boolx✝¹:∀ (xs_1 : List Bool), x✝² = true → xs✝ = true :: xs_1 → Falsex✝:∀ (xs_1 : List Bool), x✝² = false → xs✝ = false :: xs_1 → Falseih1✝:(destutter xs✝).length ≤ xs✝.length⊢ (destutter (x✝² :: xs✝)).length ≤ (x✝² :: xs✝).length
x✝²:Boolxs✝:List Boolih1✝:(destutter xs✝).length ≤ xs✝.lengthx✝¹:∀ (xs_1 : List Bool), x✝² = true → ¬xs✝ = true :: xs_1x✝:∀ (xs_1 : List Bool), x✝² = false → ¬xs✝ = false :: xs_1⊢ (destutter xs✝).length ≤ xs✝.length xs✝:List Boolih1✝:(destutter (true :: xs✝)).length ≤ xs✝.length + 1⊢ (destutter (true :: xs✝)).length ≤ xs✝.length + 1 + 1xs✝:List Boolih1✝:(destutter (false :: xs✝)).length ≤ xs✝.length + 1⊢ (destutter (false :: xs✝)).length ≤ xs✝.length + 1 + 1x✝²:Boolxs✝:List Boolih1✝:(destutter xs✝).length ≤ xs✝.lengthx✝¹:∀ (xs_1 : List Bool), x✝² = true → ¬xs✝ = true :: xs_1x✝:∀ (xs_1 : List Bool), x✝² = false → ¬xs✝ = false :: xs_1⊢ (destutter xs✝).length ≤ xs✝.length All goals completed! 🐙
You might be surprised that simp [destutter]
suffices here, and we did not have to explicitly write simp [destutter, *]
to tell simp
that it should also use facts in the local context. This is due to special handling in simp
: if rewrite rules have premises that look like like the premise of a function’s equational lemma, simp
will consult the local context anyways.
This special handling does not exist in rewrite
and rw
, so if we use these tactics to unfold the function, we will get new goals with these side conditions, and have to resolve them explicitly, for example using assumption
.
Mutual recursion
Proofs about mutually defined functions can become quite tricky: following the rule that the proof should follow the structure of the function, the usual approach is to prove two mutually recursive theorems, replicating the case splits of the original functions by matching or using split
. Again, functional induction can help us avoid this repetition.
We will use a minimal example of mutually defined functions, even
and odd
:
mutual
def even : (n : Nat) → Bool
 0 => true
 n+1 => odd n
def odd : (n : Nat) → Bool
 0 => false
 n+1 => even n
end
The functional induction principle generated for one of these functions looks as follows:
even.induct
(motive1 motive2 : Nat → Prop)
(case1 : motive1 0)
(case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
(case3 : motive2 0)
(case4 : ∀ (n : Nat), motive1 n → motive2 n.succ)
(n : Nat) :
motive1 n
This theorem now has two motives, one for each function in the recursive group, and four cases, corresponding to the two cases of even
and then two cases of odd
.
Recall that the role of the motive is to specify the statement that we want to prove about the parameters of the recursive function. If we have two mutually recursive functions, we typically have two such statements in mind that we want to prove together, one for each of the two functions.
One of the main benefits of the induction
tactic, over simply trying to apply
an induction principle, is that the induction
tactic constructs the motive
from the current proof goal. If the proof goal is P x y
then induction x, y
sets (motive := fun x y => P x y)
. (There is a bit more to it when there are assumptions about x
or y
in the local context, or the generalizing
clause is used.)
So if the induction principle expects multiple motives, only of them can be inferred from the goal, and we will have to instantiate the other motive explicitly. So to prove that all numbers of the form 2n
are even
, were we want to use that all numbers of the form 2n + 1
are odd
, we can write:
theorem evenDouble (n : Nat) : even (2 * n) := n:Nat⊢ even (2 * n) = true
⊢ even (2 * 0) = truen✝:Natih1✝:odd (2 * n✝ + 1) = true⊢ even (2 * n✝.succ) = true⊢ odd (2 * 0 + 1) = truen✝:Natih1✝:even (2 * n✝) = true⊢ odd (2 * n✝.succ + 1) = true ⊢ even (2 * 0) = truen✝:Natih1✝:odd (2 * n✝ + 1) = true⊢ even (2 * n✝.succ) = true⊢ odd (2 * 0 + 1) = truen✝:Natih1✝:even (2 * n✝) = true⊢ odd (2 * n✝.succ + 1) = true
All goals completed! 🐙
We can of course also prove the statement about odd
. Now the induction
tactic infers motive2
and we have to give motive1
explicitly:
theorem oddDouble (n : Nat) : odd (2 * n + 1) := n:Nat⊢ odd (2 * n + 1) = true
⊢ even (2 * 0) = truen✝:Natih1✝:odd (2 * n✝ + 1) = true⊢ even (2 * n✝.succ) = true⊢ odd (2 * 0 + 1) = truen✝:Natih1✝:even (2 * n✝) = true⊢ odd (2 * n✝.succ + 1) = true ⊢ even (2 * 0) = truen✝:Natih1✝:odd (2 * n✝ + 1) = true⊢ even (2 * n✝.succ) = true⊢ odd (2 * 0 + 1) = truen✝:Natih1✝:even (2 * n✝) = true⊢ odd (2 * n✝.succ + 1) = true
All goals completed! 🐙
If you compare even.induct
and odd.induct
, or inspect the proof state after induction
, you will notice that we get the same proof obligations in both proofs, and we had to perform the same proofs twice to get both theorems. In the example above, where the proofs are rather trivial, this is not so bad, but in general we would be quite unsatisfied by that repetition. In that case, we can use the mutual functional induction principle:
even.mutual_induct
(motive1 motive2 : Nat → Prop)
(case1 : motive1 0)
(case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
(case3 : motive2 0)
(case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) :
(∀ (n : Nat), motive1 n) ∧ (∀ (n : Nat), motive2 n)
This induction principle proves both motive1
and motive2
. Unfortunately, this kind of induction principle can no longer be used
by induction
, so we have to manually prepare the goal to be of the right shape to be able to apply
the theorem, essentially constructing both motives manually, and then project out the components:
theorem evenDouble_oddDouble :
((n : Nat) → even (2 * n)) ∧ ((n : Nat) → odd (2 * n + 1)) := ⊢ (∀ (n : Nat), even (2 * n) = true) ∧ ∀ (n : Nat), odd (2 * n + 1) = true
⊢ even (2 * 0) = true⊢ ∀ (n : Nat), odd (2 * n + 1) = true → even (2 * n.succ) = true⊢ odd (2 * 0 + 1) = true⊢ ∀ (n : Nat), even (2 * n) = true → odd (2 * n.succ + 1) = true ⊢ even (2 * 0) = true⊢ ∀ (n : Nat), odd (2 * n + 1) = true → even (2 * n.succ) = true⊢ odd (2 * 0 + 1) = true⊢ ∀ (n : Nat), even (2 * n) = true → odd (2 * n.succ + 1) = true All goals completed! 🐙
theorem evenDouble2 : (n : Nat) → even (2 * n) := evenDouble_oddDouble.1
theorem oddDouble2 : (n : Nat) → odd (2 * n + 1) := evenDouble_oddDouble.2
We plan to provide commands to perform such a joint declaration of two theorems with less repetition and more convenience in the future.
Unrelated to mutual induction, but worth pointing out at this point: in this section we were able to solve all subgoals using simp_all [even, odd]
. This high level of automation means that our proofs are quite stable under changes to the function definitions, and indeed, if we changed the definition of odd
in
mutual
def even : (n : Nat) → Bool
 0 => true
 n+1 => odd n
def odd (n : Nat) : Bool := !(even n)
end
all of our proofs still go through, even though the number and shape of the cases changed!
What is a branch?
When Lean defines the functional induction principle, it has to decide what constitutes a branch of the function, and should therefore become a case of the induction principle. This is necessarily a heuristic, and is guided by the notion of tail position: Lean splits match statements and ifthenelse
statements that occur in the body of the function or in a case of such statements, but not when they appear, for example, in arguments to functions.
As a slight variant of cutN
, consider a function that inserts a separator before, between and after groups of n
:
#eval sepWith 3 (⊢ 0 < 3 All goals completed! 🐙) "🐕" ["😏", "😄", "😊", "😎", "😍", "😘", "🥰", "😃", "😉", "😋", "😆"]
["🐕", "😏", "😄", "😊", "🐕", "😎", "😍", "😘", "🐕", "🥰", "😃", "😉", "🐕", "😋", "😆", "🐕"]
Instead of using pattern matching as with cutN
, let us try to use ifthenelse
:
def sepWith (n : Nat) (hpos : 0 < n) (sep : α) (xs : List α) : List α :=
if xs.length = 0 then [sep]
else [sep] ++ xs.take n ++ sepWith n hpos sep (xs.drop n)
termination_by xs.length
Because we use ifthenelse
in a tail position the induction principle has two goals, one for each of the two branches:
sepWith.induct {α : Type _} (n : Nat) (hpos : 0 < n) (sep : α)
(motive : List α → Prop)
(case1 : ∀ (x : List α), x.length = 0 → motive x)
(case2 : ∀ (x : List α), ¬x.length = 0 → motive (List.drop n x) → motive x)
(xs : List α) :
motive xs
We could also have defined the function slightly differently, moving the ifthenelse
into the (sep :: ·)
, as follows:
def sepWith2 (n : Nat) (hpos : 0 < n) (sep : α) (xs : List α) : List α :=
sep :: (if xs.length = 0 then []
else xs.take n ++ sepWith2 n hpos sep (xs.drop n))
termination_by xs.length
Now we get an induction principle with just one case:
sepWith2.induct {α : Type _} (n : Nat) (hpos : 0 < n) (sep : α)
(motive : List α → Prop)
(case1 : ∀ (x : List α), (¬x.length = 0 → motive (List.drop n x)) → motive x)
(xs : List α) :
motive xs
Also note that the induction hypothesis in this case now has a condition ¬x.length = 0
. This is to be expected: The corresponding recursive call is in the else
branch, and if x.length = 0
we may not assume that the induction hypothesis holds.
Hurdle: Looping simp
At this point we should discuss an issue with simp
and certain recursive function definitions that can lead to simp [foo]
looping. This is relevant because unfolding the function’s definition with simp
is often the first thing we do in the case of a functional induction.
Consider the following proof that relates sepWith
and cutN
theorem sepWith_cutN :
sepWith n hpos sep xs = (cutN n xs >.map (sep :: ·) >.join) ++ [sep] := n:Nathpos:0 < nα✝:Type u_1sep:α✝xs:List α✝⊢ sepWith n hpos sep xs = (List.map (fun x => sep :: x) (cutN n xs)).join ++ [sep]
n:Nathpos:0 < nα✝:Type u_1sep:α✝⊢ sepWith n hpos sep [] = (List.map (fun x => sep :: x) (cutN n [])).join ++ [sep]n:Nathpos:0 < nα✝:Type u_1sep:α✝x✝:α✝xs✝:List α✝ih1✝:sepWith n hpos sep (List.drop (n  1) xs✝) =
(List.map (fun x => sep :: x) (cutN n (List.drop (n  1) xs✝))).join ++ [sep]⊢ sepWith n hpos sep (x✝ :: xs✝) = (List.map (fun x => sep :: x) (cutN n (x✝ :: xs✝))).join ++ [sep]
case case1 n:Nathpos:0 < nα✝:Type u_1sep:α✝⊢ sepWith n hpos sep [] = (List.map (fun x => sep :: x) (cutN n [])).join ++ [sep] All goals completed! 🐙
case case2 x xs ih n:Nathpos:0 < nα✝:Type u_1sep:α✝x:α✝xs:List α✝ih:sepWith n hpos sep (List.drop (n  1) xs) = (List.map (fun x => sep :: x) (cutN n (List.drop (n  1) xs))).join ++ [sep]⊢ sepWith n hpos sep (x :: xs) = (List.map (fun x => sep :: x) (cutN n (x :: xs))).join ++ [sep]
n✝:Natα✝:Type u_1sep:α✝x:α✝xs:List α✝n:Nathpos:0 < n + 1ih:sepWith (n + 1) hpos sep (List.drop (n + 1  1) xs) =
(List.map (fun x => sep :: x) (cutN (n + 1) (List.drop (n + 1  1) xs))).join ++ [sep]⊢ sepWith (n + 1) hpos sep (x :: xs) = (List.map (fun x => sep :: x) (cutN (n + 1) (x :: xs))).join ++ [sep]  uses `hpos` to destruct n
n✝:Natα✝:Type u_1sep:α✝x:α✝xs:List α✝n:Nathpos:0 < n + 1ih:sepWith (n + 1) hpos sep (List.drop (n + 1  1) xs) =
(List.map (fun x => sep :: x) (cutN (n + 1) (List.drop (n + 1  1) xs))).join ++ [sep]⊢ (if (x :: xs).length = 0 then [sep]
else [sep] ++ List.take (n + 1) (x :: xs) ++ sepWith (n + 1) hpos sep (List.drop (n + 1) (x :: xs))) =
(List.map (fun x => sep :: x) (cutN (n + 1) (x :: xs))).join ++ [sep]; All goals completed! 🐙
We have two recursive functions, each with their own induction principle. We chose to use cutN
's induction principle, because those generated from pattern matching tend to be easier to work with than those generated from ifthenelse
, and indeed we can conclude the proof.
You might wonder why we wrote
rw [sepWith]; simp_all [cutN, List.join_cons]
and not
simp_all [sepWith, cutN, List.join_cons]
The latter would lead to an error:
tactic 'simp' failed, nested error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
The problem is that the equational theorem generated for sepWith
matches any call to sepWith
, including the one on its own right hand side, and that sends simp
into a loop:
sepWith2.eq_1 {α : Type _} (n : Nat) (hpos : 0 < n) (sep : α) (xs : List α) :
sepWith2 n hpos sep xs =
sep :: if xs.length = 0
then []
else List.take n xs ++ sepWith2 n hpos sep (List.drop n xs)
The solution is to unfold such functions more carefully using rw
(or possibly unfold
). We hope that we can improve Lean's behaviour in this regard in the future.
Hurdle: Complex parameters
We saw that when a function like unstutter
is defined with overlapping patterns, its equational theorems have preconditions, such as
destutter.eq_4 (x_1 : Bool) (xs : List Bool)
(x_2 : ∀ (xs_1 : List Bool), x_1 = true → xs = true :: xs_1 → False)
(x_3 : ∀ (xs_1 : List Bool), x_1 = false → xs = false :: xs_1 → False) :
destutter (x_1 :: xs) = x_1 :: destutter xs
These sideconditions are sometimes hard for simp
to discharge. Consider the following theorem that says that destutter
commutes with List.map not
. This is obviously true, and we'd hope that the straightforward proof
theorem map_not_destutter :
List.map not (destutter xs) = destutter (List.map not xs) := xs:List Bool⊢ List.map not (destutter xs) = destutter (List.map not xs)
⊢ List.map not (destutter []) = destutter (List.map not [])xs✝:List Boolih1✝:List.map not (destutter (true :: xs✝)) = destutter (List.map not (true :: xs✝))⊢ List.map not (destutter (true :: true :: xs✝)) = destutter (List.map not (true :: true :: xs✝))xs✝:List Boolih1✝:List.map not (destutter (false :: xs✝)) = destutter (List.map not (false :: xs✝))⊢ List.map not (destutter (false :: false :: xs✝)) = destutter (List.map not (false :: false :: xs✝))x✝²:Boolxs✝:List Boolx✝¹:∀ (xs_1 : List Bool), x✝² = true → xs✝ = true :: xs_1 → Falsex✝:∀ (xs_1 : List Bool), x✝² = false → xs✝ = false :: xs_1 → Falseih1✝:List.map not (destutter xs✝) = destutter (List.map not xs✝)⊢ List.map not (destutter (x✝² :: xs✝)) = destutter (List.map not (x✝² :: xs✝)) ⊢ List.map not (destutter []) = destutter (List.map not [])xs✝:List Boolih1✝:List.map not (destutter (true :: xs✝)) = destutter (List.map not (true :: xs✝))⊢ List.map not (destutter (true :: true :: xs✝)) = destutter (List.map not (true :: true :: xs✝))xs✝:List Boolih1✝:List.map not (destutter (false :: xs✝)) = destutter (List.map not (false :: xs✝))⊢ List.map not (destutter (false :: false :: xs✝)) = destutter (List.map not (false :: false :: xs✝))x✝²:Boolxs✝:List Boolx✝¹:∀ (xs_1 : List Bool), x✝² = true → xs✝ = true :: xs_1 → Falsex✝:∀ (xs_1 : List Bool), x✝² = false → xs✝ = false :: xs_1 → Falseih1✝:List.map not (destutter xs✝) = destutter (List.map not xs✝)⊢ List.map not (destutter (x✝² :: xs✝)) = destutter (List.map not (x✝² :: xs✝))
x✝²:Boolxs✝:List Boolx✝¹:∀ (xs_1 : List Bool), x✝² = true → xs✝ = true :: xs_1 → Falsex✝:∀ (xs_1 : List Bool), x✝² = false → xs✝ = false :: xs_1 → Falseih1✝:List.map not (destutter xs✝) = destutter (List.map not xs✝)⊢ (!x✝²) :: destutter (List.map not xs✝) = destutter ((!x✝²) :: List.map not xs✝)
All goals completed! 🐙
would work, but it fails with
unsolved goals case case4 x✝² : Bool xs✝ : List Bool x✝¹ : ∀ (xs_1 : List Bool), x✝² = true → xs✝ = true :: xs_1 → False x✝ : ∀ (xs_1 : List Bool), x✝² = false → xs✝ = false :: xs_1 → False ih1✝ : List.map not (destutter xs✝) = destutter (List.map not xs✝) ⊢ (!x✝²) :: destutter (List.map not xs✝) = destutter ((!x✝²) :: List.map not xs✝)
It is stuck in the fourth case, and we can see that the destutter
call on the left hand side has
been simplified, but not the one on the righthand side. The simplifier is not able to prove the
preconditions of destutter.eq_4
for the arguments !x✝²
and List.map not xs✝
from the information present in the goal. More powerful proof automation might handle that in the future, but for now we have to work around this issue.
One solution is to use rw
to apply the equational theorem and manually discharge the sideconditions:
theorem map_not_destutter2 :
List.map not (destutter xs) = destutter (List.map not xs) := xs:List Bool⊢ List.map not (destutter xs) = destutter (List.map not xs)
induction xs using destutter.induct with
 case1  case2  case3 xs✝:List Boolih1✝:List.map not (destutter (false :: xs✝)) = destutter (List.map not (false :: xs✝))⊢ List.map not (destutter (false :: false :: xs✝)) = destutter (List.map not (false :: false :: xs✝)) All goals completed! 🐙
 case4 x xs h1 h2 ih x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ List.map not (destutter (x :: xs)) = destutter (List.map not (x :: xs))
x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ (!x) :: List.map not (destutter xs) = destutter ((!x) :: List.map not xs)
x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ (!x) :: List.map not (destutter xs) = (!x) :: destutter (List.map not xs)x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not xs = true :: xs_1 → Falsex:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not xs = false :: xs_1 → False; x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not xs = true :: xs_1 → Falsex:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not xs = false :: xs_1 → Falsex:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ (!x) :: List.map not (destutter xs) = (!x) :: destutter (List.map not xs)
x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not xs = true :: xs_1 → False x:Boolh1:∀ (xs_1 : List Bool), x = true → [] = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → [] = false :: xs_1 → Falseih:List.map not (destutter []) = destutter (List.map not [])⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not [] = true :: xs_1 → Falsex:Boolhead✝:Booltail✝:List Boolh1:∀ (xs_1 : List Bool), x = true → head✝ :: tail✝ = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → head✝ :: tail✝ = false :: xs_1 → Falseih:List.map not (destutter (head✝ :: tail✝)) = destutter (List.map not (head✝ :: tail✝))⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not (head✝ :: tail✝) = true :: xs_1 → False x:Boolh1:∀ (xs_1 : List Bool), x = true → [] = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → [] = false :: xs_1 → Falseih:List.map not (destutter []) = destutter (List.map not [])⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not [] = true :: xs_1 → Falsex:Boolhead✝:Booltail✝:List Boolh1:∀ (xs_1 : List Bool), x = true → head✝ :: tail✝ = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → head✝ :: tail✝ = false :: xs_1 → Falseih:List.map not (destutter (head✝ :: tail✝)) = destutter (List.map not (head✝ :: tail✝))⊢ ∀ (xs_1 : List Bool), (!x) = true → List.map not (head✝ :: tail✝) = true :: xs_1 → False All goals completed! 🐙
x:Boolxs:List Boolh1:∀ (xs_1 : List Bool), x = true → xs = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → xs = false :: xs_1 → Falseih:List.map not (destutter xs) = destutter (List.map not xs)⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not xs = false :: xs_1 → False x:Boolh1:∀ (xs_1 : List Bool), x = true → [] = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → [] = false :: xs_1 → Falseih:List.map not (destutter []) = destutter (List.map not [])⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not [] = false :: xs_1 → Falsex:Boolhead✝:Booltail✝:List Boolh1:∀ (xs_1 : List Bool), x = true → head✝ :: tail✝ = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → head✝ :: tail✝ = false :: xs_1 → Falseih:List.map not (destutter (head✝ :: tail✝)) = destutter (List.map not (head✝ :: tail✝))⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not (head✝ :: tail✝) = false :: xs_1 → False x:Boolh1:∀ (xs_1 : List Bool), x = true → [] = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → [] = false :: xs_1 → Falseih:List.map not (destutter []) = destutter (List.map not [])⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not [] = false :: xs_1 → Falsex:Boolhead✝:Booltail✝:List Boolh1:∀ (xs_1 : List Bool), x = true → head✝ :: tail✝ = true :: xs_1 → Falseh2:∀ (xs_1 : List Bool), x = false → head✝ :: tail✝ = false :: xs_1 → Falseih:List.map not (destutter (head✝ :: tail✝)) = destutter (List.map not (head✝ :: tail✝))⊢ ∀ (xs_1 : List Bool), (!x) = false → List.map not (head✝ :: tail✝) = false :: xs_1 → False All goals completed! 🐙
All goals completed! 🐙
We are using rotate_left
here to put the two sideconditions generated by rw
first. This way we can discharge them first, and continue with the original goal afterwards.
Another solution is to write a recursive theorem, manually expanding the proof into all nonoverlapping cases. If this does not require too many cases, and all or most cases can be handled by the same proof, then this can also work well (note how pattern matching allows multiple patterns to share one righthand side):
theorem map_not_destutter3 : (xs : List Bool) →
List.map not (destutter xs) = destutter (List.map not xs)
 []  [_]
 true :: true :: _  true :: false :: _
 false :: true :: _  false :: false :: _
=> tail✝:List Bool⊢ List.map not (destutter (false :: false :: tail✝)) = destutter (List.map not (false :: false :: tail✝)) All goals completed! 🐙
Outlook
There are further improvements on our road map or our mind. A dedicated functional induction
tactic could help with identifying parameters, separating them from targets, and maybe do careful unfolding of the function in question. We already mentioned the need for a more convenient way to use the mutual induction principle.
Some function definitions lead to equations that are not easy to use with simp
. Overlapping patterns can lead to side conditions that make rewriting too hard, whereas in other cases the equations apply too easily and can cause simp
to loop. We expect that improved proof automation in general helps with the former, and more cleverness or more user control for simp
with the latter.
Conclusion
Proofs about recursive functions with interesting branching and/or termination patterns are often simpler to create, easier to automate and more robust against changes when they use the corresponding functional induction principle, which can even handle handle mutual and nested recursion and overlapping patterns.
Functional induction principles are not a novel idea. While implementing them, I drew inspiration in particular from Isabelle's function
package and Coq's FunInd
library..