Recursive definitions in Lean

Lean is a general purpose programming language. For example, the Lean compiler itself is written in Lean, and so is its language server, which provides those nice squiggly lines that you see when you edit a Lean file. As a Lean developer, you can rightfully expect to be able to write the kind of code you’d be writing in other programming languages.

Lean is also an interactive theorem prover that allows you to formalize mathematics or prove that the programs you wrote are actually correct with regard to their specification. Because Lean is both of these things, there are some possibly unfamiliar aspects that you have to pay attention to, even if you are just interested in Lean as a programming language.

One such aspect is termination - Lean is much pickier about whether programs ever actually return a result. This post explains why termination matters, how you can deal with it when you care, and how you you can avoid having to deal with it when you do not care.

Nontermination vs. soundness

To begin, let's briefly recapitulate why termination matters. Consider the following function search that goes through the natural numbers until its argument f returns a value (or keeps searching if f always returns Option.none):

def search
{α : Type u_1} → (Nat → Option α) → Nat → α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) : α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> search
{α : Type u_1} → (Nat → Option α) → Nat → α
f
Nat → Option α
(start
Nat
+ 1)

We could use this function as a blunt way to find the square root of 121. For example, running

11
#eval search
search.{u_1} {α : Type u_1} (_f : Nat → Option α) (_start : Nat) : α
(fun n
Nat
=> 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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
n
Nat
* n
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
n
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.none
Option.none.{u} {α : Type u} : Option α
No value. 
) 0

will output

11

In a conventional programming language we can write this function without further ado, but Lean will not let us. And that is a good thing, because if it would, we could write a function that claims to calculate a value of any type α:

def anything
{α : Type u_1} → α
{α
Type u_1
} : α
Type u_1
:= search
search.{u_1} {α : Type u_1} (_f : Nat → Option α) (_start : Nat) : α
(fun _ => .none
Option.none.{u} {α : Type u} : Option α
No value. 
) 0

The existence of this function is bad news for Lean-the-theorem-prover! In Lean, propositions (statements to prove) are represented as types, and a proof of a proposition is represented as a term of that type. False propositions like 1 = 0 are therefore empty types, types that are not inhabited by any terms. But our anything function can have any type α we want, and thus would allow us to prove anything:

theorem boom
1 = 0
: 1 = 0 :=
All goals completed! 🐙
element_of_empty_type
Empty
:Empty
Empty : Type
The empty type. It has no constructors. The `Empty.rec`
eliminator expresses the fact that anything follows from the empty type.
1 =
Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
The 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)
0
All goals completed! 🐙

We certainly don't want to be able to prove 1 = 0, and so it is just for the better that Lean expects us to pay attention to termination.

Your options

As a Lean developer, you now have a few options when writing recursive definitions. On your menu are

  • writing structurally recursive functions

  • proving that your functions terminate, using well-founded recursion

  • not worrying about recursion and mark your functions as partial or even unsafe.

Each of them have their respective advantages and disadvantages, which we’ll discuss now.

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:

def search
{α : Type u_1} → (Nat → Option α) → Nat → Option α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) : Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> match
Pattern 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.
start
Nat
with
Pattern 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.
| 0 => .none
Option.none.{u} {α : Type u} : Option α
No value. 
| n
Nat
+1 => search
{α : Type u_1} → (Nat → Option α) → Nat → Option α
f
Nat → Option α
n
Nat

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

