Mathlib has many lemmas and theorems for us to use. We can also write our own.
Here we'll create a small but convenient lemma about the natural numbers.
Task
If we pick a natural number $b$, then any other natural number $a$ must be less than or equal to $b$, or greater than or equal to $b+1$.
The following illustrates this idea.
By the definition of natural numbers, $b+1$ is the successor of $b$, so we can be sure a is not in the “gap” from b to b+1.
Our task is to create a lemma for natural numbers $a$ and $b$ that says
$$\boxed{a\le b\;\lor\;b+1\le a}$$
Let's bring this to life with an example. If we say $b=7$, but leave $a$ unspecified, the lemma tells us that either $a\le7$ or $8\le a$, which makes sense.
Maths
To prove our lemma we'll try to make use of lemmas that also exist in Mathlib, not only to shorten the proof, but also to ease the transition to a Lean proof.
$$\begin{align}a\le b\;&\lor\;b+1\le a&&\text{proof objective, }a,b\in\mathbb{N}\\&&&\\a\le b\;&\lor\;b<a&&\text{known lemma, }a,b\in\mathbb{N}\tag{1}\label{16.1}\\m+1\le n&\iff m<n&&\text{known lemma, }m,n\in\mathbb{N}\tag{2}\label{16.2}\\&&&\\a\le b\;&\lor\;b+1\le a&&\text{apply lemma }(\ref{16.2})\text{ to }(\ref{16.1})\tag*{\(\Box\)}\end{align}$$
Lemma (1) is already very close to our proof objective. It says that $a\le b\lor b<a$ for any natural numbers $a$ and $b$.
Lemma (2) says that $m+1\le n$ is equivalent to $m<n$, for natural numbers $m$ and $n$. It lets us rewrite $b<a$ as $b+1\le a$, which immediately gives us the proof objective.
Both lemmas (1) and (2) exist in Mathlib.
Code
The following Lean code creates a lemma that says either $a\le b$ or $b+1\le a$, for natural numbers $a$ and $b$.
-- 16 - Writing Our Own Lemma
import Mathlib.Tactic
lemma Nat.le_or_succ_le (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
rw [Nat.add_one_le_iff]
exact le_or_lt a b
example {c : ℕ} : c ≤ 2 ∨ 3 ≤ c := by
exact Nat.le_or_succ_le c 2
The lemma header starts with lemma Nat.le_or_succ_le to tell Lean we want to create a new lemma named Nat.le_or_succ_le.
The Nat. prefix is conventional for lemmas about natural numbers. The rest of the name le_or_succ_le tries to follow the naming convention to describe what the lemma is about.
The Lean proofs we've previously explored started with example and no name. They can be thought of as anonymous lemmas, anonymous because there was no need to refer to them after they'd been proved.
The remainder of the header declares a and b as natural numbers, and states the lemma's proposal a ≤ b ∨ b + 1 ≤ a. The round brackets around the variables (a b : ℕ) require anyone using the lemma to always provide a and b as parameters.
Our lemma is proved in just two lines of code by making effective use of existing Mathlib lemmas:
- The first line of the proof rewrites the goal using a Mathlib lemma Nat.add_one_le_iff. Let's check its header:
theorem add_one_le_iff : n + 1 ≤ m ↔ n < m :=
The rw tactic is akin to “find and replace”, so it looks at the goal a ≤ b ∨ b + 1 ≤ a and finds b + 1 ≤ a matches the left hand side of the Nat.add_one_le_iff lemma. The matched b + 1 ≤ a is rewritten with the right hand side of the lemma b < a.
- As we'll see in the Infoview, the goal is now a ≤ b ∨ b < a.
- The final line of the proof applies another Mathlib lemma le_or_lt. Let's check its header:
This lemma le_or_lt says that, given two numbers a and b, then a ≤ b ∨ b < a. This matches our current goal exactly, so we can use exact to resolve it and complete the proof.lemma le_or_lt (a b : α) : a ≤ b ∨ b < a :=
Notice how the header of the Mathlib lemma le_or_lt (a b : α) uses round brackets requiring us to provide a and b when we use it.
Infoview
Placing the cursor before rw [Nat.add_one_le_iff] shows the original proof goal.
⊢ a ≤ b ∨ b + 1 ≤ a
Moving the cursor to the start of the next line shows the rewritten goal.
⊢ a ≤ b ∨ b < a
Minimal Example
When writing your own lemmas, it is considerate to provide a minimal example showing how to use them.
The minimal example here illustrates how to use our lemma to prove $c\le2\lor3\le c$ for any natural number $c$.
With a set to c, and b set to 2, our lemma becomes c ≤ 2 ∨ 3 ≤ c. This matches the proof goal exactly, allowing us to use exact to complete the proof neatly in one line.
Forwards & Backwards
Comparing the maths and Lean proofs, we can see they are similar, but not quite the same.
- The maths proof starts with a lemma $a\le b\lor b<a$ and uses another lemma to arrive at the goal $a\le b\lor b+1\le a$.
- The Lean proof starts with the goal $a\le b\lor b+1\le a$ and uses another lemma to arrive at an equivalent statement, which happens to be a known lemma $a\le b\lor b<a$.
The proofs go in opposite directions. Where one starts, the other finishes.
Starting with the proof objective and resolving it down to known true facts, rather than building up from known facts to a proof objective, will be a little more common with Lean proofs because many of the tactics bias towards operating on the current goal.
Just for interest, the following is a Lean proof which follows the same path as the maths proof.
lemma Nat.le_or_succ_le (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
have h : a ≤ b ∨ b < a := le_or_lt a b
rw [← Nat.succ_le] at h
exact h
The left arrow in rw [← Nat.succ_le] selects the reverse direction of the bidirectional lemma.
Easy Exercise
Write a lemma for integers $a$ and $b$ that says
$$a\le b\;\lor\;b+1\le a$$
Create a minimal example illustrating how your lemma can prove the following for any integer $c$.
$$c\le-5\;\lor\;-4\le c$$
