4.4. Recursive Definitions🔗

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 parameter 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 parameter 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:

cannot use specified parameter for structural recursion:
  its type is an inductive datatype
    WithParam' p n
  and the datatype parameter
    p
  depends on the function parameter
    p
  which does not come before the varying parameters and before the indices of the recursion parameter.

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 xref sigma 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.

It's 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:Trace not showing up in serialized info - figure out why so this test can work better, or better yet, add proper trace rendering to Verso

[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.