Primitives
When used as a proof assistant, the central form of interaction with Lean is declaring a definition.[…]In fact, the Lean code in these notes consists almost exclusively of commands declaring a definition, namely def together with its variants example, abbrev, lemma, and theorem, as well as inductive, which declares an inductive type. The remaining commands we encounter are related to namespaces and diagnostics. These include #check and set_option, which configures diagnostic output. Commands producing diagnostic output are prefixed with #. The following definition gives the name z to 0, and states that z is a natural number.[…]The natural numbers 0, 1,… are denoted by ℕ. Hovering over ℕ in VS Code shows that it can be entered using \N.
def z : ℕ := 0
In Lean, every expression has a type. While we could have chosen a name other than z, the kernel verifies that 0 has the type ℕ. We will make extensive use of a variant of def that omits the name and only verifies the type.
example : ℕ := 0
The following invalid example produces a type mismatch error, since the pair (0, 1) does not have type ℕ.
example : ℕ := (0, 1)
The command #check is used to inspect the type of an expression.[…]Hovering over #check shows its output.
#check 0
#check (0, 1)
The pair (0, 1) has type ℕ × ℕ, encoding the Cartesian product of ℕ with itself.
example : ℕ × ℕ := (0, 1)
def p : ℕ × ℕ := (0, 1)
One way in which Lean differs from many programming languages is that types are first-class citizens.
#check ℕ
The type of ℕ is Type, the type universe. It is the first kernel-level primitive we have seen. In what follows, we will consider three other primitive concepts: the universe of propositions, functions, and inductive types.[…]The remaining primitives are used more rarely. They are quotient types and higher universes. Natural numbers and the cartesian product are inductive types.
Propositions
Propositions are expressions of type Prop, the universe of propositions.
example : Prop := 0 = 0
example : Prop := 1 = 0
The first proposition is provable, while the second is not.[…]We later prove the negation of 1 = 0 as a consequence of the Peano axioms. Interestingly, the proposition 0 = 0 is itself a type,[…]We will return to equality later. and an expression of type 0 = 0 encodes a proof of 0 = 0. In general, an expression p of type Prop is itself a type. To prove p is to give an expression of type p.
The proposition 0 = 0 has a canonical proof by reflexivity of equality.[…]We will explain the precise meaning of rfl later.
example : 0 = 0 := rfl
Definitional equality
In addition to enforcing the rules of the type theory, the kernel implements definitional equality. If two expressions are definitionally equal, then rfl proves their equality.[…]More precisely, rfl proves equality of definitionally equal expressions modulo elaboration-time transparency settings: definitions annotated as irreducible are not unfolded under default transparency, a restriction typically imposed for performance reasons. Full transparency can be enforced using with_unfolding_all. A sufficient condition for definitional equality is that the expressions have the same normal form.[…]Definitional equality has aspects beyond reduction to normal form, summarized later. The #reduce command computes this normal form.
#reduce 1 + 1
Since the normal form of 1 + 1 is 2, we can use rfl to prove 1 + 1 = 2.
example : 1 + 1 = 2 := rfl
The following example is invalid.
example : 1 = 0 := rfl
Functions
Functions are given by \lambda-abstractions.
def plus1 : ℕ → ℕ := λ n ↦ n + 1
An alternative notation is
def plus1₁ : ℕ → ℕ := fun n => n + 1
The command #eval evaluates a given expression.[…]Parentheses are not needed in function evaluation syntax.
#eval plus1 0
Lean is a proof assistant and a functional programming language. One may think of #check and #eval as reflecting these two sides. We will focus on the proof assistant features and favor a proof over #eval.
example : plus1 0 = 1 := rfl
Syntactic sugar allows for introducing the argument using parentheses.
def plus1₂ (n : ℕ) : ℕ := n + 1
The functions plus1₁ and plus1₂ coincide with plus1.
All functions take exactly one argument, but syntactic sugar creates the appearance of functions taking several arguments.
def add : ℕ → (ℕ → ℕ) := λ n ↦ (λ m ↦ n + m)
def add₁ : ℕ → ℕ → ℕ := λ n m ↦ n + m
def add₂ (n m : ℕ) : ℕ := n + m
The functions add₁ and add₂ coincide with add.
Implication and universal quantification
In Lean, logical implication and universal quantification are not separate primitives but arise as function types.[…]Other logical connectives and existential quantification are encoded as inductive types, as seen later.
Implication is a function type from a proposition to a proposition. While 0 = 0 is provable and 1 = 0 is not, the following two implications are both proven by the identity function.
example : 0 = 0 → 0 = 0 := λ h ↦ h
example : 1 = 0 → 1 = 0 := λ h ↦ h
All natural numbers n satisfy n + 1 ≠ 0.[…]We will explain the proof nofun later.
example (n : ℕ) : n + 1 ≠ 0 := nofun
This example should be compared to plus1₂.[…]Recall that example is simply a variant of def that omits giving a name. It states that an anonymous function taking the argument n yields an expression of type n + 1 ≠ 0. Notably, this type depends on the argument n. Without syntactic sugar, the example reads
example : (n : ℕ) → n + 1 ≠ 0 := nofun
It can also be written using syntactic sugar for universal quantification.
example : ∀ n : ℕ, n + 1 ≠ 0 := nofun
Inductive types
Inductive types are a general mechanism for defining new types by specifying constructors. For instance, ℕ is an inductive type with two constructors. Its constructors can be inspected by #print command. However, #print does not interact well with syntactic sugar, and ℕ is in fact syntactic sugar for Nat. We can strip this sugar by adjusting pretty-printing via set_option.
set_option pp.notation false in
#check ℕ
set_option pp.notation false in
#print Nat
Let us reproduce the definition of Nat under a fresh name Nat'.
inductive Nat' : Type where
| zero : Nat'
| succ (n : Nat') : Nat'
Now we can reconstruct our first definition z from scratch.
def z' : Nat' := Nat'.zero
Expressions of type Nat' are put together using the
constructors zero and succ.[…]The constructors use the same syntax as the left-hand side of := in def. They are taken apart by using pattern matching. Here is the predecessor function.
def Nat'.pred (n : Nat') :=
match n with
| zero => zero
| succ m => m
The constructor succ encodes the successor function, and pred is its left inverse.
open Nat' in
example (n : Nat') : pred (succ n) = n := rfl
Let us construct our second definition p from scratch.
set_option pp.notation false in
#check ℕ × ℕ
#print Prod
inductive Prod' (α β : Type) : Type where
| mk (fst : α) (snd : β) : Prod' α β
def one := Nat'.succ z'
def p' : Prod' Nat' Nat' := Prod'.mk z' one
The Cartesian product is parametrized by two types α and β. Pairs are put together using the only constructor mk.
Further proofs
Above we made claims about certain expressions being equal. These claims can be verified using rfl.
example : ℕ = Nat := rfl
example : (ℕ × ℕ) = (Prod Nat Nat) := rfl
example : (0 = 0) = Eq 0 0 := rfl
example : plus1 = plus1₁ := rfl
example : plus1 = plus1₂ := rfl
example : add = add₁ := rfl
example : add = add₂ := rfl
example : (∀ n : ℕ, n + 1 ≠ 0) = ((n : ℕ) → n + 1 ≠ 0)
:= rfl
example : 0 = Nat.zero := rfl
example : 1 = Nat.succ 0 := rfl
example : (0, 1) = Prod.mk 0 1 := rfl