We review the logical foundation of Lean and introduce the axiom of choice, the law of excluded middle, and quotients
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)
where
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
Propis impredicative
Typeis predicative
Impredicativity works because Lean has 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:
Agda and Coq are proof relevant by default (but are compatible with proof irrelevance)
Homotopy type theory and other constructive or intuitionistic type theories build on data in equality proofs and therefore are incompatible with proof irrelevance
Prop is an instance of subsingleton α := ∀a b : α, a = b
(Other subsingletons: unit, empty, decidable P, ...)
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
Then
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
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
Propor appear as immediate arguments in the output type
This exception is called subsingleton elimination
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:
choice is equivalent to Zorn's lemma and the well-ordering theorem
choice implies the axiom of choice: (∀a : α, ∃b : β, r a b) ↔ (∃f, ∀a, r a (f a))
choice implies the law of excluded middle (LEM or EM): ∀p : Prop, p ∨ ¬ p
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 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: