Functions🔗

We now focus on the \lambda-calculus aspect of Lean's type theory. Functions are given by \lambda-abstractions.

example : ℕ → ℕ := λ n ↦ n + 1

This is syntactic sugar for

example : ℕ → ℕ := fun n => n + 1

Here ℕ → ℕ is a function type. More generally, a function type is denoted by α → β, where α and β are types specifying the domain and codomain, respectively. As any other expression, ℕ → ℕ has a type.

example : Type := ℕ → ℕ

We can give a name to a function by replacing example with def and the name.

def plus1 : ℕ → ℕ := λ n ↦ n + 1

The command #eval evaluates a given expression.[…]Parentheses are not needed in function evaluation syntax.

1#eval plus1 0

Lean is a proof assistant and a functional programming language. One may think of #check and #eval as reflecting these two sides. We will focus on the proof assistant features and favor a proof over #eval.

example : plus1 0 = 1 := rfl

Arguments🔗

The domain of a function may be specified by annotating its argument with a type. Then Lean can often infer the codomain.

def plus1₁ := λ n : ℕ ↦ n + 1

Syntactic sugar allows for introducing the argument using parentheses.

def plus1₂ (n : ℕ) := n + 1

Yet another way is to introduce a variable in the surrounding context.

variable (n : ℕ)
def plus1₃ := n + 1

The functions plus1₁, plus1₂, and plus1₃ coincide with plus1.

Several arguments🔗

Functions take exactly one argument in Lean. A function taking several arguments can be encoded as a function whose codomain is a function type.

def add : ℕ → (ℕ → ℕ) := λ n ↦ (λ m ↦ n + m)

We refer to a function like this simply as a function taking two arguments. Syntactic sugar creates the appearance of functions taking several arguments.

def add₁ : ℕ → ℕ → ℕ := λ n m ↦ n + m

When viewing add₁ as a function taking two arguments, we refer to the final ℕ in ℕ → ℕ → ℕ as the codomain. The arguments may be introduced using parentheses, and we can also make use of the variable n that we defined above.

def add₂ (n : ℕ) (m : ℕ) : ℕ := n + m
def add₃ (n m : ℕ) : ℕ := n + m
def add₄ (m : ℕ) : ℕ := n + m

All this is syntactic sugar. The functions add₁, …, add₄ coincide with add.

Partial application produces a function taking the remaining arguments.

def plus1' : ℕ → ℕ := add 1

In contrast, saturated application produces an expression that is not a function.

example : ℕ := add 1 0

The following function taking two arguments ignores the second one.

def proj : ℕ → ℕ → ℕ := λ n _ ↦ n

example : proj 0 1 = 0 := rfl

Types as arguments🔗

Recall that Prod encodes the Cartesian product. It is a function taking types as arguments.

example : Type → Type → Type := Prod

In fact, Prod is a more general universe-polymorphic function.[…]We will return to the maximum appearing in the codomain.

example : Type u → Type v → Type (max u v) := Prod

Here are some variations.

def Prod₁ (t : Type) (s : Type) : Type := Prod t s
def Prod₂ : Type → Type → Type := Prod
def Prod₃ : Type → Type → Type := λ t ↦ λ s ↦ t × s
def Prod₄ (t s : Type) : Type := t × s

The functions Prod₁, …, Prod₄ all coincide with Prod, though, they are instantiated with a fixed level of the universe hierarchy.

Implicit arguments🔗

Recall that if two expressions are definitionally equal, then their equality can be proven using rfl. In fact, rfl is a function taking two implicit arguments.

rfl.{u} {α : Sort u} {a : α} : a = a#check rfl

Implicit arguments are written using curly braces {…}. Lean infers their values from context.

example : {α : Sort u} → {a : α} → a = a := rfl
example {α : Sort u} {a : α} : a = a := rfl

Inference of implicit arguments can be disabled using @.

example : (α : Sort u) → (a : α) → a = a := @rfl
example (α : Sort u) (a : α) : a = a := @rfl α a

