5. Elementary 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

5.2. Induction and Recursion

5.2.1. Factorial

Recursive definition of the factorial function.

def fac : ℕ → ℕ  -- no := here
  | 0 => 1
  | n + 1 => (n + 1) * fac n

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]

5.2.2. Prove Induction using induction' n with n ih

Prove a general statement by proving that the statement holds of 0; and if it holds at \(n\), it also holds of \(n + 1\).

induction' n with n ih leads to two goals: 1) 0 < fac 0, 2) assuming ih : 0 < fac n, prove 0 < fac (n + 1).

theorem fac_pos (n : ℕ) : 0 < fac n := by
  -- n defines the fac;
  -- ``with n' ih`` names the variable and the assumption for the inductive hypothesis
  induction' n with n' ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n'.succ_pos ih

The induction' tactic can include hypotheses (ile in the example below) that depend on the induction variable as part of the induction hypothesis.

theorem dvd_fac {i n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n := by
  -- ``ile`` depends on ``n``, the induction variable
  induction' n with n ih
  · exact absurd ipos (not_lt_of_ge ile)  -- "ex falso quodlibet"
  rw [fac]
  rcases Nat.of_le_succ ile with h | h  -- ile: i ≤ n i.e. i ≤ n.succ
  · apply dvd_mul_of_dvd_right (ih h)  -- dvd_mul_of_dvd_right takes ih; ih takes h
  · rw [h]; apply dvd_mul_right  -- n.succ = n+1

5.2.3. Finite Sums and Products

Induction is often used to prove identities involving finite sums and products.

Finset.sum s f: s : Finset α is a finite set of elements of the type α and f is a function defined on α.

You need import Algebra.BigOperators.Ring and open BigOperators to use notations like ∑ x ∈ s, f x ∏ x ∈ s, f x.

variable {α : Type*} (s : Finset ℕ) (f : ℕ → ℕ) (n : ℕ)

#check Finset.sum s f
#check Finset.prod s f

open BigOperators
open Finset

example : s.sum f = ∑ x ∈ s, f x :=
  rfl

example : s.prod f = ∏ x ∈ s, f x :=
  rfl

example : (range n).sum f = ∑ x ∈ range n, f x :=
  rfl

example : (range n).prod f = ∏ x ∈ range n, f x :=
  rfl

The facts Finset.sum_range_zero and Finset.sum_range_succ provide a recursive description of summation up to \(n\), and similarly for products.

example (f : ℕ → ℕ) : ∑ x ∈ range 0, f x = 0 :=
  Finset.sum_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∑ x ∈ range n.succ, f x = ∑ x ∈ range n, f x + f n :=
  Finset.sum_range_succ f n

example (f : ℕ → ℕ) : ∏ x ∈ range 0, f x = 1 :=
  Finset.prod_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∏ x ∈ range n.succ, f x = (∏ x ∈ range n, f x) * f n :=
  Finset.prod_range_succ f n

5.2.4. Nature Number

In Lean’s core library, both the natural numbers and its addition and multiplication are defined using recursion, and their fundamental properties are also established using induction.

inductive Nat where  -- ``Nat`` is a Type defined by induction
  | zero : Nat
  | succ (n : Nat) : Nat


def Nat.add : Nat → Nat → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)


-- Similar for multiplication
def Nat.mul : Nat → Nat → Nat
  | _, Nat.zero          => Nat.zero
  | a, Nat.succ b => Nat.add (Nat.mul a b) a

Thus:

n + 1
= Nat.add n 1
= Nat.add n (Nat.succ 0)
= Nat.succ (Nat.add n 0)
= Nat.succ n

5.3. Infinitely Many Primes

5.4. More Induction

In Section 5.2, we saw how to define the factorial function by recursion on the natural numbers.

def fac : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fac n

We also saw how to prove theorems using the induction' tactic.

theorem fac_pos (n : ℕ) : 0 < fac n := by
  induction' n with n ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n.succ_pos ih

5.4.1. induction

• The induction tactic (without the prime tick mark) allows for more structured syntax.

example (n : ℕ) : 0 < fac n := by
  induction n
  case zero =>
    rw [fac]
    exact zero_lt_one
  case succ n' ih =>
    rw [fac]
    exact mul_pos n'.succ_pos ih

example (n : ℕ) : 0 < fac n := by
  induction n with
  | zero =>
    rw [fac]
    exact zero_lt_one
  | succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

5.4.2. More Ways to Define/Use Inductions

We can even prove a theorem (with the same notation) as if we are defining a recursive function.

theorem fac_pos' : ∀ n, 0 < fac n  -- we insert ``∀ n``; also the absence of ``:=``
  | 0 => by  -- by
    rw [fac]
    exact zero_lt_one
  | n + 1 => by  -- by
    rw [fac]
    -- as if the theorem itself is a recursive function of n
    exact mul_pos n.succ_pos (fac_pos' n)  -- we make a recursive call for the inductive step

• We can also define the Fibonacci function with multiple base cases:

@[simp] def fib : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

The @[simp] annotation means that the simplifier will use the defining equations. You can also apply them by writing rw [fib]. Below it will be helpful to give a name to the n + 2 case.

theorem fib_add_two (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := rfl

example (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := by rw [fib]

• Using Lean’s computational interpretation, we can evaluate the Fibonacci numbers.

#eval fib 6
-- ``|>``: forward pipe operator
-- ``x |> f`` means “take x and apply f to it”, i.e., f x.
#eval List.range 20 |>.map fib  -- ``(List.range 20).map fib`` or ``List.map fib (List.range 20)``

5.4.3. Tail-Recursive

The straightforward implementation of fib is computationally inefficient: It runs in time exponential in its argument.

Tail-Recursive defines recursion with pattern matching, running time is linear in n.

def fib' (n : Nat) : Nat :=
  -- pattern:
  -- aux remaining #recursions, F(0), F(1)
  -- aux remaining #recursions, value we should return, next value we should return
  aux n 0 1  -- aux is just a name, choose whatever you want
where aux  -- ``where`` implements ``aux`` by defining rules for matching patterns
  | 0,   x, _ => x
  | n+1, x, y => aux n y (x + y)  -- after each recursion, we count--, and shift (x, y) to (y, x + y)


def fib'' (n : Nat) : Nat :=
  aux n 0 1 1
where aux
  | 0,   x, _, _ => x
  | 1,   _, y, _ => y
  | n+1, x, y, z => aux n y z (x + y + z)

#eval fib' 10000
#eval fib'' 5

theorem fib'.aux_eq (m n : ℕ) : fib'.aux n (fib m) (fib (m + 1)) = fib (n + m) := by
  induction n generalizing m with  -- ``induction ... with`` will intro hypo ``ih`` in the succ case
  | zero => simp [fib'.aux]
  -- ``generalizing m`` inserts ``∀ m`` in front of ``ih``
  | succ n ih => rw [fib'.aux, ←fib_add_two, ih, add_assoc, add_comm 1]