09 - "Or" Goal

We've seen that a hypothesis can be a disjunction or a conjunction. 

Here we look at a slightly more interesting scenario, a proof goal that is a disjunction.

Task

For integer $x$, given that $x=-1$, show that 

$$(x^2=1)\vee (x^3=1)$$

Maths

Our initial reaction might be concern at seeing $x^3=1$. Clearly $(-1{)}^3=1$ is not true. 

Remember that $P\vee Q$ being true means at least one of $P$ and $Q$ is true. If $Q$ is false, but $P$ is true, then the disjunction $P\vee Q$ is still true.

Given the hypothesis $x=-1$, if we can prove $x^2=1$ is true, then we'll have proven the disjunction $(x^2=1)\vee (x^3=1)$ is also true.

Let's write a step by step proof.

$$\begin{array}{rlrl}\text{(1)}& x& =-1& & \text{given fact}\text{(2)}& (x^2=1)& \vee (x^3=1)& & \text{proof objective }& & & \\ \text{(3)}& x^2& =1& & \text{sufficient goal }(\text{2})& & & \\ x^2& =(-1{)}^2& & \text{using fact }(\text{1})\\ & =1& & \text{using arithmetic }\\ & & & \\ ◻& (x=-1)& ⟹(x^2=1)\vee (x^3=1)& & \end{array}$$

Once we state that it is sufficient to prove $(x^2=1)$ in order to prove $(x^2=1)\vee (x^3=1)$, the rest of the proof continues in the familiar way we've seen before.

Choice

If the proof objective were $(x^2=1)\vee (x^3=-1)$, then both statements $x^2=1$ and $x^3=-1$ can be proven to be true. 

We can choose which one of the two statements we want to prove. We don't need to prove both, because proving one is sufficient for a disjunction.

Code

The following Lean program proves $(x^2=1)\vee (x^3=1)$ follows from $x=-1$.

-- 09 - Disjunctive "or" Goal

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∨ x^3 = 1 := by
  left
  calc
    x^2 = (-1)^2 := by rw [h]
    _ = 1 := by norm_num

As usual, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof objective. The objective here is a disjunction, and uses the symbol $\vee$  to denote “logical or”. 

We state our intention to prove only the “left” part of the disjunction. The instruction left does precisely this. 

The Infoview will confirm that left replaces the goal x^2 = 1 ∨ x^3 = 1 with x^2 = 1.

The rest of the proof uses the familiar calc structure to show x^2 = 1. This matches the new proof goal, and because it is sufficient, the original goal x^2 = 1 ∨ x^3 = 1 is also proven.

Infoview

Placing the cursor before the left instruction shows the original proof goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1 ∨ x ^ 3 = 1

Placing the cursor on the next line after left confirms the proof goal has been replaced by a smaller, but sufficient, goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1

This manipulation of the proof goal might appear to be a hack, something to be discouraged. In fact, it is quite common, and considered quite normal.

---

Easy Exercise

A longer disjunction could be $P\vee Q\vee R\vee S$. The instruction left selects the left-most statement $P$ as the new goal. The instruction right selects the remainder $Q\vee R\vee S$ as the new goal. 

For integer $x$, given that $x=-1$, write a Lean program to show that 

$$(x=1)\vee (x^2=1)\vee (x^3=1)$$

Both the right and left instructions will be needed to write the proof.