5.3. Well-Founded Recursion🔗

Functions defined by well-founded recursion are those in which each recursive call has arguments that are smaller (in a suitable sense) than the functions' parameters. In contrast to structural recursion, in which recursive definitions must satisfy particular syntactic requirements, definitions that use well-founded recursion employ semantic arguments. This allows a larger class of recursive definitions to be accepted. Furthermore, when Lean's automation fails to construct a termination proof, it is possible to specify one manually.

All definitions are treated identically by the Lean compiler. In Lean's logic, definitions that use well-founded recursion typically do not reduce definitionally. The reductions do hold as propositional equalities, however, and Lean automatically proves them. This does not typically make it more difficult to prove properties of definitions that use well-founded recursion, because the propositional reductions can be used to reason about the behavior of the function. It does mean, however, that using these functions in types typically does not work well. Even when the reduction behavior happens to hold definitionally, it is often much slower than structurally recursive definitions in the kernel, which must unfold the termination proof along with the definition. When possible, recursive function that are intended for use in types or in other situations where definitional equality is important should be defined with structural recursion.

To explicitly use well-founded recursion recursion, a function or theorem definition can be annotated with a Lean.Parser.Command.declaration : commandtermination_by clause that specifies the measure by which the function terminates. The measure should be a term that decreases at each recursive call; it may be one of the function's parameters or a tuple of the parameters, but it may also be any other term. The measure's type must be equipped with a well-founded relation, which determines what it means for the measure to decrease.

syntaxExplicit Well-Founded Recursion

The Lean.Parser.Command.declaration : commandtermination_by clause introduces the termination argument.

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 (ident* =>)? term

The identifiers before the optional => can bring function parameters into scope that are not already bound in the declaration header, and the mandatory term must indicate one of the function's parameters, whether introduced in the header or locally in the clause.

Division by Iterated Subtraction

Division can be specified as the number of times the divisor can be subtracted from the dividend. This operation cannot be elaborated using structural recursion because subtraction is not pattern matching. The value of n does decrease with each recursive call, so well-founded recursion can be used to justify the definition of division by iterated subtraction.

def div (n k : Nat) : Nat := if k = 0 then 0 else if k > n then 0 else 1 + div (n - k) k termination_by n

5.3.1. Well-Founded Relations🔗

A relation ≺ is a well-founded relation if there exists no infinitely descending chain

x_0 ≻ x_1 ≻ \cdots

In Lean, types that are equipped with a canonical well-founded relation are instances of the WellFoundedRelation type class.

🔗type class
WellFoundedRelation.{u} (α : Sort u)
    : Sort (max 1 u)

Instance Constructor

WellFoundedRelation.mk.{u}

Methods

rel : α → α → Prop
wf : WellFounded WellFoundedRelation.rel

The most important instances are:

  • Nat, ordered by (· < ·).

  • Prod, ordered lexicographically: (a₁, b₁) ≺ (a₂, b₂) if and only if a₁ ≺ a₂ or a₁ = a₂ and b₁ ≺ b₂.

  • Every type that is an instance of the SizeOf type class, which provides a method SizeOf.sizeOf, has a well-founded relation. For these types, x₁ ≺ x₂ if and only if sizeOf x₁ < sizeOf x₂. For inductive types, a SizeOf instance is automatically derived by Lean.

Note that there exists a low-priority instance instSizeOfDefault that provides a SizeOf instance for any type, and always returns 0. This instance cannot be used to prove that a function terminates using well-founded recursion because 0 < 0 is false.

Default Size Instance

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.

def declaration uses 'sorry'fooInst (b : Bool → Bool) : Unit := fooInst (b ∘ b) termination_by b decreasing_by b:Bool → Bool⊢ sizeOf (b ∘ b) < sizeOf b b:Bool → Bool⊢ 0 < 0 b:Bool → Bool⊢ 0 < 0 b:Bool → Bool⊢ False b:Bool → Bool⊢ False All goals completed! 🐙

5.3.2. Termination proofs

Once a measure is specified and its well-founded relation is determined, Lean determines the termination proof obligation for every recursive call.

The proof obligation for each recursive call is of the form g a₁ a₂ … ≺ g p₁ p₂ …, where:

  • g is the measure as a function of the parameters,

  • ≺ is the inferred well-founded relation,

  • a₁ a₂ … are the arguments of the recursive call and

  • p₁ p₂ … are the parameters of the function definition.

The context of the proof obligation is the local context of the recursive call. In particular, local assumptions (such as those introduced by if h : _, match h : _ with or have) are available. If a function parameter is the discriminant of a pattern match (e.g. by a 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), then this parameter is refined to the matched pattern in the proof obligation.

The overall termination proof obligation consists of one goal for each recursive call. By default, the tactic decreasing_trivial is used to prove each proof obligation. A custom tactic script can be provided using the optional Lean.Parser.Command.declaration : commanddecreasing_by clause, which comes after the Lean.Parser.Command.declaration : commandtermination_by clause. This tactic script is run once, with one goal for each proof obligation, rather than separately on each proof obligation.

Termination Proof Obligations

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

def fib (n : Nat) := if h : n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n unsolved goals n : Nat h : ¬n ≤ 1 ⊢ n - 1 < n n : Nat h : ¬n ≤ 1 ⊢ n - 2 < ndecreasing_by n:Nath:¬n ≤ 1⊢ n - 1 < nn:Nath:¬n ≤ 1⊢ n - 2 < n
n:Nath:¬n ≤ 1⊢ n - 1 < nn:Nath:¬n ≤ 1⊢ n - 2 < n

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.

def fib (n : Nat) := if h : n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n decreasing_by n:Nath:¬n ≤ 1⊢ n - 1 < n All goals completed! 🐙 n:Nath:¬n ≤ 1⊢ n - 2 < n All goals completed! 🐙
Refined Parameters

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

def fib : Nat → Nat | 0 | 1 => 1 | .succ (.succ n) => fib (n + 1) + fib n termination_by n => n unsolved goals n : Nat ⊢ n + 1 < n.succ.succ n : Nat ⊢ n < n.succ.succdecreasing_by n:Nat⊢ n + 1 < n.succ.succn:Nat⊢ n < n.succ.succ
n:Nat⊢ n + 1 < n.succ.succn:Nat⊢ n < n.succ.succ

Additionally, in the branches of if-then-else expressions, a hypothesis asserting the current branch's condition is brought into scope, much as if the dependent if-then-else syntax had been used.

Local Assumptions and Conditionals

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 bring a local assumption about the condition into scope. Nevertheless, it is available in the context of the termination proof.

def fib (n : Nat) := if n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n unsolved goals n : Nat h✝ : ¬n ≤ 1 ⊢ n - 1 < n n : Nat h✝ : ¬n ≤ 1 ⊢ n - 2 < ndecreasing_by n:Nath✝:¬n ≤ 1⊢ n - 1 < nn:Nath✝:¬n ≤ 1⊢ n - 2 < n
n:Nath✝:¬n ≤ 1⊢ n - 1 < nn:Nath✝:¬n ≤ 1⊢ n - 2 < n
Nested Recursion in Higher-order Functions

When recursive calls are nested in higher-order functions, sometimes the function definition has to be adjusted so that the termination proof obligations can be discharged. This often happens when defining functions recursively over nested inductive types, such as the following tree structure:

structure Tree where children : List Tree

A naïve attempt to define a recursive function over this data structure will fail:

def Tree.depth (t : Tree) : Nat := let depths := t.children.map (fun c => 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 t c : Tree ⊢ sizeOf c < sizeOf tTree.depth c) match depths.max? with | some d => d+1 | none => 0 termination_by t 
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
t c : Tree
⊢ sizeOf c < sizeOf t

The termination proof obligation is not provable, because there is no connection between the local variable c and the parameter t. However, List.map applies its function argument only to elements of the given list; thus, c is always an element of t.children.

