Types, propositions and universes
Lean is based on a typed \lambda-calculus, specifically a version of the calculus of constructions with inductive types. We will refer to this formal system simply as type theory. In particular, every expression has a type. The example command checks that a given expression has the specified type.[…]Hovering over ℕ in VS Code shows that it can be entered using \N.
example : ℕ := 0
The example asserts that ℕ is the type of 0. The type ℕ encodes the natural numbers. The command #check is used to inspect the type of an expression.[…]Hovering over #check shows its output.
#check 0
The output 0 : ℕ means that 0 has type ℕ. Another way to say this is that 0 inhabits ℕ.
Lean provides a substantial amount of syntactic sugar and more general user-facing surface syntax. When studying the underlying type theory, it can be useful to consider expressions from which the surface syntax has been removed. Pretty-printing can be adjusted using set_option command. For example, ℕ is syntactic sugar for Nat.
set_option pp.notation false in
#check 0
The pair (0, 1) has type ℕ × ℕ, encoding the Cartesian product of ℕ with itself. This is syntactic sugar for Prod Nat Nat.
#check (0, 1)
example : Prod Nat Nat := (0, 1)
The following invalid example produces a type mismatch error, since the pair (0, 0) does not have type ℕ.
example : ℕ := (0, 0)
Types as expressions
One way in which Lean differs from many other programming languages is that types are first-class citizens.
example : ℕ := 0
example : Type := ℕ
That is, 0 has type ℕ, and ℕ has type Type. Also,
example : Type := ℕ × ℕ
Like all types, Type has a type.
example : Type 1 := Type
In fact, there is an infinite sequence of types,
example : Type 2 := Type 1
example : Type 3 := Type 2
and so on. Type is an abbreviation for Type 0; in fact, both are syntactic sugar, as we will explain shortly.
Propositions
Propositions are expressions of type Prop.
example : Prop := 0 = 0
example : Prop := 1 = 0
The first proposition is provable, while the second is not.[…]In fact, the negation of 1 = 0 is a consequence of the Peano axioms that we prove later Interestingly, the proposition 0 = 0 is itself a type,[…]The expression 0 = 0 is syntactic sugar for Eq 0 0. We will return to this later. and an expression of type 0 = 0 encodes a proof of 0 = 0. In general, all expressions of type Prop are themselves types. To prove a proposition in Lean is to construct an expression inhabiting the proposition.
example : 0 = 0 := rfl
We will consider the precise meaning of rfl later. For the moment, let us simply view rfl as a canonical proof of reflexivity of equality.
Like ℕ, Prop inhabits Type.
example : Type := Prop
Definitional equality
If two expressions are definitionally equal, then their equality can be proven using rfl. A sufficient (but not necessary) condition for definitional equality is that the expressions have the same normal form. The #reduce command displays this normal form.[…]Further details of the reduction to normal form will be provided in due course. A summary covering all aspects of definitional equality is also available.
#reduce 1 - 1
Since the normal form of 1 - 1 is 0, we can use rfl to prove 1 - 1 = 0.
example : 1 - 1 = 0 := rfl
By default, #reduce does not reduce inside types. This matters for equality, since it is itself a type.
#reduce 1 - 1 = 0
We can force reduction inside types as follows.
#reduce (types := true) 1 - 1 = 0
The following example is invalid.
example : 1 = 0 := rfl
Universe hierarchy
The infinite sequence Prop, Type 0, Type 1, … is syntactic sugar for the universe hierarchy Sort 0, Sort 1, Sort 2, …. Here Sort u is called a universe and u is its level. We can verify that the two sequences coincide using rfl.
example : Prop = Sort 0 := rfl
example : Type u = Sort (u + 1) := rfl
The type of a universe is the next universe in the hierarchy.
example : Sort (u + 1) := Sort u
Each type α inhabits Sort u for exactly one u = 0, 1, …. We say that this Sort u is the universe of α.
Further proofs
Above we made claims about certain expressions being equal. These claims can be verified using rfl.
example : ℕ = Nat := rfl
example : (ℕ × ℕ) = (Prod ℕ ℕ) := rfl
example : Type = Type 0 := rfl
example : (0 = 0) = Eq 0 0 := rfl