Function types in general do not have a well-founded relation that's useful for termination proofs. Instance synthesis thus selects instSizeOfDefault and the corresponding well-founded relation. If the measure is a function, the default SizeOf instance is selected and the proof cannot succeed.

The following recursive definition of the Fibonacci numbers has two recursive calls, which results in two goals in the termination proof.

Here, the measure is simply the parameter itself, and the well-founded order is the less-than relation on natural numbers. The first proof goal requires the user to prove that the argument of the first recursive call, namely n - 1, is strictly smaller than the function's parameter, n.

Both termination proofs can be easily discharged using the omega tactic.

If a parameter of the function is the discriminant of a pattern match, then the proof obligations mention the refined parameter.

Here, the termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if does not add a local assumption about the condition (that is, whether n ≤ 1) to the local contexts in the branches.

Nevertheless, the assumptions are available in the context of the termination proof:

Termination proof obligations in body of a Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass. for​…​Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass. in loop are also enriched, in this case with a Std.Range membership hypothesis:

Similarly, in the following (contrived) example, the termination proof contains an additional assumption showing that x ∈ xs.

This feature requires special setup for the higher-order function under which the recursive call is nested, as described in the section on preprocessing. In the following definition, identical to the one above except using a custom, equivalent function instead of List.map, the proof obligation context is not enriched:

A classic example of a recursive function that needs a more complex measure is the Ackermann function:

The measure is a tuple, so every recursive call has to be on arguments that are lexicographically smaller than the parameters. The default decreasing_tactic can handle this.

In particular, note that the third recursive call has a second argument that is smaller than the second parameter and a first argument that is definitionally equal to the first parameter. This allowed decreasing_tactic to apply Prod.Lex.right.

It fails, however, with the following modified function definition, where the third recursive call's first argument is provably smaller or equal to the first parameter, but not syntactically equal:

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
case h
m n : Nat
⊢ m / 2 + 1 < m + 1

Because Prod.Lex.right is not applicable, the tactic used Prod.Lex.left, which resulted in the unprovable goal above.

This function definition may require a manual proof that uses the more general theorem Prod.Lex.right', which allows the first component of the tuple (which must be of type Nat) to be less or equal instead of strictly equal:

The decreasing_tactic tactic does not use the stronger Prod.Lex.right' because it would require backtracking on failure.

If there is no Lean.Parser.Command.declaration : commandtermination_by clause, Lean attempts to infer a measure for well-founded recursion. If it fails, then it prints the table mentioned above. In this example, the Lean.Parser.Command.declaration : commanddecreasing_by clause simply prevents Lean from also attempting structural recursion; this keeps the error message specific.

Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
           n m l
1) 30:6-25 = = =
2) 31:6-23 = < _
3) 32:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.

The three recursive calls are identified by their source positions. This message conveys the following facts:

• In the first recursive call, all arguments are (provably) equal to the parameters

• In the second recursive call, the first argument is equal to the first parameter and the second argument is provably smaller than the second parameter. The third parameter was not checked for this recursive call, because it was not necessary to determine that no suitable termination argument exists.

• In the third recursive call, the first argument decreases strictly, and the other arguments were not checked.

When termination proofs fail in this manner, a good technique to discover the problem is to explicitly indicate the expected termination argument using Lean.Parser.Command.declaration : commandtermination_by. This will surface the messages from the failing tactic.

The purpose of considering expressions of the form e₂ - e₁ as measures is to support the common idiom of counting up to some upper bound, in particular when traversing arrays in possibly interesting ways. In the following function, which performs binary search on a sorted array, this heuristic helps Lean to find the j - i measure.

The fact that the inferred termination argument uses some arbitrary measure, rather than an optimal or minimal one, is visible in the inferred measure, which contains a redundant j:

Try this: termination_by (j, j - i)

The tactic indicated by Lean.Parser.Command.declaration : commanddecreasing_by is used slightly differently when inferring the termination measure than it is in the actual termination proof.

• During inference, it is applied to a single goal, attempting to prove < or ≤ on Nat.

• During the termination proof, it is applied to many simultaneous goals (one per recursive call), and the goals may involve the lexicographic ordering of pairs.