Because the termination proof goal provides access to the local context of the recursive call, it helps to bring facts into scope in the function definition that indicate that c is indeed an element of the list t.children. This can be achieved by “attaching” a proof of membership in t.children to each of its elements using the function List.attach and then bringing this proof into scope in the function passed to List.map:

def Tree.depth (t : Tree) : Nat := let depths := t.children.attach.map (fun ⟨c, hc⟩ => Tree.depth c) match depths.max? with | some d => d+1 | none => 0 termination_by t decreasing_by t:Treec:Treehc:c ∈ t.children⊢ sizeOf c < sizeOf t

Note that the proof goal after Lean.Parser.Command.declaration : commanddecreasing_by now includes the assumption c ∈ t.children, which suffices for decreasing_tactic to succeed.

5.3.3. Default Termination Proof Tactic

If no Lean.Parser.Command.declaration : commanddecreasing_by clause is given, then the decreasing_tactic is used implicitly, and applied to each proof obligation separately.

🔗tactic
decreasing_tactic

The tactic decreasing_tactic mainly deals with lexicographic ordering of tuples, applying Prod.Lex.right if the left components of the product are definitionally equal, and Prod.Lex.left otherwise. After preprocessing tuples this way, it calls the decreasing_trivial tactic.

🔗tactic
decreasing_trivial

Extensible helper tactic for decreasing_tactic. This handles the "base case" reasoning after applying lexicographic order lemmas. It can be extended by adding more macro definitions, e.g.

macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)

The tactic decreasing_trivial is an extensible tactic that applies a few common heuristics to solve a termination goal. In particular, it tries the following tactics and theorems:

  • simp_arith

  • assumption

  • theorems Nat.sub_succ_lt_self, Nat.pred_lt', Nat.pred_lt, which handle common arithmetic goals

  • omega

  • array_get_dec and array_mem_dec, which prove that the size of array elements is less than the size of the array

  • sizeOf_list_dec that the size of list elements is less than the size of the list

  • String.Iterator.sizeOf_next_lt_of_hasNext and String.Iterator.sizeOf_next_lt_of_atEnd, to handle iteration through a string using 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

This tactic is intended to be extended with further heuristics using Lean.Parser.Command.macro_rules : commandmacro_rules.

No Backtracking of Lexicographic Order

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

def ack : Nat → Nat → Nat | 0, n => n + 1 | m + 1, 0 => ack m 1 | m + 1, n + 1 => ack m (ack (m + 1) n) termination_by m n => (m, n)

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.

Prod.Lex.right {α β} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β} (h : rb b₁ b₂) : Prod.Lex ra rb (a, b₁) (a, b₂)

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:

def synack : Nat → Nat → Nat | 0, n => n + 1 | m + 1, 0 => synack m 1 | m + 1, n + 1 => synack m (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 + 1synack (m / 2 + 1) n) termination_by m n => (m, n) 
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:

