Learning Lean (Part 2)
In part 1 we learned some basics about Lean and we defined the natural numbers as a type Nat and the addition function for Nat.
namespace Tutorial
inductive Nat : Type where
| zero : Nat
| succ : Nat → Nat
def add (a b : Nat) : Nat :=
match b with
| zero => a
| succ c => succ (add a c)
end Tutorial
Now we will learn how to prove our first theorems about the natural numbers. [Note that all of the code in these posts are in the namespace Tutorial to avoid name clashes with types and functions in Lean's standard library.]
Here we declare our first theorem:
theorem add_zero_zero : add zero zero = zero := sorry
Almost every expression in Lean is either an inductive type or a function type (constructed using def), but again, Lean has a lot of syntactic sugar and aliases for things. The keyword theorem is just an alias for def, and indeed, theorems are just terms of a specified type (in fact, often theorems are just functions). We used the def keyword in the last post to define functions, but as the name suggests, it is a general way to define a named term of some specific type, or in other words, it lets you assign a type and expression or value to an identifier.
For example,
def x : Nat := succ zero
We've defined a term named x of type Nat assigned to the value zero. Now you can use it in other expressions, such as:
#reduce add x x
Back to the theorem.
theorem add_zero_zero : add zero zero = zero := sorry
So we are defining a theorem called add_zero_zero and this term has the type add zero zero = zero. We have assigned the term to the expression sorry, which is a keyword in Lean that serves as a placeholder when you want to be able to state a theorem without proving it yet.
It is interesting that this theorem has the type add zero zero = zero, what is going on here? We are trying to state the theorem that 0 + 0 = 0 (but we haven't built the nice + notation for our Nat type yet), and we do so by defining a term with that type. If we can actually specify an expression after the assignment operator := that constructs a term of type 0 + 0 = 0, then our term will type check as a valid term, or in this context, Lean will verify we have proved the theorem.
Firstly, it might seem ridiculous that we should prove 0 + 0 = 0, isn't that totally obvious? Well Lean is a powerful programming environment but it doesn't generate theorems automatically, it doesn't know what we care about, so even extremely trivial statements like this must be explicitly stated and proved. However, Lean does agree that proving this is obvious in the sense that the proof is trivial. And recall, by proof we mean an implementation of an expression that generates a term of this type.
Well what exactly is this type add zero zero = zero? We are trying to prove two things are equal, and recall the (mostly true) mantra everything in Lean is an inductive type or function type, so this expression must be one of those. Indeed, this is an equality type, and the equality type is defined in Lean as an inductive type. Here's how it is defined:
inductive Eq {α : Sort _} : α → α → Prop where
| refl (a : α) : Eq a a
Okay there's a lot more going on here than our Nat type, and we will need to learn more features of Lean to understand it. First, notice this is defining an inductive type called Eq, but then there are these curly braces and an alpha symbol and sort... Confusing.
{α : Sort _} is an implicit input to this type.
Recall our identity function,
def natId (a : Nat) : Nat := a
The a is an explicit input to this function; without supplying a term a, this function doesn't work. However, some functions have inputs that do not need to be supplied explicitly, but can be inferred by Lean automatically. When this is the case, these inputs can be put in curly braces instead of parentheses.
As an example, let's make a more general version of our identity function. Before our identity function only worked on terms of type Nat, but we can make a polymorphic identity function that works on terms of any type.
def id { α : Type _ } (a : α) := a
This function has one implicit (optional because it can be automatically inferred) input α (which you can type in Visual Studio Code by typing \a) and one explicit (required) a. If you apply the function id to a term of any type it will work and just return that term unchanged.
The implicit input α is assigned the type Type _ because it is itself representing some type, and we want to make sure our function works on all types in the type hierarchy Type 0, Type 1, Type 2 ... that we discussed in the last post. These numbered type levels are called universes, by the way. The underscore character _ is like a "wildcard" that tells lean to infer what should go there based on the context.
When we apply id to a term of type Nat,
#check id zero
--Output: id zero : Nat
Lean will infer that α must be Nat and Nat lives in the type universe Type 0, so the wildcard _ can be inferred to be 0. The underscore wildcard is quite useful as Lean can often infer simple holes we leave for it.
Okay, back to trying to understand the equality type.
inductive Eq {α : Sort _} : α → α → Prop where
| refl (a : α) : Eq a a
We now know what the {α : Sort _} means, oh wait, no we don't, because it says Sort _ instead of Type _. Ok, so Type u (where u is some non-negative number) is actually an alias for Sort (u + 1), so e.g. Type 0 = Sort 1. What's the point of this alias? Well, because Sort 0 is special. Sort 0 itself has another alias, namely Prop. Prop (Sort 0) is a special type universe because it is where propositions live.
A proposition is a statement with a truth value, i.e. something that we think is either true or false, like 0 + 0 = 0. A proposition in Lean, therefore, is just a type that lives in the Prop universe, but everything else we've talked about with regard to "regular" types and universes like Nat and Type 0 still applies. And as mentioned earlier, a proof of a proposition (or theorem) is just an expression that generates or constructs a term of that specific type, and that type will itself have the type Prop.
So the type 0 + 0 = 0 is of type Prop (aka Sort 0), and a proof of 0 + 0 = 0 is an expression that constructs a term of type 0 + 0 = 0.
Oh, and the main reason Prop is special is that in Lean, any two terms of a given Prop are considered definitionally equal. So if we came up with two different ways of proving that 0 + 0 = 0, then Lean will consider them definitionally equal, unlike in other type universes Type 0, Type 1, etc... If we have proved a proposition to be true, it no logner matters in Prop how exactly it was proved, we just care that it was indeed proved.
And again, let's get back to trying to understand the equality type.
inductive Eq {α : Sort _} : α → α → Prop where
| refl (a : α) : Eq a a
So far we have explained everything up to the colon. After the colon, we are defining the type of our new inductive type, and unlike Nat which has the (default) type Type 0, Eq is given the type α → α → Prop, which you should recognize as a function type. The input types to functions are all the types before the last type after a chain ... → ... → .... So in this case, this function has two inputs of type α, and remember, α is an implicit input type that Lean will infer for us.
Inductive types like this are actually defining a family of inductive types, each family is parameterized by the specific α given. If we parameterize Eq with Nat, then we get a family of inductive equality types where some expression of Nat (propositionally) equals some other expression of type Nat.
We can force implicit inputs to become explicit inputs to a function by prefixing the function name with the @ character, for example:
#check @Eq Nat
--Output: Eq : Nat → Nat → Prop
This defines the family of equality propositions between natural numbers. A specific proposition in this family of equality types Nat → Nat → Prop would be what we have been trying to prove, namely add zero zero = zero (aka 0 + 0 = 0).
#check Eq (add zero zero) zero
-- Which is the same as:
#check add zero zero = zero
--Output: add zero zero = zero : Prop
By supplying Eq with two terms of type Nat, we get a proposition, as the type signature Nat → Nat → Prop would predict.
Back to the equality type.
inductive Eq {α : Sort _} : α → α → Prop where
| refl (a : α) : Eq a a
We should now understand the top line, now let's figure out what's going on in the one constructor for this type. The one constructor is called refl for reflexivity, which is a math term, and it allows us a construct a term of type Eq _ _ (there are those wildcards again) simply by giving it a term of type α.
For example,
#check Eq.refl zero
--Output: Eq.refl zero : zero = zero
The only things that are equal are those terms that are literally the same term, e.g. zero = zero. This defines syntactic equality, the notion that expressions in Lean are equal only when they represent the exact same string of characters. There is another kind of equality in Lean that is not an inductive type, namely, definitional equality. If I define def x := zero then x = zero by definition, because anywhere there is an x in an expression it can be replaced with zero.
Now we can get back to studying our first theorem.
theorem add_zero_zero : add zero zero = zero := sorry
We now know that in order to prove this theorem (replace the sorry with a valid expression of type add zero zero = zero), we need to construct an equality term, and we now know the way to do that is using equality's single constructor refl.
At long last, we are ready for the proof.
theorem add_zero_zero : add zero zero = zero := Eq.refl zero
We proved this theorem with Eq.refl zero. How do we know it is proved? Because Lean doesn't give us any errors and if we do
#check add_zero_zero we don't get an error.
But wait, what just happened when we did Eq.refl zero? Well, Lean will automatically compute (or reduce) add zero zero, which reduces to zero, so the proposition becomes zero = zero, which is a type whose term is constructed with Eq.refl zero. What this illustrates is that proofs of equality where one side of the equality expression can be automatically reduced (by definition of the function) can be proved by Eq.refl _. This pattern occurs frequently enough that, yep, there is an alias for it called rfl.
So this does the same thing, and is more commonly used:
theorem add_zero_zero : add zero zero = zero := rfl
Here rfl is essentially an alias for Eq.refl _ where again, the wildcard _ tells Lean to infer, in this case, that _ needs to be zero for the expression to type check.
Okay, so now we understand how to state the proposition that 0 + 0 = 0 and how to prove it Lean.
Let's prove something slightly more general, namely that for any a : Nat, a + zero = a, or in math-y notation that \(\forall a \in \mathbb{N},\ a + 0 = a\), where the upside down A \(\forall\) means "for all", \(\in\) means "in", and \(\mathbb{N}\) is the standard notation for the set of natural numbers, if that isn't already familiar to you.
Actually, let me take some time to degress to talk about the difference between mathematics in Lean and mathematics in say a typical university-level mathematics course. One could think of mathematics in very broad strokes as starting with some rules that are assumed to be true (i.e. axioms) and then just seeing what you can create from there. In this sense, a game like Chess or Go are mathematical because we can study the space of things that can happen given the rules.
It is possible to come up with all sorts of different starting rules (axioms), but one must take care that they do not lead to inconsistencies such as being able to prove 0 = 1, or like a board game where no one can win. But there are many axiom systems that are consistent, and many of them can be proved to be equivalent to other axiom systems, in the sense that expressions in one system can be faithfully translated into another system.
But it seems that by historical happenstance, modern mathematics worldwide is dominated by a particular axiom system called Zermelo–Fraenkel (with Choice) set theory, typically abbreviated ZFC. In ZFC, everything in mathematics is a set, which is an unordered collection of things without repeats. Then there are a bunch of rules (axioms) about how sets work and what you can do with them. Sets are denoted using curly braces, for example, we can say \(\{1,2,3\}\) is a set of the numbers \(1,2,3\). However, in set theory, everything is a set, even the numbers. You denote that some element is in a set using the \(\in\) notation, e.g. \(1 \in \{1,2,3\}\).
Many propositions in set theory are stated as propositions for all members of a set, such as our proposition that \(\forall a \in \mathbb{N},\ a + 0 = a\). Another form of proposition is the existence of some element or set, for example, \(\forall a \in \mathbb{N}, \exists b \in \mathbb{N}, b > a\), which is read as "for all natural numbers \(a\), there exists another natural number \(b\) such that \(b\) is greater than \(a\).
My goal is not to explain set theory because I only know the basics myself and that's a whole massive subject in its own right. The point I have been leading up to is that Lean does not use ZFC set theory as it's logical/mathematical foundation (i.e. axiom system). Lean uses type theory, which is actually a family of axiom systems. Lean uses a particular type theory called the Calculus of Constructions, which doesn't matter for our purposes unless you're into that sort of thing.
In type theory, everything is not a set, everything is a type as I have already exclaimed earlier. Types and sets are very similar, and as far as I know, unless you're a set theorist or into studying axiom systems, we can mostly ignore the differences. It turns out that every expression in Lean's type theory can be translated into ZFC set theory and vice versa, so all the mathematics that has been developed on top of ZFC can be easily translated into Lean's type theory. Perhaps in parallel universe, modern mathematics was developed in type theory rather than set theory.
In any case, the main reason for that digression was to point out that if we state our theorem in Lean and check its type:
theorem add_zero (a : Nat) : add a zero = a := sorry
#check add_zero
-- Output: ∀ (a : Nat), add a zero = a
The type of add_zero is actually ∀ (a : Nat), add a zero = a, unlike what we actually typed in, which did not include the \(\forall\) "for all" symbol. Remember that theorem is just an alias for def, and in this particular theorem we have an explicit input a, so this theorem is actually a function that takes an a (of type Nat) and produces a proposition add a zero = a, which recall, is an equality type.
But remember that the equality type is actually parameterized by two inputs of the same type, and when it is parameterized the equality type has the type Prop instead of Type. Remember we said Lean is a dependently-typed functional programming language? Well here is our first introduction to dependent types. The concrete output type of our theorem (function in this case) add_zero depends on the first input type. Hence, it is a dependent function type.
We actually already saw an example of a dependent function type when we made a polymorphic identity type:
def id { α : Type _ } (a : α) := a
#check id
-- Output: {α : Type u_1} → α → α
This function is a dependent function type because the output type will depend on the input type. But there's none of that ∀ notation here... But watch what happens when we change Type _ to Prop
def id { α : Prop } (a : α) := a
#check id
-- Output: ∀ {α : Prop}, α → α
We get that ∀ notation again. There is nothing fundamenetally different going on in these two examples, we're just changing the type universe that α lives in. But by default, Lean will utilize the ∀ notation in place of the → notation in the Prop type level, because when we're restricting ourselves to Prop it's usually because we're doing mathematics, and then the ∀ notation is more convenient.
Now, this sort of type polymorphism is present in non-dependently typed functional programming languages, so the real power of dependent types comes from the fact that the output type can depend on specific values (terms), and not just types. For example, we can (and will in a later post), define lists of a specific length, so the type will depend on a particular term of type natural number.
Okay, that was another digression to explain some more Lean syntactic sugar. Back to our theorem.
theorem add_zero (a : Nat) : add a zero = a := sorry
If you look back at our definition for the add function, you will see that when the second input is zero, it will just return the first input. So Lean can automatically reduce add a zero to just a, so we will get a = a. How do we construct a term of type a = a? We use the one constructor for the equality type, Eq.refl. So we can easily prove this theorem:
theorem add_zero (a : Nat) : add a zero = a := Eq.refl a
Or equivalently:
theorem add_zero (a : Nat) : add a zero = a := Eq.refl _
Or equivalently:
theorem add_zero (a : Nat) : add a zero = a := rfl
Let's move on to proving something very similar appearing, but significantly more difficult to prove:
theorem zero_add : add zero a = a := sorry
So instead of proving a + 0 = a like we just did, we want to prove 0 + a = a. We know that in math a + b = b + a, because addition is commutative (the order of the inputs doesn't matter). But we haven't proved that yet, and in fact our proof of the commutativity of addition will use our proof of zero_add and add_zero.
Why is zero_add harder than proving add_zero? Because 0 + a is not reduced to a by definition. Look back at our addition function, if the first argument is zero and the second argument is a, then without knowing what a is, Lean can't just reduce it. So in this case, since we don't know what a is, we have to do a match on it, and we will have a branch of code for if a is zero and a separate branch of code for if a has the pattern succ b where b is another natural number.
I'm going to build up the proof incrementally and explain the steps.
theorem zero_add : add zero a = a :=
match a with
| zero => _
/-
Proof state:
a: Nat
⊢ add zero zero = zero
-/
I've started a proof for our theorem, and I've left a wildcard _. In this case, I'm not asking Lean to infer what to put there, because it can't, but what Lean will do is tell me what data I have access to and what term I need to construct in place of the wildcard. You should be able to see this by putting your cursor after the _ in Visual Studio Code and looking at the Lean Infoview pane. This is what makes Lean an interactive theorem prover, because Visual Studio Code is continuously running Lean in the background and updating the state depending on where our cursor is.
The expression after the turnstile ⊢ symbol shows us that for the case where a = zero, we need to prove that add zero zero = zero. Well we already know how to do this, we can just use rfl.
Let's keep going.
theorem zero_add : add zero a = a :=
match a with
| zero => rfl
| succ c => _
/-
Proof state:
a c: Nat
⊢ add zero (succ c) = succ c
-/
We've "closed the subgoal" where a = zero, but in order to prove the general case that 0 + a = a we also need to prove that it holds when a = succ c. We see that this sub-goal is add zero (succ c) = succ c. So now we are stuck. We cannot prove this with rfl. However, look back at our definition for add. Notice that by definition add a (succ b) => succ (add a b). So we can use this fact to change the (sub)goal expression a bit:
⊢ add zero (succ c) = succ c
-- By definition we can change it to:
⊢ succ (add zero c) = succ c
Let's take stock of what we already know. We have already proved a subgoal that add zero c = c when c = zero (the base case). Can we use that proof to produce a proof of succ (add zero c) = succ c? If we could somehow apply succ to both sides of the equation, we could, but Lean doesn't know if that is a valid move yet.
In order to solve this, we need to prove an intermediate proposition or theorem, that if a = b then that implies succ a = succ b. This should be obviously true, because a function has to map equal input terms to the same output term, otherwise it would be a non-deterministic function. But even the obvious things need to be stated and formally proved.
So here we go.
theorem congr {a b : Nat} (h : a = b) : (succ a = succ b) := sorry
We are stating a theorem named congr (for congruence), which takes two implicit parameters a and b and a term (called a hypothesis in this context) h : a = b and is of the type succ a = succ b.
If we check the type of this theorem, we get
∀ {a b : Nat}, a = b → succ a = succ b
To translate this into English: "For all natural numbers a and b, if we have a proof that a = b then that implies that succ a = succ b."
In type theory, implication is simply a function type, so we can interpret the arrow as "... implies ..."
Let me show you the proof of this:
theorem congr {a b : Nat} (h : a = b) : (succ a = succ b) := by rw [h]
The proof is by rw [h], which is something we haven't seen before. This is opening a can of worms that we cannot fully explain in this post, but I will introduce it here. The keyword by puts us into tactic mode. Tactic mode is a high-level Lean language feature that lets us use tactics. Tactics are metaprograms, which is to say they are not regular language constructs but can read, construct and manipulate the regular language. These metaprograms can make proving theorems a lot easier. For one, they allow us to write proofs in a sequential manner, avoiding the hassle that comes with pure functional programming. Secondly, they can do a lot of automation behind the scenes for us. That's as much as I'll say about tactics in this post as that is not the focus of this post and we will learn more about tactics later.
The rw tactic stands for rewrite, as it allows us to rewrite expressions in terms of equalities that are known to us. In our case of proving ∀ {a b : Nat}, a = b → succ a = succ b, we rewrite the final goal succ a = succ b with the hypothesis h : a = b, which gives us a new goal succ b = succ b, which is true by rfl.
Now that we have this intermediate theorem congr available, we can get back to proving that 0 + a = a.
theorem zero_add : add zero a = a :=
match a with
| zero => rfl
| succ c => _
/-
Proof state:
a c: Nat
⊢ add zero (succ c) = succ c
-/
The goal is technically add zero (succ c) = succ c but as we previously discussed, that is definitionally equal to succ (add zero c) = succ c, which Lean knows, so we can treat the goal as the latter. Since we proved the base case that add zero c = c when c = zero, we can use this as our hypothesis h in the congr theorem to get a proof that succ (add zero c) = succ c. Thus to prove this theorem we use recursion, which is going to be a common approach. As we will learn later, proving theorems using recursion is identical to the mathematical concept of proof by induction.
So here's the final proof.
theorem zero_add : add zero a = a :=
match a with
| zero => rfl
| succ c => congr (zero_add c)
Let's work through a concrete input, because remember zero_add is a function, so we can apply it as a function.
Let's say we give it the input a = zero.succ.succ (which, recall is the number 2). It will match the pattern succ c, and the output will be congr (zero_add zero.succ). Now we do the recursive call with zero_add zero.succ, and again, we match the pattern succ c, so we get congr (zero_add zero). We do another recursive call, this time matching the base case zero => rfl, which will return zero = zero.
So now we can start subtituting these recursive outputs back into the first function call; here's the sequence of steps happening:
congr (zero_add zero.succ)
congr (congr (zero_add zero))
congr (congr (zero = zero))
congr (succ zero = succ zero)
succ succ zero = succ succ zero
And this will of course work the same way for any natural number, hence the theorem is proved for all natural numbers.
The theorem congr we proved only works for inputs of type Nat, but this theorem must be true for any type and any function on that type, because if it were not true then the function would not be deterministic, and all functions in Lean are pure, which implies they are deterministic. The Lean standard library includes a polymorphic version of this theorem called congrArg, and we could have used that in place of our own.
theorem zero_add (a : Nat) : add zero a = a :=
match a with
| zero => rfl
| succ c => congrArg succ (zero_add c)
The only difference is that congrArg also requires the function succ as input, because it is a theorem that ∀ {α : Sort u_1} {β : Sort u_2} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂, which is read as "for some types α and β, some terms a₁ a₂ : α, and a function f : α → β, if we have a proof that a₁ = a₂, then that implies f a₁ = f a₂. So we need to supply the function f which is succ in this case.
That's it for now. Next time we will take a brief pause from the natural numbers to discuss type classes, structures, custom notation, and construct some other kinds of types.
References
- https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html
- https://leanprover.github.io/lean4/doc/
- https://leanprover.github.io/theorem_proving_in_lean4/
- Friendly people in the Lean zulip.