1. Lean and its type theory🔗

This part covers Lean both as a practical proof assistant and as the dependent type theory it is built on. We begin with the natural numbers — which comes with its constructors as well as with reduction rules. We then turn to types and the universe hierarchy — including how to define your own types with inductive and structure — then functions and terms and the typeclass system. Finally comes the theory: the Curry-Howard correspondence tying propositions to types and proofs to terms (and, with it, how to prove things interactively), dependent types, and notation. (Several reference topics — the alphabetical tactic glossary, how a Lean file is organized, Lean's brackets, equality and reduction, the diagnostic commands, and Navigating Mathlib — are covered in the Appendix; the deeper foundations, the axioms of Lean and well-foundedness, are treated in the Mathematics part.)

1.1. Introduction🔗

We begin with the natural numbers, ℕ (notation for the type Nat), as a running example.

1.1.1. The natural numbers🔗

Nat is an inductive type: it is generated by a fixed list of constructors (the different possibilities to construct a natural number), the basic ways to build a value. Nat has exactly two (read a : b as a is a term of type b, and a → b as the type of maps from a to b, and succ means the successor of a natural number):

Nat.zero : Nat
Nat.succ : Nat → Nat

so every natural number is either Nat.zero is 0, or the successor of another natural number, so Nat.succ Nat.zero is 1, Nat.succ (Nat.succ Nat.zero) is 2, and so on. (The numerals 0, 1, 2 are just notation for these terms.) The general inductive declaration comes later; here we need only Nat.

These two constructors are Giuseppe Peano's axiomatization of 1889: a zero, a successor, and induction. Induction is not a third constructor. It is the recursor, generated together with the type, and it is the subject of the next paragraph.

Generated alongside the type is the recursor Nat.rec. The constructors build a value; the recursor consumes one. With other words, it is the primitive way to define a function with domain Nat. To define some f : Nat → C (where C is some type), you supply two things: a base value base : C for the zero case (i.e. f 0 := base, where f 0 is the Lean way to write f(0)), and a step : Nat → C → C such that, for succ n (which equals n + 1), you may reuse both n and the result already computed for n, i.e. you define in this way f (n + 1) := step n (f n). (Note the important notation here: We write α → β → γ — with implicit brackets g : α → (β → γ) for a function g mapping every a : α to a function β → γ. So, g a b : γ. Application brackets the other way: g a b means (g a) b, first g a : β → γ, then that function applied to b. Arrows omit brackets on the right, application omits them on the left, and the two fit together. You only write brackets where an argument is itself an application, as in step n (f n); see Different parentheses. In other words, this is the Lean and more flexible way to write a function depending on two variables.)

Noting the example keyword, as well as the inputs C, base, step, we define the terms of type Nat → C by introducing a function (using the fun keyword, and the mapping rule):

example (C : Type) (base : C) (step : Nat → C → C) :
    Nat → C :=
  fun n ↦ Nat.rec base step n

Pattern matching and the cases and induction tactics all compile down to Nat.rec. (A more general form lets the result type vary with the Nat, which unifies recursion with the induction principle. It needs universes, so it comes with the inductive types.)

Nat.rec computes. Applied to a value that is literally one of the two constructors, it selects the matching case by the iota rule (ι), made precise below (numerals such as 2 are put into constructor form first, so the rule applies to them too):

Nat.rec base step Nat.zero      ⟶ base
Nat.rec base step (Nat.succ n)  ⟶ step n (Nat.rec base step n)

As an example, define "double" through the recursor and reduce it on 2. The keyword def opens the definition, myDouble is the name, n : Nat the input, and _ an unused variable:

def step (_ j : Nat) : Nat := j + 2

def myDouble (n : Nat) : Nat :=
  Nat.rec 0 step n

--   myDouble 2
-- ⟶ Nat.rec 0 step 2                -- δ: unfold myDouble
-- ⟶ step 1 (Nat.rec 0 step 1)       -- ι on succ, then δβ
-- ⟶ (Nat.rec 0 step 1) + 2          -- δ: unfold step
-- ⟶ (step 0 (Nat.rec 0 step 0)) + 2 -- ι again
-- ⟶ ((Nat.rec 0 step 0) + 2) + 2    -- δ: unfold step
-- ⟶ (0 + 2) + 2  ⟶  4               -- ι on zero, then +
example : myDouble 2 = 4 := rfl

myDouble 2 = 4 needs no proof beyond rfl, Lean's way of saying that two terms are definitionally equal: both sides reduce to a common form. The rest of this chapter names those reduction steps and says when two terms are the same by computation.

1.1.2. Definitional equality and `rfl`🔗

Terms in Lean reduce, by a fixed set of steps, toward a simpler form — (fun x => x + 1) 4 becomes 5, and 2 + 2 becomes 4. Each such step is called a reduction and is written term ⟶ simpler term. Two terms are definitionally equal — also judgmentally equal, written a ≡ b — when they reduce to a common form, and Lean's kernel then treats them as fully interchangeable, in particular when it compares types during type-checking. That comparison test is called conversion (or defeq checking). Definitional equality must be kept apart from propositional equality a = b, which is itself a Prop and may require a genuine proof; the full three-way distinction — syntactic, definitional, propositional — is laid out in the appendix on equality.

The tactic rfl proves exactly a definitional equality. That is why goals whose two sides are written differently but reduce to the same thing close by rfl:

example : 2 + 2 = 4 := rfl
example : Nat.succ 0 = 1 := rfl

The #eval command (used throughout the chapter on terms) runs the same reduction and prints the value. rfl, #eval and every "reduces to" below are the same phenomenon. The steps are the kernel's reduction rules; they recur whenever a later step is claimed to hold "by definition".

The reduction rules🔗

Definitional equality is generated by a fixed list of reduction rules that the kernel applies to compute terms. Most of the names come from the lambda calculus of Alonzo Church in the 1930s, where functions are written fun x => e and each rewriting rule carries a Greek letter. Lean's kernel uses six of them:

Rule	Technical name	What it does	Example
α (alpha)	α-conversion	rename a bound variable	`fun x => x` and `fun y => y` agree
β (beta)	β-reduction	apply a function: substitute the argument	`(fun x => x + 1) 4 ⟶ 4 + 1`
η (eta)	η-conversion	a function equals its expansion `fun x => f x`	`fun x => f x ⟶ f`
δ (delta)	δ-reduction	unfold a definition: replace a constant by its value	`twice 3 ⟶ 2 * 3`
ι (iota)	ι-reduction	run a recursor on a constructor	`Nat.rec base step (n+1) ⟶ step n (Nat.rec base step n)`
ζ (zeta)	ζ-reduction	substitute a `let`-binding	`let x := 4; x + x ⟶ 4 + 4`

Here are some examples:

-- beta, then arithmetic computes (delta + iota)
example : (fun x => x + 1) 4 = 5 := rfl
example : 2 + 2 = 4 := rfl
example : List.length [7, 8, 9] = 3 := rfl

-- eta: a function equals its eta-expansion
example (f : Nat → Nat) : (fun x => f x) = f := rfl

-- zeta: a `let` unfolds
example : (let x := 4; x + x) = 8 := rfl

-- iota: a recursor applied to a constructor
example (b : Nat) (s : Nat → Nat → Nat) :
    Nat.rec (motive := fun _ => Nat) b s 0 = b := rfl
example (b : Nat) (s : Nat → Nat → Nat) (n : Nat) :
    Nat.rec (motive := fun _ => Nat) b s (n + 1)
      = s n (Nat.rec b s n) := rfl

-- delta + iota: a defined function on a literal
def twice (n : Nat) : Nat := 2 * n
example : twice 3 = 6 := rfl

Conversely, rfl fails when no chain of reductions connects the two sides — typically when a variable blocks computation. Nat's addition is defined by recursion on its second argument, so n + 0 fires the ι rule and reduces to n, whereas 0 + n is stuck: with n a bare variable there is no constructor for the recursor to fire on.

-- `n + 0` reduces to `n`, so this is `rfl`:
example (n : Nat) : n + 0 = n := rfl

Here, the red squiggly line indicates an error, i.e. a proof which does not work.

-- `0 + n` is stuck (nothing to recurse on), so `rfl`
-- fails and you need induction (see below) instead:
example (n : Nat) : 0 + n = n := Type mismatch
  rfl
has type
  ?m.9 = ?m.9
but is expected to have type
  0 + n = nrfl

To actually prove 0 + n = n you must run the recursor yourself, and for that you need induction — the full Nat.rec, which hands you the induction hypothesis for the predecessor:

example (n : Nat) : 0 + n = n := byn:ℕ⊢ 0 + n = n
  induction n with
  | zero =>zero⊢ 0 + 0 = 0 rflAll goals completed! 🐙
  | succ k ih =>succk:ℕih:0 + k = k⊢ 0 + (k + 1) = k + 1
      -- goal: 0 + (k + 1) = k + 1
      -- ι reduces the LHS to succ (0 + k);
      -- `Nat.add_succ` makes that step explicit,
      -- then `ih : 0 + k = k` closes it.
      rw [Nat.add_succ,succk:ℕih:0 + k = k⊢ (0 + k).succ = k + 1 ihsucck:ℕih:0 + k = k⊢ k.succ = k + 1]All goals completed! 🐙

(Here, rw [...] rewrites the goal using an equation; see the rw tactic.) Note that rw [ih] alone fails here: the goal reads 0 + (k + 1) = k + 1, and the subterm 0 + k is not yet visible — it only appears after the ι step 0 + succ k ⟶ succ (0 + k), which Nat.add_succ performs. This is the same stuck-until-a-constructor-shows-up phenomenon one level down.

Recognizing when a goal is "true by reduction" — and therefore closed by rfl — is one of the most useful instincts to develop.

Reducibility, weak head normal form, and decidability

How eagerly the δ rule fires is governed by reducibility annotations: a @[reducible] definition is unfolded freely, an ordinary def is unfolded on demand, and an @[irreducible] one is left folded. And the kernel usually does not reduce all the way to a normal form; it stops at weak head normal form (WHNF) — just far enough to expose the outermost constructor or binder — which is all that comparing two terms requires. On the terms that occur in practice this terminates, so rfl and the type checker give an answer. In full generality definitional equality in Lean is undecidable, and the checker is sound but incomplete: there are equal terms on which it fails (next chapter). The counterexamples are constructed and need Acc.rec, the recursor of well-founded recursion, on proofs.

1.1.3. Bool🔗

Bool is simpler than Nat: two values, true and false, and two constructors, neither taking an argument. Its definition, from Lean's core library (where introduces the constructors):

inductive type

Bool : Type
Bool : Type

The Boolean values, true and false.

Logically speaking, this is equivalent to Prop (the type of propositions). The distinction is public important for programming: both propositions and their proofs are erased in the code generator, while Bool corresponds to the Boolean type in most programming languages and carries precisely one bit of run-time information.

Constructors

Bool.false : Bool

The Boolean value false, not to be confused with the proposition False.

Bool.true : Bool

The Boolean value true, not to be confused with the proposition True.

Its recursor Bool.rec consumes a Bool by offering one value for each constructor — first the false case, then the true case — and returns the matching one. Into a fixed result C : Type, its (non-dependent) signature is just this, exactly as Nat.rec above:

-- the `false` case first, then the `true` case:
Bool.rec : C → C → Bool → C

This is exactly an if-then-else: reading Bool.rec e f b as "if b then f else e" (note the order: the false result e comes first). Applied to a literal constructor it reduces by the ι rule (the reduction rules below). Equivalently (and definitionally equal) is the following construction (read bif as Boolean if):

-- `bif true …` picks the then-branch:
example :
    (bif true  then "Hi" else "Salut") = "Hi" := rfl
-- and in general `bif b then f else e` is `Bool.rec e f b`:
example {α : Type} (e f : α) :
    (bif false then f else e) = Bool.rec e f false := rfl

Note, as above in the 0 + n = n example, the bif fails to reduce if the value of b is unknown:

example (b : Bool) :
    (bif b then "Hi" else "Salut")
      = Bool.rec "Salut" "Hi" b := byb:Bool⊢ (bif b then "Hi" else "Salut") = Bool.rec "Salut" "Hi" b
  Tactic `rfl` failed: The left-hand side
  bif b then "Hi" else "Salut"
is not definitionally equal to the right-hand side
  Bool.rec "Salut" "Hi" b

b:Bool⊢ (bif b then "Hi" else "Salut") = Bool.rec "Salut" "Hi" brflb:Bool⊢ (bif b then "Hi" else "Salut") = Bool.rec "Salut" "Hi" b

The fix is to make a case analysis as follows (cases is a simpler form of induction; see cases and induction):

example (b : Bool) :
    (bif b then "Hi" else "Salut")
      = Bool.rec "Salut" "Hi" b := byb:Bool⊢ (bif b then "Hi" else "Salut") = Bool.rec "Salut" "Hi" b
  cases bfalse⊢ (bif false then "Hi" else "Salut") = Bool.rec "Salut" "Hi" falsetrue⊢ (bif true then "Hi" else "Salut") = Bool.rec "Salut" "Hi" true <;>false⊢ (bif false then "Hi" else "Salut") = Bool.rec "Salut" "Hi" falsetrue⊢ (bif true then "Hi" else "Salut") = Bool.rec "Salut" "Hi" true rflAll goals completed! 🐙

Note that Bool also carries the usual &&, ||, !.

Instead of calling Bool.rec by hand, you can define a function on Bool by pattern matching: one line per constructor, introduced by |, giving the result for that constructor.

def myNot : Bool → Bool
  | false => true
  | true  => false

example : myNot false = true := rfl

Lean translates such a definition into the recursor, so on constructors it reduces just as Bool.rec does. Pattern matching works for every inductive type, including recursive ones like Nat; it is treated in detail in the chapter on terms.

How bif is defined under the hood

Internally, Lean does not build runnable definitions from Bool.rec directly — the code generator cannot compile a bare recursor, whereas it can compile a match. So bif is not primitive: it is notation for a function cond, which does the actual branching with a match (the inline form of pattern matching, see the chapter on terms):

-- the underlying function, defined by matching on `c`:
def cond {α : Type} (c : Bool) (x y : α) : α :=
  match c with
  | true  => x
  | false => y

-- `bif` is *notation* that expands to a `cond` call:
macro "bif " c:term " then " t:term " else " e:term :
    term => `(cond $c $t $e)

1.1.4. The propositions `True` and `False`🔗

Both types in this section live in Prop, the universe of propositions. Unlike Bool, Nat, or the True and False below — each an inductive type whose definition you can read off — Prop has no such definition. It is not an inductive type, and there is no def Prop := … to unfold; asking Lean to print it (#print Prop) even fails, because there is nothing written in Lean to print. Instead, Prop is a primitive, baked directly into Lean's kernel: it is the bottom universe Sort 0 (with Type u being Sort (u+1); more on the universe hierarchy in the next chapter). What makes Prop usable is therefore not a definition but the rules the kernel attaches to it — proof irrelevance and the rest, taken up in why Prop is special.

The trivial proposition True. True is the proposition that always holds. Being a Prop, its terms are proofs. It has a single constructor, taking no argument, which is therefore already a complete proof of it (note that the type after the colon is now Prop, not Type):

inductive proposition

True : Prop
True : Prop

True is a proposition and has only an introduction rule, True.intro : True. In other words, True is simply true, and has a canonical proof, True.intro For more information: Propositional Logic

Constructors

True.intro : True

True is true, and True.intro (or more commonly, trivial) is the proof.

So proving True is as easy as naming that constructor:

example : True := True.intro
example : True := trivial
example : True := by⊢ True trivialAll goals completed! 🐙

The term trivial is nothing but a name for this constructor (theorem trivial : True := True.intro), and on a goal True the trivial tactic does exactly this. The tactic also tries a few other simple steps, such as rfl and assumption, before it gives up.

Its recursor has exactly one case, for the single constructor True.intro, so into a fixed result type C its (non-dependent) signature is:

-- one constructor, hence one case:
True.rec : C → True → C

There is correspondingly nothing to learn from a proof of True: the recursor just hands back the value you supplied for that one case (True.rec c h reduces to c), which is why True carries no information.

The empty proposition False. False is the opposite extreme: the proposition that is never true. It is the inductive type with no constructors at all — so its definition has no where clause and no | lines:

inductive proposition

False : Prop
False : Prop

False is the empty proposition. Thus, it has no introduction rules. It represents a contradiction. False elimination rule, False.rec, expresses the fact that anything follows from a contradiction. This rule is sometimes called ex falso (short for ex falso sequitur quodlibet), or the principle of explosion. For more information: Propositional Logic

Constructors

With no constructor there is no way to build a term of False, as it must be for a statement that has no proof. Its recursor, in full (the result universe Sort u is treated in the next chapter):

False.rec : (motive : False → Sort u) → (t : False) → motive t

Implicit vs. explicit motive: why False.rec looks different

This looks different from Bool.rec and True.rec above for one reason — implicit versus explicit: there the motive sat in curly braces {motive …} and Lean inferred it from the case values, which is why we could drop it and even present those signatures non-dependently as C → C → Bool → C and C → True → C. False has no case values, so nothing lets Lean infer the motive; it is therefore explicit (round brackets (motive …)), and you must supply it — you write False.rec (fun _ => C) h, or False.rec _ h letting the goal fix it, but never plain False.rec h (which would read h as the motive). Note also that between the motive and the input t there is no case argument at all — Bool.rec had two there, True.rec one, False.rec none — which is exactly why its result motive t may be of any type: the principle ex falso quodlibet ("from a falsehood, anything follows"). The filled-in form is packaged as False.elim, so that False.elim h = False.rec (fun _ => C) h.

For ex falso quodlibet, Lean does not use False.rec but False.elim, which is the following:

def False.elim {C : Sort u} (h : False) : C :=
  False.rec (fun _ => C) h

example (h : False) : 0 = 1 := False.elim h
example (h : False) (P : Prop) : P := h.elim

This is exactly why False is so important for consistency. Because False.elim turns a single proof of False into a proof of every proposition P (the second example above), one term of type False would make every statement a theorem — and the logic would no longer distinguish the provable from the false.