Prod.Lex.right' {β} (rb : β → β → Prop) {a₂ : Nat} {b₂ : β} {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)def synack : Nat → Nat → Nat | 0, n => n + 1 | m + 1, 0 => synack m 1 | m + 1, n + 1 => synack m (synack (m / 2 + 1) n) termination_by m n => (m, n) decreasing_by m:Nat⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (m, 1) (m.succ, 0) m:Nat⊢ m < m.succ All goals completed! 🐙 -- the next goal corresponds to the third recursive call m:Natn:Nat⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (m / 2 + 1, n) (m.succ, n.succ) m:Natn:Nat⊢ m / 2 + 1 ≤ m.succm:Natn:Nat⊢ n < n.succ m:Natn:Nat⊢ m / 2 + 1 ≤ m.succ All goals completed! 🐙 m:Natn:Nat⊢ n < n.succ All goals completed! 🐙 m:Natn:Natx✝:(y : (_ : Nat) ×' Nat) → (invImage (fun x => PSigma.casesOn x fun a a_1 => (a, a_1)) Prod.instWellFoundedRelation).1 y ⟨m.succ, n.succ⟩ → Nat⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (m, x✝ ⟨m / 2 + 1, n⟩ ⋯) (m.succ, n.succ) m:Natn:Natx✝:(y : (_ : Nat) ×' Nat) → (invImage (fun x => PSigma.casesOn x fun a a_1 => (a, a_1)) Prod.instWellFoundedRelation).1 y ⟨m.succ, n.succ⟩ → Nat⊢ m < m.succ All goals completed! 🐙

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

5.3.4. Inferring Well-Founded Recursion🔗

If a recursive function definition does not indicate a termination measure, Lean will attempt to discover one automatically. If neither Lean.Parser.Command.declaration : commandtermination_by nor Lean.Parser.Command.declaration : commanddecreasing_by is provided, Lean will try to infer structural recursion before attempting well-founded recursion. If a Lean.Parser.Command.declaration : commanddecreasing_by clause is present, only well-founded recursion is attempted.

To infer a suitable termination measure, Lean considers multiple basic termination measures, which are termination measures of type Nat, and then tries all tuples of these measures.

The basic termination measures considered are:

  • all parameters whose type have a non-trivial SizeOf instance

  • the expression e₂ - e₁ whenever the local context of a recursive call has an assumption of type e₁ < e₂ or e₁ ≤ e₂, where e₁ and e₂ are of type Nat and depend only on the function's parameters. This approach is based on work by Panagiotis Manolios and Daron Vroon, 2006. “Termination Analysis with Calling Context Graphs”. In Proceedings of the International Conference on Computer Aided Verification (CAV 2006). (LNCS 4144).

  • in a mutual group, an additional basic measure is used to distinguish between recursive calls to other functions in the group and recursive calls to the function being defined (for details, see the section on mutual well-founded recursion)

Candidate measures are basic measures or tuples of basic measures. If any of the candidate measures allow all proof obligations to be discharged by the termination proof tactic (that is, the tactic specified by Lean.Parser.Command.declaration : commanddecreasing_by, or decreasing_trivial if there is no Lean.Parser.Command.declaration : commanddecreasing_by clause), then an arbitrary such candidate measure is selected as the automatic termination measure.

A termination_by? clause causes the inferred termination annotation to be shown. It can be automatically added to the source file using the offered suggestion or code action.

To avoid the combinatorial explosion of trying all tuples of measures, Lean first tabulates all basic termination measures, determining whether the basic measure is decreasing, strictly decreasing, or non-decreasing. A decreasing measure is smaller for at least one recursive call and never increases at any recursive call, while a strictly decreasing measure is smaller at all recursive calls. A non-decreasing measure is one that the termination tactic could not show to be decreasing or strictly decreasing. A suitable tuple is chosen based on the table.This approach is based on Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 2007. “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”. In Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2007). (LNTCS 4732). This table shows up in the error message when no automatic measure could be found.

Termination 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 arguments 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.def f : (n m l : Nat) → Nat | n+1, m+1, l+1 => [ f (n+1) (m+1) (l+1), f (n+1) (m-1) (l), f (n) (m+1) (l) ].sum | _, _, _ => 0 decreasing_by all_goals decreasing_tactic 
Could not find a decreasing measure.
The arguments 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.

Array Indexing

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.

def binarySearch (x : Int) (xs : Array Int) : Option Nat := go 0 xs.size where go (i j : Nat) (hj : j ≤ xs.size := by omega) := if h : i < j then let mid := (i + j) / 2 let y := xs[mid] if x = y then some mid else if x < y then go i mid else go (mid + 1) j else none Try this: termination_by (j, j - i)termination_by?

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)
Termination Proof Tactics During Inference

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:

Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) x1 x2 1) 583:16-23 ? ? 2) 584:27-40 _ _ 3) 584:20-41 _ _ Please use `termination_by` to specify a decreasing measure.def ack : Nat → Nat → Nat | 0, n => n + 1 | m + 1, 0 => ack m 1 | m + 1, n + 1 => ack m (ack (m + 1) n) decreasing_by · apply Prod.Lex.left omega · apply Prod.Lex.right omega · apply Prod.Lex.left omega

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.

Inference too powerful

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:

def notAck : Nat → Nat → Nat | 0, n => n + 1 | m + 1, 0 => notAck m 1 | m + 1, n + 1 => notAck m (notAck (m / 2 + 1) n) decreasing_by all_goals All goals completed! 🐙 
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.

5.3.5. Mutual Well-Founded Recursion🔗

Lean supports the definition of mutually recursive functions using well-founded recursion. Mutual recursion may be introduced using a mutual block, but it also results from Lean.Parser.Term.letrec : termlet rec expressions and Lean.Parser.Command.declaration : commandwhere blocks. The rules for mutual well-founded recursion are applied to a group of actually mutually recursive, lifted definitions, that results from the elaboration steps for mutual groups.

If any function in the mutual group has a Lean.Parser.Command.declaration : commandtermination_by or Lean.Parser.Command.declaration : commanddecreasing_by clause, well-founded recursion is attempted. If a termination measure is specified using Lean.Parser.Command.declaration : commandtermination_by for any function in the mutual group, then all functions in the group must specify a termination measure, and they have to have the same type.

If no termination argument is specified, the termination argument is inferred, as described above. In the case of mutual recursion, a third class of basic measures is considered during inference, namely for each function in the mutual group the measure that is 1 for that function and 0 for the others. This allows Lean to order the functions so that some calls from one function to another are allowed even if the parameters do not decrease.

Mutual recursion without parameter decrease

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.

mutual def f : (n : Nat) → Nat | 0 => 0 | n+1 => g n Try this: termination_by n => (n, 0)termination_by? def g (n : Nat) : Nat := (f n) + 1 Try this: termination_by (n, 1)termination_by? end

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)

5.3.6. Theory and Construction

This section gives a very brief glimpse into the mathematical constructions that underlie termination proofs via well-founded recursion, which may surface occasionally. The elaboration of functions defined by well-founded recursion is based on the WellFounded.fix operator.

🔗def
WellFounded.fix.{u, v} {α : Sort u}
    {C : α → Sort v} {r : α → α → Prop}
    (hwf : WellFounded r)
    (F : (x : α) →
      ((y : α) → r y x → C y) → C x)
    (x : α) : C x

The type α is instantiated with the function's (varying) parameters, packed into one type using PSigma. The WellFounded relation is constructed from the termination measure via invImage.

🔗def
invImage.{u_1, u_2} {α : Sort u_1}
    {β : Sort u_2} (f : α → β)
    (h : WellFoundedRelation β)
    : WellFoundedRelation α

The function's body is passed to WellFounded.fix, with parameters suitably packed and unpacked, and recursive calls are replaced with a call to the value provided by WellFounded.fix. The termination proofs generated by the Lean.Parser.Command.declaration : commanddecreasing_by tactics are inserted in the right place.

Finally, the equational and unfolding theorems for the recursive function are proved from WellFounded.fix_eq. These theorems hide the details of packing and unpacking arguments and describe the function's behavior in terms of the original definition.

In the case of mutual recursion, an equivalent non-mutual function is constructed by combining the function's arguments using PSum, and pattern-matching on that sum type in the result type and the body.

The definition of WellFounded builds on the notion of accessible elements of the relation:

🔗inductive predicate
WellFounded.{u} {α : Sort u} (r : α → α → Prop)
    : Prop

A relation r is WellFounded if all elements of α are accessible within r. If a relation is WellFounded, it does not allow for an infinite descent along the relation.

If the arguments of the recursive calls in a function definition decrease according to a well founded relation, then the function terminates. Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.

Constructors

intro.{u} {α : Sort u} {r : α → α → Prop}
    (h : ∀ (a : α), Acc r a) : WellFounded r
🔗inductive predicate
Acc.{u} {α : Sort u} (r : α → α → Prop)
    : α → Prop

Acc is the accessibility predicate. Given some relation r (e.g. <) and a value x, Acc r x means that x is accessible through r:

x is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x.

Constructors

intro.{u} {α : Sort u} {r : α → α → Prop} (x : α)
    (h : ∀ (y : α), r y x → Acc r y) : Acc r x

A value is accessible if for all y such that r y x, y is also accessible. Note that if there exists no y such that r y x, then x is accessible. Such an x is called a base case.

Division by Iterated Subtraction: Termination Proof

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

noncomputable def div (n k : Nat) : Nat := (inferInstanceAs (WellFoundedRelation Nat)).wf.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + (r (n - k) <| α:Type un✝:Natk:Natn:Natr:(y : Nat) → WellFoundedRelation.rel y n → Nath✝:¬k = 0h:¬k > n⊢ WellFoundedRelation.rel (n - k) n α:Type un✝:Natk:Natn:Natr:(y : Nat) → WellFoundedRelation.rel y n → Nath✝:¬k = 0h:¬k > n⊢ n - k < n All goals completed! 🐙)) n

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:

theorem div.eq0 : div n 0 = 0 := n:Nat⊢ div n 0 = 0 n:Nat⊢ div n 0 = 0 
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:

theorem div.eq0 : div n 0 = 0 := n:Nat⊢ div n 0 = 0 n:Nat⊢ proof_1.fix (fun n r => if h : 0 = 0 then 0 else if h : 0 > n then 0 else 1 + r (n - 0) ⋯) n = 0 All goals completed! 🐙 theorem div.eq1 : k > n → div n k = 0 := k:Natn:Nat⊢ k > n → div n k = 0 k:Natn:Nath:k > n⊢ div n k = 0 k:Natn:Nath:k > n⊢ proof_1.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + r (n - k) ⋯) n = 0 k:Natn:Nath:k > n⊢ (if h : k = 0 then 0 else if h : k > n then 0 else 1 + (fun y x => proof_1.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + r (n - k) ⋯) y) (n - k) ⋯) = 0 k:Natn:Nath:k > n⊢ ¬k = 0 → k ≤ n → 1 + proof_1.fix (fun n r => if h : k = 0 then 0 else if h : n < k then 0 else 1 + r (n - k) ⋯) (n - k) = 0 k:Natn:Nath:k > na✝¹:¬k = 0a✝:k ≤ n⊢ 1 + proof_1.fix (fun n r => if h : k = 0 then 0 else if h : n < k then 0 else 1 + r (n - k) ⋯) (n - k) = 0; All goals completed! 🐙 theorem div.eq2 : ¬ k = 0 → ¬ (k > n) → div n k = 1 + div (n - k) k := k:Natn:Nat⊢ ¬k = 0 → ¬k > n → div n k = 1 + div (n - k) k k:Natn:Nata✝¹:¬k = 0a✝:¬k > n⊢ div n k = 1 + div (n - k) k k:Natn:Nata✝¹:¬k = 0a✝:¬k > n⊢ proof_1.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + r (n - k) ⋯) n = 1 + proof_1.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + r (n - k) ⋯) (n - k) k:Natn:Nata✝¹:¬k = 0a✝:¬k > n⊢ (if h : k = 0 then 0 else if h : k > n then 0 else 1 + (fun y x => proof_1.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + r (n - k) ⋯) y) (n - k) ⋯) = 1 + proof_1.fix (fun n r => if h : k = 0 then 0 else if h : k > n then 0 else 1 + r (n - k) ⋯) (n - k) k:Natn:Nata✝¹:¬k = 0a✝:k ≤ n⊢ n < k → 0 = 1 + proof_1.fix (fun n r => if h : n < k then 0 else 1 + r (n - k) ⋯) (n - k) All goals completed! 🐙