Like Prod, @rfl is a function taking two arguments: first a type α, and then an expression a of that type. Its codomain a = a depends on the arguments.

Pi-types🔗

To simplify the notation, we define the following function taking two arguments, the first of which is introduced as an implicit variable in the surrounding context.

variable {I : Type}
def X (i : I) := i = i

Consider the following partial application of @rfl.

example : (i : I) → X i := @rfl I

We refer to (i : I) → X i as a \Pi-type and i : I as the index of the \Pi-type.[…]\Pi-types are also called dependent function types. Such a type can be thought of as encoding an indexed product of sets, \prod_{i \in I} X_i = \left\{\left. f: I \to \bigcup_{i \in I} X_i\ \right| \ f(i) \in X_i,\ i \in I \right\}.

All function types are \Pi-types.

example
  (α : Sort u) (β : Sort v) : (α → β) = ((a : α) → β)
:= rfl

example
  (α : Sort u) (β : Sort v) : (α → β) = ((_ : α) → β)
:= rfl

Often codomains do not depend on arguments, as illustrated by functions such as plus1 and Prod.

example : (_ : ℕ) → ℕ := plus1
example : (_ : Type) → ((_ : Type) → Type) := Prod

Implication🔗

Recall that all expressions of type Prop are themselves types. Accordingly, they can occur as the domain or codomain of a function type. The case where both the domain and codomain are expressions of type Prop encodes logical implication.

example (p q : Prop) : Prop := p → q

Recall that a proof of a proposition is an expression having the proposition as its type. Function application encodes modus ponens. We give two formulations.

example (p q : Prop) (h1 : p → q) (h2 : p) : q := h1 h2

example
  (p q : Prop) : (p → q) → p → q
:=
  λ h1 ↦ λ h2 ↦ h1 h2

Impredicative maximum rule🔗

The type of a function type is governed by the impredicative maximum rule:[…]This name is not used in the Lean Language Reference; the rule itself is described in Predicativity. The level expression imax u v is called the impredicative maximum (or least upper bound) of u and v. We have named the rule accordingly.

example (α : Sort u) (β : α → Sort v) :
  Sort (imax u v) := (a : α) → β a

where

example : Sort (imax _ 0) = Sort 0 := rfl
example : Sort (imax u (v + 1)) = Sort (max u (v + 1))
:= rfl

This rule is essential for the consistency of the type theory: certain typed \lambda-calculi that lack such universe-level stratification are subject to Girard's paradox. The special case v = 0 is related to proof irrelevance: any two proofs of the same proposition are definitionally equal.

example (p : Prop) (proof₁ proof₂ : p) : proof₁ = proof₂
:= rfl

Heuristically speaking, since proofs carry no information beyond the fact that a proposition holds, they do not enable the kind of self-referential constructions that lead to paradoxes.

We revisit the earlier example of logical implication and emphasize again that all expressions of type Prop are themselves types.

example (p : Prop) (q : Prop) : Prop := p → q

The type Prop of p → q arises from the impredicative maximum rule. Indeed, since

example (p : Prop) : Sort 0 := p
example (q : Prop) : Sort 0 := q

the rule applies with u = 0 and v = 0, yielding the type

example : Sort 0 = Sort (imax 0 0) := rfl
example : Sort 0 = Prop := rfl

Universal quantification🔗

For any type α, the function type with domain α and codomain Prop encodes the predicates on α.

example (α : Sort u) : Sort (max u 1) := α → Prop

The type Sort (max u 1) of α → Prop arises from the impredicative maximum rule. Indeed, since

example : Sort 1 := Prop

the rule applies with v = 1, yielding Sort (max u 1).

Consider an evaluation of a predicate.

example (α : Sort u) (P : α → Prop) (a : α) : Prop := P a

Since P a has type Prop, it is itself a type.[…]Once again, all expressions of type Prop are themselves types. In particular, it can occur as the codomain of a \Pi-type. Such types encode universal quantification.

example (α : Sort u) (P : α → Prop) : Prop := (a : α) → P a

The type Prop of (a : α) → P a arises from the impredicative maximum rule. Indeed, since

