@[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