Natural numbers

The natural numbers—0, 1, 2, and so on—form the foundation of mathematics. In Lean and other proof assistants, natural numbers aren’t taken for granted; instead, they are built from the ground up using inductive types. This approach not only mirrors their intuitive construction but also unlocks powerful tools for reasoning about them formally.

In this chapter, we’ll explore how the natural numbers are defined inductively in Lean, and how such a definition allows us to reason about them using case analysis and mathematical induction. We’ll also examine how to define functions on natural numbers using recursion, and use this technique to construct the familiar operations of maximum and minimum, addition and multiplication. The chapter concludes with exercises to reinforce our understanding and help us apply these concepts.

Definition

The natural numbers Nat are defined inductively in Lean using two constructors: zero, which represents the base case, and succ, which takes a natural number and returns its successor. This closely follows the Peano axioms, where 0 is a natural number and, if n is a natural number, then so is n + 1.

If we #print Nat, Lean returns:

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

Inductive types like Nat not only specify how values are built, but also provide fundamental principles of recursion and induction. These principles allow functions to be defined by pattern matching on constructors, and proofs to be carried out using structural induction.

Lean comes with the Nat type already implemented, along with many theorems related to natural numbers. However, to gain a deeper understanding of how natural numbers can be constructed and reasoned about, we will define our own custom type, which we will simply call N.

Natural Numbers.lean

inductive N : Type where
  | z : N
  | s : N →  N
deriving Repr

The deriving Repr clause is used to automatically generate an instance of the Repr type class for a user-defined type. The Repr class defines how values of a type can be converted into a human-readable format, primarily for the purpose of displaying them during evaluation or debugging. When a type derives Repr, Lean synthesizes the necessary code to produce a structured string representation of any value of that type. This is particularly useful when using commands like #eval, where Lean attempts to evaluate an expression and display the result. Without a Repr instance, Lean would not know how to present the value, resulting in an error. By including deriving Repr in a type declaration, users enable Lean to show values automatically, making it easier to inspect the behavior of programs and proofs.

If we #print N, Lean returns:

Natural Numbers.lean

inductive N : Type
number of parameters: 0
constructors:
N.z : N
N.s : N → N

We can acces the two constructors of N with N.z and N.s. To work with N without needing to prefix everything with N., we can open the namespace to bring its notation into scope.

Natural Numbers.lean

open N
#check z
#check s

Cases

Assuming x is a variable in the local context with an inductive type, cases x splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor.

The code below defines a function Eqzero in Lean, which takes a natural number n of type N and returns a boolean value in Bool. The purpose of this function is to compare the given number n with zero. The function is defined using cases over the structure of a natural number n, used to perform a case analysis. This splits the proof into two cases:

1. Case Zero: When n is zero, represented by z, the function returns true, indicating that n is equal to zero.
2. Case Successor: When n is the successor s of some natural number m the function returns false, indicating that n is not equal to zero.

Natural Numbers.lean

def Eqzero : N → Bool := by
  intro n
  cases n
  -- Case zero
  exact true
  -- Case successor
  exact false

Match

Let us recall that an alternative to using cases is the match expression, which enables us to perform pattern matching directly within a definition. In what follows, we will define an alternative version of Eqzero using this approach.

Natural Numbers.lean

def Eqzero2 : N → Bool := by
  intro n
  match n with
    | z    => exact true
    | s _  => exact false

Dedekind-Peano

Cases

Note that the type N gives us a Dedekind–Peano algebra. We can think of this type as the free algebra generated by a constant z and a unary operation s. In this setup, z can never be equal to s n for any n : N.

Natural Numbers.lean

theorem TZInj : ∀ (n : N), z ≠ s n := by
  intro n
  intro h
  cases h

In the proof of the theorem NInj, the first step intro n introduces an arbitrary element n of type N. This sets the stage for proving that z is not equal to s n for any such n. The next step, intro h, assumes the contrary—that is, it introduces a hypothesis h : z = s n. To analyze this equality, we apply the tactic cases h, which attempts to decompose the equation. However, since z and s n are built using different constructors of the inductive type N, Lean can immediately determine that this equality is impossible. This is a consequence of the fact that constructors of an inductive type are disjoint—they produce values that can never be equal. As a result, Lean closes the goal automatically, completing the proof.

