Here’s information about workshop 1 of the 8 workshops in my formalising mathematics course.

## Mathematical background

At Imperial I lecture part of a standard “introduction to proof” course, a compulsory course for every beginning maths undergraduate. In my lectures we cover the basics of logic, sets, functions and equivalence relations. The idea is that the students see some abstract definitions (such as injective functions) and then some simple theorems (such as the composite of two injective functions is injective) and then try some problem sheet questions where they practice their skills at putting basic proofs together on paper.

My formalising course is for more advanced students (on paper it’s for PhD students but next year there’s a rumour that I will be teaching it to final year undergraduates), so I can assume that they know how to prove that the composite of two injective functions is injective in the traditional way. The goal of this workshop is to get students proving statements at this kind of level of difficulty, in Lean.

## What I will assume

- You have installed Lean 3 and the community tools e.g. by following the instructions on the Lean community website.
- You know the pen-and-paper proofs of the results we’re talking about (e.g. that equivalence relations on a set are the same as partitions).
- (optional but helpful): you’ve had a go at the natural number game so you know the basics of what it’s all about.

## The workshop

Start by installing the course repository by following the instructions in the README on that page. NB if you skipped the Lean 3 installation part, then you can still play along by using the links on the README, but you will have a degraded (slower) Lean experience and I cannot guarantee that the links will continue to compile correctly as Lean and mathlib evolve; on the other hand, the course repository will always compile.

[ Note for nerds: you can’t *just* clone the repo. You have to install it correctly using `leanproject`

as explained in the README if you want access to Lean’s maths library (which you will need for some of the questions). ]

Open the repository using VS Code as explained in the README (you must use the “open folder” functionality of VS Code to open the entire repo, don’t just open a file or else again you won’t have access to the maths library), and find your way to the Lean files in `src/week1`

.

[note for people who have not actually downloaded and installed Lean or anything — you can still play along with this part, you can click here and then wait for a while until Lean stops saying “Lean is busy…” and switches to “Lean is ready!”. You’ll have to allow cookies I think, and you won’t get the colours, but you gets what you pays for here]

Open the first of the Lean files — `part_A_logic.lean`

. You will see some `sorry`

s in the file — they’re in red (and there are corresponding little orange dots in the area where the scrollbar is). Let’s take a look at the first sorry in this file — it’s on line 68. In this puzzle, `P`

is a *proposition*, which is a computer-science word for a general true-false statement (in particular, `P`

might not be true: 2+2=4 and 2+2=5 are both propositions in Lean). The puzzle is to prove that . The `sorry`

indicates that the proof is incomplete — it tells Lean that this proof is omitted right now.

Let’s figure out how to prove this theorem in Lean.

## Your first Lean proof.

Here is the maths proof that we’re going to formalise. We are trying to prove that if `P`

is any true-false statement, then `P`

implies `P`

. One proof of this is a boring “truth table” proof, where we just check the two cases where `P`

is true and `P`

is false. You can do this in Lean using the `tauto!`

tactic, which will in fact solve pretty much all of the problems in this first logic file. But let’s solve it “constructively”, as the computer scientists call it.

Here’s the mathematical proof we’re going to formalise. Our goal is to show that `P`

implies `P`

. So let’s start by assuming that `P`

is true. Our goal now changes into a new goal: we now have to prove that `P`

is true. But this is exactly one of our assumptions, so we are done.

Let’s step through how this looks in Lean. We have our file on the left, and another window called the “infoview” on the right, which displays the tactic state (the goal and the hypotheses — i.e., the state of Lean’s brain). Right now the tactic state should look like this:

This means that `P`

is a Proposition, and the goal (the statement after the sideways `T`

) is to prove . Now, back in the Lean file, under the `-- Prove this using intro and exact`

comment, type `intro hP`

, so it looks like this:

Don’t forget the comma. Just after you’ve typed the comma, look at the infoview. It has changed — it now looks like this:

We now have a Proposition called P, and a new hypothesis `hP`

which is the hypothesis that `P`

holds, i.e., that `P`

is true. The goal has changed too — our goal now is to prove that `P`

is true.

Note that `hP`

is just a name. We could instead of typed `intro Nigel`

and then Lean’s infoview would display `Nigel : P`

. Beginners can get confused about the difference between `P`

and `hP`

; I will say more about the difference later on, although I could make the following cryptic remark now that `P`

is what is called a *Type*, and `hP`

is a *term* of that type. We’ll come back to this. Let’s concentrate on finishing the proof right now.

Our goal is now to show that `P`

is true. But this is exactly one of our assumptions, namely `hP`

. So we can finish the proof by adding `exact hP,`

under the `intro hP`

tactic, like this:

If we take a look at the infoview just after typing that comma, we see that a good thing has happened:

You just proved a theorem in Lean! But actually there is still something wrong: you can see that the `sorry`

on the left now has a red underline on it. Clicking on `sorry`

shows you the text `tactic failed, there are no goals to be solved`

. in the infoview. We are apologising unnecessarily. Delete the `sorry`

, the error goes away, and now the proof is complete. If you look down at the bottom left hand corner of VS Code you will now see something like this:

