Sunday, June 30, 2024

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 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$ and $c$.


Maths

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 := by
  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$ and $y$ are real numbers.


Saturday, June 29, 2024

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 := by
  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 ourselves, or any 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 := by 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 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 the rewrite tactic 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$ and $y$ are real numbers.

Friday, June 28, 2024

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 := by
  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 := by 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, there's no 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 and common methods 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 do 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.

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.


GitHub

All the code in this course is freely available online: