In this last post of Part I, we make a start on proofs which have more structure than a simple direct calculation.
The proof we examine derives an intermediate result, which we make use of later in the full proof.
Task
Given the following facts about integers $a$ and $b$,
$$\begin{align}a&=b+1\\b-1&=0\end{align}$$
our task is to show
$$a=2$$
Maths
Most mathematicians would glance at the facts and immediately find $b=1$, and then use this in $a=b+1$ to give $a=2$.
Let's write this out, making clear each step.
$$\begin{align}a&=b+1&&\text{given fact}\tag{1}\label{6.1}\\b-1&=0&&\text{given fact}\tag{2}\label{6.2}\\&&&\\b-1&=0&&\text{using fact }(\ref{6.2})\\b&=1&&\text{adding 1 to both sides }\tag{3}\label{6.3}\\&&&\\a&=b+1&&\text{using fact }(\ref{6.1})\\&=(1)+1&&\text{using intermediate result }(\ref{6.3})\\a&=2&&\text{using arithmetic}\tag*{\(\Box\)}\end{align}$$
We've derived an intermediate result $b=1$ at line (3), and used it later at line (4). This is not something we've done before.
Notice how we justify $b=1$ from $b-1=0$ by adding 1 to both sides. This is an uncontroversial step when working with integers, and deeper justification would be disproportionate.
Learning to think in Lean might have encouraged us to rewrite $a=b+1$ as $a=b-1+1+1$, and then use the given fact $b-1=0$ to remove $b-1$ from the expression to give $a=(0)+1+1=2$.
This trickery is not as natural as establishing $b=1$ as an intermediate result. Fortunately, Lean supports the creation and subsequent use of intermediate results.
Code
The following Lean program proves $a=2$ given $a=b+1$ and $b-1=0$. It creates and makes use of an intermediate result, $b=1$.
-- 06 - Intermediate Result
import Mathlib.Tactic
example {a b : ℤ} (h1 : a = b + 1) (h2: b - 1 = 0) : a = 2 := by
have h3: b = 1 := by linarith [h2]
calc
a = b + 1 := by rw [h1]
_ = 1 + 1 := by rw [h3]
_ = 2 := by norm_num
Let's examine this proof starting at the end with the familiar calc section. We want to prove something about a and so we start with a = b + 1 justified by the first hypthesis h1. We then rewrite b + 1 as 1 + 1, justifying it with a hypothesis named h3. This is not a hypothesis that was given as part of the theorem statement, but derived as an intermediate result. Finally, we have 1 + 1 calculated as 2 using the norm_num tactic to do arithmetic. This gives us the desired a = 2.
Let's now focus on the creation of the intermediate result b = 1. Looking at the code, we can see it is given a label h3, similar to how given facts are labelled in the proof header. This intermediate result does need to be justified, and this is done by “adding 1 to both sides” of h2 using the tactic linarith for linear arithmetic.
The instruction have is what establishes the new hypothesis h3 alongside the existing h1 and h2.
Infoview Again
As we develop and debug Lean proofs, it is useful to keep track of what Lean thinks are the hypotheses it can use. The Infoview gives us this insight.
Placing the cursor before the have instruction tells us the state of play before the new hypothesis is created. You should see the following in the Infoview.
a b : ℤ
h1 : a = b + 1
h2 : b - 1 = 0
⊢ a = 2
At this point Lean knows that a and b are integers, that there are two hypotheses h1 : a = b + 1 and h2 : b - 1 = 0, and that the proof goal is a = 2.
Moving the cursor to the beginning of the next line, just before calc, gives us the following.
a b : ℤ
h1 : a = b + 1
h2 : b - 1 = 0
h3 : b = 1
⊢ a = 2
We can see a new hypothesis h3 : b = 1 has been added to the existing h1 and h2.
Easy Exercise
Write a Lean program to prove $a=2$, given
$$\begin{align}a&=b+c\\b-1&=0\\c+1&=2\end{align}$$
where $a,b,c\in\mathbb{Z}$.
In your proof create and use two intermediate results, $b=1$ and $c=1$.
