When the decreasing parameter is a named parameter to the function, it can be specified by referring to its name.

When the decreasing parameter is not named in the signature, a name can be introduced locally in the Lean.Parser.Command.declaration : commandtermination_by clause.

The decreasing parameter's type must be an inductive type. In notInductive, a function is specified as the decreasing parameter:

cannot use specified measure for structural recursion:
  its type is not an inductive

If the decreasing parameter is an indexed family, all the indices must be variables. In constantIndex, the indexed family Fin' is instead applied to a constant value:

cannot use specified measure for structural recursion:
  its type Fin' is an inductive family and indices are not variables
    Fin' 100

The parameters of the decreasing parameter's type must not depend on function parameters that come after varying parameters or indices. In afterVarying, the fixed prefix is empty, because the first parameter n varies, so p is not part of the fixed prefix:

failed to infer structural recursion:
Cannot use parameter x:
  failed to eliminate recursive application
    afterVarying (n + 1) p WithParam'.zero

In the following example, the decreasing parameter n is matched against the nested pattern .succ (.succ n). Therefore .succ (.succ n) is a (non-strict) sub-term of n, and consequently both n and .succ n are strict sub-terms, and the definition is accepted.

For clarity, this example uses .succ n and .succ (.succ n) instead of the equivalent Nat-specific n+1 and n+2.

In the following example, the decreasing parameter n is not directly the discriminant of the Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match expression. Therefore, n' is not considered a sub-term of n.

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    half n'

Using well-founded recursion, and explicitly connecting the discriminant to the pattern of the match, this definition can be accepted.

Similarly, the following example fails: although xs.tail would reduce to a strict sub-term of xs, this is not visible to Lean according to the rules above. In particular, xs.tail is not definitionally equal to a strict sub-term of xs.

An important consequence of the strategies that are used to prove termination is that simultaneous matching of two discriminants is not equivalent to matching a pair. Simultaneous matching maintains the connection between the discriminants and the patterns, allowing the pattern matching to refine the types of the assumptions in the local context as well as the expected type of the Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match. Essentially, the elaboration rules for Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match treat the discriminants specially, and changing discriminants in a way that preserves the run-time meaning of a program does not necessarily preserve the compile-time meaning.

This function that finds the minimum of two natural numbers is defined by structural recursion on its first parameter:

Replacing the simultaneous pattern match on both parameters with a match on a pair causes termination analysis to fail:

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    min' n' k'

This is because the analysis only considers direct pattern matching on parameters when matching recursive calls to strictly-smaller argument values. Wrapping the discriminants in a pair breaks the connection.

This function that finds the minimum of the two components of a pair can't be elaborated via structural recursion.

failed to infer structural recursion:
Cannot use parameter nk:
  the type Nat × Nat does not have a `.brecOn` recursor

This is because the parameter's type, Prod, is not recursive. Thus, its constructor has no recursive parameters that can be exposed by pattern matching.

This definition is accepted using well-founded recursion, however:

Even though the recursive occurrence of countdown is applied to a term that is not a strict sub-term of the decreasing parameter, the following definition is accepted:

This is because n' + 0 is definitionally equal to n', which is a strict sub-term of n. Sub-terms that result from pattern matching are connected to the discriminant using the rules for match generalization, which respect definitional equality.

In countdown', the recursive occurrence is applied to 0 + n', which is not definitionally equal to n' because addition on natural numbers is structurally recursive in its second parameter:

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    countdown' (0 + n')

The following example demonstrates mutual recursion over a non-mutual inductive data type:

The following example demonstrates recursion over mutually inductive types. The functions Exp.size and App.size are mutually recursive.

The definition of App.numArgs is structurally recursive over type App. It demonstrates that not all inductive types in the mutual group need to be handled.

Lean automatically infers that the function half is structurally recursive. The termination_by? clause causes the inferred termination annotation to be displayed, and it can be automatically added to the source file with a single click.

Try this: termination_by structural x => x

Addition of natural numbers can be defined via recursion on the second argument. This function is straightforwardly structurally recursive.

Defined using Nat.rec, it is much further from the notations that most people are used to.

Structural recursive calls made on data that isn't the immediate child of the function parameter requires either creativity or a complex yet systematic encoding.

One way to think about this function is as a structural recursion that flips a bit at each call, only incrementing the result when the bit is set.

[0, 0, 1, 1, 2, 2, 3, 3, 4]

