Note: To follow along with this post create a new Lean file and write the following at the top of your Lean file. If you do not have a copy of Lean installed you can follow along here (but it will run slower).
import data.nat.basic
import data.nat.prime
import tactic
In this post we will consider the type of natural numbers \(\mathbb{N} = \{0,1,2,3,…\}\). We would like to examine the structure of its elements, and so naturally we must develop a notion of divisibility. We do this by defining the following relation among the elements of \(\mathbb{N}\).
Definition 1: Divisibility
Given \(a \, b : \mathbb{N}\), we say that “a divides b” (or “a is a divisor of b”) if \( \exists \, c : \mathbb{N}\) such that \(b=a*c\).
Notation: \(*\) denotes multiplication, ‘a divides b’ is written as \(a \mid b\), and is typed “a \mid b” in Lean.
Let us now prove that 1 divides every natural number.
Theorem 1: If \(n : \mathbb{N}\) then \(1 \mid n\)
Proof: Suppose that \(n : \mathbb{N}\). Using definition 1 we see that \(1 \mid n\) means that \(\exists c : \mathbb{N}\) such that \(n=1\times c\). So it suffices to exhibit a natural number c for which \(n=1 * c\) holds, the obvious choice is \(c = n = 1 * n\).
QED
theorem one_dvd_n (n : ℕ) : 1 ∣ n :=
begin
use n,
--exhibiting our choice for c
rw one_mul,
-- telling lean that 1 * n = n
end
Tip: Copy and paste the code into your Lean file and click at the end of each line to watch how the tactic state evolves.
As you can see in the above Lean proof we use the command “use” to exhibit our choice of natural number to resolve the existential quantifier \(\exists \). To complete the proof we have to remind Lean that we can rewrite \(1*n = n \).
Exercise 1: Prove that every natural number divides itself (i.e. if \(n : \mathbb{N}\) then \(n \mid n\)).
I mentioned earlier that we aim to examine the structure of the natural numbers, one interesting question we can ask is how many divisors (including 1 and itself) a number has. Inspect the following table (note that we have omitted 0 and 1):
Natural Number | Number of Divisors |
2 | 2 |
3 | 2 |
4 | 3 |
5 | 2 |
6 | 4 |
7 | 2 |
8 | 4 |
9 | 3 |
10 | 4 |
11 | 2 |
12 | 6 |
13 | 2 |
14 | 4 |
Notice how the number of divisors randomly dip to a minimum of 2 every now and then, this uncertain pattern continues infinitely. The numbers with only 2 divisors are precisely those with 1 and themselves as their only divisors, namely the primes. Understanding the behaviour of the primes has troubled mathematicians since Euclid in Ancient Greece.
Definition 2: Prime
A natural number p is prime if \(2 \leq p\) and \(\forall d \mid p\) we have \(d = 1\) or \(d = p\).
Let’s see this in Lean:
def prime (p : ℕ) := 2 ≤ p ∧ ∀ d ∣ p, d = 1 ∨ d = p
So now when we write “prime p” in Lean we are saying “p is a prime number”.
Let’s prove that a prime cannot be zero, this may seem trivial but it isn’t to Lean.
Theorem 2: If \(n : \mathbb{N}\) and \(h_{1} : \textrm{n is prime}\) then \(n \neq 0 \).
Proof: Let us suppose that \(n = 0\) and derive a contradiction (or false). By \(h_{1}\) we know n is prime, by the definition of prime we have the following two hypotheses \(h_{3} : 2 \leq n\) and \(h_{4} : \forall d \mid n \quad\textrm{we have}\quad d = 1 \quad \textrm{or} \quad d = n\). Now rewriting (or substituting) \(h_{1} : n = 0\) into \(h_{3} : 2 \leq n\) we yield \(h_{3} : 2 \leq 0\) which is a contradiction as required.
QED
lemma prime_ne_zero (n : ℕ) (h₁ : prime n) : n ≠ 0 :=
begin
intro h₂,
-- In Lean n ≠ 0 is defined as n = 0 → false and so we use implication introduction
rw prime at h₁,
--unpacking the definition of prime
cases h₁ with h₃ h₄,
-- splitting the conjunction in the definition of prime
rw h₂ at h₃,
-- substituting n = 0 into the inequality
linarith,
-- the linarith tactic solves goals involving linear inequalities
end
The line “rw prime at h₁,” is not necessary for this proof, however it does make it easier to make sense of the evolving tactic state. Comment the line out by typing “- -” in front of it and see that Lean still accepts the proof.
Exercise 2: Prove that a prime cannot be 1 in Lean.