Recursive definitions in Lean

Structural recursion

It is often the case that your recursive functions follow the structure of a recursively defined data type. In these cases, Lean will see that your function definition is obviously terminating and nothing more needs to be done.

Consider a variant of our search function from above, where we count down from the number start:

We have changed the result type of the function to Option α so that search can return Option.none if nothing is found, and use pattern matching to try each number in sequence.

This follows the recursive structure of the Nat type, which is defined as

in the Lean Prelude, and 0 and n+1 are merely pretty syntax for the constructors Nat.zero and Nat.succ n. Because search follows the recursive structure, Lean accepts the definition as is; no extra termination argument needed.

In general, if you plan to prove theorems about your functions, a structurally recursive definition is most pleasant to work with, for two reasons:

1. Since the definition follows the structure of the argument’s data type, you can use induction over that data type when proving theorems, as in this case:

   theorem search_const_nonesearch_const_none.{u_1} {α : Type u_1} (start : Nat) : search (fun x => none) start = none {αType u_1} (startNat : NatNat : TypeThe type of natural numbers, starting at zero. It is defined as an inductive type freely generated by "zero is a natural number" and "the successor of a natural number is a natural number". You can prove a theorem `P n` about `n : Nat` by `induction n`, which will expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming a proof of `P i`. The same method also works to define functions by recursion on natural numbers: induction and recursion are two expressions of the same operation from Lean's point of view. ``` open Nat example (n : Nat) : n < succ n := by induction n with | zero => show 0 < 1 decide | succ i ih => -- ih : i < succ i show succ i < succ (succ i) exact Nat.succ_lt_succ ih ``` This type is special-cased by both the kernel and the compiler: * The type of expressions contains "`Nat` literals" as a primitive constructor, and the kernel knows how to reduce zero/succ expressions to nat literals. * If implemented naively, this type would represent a numeral `n` in unary as a linked list with `n` links, which is horribly inefficient. Instead, the runtime itself has a special representation for `Nat` which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually [GMP](https://gmplib.org/)). ) : searchsearch.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α (α := αType u_1) (fun _ => .noneOption.none.{u} {α : Type u} : Option αNo value. ) startNat = .noneOption.none.{u} {α : Type u} : Option αNo value. := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. inductionAssuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well. For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `induction n` produces one goal with hypothesis `h : P 0` and target `Q 0`, and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`. Here the names `a` and `ih₁` are chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor. - `induction e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then performs induction on the resulting variable. - `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a term whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables - `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. - Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case. startNat

   αType u_1

   :

   Type u_1

   ⊢ searchsearch.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α (fun xNat => none) 0 = Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) none

   succ

   αType u_1	:	Type u_1
   n✝Nat	:	NatNat : TypeThe type of natural numbers, starting at zero. It is defined as an inductive type freely generated by "zero is a natural number" and "the successor of a natural number is a natural number". You can prove a theorem `P n` about `n : Nat` by `induction n`, which will expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming a proof of `P i`. The same method also works to define functions by recursion on natural numbers: induction and recursion are two expressions of the same operation from Lean's point of view. ``` open Nat example (n : Nat) : n < succ n := by induction n with | zero => show 0 < 1 decide | succ i ih => -- ih : i < succ i show succ i < succ (succ i) exact Nat.succ_lt_succ ih ``` This type is special-cased by both the kernel and the compiler: * The type of expressions contains "`Nat` literals" as a primitive constructor, and the kernel knows how to reduce zero/succ expressions to nat literals. * If implemented naively, this type would represent a numeral `n` in unary as a linked list with `n` links, which is horribly inefficient. Instead, the runtime itself has a special representation for `Nat` which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually [GMP](https://gmplib.org/)).
   a✝search (fun x => none) n✝ = none	:	searchsearch.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α (fun xNat => none) n✝Nat = Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) none

   ⊢ searchsearch.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α (fun xNat => none) (n✝Nat + HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent. 1) = Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) none
   case* `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, or else fails. * `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. * `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`. zero => rfl`rfl` tries to close the current goal using reflexivity. This is supposed to be an extensible tactic and users can add their own support for new reflexive relations. Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different reflexivity theorems (e.g., `Iff.rfl`).
   All goals completed! 🐙
   case* `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, or else fails. * `case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. * `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`. succ _nNat IHsearch (fun x => none) _n = none => exact`exact e` closes the main goal if its target type matches that of `e`. IHsearch (fun x => none) _n = none
   All goals completed! 🐙

