Some lemmas are bidirectional implications. To apply them, we need to decide which of the two directions match our task.
Here we'll apply such a lemma to help solve an equation.
Task
Given the zero product
$$(p-1)\cdot(q-2)=0$$
show that
$$p=1\text{ or }q=2$$
where $p$ and $q$ are rational numbers.
Maths
It is common knowledge that the product of two numbers, $a$ and $b$, is zero, if and only if, one or the other is zero.
We'll think of this as a lemma,
$$a\cdot b=0\iff(a=0)\lor(b=0)$$
A statement of the form $P\iff Q$ is equivalent to both of the following being true:
- $P\implies Q$
- $Q\implies P$
We say “$P$ is true if and only if $Q$ is true” or “$P$ is true iff $Q$ is true.”
So our lemma is equivalent to the following two statements:
- $a\cdot b=0\implies(a=0)\lor(b=0)$
- $(a=0)\lor(b=0)\implies a\cdot b=0$
The antecedent of the first matches our hypothesis $(p-1)\cdot(q-2)=0$, so applying it gives us a disjunction.
$$(p-1=0)\lor(q-2=0)$$
We could conclude $p=1$ or $q=2$ just by looking at this, but to write a Lean proof we'll need to plan out more detail.
$$\begin{align}(p-1)\cdot(q-2)&=0&&\text{hypothesis}\tag{1}\label{15.1}\\&&&\\a\cdot b=0&\iff(a=0)\lor(b=0)&&\text{existing lemma}\tag{2}\label{15.2}\\&&&\\(p-1=0)&\lor(q-2=0)&&\text{apply lemma }(\ref{15.2})\text{ to }(\ref{15.1})\tag{3}\label{15.3}\\&&&\\\text{case }p-1=0&&&\text{using }(\ref{15.3})\\p&=1&&\text{add 1 to both sides}\\&&&\\\text{case }q-2=0&&&\text{using }(\ref{15.3})\\q&=2&&\text{add 2 to both sides}\\&&&\\(p=1)&\lor(q=2)&&\text{conclusion}\tag*{\(\Box\)}\end{align}$$
The key step is applying the lemma (2) to the hypothesis (1) to derive a new intermediate result (3).
This intermediate result is a disjunction $(p-1=0)\lor(q-2=0)$, and so the proof proceeds as a proof by cases.
Code
The following Lean program proves that $p=1$ or $q=2$ given $(p-1)\cdot(q-2)=0$, where $p,q\in\mathbb{Q}$.
-- 15 - Using Lemmas: Multiplied Factors Equal Zero
import Mathlib.Tactic
example {p q : ℚ} (h : (p - 1) * (q - 2) = 0) : p = 1 ∨ q = 2 := by
apply mul_eq_zero.mp at h
obtain hp | hq := h
· left
linarith
· right
linarith
Mathlib has a lemma mul_eq_zero which expresses the idea we want to use, that $a\cdot b=0\iff(a=0)\lor(b=0)$. Let's take a look at its definition.
theorem mul_eq_zero : a * b = 0 ↔ a = 0 ∨ b = 0 :=
The first line of the proof applies mul_eq_zero to hypothesis h, but the lemma name has a .mp appended.
- Adding .mp to a bidirectional lemma selects the forward direction.
- Adding .mpr to a bidirectional lemma selects the reverse direction.
The mp is “modus ponens”, terminology from the field of logic for the process of reaching a conclusion using an implication.
The Infoview will confirm the hypothesis has been replaced with the equivalent disjunction p - 1 = 0 ∨ q - 2 = 0.
The proof then proceeds as a proof by cases.
- The obtain instruction splits the hypotheses h into two cases, p - 1 = 0 and q - 2 = 0. The proof then uses focussing dots to organise the sub-proofs for each of these cases.
- The first case uses left to state our intention to prove the left side of the disjunctive proof goal, p = 1. The linarith tactic can perform an “add a number to both sides” step to justify the goal p = 1 from the current hypotheses, one of which is hp : p - 1 = 0.
- The second case is almost the same, but we use right to state our intention to prove the right side of the disjunctive proof goal, q = 2.
Both cases, p - 1 = 0 and q - 2 = 0, confirm the same disjunctive proof goal, so the proof is complete.
Replacing A Hypothesis?
In the maths proof we derived an intermediate result from the hypothesis, but in the Lean code the hypothesis was replaced.
Mathematically, the original hypothesis (1) always holds. The lemma allows us to derive an equivalent, but more useful, intermediate result (3). Because it is equivalent, we could replace the original hypothesis, but that's not how we write maths proofs.
In the Lean proof, the apply tactic does actually replace the original hypothesis. This is valid only because the new hypothesis is equivalent to the original. If we wanted to preserve the original hypothesis, we could use have to create a new intermediate result.
Infoview
Placing the cursor before apply mul_eq_zero.mp at h shows the original hypothesis.
h : (p - 1) * (q - 2) = 0
Moving the cursor to the beginning of the next line shows the hypothesis has been replaced.
h : p - 1 = 0 ∨ q - 2 = 0
Easy Exercise
Write a Lean program to prove $(p-1)\cdot(q-2)\ne0$ given $p-1\ne0$ and $q-2\ne0$, where $p$ and $q$ are rational numbers.
Use the lemma mul_ne_zero_iff. Look up the definition to understand what it says, then decide in which direction to apply it.
