Maths Proofs in Lean - First Steps is now available in paperback, hardback and ebook format:
The content on this website will remain free and open.
There are small differences, mostly to help with page layout and typesetting in the book - to avoid typographical orphans for example.
The following is the famous Fibonacci sequence.
$$ 1,\;1,\;2,\;3,\;5,\;8,\;13,\;21,\;\ldots $$
From 2 onwards, each number is the sum of the previous two. This is an example of a recursive definition.
Here we'll see how to define and work with a recursively defined function.
The following is a recursively defined function $f_{n}$. It takes a natural number n, and returns a natural number.
$$f_{n}=\begin{cases}\:0 & \;\text{if }n=0\\\:2n-1+f_{n-1} & \;\text{otherwise}\end{cases}\tag{1}\label{22.1}$$
Let's see how it works.
What makes the definition recursive is that, apart from $f_{0}$, each value of the function $f_{n}$ is defined in terms of an earlier value $f_{n-1}$. Informally, the function is defined in terms of itself.
Our task is to prove this recursively defined function has a much neater closed form,
$$f_{n}=n^{2}$$
It is worth pausing to reflect on the process of calculating each $f_{n}$.
It looks very similar to the process of induction we saw in the last chapter.
We'll try a proof by induction. Let $P(n)$ be the proposition $f_{n}=n^{2}$.
The base case $P(0)$ is the proposition $f_{0}=0^{2}$. The definition tells us $f_{0}=0$ so the base case $P(0)$ is indeed true.
The inductive step is the implication $P(n)\implies P(n+1)$. To prove this we assume $P(n)$ is true and derive $P(n+1)$. That is, we assume $f_{n}=n^{2}$ and derive $f_{n+1}=(n+1)^{2}$.
We have shown the base case $P(0)$ and the inductive step $P(n)\implies P(n+1)$ are true, and so, by induction, $P(n)$ is true for all natural numbers $n$. That is, $f_{n}=n^{2}$ is true for all $n$.
Let's write this out as preparation for a Lean proof.
$$\begin{align}P(n):f_{n}&=n^{2}&&\text{proof objective}\\&&&\\\text{base case }P(0)&&&\\&&&\\f(0)&=0&&\text{by definition }(\ref{22.1})\\&=0^{2}&&\text{so }P(0)\text{ is true}\\&&&\\\text{inductive step }P(n)&\implies P(n+1)&&\\&&&\\P(n):f_{n}&=n^{2}&&\text{induction hypothesis}\tag{2}\label{22.2}\\&&&\\f_{n+1}&=2\cdot n-1+f_{n}&&\text{by definition }(\ref{22.1})\\&=2\cdot n-1+n^{2}&&\text{by }(\ref{22.2})\\&=(n+1)^{2}&&\text{so }P(n+1)\text{ is true}\\&&&\\P(n):f_{n}&=n^{2}&&\text{by induction}\tag*{\(\Box\)}\end{align}$$
The following Lean program proves, by induction, that $f_{n}=n^{2}$.
-- 22 - Recursion
import Mathlib.Tactic
def f : ℕ → ℕ
| 0 => 0
| n + 1 => 2 * n + 1 + f n
#eval f 2
example {n: ℕ} : f n = n^2 := by
induction n with
| zero =>
calc
f 0 = 0 := by rw [f]
_ = 0^2 := by norm_num
| succ n ih =>
calc
f (n + 1) = 2 * n + 1 + f n := by rw [f]
_ = 2 * n + 1 + n^2 := by rw [ih]
_ = (n + 1)^2 := by ring
This code is in three parts. Let's look at each in turn.
The first part is the recursive definition of f.
The f : ℕ → ℕ declares f as a function which maps natural numbers to natural numbers.
Even though the code is new, we can see how it maps 0 to 0, and n + 1 to 2 * n + 1 + f n. Here f n means “f applied to n”, which is just $f_{n}$.
Our earlier definition (1) mapped $n\mapsto2n-1+f_{n-1}$. We can't use $f_{n-1}$ in the Lean definition because $(n-1)$ does not exist for all natural numbers $n$. By replacing $n$ with $n+1$, we get the equivalent $n+1\mapsto2n+1+f_{n}$.
The second part tests our function behaves as we expect.
The #eval is a special instruction which evaluates an expression and prints the answer in the Infoview. Just as #eval 2 + 3 will print 5, #eval f 2 will evaluate the function f applied to 2, and print the answer. Try evaluating f with other parameters.
The third part is the proof of the proposition f n = n^2.
This proof by induction is not very different to the one we saw in the last chapter.
We saw earlier the similarity between the process of induction and the evaluation of a recursively defined function.
We now see the similarity between the structure of an induction proof and the definition of a recursively defined function.
These similarities are not a coincidence. If you're curious to find out more, search the more advanced guides for recursive types.
Placing the cursor after #eval f 2 shows the result of the function f applied to 2.
4
Changing the code to #eval f 3 shows the result of the function f applied to 3.
9
The following is a recursively defined function $g_{n}$, which maps natural numbers to integers,
$$g_{n}=\begin{cases}\:1 & \;\text{if }n=0\\\:(-1)\cdot g_{n-1} & \;\text{otherwise}\end{cases}$$
Write a recursive definition for $g_n$ in Lean, then show, by induction, that $g_{n}=(-1)^{n}$.
Induction is a powerful idea that can dramatically simplify some proofs that would otherwise be quite hairy.
Here we'll see how simple induction can unlock a not-so-simple task.
Prove the following is true for every natural number $n$,
$$2^{n}\ge n+1$$
It is not immediately obvious how to do this in our head.
Let's introduce the idea of induction. To prove a proposition $P$ is true for any natural number n, we need to show two things:
The following illustrates how these two things together allow us to prove $P(n)$ is true for all n. We can see why some describe induction as knocking over dominoes.
For our task, let $P(n)$ be the proposition $2^{n}\ge n+1$. We need to show both the base case and the inductive step.
The base case $P(0)$ is the proposition $2^{0}\ge 0+1$. Because $2^{0}=1\ge 1$, the base case $P(0)$ is true.
The inductive step is the implication $P(n)\implies P(n+1)$. To prove this implication, we assume $P(n)$ is true and derive $P(n+1)$. That is, we assume $2^{n}\ge n+1$ and derive $2^{n+1}\ge(n+1)+1$.
In the inductive step, the assumption that $P(n)$ is true is called the induction hypothesis.
We have shown the base case $P(0)$ and the inductive step $P(n)\implies P(n+1)$ are true, and so, by induction, we can say $P(n)$ is true for all natural numbers $n$.
Let's write this out in a form that takes us towards a Lean proof.
$$\begin{align}P(n):2^{n}&\ge n+1&&\text{proof objective}\\&&&\\\text{base case }P(0)&&&\\&&&\\2^{0}&=1&&\\&\ge0+1&&\text{so }P(0)\text{ is true}\\&&&\\\text{inductive step }P(n)&\implies P(n+1)&&\\&&&\\P(n):2^{n}&\ge n+1&&\text{induction hypothesis}\tag{1}\label{21.1}\\&&&\\2^{n+1}&=2\cdot2^{n}&&\\&\ge2\cdot(n+1)&&\text{by }(\ref{21.1})\\&=(n+1)+1+n&&\\&\ge(n+1)+1&&\text{so }P(n+1)\text{ is true}\\&&&\\P(n):2^{n}&\ge n+1&&\text{by induction}\tag*{\(\Box\)}\end{align}$$
The following Lean program proves, by induction, that $2^{n}\ge n+1$ for all natural numbers $n$.
-- 21 - Simple Induction
import Mathlib.Tactic
example {n : ℕ} : 2^n ≥ n + 1 := by
induction n with
| zero =>
norm_num
| succ n ih =>
calc
2^(n + 1) = 2 * 2^n := by ring
_ ≥ 2 * (n + 1) := by rel [ih]
_ = (n + 1) + 1 + n := by ring
_ ≥ (n + 1) + 1 := by norm_num
The proof header is as we'd expect, but the rest of the proof has a structure we've not seen before.
The induction is started using induction n with which tells Lean we want to do induction on the variable n. We need to specify the variable because some tasks may have more than one variable.
After that we have two sections, starting with | zero => for the base case, and | succ n ih => for the inductive step.
Placing the cursor before induction n with shows the original proof goal.
⊢ 2 ^ n ≥ n + 1
Moving the cursor to the start of the next line | zero => shows the goal for the base case.
⊢ 2 ^ 0 ≥ 0 + 1
Placing the curser just before | succ n ih => shows the goal for the inductive step, and also the inductive hypothesis ih.
ih : 2 ^ n ≥ n + 1
⊢ 2 ^ (n + 1) ≥ n + 1 + 1
Write a Lean program to prove, by induction, that
$$3^{n}\ge n+1$$
for any natural number $n$.
When we explored proof by cases, each case led to the proof objective.
In general, not all cases permitted by a hypothesis will lead to the proof objective. Some cases may lead to a contradiction, meaning they are ruled out as possible cases.
If P is a proposition, show that
$$\neg(\neg P)\implies P$$
We may be tempted to cancel the two negations on the left. For this task we'll pretend we don't yet know this is a valid simplification.
We haven't specified what proposition $P$ is. That means our theorem, if we can prove it, will hold for any proposition.
So proving $\neg(\neg P)\implies P$ will justify our intuition that two negations do indeed cancel out.
A fundamental idea is that a proposition is either true or false, and there is no other possibility. This is called the Law of the Excluded Middle.
It means there are only two possibilities for our proposition $P$. It is either true, or it is false.
Let's consider each case.
To summarise, we've shown that $P$ true is possible, but $P$ false is not.
A couple of points about our reasoning are worth explaining.
First, two statements of the form $Q$ and $\neg Q$ are contradictory. This is how, in the second case, we justify $\neg P$ and $\neg(\neg P)$ are contradictory.
Second, it may look like a circular argument that the first case assumes $P$ is true to prove $P$ is true. It isn't circular because we consider all the possibilities for $P$, which here means considering $P$ is false. It just so happens we then rule out this possibility.
Let's try to write this in small steps as preparation for a Lean proof.
\begin{align}\neg(\neg P)&\implies P&&\text{proof objective}\\&&&\\&\neg(\neg P)&&\text{hypothesis}\tag{1}\label{20.1}\\&P&&\text{proof goal}\tag{2}\label{20.2}\\&&&\\P&\lor\neg P&&\text{law of excluded middle}\tag{3}\label{20.3}\\&&&\\\text{case }P&&&\text{using fact }(\ref{20.3})\\&P&&\text{proof goal}\\&&&\\\text{case }\neg P&&&\text{using fact }(\ref{20.3})\\&\neg P&&\text{contradicts hypothesis }(\ref{20.1})\\&&&\text{}\\\neg(\neg P)&\implies P&&\text{only consistent case}\tag*{\(\Box\)}\end{align}
We've not proved an implication before so let's clarify how it's done. To prove an implication $A\implies B$, we assume $A$ as a hypothesis and then prove $B$.
So to prove $\neg(\neg P)\implies P$, we take $\neg(\neg P)$ as a hypothesis (1) and set $P$ as a proof goal (2).
The rest is a proof by cases, and proceeds just as we discussed above.
The following Lean program proves $\neg(\neg P)\implies P$, where $P$ is a proposition.
-- 20 - Contradictory Cases
import Mathlib.Tactic
example {P : Prop} : ¬(¬P) → P := by
intro g
by_cases h : P
· exact h
· contradiction
The proof header declares P as a proposition using {P : Prop}.
The proof starts with intro g which converts the proof objective, the implication ¬(¬P) → P, into a hypothesis g : ¬¬P and a new goal P.
Next, by_cases h : P creates the two cases for P using the Law of the Excluded Middle. Just like a proof by cases, Lean will replace the current goal with two new separate goals, one with h : P as a hypothesis, the other with h : ¬P as a hypothesis.
The rest of the proof handles each case, using focussing dots to organise the sub-proofs.
Placing the cursor before intro g shows the original proof goal.
⊢ ¬¬P → P
Moving the cursor to the start of the next line shows ¬¬P established as a new hypothesis g, and P set as the new goal.
g : ¬¬P
⊢ P
Placing the curser after by_cases h : P shows the two new goals, one for each case.
case pos
P : Prop
g : ¬¬P
h : P
⊢ P
case neg
P : Prop
g : ¬¬P
h : ¬P
⊢ P
If $P$ is a proposition, write a Lean program to show that
$$P\implies\neg(\neg P)$$
To keep the proof as short as the example above, try applying the law of the excluded middle, not to $P$, but to $(\neg P)$.
In this final Part IV we'll explore some more interesting kinds of proof.
Here we'll take a first look at proof by contradiction.
Given these two facts about natural numbers $a$ and $b$,
$$(a=5) \implies (b=6)$$
$$b=7$$
show that
$$\neg a=5$$
The symbol $\neg$ means negation, and can be read as “it is not the case that”.
So here, $\neg a=5$ reads as “it is not the case that $a=5$”, or more simply, “$a$ is not 5.”
Looking at $a=5\implies b=6$ tells us that if $a=5$ then $b=6$. But $b$ is supposed to be 7. So it can't be the case that $a=5$.
This intuition matches the more formal approach we'll take.
To prove a statement is false we show that applying correct logical steps to it leads to a contradiction. This is called proof by contradiction.
Let's say that again, but with symbols. To show $\neg P$ we need to show the statement $P$ leads to a contradiction.
For our task, $P$ is $a=5$. So, to show $\neg a=5$, we need to show $a=5$, if taken as a hypothesis, leads to a contradiction.
Let's do this in small steps.
\begin{align}(a=5)&\implies(b=6)&&\text{given fact}\tag{1}\label{19.1}\\b&=7&&\text{given fact}\tag{2}\label{19.2}\\&&&\\\neg a&=5&&\text{proof objective}\\&&&\\\text{assume }a&=5&&\text{for contradiction}\tag{3}\label{19.3}\\b&=6&&\text{using }(\ref{19.1})\\&\ne7&&\text{arithmetic}\tag{4}\label{19.4}\\&&&\\\text{(\ref{19.4})}&\text{ contradicts (\ref{19.2})}&&\text{(\ref{19.3}) must be false}\tag*{\(\Box\)}\end{align}
Proof by contradiction is sometimes called reductio ad absurdum, Latin for “reduction to absurdity”. In our example, the absurdity is the notion that $b=6$ and $b=7$ are both true.
The following Lean program proves $\neg a=5$, given $a=5\implies b=6$ and $b=7$, for natural numbers $a$ and $b$.
-- 19 - Proof by Contradiction
import Mathlib.Tactic
example {a b : ℕ} (h1: a = 5 → b = 6) (h2: b = 7) : ¬a = 5 := by
by_contra g
apply h1 at g
have h2x : ¬b = 7 := by linarith
contradiction
As we saw earlier, to prove $\neg P$ we assume $P$ is true and derive a contradiction. The by_contra g starts this journey. It takes the goal ¬a = 5, creates a new hypothesis g : a = 5, and sets the goal to False.
A goal of False means we have to show a contradiction. How do we do this in Lean?
We do it by arranging for two contradictory hypotheses to exist, one of the form Q and the other ¬Q. The two need to be exactly the same, except one has a negation in front of it. Once that's done, we use contradition to resolve the False goal.
The code between by_contra g and contradiction has only one purpose, to arrange for two contradictory hypotheses. Let's break it down:
Placing the cursor before by_contra g shows the original proof goal.
⊢ ¬a = 5
Moving the cursor to the start of the next line shows a = 5 has been added as hypothesis g, and the proof goal changed to False.
g : a = 5
⊢ False
Placing the cursor just before contradiction shows the two directly contradictory hypotheses h2 and h2x.
h2 : b = 7
g : b = 6
h2x : ¬b = 7
Write a Lean program to prove $\neg a=5$, given $a>5\iff b=6$ and $b=6$.
Here $a$ and $b$ are natural numbers.
At the start of Part III we used Mathlib's definition of odd and even numbers.
Here we'll create our own definition of triangle numbers.
The following picture illustrates triangle numbers. The first few are 1, 3, 6, 10, 15, 21 and 28.
In general, the $n$th triangle number is
$$\frac{n \cdot (n+1)}{2}$$
We saw previously the Mathlib definition of Odd didn't produce the $n$th odd number. Instead the definition is a proposition about a supplied number. So Odd 3 is true, but Odd 4 is false.
Our task is to create a definition of triangle numbers that is a proposition, true only if the supplied number is actually a triangle number.
A proposition for a triangle number $T$ could be:
$$\exists n\in\mathbb{N}\quad[\;T=\frac{n\cdot(n+1)}{2}\;]$$
This proposition is only true if $T$ is a triangle number. That is, if $T$ can be expressed in the form $n\cdot(n+1)/2$ for some natural number $n$.
When working with natural numbers, we should be cautious about dividing them. In this case division is safe because either $n$ or $(n+1)$ is an even number, and so $n \cdot (n+1)$ is divisible by $2$.
Even so, let's avoid division of natural numbers as good practice. We'll adjust the proposition to the equivalent:
$$\exists n\in\mathbb{N}\quad[\;2 T=n\cdot(n+1)\;]$$
That is, $T$ is a triangle number if $2 T$ can be expressed in the form $n\cdot(n+1)$ for some natural number $n$.
The following Lean code creates a definition of triangle numbers.
-- 18 - Our Own Definition
import Mathlib.Tactic
def Triangle (a : ℕ) : Prop := ∃ n, 2 * a = n * (n + 1)
example : Triangle 10 := by
dsimp [Triangle]
use 4
The keyword def signals we're about to create a named definition. Here the name is Triangle.
After that is a declaration of variables, here a as a natural number. The round brackets require anyone using the definition to provide a as a parameter.
The Prop specifies that Triangle a will be a proposition, a statement that can be true or false.
After the := is the actual detail of the definition of a triangle number, ∃ n, 2 * a = n * (n + 1).
The following picture summarises the structure of simple definitions.
When creating our own definitions, it is considerate to provide a minimal example that illustrates how to use the definition.
Here the example is a proof of Triangle 10, a proposition that says $10$ is a triangle number. The dsimp [Triangle] unfolds the definition in the Infoview. Because the definition is a “there exists” statement, the proof is resolved by a simple use 4.
Placing the cursor before dsimp [Triangle] in the illustrative example shows the proof objective.
⊢ Triangle 10
Moving the cursor to the start of the next line shows the goal with the definition of Triangle unfolded.
⊢ ∃ n, 20 = n * (n + 1)
Let's take a first peek at the hierarchy of objects in Lean.
Compare the definition of Triangle with a definition of Triple that I just made up:
def Triangle (a : ℕ) : Prop := ∃ n, 2 * a = n * (n + 1)
def Triple (a : ℕ) : ℕ := 3 * a
The type of Triangle a is Prop, a proposition. The type of Triple a is ℕ, a natural number.
We say the detail ∃ n, 2 * a = n * (n + 1) is a term of type Prop. Similarly, 3 * a is a term of type ℕ.
Appendix A illustrates the hierarchy of objects in Lean and Mathlib. The diagram there shows 13 is a term of type ℕ. What may be surprising is that proofs are terms of type Prop.
Knowing this isn't crucial at this stage of our learning, but it can help us read and write Lean proofs with an additional level of understanding.
Create a definition of square numbers named Square. It should be a proposition which is only true if a given number can be written in the form $n^{2}$, for some natural number $n$.
Write a proof showing 25 is a square number, illustrating the use of Square.
Packaging your own lemmas and theorems into a library is a tidier way of maintaining them, and making them available for others to use.
In your project's lakefile.lean file, add a reference to the Lean file which contains your lemmas.
lean_lib MyLeanLemmas
Replace MyLeanLemmas with the name you want for your own library.
To use the lemmas in the MyLeanLemmas library, we simply use import at the top of our lean program.
import Mathlib.Tactic
import MyLeanLemmas
It is a good habit to import additional libraries after any official Mathlib libraries.