A proof by cases divides a task into separate cases, and proves each one leads to the desired conclusion.
Task
Given the following fact about the real number $x$,
$$(x=3)\lor(x=-3)$$
our task is to show
$$x^{2}=9$$
The symbol $\lor$ means “logical or”. The statement $P \lor Q$ means either $P$ is true, or $Q$ is true, or possibly even both are true.
Statements of the form $P \lor Q$ are called disjunctions.
Maths
Our aim is to show $x^{2}=9$ follows from the hypothesis $(x=3) \lor (x=-3)$.
This hypothesis tells us that either $x=3$ is true, or $x=-3$ is true. We don't know which, so we have to consider both cases, and show the conclusion follows from each case.
The following illustrates this.
Let's write a proof by cases, making clear each step.
$$\begin{align}(x=3)&\lor(x=-3)&&\text{given fact}\tag{1}\label{7.1}\\&&&\\\text{case }x=3&&&\text{using fact }(\ref{7.1})\tag{2}\label{7.2}\\x^{2}&=(3)^{2}&&\text{using case }(\ref{7.2})\\&=9&&\\&&&\\\text{case }x=-3&&&\text{using fact }(\ref{7.1})\tag{3}\label{7.3}\\x^{2}&=(-3)^{2}&&\text{using case }(\ref{7.3})\\&=9&&\\&&&\text{}\\(x=3)\lor(x=-3)&\implies x^{2}=9&&\text{}\tag*{\(\Box\)}\end{align}$$
The given fact (1) splits into two cases, $x=3$ and $x=-3$.- The first case (2) is $x=3$. We want to prove something about $x^{2}$. This case gives us $x^{2}=(3)^{2}$, leading to the conclusion $x^{2}=9$.
- The second case (3) is $x=-3$. This gives us $x^{2}=(-3)^{2}$, also leading to the conclusion $x^{2}=9$.
The two cases $x=3$ and $x=-3$ are sufficient to fully cover the hypothesis $(x=3)\lor(x=-3)$. There is no third option. So we have shown that, given the hypothesis, $x^{2}$ is indeed always $9$.
Code
The following Lean program proves $x^{2}=9$ follows from $(x=3)\lor(x=-3)$.
-- 07 - Proof by Cases
import Mathlib.Tactic
example {x : ℤ} (h : x = 3 v x = -3) : x^2 = 9 := by
obtain ha | hb := h
· calc
x^2 = (3)^2 := by rw [ha]
_ = 9 := by norm_num
· calc
x^2 = (-3)^2 := by rw [hb]
_ = 9 := by norm_num
The proof header is no different to the ones we've seen before, setting out the variable type, the hypothesis, and the proof objective. The hypothesis is a disjunction, and uses the letter v, to denote “logical or”.
The next line is new. The obtain ha | hb := h splits the disjunction hypothesis h into ha and hb. These new hypotheses correspond to the two cases.
The Infoview will show that ha : x = 3 and hb : x = -3.
We now need to show that each case, with ha and hb as hypotheses, leads to the desired conclusion . The two calc sections, one after the other, do exactly this.
In the first calc section, we start with x^2 because that is what we want to prove something about. We use the newly created hyopthesis ha : x = 3 to justify x^2 = (3)^2, and then show this is 9 by simple arithmetic.
The second calc section is almost exactly the same, but uses the hypothesis for second case hb : x = -3.
Notice the calc sections have a dot preceding them, · calc. This focussing dot is considered good style when writing sub-proofs within a larger proof. They help us visually see, at a glance, the structure of the proof, and the Infoview restricts information to the current goal. You can enter the focussing dot by typing \. and your Lean editor should turn it into a focussing dot.
Infoview
Placing the cursor before obtain shows only one goal, the overall proof goal.
1 goal
x : ℤ
h : x = 3 v x = -3
⊢ x ^ 2 = 9
Moving the cursor after the obtain instruction, just before the first · calc, shows the two sub-goals and their respective hypotheses ha and hb.
2 goals
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9
case inr
x : ℤ
hb : x = -3
⊢ x ^ 2 = 9
Moving the cursor past the focussing dot, placing it just before calc, shows only the sub-goal and hypothesis relevant to the first case.
1 goal
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9
Easy Exercise
Write a Lean program to prove $x^{2}-3x+2=0$, given
$$(x=1)\lor(x=2)$$
where $x \in \mathbb{R}$.
In your proof create two cases $x=1$ and $x=2$ from the given hypothesis $(x=1) \lor (x=2)$.
