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

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

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

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

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

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

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++
    .zero⊢ (fun n => ↑n) zero.toNat = zero rflAll goals completed! 🐙
    simp [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'declaration uses 'sorry'declaration uses 'sorry'Chapter2.Nat.equivNat_ordered_ring : Chapter2.Nat ≃+*o ℕ where
  toEquiv := 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! 🐙
  map_le_map_iff' := by⊢ ∀ {a b : Nat}, equivNat.toFun a ≤ equivNat.toFun b ↔ a ≤ b 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! 🐙

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

@[ext]
class PeanoAxioms where
  Nat : Type
  zero : Nat -- Аксіома 2.1
  succ : Nat → Nat -- Аксіома 2.2
  succ_ne : ∀ n : Nat, succ n ≠ zero -- Аксіома 2.3
  succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Аксіома 2.4
  induction : ∀ (P : Nat → Prop),
    P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Аксіома 2.5

namespace PeanoAxioms

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

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

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

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

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

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! 🐙

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

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! 🐙

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

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⊢ 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! 🐙

noncomputable 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! 🐙

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

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