Equivalence of naturals

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 : TypeChapter2.Nat are isomorphic in various senses to the standard natural numbers ℕ : Typeℕ.

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

Filling the sorries here requires both the Chapter2.Nat API and the Mathlib API for the standard natural numbers ℕ : Typeℕ. 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 : TypeChapter2.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)

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

abbrev Chapter2.Nat.toNat (n : Chapter2.Nat) : ℕ := match n with
  | zero => 0
  | succ n' => n'.toNat + 1

lemma Chapter2.Nat.zero_toNat : (0 : Chapter2.Nat).toNat = 0 := rfllemma Chapter2.Nat.succ_toNat (n : Chapter2.Nat) : (n++).toNat = n.toNat + 1 := rfl

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.

abbrev Chapter2.Nat.equivNat : Chapter2.Nat ≃ ℕ where
  toFun := 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++; rflsuccn:Nathn:(fun n => ↑n) n.toNat = n⊢ (fun n => ↑n) n++.toNat = n++
    simp [hn]succn:Nathn:(fun n => ↑n) n.toNat = n⊢ n + 1 = n++
    rw [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; rflsuccn:ℕhn:((fun n => ↑n) n).toNat = n⊢ ((fun n => ↑n) (n + 1)).toNat = n + 1
    simp [←succ_eq_add_one, hn]All goals completed! 🐙

The conversion preserves addition.

abbrev declaration uses 'sorry'Chapter2.Nat.map_add : ∀ (n m : Nat), (n + m).toNat = n.toNat + m.toNat := by⊢ ∀ (n m : Nat), (n + m).toNat = n.toNat + m.toNat
  intro n mn:Natm:Nat⊢ (n + m).toNat = n.toNat + m.toNat
  induction' n with n hnzerom:Nat⊢ (zero + m).toNat = zero.toNat + m.toNatsuccm:Natn:Nathn:(n + m).toNat = n.toNat + m.toNat⊢ (n++ + m).toNat = n++.toNat + m.toNat
  ·zerom:Nat⊢ (zero + m).toNat = zero.toNat + m.toNat rw [show zero = 0 from rfl, zero_add, _root_.Nat.zero_add]All goals completed! 🐙
  sorryAll goals completed! 🐙

The conversion preserves multiplication.

abbrev declaration uses 'sorry'Chapter2.Nat.map_mul : ∀ (n m : Nat), (n * m).toNat = n.toNat * m.toNat := by⊢ ∀ (n m : Nat), (n * m).toNat = n.toNat * m.toNat
  intro n mn:Natm:Nat⊢ (n * m).toNat = n.toNat * m.toNat
  sorryAll goals completed! 🐙

The conversion preserves order.

abbrev declaration uses 'sorry'Chapter2.Nat.map_le_map_iff : ∀ {n m : Nat}, n.toNat ≤ m.toNat ↔ n ≤ m := by⊢ ∀ {n m : Nat}, n.toNat ≤ m.toNat ↔ n ≤ m
  intro n mn:Natm:Nat⊢ n.toNat ≤ m.toNat ↔ n ≤ m
  sorryAll goals completed! 🐙

abbrev Chapter2.Nat.equivNat_ordered_ring : Chapter2.Nat ≃+*o ℕ where
  toEquiv := equivNat
  map_add' := map_add
  map_mul' := map_mul
  map_le_map_iff' := map_le_map_iff

The conversion preserves exponentiation.

lemma declaration uses 'sorry'Chapter2.Nat.pow_eq_pow (n m : Chapter2.Nat) :
    n.toNat ^ m.toNat = (n^m).toNat := byn:Natm:Nat⊢ n.toNat ^ m.toNat = (n ^ m).toNat
  sorryAll goals completed! 🐙

The Peano axioms for an abstract type Nat : TypeNat

@[ext]
structure 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.5

namespace PeanoAxioms

The Chapter 2 natural numbers obey the Peano axioms.

def Chapter2_Nat : PeanoAxioms where
  Nat := 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)

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

theorem declaration uses 'sorry'natCast_injective (P : PeanoAxioms) : Function.Injective P.natCast  := byP:PeanoAxioms⊢ Function.Injective P.natCast
  sorryAll goals completed! 🐙

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

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. The symbol is an alias for Mathlib's PeanoAxioms.Equiv (P Q : PeanoAxioms) : TypeEquiv class; for instance Unknown identifier `P.Nat`sorry ≃ sorry : Sort (max (max 1 u_1) u_2)P.Nat ≃ Unknown identifier `Q.Nat`Q.Nat is an alias for sorry ≃ sorry : Sort (max (max 1 u_1) u_2)_root_.Equiv Unknown identifier `P.Nat`P.Nat Unknown identifier `Q.Nat`Q.Nat.

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)

This exercise will require application of Mathlib's API for the PeanoAxioms.Equiv (P Q : PeanoAxioms) : TypeEquiv class. Some of this API can be invoked automatically via the Unknown identifier `simp`simp tactic.

