Analysis I, Chapter 2 epilogue

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

From this point onwards, Chapter2.Nat will be deprecated, and we will use the standard natural numbers ℕ instead. 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.

abbrev Chapter2.Nat.toNat (n : Chapter2.Nat) : ℕ := match n with | Chapter2.Nat.zero => 0 | Chapter2.Nat.succ n' => n'.toNat + 1lemma Chapter2.Nat.zero_toNat : (0 : Chapter2.Nat).toNat = 0 := rfllemma Chapter2.Nat.succ_toNat (n : Chapter2.Nat) : (n++).toNat = n.toNat + 1 := rflabbrev Chapter2.Nat.equivNat : Chapter2.Nat ≃ ℕ where toFun := Chapter2.Nat.toNat invFun n := (n:Chapter2.Nat) left_inv n := byn:Nat⊢ (fun n => ↑n) n.toNat = n induction' n with n hnzero⊢ (fun n => ↑n) zero.toNat = zerosuccn:Nathn:(fun n => ↑n) n.toNat = n⊢ (fun n => ↑n) n++.toNat = n++ .zero⊢ (fun n => ↑n) zero.toNat = zero rflAll goals completed! 🐙 simp [Chapter2.Nat.succ_toNat, hn]succn:Nathn:(fun n => ↑n) n.toNat = n⊢ n + 1 = n++ symmsuccn:Nathn:(fun n => ↑n) n.toNat = n⊢ n++ = n + 1 exact succ_eq_add_one _All goals completed! 🐙 right_inv n := byn:ℕ⊢ ((fun n => ↑n) n).toNat = n induction' n with n hnzero⊢ ((fun n => ↑n) 0).toNat = 0succn:ℕhn:((fun n => ↑n) n).toNat = n⊢ ((fun n => ↑n) (n + 1)).toNat = n + 1 .zero⊢ ((fun n => ↑n) 0).toNat = 0 rflAll goals completed! 🐙 simp [←succ_eq_add_one]succn:ℕhn:((fun n => ↑n) n).toNat = n⊢ (↑n).toNat = n exact hnAll goals completed! 🐙abbrev declaration uses 'sorry'Chapter2.Nat.equivNat_order : Chapter2.Nat ≃o ℕ where toEquiv := Chapter2.Nat.equivNat map_rel_iff' := by⊢ ∀ {a b : Nat}, equivNat a ≤ equivNat b ↔ a ≤ b intro n mn:Natm:Nat⊢ equivNat n ≤ equivNat m ↔ n ≤ m simp [equivNat]n:Natm:Nat⊢ n.toNat ≤ m.toNat ↔ n ≤ m sorryAll goals completed! 🐙abbrev declaration uses 'sorry'declaration uses 'sorry'Chapter2.Nat.equivNat_ring : Chapter2.Nat ≃+* ℕ where toEquiv := Chapter2.Nat.equivNat map_add' := by⊢ ∀ (x y : Nat), equivNat.toFun (x + y) = equivNat.toFun x + equivNat.toFun y intro n mn:Natm:Nat⊢ equivNat.toFun (n + m) = equivNat.toFun n + equivNat.toFun m simp [equivNat]n:Natm:Nat⊢ (n + m).toNat = n.toNat + m.toNat sorryAll goals completed! 🐙 map_mul' := by⊢ ∀ (x y : Nat), equivNat.toFun (x * y) = equivNat.toFun x * equivNat.toFun y intro n mn:Natm:Nat⊢ equivNat.toFun (n * m) = equivNat.toFun n * equivNat.toFun m simp [equivNat]n:Natm:Nat⊢ (n * m).toNat = n.toNat * m.toNat sorryAll goals completed! 🐙lemma declaration uses 'sorry'Chapter2.Nat.pow_eq_pow (n m : Chapter2.Nat) : n.toNat ^ m.toNat = n^m := byn:Natm:Nat⊢ ↑n.toNat ^ m.toNat = n ^ m sorryAll goals completed! 🐙

The Peano axioms for an abstract type Nat

@[ext] class PeanoAxioms where Nat : Type zero : Nat -- Axiom 2.1 succ : Nat → Nat -- Axiom 2.2 succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3 succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4 induction : ∀ (P : Nat → Prop), P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5namespace PeanoAxioms

The Chapter 2 natural numbers obey the Peano axioms.

def Chapter2.Nat : PeanoAxioms where Nat := _root_.Chapter2.Nat zero := Chapter2.Nat.zero succ := Chapter2.Nat.succ succ_ne := Chapter2.Nat.succ_ne succ_cancel := Chapter2.Nat.succ_cancel induction := Chapter2.Nat.induction

The Mathlib natural numbers obey the Peano axioms.

def Mathlib.Nat : PeanoAxioms where Nat := ℕ zero := 0 succ := Nat.succ succ_ne := Nat.succ_ne_zero succ_cancel := Nat.succ_inj.mp induction _ := Nat.rec

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

abbrev natCast (P : PeanoAxioms) : ℕ → P.Nat := fun n ↦ match n with | Nat.zero => P.zero | Nat.succ n => P.succ (natCast P n)theorem declaration uses 'sorry'natCast_injective (P : PeanoAxioms) : Function.Injective P.natCast := byP:PeanoAxioms⊢ Function.Injective P.natCast sorryAll goals completed! 🐙theorem declaration uses 'sorry'natCast_surjective (P : PeanoAxioms) : Function.Surjective P.natCast := byP:PeanoAxioms⊢ Function.Surjective P.natCast sorryAll goals completed! 🐙

The notion of an equivalence between two structures obeying the Peano axioms

class Equiv (P Q : PeanoAxioms) where 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)abbrev declaration uses 'sorry'declaration uses 'sorry'Equiv.symm (equiv : Equiv P Q) : Equiv Q P where equiv := equiv.equiv.symm equiv_zero := byP:PeanoAxiomsQ:PeanoAxiomsequiv:P.Equiv Q⊢ PeanoAxioms.Equiv.equiv.symm zero = zero sorryAll goals completed! 🐙 equiv_succ n := byP:PeanoAxiomsQ:PeanoAxiomsequiv:P.Equiv Qn:Nat⊢ PeanoAxioms.Equiv.equiv.symm (succ n) = succ (PeanoAxioms.Equiv.equiv.symm n) sorryAll goals completed! 🐙abbrev declaration uses 'sorry'declaration uses 'sorry'Equiv.trans (equiv1 : Equiv P Q) (equiv2 : Equiv Q R) : Equiv P R where equiv := equiv1.equiv.trans equiv2.equiv equiv_zero := byP:PeanoAxiomsQ:PeanoAxiomsR:PeanoAxiomsequiv1:P.Equiv Qequiv2:Q.Equiv R⊢ (equiv.trans equiv) zero = zero sorryAll goals completed! 🐙 equiv_succ n := byP:PeanoAxiomsQ:PeanoAxiomsR:PeanoAxiomsequiv1:P.Equiv Qequiv2:Q.Equiv Rn:Nat⊢ (equiv.trans equiv) (succ n) = succ ((equiv.trans equiv) n) sorryAll goals completed! 🐙abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Equiv.fromNat (P : PeanoAxioms) : Equiv Mathlib.Nat P where equiv := { toFun := P.natCast invFun := byP:PeanoAxioms⊢ Nat → Nat sorryAll goals completed! 🐙 left_inv := byP:PeanoAxioms⊢ Function.LeftInverse sorry P.natCast sorryAll goals completed! 🐙 right_inv := byP:PeanoAxioms⊢ Function.RightInverse sorry P.natCast sorryAll goals completed! 🐙 } equiv_zero := byP:PeanoAxioms⊢ { toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ } zero = zero sorryAll goals completed! 🐙 equiv_succ n := byP:PeanoAxiomsn:Nat⊢ { toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ } (succ n) = succ ({ toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ } n) sorryAll goals completed! 🐙abbrev declaration uses 'sorry'Equiv.mk' (P Q : PeanoAxioms) : Equiv P Q := byP:PeanoAxiomsQ:PeanoAxioms⊢ P.Equiv Q sorryAll goals completed! 🐙theorem declaration uses 'sorry'Equiv.uniq {P Q : PeanoAxioms} (equiv1 equiv2 : PeanoAxioms.Equiv P Q) : equiv1 = equiv2 := byP:PeanoAxiomsQ:PeanoAxiomsequiv1:P.Equiv Qequiv2:P.Equiv Q⊢ equiv1 = equiv2 sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'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, a (P.succ n) = f n (a n) := byP:PeanoAxiomsf:Nat → Nat → Natc:Nat⊢ ∃! a, a zero = c ∧ ∀ (n : Nat), a (succ n) = f n (a n) sorryAll goals completed! 🐙end PeanoAxioms