04 - Simple Algebra

Task

We now take a step up and require Lean to do some algebra.

Our task is to show the following is true

$$(a+b)(a-b)=a^{2}-b^{2}$$

We'll assume $a$ and $b$ are integers.

Maths

Let's try to write out a proof, aiming to show and justify each step.

$$\begin{align}(a+b)(a-b)&=a^{2}-ab+ba-b^{2}&&\text{by algebra}\\&=a^{2}-b^{2}&&\text{by algebra}\tag*{\(\Box\)}\end{align}$$

This proof is much simpler than our previous ones. There is no need for any hypotheses, there are no substitutions, and no arithmetic. 

• We start with the expression we want to prove something about, $(a+b)(a-b)$.
• We expand out the brackets, multiplying every combination of terms inside the brackets, to give $a^{2}-ab+ba-b^{2}$.
• We collect like terms, and find that $ba$ and $-ba$ cancel out, to give the desired result $a^{2}-b^{2}$.

All we needed for this proof was basic algebra, specifically, multiplying out brackets, and collecting like terms.

Code

The following Lean program proves (a+b)(a-b)=a^{2}-b^{2}. 

-- 04 - Simple Algebra

import Mathlib.Tactic

example {a b : ℤ} : (a - b) * (a + b) = a^2 - b^2 :=
  calc
    (a - b) * (a + b) = a^2 - a*b + a*b - b^2 := by ring
    _ = a^2 - b^2 := by ring

Notice the line stating the theorem has no hypotheses to declare. It goes straight from the variable types to the statement we want to prove.

The proof itself starts with the expression we want to prove something about, (a - b) * (a + b), and states that this is equal to a^2 - a*b + a*b - b^2. This is justified by the ring tactic, which can do basic algebra. The final line of the proof states the previous expression is equivalent to a^2 - b^2, again justified by the ring tactic.

The first use of the ring tactic was to justify multiplying out the brackets. The second use of the ring tactic was to justify collecting like terms, and cancelling the -a*b and +a*b terms. 

We could have combined both steps into one, using the ring tactic just once, but it wouldn't have made clear to us what the ring tactic can do. Try it anyway. Your code should look like the following.

  calc
    (a - b) * (a + b) = a^2 - b^2 := by ring

Intentional Error

What would happen if $a$ and $b$ were natural numbers, not integers? Let's try it.

Change the variable type declaration from {a b : ℤ} to {a b : ℕ}.

The Infoview now shows errors, indicating that the ring tactic failed. Why is this?

If $a$ and $b$ are natural numbers, then $(a-b)$ doesn't make sense when $b>a$, because natural numbers can't be negative integers. 

More formally, Lean fails to apply the ring tactic because the natural numbers are not a ring under subtraction. Don't worry if this is jargon, it means the same as what we said first. 

This illustrates one of the benefits of Lean. It can catch apparently small assumptions that end up invalidating our results.

---

Exercise

Write a Lean program to prove $(a+b)^{2}=a^{2}+b^{2}$ if we know $ab=0$, where $a,b\in\mathbb{Z}$.

This will require both the ring and rewriting tactics.

03 - Symbols, No Numbers

Task

This task is similar to the previous one, but this time there are no numbers involved. The idea is to see Lean prove purely symbolic statements. Because these don't mention specific numbers, they can be stronger, more general, statements.

Imagine we're given the following facts about the variables x, y, z and c, all of which are real numbers.

$$\begin{align}z&=y^{2}\\&\\y&=x+c\end{align}$$

Our task is to prove

$$z=(x+c)^{2}$$

If true, this statement holds for any values of $x,c\in\mathbb{R}$.

Maths

Again, the task is not difficult. Even so, let's try to write out a structured proof.

$$\begin{align}z&=y^{2}&&\text{given fact}\tag{1}\label{3.1}\\y&=x+c&&\text{given fact}\tag{2}\label{3.2}\\&&&\\z&=y^{2}&&\text{using fact }(\ref{3.1})\\&=(x+c)^{2}&&\text{substitution using fact }(\ref{3.2})\tag*{\(\Box\)}\end{align}$$

Let's talk through this proof.