A consequence is that a Lean.Parser.Command.declaration : commanddecreasing_by block that addresses goals individually and which works successfully with an explicit termination argument can cause inference of the termination measure to fail:

It is advisable to always include a Lean.Parser.Command.declaration : commandtermination_by clause whenever an explicit Lean.Parser.Command.declaration : commanddecreasing_by proof is given.

Because decreasing_tactic avoids the need to backtrack by being incomplete with regard to lexicographic ordering, Lean may infer a termination measure that leads to goals that the tactic cannot prove. In this case, the error message is the one that results from the failing tactic rather than the one that results from being unable to find a measure. This is what happens in notAck:

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
case h
m n : Nat
⊢ m / 2 + 1 < m + 1

In this case, explicitly stating the termination measure helps.

In the following mutual function definitions, the parameter does not decrease in the call from g to f. Nonetheless, the definition is accepted due to the ordering imposed on the functions themselves by the additional basic measure.

The inferred termination argument for f is:

Try this: termination_by n => (n, 0)

The inferred termination argument for g is:

Try this: termination_by (n, 1)

This example demonstrates what is necessary to enable automatic well-founded recursion for a custom container type. The structure type Pair is a homogeneous pair: it contains precisely two elements, both of which have the same type. It can be thought of as being similar to a list or array that always contains precisely two elements.

As a container, Pair can support a map operation. To support well-founded recursion in which recursive calls occur in the body of a function being mapped over a Pair, some additional definitions are required, including a membership predicate, a theorem that relates the size of a member to the size of the containing pair, helpers to introduce and eliminate assumptions about membership, wf_preprocess rules to insert these helpers, and an extension to the decreasing_trivial tactic. Each of these steps makes it easier to work with Pair, but none are strictly necessary; there's no need to immediately implement all steps for every type.

Defining a nested inductive data type of binary trees that uses Pair and attempting to define its map function demonstrates the need for preprocessing rules.

A straightforward definition of the map function fails:

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 u_1
p : Pair (Tree α)
t' : Tree α
⊢ sizeOf t' < 1 + sizeOf p

The standard idiom to enable this kind of function definition is to have a function that enriches each element of a collection with a proof that they are, in fact, elements of the collection. Stating this property requires a membership predicate.

Every inductive type automatically has a SizeOf instance. An element of a collection should be smaller than the collection, but this fact must be proved before it can be used to construct a termination proof:

The next step is to define attach and unattach functions that enrich the elements of the pair with a proof that they are elements of the pair, or remove said proof. Here, the type of Pair.unattach is more general and can be used with any subtype; this is a typical pattern.

Tree.map can now be defined by using Pair.attach and Pair.sizeOf_lt_of_mem explicitly:

This transformation can be made fully automatic. The preprocessing feature of well-founded recursion can be used to automate the introduction of the Pair.attach function. This is done in two stages. First, when Pair.map is applied to one of the function's parameters, it is rewritten to an attach/unattach composition. Then, when a function is mapped over the result of Pair.unattach, the function is rewritten to accept the proof of membership and bring it into scope.

Now the function body can be written without extra considerations, and the membership assumption is still available to the termination proof.

The proof can be made fully automatic by adding sizeOf_lt_of_mem to the decreasing_trivial tactic, as is done for similar built-in theorems.

To keep the example short, the sizeOf_pair_dec tactic is tailored to this particular recursion pattern and isn't really general enough for a general-purpose container library. It does, however, demonstrate that libraries can be just as convenient in practice as the container types in the standard library.

The definition of division by iterated subtraction can be written explicitly using well-founded recursion.

The definition must be marked Lean.Parser.Command.declaration : commandnoncomputable because well-founded recursion is not supported by the compiler. Like recursors, it is part of Lean's logic.

The definition of division should satisfy the following equations:

• ∀{n k : Nat}, (k = 0) → div n k = 0

• ∀{n k : Nat}, (k > n) → div n k = 0

• ∀{n k : Nat}, (k ≠ 0) → (¬ k > n) → div n k = div (n - k) k

This reduction behavior does not hold definitionally:

tactic 'rfl' failed, the left-hand side
  div n 0
is not definitionally equal to the right-hand side
  0
n : Nat
⊢ div n 0 = 0

However, using WellFounded.fix_eq to unfold the well-founded recursion, the three equations can be proved to hold: