07 - Proof By Cases

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 a real number $x$,

$$(x=3)\vee (x=-3)$$

our task is to show

$$x^2=9$$

The symbol $\vee$  means “logical or”. The statement $P\vee Q$ means either $P$ is true, or $Q$ is true, or possibly even both are true. 

Statements of the form $P\vee Q$ are called disjunctions.

Maths

Our aim is to show $x^2=9$ follows from the hypothesis $(x=3)\vee (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{array}{rlrl}\text{(1)}& (x=3)& \vee (x=-3)& & \text{given fact}& & & \\ \text{(2)}& \text{case }x=3& & & \text{using fact }(\text{1})x^2& =(3{)}^2& & \text{using case }(\text{2})\\ & =9& & \\ & & & \\ \text{(3)}& \text{case }x=-3& & & \text{using fact }(\text{1})x^2& =(-3{)}^2& & \text{using case }(\text{3})\\ & =9& & \\ & & & \\ ◻& (x=3)\vee (x=-3)& ⟹x^2=9& & \end{array}$$

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 possibilities $x=3$ and $x=-3$ are sufficient to fully cover the hypothesis $(x=3)\vee (x=-3)$. There is no third possibility. 

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)\vee (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 hypothesis 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 see, at a glance, the structure of the proof. In additional, the Infoview restricts information to the current goal. You can enter the focussing dot by typing \. and your Lean-enabled 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 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)\vee (x=2)$$

where $x$ is a real number. 

In your proof create two cases $x=1$ and $x=2$ from the given hypothesis $(x=1)\vee (x=2)$.