5. Number Theory
In this chapter, we show you how to formalize some elementary results in number theory. As we deal with more substantive mathematical content, the proofs will get longer and more involved, building on the skills you have already mastered.
5.1. Irrational Roots
Let’s start with a fact known to the ancient greeks, namely, that the square root of 2 is irrational. If we suppose otherwise, we can write \(\sqrt{2} = a / b\) as a fraction in lowest terms. Squaring both sides yields \(a^2 = 2 b^2\), which implies that \(a\) is even. If we write \(a = 2c\), then we get \(4c^2 = 2 b^2\) and hence \(b^2 = 2 c^2\). This implies that \(b\) is also even, contradicting the fact that we have assumed that \(a / b\) has been reduced to lowest terms.
Saying that \(a / b\) is a fraction in lowest terms means
that \(a\) and \(b\) do not have any factors in common,
which is to say, they are coprime.
Mathlib defines the predicate nat.coprime m n to be nat.gcd m n = 1.
Using Lean’s anonymous projection notation, if s and t are
expressions of type nat, we can write s.coprime t instead of
nat.coprime s t, and similarly for nat.gcd.
As usual, Lean will often unfold the definition of nat.coprime automatically
when necessary,
but we can also do it manually by rewriting or simplifying with
the identifier nat.coprime.
The norm_num tactic is smart enough to compute concrete values.
#print nat.coprime
example (m n : nat) (h : m.coprime n) : m.gcd n = 1 := h
example (m n : nat) (h : m.coprime n) : m.gcd n = 1 :=
by { rw nat.coprime at h, exact h }
example : nat.coprime 12 7 := by norm_num
example : nat.gcd 12 8 = 4 := by norm_num
We have already encountered the gcd function in
Section 2.4.
There is also a version of gcd for the integers;
we will return to a discussion of the relationship between
different number systems below.
There are even a generic gcd function and generic
notions of prime and is_coprime
that make sense in general classes of algebraic structures.
We will come to understand how Lean manages this generality
in the next chapter.
In the meanwhile, in this section, we will restrict attention
to the natural numbers.
We also need the notion of a prime number, nat.prime.
The theorem nat.prime_def_lt provides one familiar characterization,
and nat.prime.eq_one_or_self_of_dvd provides another.
#check @nat.prime_def_lt
example (p : ℕ) (prime_p : nat.prime p) : 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1 :=
by rwa nat.prime_def_lt at prime_p
#check nat.prime.eq_one_or_self_of_dvd
example (p : ℕ) (prime_p : nat.prime p) : ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p :=
prime_p.eq_one_or_self_of_dvd
example : nat.prime 17 := by norm_num
-- commonly used
example : nat.prime 2 := nat.prime_two
example : nat.prime 3 := nat.prime_three
In the natural numbers, a prime number has the property that it cannot
be written as a product of nontrivial factors.
In a broader mathematical context, an element of a ring that has this property
is said to be irreducible.
An element of a ring is said to be prime if whenever it divides a product,
it divides one of the factors.
It is an important property of the natural numbers
that in that setting the two notions coincide,
giving rise to the theorem nat.prime.dvd_mul.
We can use this fact to establish a key property in the argument
above:
if the square of a number is even, then that number is even as well.
Mathlib defines the predicate even in data.nat.parity,
but for reasons that will become clear below,
we will simply use 2 ∣ m to express that m is even.
#check @nat.prime.dvd_mul
#check nat.prime.dvd_mul nat.prime_two
#check nat.prime_two.dvd_mul
lemma even_of_even_sqr {m : ℕ} (h : 2 ∣ m^2) : 2 ∣ m :=
begin
rw [pow_two, nat.prime_two.dvd_mul] at h,
cases h; assumption
end
example {m : ℕ} (h : 2 ∣ m^2) : 2 ∣ m :=
nat.prime.dvd_of_dvd_pow nat.prime_two h
As we proceed, you will need to become proficient at finding the facts you
need.
Remember that if you can guess the prefix of the name and
you have imported the relevent library,
you can use tab completion (sometimes with ctrl-tab) to find
what you are looking for.
You can use ctrl-click on any identifier to jump to the file
where it is defined, which enables you to browse definitions and theorems
nearby.
You can also use the search engine on the
Lean community web pages,
and if all else fails,
don’t hesitate to ask on
Zulip.
example (a b c : nat) (h : a * b = a * c) (h' : a ≠ 0) :
b = c :=
begin
-- library_search suggests the following:
exact (mul_right_inj' h').mp h
end
The heart of our proof of the irrationality of the square root of two
is contained in the following theorem.
See if you can fill out the proof sketch, using
even_of_even_sqr and the theorem nat.dvd_gcd.
example {m n : ℕ} (coprime_mn : m.coprime n) : m^2 ≠ 2 * n^2 :=
begin
intro sqr_eq,
have : 2 ∣ m,
sorry,
obtain ⟨k, meq⟩ := dvd_iff_exists_eq_mul_left.mp this,
have : 2 * (2 * k^2) = 2 * n^2,
{ rw [←sqr_eq, meq], ring },
have : 2 * k^2 = n^2,
sorry,
have : 2 ∣ n,
sorry,
have : 2 ∣ m.gcd n,
sorry,
have : 2 ∣ 1,
sorry,
norm_num at this
end
In fact, with very few changes, we can replace 2 by an arbitrary prime.
Give it a try in the next example.
At the end of the proof, you’ll need to derive a contradiction from
p ∣ 1.
You can use nat.prime.two_le, which says that
any prime number is greater than or equal to two,
and nat.le_of_dvd.
example {m n p : ℕ} (coprime_mn : m.coprime n) (prime_p : p.prime) : m^2 ≠ p * n^2 :=
sorry
Let us consider another approach. Here is a quick proof that if \(p\) is prime, then \(m^2 \ne p n^2\): if we assume \(m^2 = p n^2\) and consider the factorization of \(m\) and \(n\) into primes, then \(p\) occurs an even number of times on the left side of the equation and an odd number of times on the right, a contradiction. Note that this argument requires that \(n\) and hence \(m\) are not equal to zero. The formalization below confirms that this assumption is sufficient.
The unique factorization theorem says that any natural number other
than zero can be written as the product of primes in a unique way.
Mathlib contains a formal version of this, expressed in terms of a function
nat.factors, which returns the list of
prime factors of a number in nondecreasing order.
The library proves that all the elements of nat.factors n
are prime, that any n greater than zero is equal to the
product of its factors,
and that if n is equal to the product of another list of prime numbers,
then that list is a permutation of nat.factors n.
#check nat.factors
#check nat.prime_of_mem_factors
#check nat.prod_factors
#check nat.factors_unique
You can browse these theorems and others nearby, even though we have not
talked about list membership, products, or permutations yet.
We won’t need any of that for the task at hand.
We will instead use the fact that Mathlib has a function list.count
that counts the number of times an element occurs in a list.
Counting the number of times that a prime p occurs in n.factors
yields the multiplicity of p in the prime factorization of n,
and the library contains some key identities.
#check @nat.count_factors_mul_of_pos
#check @nat.factors_count_pow
#check @nat.factors_prime
example (m n p : ℕ) (mpos : 0 < m) (npos : 0 < n) :
(m * n).factors.count p = m.factors.count p + n.factors.count p :=
nat.count_factors_mul_of_pos mpos npos
example (n k p : ℕ) : (n^k).factors.count p = k * n.factors.count p :=
nat.factors_count_pow
example (p : ℕ) (prime_p : p.prime) : p.factors.count p = 1 :=
begin
rw nat.factors_prime prime_p,
simp
end
Notice that in the third example, we use the simplifier to close the goal
list.count p [p] = 1. This is the sort of thing that the simplifier
is good for.
In fact, the equation list.count_singleton would do the trick.
If you replace simp by squeeze_simp,
the information window will show you that the simplifier has found a more
roundabout way of discharging the goal.
The next example shows that the simplifier is also smart enough to replace
n^2 ≠ 0 by n ≠ 0. The tactic simpa just calls simp
followed by assumption.
See if you can use the identities above to fill in the missing parts of the proof.
example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.prime) : m^2 ≠ p * n^2 :=
begin
intro sqr_eq,
have nsqr_nez : n^2 ≠ 0,
by simpa,
have eq1 : (m^2).factors.count p = 2 * m.factors.count p,
sorry,
have eq2 : (p * n^2).factors.count p = 2 * n.factors.count p + 1,
sorry,
have : (2 * m.factors.count p) % 2 = (2 * n.factors.count p + 1) % 2,
{ rw [←eq1, sqr_eq, eq2] },
rw [add_comm, nat.add_mul_mod_self_left, nat.mul_mod_right] at this,
norm_num at this
end
A nice thing about this proof is that it also generalizes. There is
nothing special about 2; with small changes, the proof shows that
whenever we write m^k = r * n^k, the multiplicity of any prime p
in r has to be a multiple of k.
To use nat.count_factors_mul_of_pos with r * n^k,
we need to know that r is positive.
But when r is zero, the theorem below is trivial, and easily
proved by the simplifier.
So the proof is carried out in cases.
The line cases r with r replaces the goal with two versions:
one in which r is replaced by 0,
and the other in which r is replaces by r.succ,
the successor of r.
In the second case, we can use the theorem r.succ_pos, which
establishes 0 < r.succ.
Notice also that the line that begins have : npow_nz provides a
short proof-term proof of n^k ≠ 0.
To understand how it works, try replacing it with a tactic proof,
and then think about how the tactics describe the proof term.
See if you can fill in the missing parts of the proof below.
At the very end, you can use nat.dvd_sub' and nat.dvd_mul_right
to finish it off.
example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m^k = r * n^k) :
∀ p : ℕ, p.prime → k ∣ r.factors.count p :=
begin
intros p prime_p,
cases r with r,
{ simp },
have npow_nz : n^k ≠ 0 := λ npowz, nnz (pow_eq_zero npowz),
have eq1 : (m^k).factors.count p = k * m.factors.count p,
sorry,
have eq2 : (r.succ * n^k).factors.count p =
k * n.factors.count p + r.succ.factors.count p,
sorry,
have : r.succ.factors.count p = k * m.factors.count p - k * n.factors.count p,
{ rw [←eq1, pow_eq, eq2, add_comm, nat.add_sub_cancel] },
rw this,
sorry
end
There are a number of ways in which we might want to improve on these results. To start with, a proof that the square root of two is irrational should say something about the square root of two, which can be understood as an element of the real or complex numbers. And stating that it is irrational should say something about the rational numbers, namely, that no rational number is equal to it. Moreover, we should extend the theorems in this section to the integers. Although it is mathematically obvious that if we could write the square root of two as a quotient of two integers then we could write it as a quotient of two natural numbers, proving this formally requires some effort.
In Mathlib, the natural numbers, the integers, the rationals, the reals, and the complex numbers are represented by separate data types. Restricting attention to the separate domains is often helpful: we will see that it is easy to do induction on the natural numbers, and it is easiest to reason about divisibility of integers when the real numbers are not part of the picture. But having to mediate between the different domains is a headache, one we will have to contend with. We will return to this issue later in this chapter.
We should also expect to be able to strengthen the conclusion of the
last theorem to say that the number r is a k-th power,
since its k-th root is just the product of each prime dividing r
raised to its multiplicity in r divided by k.
To be able to do that we will need better means for reasoning about
products and sums over a finite set,
which is also a topic we will return to.
In fact, the results in this section are all established in much
greater generality in mathlib,
in data.real.irrational.
The notion of multiplicity is defined for an
arbitrary commutative monoid,
and that it takes values in the extended natural numbers enat,
which adds the value infinity to the natural numbers.
In the next chapter, we will begin to develop the means to
appreciate the way that Lean supports this sort of generality.
5.2. Induction and Recursion
The set of natural numbers \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\) is not only fundamentally important in its own right, but also a plays a central role in the construction of new mathematical objects. Lean’s foundation allows us to declare inductive types, which are types generated inductively by a given list of constructors. In Lean, the natural numbers are declared as follows.
inductive nat
| zero : nat
| succ (n : nat) : nat
You can find this in the library by writting #check nat and
then using ctrl-click on the identifier nat.
The command specifies that nat is the datatype generated
freely and inductively by the two constructors zero : nat and
succ : nat → nat.
Of course, the library introduces notation ℕ and 0 for
nat and zero respectively. (Numerals are translated to binary
representations, but we don’t have to worry about the details of that now.)
What “freely” means for the working mathematician is that the type
nat has an element zero and an injective successor function
succ whose image does not include zero.
example (n : nat) : n.succ ≠ nat.zero := nat.succ_ne_zero n
example (m n : nat) (h : m.succ = n.succ) : m = n := nat.succ.inj h
What the word “inductively” means for the working mathematician is that the natural numbers comes with a principle of proof by induction and a principle of definition by recursion. This section will show you how to use these.
Here is an example of a recursive definition of the factorial function.
def fac : ℕ → ℕ
| 0 := 1
| (n + 1) := (n + 1) * fac n
The syntax takes some getting used to.
Notice that there is no := on the first line.
The next two lines provide the base case and inductive step
for a recursive definition.
These equations hold definitionally, but they can also
be used manually by giving the name fac to simp or rw.
example : fac 0 = 1 := rfl
example : fac 0 = 1 := by rw fac
example : fac 0 = 1 := by simp [fac]
example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := rfl
example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by rw fac
example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by simp [fac]
The factorial function is actually already defined in mathlib as
nat.factorial. Once again, you can jump to it by typing
#check nat.factorial and using ctrl-click.
For illustrative purposes, we will continue using fac in the examples.
The annotation @[simp] before the definition
of nat.factorial specifies that
the defining equation should be added to the database of identities
that the simplifier uses by default.
The principle of induction says that we can prove a general statement
about the natural numbers by proving that the statement holds of 0
and that whenever it holds of a natural number \(n\),
it also holds of \(n + 1\).
The line induction n with n ih in the proof
below therefore results in two goals:
in the first we need to prove 0 < fac 0,
and in the second we have the added assumption ih : 0 < fac n
and a required to prove 0 < fac (n + 1).
The phrase with n ih serves to name the variable and
the assumption for the inductive hypothesis,
and you can choose whatever names you want for them.
theorem fac_pos (n : ℕ) : 0 < fac n :=
begin
induction n with n ih,
{ rw fac, exact zero_lt_one },
rw fac,
exact mul_pos n.succ_pos ih,
end
The induction tactic is smart enough to include hypotheses
that depend on the induction variable as part of the
induction hypothesis.
Step through the next example to see what is going on.
theorem dvd_fac {i n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n :=
begin
induction n with n ih,
{ exact absurd ipos (not_lt_of_ge ile) },
rw fac,
cases nat.of_le_succ ile with h h,
{ apply dvd_mul_of_dvd_right (ih h) },
rw h,
apply dvd_mul_right
end
The following example provides a crude lower bound for the factorial function. It turns out to be easier to start with a proof by cases, so that the remainder of the proof starts with the case \(n = 1\). See if you can complete the argument with a proof by induction.
theorem pow_two_le_fac (n : ℕ) : 2^(n-1) ≤ fac n :=
begin
cases n with n,
{ simp [fac] },
sorry
end
Induction is often used to prove identities involving finite sums and
products.
Mathlib defines the expressions finset.sum s f where
s : finset α if a finite set of elements of the type α and
f is a function defined on α.
The codomain of f can be any type that supports a commutative,
associative addition operation with a zero element.
If you import algebra.big_operators and issue the command
open_locale big_operators, you can use the more suggestive notation
∑ x in s, f x. Of course, there is are an analogous operation and
notation for finite products.
We will talk about the finset type and the operations
it supports in the next section, and again in a later chapter.
For now, we will only make use
of finset.range n, which is the finite set of natural numbers
less than n.
variables {α : Type*} (s : finset ℕ) (f : ℕ → ℕ) (n : ℕ)
#check finset.sum s f
#check finset.prod s f
open_locale big_operators
open finset
example : s.sum f = ∑ x in s, f x := rfl
example : s.prod f = ∏ x in s, f x := rfl
example : (range n).sum f = ∑ x in range n, f x := rfl
example : (range n).prod f = ∏ x in range n, f x := rfl
The facts finset.sum_range_zero and finset.sum_range_succ
provide a recursive description summation up to \(n\),
and similarly for products.
example (f : ℕ → ℕ) : ∑ x in range 0, f x = 0 :=
finset.sum_range_zero f
example (f : ℕ → ℕ) (n : ℕ): ∑ x in range n.succ, f x = (∑ x in range n, f x) + f n :=
finset.sum_range_succ f n
example (f : ℕ → ℕ) : ∏ x in range 0, f x = 1 :=
finset.prod_range_zero f
example (f : ℕ → ℕ) (n : ℕ): ∏ x in range n.succ, f x = (∏ x in range n, f x) * f n :=
finset.prod_range_succ f n
The first identity in each pair holds definitionally, which is to say,
you can replace the proofs by rfl.
The following expresses the factorial function that we defined as a product.
example (n : ℕ) : fac n = ∏ i in range n, (i + 1) :=
begin
induction n with n ih,
{ simp [fac] },
simp [fac, ih, prod_range_succ, mul_comm]
end
The fact that we include mul_comm as a simplification rule deserves
comment.
It should seem dangerous to simplify with the identity x * y = y * x,
which would ordinarily loop indefinitely.
Lean’s simplifier is smart enough to recognize that, and applies the rule
only in the case where the resulting term has a smaller value in some
fixed but arbitrary ordering of the terms.
The following example shows that simplifying using the three rules
mul_assoc, mul_comm, and mul_left_comm
manages to identify products that are the same up to the
placement of parentheses and ordering of variables.
example (a b c d e f : ℕ) : a * ((b * c) * f * (d * e)) = d * (a * f * e) * (c * b) :=
by simp [mul_assoc, mul_comm, mul_left_comm]
Roughly, the rules work by pushing parentheses to the right and then re-ordering the expressions on both sides until they both follow the same canonical order. Simplifying with these rules, and the corresponding rules for addition, is a handy trick.
Returning to summation identities, we suggest stepping through the following proof that the sum of the natual numbers up to an including \(n\) is \(n (n + 1) / 2\). The first step of the proof clears the denominator. This is generally useful when formalizing identities, because calculations with division generally have side conditions. (It is similarly useful to avoid using subtraction on the natural numbers when possible.)
theorem sum_id (n : ℕ) : ∑ i in range (n + 1), i = n * (n + 1) / 2 :=
begin
symmetry, apply nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2),
induction n with n ih,
{ simp },
rw [finset.sum_range_succ, mul_add 2, ←ih, nat.succ_eq_add_one],
ring
end
We encourage you to prove the analogous identity for sums of squares, and other identities you can find on the web.
theorem sum_sqr (n : ℕ) : ∑ i in range (n + 1), i^2 = n * (n + 1) * (2 *n + 1) / 6 :=
sorry
In Lean’s core library, addition and multiplication are themselves defined
using recursive definitions,
and their fundamental properties are established using induction.
If you like thinking about foundational topics like that,
you might enjoy working through proofs
of the commutativity and associativity of multiplication and addition
and the distributivity of multiplication over addition.
You can do this on a copy of the natural numbers
following the outline below.
Notice that we can use the induction tactic with my_nat;
Lean is smart enough to know to
use the relevant induction principle (which is, of course,
the same as that for nat).
We start you off with the commutativity of addition. A good rule of thumb is that because addition and multiplication are defined by recursion on the second argument, it is generally advantageous to do proofs by induction on a variable that occurs in that position. It is a bit tricky to decide which variable to use in the proof of associativity.
It can be confusing to write things without the usual notation
for zero, one, addition, and multiplication.
We will learn how to define such notation later.
Working in the namespace my_nat means that we can write
zero and succ rather than my_nat.zero and my_nat.succ,
and that these interpretations of the names take precedence over
others.
Outside the namespace, the full name of the add defined below,
for example, is my_nat.add.
If you find that you really enjoy this sort of thing, try defining
truncated subtraction and exponentiation and proving some of their
properties as well.
Remember that truncated subtraction cuts off at zero.
To define that, it is useful to define a predecessor function, pred,
that subtracts one from any nonzero number and fixes zero.
The function pred can be defined by a simple instance of recursion.
inductive my_nat
| zero : my_nat
| succ : my_nat → my_nat
namespace my_nat
def add : my_nat → my_nat → my_nat
| x zero := x
| x (succ y) := succ (add x y)
def mul : my_nat → my_nat → my_nat
| x zero := zero
| x (succ y) := add (mul x y) x
theorem zero_add (n : my_nat) : add zero n = n :=
begin
induction n with n ih,
{ refl },
rw [add, ih]
end
theorem succ_add (m n : my_nat) : add (succ m) n = succ (add m n) :=
begin
induction n with n ih,
{ refl },
rw [add, ih],
refl
end
theorem add_comm (m n : my_nat) : add m n = add n m :=
begin
induction n with n ih,
{ rw zero_add, refl },
rw [add, succ_add, ih]
end
theorem add_assoc (m n k : my_nat) : add (add m n) k = add m (add n k) :=
sorry
theorem mul_add (m n k : my_nat) : mul m (add n k) = add (mul m n) (mul m k) :=
sorry
theorem zero_mul (n : my_nat) : mul zero n = zero :=
sorry
theorem succ_mul (m n : my_nat) : mul (succ m) n = add (mul m n) n :=
sorry
theorem mul_comm (m n : my_nat) : mul m n = mul n m :=
sorry
end my_nat
5.3. Infinitely Many Primes
Let us continue our exploration of induction and recursion with another mathematical standard: a proof that there are infinitely many primes. One way to formulate this is as the statement that for every natural number \(n\), there is a prime number greater than \(n\). To prove this, let \(p\) be any prime factor of \(n! + 1\). If \(p\) is less than \(n\), it divides \(n!\). Since it also divides \(n! + 1\), it divides 1, a contradiction. Hence \(p\) is greater than \(n\).
To formalize that proof, we need to show that any number greater than or equal to 2 has a prime factor. To do that, we will need to show that any natural number that is not equal to 0 or 1 is greater-than or equal to 2. And this brings us to a quirky feature of formalization: it is often trivial statements like this that are among the most annoying to formalize. Here we consider a few ways to do it.
To start with, we can use the cases tactic and the fact that the
successor function respects the ordering on the natural numbers.
theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m :=
begin
cases m, contradiction,
cases m, contradiction,
repeat { apply nat.succ_le_succ },
apply zero_le
end
Another strategy is to use the tactic interval_cases,
which automatically splits the goal into cases when
the variable in question is contained in an interval
of natural numbers or integers.
Remember that you can hover over it to see its documentation.
example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m :=
begin
by_contradiction h,
push_neg at h,
interval_cases m; contradiction
end
Recall that the semicolon after interval_cases m means
that the next tactic is applied to each of the cases that it generates.
Yet another option is to use the tactic, dec_trivial, which tries
to find a decision procedure to solve the problem.
Lean knows that you can decide the truth value of a statement that
begins with a bounded quantifier ∀ x, x < n → ... or ∃ x, x < n ∧ ...
by deciding each of the finitely many instances.
example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m :=
begin
by_contradiction h,
push_neg at h,
revert m h h0 h1,
dec_trivial
end
In fact, the variant dec_trivial! will revert all the hypotheses
that contain a variable that is found in the target.
example {m : ℕ} (h : m < 2) : m = 0 ∨ m = 1 :=
by dec_trivial!
Finally, in this case we can use the omega tactic, which is designed
to reason about linear expressions in the natural numbers.
example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m :=
by omega
With the theorem two_le in hand, let’s start by showing that every
natural number greater than two has a prime divisor.
Mathlib contains a function nat.min_fac that
returns the smallest prime divisor,
but for the sake of learning new parts of the library,
we’ll avoid using it and prove the theorem directly.
Here, ordinary induction isn’t enough.
We want to use strong induction, which allows us to prove
that every natural number \(n\) has a property \(P\)
by showing that for every number \(n\), if \(P\) holds
of all values less than \(n\), it holds at \(n\) as well.
In Lean, this principle is called nat.strong_induction_on,
and we can use the with keyword to tell the induction tactic
to use it.
Notice that when we do that, there is no base case; it is subsumed
by the general induction step.
The argument is simply as follows. Assuming \(n ≥ 2\),
if \(n\) is prime, we’re done. If it isn’t,
then by one of the characterizations of what it means to be a prime number,
it has a nontrivial factor, \(m\),
and we can apply the inductive hypothesis to that.
Step through the next proof to see how that plays out.
The line dsimp at ih simplifies the expression of the
inductive hypothesis to make it more readable.
The proof still works if you delete that line.
theorem exists_prime_factor {n : nat} (h : 2 ≤ n) :
∃ p : nat, p.prime ∧ p ∣ n :=
begin
by_cases np : n.prime,
{ use [n, np, dvd_rfl] },
induction n using nat.strong_induction_on with n ih,
dsimp at ih,
rw nat.prime_def_lt at np,
push_neg at np,
rcases np h with ⟨m, mltn, mdvdn, mne1⟩,
have : m ≠ 0,
{ intro mz,
rw [mz, zero_dvd_iff] at mdvdn,
linarith },
have mgt2 : 2 ≤ m := two_le this mne1,
by_cases mp : m.prime,
{ use [m, mp, mdvdn] },
rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩,
use [p, pp, pdvd.trans mdvdn]
end
We can now prove the following formulation of our theorem.
See if you can fill out the sketch.
You can use nat.factorial_pos, nat.dvd_factorial,
and nat.dvd_sub.
theorem primes_infinite : ∀ n, ∃ p > n, nat.prime p :=
begin
intro n,
have : 2 ≤ nat.factorial (n + 1) + 1,
sorry,
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩,
refine ⟨p, _, pp⟩,
show p > n,
by_contradiction ple, push_neg at ple,
have : p ∣ nat.factorial (n + 1),
sorry,
have : p ∣ 1,
sorry,
show false,
sorry
end
Let’s consider a variation of the proof above, where instead of using the factorial function, we suppose that we are given by a finite set \(\{ p_1, \ldots, p_n \}\) and we consider a prime factor of \(\prod_{i = 1}^n p_i + 1\). That prime factor has to be distinct from each \(p_i\), showing that there is no finite set that contains all the prime numbers.
Formalizing this argument requires us to reason about finite
sets. In Lean, for any type α, the type finset α
represents finite sets of elements of type α.
Reasoning about finite sets computationally requires having
a procedure to test equality on α, which is why the snippet
below includes the assumption [decidable_eq α].
For concrete data types like ℕ, ℤ, and ℚ,
the assumption is satisfied automatically. When reasoning about
the real numbers, it can be satisfied using classical logic
and abandoning the computational interpretation.
We use the command open finset to avail ourselves of shorter names
for the relevant theorems. Unlike the case with sets,
most equivalences involving finsets do not hold definitionally,
so they need to be expanded manually using equivalances like
finset.subset_iff, finset.mem_union, finset.mem_inter,
and finset.mem_sdiff. The ext tactic can still be used
to reduce show that two finite sets are equal by showing
that every element of one is an element of the other.
open finset
section
variables {α : Type*} [decidable_eq α] (r s t : finset α)
example : r ∩ (s ∪ t) ⊆ (r ∩ s) ∪ (r ∩ t) :=
begin
rw subset_iff,
intro x,
rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter],
tauto
end
example : r ∩ (s ∪ t) ⊆ (r ∩ s) ∪ (r ∩ t) :=
by { simp [subset_iff], intro x, tauto }
example : (r ∩ s) ∪ (r ∩ t) ⊆ r ∩ (s ∪ t) :=
by { simp [subset_iff], intro x, tauto }
example : (r ∩ s) ∪ (r ∩ t) = r ∩ (s ∪ t) :=
by { ext x, simp, tauto }
end
We have used a new trick: the tauto tactic (and a strengthened
version, tauto!, which uses classical logic) can be used to
dispense with propositional tautologies. See if you can use
these methods to prove the two examples below.
example : (r ∪ s) ∩ (r ∪ t) = r ∪ (s ∩ t) :=
sorry
example : (r \ s \ t) = r \ (s ∪ t) :=
sorry
The theorem finset.dvd_prod_of_mem tells us that if an
n is an element of a finite set s, then n divides
∏ i in s, i.
example (s : finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ (∏ i in s, i) :=
finset.dvd_prod_of_mem _ h
We also need to know that the converse holds in the case where
n is prime and s is a set of primes.
To show that, we need the following lemma, which you should
be able to prove using the theorem nat.prime.eq_one_or_self_of_dvd.
theorem nat.prime.eq_of_dvd_of_prime {p q : ℕ}
(prime_p : nat.prime p) (prime_q : nat.prime q) (h : p ∣ q) :
p = q :=
sorry
We can use this lemma to show that if a prime p divides a product of a finite
set of primes, then it divides one of them.
Mathlib provides a useful principle of induction on finite sets:
to show that a property holds of an arbitrary finite set s,
show that it holds of the empty set, and show that it is preserved
when we add a single new element a ∉ s.
The principle is known as finset.induction_on.
When we tell the induction tactic to use it, we can also specify the names
a and s, the name for the assumption a ∉ s in the inductive step,
and the name of the inductive hypothesis.
The expression finset.insert a s denotes the union of s with the singleton a.
The identities finset.prod_empty and finset.prod_insert then provide
the relevant rewrite rules for the product.
In the proof below, the first simp applies finset.prod_empty.
Step through the beginning of the proof to see the induction unfold,
and then finish it off.
theorem mem_of_dvd_prod_primes {s : finset ℕ} {p : ℕ} (prime_p : p.prime) :
(∀ n ∈ s, nat.prime n) → (p ∣ ∏ n in s, n) → p ∈ s :=
begin
intros h₀ h₁,
induction s using finset.induction_on with a s ans ih,
{ simp at h₁,
linarith [prime_p.two_le] },
simp [finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁,
rw mem_insert,
sorry
end
We need one last property of finite sets.
Given an element s : set α and a predicate
P on α, in Chapter 4
we wrote { x ∈ s | P x } for the set of
elements of s that satisfy P.
Given s : finset α,
the analogous notion is written s.filter P.
example (s : finset ℕ) (x : ℕ) : x ∈ s.filter nat.prime ↔ x ∈ s ∧ x.prime :=
mem_filter
We now prove an alternative formulation of the statement that there are infinitely many
primes, namely, that given any s : finset ℕ, there is a prime p that is not
an element of s.
Aiming for a contradiction, we assume that all the primes are in s, and then
cut down to a set s' that contains all and only the primes.
Taking the product of that set, adding one, and finding a prime factor
of the result
leads to the contradiction we are looking for.
See if you can complete the sketch below.
You can use finset.prod_pos in the proof of the first have.
theorem primes_infinite' : ∀ (s : finset nat), ∃ p, nat.prime p ∧ p ∉ s :=
begin
intro s,
by_contradiction h,
push_neg at h,
set s' := s.filter nat.prime with s'_def,
have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.prime,
{ intro n,
simp [s'_def],
apply h },
have : 2 ≤ (∏ i in s', i) + 1,
sorry,
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩,
have : p ∣ (∏ i in s', i),
sorry,
have : p ∣ 1,
{ convert nat.dvd_sub' pdvd this, simp },
show false,
sorry
end
We have thus seen two ways of saying that there are infinitely many primes:
saying that they are not bounded by any n, and saying that they are
not contained in any finite set s.
The two proofs below show that these formulations are equivalent.
In the second, in order to form s.filter Q, we have to assume that there
is a procedure for deciding whether or not Q holds. Lean knows that there
is a procedure for nat.prime. In general, if we use classical logic
by writing open_locale classical,
we can dispense with the assumption.
In mathlib, finset.sup s f denotes the supremum of the values of f x as x
ranges over s, returning 0 in the case where s is empty and
the codomain of f is ℕ. In the first proof, we use s.sup id,
where id is the identity function, to refer to the maximum value in s.
theorem bounded_of_ex_finset (Q : ℕ → Prop):
(∃ s : finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n :=
begin
rintros ⟨s, hs⟩,
use s.sup id + 1,
intros k Qk,
apply nat.lt_succ_of_le,
show id k ≤ s.sup id,
apply le_sup (hs k Qk)
end
theorem ex_finset_of_bounded (Q : ℕ → Prop) [decidable_pred Q] :
(∃ n, ∀ k, Q k → k ≤ n) → (∃ s : finset ℕ, ∀ k, Q k ↔ k ∈ s) :=
begin
rintros ⟨n, hn⟩,
use (range (n + 1)).filter Q,
intro k,
simp [nat.lt_succ_iff],
exact hn k
end
A small variation on our second proof that there are infinitely many primes shows that there are infinitely many primes congruent to 3 modulo 4. The argument goes as follows. First, notice that if the product of two numbers \(m\) and \(n\) is equal to 3 modulo 4, then one of the two numbers is congruent to three modulo 4. After all, both have to be odd, and if they are both congruent to 1 modulo 4, so is their product. We can use this observation to show that if some number greater than 2 is congruent to 3 modulo 4, then that number has a prime divisor that is also congruent to 3 modulo 4.
Now suppose there are only finitely many prime numbers congruent to 3 modulo 4, say, \(p_1, \ldots, p_k\). Without loss of generality, we can assume that \(p_1 = 3\). Consider the product \(4 \prod_{i = 2}^k p_i + 3\). It is easy to see that this is congruent to 3 modulo 4, so it has a prime factor \(p\) congruent to 3 modulo 4. It can’t be the case that \(p = 3\); since \(p\) divides \(4 \prod_{i = 2}^k p_i + 3\), if \(p\) were equal to 3 then it would also divide \(\prod_{i = 2}^k p_i\), which implies that \(p\) is equal to one of the \(p_i\) for \(i = 2, \ldots, k\); and we have excluded 3 from this list. So \(p\) has to be one of the other elements \(p_i\). But in that case, \(p\) divides \(4 \prod_{i = 2}^k p_i\) and hence 3, which contradicts the fact that it is not 3.
In Lean, the notation n % m, read “n modulo m,”
denotes the remainder of the division of n by m.
example : 27 % 4 = 3 := by norm_num
We can then render the statment “n is congruent to 3 modulo 4”
as n % 4 = 3. The following example and theorems sum up
the facts about this function that we will need to use below.
The first named theorem is another illustration of reasoning by
a small number of cases.
In the second named theorem, remember that the semicolon means that
the subsequent tactic block is applied to both of the goals
that result from the application of two_le.
example (n : ℕ) : (4 * n + 3) % 4 = 3 :=
by { rw [add_comm, nat.add_mul_mod_self_left], norm_num }
theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) :
m % 4 = 3 ∨ n % 4 = 3 :=
begin
revert h,
rw [nat.mul_mod],
have : m % 4 < 4 := nat.mod_lt m (by norm_num),
interval_cases m % 4 with hm; simp [hm],
have : n % 4 < 4 := nat.mod_lt n (by norm_num),
interval_cases n % 4 with hn; simp [hn]; norm_num
end
theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n :=
by apply two_le; { intro neq, rw neq at h, norm_num at h }
We will also need the following fact, which says that if
m is a nontrivial divisor of n, then so is m / n.
See if you can complete the proof using nat.div_dvd_of_dvd
and nat.div_lt_self.
theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) :
(n / m) ∣ n ∧ n / m < n :=
sorry
Now put all the pieces together to prove that any number congruent to 3 modulo 4 has a prime divisor with that same property.
theorem exists_prime_factor_mod_4_eq_3 {n : nat} (h : n % 4 = 3) :
∃ p : nat, p.prime ∧ p ∣ n ∧ p % 4 = 3 :=
begin
by_cases np : n.prime,
{ use [n, np, dvd_rfl, h] },
induction n using nat.strong_induction_on with n ih,
dsimp at ih,
rw nat.prime_def_lt at np,
push_neg at np,
rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩,
have mge2 : 2 ≤ m,
{ apply two_le _ mne1,
intro mz,
rw [mz, zero_dvd_iff] at mdvdn, linarith },
have neq : m * (n / m) = n := nat.mul_div_cancel' mdvdn,
have : m % 4 = 3 ∨ (n / m) % 4 = 3,
{ apply mod_4_eq_3_or_mod_4_eq_3, rw [neq, h] },
cases this with h1 h1,
{ sorry },
sorry
end
We are in the home stretch. Given a set s of prime
numbers, we need to talk about the result of removing 3 from that
set, if it is present. The function finset.erase handles that.
example (m n : ℕ) (s : finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s :=
by rwa mem_erase at h
example (m n : ℕ) (s : finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s :=
by { simp at h, assumption }
We are now ready to prove that there are infinitely many primes
congruent to 3 modulo 4.
Fill in the missing parts below.
Our solution uses nat.dvd_add_iff_left and nat.dvd_sub'
along the way.
theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, nat.prime p ∧ p % 4 = 3 :=
begin
by_contradiction h,
push_neg at h,
cases h with n hn,
have : ∃ s : finset nat, ∀ p : ℕ, p.prime ∧ p % 4 = 3 ↔ p ∈ s,
{ apply ex_finset_of_bounded,
use n,
contrapose! hn,
rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩,
exact ⟨p, pltn, pp, p4⟩ },
cases this with s hs,
have h₀ : 2 ≤ 4 * (∏ i in erase s 3, i) + 3,
sorry,
have h₁ : (4 * (∏ i in erase s 3, i) + 3) % 4 = 3,
sorry,
rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩,
have ps : p ∈ s,
sorry,
have pne3 : p ≠ 3,
sorry,
have : p ∣ 4 * (∏ i in erase s 3, i),
sorry,
have : p ∣ 3,
sorry,
have : p = 3,
sorry,
contradiction
end
If you managed to complete the proof, congratulations! This has been a serious feat of formalization.