abbrev declaration uses 'sorry'declaration uses 'sorry'Equiv.symm {P Q: PeanoAxioms} (equiv : Equiv P Q) : Equiv Q P where
  equiv := equiv.equiv.symm
  equiv_zero := byP:PeanoAxiomsQ:PeanoAxiomsequiv:P.Equiv Q⊢ Equiv.equiv.symm Q.zero = P.zero sorryAll goals completed! 🐙
  equiv_succ n := byP:PeanoAxiomsQ:PeanoAxiomsequiv:P.Equiv Qn:Q.Nat⊢ Equiv.equiv.symm (Q.succ n) = P.succ (Equiv.equiv.symm n) sorryAll goals completed! 🐙

abbrev declaration uses 'sorry'declaration uses 'sorry'Equiv.trans {P Q R: PeanoAxioms} (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) P.zero = R.zero sorryAll goals completed! 🐙
  equiv_succ n := byP:PeanoAxiomsQ:PeanoAxiomsR:PeanoAxiomsequiv1:P.Equiv Qequiv2:Q.Equiv Rn:P.Nat⊢ (equiv.trans equiv) (P.succ n) = R.succ ((equiv.trans equiv) n) sorryAll goals completed! 🐙

Useful Mathlib tools for inverting bijections include Function.surjInv.{u, v} {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β) : αFunction.surjInv and Function.invFun.{u, u_3} {α : Sort u} {β : Sort u_3} [Nonempty α] (f : α → β) : β → αFunction.invFun.

noncomputable 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⊢ P.Nat → Mathlib_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 := ⋯ } Mathlib_Nat.zero = P.zero sorryAll goals completed! 🐙
  equiv_succ n := byP:PeanoAxiomsn:Mathlib_Nat.Nat⊢ { toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ } (Mathlib_Nat.succ n) =
  P.succ ({ toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ } n) sorryAll goals completed! 🐙

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

noncomputable abbrev declaration uses 'sorry'Equiv.mk' (P Q : PeanoAxioms) : Equiv P Q := byP:PeanoAxiomsQ:PeanoAxioms⊢ P.Equiv Q sorryAll goals completed! 🐙

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

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
  obtain ⟨equiv1, equiv_zero1, equiv_succ1⟩ := equiv1mkP:PeanoAxiomsQ:PeanoAxiomsequiv2:P.Equiv Qequiv1:P.Nat ≃ Q.Natequiv_zero1:equiv1 P.zero = Q.zeroequiv_succ1:∀ (n : P.Nat), equiv1 (P.succ n) = Q.succ (equiv1 n)⊢ { equiv := equiv1, equiv_zero := equiv_zero1, equiv_succ := equiv_succ1 } = equiv2
  obtain ⟨equiv2, equiv_zero2, equiv_succ2⟩ := equiv2mk.mkP:PeanoAxiomsQ:PeanoAxiomsequiv1:P.Nat ≃ Q.Natequiv_zero1:equiv1 P.zero = Q.zeroequiv_succ1:∀ (n : P.Nat), equiv1 (P.succ n) = Q.succ (equiv1 n)equiv2:P.Nat ≃ Q.Natequiv_zero2:equiv2 P.zero = Q.zeroequiv_succ2:∀ (n : P.Nat), equiv2 (P.succ n) = Q.succ (equiv2 n)⊢ { equiv := equiv1, equiv_zero := equiv_zero1, equiv_succ := equiv_succ1 } =
  { equiv := equiv2, equiv_zero := equiv_zero2, equiv_succ := equiv_succ2 }
  congrmk.mk.e_equivP:PeanoAxiomsQ:PeanoAxiomsequiv1:P.Nat ≃ Q.Natequiv_zero1:equiv1 P.zero = Q.zeroequiv_succ1:∀ (n : P.Nat), equiv1 (P.succ n) = Q.succ (equiv1 n)equiv2:P.Nat ≃ Q.Natequiv_zero2:equiv2 P.zero = Q.zeroequiv_succ2:∀ (n : P.Nat), equiv2 (P.succ n) = Q.succ (equiv2 n)⊢ equiv1 = equiv2
  ext nmk.mk.e_equiv.HP:PeanoAxiomsQ:PeanoAxiomsequiv1:P.Nat ≃ Q.Natequiv_zero1:equiv1 P.zero = Q.zeroequiv_succ1:∀ (n : P.Nat), equiv1 (P.succ n) = Q.succ (equiv1 n)equiv2:P.Nat ≃ Q.Natequiv_zero2:equiv2 P.zero = Q.zeroequiv_succ2:∀ (n : P.Nat), equiv2 (P.succ n) = Q.succ (equiv2 n)n:P.Nat⊢ equiv1 n = equiv2 n
  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:P.Nat → P.Nat → P.Natc:P.Nat⊢ ∃! a, a P.zero = c ∧ ∀ (n : P.Nat), a (P.succ n) = f n (a n)
  sorryAll goals completed! 🐙

end PeanoAxioms