In Part III we'll practise using lemmas and definitions in our proofs.
There is a huge body of commonly agreed knowledge that mathematicians refer to in their own proofs. A large, and ever-growing, number of these lemmas, theorems, and definitions are encoded in the Mathlib library, ready for us to use in our own Lean proofs.
We'll start by using the definition of an odd number.
Task
Show the integer 13 is odd.
Maths
To show 13 is odd, we need to show it meets the definition of odd.
An odd integer is of the form $2k+1$, where $k$ is an integer.
In more mathematical phrasing; if there exists an integer $k$ such that $n=2k+1$, then $n$ is odd.
The task has become an existence proof. If we can find an integer $k$ such that $13=2k+1$, then we have shown 13 is odd.
Let's write out a step by step proof.
$$\begin{align}13&\text{ is odd}&&\text{proof objective }\\&&&\\\exists k\in\mathbb{Z}[n=2k+1]&\implies n\text{ is odd}&&\text{definition of odd}\tag{1}\label{12.1}\\&&&\\\exists k\in\mathbb{Z}[13=2k+1]&&&\text{sufficient goal, using }(\ref{12.1})\\&&&\\\text{use }k=6&&&\text{chosen example}\tag{2}\label{12.2}\\13&=2(6)+1&&\text{using }(\ref{12.2})\\&&&\\13=2(6)+1&\implies13\text{ is odd}&&\text{by definition }(\ref{12.1})\tag*{\(\Box\)}\end{align}$$
This may look a little laborious, but the detail will help us develop a Lean proof. .
We start with the proof objective, to show $13$ is odd.
We then state the definition, that $n$ is odd if it can be written in the form $2k+1$, where $k$ is an integer.
So, to show $13$ is odd, it is sufficient to show it can be written in the form $2k+1$. This gives us a new goal, to show there exists an integer $k$ such that $13=2k+1$.
We choose $k=6$, and confirm that $13=2(6)+1$.
We have shown that $13$ can indeed be written in the form $2k+1$. And so, by the definition of odd, we have finally shown that $13$ is odd.
Code
The following Lean program proves the integer 13 is odd.
-- 12 - Definition: Odd Number
import Mathlib.Tactic
example : Odd (13: ℤ) := by
dsimp [Odd]
use 6
norm_num
The proof objective states that 13 is Odd.
If we had simply written Odd 13 as the proof objective, 13 would be interpreted, by default, as a natural number. We write (13: ℤ) to specify 13 as an integer.
The idea of Odd is defined in Mathlib. The next line dsimp [Odd] expands that definition in the Infoview so we can see what it actually is. We'll see below the goal changes from being displayed as Odd 13, to ∃ k, 13 = 2 * k + 1, which we recognise as the definition of odd applied to 13.
The instruction dsimp has no effect on the proof itself. It only changes how Odd is displayed in the Infoview.
After this point, the proof proceeds as a simple existence proof.
The instruction use 6 tells Lean we want to try 6 for k. This changes the goal to 13 = 2 * 6 + 1. We resolve this goal by arithmetic, using the norm_num tactic. For such a simple and clear goal, there is no need for a multi-line calc section.
What is Odd?
The proof objective was written as Odd (13: ℤ). The intention is for this to be a statement saying 13 is an odd number.
How does this work?
The idea of Odd is defined in Mathlib as a function. A definition is distinct from a lemma, and Mathlib contains many of both. A lemma needs to be justified by proof, but a definition does not.
That function Odd takes one parameter, and outputs a proposition involving that parameter, which may or may not be true.
When applied to 13, the output is a proposition ∃k such that 13 = 2*k + 1. This proposition is true because we can prove it.
If we applied Odd to 14, the output is a proposition ∃k such that 14 = 2*k + 1. This proposition is not true because there is no proof for it.
It is interesting to see the actual definition of Odd inside Mathlib:
def Odd (a : α) : Prop := ∃ k, a = 2 * k + 1
We can see how a is mapped to a proposition about a.
Infoview
The Infoview is particularly useful when working with definitions and existence proofs.
Placing the cursor before dsimp [Odd] shows the original proof goal.
⊢ Odd 13
Moving the cursor to the end of the line after dsimp [Odd] shows the goal is now displayed using the definition of Odd.
⊢ ∃ k, 13 = 2 * k + 1
Placing the cursor after use 6 shows the goal is now specific to k = 6.
⊢ ∃ k, 13 = 2 * 6 + 1
Easy Exercise
Write a Lean program to prove the integer 14 is even.
Your proof should use Mathlib's definition Even for even numbers. Use dsimp to see how the definition is applied to 14.