example (α : Sort u) (P : α → Prop) (a : α) : Sort 0 := P a

the rule applies with v = 0, yielding the type

example : Sort 0 = Sort (imax _ 0) := rfl
example : Sort 0 = Prop := rfl

Convenient syntactic sugar is provided.

example
  (α : Sort u) (P : α → Prop)
  : (∀ a : α, P a) = ((a : α) → P a)
:= rfl

Here is a proof encoding universal instantiation followed by modus ponens.

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:= λ a ↦ h1 a (h2 a)

In fact, the proof uses universal instantiation twice: first in the application h2 a and then in the partial application h1 a.

Recall that @rfl has the following type.

example : (α : Sort u) → (a : α) → a = a := @rfl

It can be rewritten using universal quantification.

example : ∀ α : Sort u, ∀ a : α, a = a := @rfl
example : ∀ (α : Sort u) (a : α), a = a := @rfl

Local definitions🔗

Consider the following function.

def pq (x : ℕ) : ℕ :=
  (x + 1)^2 + 3*(x + 1) + 1

We can avoid repeating the expression x + 1 by composing two functions.

def q (x : ℕ) : ℕ := x + 1
def p (y : ℕ) : ℕ := y^2 + 3*y + 1
def pq₁ (x : ℕ) := p (q x)

This introduces two names p and q. Such auxiliary definitions can be avoided as follows.

def pq₂ (x : ℕ) :=
  have y := x + 1
  y^2 + 3*y + 1

Here have is syntactic sugar for \lambda-abstraction and application.

example (α : Sort u) (β : Sort v) (a : α) (b : β) :
  (
    have x : α := a
    b
  ) = (λ x : α ↦ b) a := rfl

The parentheses around the have syntax can be omitted.

example (α : Sort u) (β : Sort v) (a : α) (b : β) :
  have x : α := a
  b = (λ x : α ↦ b) a := rfl

In particular, the following coincides with pq₂.

def pq₃ (x : ℕ) :=
  (λ y ↦ y^2 + 3*y + 1) (x + 1)

Steps in proofs🔗

A typical use of have is to isolate steps in proofs. Let us return to our earlier example on universal instantiation followed by modus ponens, and isolate the universal instantiation.

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:=
  λ a : α ↦
  have Pa := h2 a
  h1 a Pa

We can read the first line of the example as introducing the symbols involved in the statement, which itself consists of the second and third lines. The statement is:

Suppose h1 : … and h2 : ….
Then ∀ a : α, Q a.

The leading : on the third line reads as "Then" and := on the fourth line as "Proof:".[…]It is due to this reading that we prefer the indentation in the example over the one in Mathlib's style guidelines. When not proving a proposition, we adopt the usual indentation style. The proof has the reading:

Let a : α.
We have P a by hypothesis h2, applied to a.
We conclude by hypothesis h1, applied to a and the fact P a.

Naming every intermediate step can become cumbersome. Omitting the name after have makes the step accessible as this.

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:=
  λ a : α ↦
  have : P a := h2 a
  h1 a this

A proof can also be referenced by its type using ‹…› notation.[…]This introduces no ambiguity, since any two proofs of the same proposition are equal.

example (α : Sort u) (P Q : α → Prop)
  (h1 : ∀ a : α, P a → Q a) (h2 : ∀ a : α, P a)
  : ∀ a : α, Q a
:=
  λ a : α ↦
  have : P a := h2 a
  h1 a ‹P a›

Syntactic abbreviation🔗

A more general abbreviation is given by let.

def pq₄ (x : ℕ) : ℕ :=
  let y := x + 1
  y^2 + 3*y + 1

There are cases where let is applicable but have is not.

def plus1₄ :=
  let t := ℕ
  λ x : t ↦ x + 1

Reductions of beta, delta, and zeta kind🔗

Recall that having the same normal form is a sufficient condition for two expressions to be definitionally equal. Computing normal forms involves several kinds of reduction, three of which are related to the concepts introduced in this section.

beta-reduction🔗

