Analysis I, Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers

In this (technical) epilogue, we show that the "Chapter 2" natural numbers Chapter2.Nat are isomorphic in various senses to the standard natural numbers ℕ.

After this epilogue, Chapter2.Nat will be deprecated, and we will instead use the standard natural numbers ℕ throughout. In particular, one should use the full Mathlib API for ℕ for all subsequent chapters, in lieu of the Chapter2.Nat API.

Filling the sorries here requires both the Chapter2.Nat API and the Mathlib API for the standard natural numbers ℕ. As such, they are excellent exercises to prepare you for the aforementioned transition.

In second half of this section we also give a fully axiomatic treatment of the natural numbers via the Peano axioms. The treatment in the preceding three sections was only partially axiomatic, because we used a specific construction Chapter2.Nat of the natural numbers that was an inductive type, and used that inductive type to construct a recursor. Here, we give some exercises to show how one can accomplish the same tasks directly from the Peano axioms, without knowing the specific implementation of the natural numbers.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

• (Add tip here)

@[reducible, inline]

abbrev Chapter2.Nat.toNat (n : Nat) : ℕ

Converting a Chapter 2 natural number to a Mathlib natural number.

Equations

• Chapter2.Nat.zero.toNat = 0
• n'++.toNat = n'.toNat + 1

theorem Chapter2.Nat.zero_toNat : toNat 0 = 0

theorem Chapter2.Nat.succ_toNat (n : Nat) : n++.toNat = n.toNat + 1

@[reducible, inline]

abbrev Chapter2.Nat.equivNat : Nat ≃ ℕ

The conversion is a bijection. Here we use the existing capability (from Section 2.1) to map the Mathlib natural numbers to the Chapter 2 natural numbers.

Equations

• Chapter2.Nat.equivNat = { toFun := Chapter2.Nat.toNat, invFun := fun (n : ℕ) => ↑n, left_inv := Chapter2.Nat.equivNat._proof_1, right_inv := Chapter2.Nat.equivNat._proof_2 }

@[reducible, inline]

abbrev Chapter2.Nat.map_add (n m : Nat) : (n + m).toNat = n.toNat + m.toNat

The conversion preserves addition.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Chapter2.Nat.map_mul (n m : Nat) : (n * m).toNat = n.toNat * m.toNat

The conversion preserves multiplication.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Chapter2.Nat.map_le_map_iff {n m : Nat} : n.toNat ≤ m.toNat ↔ n ≤ m

The conversion preserves order.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Chapter2.Nat.equivNat_ordered_ring : Nat ≃+*o ℕ

Equations

• Chapter2.Nat.equivNat_ordered_ring = { toEquiv := Chapter2.Nat.equivNat, map_mul' := Chapter2.Nat.map_mul, map_add' := Chapter2.Nat.map_add, map_le_map_iff' := ⋯ }

theorem Chapter2.Nat.pow_eq_pow (n m : Nat) : n.toNat ^ m.toNat = (n ^ m).toNat

The conversion preserves exponentiation.

structure PeanoAxioms : Type 1

The Peano axioms for an abstract type Nat

• Nat : Type
• zero : self.Nat
• succ : self.Nat → self.Nat
• succ_ne (n : self.Nat) : self.succ n ≠ self.zero
• succ_cancel {n m : self.Nat} : self.succ n = self.succ m → n = m
• induction (P : self.Nat → Prop) : P self.zero → (∀ (n : self.Nat), P n → P (self.succ n)) → ∀ (n : self.Nat), P n

theorem PeanoAxioms.ext {x y : PeanoAxioms} (Nat : x.Nat = y.Nat) (zero : x.zero ≍ y.zero) (succ : x.succ ≍ y.succ) : x = y

theorem PeanoAxioms.ext_iff {x y : PeanoAxioms} : x = y ↔ x.Nat = y.Nat ∧ x.zero ≍ y.zero ∧ x.succ ≍ y.succ

def PeanoAxioms.Chapter2_Nat : PeanoAxioms

The Chapter 2 natural numbers obey the Peano axioms.

Equations

• PeanoAxioms.Chapter2_Nat = { Nat := Chapter2.Nat, zero := Chapter2.Nat.zero, succ := Chapter2.Nat.succ, succ_ne := Chapter2.Nat.succ_ne, succ_cancel := ⋯, induction := Chapter2.Nat.induction }

def PeanoAxioms.Mathlib_Nat : PeanoAxioms

The Mathlib natural numbers obey the Peano axioms.

Equations

• PeanoAxioms.Mathlib_Nat = { Nat := ℕ, zero := 0, succ := Nat.succ, succ_ne := Nat.succ_ne_zero, succ_cancel := @PeanoAxioms.Mathlib_Nat._proof_1, induction := ⋯ }

@[reducible, inline]

abbrev PeanoAxioms.natCast (P : PeanoAxioms) : ℕ → P.Nat

One can map the Mathlib natural numbers into any other structure obeying the Peano axioms.

Equations

• P.natCast Nat.zero = P.zero
• P.natCast n_2.succ = P.succ (P.natCast n_2)

theorem PeanoAxioms.natCast_injective (P : PeanoAxioms) : Function.Injective P.natCast

One can start the proof here with unfold Function.Injective, although it is not strictly necessary.

theorem PeanoAxioms.natCast_surjective (P : PeanoAxioms) : Function.Surjective P.natCast

One can start the proof here with unfold Function.Surjective, although it is not strictly necessary.

class PeanoAxioms.Equiv (P Q : PeanoAxioms) : Type

The notion of an equivalence between two structures obeying the Peano axioms. The symbol ≃ is an alias for Mathlib's Equiv class; for instance P.Nat ≃ Q.Nat is an alias for _root_.Equiv P.Nat Q.Nat.

• equiv : P.Nat ≃ Q.Nat
• equiv_zero : equiv P.zero = Q.zero
• equiv_succ (n : P.Nat) : equiv (P.succ n) = Q.succ (equiv n)

@[reducible, inline]

abbrev PeanoAxioms.Equiv.symm {P Q : PeanoAxioms} (equiv : P.Equiv Q) : Q.Equiv P

This exercise will require application of Mathlib's API for the Equiv class. Some of this API can be invoked automatically via the simp tactic.

Equations

• equiv.symm = { equiv := PeanoAxioms.Equiv.equiv.symm, equiv_zero := ⋯, equiv_succ := ⋯ }

@[reducible, inline]

abbrev PeanoAxioms.Equiv.trans {P Q R : PeanoAxioms} (equiv1 : P.Equiv Q) (equiv2 : Q.Equiv R) : P.Equiv R

This exercise will require application of Mathlib's API for the Equiv class. Some of this API can be invoked automatically via the simp tactic.

Equations

• equiv1.trans equiv2 = { equiv := PeanoAxioms.Equiv.equiv.trans PeanoAxioms.Equiv.equiv, equiv_zero := ⋯, equiv_succ := ⋯ }

@[reducible, inline]

noncomputable abbrev PeanoAxioms.Equiv.fromNat (P : PeanoAxioms) : Mathlib_Nat.Equiv P

Useful Mathlib tools for inverting bijections include Function.surjInv and Function.invFun.

Equations

• PeanoAxioms.Equiv.fromNat P = { equiv := { toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }, equiv_zero := ⋯, equiv_succ := ⋯ }

@[reducible, inline]

noncomputable abbrev PeanoAxioms.Equiv.mk' (P Q : PeanoAxioms) : P.Equiv Q

The task here is to establish that any two structures obeying the Peano axioms are equivalent.

Equations

• PeanoAxioms.Equiv.mk' P Q = sorry

theorem PeanoAxioms.Equiv.uniq {P Q : PeanoAxioms} (equiv1 equiv2 : P.Equiv Q) : equiv1 = equiv2

There is only one equivalence between any two structures obeying the Peano axioms.

theorem PeanoAxioms.Nat.recurse_uniq {P : PeanoAxioms} (f : P.Nat → P.Nat → P.Nat) (c : P.Nat) : ∃! a : P.Nat → P.Nat, a P.zero = c ∧ ∀ (n : P.Nat), a (P.succ n) = f n (a n)

A sample result: recursion is well-defined on any structure obeying the Peano axioms