inductive Nat
Type
where | zero
Nat.zero : Nat
: Nat
Type
| succ
Nat.succ (n : Nat) : Nat
(n
Nat
: Nat
Type
) : Nat
Type

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_none
    ∀ {α : Type u_1} (start : Nat), search (fun x => none) start = none
    {α
    Type u_1
    } (start
    Nat
    : Nat
    Nat : Type
    The 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/)).
    
    ) : search
    search.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α
    (α := α
    Type u_1
    ) (fun _ => .none
    Option.none.{u} {α : Type u} : Option α
    No value. 
    ) start
    Nat
    = .none
    Option.none.{u} {α : Type u} : Option α
    No value. 
    :=
    All goals completed! 🐙
    α
    Type u_1
    :Type u_1
    search
    search.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α
    (fun x => none) Nat.zero
    Nat.zero : Nat
    `Nat.zero`, normally written `0 : Nat`, is the smallest natural number.
    This is one of the two constructors of `Nat`. 
    =
    Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
    The 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
    :Nat
    Nat : Type
    The 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/)).
    
    n_ih✝
    search (fun x => none) n✝ = none
    :search
    search.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α
    (fun x => none) n✝
    Nat
    =
    Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
    The 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
    search
    search.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α
    (fun x => none) (Nat.succ
    Nat.succ (n : Nat) : Nat
    The successor function on natural numbers, `succ n = n + 1`.
    This is one of the two constructors of `Nat`. 
    n✝
    Nat
    ) =
    Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
    The 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 =>
    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 _n
    Nat
    IH
    search (fun x => none) _n = none
    =>
    All goals completed! 🐙
  2. The defining equation of your function holds definitionally:

    example : search
    search.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α
    (fun n
    Nat
    => 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.
    
    Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
    function is problematic in that it would require `t` and `e` to be evaluated before
    calling the `ite` function, which would cause both sides of the `if` to be evaluated.
    Even if the result is discarded, this would be a big performance problem,
    and is undesirable for users in any case. To resolve this, `ite` is marked as
    `@[macro_inline]`, which means that it is unfolded during code generation, and
    the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
    the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
    until `c` is known.
    
    n
    Nat
    * n
    Nat
    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.
    
    Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
    function is problematic in that it would require `t` and `e` to be evaluated before
    calling the `ite` function, which would cause both sides of the `if` to be evaluated.
    Even if the result is discarded, this would be a big performance problem,
    and is undesirable for users in any case. To resolve this, `ite` is marked as
    `@[macro_inline]`, which means that it is unfolded during code generation, and
    the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
    the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
    until `c` is known.
    
    .some
    Option.some.{u} {α : Type u} (val : α) : Option α
    Some value of type `α`. 
    n
    Nat
    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.
    
    Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
    function is problematic in that it would require `t` and `e` to be evaluated before
    calling the `ite` function, which would cause both sides of the `if` to be evaluated.
    Even if the result is discarded, this would be a big performance problem,
    and is undesirable for users in any case. To resolve this, `ite` is marked as
    `@[macro_inline]`, which means that it is unfolded during code generation, and
    the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
    the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
    until `c` is known.
    
    .none
    Option.none.{u} {α : Type u} : Option α
    No value. 
    ) 100 = .some
    Option.some.{u} {α : Type u} (val : α) : Option α
    Some value of type `α`. 
    11 := rfl
    rfl.{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:

def fib
Nat → Nat
: Nat
Nat : Type
The 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/)).
Nat
Nat : Type
The 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/)).
| 0 => 0 | 1 => 1 | .succ
Nat.succ (n : Nat) : Nat
The successor function on natural numbers, `succ n = n + 1`.
This is one of the two constructors of `Nat`. 
(.succ
Nat.succ (n : Nat) : Nat
The successor function on natural numbers, `succ n = n + 1`.
This is one of the two constructors of `Nat`. 
n
Nat
) => fib
Nat → Nat
n
Nat
+ fib
Nat → Nat
(.succ
Nat.succ (n : Nat) : Nat
The successor function on natural numbers, `succ n = n + 1`.
This is one of the two constructors of `Nat`. 
n
Nat
)

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:

def search
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) (to
Nat
: Nat
Nat : Type
The 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/)).
) : Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> 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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
start
Nat
< to
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
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) 186:6-29 ? = Please use `termination_by` to specify a decreasing measure.search
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
f
Nat → Option α
(start
Nat
+ 1) to
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.none
Option.none.{u} {α : Type u} : Option α
No value. 

Notice the squiggly line beneath the recursive call search f (start + 1) to. 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) 186:6-29     ?  =
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!

Proving termination

Taking a step back, let us consider our function definition and ask: Why does it terminate? It terminates because it keeps making recursive calls only as long as start < to holds. Put differently, it makes at most to - start recursive calls. This forms a decreasing measure on the function arguments, and we can tell Lean about it using the termination_by annotation, which goes after the function definition:

def search
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) (to
Nat
: Nat
Nat : Type
The 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/)).
) : Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> 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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
start
Nat
< to
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
search
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
f
Nat → Option α
(start
Nat
+ 1) to
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.none
Option.none.{u} {α : Type u} : Option α
No value. 
termination_by search f start to => to
Nat
- start
Nat

The termination_by clause is followed by the function name (there could be multiple functions when you have mutual recursion; if there is only one you can write _ instead), the parameters and then after the arrow an expression that gets smaller in each recursive call.

With this information, Lean will notice that to - (start + 1) really is smaller than to - start, and therefore this function definition terminates. Here Lean finds the proof automatically, but we can also do the proof manually, by writing a decreasing_by clause with a tactic proof:

decreasing_by
  simp_wf
  apply Nat.sub_succ_lt_self
  assumption

After the simp_wf tactic, which cleans up some internal technicalities, we have to solve the goal

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

where we recognize the measure we specified in termination_by. It is worth noting that Lean understands that the recursive call is in the then branch of an if, and helpfully added the condition start < to as a hypothesis.

If you don't write a decreasing_by clause, then by default Lean uses

decreasing_by decreasing_tactic

The decreasing_tactic runs simp_wf, applies lexicographic ordering lemmas and then tries to use the extensible decreasing_trivial tactic to discharge the subgoals.

Often, the expression after termination_by is of type Nat. Then it is called a measure on the function arguments, and gives an upper bound on how often the function will make recursive calls. Generally, that expression can have any type α with a WellFoundedRelation α instance. This type class declares what it means for a value of α to be “smaller” to another (like < on Nat) and provides a proof that that relation is well-founded, meaning that starting from any value you can go to “smaller” values only a finite number of times.

Proofs about well-founded recursion

Proving theorems about our structurally recursive search variant was straight-forward, because we could use induction on the parameter start. With well-founded recursion this is not so easy: Simple induction on start or to will lead the proof into a different direction than the function definition, and that is rarely productive. Maybe we could introduce a variable that’s equal to to - start and perform induction on that, or use a suitable induction principle like Mathlib’s Nat.le_induction. But more often that not it's easiest to write the proof itself as a recursive definition, following the same recursion structure as the function:

theorem search_const_none
∀ {α : Type u_1} (start to : Nat), search (fun x => none) start to = none
{α
Type u_1
} (start
Nat
to
Nat
: Nat
Nat : Type
The 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/)).
) : search
search.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) : Option α
(α := α
Type u_1
) (fun _ => .none
Option.none.{u} {α : Type u} : Option α
No value. 
) start
Nat
to
Nat
= .none
Option.none.{u} {α : Type u} : Option α
No value. 
:=
All goals completed! 🐙
α
Type u_1
:Type u_1
start
Nat
:Nat
Nat : Type
The 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/)).
to
Nat
:Nat
Nat : Type
The 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/)).
(if start
Nat
<
LT.lt.{u} {α : Type u} [self : LT α] (a✝a✝¹ : α) : Prop
The less-than relation: `x < y` 
to
Nat
then search
search.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) : Option α
(fun x => none) (start
Nat
+
HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] (a✝ : α) (a✝¹ : β) : γ
`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 
1) to
Nat
else none) =
Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
The 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
inl
α
Type u_1
:Type u_1
start
Nat
:Nat
Nat : Type
The 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/)).
to
Nat
:Nat
Nat : Type
The 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/)).
h✝
start < to
:start
Nat
<
LT.lt.{u} {α : Type u} [self : LT α] (a✝a✝¹ : α) : Prop
The less-than relation: `x < y` 
to
Nat
search
search.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) : Option α
(fun x => none) (start
Nat
+
HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] (a✝ : α) (a✝¹ : β) : γ
`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 
1) to
Nat
=
Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
The 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
inr
α
Type u_1
:Type u_1
start
Nat
:Nat
Nat : Type
The 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/)).
to
Nat
:Nat
Nat : Type
The 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/)).
h✝
¬start < to
:¬
Not (a : Prop) : Prop
`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
start
Nat
<
LT.lt.{u} {α : Type u} [self : LT α] (a✝a✝¹ : α) : Prop
The less-than relation: `x < y` 
to
Nat
none =
Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
The 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
inl
α
Type u_1
:Type u_1
start
Nat
:Nat
Nat : Type
The 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/)).
to
Nat
:Nat
Nat : Type
The 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/)).
h✝
start < to
:start
Nat
<
LT.lt.{u} {α : Type u} [self : LT α] (a✝a✝¹ : α) : Prop
The less-than relation: `x < y` 
to
Nat
search
search.{u_1} {α : Type u_1} (f : Nat → Option α) (start to : Nat) : Option α
(fun x => none) (start
Nat
+
HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] (a✝ : α) (a✝¹ : β) : γ
`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 
1) to
Nat
=
Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
The 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
All goals completed! 🐙
inr
α
Type u_1
:Type u_1
start
Nat
:Nat
Nat : Type
The 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/)).
to
Nat
:Nat
Nat : Type
The 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/)).
h✝
¬start < to
:¬
Not (a : Prop) : Prop
`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
start
Nat
<
LT.lt.{u} {α : Type u} [self : LT α] (a✝a✝¹ : α) : Prop
The less-than relation: `x < y` 
to
Nat
none =
Eq.{u_1} {α : Sort u_1} (a✝a✝¹ : α) : Prop
The 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
All goals completed! 🐙
termination_by _ start to => to
Nat
- start
Nat

The unfold search step exposes the function definition's if start < to then … else, the split then proceeds into the two branches, and in the first case we use the theorem we are currently defining. This seemingly circular reasoning is then justified by the termination checker, which we have to help out with termination_by, just like above.

It is one of the perks of proving theorems in a system based on dependent type theory that the tools we have to define functions can also be used to prove theorems!

Nevertheless, it is a bit silly to repeat the whole termination argument at every proof about search. In the future, Lean will generate a bespoke induction principle for each recursive function, which should simplify these proofs considerably.

As you prove more theorems about your function you might notice that you often have to explicitly unfold it (e.g. using unfold search, rw [search] or simp [search]) where you may expect an equality to hold just by definition. This is one of the downsides of definitions using well-founded recursion: the defining equation no longer holds by definition, but is merely a propositional equality proved by Lean for you, in the theorem search._unfold:

search._unfold.{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#check search._unfold
search._unfold.{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
search._unfold.{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

Nested recursion

Well-founded recursion can handle nested recursion, where the recursive call is an argument to another higher-order function. A typical occurrence of that pattern is if you have an inductive type (here Tree) whose definition includes a recursive occurrence of itself inside some other type (here List):

inductive
In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructor.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).
Tree
Type → Type
(α
Type
: Type) where | node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
: α
Type
List
List.{u} (α : Type u) : Type u
`List α` is the type of ordered lists with elements of type `α`.
It is implemented as a linked list.

`List α` is isomorphic to `Array α`, but they are useful for different things:
* `List α` is easier for reasoning, and
  `Array α` is modeled as a wrapper around `List α`
* `List α` works well as a persistent data structure, when many copies of the
  tail are shared. When the value is not shared, `Array α` will have better
  performance because it can do destructive updates.
(Tree
Type → Type
α
Type
) Tree
Type → Type
α
Type

A naive implementation of Tree.map like

def fail to show termination for
  Tree.map
with errors
structural recursion cannot be used

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 tsTree.map
{α β : Type} → (α → β) → Tree α → Tree β
{α
Type
β
Type
} (f
α → β
: α
Type
β
Type
) : Tree
Tree (α : Type) : Type
α
Type
Tree
Tree (α : Type) : Type
β
Type
| node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
v
α
ts
List (Tree α)
=> node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
(f
α → β
v
α
) (List.map
List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β
`O(|l|)`. `map f l` applies `f` to each element of the list.
* `map f [a, b, c] = [f a, f b, f c]`
(fun t
Tree α
=> Tree.map
{α β : Type} → (α → β) → Tree α → Tree β
f
α → β
t
Tree α
) ts
List (Tree α)
)

will not be accepted as-is. Lean does not find a termination argument and suggests we use termination_by. With

def Tree.map
{α β : Type} → (α → β) → Tree α → Tree β
{α
Type
β
Type
} (f
α → β
: α
Type
β
Type
) : Tree
Tree (α : Type) : Type
α
Type
Tree
Tree (α : Type) : Type
β
Type
| node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
v
α
ts
List (Tree α)
=> node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
(f
α → β
v
α
) (List.map
List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β
`O(|l|)`. `map f l` applies `f` to each element of the list.
* `map f [a, b, c] = [f a, f b, f c]`
(fun t
Tree α
=> 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 tsTree.map
{α β : Type} → (α → β) → Tree α → Tree β
f
α → β
t
Tree α
) ts
List (Tree α)
) termination_by _ f t => t
Tree α

we clarify that; now the recursive call has a squiggly underline with the following error message:

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

We recognize v and ts as the fields of our tree, t as the tree in the argument to List.map, and quite reasonably Lean tries to prove that t is in some sense smaller than the argument to Tree.map. The sizeOf : Tree α → Nat function was automatically generated by Lean when we defined the Tree inductive data type.

But note that nothing in this proof goal connects t to ts. The variable t is an arbitrary Tree! This is because Lean does not know that List.map f l calls its argument only on elements on l. So in this form, the proof goal is unsolvable.

The cure for this problem is called List.attach, a function defined in the standard library (so import Std if you haven't already) with type

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

It replaces each element x in the list l with a pair consisting of the element x, and a proof x ∈ l that the element is in the list. We can use this function before Lift.map, ignore the proof in the argument to List.map, and suddenly Lean accepts the definition:

def Tree.map
{α β : Type} → (α → β) → Tree α → Tree β
{α
Type
β
Type
} (f
α → β
: α
Type
β
Type
) : Tree
Tree (α : Type) : Type
α
Type
Tree
Tree (α : Type) : Type
β
Type
| node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
v
α
ts
List (Tree α)
=> node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
(f
α → β
v
α
) (List.map
List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β
`O(|l|)`. `map f l` applies `f` to each element of the list.
* `map f [a, b, c] = [f a, f b, f c]`
(fun t
Tree α
, unused variable `h` [linter.unusedVariables]h
t ∈ ts
=> Tree.map
{α β : Type} → (α → β) → Tree α → Tree β
f
α → β
t
Tree α
) ts
List (Tree α)
.attach
List.attach.{u_1} {α : Type u_1} (l : List α) : List { x // x ∈ l }
"Attach" the proof that the elements of `l` are in `l` to produce a new list
with the same elements but in the type `{x // x ∈ l}`. 
)

