2.2.1. Typed lambda calculus🔗

The classical lambda calculus does not incorporate types: any function can be applied to any argument. To avoid inconsistencies and provide more structure, the typed lambda calculus is introduced, where each term is assigned a concrete type.

We can write the previous example in Lean as follows:

Here, we are indicating that f has type \mathbb{N} \to \mathbb{N}, that is, that it is a function that takes values in \mathbb{N} and returns values in \mathbb{N}. This information allows Lean to verify that expressions are well formed.

2.2.2. Dependent type theory🔗

In order to express the various mathematical objects in this theory, we need to introduce dependent types. A dependent type is one that can vary depending on a term.

For example, in Lean, the type List α represents a list of elements of type \alpha. If we define an object of type List α, the type of this object will depend on the type \alpha we assign to it. Internally, it is defined as a function of type Type u → Type u.

List.{u} (α : Type u) : Type u

List Nat : Type

We can think of dependent types as a generalisation of functions from one type to another type, where the target type may depend on the input type. We call such functions "dependent functions".

In particular, the proposition \forall x \in \mathbb{N}, P x is represented in Lean by a dependent type that expresses the set of functions that, given an element x \in \mathbb{N}, return a proof of P x. Lean's notation for this kind of construction is Π x : ℕ, P x. The \Pi operator denotes that the output type may depend on the input value.

2.2.3. Universe hierarchy🔗

Since in type theory every element has a type, the type Type also has an associated type. But if we simply wrote Type : Type, the system would fall into an inconsistency similar to Russell's paradox. To avoid this, Lean introduces an infinite hierarchy of universes: Type 0 : Type 1, Type 1 : Type 2, and so on.

This hierarchy is non-cumulative, which means that if A : Type u, it is not assumed in general that A : Type (u+1). This allows Lean to better control how types are combined and to avoid ambiguities when determining which universe each term belongs to, although it can perform certain conversions automatically when it is safe to do so. For this reason, in most cases it is not necessary to work explicitly with these universes.

2.2.4. Inductive types🔗

In Lean, the vast majority of types are instances of a family of types known as inductive types. An inductive type is a structure formed by a finite list of constructors, each with its corresponding type. Each constructor describes a valid way of building a term of this new type.

In Lean, we define an inductive type using the inductive keywordAlthough in Lean inductive types are introduced as a primitive construction of the language, they can be defined equivalently purely in terms of dependent types. This reduction is formally explored in Mario Carneiro, 2019. “The Type Theory of Lean”. Section 5, "Reduction of inductive types to W-types"...

inductive Foo where
  | constructor₁ : ... → Foo
  | constructor₂ : ... → Foo
  ...
  | constructorₙ : ... → Foo

A classic example of an inductive definition is the set of natural numbers, \mathbb{N}. In Lean, we can describe the type Nat of natural numbers as

Internally, the inductive declaration automatically generates a collection of axioms that define the type:

• A constant, Nat, which represents the new type.

• A series of introduction rules or constructors, which indicate the possible ways of building terms of the new type.

• An elimination rule, Nat.rec, which indicates the way of "using" a term of this typeThe #print command shows the complete definition of the object, unlike #check, which only shows its type..

recursor Nat.rec.{u} : {motive : Nat → Sort u} →
  motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t
number of parameters: 0
number of indices: 0
number of motives: 1
number of minors: 2
rules:
for Nat.zero (0 fields): fun motive zero succ => zero
for Nat.succ (1 fields): fun motive zero succ n => succ n (Nat.rec zero succ n)

That is, inductive can be seen as syntactic sugar that automatically generates the following Lean codeWe will study the axiom command in detail later.:

axiom (Nat : Type)
axiom (zero : Nat)
axiom (succ : Nat → Nat)
axiom (Nat.rec : {motive : Nat → Sort u} → motive Nat.zero →
  ((n : Nat) → motive n → motive Nat.succ n) → (t : Nat) →
  motive t)

This last object, Nat.rec, encodes the principle of induction on the naturalsNat.rec is a type that depends on motive, which is any property about the naturals. Nat.rec tells us that if motive holds for Nat.zero (motive Nat.zero), then if for each n (n : Nat) satisfying motive (motive n) we have that n+1 satisfies motive (motive Nat.succ n), then motive holds for every n ((t : Nat) → motive t).. This principle is used implicitly in many definitions by cases, for example:

In this definition, we use the expression match n with to distinguish the two possible cases of a natural number: zero and succ n. Internally, Lean compiles this expression as an application of Nat.rec. We will see later how this principle of induction can be used not only to define functions, but also to prove properties about all the terms of an inductive type.

It is worth noting that there are other constructions in Lean, such as structure or class, which are internally defined as particular cases of inductive types, but are added as separate constructions to improve readability and functionality. We will see some examples of their use throughout this work.

Finally, through inductive types it is possible to define the logical connectives (negation, conjunction, disjunction and implication). This constitutes another big difference between set theory and the calculus of inductive constructions. In order to use set theory, it is necessary to have previously developed (first-order) logic. In this way, formal proofs are not mathematical objects, but live exclusively at the meta-theoretical level.

In the calculus of inductive constructions, on the other hand, logic is expressed within the theory itself, and proofs are mathematical objects that live inside it.

2.2.5. Proofs as mathematical objects🔗

Propositions, like any other object in this theory, are terms with an associated type. In Lean, this type is called Prop.

Prop : Type

inductive True : Prop
number of parameters: 0
constructors:
True.intro : True

P : Prop

¬P : Prop

In Lean, we interpret objects of type Prop as types in themselves and the proofs of each proposition as terms inhabiting that type, following the Curry–Howard correspondence. That is, a proposition p : Prop is the type of the proofs of p; an expression of the form h : p means that h is a proof of p. We say that a proposition p is true if we can construct a term of type p.

h : p

This, together with dependent type theory, gives us a way of defining any mathematical result. For example, "being even" is a property that depends on a natural number n, so we could describe it by es_par : ℕ → Prop. For each natural n, we obtain a term of type Prop.

def es_par : ℕ → Prop := ...
#check es_par    -- es_par : ℕ → Prop
#check es_par 3    -- es_par 3 : Prop

In this case, a term of type es_par n will be a proof that n is even.

Moreover, if p : Prop is a proposition, Lean recognises any two elements of type p (h1 h2 : p) as definitionally equal: it does not matter which concrete proof we have, only its existence matters. This is known as proof irrelevance.

This property has important consequences. On the one hand, it avoids undesired behaviour when we define structures that depend on propositions. For example, if we wanted to define a point of the first quadrant in \mathbb{R}^2 as a pair of the form x y : ℝ × ℝ together with a proof h : x ≥ 0 ∧ y ≥ 0, then, thanks to proof irrelevance, we can identify two points that have the same coordinates, because the proofs h and h' associated with each of them are the same.

On the other hand, this same property prevents access to the content of a proof. In particular, it is not possible to directly extract the witness from the proof of an existential proposition of the form \exists x, P(x), since all the proofs of that proposition are considered equal. Given a proof of \exists x, P(x), we have several methods for obtaining a witness, one of which is using the axiom of choice. We will come back to this question later.

One last remarkable feature of propositions in Lean is that logical implication is represented directly by functions: given two propositions p q : Prop, a proof of p → q is simply a function that, given a proof of p, returns a proof of q. This identification between functions and implications is another manifestation of the Curry–Howard correspondence.

In summary, in order to express a mathematical result in this language, we have to write a term of the form p : Prop. To prove that the result is true, we must construct a term h : p. Lean's job as a proof assistant is to verify that the term h is well constructed and has the correct type.