2. The defining equation of your function holds definitionally:

   example : searchsearch.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α (fun nNat => if`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. nNat * nNat ≤ 121 then`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. .someOption.some.{u} {α : Type u} (val : α) : Option αSome value of type `α`. nNat else`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. .noneOption.none.{u} {α : Type u} : Option αNo value. ) 100 = .someOption.some.{u} {α : Type u} (val : α) : Option αSome value of type `α`. 11 := rflrfl.{u} {α : Sort u} {a : α} : a = a`rfl : a = a` is the unique constructor of the equality type. This is the same as `Eq.refl` except that it takes `a` implicitly instead of explicitly. This is a more powerful theorem than it may appear at first, because although the statement of the theorem is `a = a`, Lean will allow anything that is definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in Lean by `rfl`, because both sides are the same up to definitional equality.

   This can be crucial if you use your function in types, and expect the type checker to calculate with your function. A full discussion of why and when that matters would takes us too far here, though.

Lean will automatically recognize structurally recursive functions, and even allows you to peel off more than one constructor at a time, as in the ubiquitous example of recursively calculating the Fibonacci numbers:

If you want to know whether Lean is using structural recursion to implement your definition, run #print fib and look for mentions of functions called brecOn.

Well-founded recursion

If your function happens to follow the recursive structure of its argument and it just works, great! But often your code just doesn't fit this pattern. Consider these popular algorithms:

• Sorting algorithms like Quicksort and Mergesort split and reorder the input lists, rather than recursing on just the tail of the list.

• Division, implemented as iterated subtraction, recurses not on the predecessor of the input number, but takes bigger steps.

• With binary search sometimes one argument increases and sometimes the other argument decreases. However, their difference always decreases, and often by more than just one.

In such cases, you can still define your function, but now an explicit termination proof is needed. To stick with our example, let us search counting up again, as originally, but define an upper bound (called to), so that the search always terminates:

Notice the squiggly line beneath the recursive call fail to show termination for search with errors argument #3 was not used for structural recursion failed to eliminate recursive application search f✝ (start + 1) to argument #4 was not used for structural recursion failed to eliminate recursive application search f✝ (start + 1) to structural recursion cannot be used Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) start to 1) 16:21-44 ? = Please use `termination_by` to specify a decreasing measure.searchsearch.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) : Option α fNat → Option α (startNat + 1) toNat. If you hover it, you will see that Lean complains rather verbosely:

fail to show termination for
  search
with errors
argument #3 was not used for structural recursion
  failed to eliminate recursive application
    search f✝ (start + 1) to

argument #4 was not used for structural recursion
  failed to eliminate recursive application
    search f✝ (start + 1) to

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            start to
1) 16:21-44     ?  =
Please use `termination_by` to specify a decreasing measure.

This message gives us a glimpse into the inner workings of Lean here. It first tries really hard to find structural recursion, but neither argument three (start) nor argument four (to) decreases structurally.

Then, it also tries to prove well-founded termination automatically, but fails again. It displays in a small, mildly obscure matrix how the parameters (start and to) behave at the recursive calls (of which our function only has one). In the output above we see that Lean could not prove start to be decreasing, and the parameter to was proved to be equal, so certainly not decreasing.

Finally, it at least tells us what to do: Use termination_by!

decreasing_by
  simp_wf
  apply Nat.sub_succ_lt_self
  assumption

start to : Nat
h✝: start < to
⊢ to - (start + 1) < to - start

decreasing_by decreasing_tactic

search.eq_def.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) :
  search f start to =
    match f start with
    | some x => some x
    | none => if start < to then search f (start + 1) to else none

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
v : α
ts : List (Tree α)
t : Tree α
⊢ sizeOf t < 1 + sizeOf ts

List.attach.{u_1} {α : Type u_1} (l : List α) : List { x // x ∈ l }

α: Type
v: α
ts: List (Tree α)
t: Tree α
h: t ∈ ts
⊢ sizeOf t < 1 + sizeOf ts

Avoiding termination proofs

As we just saw, structural and well-founded recursion are powerful tools to define recursive functions in a way that we can use them in proofs, but are sometimes non-trivial to use. When we just want to define functions for use in programs, but not in proofs, there is a way out.

We can declare that a function is partial. If we do that, Lean will accept almost any function definition, like our non-terminating search:

As a partial function, it can be used in program just fine: the command

prints

some 11

But for the purposes of proofs, search is completely opaque. All we know is that it exists, but not how it behaves.

You might have spotted that this search function returns an Option α, unlike the example we started with, which simply returned an α. That is because the type of a partial function must be inhabited, or else allowing proofs to merely mention the function causes havoc, as we saw in the introduction.

If you need to define such a function, you can use the final technique presented in this post, namely the unsafe keyword:

Now Lean will accept, compile and run even this definition, just like a conventional programming language out there. Lean will, however, prevent you from using unsafe definitions in theorems and proofs, so that soundness is preserved.