How does this work when we didn't even use the proof? To understand that, let us spell out the termination proof:

def Tree.map
{α β : Type} → (α → β) → Tree α → Tree β
{α
Type
β
Type
} (f
α → β
: α
Type
β
Type
) : Tree
Tree (α : Type) : Type
α
Type
Tree
Tree (α : Type) : Type
β
Type
| node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
v
α
ts
List (Tree α)
=> node
Tree.node {α : Type} (a✝ : α) (a✝¹ : List (Tree α)) : Tree α
(f
α → β
v
α
) (List.map
List.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β
`O(|l|)`. `map f l` applies `f` to each element of the list.
* `map f [a, b, c] = [f a, f b, f c]`
(fun t
Tree α
, unused variable `h` [linter.unusedVariables]h
t ∈ ts
=> Tree.map
{α β : Type} → (α → β) → Tree α → Tree β
f
α → β
t
Tree α
) ts
List (Tree α)
.attach
List.attach.{u_1} {α : Type u_1} (l : List α) : List { x // x ∈ l }
"Attach" the proof that the elements of `l` are in `l` to produce a new list
with the same elements but in the type `{x // x ∈ l}`. 
) termination_by _ f t => t
Tree α
decreasing_by
α
Type
:Type
v
α
:α
Type
ts
List (Tree α)
:List
List.{u} (α : Type u) : Type u
`List α` is the type of ordered lists with elements of type `α`.
It is implemented as a linked list.

`List α` is isomorphic to `Array α`, but they are useful for different things:
* `List α` is easier for reasoning, and
  `Array α` is modeled as a wrapper around `List α`
* `List α` works well as a persistent data structure, when many copies of the
  tail are shared. When the value is not shared, `Array α` will have better
  performance because it can do destructive updates.
(Tree
Tree (α : Type) : Type
α
Type
)
t
Tree α
:Tree
Tree (α : Type) : Type
α
Type
h
t ∈ ts
:t
Tree α
Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] (a✝ : α) (a✝¹ : γ) : Prop
The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 
ts
List (Tree α)
sizeOf
SizeOf.sizeOf.{u} {α : Sort u} [self : SizeOf α] (a✝ : α) : Nat
The "size" of an element, a natural number which decreases on fields of
each inductive type. 
t
Tree α
<
LT.lt.{u} {α : Type u} [self : LT α] (a✝a✝¹ : α) : Prop
The less-than relation: `x < y` 
1 +
HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] (a✝ : α) (a✝¹ : β) : γ
`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 
sizeOf
SizeOf.sizeOf.{u} {α : Sort u} [self : SizeOf α] (a✝ : α) : Nat
The "size" of an element, a natural number which decreases on fields of
each inductive type. 
ts
List (Tree α)
All goals completed! 🐙

After simp_wf the proof goal reads

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

and we now see the crucial hypothesis t ∈ ts that connects t to ts, and makes this proof obligation provable. The default tactic decreasing_trivial recognizes this pattern and closes the proof for us.

So if you struggle defining a function with nested recursion, try List.attach or search for a similar function for your data type.

Lexicographic orders

For some functions, the termination argument is not merely that a single measure (i.e. a function from the function arguments to Nat) decreases, but we have two (or more) measures, and at each recursive call, either the first measure decreases, or the first stays the same and the second decreases. This combined order is called the lexicographic order, and is well-supported by Lean, as in this example:

def ackermann
Nat → Nat → Nat
: Nat
Nat : Type
The 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/)).
Nat
Nat : Type
The 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/)).
Nat
Nat : Type
The 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/)).
| 0, m
Nat
=> m
Nat
+ 1 | n
Nat
+ 1, 0 => ackermann
Nat → Nat → Nat
n
Nat
1 | n
Nat
+ 1, m
Nat
+ 1 => ackermann
Nat → Nat → Nat
n
Nat
(ackermann
Nat → Nat → Nat
(n
Nat
+ 1) m
Nat
) termination_by _ n m => (n
Nat
, m
Nat
)

For tuples, Lean by default uses the lexicographic order, and here Lean figures out that in each recursive call, either n gets smaller, or n stays the same and m gets smaller.

Mutual recursion

Well-founded recursion can also be used to define mutually-recursive functions. Imagine we want to split our search function into two functions, one that checks f n and a second one that increases n – maybe because we want to be able to call both variants. We can put the two functions into a mutual block:

mutual
def search
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) (to
Nat
: Nat
Nat : Type
The 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/)).
) : Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> searchAbove
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
f
Nat → Option α
start
Nat
to
Nat
def searchAbove
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) (to
Nat
: Nat
Nat : Type
The 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/)).
) : Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
:= 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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
start
Nat
< to
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
search
{α : Type u_1} → (Nat → Option α) → Nat → Nat → Option α
f
Nat → Option α
(start
Nat
+ 1) to
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.none
Option.none.{u} {α : Type u} : Option α
No value. 
end termination_by search f start to => (to
Nat
- start
Nat
, 1) searchAbove f start to => (to
Nat
- start
Nat
, 0)

We have to specify a termination measure for each function – this justifies why the termination_by syntax requires a function name.

In this example the call from search to searchAbove does not change the parameters at all. How can we hope to prove this definition terminating? Since the calls from searchAbove to search have decreasing arguments, it suffices if calls from search to searchAbove are equal. We can express that using a lexicographic ordering, where the first component is our usual termination measure (to - start) and the second component is simply the constant 1 for search and 0 for searchAbove. In this order, the call from search to searchAbove is decreasing, because the second component decreases.

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:

partial def search
{α : Type u_1} → (Nat → Option α) → Nat → Option α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) : Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> search
{α : Type u_1} → (Nat → Option α) → Nat → Option α
f
Nat → Option α
(start
Nat
+ 1)

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

some 11
#eval search
search.{u_1} {α : Type u_1} (f : Nat → Option α) (start : Nat) : Option α
(fun n
Nat
=> 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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
n
Nat
* n
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
n
Nat
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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
.none
Option.none.{u} {α : Type u} : Option α
No value. 
) 0

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:

unsafe def search
{α : Type u_1} → (Nat → Option α) → Nat → α
{α
Type u_1
} (f
Nat → Option α
: Nat
Nat : Type
The 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/)).
Option
Option.{u} (α : Type u) : Type u
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.

For example, the function `HashMap.find? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.

To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none
```
α
Type u_1
) (start
Nat
: Nat
Nat : Type
The 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/)).
) : α
Type u_1
:= match
Pattern 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.
f
Nat → Option α
start
Nat
with
Pattern 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.
| .some
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type `α`. 
x
α
=> x
α
| .none
Option.none.{u} {α : Type u} : Option α
No value. 
=> search
{α : Type u_1} → (Nat → Option α) → Nat → α
f
Nat → Option α
(start
Nat
+ 1)

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.

Conclusion

We have come full circle: Starting with code that you might write in another functional programming language, we saw why this can't just go through in Lean. We learned how to convince Lean that a function definition is fine by using structural and well-founded recursion, and saw that well-founded recursion is very general and powerful, but also not necessarily easy to use. Luckily, we do not have to deal with any of that if we just want to write programs, as Lean lets us opt out of termination checking with partial and unsafe.

The Lean FRO has improvements to recursive definitions on its roadmap, and future versions of Lean will generate induction principles from recursive functions, support mutual structural recursion and more. And if there is something that Lean could do differently here to make your Lean programming experience more pleasant, please let us know!