2.1. Lean's type theory
Zermelo–Fraenkel set theory with the axiom of choice (ZFC) is the foundational basis chosen to formalise most of the mathematics we know. In this framework, all mathematical objects (numbers, functions, algebraic structures, etc.) can be represented as sets, built from a few basic axioms.
However, this system lacks a differentiated internal structure: every mathematical object, such as a number, a function, or even a collection of functions is, ultimately, a set. To achieve a clearer and more differentiated representation of mathematical objects, Lean uses, instead, a system based on types. Moreover, this approach offers us the possibility of establishing a correspondence between programs and mathematical proofs, known as the Curry–Howard correspondenceThe Curry–Howard correspondence establishes a relationship between logic and programming; it lets us understand how "proving a proposition" and "constructing a term of a certain type" can be equivalent. We will see what this means in practice later on, but the deeper ideas, which are beyond the scope of this work, are presented in detail in Morten Heine Sørensen and Pawel Urzyczyn, 2006. “Lectures on the Curry-Howard isomorphism”. Volume 149. Elsevier. Chapter 5, "The Untyped Lambda Calculus"...
In particular, Lean is founded on the Calculus of Inductive Constructions, an extension of the calculus of dependent types that incorporates inductive types and a countable non-cumulative hierarchy of universes (Huet, 1986)Thierry Coquand y Gérard Huet, 1986. The calculus of constructions. Tesis doctoral, INRIA. Although it is not necessary to understand this system in order to use Lean as a proof assistant, below we give a brief explanation of the fundamental concepts: type theory, the lambda calculus, the addition of types to the latter, and the introduction of dependent types.
In this section we will see several fragments of Lean code. Lean has an interactive compiler that processes each line when the cursor is placed on it, displaying the result on screen. From now on, when a code fragment produces an output (for example, via #check or #eval), it will be shown in a separate block right below the code, with the same text that Lean would return.
2.1.1. Type theory
Let us start with the most basic part: type theory. We change the paradigm from "every object is a set", typical of ZFC, to "every object is a term with an associated type". This allows us to structure mathematical objects and their relationships more clearly.
For example, 3 is a term of type "natural" (Nat), while "true" is a term of type "boolean". In Lean, we can check the type of these expressions using the #check command.
#check 3
#check true
As in this example, in Lean we use the symbol : to describe typing information. That is, if x is a term of type X, we write x : X.
On the other hand, a type, such as Nat, is also a term. We can check its type:
#check Nat
In Lean, types have their own type, which is called Type. This allows us to define new types. We can use the variable command to define objects in our codeWe will look at this command in detail later..
variable (X : Type)
#check X
variable (x : X)
#check x
Now, we can combine different types to obtain more complex types. Let X and Y be two types. We can consider the type X \times Y, which denotes the pairs formed by an element of X and an element of Y. The type we will use the most is X \to Y, which denotes the functions from X to Y. Let us write this in Lean.
variable (X Y : Type)
#check X × Y
variable (x : X) (y : Y)
#check (x, y)
#check X → Y
variable (f : X → Y)
#check f
On the other hand, by juxtaposing simple terms, we can form more complex terms. In Lean, the typing rules dictate the type of these newly obtained terms. For example, if x has type X and f has type A \to B, as in the previous example, then f x has type B. Indeed:
#check f x
As in the previous example, Lean can automatically deduce the type of many terms from the context. This capability is known as type inference and it often makes our work easier, allowing for more concise code.