That means that there are no errors in your file, and 39 warnings. Each theorem whose proof still has one or more `sorry`

s in generates a warning, indicating that you cheated. You should always try and keep your files so that they have no errors, and your job in the workshop is to try and decrease the number of warnings, by filling in `sorry`

s with proofs.

## The difference between P and hP

If I were to say to you “What is Fermat’s Little Theorem?” then you would probably tell me that it’s the statement that is congruent to mod , if is a prime and is an integer. If you were writing a proof and you were working mod and had a number , you could replace it with and justify this in your work by saying you were using Fermat’s Little Theorem.

This is the way mathematicians speak. But something I noticed only after I started formalising is that here they are using the phrase “Fermat’s Little Theorem” in two different ways. When asked what the theorem is, the response above is a description of the *statement* of the theorem. But in the middle of a proof, if you want to invoke it, then you are really using the *proof* of the theorem. If I were to ask you what the Riemann Hypothesis was, then you might state it, but this doesn’t mean that you can just say “now by the Riemann Hypothesis” in the middle of a proof, at least not if you want your proof to be complete, because in the middle of a proof you are only allowed to use stuff which is proved in your arguments, not just stuff which is stated.

We saw `hP : P`

above. One model of what is going on here is that `P`

is the *statement* of the proposition we’re thinking about, and `hP`

is the *proof*. I see beginners writing things like `exact P`

in their proofs. But In the proof we have to use `exact hP`

because we need to use the proof, not the statement. In fact what we are doing in this proof is constructing a function which sends proofs of `P`

to proofs of `P`

. Lean is a functional programming language, and under the hood the way Lean understands a proof of the form is as a function, or an algorithm, which takes as input a proof of `P`

and returns as output a proof of `Q`

. If you want to learn more about how Lean’s type theory models theorems and proofs, you can try this other blog post — it’s not too difficult — but you don’t really need to know about this stuff to get something out of this course.

## A second proof.

Let me go through one more proof. Let’s prove that and together imply . The `sorry`

ed proof is around like 98 or so in the file (it might have moved a bit if you typed in the earlier proof). It looks like this:

The first surprise is that there is no “and” here. The way I have formalised this statement in Lean is like this: . In words, implies that (deep breath) implies . This is of course logically the same as saying that and imply . Also worth noting is that the Lean formalisation has a disconcertingly small number of brackets in. This is because the `→`

symbol in Lean is *right associative*, which is just a fancy way of saying that if you see `P → Q → R`

it means `P → (Q → R)`

.

Our goal is hence of the form “`P`

implies something” so we can start with `intro hP,`

(or `intro Nigel`

or whatever you want to call the assumption that `P`

is true). The goal now changes to the something, which is “(`P`

implies `Q`

) implies something”, so we can continue with `intro hPQ,`

and now our tactic state looks like this:

We have two propositions, `P`

and `Q`

, and hypotheses `hP`

(saying that `P`

is true) and `hPQ`

(saying that `P`

implies `Q`

). So, exactly as advertised, we know and , and we want to prove . Next we need to learn a new tactic, the `apply`

tactic.

`apply`

is a difficult word. Humans apply all sorts of facts to deduce other facts all over the place in mathematics. In Lean, `apply`

has a very precise meaning, and we are in precisely the situation here where we can use it. If you try `apply hPQ,`

for your next move in this puzzle game, the tactic state changes to the following:

The difference: the goal has changed! Our goal used to be to come up with a proof of `Q`

. But `P`

implies `Q`

, so if we *apply this fact* then we see that it suffices to come up with a proof of `P`

instead. That is what the `apply`

tactic does — it reduces our problem to a simpler one by applying an implication. You can only use the `apply h`

tactic if `h`

is an implication, or a series of implications, which ultimately imply your goal.

The rest is easy — `exact hP`

, or even the `assumption`

tactic (which closes any goal which happens to be one of your assumptions) will work.

## Try the rest on your own.

The rest is up to you. I have put model solutions in the `solutions`

directory. You will need to know a few more tactics than these three — I have explained them in the week 1 README. Thanks for coming to my course, and good luck!

## Post workshop thoughts.

There was far too much material for a beginner to complete within 2 hours. Most people did not even finish Part A. In some sense, there was a lot of material designed to hammer home a few basic tactics again and again. I don’t think it matters if students don’t make it through the material. I’m going to press on next week and do basic group theory and subgroups.

Interchanging a and b in the definition of the map from partitions to equivalence relations leads to simpler proofs: https://github.com/alreadydone/formalising-mathematics/commit/3471623093dc25dbe0c81d13d621abbc5824e2c4#diff-e9da3c1e3976fb64f273b71c867e381551844a150f7bb8dbcf733a3b17a507c0

Without the interchange, it’s best to reuse the fact that inv_fun P is a symmetric relation; the way to do this that I figured out is at https://github.com/alreadydone/formalising-mathematics/commit/3471623093dc25dbe0c81d13d621abbc5824e2c4#diff-80fbf2d68e758b84fa69751b0b792ef6633998c6b98452498caad397b3c2a067R283

Let me know if there’s a more elegant way!

LikeLike

Oh interesting! Thanks a lot for pointing this out!

LikeLike