• We start by listing the two given facts, $z=y^{2}$ and $y=x+c$. 
• We want to prove something about z, so starting with the first fact about $z$ is a good strategy. This gives us $z=y^{2}$. We'd like express that $y$ in terms of $x$ and $c$, if possible. 
• The second fact tells us $y=x+c$. We can use it to substitute for the $y$ in $y^{2}$. This gives us $z=(x+c)^{2}$, our objective.

This proof has no numbers, it is entirely symbolic.

Code

Let's look at a Lean program that proves $z=(x+c)^{2}$, given $z=y^{2}$ and $y=x+c$. 

-- 03 - Symbols, No Numbers

import Mathlib.Tactic

example {x y z c: ℝ} (h1 : z = y^2) (h2: y = x + c) : z = (x + c)^2 :=
  calc
    z = y^2 := by rw [h1]
    _ = (x + c)^2 := by rw [h2]

Notice how similar this code is to the code from the previous chapter. We can see in the proof header how we define the variables x, y, z and c as real numbers, list the two hypotheses, and specify the overall proof objective z = (x + c)^2. 

The main body of the proof is also similar. We first establish that z = y^2, justifying it by the first hypothesis h1. Then we say this is the same as (x + c)^2, justifying it with second hypothesis h2. 

That completes the proof, which is one line shorter than the previous one because we don't need to do a numerical calculation.

---

Exercise

Write a Lean program to prove that $z=x$ given $z=y$ and $y=x$, where $x,y,z\in\mathbb{R}$.

02 - Substitution

Task

Let's continue with another simple task. Imagine we have the following formula.

$$y=x+4$$

Given $x=3$, our task is to prove that $y=7$.

Here, $x$, $y$, $3$ and $4$ are all real numbers.

Maths

Again, this task is so easy it will take an effort to think about the steps involved. Let's give it a go.

$$\begin{align}y&=x+4&&\text{given fact}\tag{1}\label{2.1}\\x&=3&&\text{given fact}\tag{2}\label{2.2}\\&&&\\y&=x+4&&\text{using fact }(\ref{2.1})\\&=(3)+4&&\text{substitution using fact }(\ref{2.2})\\&=7&&\text{using arithmetic}\tag*{\(\Box\)}\end{align}$$

Let's talk through this proof, step by step.

• We start by listing the two given facts, $y=x+4$ and $x=3$. 
• We want to prove something about $y$. What is $y$? The first fact tells us $y=x+4$. 
• At this point, we have $y=x+4$, which is fine, but we do want to resolve that $x$ into a number. 
• Looking back at the facts, we notice the second one tells us $x=3$. We can use it to substitute $3$ for the $x$ in $x+4$. This gives us $y=(3)+4$. We're almost there.
• Finally, we can use arithmetic to evaluate $(3)+4$ as $7$. That gives us what we want, $y=7$.

It is this kind of structured step-by-step thinking that we'll need to write proofs in Lean. It may seem disproportionate for simple tasks like this one, but it is better to develop that thinking with simple tasks than with more difficult ones.

Code

The following Lean program proves $y=7$, given the facts $y=x+4$ and $x=3$, just as we did above.

-- 02 - Simple Proof by Calculation

import Mathlib.Tactic

