4.4.Β Recursive DefinitionsπŸ”—

Allowing arbitrary recursive function definitions would make Lean's logic inconsistent. General recursion makes it possible to write circular proofs: "proposition P is true because proposition P is true". Outside of proofs, an infinite loop could be assigned the type Empty, which can be used with Lean.Parser.Term.nomatch : termEmpty match/ex falso. `nomatch e` is of arbitrary type `Ξ± : Sort u` if Lean can show that an empty set of patterns is exhaustive given `e`'s type, e.g. because it has no constructors. nomatch or Empty.rec to prove any theorem.

Banning recursive function definitions outright would render Lean far less useful: inductive types are key to defining both predicates and data, and they have a recursive structure. Furthermore, most useful recursive functions do not threaten soundness, and infinite loops usually indicate mistakes in definitions rather than intentional behavior. Instead of banning recursive functions, Lean requires that each recursive function is defined safely. While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.The section on the elaborator's output in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.

There are four main kinds of recursive functions that can be defined:

Structurally recursive functions

Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.Strictly speaking, arguments whose types are indexed families are grouped together with their indices, with the whole collection considered as a unit. The elaborator translates the recursion into uses of the argument's recursor. Because every type-correct use of a recursor is guaranteed to avoid infinite regress, this translation is evidence that the function terminates. Applications of functions defined via recursors are definitionally equal to the result of the recursion, and are typically relatively efficient inside the kernel.

Recursion over well-founded relations

Many functions are also difficult to convert to structural recursion; for instance, a function may terminate because the difference between an array index and the size of the array decreases as the index increases, but Nat.rec isn't applicable because the index that increases is the function's argument. Here, there is a measure of termination that decreases at each recursive call, but the measure is not itself an argument to the function. In these cases, well-founded recursion can be used to define the function. Well-founded recursion is a technique for systematically transforming recursive functions with a decreasing measure into recursive functions over proofs that every sequence of reductions to the measure eventually terminates at a minimum. Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition. Even when definitional equalities exist, these functions are frequently slow to compute with because they require reducing proof terms that are often very large.

Partial functions with nonempty ranges

For many applications, it's not important to reason about the implementation of certain functions. A recursive function might be used only as part of the implementation of proof automation steps, or it might be an ordinary program that will never be formally proved correct. In these cases, the Lean kernel does not need either definitional or propositional equalities to hold for the definition; it suffices that soundness is maintained. Functions marked Lean.Parser.Command.declaration : commandpartial are treated as opaque constants by the kernel and are neither unfolded nor reduced. All that is required for soundness is that their return type is inhabited. Partial functions may still be used in compiled code as usual, and they may appear in propositions and proofs; their equational theory in Lean's logic is simply very weak.

Unsafe recursive definitions

Unsafe definitions have none of the restrictions of partial definitions. They may freely make use of general recursion, and they may use features of Lean that break assumptions about its equational theory, such as primitives for casting (unsafeCast), checking pointer equality (ptrAddrUnsafe), and observing reference counts (isExclusiveUnsafe). However, any declaration that refers to an unsafe definition must itself be marked Lean.Parser.Command.declaration : commandunsafe, making it clear when logical soundness is not guaranteed. Unsafe operations can be used to replace the implementations of other functions with more efficient variants in compiled code, while the kernel still uses the original definition. The replaced function may be opaque, which results in the function name having a trivial equational theory in the logic, or it may be an ordinary function, in which case the function is used in the logic. Use this feature with care: logical soundness is not at risk, but the behavior of programs written in Lean may diverge from their verified logical models if the unsafe implementation is incorrect.

As described in the overview of the elaborator's output, elaboration of recursive functions proceeds in two phases:

  1. The definition is elaborated as if Lean's core type theory had recursive definitions. Aside from using recursion, this provisional definition is fully elaborated. The compiler generates code from these provisional definitions.

  2. A termination analysis attempts to use the four techniques to justify the function to Lean's kernel. If the definition is marked Lean.Parser.Command.declaration : commandunsafe or Lean.Parser.Command.declaration : commandpartial, then that technique is used. If an explicit Lean.Parser.Command.declaration : commandtermination_by clause is present, then the indicated technique is the only one attempted. If there is no such clause, then the elaborator performs a search, testing each parameter to the function as a candidate for structural recursion, and attempting to find a measure with a well-founded relation that decreases at each recursive call.

This section describes the four techniques in detail.

4.4.1.Β Structural RecursionπŸ”—

Structurally recursive functions are those in which each recursive call is on a structurally smaller term than the argument. Structural recursion is stronger than the primitive recursion that recursors provide, because the recursive call can use more deeply nested sub-terms of the argument, rather than only an immediate sub-term. The constructions used to implement structural recursion are, however, implemented using the recursor; these helper constructions are described in the section on inductive types.

