Еквівалентність натуральних чисел

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

У цьому (технічному) епілозі ми показуємо, що натуральні числа 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 натуральних чисел, яка була індуктивного типу, і використовували цей індуктивний тип для побудови рекурсора. Тут ми наводимо кілька вправ, щоб показати, як можна виконати ті ж завдання безпосередньо з аксіом Пеано, не знаючи конкретної реалізації натуральних чисел.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[ext]
structure 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 := 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)

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

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

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

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

Поняття еквівалентності між двома структурами, що задовольняють аксіоми Пеано. Символ є псевдонімом для класу PeanoAxioms.Equiv (P Q : PeanoAxioms) : TypeEquiv у Mathlib; наприклад, Unknown identifier `P.Nat`sorry ≃ sorry : Sort (max (max 1 u_1) u_2)P.Nat ≃ Unknown identifier `Q.Nat`Q.Nat є псевдонімом для 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)

Ця вправа вимагатиме застосування API Mathlib для класу PeanoAxioms.Equiv (P Q : PeanoAxioms) : TypeEquiv. Деякі частини цього API можна викликати автоматично за допомогою тактики Unknown identifier `simp`simp.

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

Корисні інструменти Mathlib для інверсії бієкцій включають Function.surjInv.{u, v} {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β) : αFunction.surjInv та 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! 🐙

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

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

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

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