example {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 :=
  calc
    y = x + 4 := by rw [h1]
    _ = 3 + 4 := by rw [h2]
    _ = 7 := by norm_num

Let's talk about the code in a little more detail.

Lines beginning with -- are comments for us to read, and are ignored by Lean. It is a good habit to write at least a short comment to remind us, or inform other readers, what the code is about.

The next line import Mathlib.Tactic loads into Lean information about fundamental results and common methods used in proofs. These are the tactics we mentioned in the previous post. Without these, we can't specify how each line of a proof follows legitimately from the previous one.

The next line is the beginning of the proof. It's a long line, so let's break it down:

• The first part is usually a name we give to the theorem we're proving. As a special case, example tells Lean that this theorem doesn't need a name because we're not going to refer to it later. 
• The next part {x y : ℝ} tells Lean the variables x and y are real numbers. 
• Then we have (h1 : y = x + 4) (h2 : x = 3) which are the given facts, or hypotheses, we'll be using in our proof. They are given names h1 and h2 so we can refer to them later.
• After a colon : is the statement we want to prove, y = 7. This is important because Lean needs to know what our overall objective, or goal, is.
• Finally, there is a := which signals to Lean that the subsequent code will seek to prove the objective.

So, in effect, the first line states the theorem we want to pove. The following picture summarises its structure.

On the next line we have calc, which tells Lean the strategy we plan to use. The calc strategy is a proof by direct calculation, one of the simplest proof strategies. We'll talk more about it later.

After that we're finally into the proof itself. The next line sets out the starting point with a statement beginning with y =, just as we did in our maths proof. It continues y = x + 4 with a justification for why this is true after the :=. That justification is by rw [h1], which means we are rewriting y using hypothesis h1.

The next line continues to follow our maths proof by stating that the previous expression x + 4, denoted by the shorthand _, is equal to 3 + 4. This is justified by hypothesis h2, which allows us to rewrite x as 3. 

Finally, we conclude with y = 7. The simplification of 3 + 4 to 7 is justified with the norm_num tactic, which can do numerical arithmetic.

Don't worry if all this code is not immediately familar. We'll see the same code structure again and again, and become familiar with it that way. But do take some time to look again at both the maths proof and the Lean code proof, and see how they correlate.

Infoview First Look

Lean provides feedback through its Infoview, which will appear in a separate pane, usually to the right of the code. It is updated as we edit our code, and provides warnings and errors. 

With the above correct Lean code, Infoview includes the following information.

All Messages (0)
No messages.

No messages means no warnings or errors. And that means Lean has determined our proof to be correct.

Let's introduce a deliberate error to see how Infoview reports it. Temporarily change the hypothesis h2, used to rewrite x as 3, to the incorrect hypothesis h1. The incorrect line now reads as follows.

    _ = 3 + 4 := by rw [h1]

Immediately the Infoview updates with an error message.

01_simple.lean:8:24
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  y

It tells us that at line 8 of the code, Lean found the rewrite tactic had failed. Changing the hypothesis back to h2 sees all error messages disappearing from the Infoview.

---

Exercise

Write a Lean program to prove $y=0$ given $y=x^{2}-9$ and $x=-3$, where $x,y\in\mathbb{R}$.

01 - First Proof

Task

Let's start with a very simple task. Imagine we're given the following fact.

$$a=4$$

Our task is to prove that

$$a>1$$

Here, $a$, $1$ and $4$ are all natural numbers. 

Maths

It seems trivially obvious that if $a=4$ then $a>1$. 

The challenge we'll often face writing proofs in Lean is getting inside intuitively easy tasks to think about them in a more structured way.

How can we justify $a>1$, given $a=4$? The question we're asking is whether $4>1$. To answer this, we appeal to the fact that the natural numbers are ordered by the “greater than” $>$ relation. 

Let's now try to write down these thoughts in a structured way.

$$\begin{align}a&=4&&\text{given fact}\\&&&\\&>1&&\text{by the ordering of natural numbers}\tag*{\(\Box\)}\end{align}$$

That wasn't too difficult.

Code

Let's now look at a Lean program that proves $a>1$, given $a=4$, just as we did above.

-- 01 - First Proof

import Mathlib.Tactic

example {a : ℕ} (h1: a = 4) : a > 1 :=
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

This is our first look at Lean code, so we'll only make some initial observations, and allow ourselves to become familiar with Lean code gradually over the coming chapters.

The proof starts on the line beginning with example. This rather long line states the theorem we want to prove.

• The {a : ℕ} tells Lean the variable a is a natural number. 
• Next we have (h1 : a = 4) which is the given fact. It's given a label h1 so we can refer to it later by name.
• After that we have the statement we want to prove, a > 1. 
• Finally there is a := which signals to Lean that we're about to prove that statement. 

The last three lines of code, from calc to norm_num, are the proof of the theorem. For now, let's just look at the last two.

• We state that a = 4, and justify it by referring to the given fact, previously labelled h1.
• We complete the proof by saying this is > 1, and justify it by the ordering of natural numbers. We'll talk more about norm_num below.

Tactics

That last line of the Lean proof justified $4>1$ by the ordering of natural numbers. How did this happen?

The natural numbers are described by the Peano axioms. On top of these axioms, we can define addition, then the “greater than” $>$ relation. 

We did not go that deep in our maths proof!

For a large body of fundamental results, we don't need to prove them every time we use them. Maths would be very tedious if we had to prove something like $4>1$, or $8>0$, every time we used it!

The same idea applies to Lean proofs. 

Many of those fundamental results have been written in Lean and packaged up as tactics, ready for us to use. So norm_num is a tactic that includes knowledge about the order created by the “greater than” $>$ relation on natural numbers. It also includes knowledge about how to evaluate arithmetic like $3+4$, which we'll see in the next chapter.

---

Exercise

The Lean program above proves $a>1$ given $a=4$. Change it to prove $a<10$ given $a=4$.

The norm_num tactic understands “less than” $<$, as well as “greater than” $>$.

00 - Proofs & Proof Assistants

Mathematics & Proof

Over thousands of years of our history, we humans have discovered many diverse, interesting, and sometimes useful, mathematical truths. We've done it through hard work, intuition, accident, or in some cases, mystical inspiration. Examples of such truths are the infinitude of prime numbers, the irrationality of $\sqrt{2}$, and the need for no more than four colours to colour a geographic map.

Alongside that is a second monumental achievement, the development of a system by which we convince ourselves, and each other, that these truths are actually true. 

That system of proofs consists of commonly agreed fundamental axioms, and a rigorous framework of logic by which we progress an argument, step by step, from its beginnngs to a desired conclusion. Without such a framework, we would always be in doubt about the actual truth. Worse, we'd risk building further mathematics, false mathematics, on false foundations.

Without proof, our proposals remain conjectures. We may believe them to be true for personal reasons. We may believe them to be true by weight of experimental evidence. But all of that fails to meet the standard we set ourselves in mathematics. We must demonstrate that something is true using that framework of axioms and logic such that anyone else who agrees on the axioms and that logic, can't disgree with our conclusion. The only way they could disagree is to find a fault in the logic of our argument.

The discipline of proof, therefore, is a central pillar of mathematics. 

And it is an eternal shame that most students aren't exposed to the idea of proofs at school, only encountering them if they choose to study mathematics at university.

Proof Assistants

Recent years have seen the emergence of software tools that aid the development or validation of proofs. Some tools produce strategies for proof, or even candidates for proofs. 

Some tools, like Lean, focus on validating a proof that we write. Automatically checking a proof is a very powerful capability to have.

Installing and Running Lean

You can use the web-based version of Lean which only requires a modern web browser and internet access. There is nothing to install. This would be the idea solution for this first steps course of small proofs, but this service is new and sometimes fails requiring a refresh. Even so, everything in this course has been tested with this online service.

• https://live.lean-lang.org

Many people have coalesced around using Microsoft's Visual Studio Code with the Lean extension which provides a richer environment. The extension installs everything you need to run Lean automatically. VSC is freely available for Linux, MacOS and Windows. The instructions at the following link will get you set up.

• https://lean-lang.org/lean4/doc/quickstart.html

GitHub

All the code in this course is freely available online:

• https://github.com/leanfirststeps

Welcome!

Welcome!

This blog will discuss the topics we cover as we learn th every basics of the Lean proof assistant:

• https://en.wikipedia.org/wiki/Lean_(proof_assistant)
• https://leanprover-community.github.io
• https://lean-lang.org

Audience & Scope

The reason this blog exists is to address the fact that a proof assistant is really cool, but almost all the tutorials and guides are too difficult for those of us who are not already familiar with proof assistant and advanced mathematics - and the high barrier of jargon that goes with it.

The aim is to gain enough understanding of Lean to be able to prove simple theorems, and to give us the grounding and confidence to learn more if we wish to.

Proof Assistant?

It is worth clarifying what Lean is and isn't. It isn't a magic tool for coming up with proofs. 

It is a proof verifier, which means we provide proofs and Lean checks to see if they are valid.