4.4.1.1.Β Explicit structural recursion

To explicitly use structural recursion, a function definition can be annotated with a termination_by structural clause specifying the decreasing parameter:

def half : Nat β†’ Nat | 0 | 1 => 0 | n + 2 => half n + 1 termination_by structural n => n
syntax

The grammar of the termination_by structural clause is

Specify a termination argument for recursive functions.
```
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the arguments `a` and `b` decreases.

If the function takes further argument after the colon, you can name them as follows:
```
def example (a : Nat) : Nat β†’ Nat β†’ Nat :=
termination_by b c => a - b
```

By default, a `termination_by` clause will cause the function to be constructed using well-founded
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
indicates the function is expected to be structural recursive on the argument. In this case
the body of the `termination_by` clause must be one of the function's parameters.

If omitted, a termination argument will be inferred. If written as `termination_by?`,
the inferrred termination argument will be suggested.

terminationBy ::= ...
    | Specify a termination argument for recursive functions.
```
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the arguments `a` and `b` decreases.

If the function takes further argument after the colon, you can name them as follows:
```
def example (a : Nat) : Nat β†’ Nat β†’ Nat :=
termination_by b c => a - b
```

By default, a `termination_by` clause will cause the function to be constructed using well-founded
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
indicates the function is expected to be structural recursive on the argument. In this case
the body of the `termination_by` clause must be one of the function's parameters.

If omitted, a termination argument will be inferred. If written as `termination_by?`,
the inferrred termination argument will be suggested.

termination_by structural (ident* =>)? term

where the identifiers before the optional => can bring function parameters into scope that are not already bound in the declaration header, and the $term must elaborate to one of the functions parameters.

The type of the selected decreasing parameter must be an inductive type. If it is an indexed family, then all indices must be parameters of the function.

Ineligible decreasing parameters

The decreasing parameter must have inductive type:

def bad (x : Nat β†’ Nat) : Nat := bad (fun n => x (n+1)) cannot use specified parameter for structural recursion: its type is not an inductivetermination_by structural x 
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:

inductive Fin' : Nat β†’ Type where | zero : Fin' (n+1) | succ : Fin' n β†’ Fin' (n+1) def bad (x : Fin' 100) : Nat := bad .zero cannot use specified parameter for structural recursion: its type Fin' is an inductive family and indices are not variables Fin' 100termination_by structural x 
cannot use specified parameter for structural recursion:
  its type Fin' is an inductive family and indices are not variables
    Fin' 100

Furthermore, every recursive call of the functions must be on a strict sub-term of the decreasing parameter. The rules are as follows:

  • The decreasing parameter itself is a (non-strict) sub-term.

  • If a sub-term is the target of a match statement, then the pattern matched against that target is a sub-term.

  • If a sub-term is a constructor applied to arguments, then its recursive arguments are strict sub-terms.

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.

def fib : Nat β†’ Nat | 0 | 1 => 1 | .succ (.succ n) => fib n + fib (.succ n) termination_by structural n => n

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

Matching on Complex Expressions Can Prevent Elaboration

In the following example, the decreasing parameter n is not directly the target of the match statement. Therefore, n' is not considered a subterm and the elaboration fails.

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application half n' def half (n : Nat) : Nat := match Option.some n with | .some (n' + 2) => half n' + 1 | _ => 0 termination_by structural 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 target to the pattern of the match, this definition can be accepted.

def half (n : Nat) : Nat := match h : Option.some n with | .some (n' + 2) => half n' + 1 | _ => 0 termination_by n decreasing_by n:Natn':Nath:n = n' + 1 + 1⊒ n' < n' + 1 + 1; All goals completed! πŸ™

Similarly, the following example fails: Although tail xs would reduce to a strict sub-term of xs, this is not visible to lean according to the rules above.

failed to infer structural recursion: Cannot use parameter #2: failed to eliminate recursive application listLen xs.tail def listLen : List Ξ± β†’ Nat | [] => 0 | xs => listLen xs.tail + 1 termination_by structural xs => xs
Simultaneous Matching vs Matching Pairs for Structural Recursion

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:

def min' (n k : Nat) : Nat := match n, k with | 0, _ => 0 | _, 0 => 0 | n' + 1, k' + 1 => min' n' k' + 1 termination_by structural n

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' def min' (n k : Nat) : Nat := match (n, k) with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' n' k' + 1 termination_by structural n 
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 def min' (nk : Nat Γ— Nat) : Nat := match nk with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' (n', k') + 1 termination_by structural nk 
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 and thus its constructor has no recursive parameters that can be exposed by pattern-matching.

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

def min' (nk : Nat Γ— Nat) : Nat := match nk with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' (n', k') + 1 termination_by nk

4.4.1.2.Β Mutual structural recursion

TODO

4.4.1.3.Β Inferring structural recursion

TODO

4.4.1.4.Β Elaboration using course-of-value recursion

In this section, the construction used to elaborate structurally recursive functions is explained in more detail.

Recursion vs Recursors

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

def add (n : Nat) : Nat β†’ Nat | .zero => n | .succ k => .succ (add n k)

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

def add' (n : Nat) := Nat.rec (motive := fun _ => Nat) n (fun k soFar => .succ soFar)

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.

def half : Nat β†’ Nat | 0 | 1 => 0 | n + 2 => half n + 1

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.

def helper : Nat β†’ Bool β†’ Nat := Nat.rec (motive := fun _ => Bool β†’ Nat) (fun _ => 0) (fun _ soFar => fun b => (if b then Nat.succ else id) (soFar !b)) def half' (n : Nat) : Nat := helper n false [0, 0, 1, 1, 2, 2, 3, 3, 4]#eval [0, 1, 2, 3, 4, 5, 6, 7, 8].map half' 
[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:

noncomputable def half'' (n : Nat) : Nat := Nat.brecOn n (motive := fun _ => Nat) fun k soFar => match k, soFar with | 0, _ | 1, _ => 0 | _ + 2, ⟨_, ⟨h, _⟩⟩ => h + 1

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]#reduce [0,1,2,3,4,5,6,7,8].map half'' 
[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:

noncomputable def half''' (n : Nat) : Nat := n.brecOn (motive := fun _ => Nat) fun k => k.casesOn (motive := fun k' => (k'.below (motive := fun _ => Nat)) β†’ Nat) (fun _ => 0) (fun k' => k'.casesOn (motive := fun k'' => (k''.succ.below (motive := fun _ => Nat)) β†’ Nat) (fun _ => 0) (fun _ soFar => soFar.2.1.succ))

This definition still works.

[0, 0, 1, 1, 2, 2, 3, 3, 4]#reduce [0,1,2,3,4,5,6,7,8].map half'' 
[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.

The structural recursion analysis attempts to translate the recursive pre-definition into a use of the appropriate structural recursion constructions. At this step, pattern matching has already been translated into the use of matcher functions; these are treated specially by the termination checker. Next, for each group of parameters, a translation using brecOn is attempted.

Course-of-Values Tables

This definition is equivalent to List.below:

def List.below' {Ξ± : Type u} {motive : List Ξ± β†’ Sort u} : List Ξ± β†’ Sort (max 1 u) | [] => PUnit | _ :: xs => motive xs Γ—' xs.below' (motive := motive)

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.

inductive Tree (Ξ± : Type u) : Type u where | leaf | branch (left : Tree Ξ±) (val : Ξ±) (right : Tree Ξ±)

It's corresponding course-of-values table contains the realizations of the motive for all subtrees:

def Tree.below' {Ξ± : Type u} {motive : Tree Ξ± β†’ Sort u} : Tree Ξ± β†’ Sort (max 1 u) | .leaf => PUnit | .branch left _val right => motive left Γ—' motive right Γ—' left.below' (motive := motive) Γ—' right.below' (motive := motive)

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.

def List.brecOnTable {Ξ± : Type u} {motive : List Ξ± β†’ Sort u} (xs : List Ξ±) (step : (ys : List Ξ±) β†’ ys.below' (motive := motive) β†’ motive ys) : motive xs Γ—' xs.below' (motive := motive) := match xs with | [] => ⟨step [] PUnit.unit, PUnit.unit⟩ | x :: xs => let res := xs.brecOnTable (motive := motive) step let val := step (x :: xs) res ⟨val, res⟩ def Tree.brecOnTable {Ξ± : Type u} {motive : Tree Ξ± β†’ Sort u} (t : Tree Ξ±) (step : (ys : Tree Ξ±) β†’ ys.below' (motive := motive) β†’ motive ys) : motive t Γ—' t.below' (motive := motive) := match t with | .leaf => ⟨step .leaf PUnit.unit, PUnit.unit⟩ | .branch left val right => let resLeft := left.brecOnTable (motive := motive) step let resRight := right.brecOnTable (motive := motive) step let branchRes := ⟨resLeft.1, resRight.1, resLeft.2, resRight.2⟩ let val := step (.branch left val right) branchRes ⟨val, branchRes⟩ def List.brecOn' {Ξ± : Type u} {motive : List Ξ± β†’ Sort u} (xs : List Ξ±) (step : (ys : List Ξ±) β†’ ys.below' (motive := motive) β†’ motive ys) : motive xs := (xs.brecOnTable (motive := motive) step).1 def Tree.brecOn' {Ξ± : Type u} {motive : Tree Ξ± β†’ Sort u} (t : Tree Ξ±) (step : (ys : Tree Ξ±) β†’ ys.below' (motive := motive) β†’ motive ys) : motive t := (t.brecOnTable (motive := motive) step).1

The below construction is a mapping from each value of a type to the results of some function call on all smaller values; it can be understood as a memoization table that already contains the results for all smaller values. Recursors expect an argument for each of the inductive type's constructors; these arguments are called with the constructor's arguments (and the result of recursion on recursive parameters) during ΞΉ-reduction. The course-of-values recursion operator brecOn, on the other hand, expects just a single case that covers all constructors at once. This case is provided with a value and a below table that contains the results of recursion on all values smaller than the given value; it should use the contents of the table to satisfy the motive for the provided value. If the function is structurally recursive over a given parameter (or parameter group), then the results of all recursive calls will be present in this table already.

When the body of the recursive function is transformed into an invocation of brecOn on one of the function's parameters, the parameter and its course-of-values table are in scope. The analysis traverses the body of the function, looking for recursive calls. If the parameter is matched against, then its occurrences in the local context are generalized and then instantiated with the pattern; this is also true for the type of the course-of-values table. Typically, this pattern matching results in the type of the course-of-values table becoming more specific, which gives access to the recursive results for smaller values. When an recursive occurrence of the function is detected, the course-of-values table is consulted to see whether it contains a result for the argument being checked. If so, the recursive call can be replaced with a projection from the table. If not, then the parameter in question doesn't support structural recursion.

Elaboration Walkthrough

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:

def half : Nat β†’ Nat | 0 | 1 => 0 | n + 2 => half n + 1

can be rewritten to this somewhat lower-level version:

def half : Nat β†’ Nat | .zero | .succ .zero => .zero | .succ (.succ n) => half n |>.succ

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:

set_option trace.Elab.definition.body true in set_option pp.all true in def half : Nat β†’ Nat | .zero | .succ .zero => .zero | .succ (.succ n) => half n |>.succ

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#print half.match_1 
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:

def half.match_1'.{u} : (motive : Nat β†’ Sort u) β†’ (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

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:

def half' : Nat β†’ Nat := fun (x : Nat) => half.match_1 (motive := fun _ => Nat) x (fun _ => 0) -- Case for 0 (fun _ => 0) -- Case for 1 (fun n => Nat.succ (half' n)) -- Case for n + 2

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

noncomputable def half'' : Nat β†’ Nat := fun (x : Nat) => x.brecOn fun n table => don't know how to synthesize placeholder context: x n : Nat table : Nat.below n ⊒ Nat_ /- To translate: half.match_1 (motive := fun _ => Nat) x (fun _ => 0) -- Case for 0 (fun _ => 0) -- Case for 1 (fun n => Nat.succ (half' n)) -- Case for n + 2 -/

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.

noncomputable def half'' : Nat β†’ Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) β†’ Nat) n 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_) table /- To translate: (fun _ => 0) -- Case for 0 (fun _ => 0) -- Case for 1 (fun n => Nat.succ (half' n)) -- Case for n + 2 -/

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:

noncomputable def half'' : Nat β†’ Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) β†’ Nat) n (fun () _ => .zero) (fun () _ => .zero) 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_) table /- To translate: (fun n => Nat.succ (half' n)) -- Case for n + 2 -/

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:

(n : Nat) β†’ Nat.below (motive := fun _ => Nat) n.succ.succ β†’ Nat

which is equivalent to

(n : Nat) β†’ Nat Γ—' Nat Γ—' Nat.below (motive := fun _ => Nat) n β†’ Nat

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:

noncomputable def half'' : Nat β†’ Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) β†’ Nat) n (fun () _ => .zero) (fun () _ => .zero) (fun _ table => Nat.succ table.2.1) table unexpected end of input; expected ')', ',' or ':'

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.

Planned Content

The construction for mutually recursive functions ought to be explained here.

Tracked at issue #56

4.4.2.Β Well-Founded RecursionπŸ”—

Planned Content

This section will describe the translation of well-founded recursion.

Tracked at issue #57

4.4.3.Β Controlling Reduction

Planned Content

This section will describe reducibility: reducible, semi-reducible, and irreducible definitions.

Tracked at issue #58

4.4.4.Β Partial and Unsafe Recursive DefinitionsπŸ”—

Planned Content

This section will describe partial and unsafe definitions:

  • Interaction with the kernel and elaborator

  • What guarantees are there, and what aren't there?

  • How to bridge from unsafe to safe code?

Tracked at issue #59