\beta-reduction corresponds to applying a function to an argument by substitution.

variable (α : Sort u) (β : Sort v) (f : α → β) (a : α)

example : (λ x ↦ f x) a = f a := rfl

f a#reduce (λ x ↦ f x) a
f a#reduce f a

delta-reduction🔗

\delta-reduction replaces a defined name by its defining expression.[…]Names are referred to as constants in the Lean Language Reference, see Definitions.

While we have so far used def only to give names to functions, any expression can be named.

def ℕ2 := ℕ × ℕ

example : ℕ2 = (ℕ × ℕ) := rfl

ℕ × ℕ#reduce (types := true) ℕ2
ℕ × ℕ#reduce (types := true) ℕ × ℕ

A function such as plus1 cannot be employed to demonstrate \delta-reduction in isolation. Indeed, the normal form of plus1 differs from its definition.[…]The #print command queries information about definitions.

fun n => n.succ#reduce plus1
def Document.Functions.plus1 : ℕ → ℕ :=
fun n => n + 1#print plus1

The normal form of plus1 is related to the inductive definition of ℕ, described later.

zeta-reduction🔗

\zeta-reduction expands a let-abbreviation.

example : (let t := ℕ; t × t) = (ℕ × ℕ) := rfl

ℕ × ℕ#reduce (types := true) (let t := ℕ; t × t)

The semicolon is a syntactic device that allows multiple expressions to be written on a single line. Replacing it by a line break leaves the expression intact.

Function eta-equivalence🔗

In addition to reduction, definitional equality identifies certain expressions that differ only by trivial abstraction. This identification is called \eta-equivalence. For functions, \eta-equivalence says that a function is definitionally equal to the \lambda-abstraction obtained by applying the function to an argument.

example : (λ x ↦ f x) = f := rfl

The definitional equality of the left and right-hand sides is not based on them having the same normal form. In fact, their normal forms differ.

fun x => f x#reduce λ x ↦ f x
f#reduce f

Reduction and \eta-equivalence differ in a fundamental way: the former has an intensional nature while the latter is a limited kind of extensionality.

Function extensionality🔗

The functions plus1 and plus1' coincide in the sense that they give the same value when applied to the same argument, that is, they are extensionally equal. However, they are not definitionally equal, because the two terms in the addition are in the opposite orders in their definitions.

example : plus1  = (λ n ↦ n + 1) := rfl
example : plus1' = (λ n ↦ 1 + n) := rfl

The following example is invalid.

example : plus1 = plus1' := Type mismatch
  rfl
has type
  ?m.3 = ?m.3
but is expected to have type
  plus1 = plus1'rfl

The principle of functional extensionality holds in Lean. It can be used to show that plus1 and plus1' are indeed equal.[…]Theorem Proving in Lean is the canonical reference for writing proofs like this in Lean.

