Аналіз I, Розділ 2, Епілог: Ізоморфізм із натуральними числами Mathlib

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

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

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

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

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

• (Додайте підказку тут)

@[reducible, inline]

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

Перетворення натурального числа з Розділу 2 на натуральне число Mathlib.

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

Перетворення є бієкцією. Тут ми використовуємо наявну можливість (з Розділу 2.1) для відображення натуральних чисел Mathlib на натуральні числа Розділу 2.

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

Перетворення зберігає операцію додавання.

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Перетворення зберігає операцію множення.

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Перетворення зберігає порядок.

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

Перетворення зберігає піднесення до степеня.

structure PeanoAxioms : Type 1

Аксіоми Пеано для абстрактного типу 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

Натуральні числа розділу 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_1, induction := ⋯ }

@[reducible, inline]

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

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

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

Доведення можна почати тут з unfold Function.Injective, хоча це не є строго обов’язковим.

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

Доведення можна почати тут з unfold Function.Surjective, хоча це не є строго обов’язковим.

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

Поняття еквівалентності між двома структурами, що задовольняють аксіоми Пеано. Символ ≃ є псевдонімом для класу Equiv у Mathlib; наприклад, P.Nat ≃ Q.Nat є псевдонімом для _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

Ця вправа вимагатиме застосування API Mathlib для класу Equiv. Деякі частини цього API можна викликати автоматично за допомогою тактики simp.

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

Ця вправа вимагатиме застосування API Mathlib для класу Equiv. Деякі частини цього API можна викликати автоматично за допомогою тактики simp.

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

Корисні інструменти Mathlib для інверсії бієкцій включають Function.surjInv та 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

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

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 : 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)

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