Injection

Similarly, the successor function s is injective. For this we use the tactic injection which states that constructors of inductive data types are injective.

Natural Numbers.lean

theorem TSuccInj : injective s := by
  intro n m
  intro h
  injection h

noConfusion

The noConfusion principle formalizes the fact that the different constructors of an inductive type are distinct and that they are injective when applied to arguments. Here’s how it works in practice:

Natural Numbers.lean

theorem TSuccInjAlt : injective s := by
  intro n m h
  exact N.noConfusion h id

In this proof, we’re saying: if s n = s m, then—by the injectivity of the s constructor—we must have n = m. The noConfusion principle takes the equality h : s n = s m and safely removes the constructors, handing us the equality n = m underneath. This is especially useful when we want to avoid manual pattern matching with cases or match, and instead reason abstractly about the structure of our inductive values.

Induction

Assuming x is a variable of inductive type in the local context, the tactic induction x applies induction on x to the main goal. This results in one subgoal for each constructor of the inductive type, where the target is replaced by a general instance of that constructor. For each recursive argument of the constructor, an inductive hypothesis is introduced. If any element in the local context depends on x, it is reverted and then reintroduced after the induction, ensuring that the inductive hypothesis properly incorporates these dependencies.

Next theorem proves that a predicate holds for every natural number.

Natural Numbers.lean

theorem TInd {P : N → Prop} (h0 : P z) (hi : ∀ (n : N), P n → P (s n)) : 
∀ (n : N), P n := by
  intro n
  induction n
  -- Base case: `z`
  exact h0
  -- Inductive step: assume the property holds for `n`,
  -- and prove it for `s n`
  rename_i n hn
  exact (hi n) hn

The proof proceeds by induction on n:

1. Base case: We begin with the case z. Here, we need to show that P z holds. But this is precisely what h0 provides, so the base case is established.

2. Inductive step: For the inductive case, we assume a natural number n and the inductive hypothesis hn : P n, which states that the property holds for n. Our goal is to show that P (s n) holds. This follows directly from the hypothesis hi.

Recursion

Recursion is a fundamental concept in both mathematics and computer science, allowing us to define functions in terms of simpler instances of themselves. In the context of natural numbers, recursive definitions mirror the inductive structure of the numbers themselves. This structure lends itself naturally to recursive functions, where we specify the result for the base case and describe how to compute the result for a successor in terms of the result for its predecessor. In this subsection, we will explore how recursion works in Lean, with simple examples like the definition of the maximum and the minimum, the addition and the multiplication.

Maximum

Recursive definition of the maximum of two natural numbers.

Maximum.lean

def max : N → N → N := by
  intro n m
  match n, m with
    | z, m  => exact m
    | n, z  => exact n
    | s n', s m' => exact s (max n' m')

Minimum

Recursive definition of the minimum of two natural numbers.

Minimum.lean

def min : N → N → N := by
  intro n m
  match n, m with
    | z, _  => exact z
    | _, z  => exact z
    | s n', s m' => exact s (min n' m')

Addition

We now define the function Addition, which recursively specifies the addition of natural numbers by recursion on the first argument. For clarity and readability, we will use the shorthand notation n + m in place of Addition n m.

Addition.lean

def Addition : N → N → N := by
  intro n m
  cases n with
  | z   => exact m
  | s n => exact s (Addition n m)
-- Notation for Addition
notation : 65 lhs:65 " + " rhs:66 => Addition lhs rhs

Addition takes two natural numbers n and m as input and computes their addition by recursion on n. The base case handles the situation when n is zero in which case the result is simply m, since adding zero to any number yields that number. In the inductive case, where we consider s n, the successor of n, the function returns the successor of the recursive addition of n and m, that is, s (Addition n m). This reflects the intuitive idea that to compute (s n) + m, we first compute n + m and then take its successor.

Fibonacci

Thanks to Addition we can define the Fibonacci function recursively.

Fibonacci.lean

def Fib : N → N := by
  intro n
  match n with
    | z       => exact z
    | s z     => exact (s z)
    | s (s n) => exact n + (s n)