example : plus1 = plus1'
:= byn:ℕI:Typeα:Sort uβ:Sort vf:α → βa:α⊢ plus1 = plus1'
  funext nhn✝:ℕI:Typeα:Sort uβ:Sort vf:α → βa:αn:ℕ⊢ plus1 n = plus1' n
  simp only [plus1, plus1', add]hn✝:ℕI:Typeα:Sort uβ:Sort vf:α → βa:αn:ℕ⊢ n + 1 = 1 + n
  grindAll goals completed! 🐙

Surface syntax and underlying type theory🔗

Lean's processing of source code can be divided into several stages. For our purposes, the important stages are:

Macro expansion that removes syntactic sugar.
Elaboration that translates the remaining user-facing surface syntax into an underlying basic form.
Kernel checking that ensures that the translated expressions follow the rules of the type theory.

For instance, implicit arguments are a part of the surface syntax. They are translated into explicit arguments during elaboration.

In addition to enforcing the rules of the type theory, the kernel implements definitional equality. We have encounted the following aspects of definitional equality.

Proof irrelevance
Function \eta-equivalence
\beta-, \delta-, and \zeta-reductions

The type theory is designed to be simple, enabling the kernel to remain small. From a foundational perspective, trusting Lean means trusting the correctness of this small kernel.

Rules of the type theory🔗

The following rules govern the concepts introduced so far. They constitute a pure type system. For each rule, we first present an example and then its abstract formulation. In the abstract formulations, we write \operatorname{Sort}_{u} for Sort u, \Pi x : \alpha.\; \beta for (x : α) → β x, and \equiv for definitional equality. Moreover, \Gamma denotes an arbitrary typing context and \beta[x := a] denotes substitution.[…]The substitution replaces all free occurrences of x in the expression \beta with the expression a. We use the standard notation for typing rules.

Axioms

example : Sort (u + 1) := Sort u

\frac{ }{ \vdash \operatorname{Sort}_{u} : \operatorname{Sort}_{u + 1} }

Start

example (α : Sort u) (a : α) : α := a

\frac{ \Gamma \vdash \alpha : \operatorname{Sort}_{u} }{ \Gamma, a : \alpha \vdash a : \alpha }

Weakening

example (α : Sort u) (a : α) (β : Sort v) (b : β) : α := a

\frac{ \Gamma \vdash a : \alpha \quad \Gamma \vdash \beta : \operatorname{Sort}_v }{ \Gamma, b : \beta \vdash a : \alpha }

Product[…]This is the impredicative maximum rule.

example (α : Sort u) (β : α → Sort v) :
  Sort (imax u v) := (x : α) → β x

\frac{ \Gamma \vdash \alpha : \operatorname{Sort}_{u} \quad \Gamma, x : \alpha \vdash \beta : \operatorname{Sort}_{v} }{ \Gamma \vdash \Pi x : \alpha.\; \beta : \operatorname{Sort}_{\operatorname{imax} u \; v} }

Application

example (α : Sort u) (β : α → Sort v)
  (f : (x : α) → β x) (a : α) :
  β a := f a

\frac{ \Gamma \vdash f : \Pi x : \alpha.\; \beta \quad \Gamma \vdash a : \alpha }{ \Gamma \vdash f\; a : \beta[x := a] }

Abstraction

example (α : Sort u) (β : α → Sort v)
  (f : (a : α) → β a) :
  (a : α) → β a := λ x ↦ f x

\frac{ \Gamma, x : \alpha \vdash e : \beta \quad \Gamma \vdash \Pi x : \alpha.\; \beta : \operatorname{Sort}_{v} }{ \Gamma \vdash \lambda x : \alpha \mapsto e : \Pi x : \alpha.\; \beta }

Conversion

example (α : Sort u) (a : α) :
  let β := α
  β := a

\frac{ \Gamma \vdash a : \alpha \quad \Gamma \vdash \alpha\equiv\beta }{ \Gamma \vdash a : \beta }

Further proofs🔗

example : plus1 = (λ n ↦ n + 1) := rfl
example : plus1 = plus1₁ := rfl
example : plus1 = plus1₂ := rfl
example : plus1 = plus1₃ := rfl
example : plus1 = plus1₄ := rfl

example : (ℕ → (ℕ → ℕ)) = (ℕ → ℕ → ℕ) := rfl
example
  (α : Sort u) (β : Sort v) (γ : Sort w)
  : (α → (β → γ)) = (α → β → γ)
:= rfl

example : add = (λ n m ↦ n + m) := rfl
example : add = add₁ := rfl
example : add = add₂ := rfl
example : add = add₃ := rfl
example : add = add₄ := rfl

example : Prod = Prod₁ := rfl
example : Prod = Prod₂ := rfl
example : Prod = Prod₃ := rfl
example : Prod = Prod₄ := rfl

example :
  ((α : Sort u) → (a : α) → a = a)
  = (∀ α : Sort u, ∀ a : α, a = a)
:= rfl
example :
  ((α : Sort u) → (a : α) → a = a)
  = (∀ (α : Sort u) (a : α), a = a)
:= rfl

example : pq = pq₁ := rfl
example : pq = pq₂ := rfl
example : pq = pq₃ := rfl
example : pq = pq₄ := rfl