Lecture 4.1: Mathematics — Foundation

We review the logical foundation of Lean and introduce the axiom of choice, the law of excluded middle, and quotients

Type universes

Where do types live? We learned that Prop : Type, but what about Type?

More generally, there is Sort u, which forms an infinite sequence of type universes: Sort u : Sort (u + 1)

Important: The universes u in Sort u are not terms; they consist of variables u, zero 0, successor _ + 1, max, and imax

Prop   := Sort 0
Type u := Sort (u + 1)
Type   := Type 0
Type*  := Type _

Sort 0 : Sort 1 : Sort 2 : ...
Prop   : Type 0 : Type 1 : ...

Lean's type hierarchy is noncumulative: Each type lives only in one universe

(This is different in Coq, where p : Type u implies p : Type v for all v ≥ u)

We can use ulift : Type u → Type (max u v) to transport types between type universes

Constants can also be polymorphic in the type universe, and can be annotated with type universes—e.g. eq.{u}


We need the whole Type hierarchy to avoid paradoxes

If we had Type : Type, we would end up with Girard's paradox, which is analogous to Russel's paradox in set theory

Typing rule for Π, including universes:

Γ ⊢ α : Sort u   Γ, a : α ⊢ β a : Sort v
————————————————————————————————————————— Pi
Γ ⊢ (Πa : α, β a) : Sort (imax u v)


imax u 0 = 0
imax u v = max u v   if v ≠ 0

In particular:

⊢ α : Sort u    (a : α) ⊢ β a : Prop
————————————————————————————————————— Pi
⊢ (Πa : α, β a) : Prop

⊢ α : Type u    (a : α) ⊢ β a : Type v
——————————————————————————————————————— Pi
⊢ (Πa : α, β a) : Type (max u v)

In particular, in the last instance, Πα : Type 0, β α cannot be in Type 0

Type constructors such as list live in Type 1 or beyond

The special behavior of the Pi rule for Prop is called impredicativity

Prop is impredicative

Type is predicative

Impredicativity works because Lean has proof irrelevance

Proof irrelevance

What is the difference between Prop and Type?

Each proposition (when interpreted as a type) is either empty or has exactly one inhabitant: Prop = {∅, {⋆}}

∀(p : Prop) (h₁ h₂ : p), h₁ = h₂

This is called proof irrelevance and makes reasoning about dependent types easier

Proof irrelevance is implemented in the kernel, which gives us definitional equality, allowing proofs by refl

In contrast:

Prop is an instance of subsingleton α := ∀a b : α, a = b

(Other subsingletons: unit, empty, decidable P, ...)

Large elimination

Compare the following definitions, which are identical except for their type universe (Prop vs. Type):

inductive nonempty (α : Sort u) : Prop
| intro (val : α) : nonempty

inductive inhabited (α : Sort u) : Sort (max 1 u) :=
| mk (default : α) : inhabited

For inhabited, we can define default {α : Type} : inhabited α → α as the projection of mk's argument:

∀a : α, default (inhabited.mk a) = a

We call this large elimination, because we are eliminating into a large type universe (Type _)

A similar projection for nonempty is explicitly disallowed by Lean, because it would be inconsistent with proof irrelevance

Assume we have a projection function witness {α : Type} : nonempty α → α with a computational rule

∀a : α, witness (nonempty.intro a) = a


example : false :=
  have tt ≠ ff :=
    by contradiction,
  have wnw : witness ⟨tt⟩ ≠ witness ⟨ff⟩ :=
    by simp only [witness_eq]; assumption,
  show false, from
    wnw rfl

Thus, there cannot be a computational projection witness {α : Type} : nonempty α → α; but there can be a noncomputational one, as we will see in a moment

In general, inductive definitions c living in Type give rise to a large eliminator:

c.elim {α : Sort u} : ∀{p : Sort v}, c α → ... → p

Small elimination

If we could not eliminate nonempty, then it would be completely useless

Fortunately, we can eliminate it, but only into Prop; we call this small elimination

Elimination is provided by the following small eliminator:

nonempty.elim {α : Sort u} : ∀{p : Prop}, nonempty α → (α → p) → p

For comparison, this is what the large eliminator would look like, if it were allowed:

nonempty.elim {α : Sort u} : ∀{p : Sort v}, nonempty α → (α → p) → p

Using it, we could construct a witness projection from nonempty.elim into Type

In general, inductive definitions c living in Prop give rise to a small eliminator:

c.elim {α : Sort u} : ∀{p : Prop}, c α → ... → p

However, if c is a "syntactic subsingleton" (e.g. false, , =, well_founded), a large eliminator is generated

A "syntactic subsingleton" is an inductive definition with at most one constructor whose arguments are either Prop or appear as immediate arguments in the output type

This exception is called subsingleton elimination

Axiom of choice

The axiom of choice is a noncomputational projection from nonempty:

axiom classical.choice {α : Sort u} : nonempty α → α

It provides an arbitrary element in α but gives no information about it

Often we are only interested in having some witness of ∃a : α, p a, without caring about which one:

classical.some : (∃a : α, p a) → α
classical.some_spec (h : ∃a : α, p a) : p (some h)

From choice, we can derive several other rules:

With LEM everything is decidable: classical.prop_decidable (Diaconescu’s theorem; see Theorem Proving in Lean, Section 11.6)

choice is the only axiom that allows us to construct elements living in Type (cf. funext and propext)

When using choice outside of Prop, we need to mark the definition as noncomputable

Quotient types

Quotient types are a powerful construction in mathematics

They are used to construct , , and many other types

They are built into Lean; for each relation r : α → α → Prop, quot r constructs a quotient type with the embedding function quot.mk r a (written ⟦a⟧) and the axiom quot.sound:

∀a b : α, r a b → ⟦a⟧ = ⟦b⟧

We can lift functions from α → β into quot r → β using quot.lift, which has the following computation rule:

quot.lift f h ⟦a⟧ = f a   for h : ∀a b, r a b → f a = f b

We can think of quot.lift as an eliminator

If r is an equivalence relation, we can derive ⟦a⟧ = ⟦b⟧ ↔ r a b from quot.sound

quotient provides a convenient interface for equivalence relations on top of quot, including quotient.lift_on (for unary functions) and quotient.lift_on₂ (for binary functions)




Further reading: