Аналіз I, Розділ 2, Епілог

У цьому (технічному) епілозі ми показуємо, що натуральні числа Chapter2.Nat з "Розділу 2" ізоморфні стандартним натуральним числам ℕ у різних типових сенсах.

З цього моменту Chapter2.Nat буде застарілим типом, і замість нього ми використовуватимемо стандартні натуральні числа ℕ. Зокрема, для всіх наступних розділів слід використовувати повний API Mathlib для ℕ замість API Chapter2.Nat.

Для заповнення цих вибачень потрібні як Chapter2.Nat API, так і Mathlib API для стандартних натуральних чисел ℕ. Таким чином, вони є чудовими вправами для підготовки до вищезгаданого переходу.

У другій половині цього розділу ми також наводимо повністю аксіоматичне трактування натуральних чисел за допомогою аксіом Пеано. Розгляд у попередніх трьох розділах був лише частково аксіоматичним, оскільки ми використовували специфічну конструкцію Chapter2.Nat натуральних чисел, яка була індуктивного типу, і використовували цей індуктивний тип для побудови рекурсора. Тут ми наводимо кілька вправ, щоб показати, як можна виконати ті ж завдання безпосередньо з аксіом Пеано, не знаючи конкретної реалізації натуральних чисел.

@[reducible, inline]

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

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 ≃ ℕ

Equations

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

@[reducible, inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

class PeanoAxioms : Type 1

Аксіоми Пеано для абстрактного типу Nat

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

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

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

def PeanoAxioms.Chapter2.Nat : PeanoAxioms

Натуральні числа розділу 2 дотримуються аксіом Пеано.

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

Натуральні числа Mathlib дотримуються аксіом Пеано.

Equations

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

@[reducible, inline]

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

Ви можете співставити натуральні числа Mathlib у іншу струкруту яка дотримується аксіом Пеано.

Equations

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

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

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

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

Поняття еквівалентності між двома структурами, що дотримуються аксіом Пеано

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

@[reducible, inline]

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

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

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

Примітка: Я підозрюю, що ця конструкція не є обчислювальною та вимагає класичної логіки.

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

Equations

• PeanoAxioms.Equiv.mk' P Q = sorry

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

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

Приклад результату: рекурсія коректно визначена на будь-якій структурі, що підпорядковується аксіомам Пеано.