In this final Part IV we'll explore some more interesting kinds of proof.
Here we'll take a first look at proof by contradiction.
Task
Given these two facts about natural numbers $a$ and $b$,
$$(a=5) \implies (b=6)$$
$$b=7$$
show that
$$\neg a=5$$
The symbol $\neg$ means negation, and can be read as “it is not the case that”.
So here, $\neg a=5$ reads as “it is not the case that $a=5$”, or more simply, “$a$ is not 5.”
Maths
Looking at $a=5\implies b=6$ tells us that if $a=5$ then $b=6$. But $b$ is supposed to be 7. So it can't be the case that $a=5$.
This intuition matches the more formal approach we'll take.
To prove a statement is false we show that applying correct logical steps to it leads to a contradiction. This is called proof by contradiction.
Let's say that again, but with symbols. To show $\neg P$ we need to show the statement $P$ leads to a contradiction.
For our task, $P$ is $a=5$. So, to show $\neg a=5$, we need to show $a=5$, if taken as a hypothesis, leads to a contradiction.
Let's do this in small steps.
\begin{align}(a=5)&\implies(b=6)&&\text{given fact}\tag{1}\label{19.1}\\b&=7&&\text{given fact}\tag{2}\label{19.2}\\&&&\\\neg a&=5&&\text{proof objective}\\&&&\\\text{assume }a&=5&&\text{for contradiction}\tag{3}\label{19.3}\\b&=6&&\text{using }(\ref{19.1})\\&\ne7&&\text{arithmetic}\tag{4}\label{19.4}\\&&&\\\text{(\ref{19.4})}&\text{ contradicts (\ref{19.2})}&&\text{(\ref{19.3}) must be false}\tag*{\(\Box\)}\end{align}
Proof by contradiction is sometimes called reductio ad absurdum, Latin for “reduction to absurdity”. In our example, the absurdity is the notion that $b=6$ and $b=7$ are both true.
Code
The following Lean program proves $\neg a=5$, given $a=5\implies b=6$ and $b=7$, for natural numbers $a$ and $b$.
-- 19 - Proof by Contradiction
import Mathlib.Tactic
example {a b : ℕ} (h1: a = 5 → b = 6) (h2: b = 7) : ¬a = 5 := by
by_contra g
apply h1 at g
have h2x : ¬b = 7 := by linarith
contradiction
As we saw earlier, to prove $\neg P$ we assume $P$ is true and derive a contradiction. The by_contra g starts this journey. It takes the goal ¬a = 5, creates a new hypothesis g : a = 5, and then sets the goal to False.
A goal of False means we have to show a contradiction. How do we do this in Lean?
We do it by arranging for two contradictory hypotheses to exist, one of the form Q and the other ¬Q. The two need to be exactly the same, except one has a negation in front of it. Once that's done, we use contradition to resolve the False goal.
The code between by_contra g and contradiction has only one purpose, to arrange for two contradictory hypotheses. Let's break it down:
- The first hypothesis h1 : a = 5 → b = 6 is applied to the newly created hypothesis g : a = 5. Because g matches the antecedent of h1, g is changed to b = 6.
- b = 6 contradicts the second hypothesis h2 : b = 7 but we need to arrange for hypotheses of the form Q and ¬Q.
- To do this we create a new intermediate result h2x : ¬b = 7, justified by the linarith tactic. This tactic is surprisingly capable. It will search the current hypotheses by itself to find any that will help, and it can justify the leap from b = 6 to ¬b = 7.
- We now have two directly contradictory hypotheses, the given h2 : b = 7 and the derived h2x : ¬b = 7. We're now ready to use contradiction to complete the proof.
Infoview
Placing the cursor before by_contra g shows the original proof goal.
⊢ ¬a = 5
Moving the cursor to the start of the next line shows a = 5 has been added as hypothesis g, and the proof goal changed to False.
g : a = 5
⊢ False
Placing the cursor just before contradiction shows the two directly contradictory hypotheses h2 and h2x.
h2 : b = 7
g : b = 6
h2x : ¬b = 7
Easy Exercise
Write a Lean program to prove $\neg a=5$, given $a>5\iff b=6$ and $b=6$.
Here $a$ and $b$ are natural numbers.
