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 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 := 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 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}$.