Multiplication

With a similar idea, we can define the function Multiplication, which recursively specifies the multiplication of natural numbers by recursion on the first argument. For clarity and readability, we will use the shorthand notation n * m in place of Multiplication n m.

Multiplication.lean

def Multiplication : N → N → N := by
  intro n m
  cases n with
  | z   => exact z
  | s n => exact (Multiplication n m) + m
-- Notation for Multiplication
notation : 70 lhs:70 " * " rhs:71 => Multiplication lhs rhs

Multiplication takes two natural numbers n and m as input and computes their addition by recursion on n. The base case handles the situation when n is zero in which case the result is simply z, since multiplying zero to any number yields zero. In the inductive case, where we consider s n, the successor of n, the function returns the sum of the recursive multiplication of n and m and m, that is, (Multiplication n m) + m. This reflects the intuitive idea that to compute (s n) * m, we first compute n * m and then add m.

Factorial

Thanks to Multiplication we can define the factorial function recursively.

Factorial.lean

def Fact : N → N := by 
  intro n 
  cases n with 
    | z   => exact (s z)
    | s n => exact (s n) * (Fact n)

Decidable Equality

Thanks to the inductive structure of N, we can define a recursive procedure to determine whether two values of type N are equal. This means providing an instance of the DecidableEq type class for N. The idea is simple: we compare two values by structurally analyzing their form—whether they are both zero, both successors, or mismatched. In the case of successors, we reduce the problem to their predecessors and apply the same logic recursively. Here’s how this can be implemented:

DecidableEqN.lean

def instDecidableEqN : DecidableEq N := by
  intro n m 
  match n, m with
    | z, z        => exact isTrue  rfl
    | z, s _      => exact isFalse (by intro h; cases h)
    | s _, z      => exact isFalse (by intro h; cases h)
    | s n', s m'  =>
      match instDecidableEqN n' m' with
      | isTrue h  => exact isTrue (congrArg s h)
      | isFalse h => exact isFalse (fun h' => N.noConfusion h' (fun h'' => h h''))

Exercises

Injection

Exercises.lean

-- Prove that no natural number is equal to its own successor
theorem TInjSucc {n : N} : ¬ (n = s n) := by sorry

Maximum

Exercises.lean

-- Max (z, n) = n
theorem TMaxzL : ∀ {n : N}, (maxi z n) = n := by sorry

-- Max (n, z) = n
theorem TMaxzR : ∀ {n : N}, (maxi n z) = n := by sorry

-- Max (n, m) = Max (m, n)
theorem TMaxComm : ∀ {n m : N}, (maxi n m) = (maxi m n) := by sorry

-- Max (n, m) = n ∨ Max (n, m) = m
theorem TMaxOut : ∀ {n m : N}, ((maxi n m) = n) ∨ ((maxi n m) = m) := by sorry

-- `Max (n, n) = n`
theorem TMaxIdpt : ∀ {n : N}, maxi n n = n := by sorry

Minimum

Exercises.lean

-- Min (z, n) = z
theorem TMinzL : ∀ {n : N}, (mini z n) = z := by sorry

-- Min (n, z) = z
theorem TMinzR : ∀ {n : N}, (mini n z) = z := by sorry

-- Min (n, m) = Min (m, n)
theorem TMinComm : ∀ {n m : N}, (mini n m) = (mini m n) := by sorry

-- Min (n, m) = n ∨ Min (n, m) = m
theorem TMinOut : ∀ {n m : N}, ((mini n m) = n) ∨ ((mini n m) = m) := by sorry

-- `Min (n, n) = n`
theorem TMinIdpt : ∀ {n : N}, mini n n = n := by sorry

-- `Min (n, m) = Max (n, m) → n = m `
theorem TMinMaxEq : ∀ {n m : N}, mini n m = maxi n m → n = m := by sorry

-- `Min (n, m) = n ↔ Max (n, m) = m`
theorem TMinMax : ∀ {n m : N}, mini n m = n ↔ maxi n m = m := by sorry

Addition

Exercises.lean

-- z is a left identity for addition
theorem TAdd0L : ∀ {n : N}, z + n = n := by sorry

-- z is a right identity for addition
theorem TAdd0R : ∀ {n : N}, n + z = n := by sorry

-- Addition of natural numbers is commutative up to a successor
theorem TAddOne : ∀ {n m : N}, (s n) + m = n + (s m) := by sorry

-- Addition is commutative
theorem TAddComm : ∀ {n m : N}, n + m = m + n := by sorry

-- If the sum of two natural numbers is zero, then the first number must be zero
theorem TAddZ : ∀ {n m : N}, n + m = z → n = z := by sorry

-- If the sum of two natural numbers is zero, then both numbers are zero
theorem TAddZ2 : ∀ {n m : N}, n + m = z → (n = z) ∧ (m = z) := by sorry

-- Addition is associative
theorem TAddAss : ∀{n m p : N}, (n + m) + p = n + (m + p) := by sorry

-- n can never be equal to n + s k
theorem TAddSucc : ∀ {n k : N}, n = n + (s k) → False := by sorry

-- A number cannot be both ahead of and behind another number by a positive amount
theorem TIncAdd : ∀ {n m k : N}, m = n + (s k) →  n = m + (s k) → False := by sorry

-- Right congruence of addition
theorem TAddCongR : ∀ {n m k : N}, m = k → n + m = n + k := by sorry

-- Left congruence of addition
theorem TAddCongL : ∀ {n m k : N}, m = k → m + n = k + n := by sorry

-- Addition on the left is cancellative
theorem TAddCancL : ∀ {n m k : N}, n + m = n + k → m = k := by sorry

-- Addition on the right is cancellative
theorem TAddCancR : ∀ {n m k : N}, m + n = k + n → m = k := by sorry

-- Left cancellation property of addition with zero
theorem TAddCancLZ : ∀ {n m : N}, n + m = n → m = z := by sorry

-- Right cancellation property of addition with zero
theorem TAddCancRZ : ∀ {n m : N}, m + n = n → m = z := by sorry

Multiplication

Exercises.lean

-- z is a left zero for multiplication
theorem TMult0L : ∀ {n : N}, z * n = z := by sorry

-- z is a right zero for multiplication
theorem TMult0R : ∀ {n : N}, n * z = z := by sorry

-- We introduce `one`
def one : N := s z

-- one + n = s n
theorem TOneAddR : ∀ {n : N}, one + n = s n := by sorry

-- n + one = s n
theorem TOneAddL : ∀ {n : N}, n + one = s n := by sorry

-- The different cases for two numbers adding to one
theorem TAddOneCases : ∀ {n m : N}, n + m = one → (n = z ∧ m = one) ∨ 
(n = one ∧ m = z) := by sorry

-- one is a left identity for multiplication
theorem TMult1L : ∀ {n : N}, one * n = n := by sorry

-- one is a right identity for multiplication
theorem TMult1R : ∀ {n : N}, n * one = n := by sorry

-- Multiplication is left distributive over addition
theorem TMultDistL : ∀ {n m k : N}, (n + m) * k = (n * k) + (m * k) := by sorry

-- Multiplication is right distributive over addition
theorem TMultDistR : ∀ {n m k : N}, n * (m + k) = (n * m) + (n * k) := by sorry

-- Multiplication is commutative
theorem TMultComm : ∀ {n m : N}, n * m = m * n := by sorry

-- If the product of two natural numbers is zero, then one of them must be zero
theorem TMultZ : ∀ {n m : N}, n * m = z → (n = z) ∨ (m = z) := by sorry

-- Right congruence of multiplication
theorem TMultCongR : ∀ {n m k : N}, m = k → n * m = n * k := by sorry

-- Left congruence of addition
theorem TMultCongL : ∀ {n m k : N}, m = k → m * n = k * n := by sorry

-- Multiplication is associative
theorem TMultAss : ∀{n m p : N}, (n * m) * p = n * (m * p) := by sorry

-- Fix points for multiplication
theorem TMultFix : ∀{n m : N}, n * m = n → n = z ∨ m = one := by sorry

-- One is the unique idempotent for multiplication
theorem TMultOne : ∀ {n m : N}, n * m = one ↔ (n = one ∧ m = one) := by sorry