Internally, in Lean, the natural numbers are defined as a type generated inductively from an axiomatically declared zero and succ operation:
namespace hidden
open Nat
-- BEGIN
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
-- END
end hiddenIf you click the button that copies this text into the editor in the online version of this textbook, you will see that we wrap it with the phrases namespace hidden and end hidden. This puts the definition into a new "namespace," so that the identifiers that are defined are hidden.Nat, hidden.Nat.zero and hidden.Nat.succ, to avoid conflicting with the one that is in the Lean library. Below, we will do that in a number of places where our examples duplicate objects defined in the library. The unicode symbol ℕ, entered with \N or \nat, is a synonym for Nat.
Declaring Nat as an inductively defined type means that we can define functions by recursion, and prove theorems by induction. For example, these are the first two recursive definitions presented in the last chapter:
import Mathlib.Data.Nat.Defs
open Nat
def two_pow : ℕ → ℕ
| 0 => 1
| (succ n) => 2 * two_pow n
def fact : ℕ → ℕ
| 0 => 1
| (succ n) => (succ n) * fact nAddition and numerals are defined in such a way that Lean recognizes succ n and n + 1 as essentially the same, so we could instead write these definitions as follows:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
def two_pow : ℕ → ℕ
| 0 => 1
| (n + 1) => 2 * two_pow n
def fact : ℕ → ℕ
| 0 => 1
| (n + 1) => (n + 1) * fact n
-- ENDIf we wanted to define the function m^n, we would do that by fixing m, and writing doing the recursion on the second argument:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
def pow (m : ℕ) : ℕ → ℕ
| 0 => 1
| (n + 1) => (pow m n) * m
-- ENDIn fact, this is how the power function on the natural numbers,
Nat.pow, is defined in Lean's library.
Lean is also smart enough to interpret more complicated forms of recursion, like this one:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
def fib : ℕ → ℕ
| 0 => 0
| 1 => 1
| (n + 2) => fib (n + 1) + fib nIn addition to defining functions by recursion, we can prove theorems by induction. In Lean, each clause of a recursive definition results in a new identity. For example, the two clauses in the definition of pow above give rise to the following two theorems:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
example (n : ℕ) : Nat.pow n 0 = 1 := rfl
example (m n : ℕ) : Nat.pow m (n+1) = (Nat.pow m n) * m := rfl
-- ENDLean defines the usual notation for exponentiation:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
example (n : ℕ) : n^0 = 1 := rfl
example (m n : ℕ) : m^(n+1) = m^n * m := rfl
#check @Nat.pow_zero
#check @Nat.pow_succ
-- ENDNotice that we could alternatively have used m * Nat.pow m n
in the second clause of the definition of Nat.pow.
Of course, we can prove that the two definitions are equivalent using the
commutativity of multiplication, but,
using a proof by induction,
we can also prove it using only the associativity of multiplication,
and the properties 1 * m = m and m * 1 = m.
This is useful, because the power function is also often used in situations
where multiplication is not commutative,
such as with matrix multiplication.
The theorem can be proved in Lean as follows:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
example (m n : ℕ) : m^(succ n) = m * m^n := by
induction n with
| zero =>
show m^(succ 0) = m * m^0
calc
m^(succ 0) = m^0 * m := by rw [Nat.pow_succ]
_ = 1 * m := by rw [Nat.pow_zero]
_ = m := by rw [Nat.one_mul]
_ = m * 1 := by rw [Nat.mul_one]
_ = m * m^0 := by rw [Nat.pow_zero]
| succ n ih =>
show m^(succ (succ n)) = m * m^(succ n)
calc
m^(succ (succ n)) = m^(succ n) * m := by rw [Nat.pow_succ]
_ = (m * m^n) * m := by rw [ih]
_ = m * (m^n * m) := by rw [Nat.mul_assoc]
_ = m * m^(succ n) := by rw [Nat.pow_succ]
-- ENDThis is a typical proof by induction in Lean.
It begins with the tactic induction n with,
which is like cases n with,
but also supplies the induction hypothesis ih
in the successor case.
Here is a shorter proof:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
example (m n : ℕ) : m^(succ n) = m * m^n := by
induction n with
| zero =>
show m^(succ 0) = m * m^0
rw [Nat.pow_succ, Nat.pow_zero, Nat.one_mul, Nat.mul_one]
| succ n ih =>
show m^(succ (succ n)) = m * m^(succ n)
rw [Nat.pow_succ, Nat.pow_succ, ← Nat.mul_assoc, ← ih, Nat.pow_succ]
-- ENDRemember that you can write a rewrite proof incrementally, checking the error messages to make sure things are working so far, and to see how far Lean got.
As another example of a proof by induction, here is a proof of the identity m^(n + k) = m^n * m^k.
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
example (m n k : ℕ) : m^(n + k) = m^n * m^k := by
induction n with
| zero =>
show m^(0 + k) = m^0 * m^k
calc m^(0 + k) = m^k := by rw [Nat.zero_add]
_ = 1 * m^k := by rw [Nat.one_mul]
_ = m^0 * m^k := by rw [Nat.pow_zero]
| succ n ih =>
show m^(succ n + k) = m^(succ n) * m^k
calc
m^(succ n + k) = m^(succ (n + k)) := by rw [Nat.succ_add]
_ = m * m^(n + k) := by rw [Nat.pow_succ']
_ = m * (m^n * m^k) := by rw [ih]
_ = (m * m^n) * m^k := by rw [Nat.mul_assoc]
_ = m^(succ n) * m^k := by rw [Nat.pow_succ']
-- ENDNotice the same pattern.
We do induction on n,
and the base case and inductive step are routine.
The theorem is called pow_add in the library,
and once again, with a bit of cleverness,
we can shorten the proof with rewrite:
import Mathlib.Data.Nat.Defs
open Nat
-- BEGIN
example (m n k : ℕ) : m^(n + k) = m^n * m^k := by
induction n with
| zero =>
show m^(0 + k) = m^0 * m^k
rw [Nat.zero_add, Nat.pow_zero, Nat.one_mul]
| succ n ih =>
show m^(succ n + k) = m^(succ n) * m^k
rw [Nat.succ_add, Nat.pow_succ', ih, ← Nat.mul_assoc, Nat.pow_succ']
-- ENDYou should not hesitate to use calc,
however, to make the proofs more explicit.
Remember that you can also use calc and rewrite together,
using calc to structure the calculational proof,
and using rewrite to fill in each justification step.
In fact, addition and multiplication are defined in Lean essentially as described in :numref:`defining_arithmetic_operations`. The defining equations for addition hold by reflexivity, but they are also named add_zero and add_succ:
import Mathlib.Data.Nat.Defs
open Nat
variable (m n : ℕ)
-- BEGIN
example : m + 0 = m := Nat.add_zero m
example : m + succ n = succ (m + n) := Nat.add_succ m n
-- ENDSimilarly, we have the defining equations for the predecessor function and multiplication:
import Mathlib.Data.Nat.Defs
-- BEGIN
#check @Nat.pred_zero
#check @Nat.pred_succ
#check @Nat.mul_zero
#check @Nat.mul_succ
-- ENDHere are the five propositions proved in :numref:`defining_arithmetic_operations`.
import Mathlib.Data.Nat.Defs
open Nat
namespace hidden
-- BEGIN
theorem succ_pred (n : ℕ) : n ≠ 0 → succ (pred n) = n := by
intro (hn : n ≠ 0)
cases n with
| zero => exact absurd rfl (hn : 0 ≠ 0)
| succ n => rw [Nat.pred_succ]
-- END
end hiddenNote that we don't need to use induction here, only cases.
We prove the next one in term mode instead:
import Mathlib.Data.Nat.Defs
open Nat
namespace hidden
-- BEGIN
theorem zero_add (n : Nat) : 0 + n = n :=
match n with
| zero => show 0 + 0 = 0 from rfl
| succ n =>
show 0 + succ n = succ n from calc
0 + succ n = succ (0 + n) := by rfl
_ = succ n := by rw [zero_add n]
-- END
end hiddenThe match notation is very similar to induction,
except it does not let us provide a name like ih
for the induction hypothesis.
Instead, we call zero_add n : 0 + n = n,
which is the induction hypothesis.
Note that calling zero_add (succ n) in the same place would be circular,
and if we did so Lean would throw an error.
import Mathlib.Data.Nat.Defs
open Nat
namespace hidden
-- BEGIN
theorem succ_add (m n : Nat) : succ m + n = succ (m + n) :=
match n with
| 0 => show succ m + 0 = succ (m + 0) from rfl
| n + 1 =>
show succ m + succ n = succ (m + succ n) from calc
succ m + succ n = succ (succ m + n) := by rfl
_ = succ (succ (m + n)) := by rw [succ_add m n]
_ = succ (m + succ n) := by rfl
-- END
end hiddenNote that this time we used 0 and n + 1 in the match cases.
Here are the final two:
import Mathlib.Data.Nat.Defs
open Nat
namespace hidden
-- BEGIN
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
match k with
| 0 => show m + n + 0 = m + (n + 0) from by
rw [Nat.add_zero, Nat.add_zero]
| k + 1 => show m + n + succ k = m + (n + (succ k)) from by
rw [add_succ, add_assoc m n k, add_succ, add_succ]
theorem add_comm (m n : Nat) : m + n = n + m :=
match n with
| 0 => show m + 0 = 0 + m from by rw [Nat.add_zero, Nat.zero_add]
| n + 1 => show m + succ n = succ n + m from calc
m + succ n = succ (m + n) := by rw [add_succ]
_ = succ (n + m) := by rw [add_comm m n]
_ = succ n + m := by rw [succ_add]
-- END
end hiddenFormalize as many of the identities from :numref:`defining_arithmetic_operations` as you can by replacing each sorry with a proof.
import Mathlib.Data.Nat.Defs open Nat --1.a. example : ∀ m n k : Nat, m * (n + k) = m * n + m * k := sorry --1.b. example : ∀ n : Nat, 0 * n = 0 := sorry --1.c. example : ∀ n : Nat, 1 * n = n := sorry --1.d. example : ∀ m n k : Nat, (m * n) * k = m * (n * k) := sorry --1.e. example : ∀ m n : Nat, m * n = n * m := sorry
Formalize as many of the identities from :numref:`arithmetic_on_the_natural_numbers` as you can by replacing each sorry with a proof.
import Mathlib.Data.Nat.Defs open Nat --2.a. example : ∀ m n k : Nat, n ≤ m → n + k ≤ m + k := sorry --2.b. example : ∀ m n k : Nat, n + k ≤ m + k → n ≤ m := sorry --2.c. example : ∀ m n k : Nat, n ≤ m → n * k ≤ m * k := sorry --2.d. example : ∀ m n : Nat, m ≥ n → m = n ∨ m ≥ n+1 := sorry --2.e. example : ∀ n : Nat, 0 ≤ n := sorry