Instead of creativity, a general technique called course-of-values recursion can be used. Course-of-values recursion uses helpers that can be systematically derived for every inductive type, defined in terms of the recursor; Lean derives them automatically. For every Nat n, the type n.below (motive := mot) provides a value of type mot k for all k < n, represented as an iterated dependent pair type. The course-of-values recursor Nat.brecOn allows a function to use the result for any smaller Nat. Using it to define the function is inconvenient:

The function is marked Lean.Parser.Command.declaration : commandnoncomputable because the compiler doesn't support generating code for course-of-values recursion, which is intended for reasoning rather that efficient code. The kernel can still be used to test the function, however:

[0, 0, 1, 1, 2, 2, 3, 3, 4]

The dependent pattern matching in the body of half'' can also be encoded using recursors (specifically, Nat.casesOn), if necessary:

This definition still works.

[0, 0, 1, 1, 2, 2, 3, 3, 4]

However, it is now far from the original definition and it has become difficult for most people to understand. Recursors are an excellent logical foundation, but not an easy way to write programs or proofs.

This definition is equivalent to List.below:

In other words, for a given motive, List.below' is a type that contains a realization of the motive for all suffixes of the list.

More recursive arguments require further nested iterations of the product type. For instance, binary trees have two recursive occurrences.

Its corresponding course-of-values table contains the realizations of the motive for all subtrees:

For both lists and trees, the brecOn operator expects just a single case, rather than one per constructor. This case accepts a list or tree along with a table of results for all smaller values; from this, it should satisfy the motive for the provided value. Dependent case analysis of the provided value automatically refines the type of the memo table, providing everything needed.

The following definitions are equivalent to List.brecOn and Tree.brecOn, respectively. The primitive recursive helpers List.brecOnTable and Tree.brecOnTable compute the course-of-values tables along with the final results, and the actual definitions of the brecOn operators simply project out the result.

The first step in walking through the elaboration of half is to manually desugar it to a simpler form. This doesn't match the way Lean works, but its output is much easier to read when there are fewer OfNat instances present. This readable definition:

can be rewritten to this somewhat lower-level version:

The elaborator begins by elaborating a pre-definition in which recursion is still present but the definition is otherwise in Lean's core type theory. Turning on the compiler's tracing of pre-definitions, as well as making the pretty printer more explicit, makes the resulting pre-definition visible:

The returned trace message is:

[Elab.definition.body] half : Nat → Nat :=
    fun (x : Nat) =>
      half.match_1.{1} (fun (x : Nat) => Nat) x
        (fun (_ : Unit) => Nat.zero)
        (fun (_ : Unit) => Nat.zero)
        fun (n : Nat) => Nat.succ (half n)

The auxiliary match function's definition is:

def half.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x :=
fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

Formatted more readably, this definition is:

In other words, the specific configuration of patterns used in half are captured in half.match_1.

This definition is a more readable version of half's pre-definition:

To elaborate it as a structurally recursive function, the first step is to establish the bRecOn invocation. The definition must be marked Lean.Parser.Command.declaration : commandnoncomputable because Lean does not support code generation for recursors such as Nat.brecOn.

The next step is to replace occurrences of x in the original function body with the n provided by brecOn. Because table's type depends on x, it must also be generalized when splitting cases with half.match_1, leading to a motive with an extra parameter.

The three cases' placeholders expect the following types:

don't know how to synthesize placeholder for argument 'h_1'
context:
x n : Nat
table : Nat.below n
⊢ Unit → (fun k => Nat.below k → Nat) Nat.zero

don't know how to synthesize placeholder for argument 'h_2'
context:
x n : Nat
table : Nat.below n
⊢ Unit → (fun k => Nat.below k → Nat) 1

don't know how to synthesize placeholder for argument 'h_3'
context:
x n : Nat
table : Nat.below n
⊢ (n : Nat) → (fun k => Nat.below k → Nat) n.succ.succ

The first two cases in the pre-definition are constant functions, with no recursion to check:

The final case contains a recursive call. It should be translated into a lookup into the course-of-values table. A more readable representation of the last hole's type is:

which is equivalent to

The first Nat in the course-of-values table is the result of recursion on n + 1, and the second is the result of recursion on n. The recursive call can thus be replaced by a lookup, and the elaboration is successful:

The actual elaborator keeps track of the relationship between the parameter being checked for structural recursion and the positions in the course-of-values tables by inserting sentinel types with fresh names into the motive.

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: