Аналіз I, Глава 2.1

Цей файл є перекладом Глави 2.1 Аналізу I до Lean 4. Вся нумерація посилається на оригінальний текст.

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Визанчення натуральних чисел "Розділу 2", Chapter2.Nat : TypeChapter2.Nat, абревіюється як Nat : TypeNat в середині простору імен unknown identifier 'Chapter2'Chapter2. (У книзі натуральні числа трактуються суто аксіоматично, як тип, що підпорядковується аксіомам Пеано; але тут ми використовуємо переваги рідних для Lean індуктивних типів, щоб явно побудувати версію натуральних чисел, які підпорядковуються цим аксіомам. Можна також діяти більш аксіоматично, як це зроблено в розділі 3 для теорії множин, але ми залишаємо це як вправу для читача..)
Встановлення аксіом Пеано для Chapter2.Nat : TypeChapter2.Nat
Рекурсивні визначення для Chapter2.Nat : TypeChapter2.Nat

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

namespace Chapter2

Припущення 2.6 (Існування натуральних чисел). Тут ми будемо використовувати явне побудування натуральних чисел (використовуючи індуктивний тип). Для більш аксіоматичного підходу, дивіться епілог до цього розділу

inductive Nat where
| zero : Nat
| succ : Nat → Nat
deriving Repr, DecidableEq  -- це дозволяє `decide` працювати із `Nat`

Аксіома 2.1 (0 це натуральне число)

instance Nat.instZero : Zero Nat := ⟨ zero ⟩

0 : Nat#check (0:Nat)

0 : Nat

/-- Аксіома 2.2 (Наступник натурального числа також є натуральним числом) -/
postfix:100 "++" => Nat.succ

fun n => n++ : Nat → Nat#check (fun n ↦ n++)

fun n => n++ : Nat → Nat

Визначення 2.1.3 (Визначення чисел 0, 1, 2, etc.). Примітка: щоб уникнути неоднозначності, вам може знадобитися явна конвертація як наприклад (0:Nat), (1:Nat), і т.д. щоб посилатися на версію натуральних чисел із цього розділу.

instance Nat.instOfNat {n:_root_.Nat} : OfNat Nat n where
  ofNat := _root_.Nat.rec 0 (fun _ n ↦ n++) n

instance Nat.instOne : One Nat := ⟨ 1 ⟩lemma Nat.zero_succ : 0++ = 1 := by⊢ 0++ = 1 rflAll goals completed! 🐙1 : Nat#check (1:Nat)

1 : Nat

lemma Nat.one_succ : 1++ = 2 := by⊢ 1++ = 2 rflAll goals completed! 🐙2 : Nat#check (2:Nat)

2 : Nat

Твердження 2.1.4 (3 є натуральним числом)

lemma Nat.two_succ : 2++ = 3 := by⊢ 2++ = 3 rflAll goals completed! 🐙

3 : Nat#check (3:Nat)

3 : Nat

Аксіома 2.3 (0 не є наступником ніякого натурального числа). Порівняйте із Mathlib-овським Nat.succ_ne_zero (n : ℕ) : n.succ ≠ 0Nat.succ_ne_zero.

theorem Nat.succ_ne (n:Nat) : n++ ≠ 0 := byn:Nat⊢ n++ ≠ 0
  by_contra hn:Nath:n++ = 0⊢ False
  simp only [reduceCtorEq] at hAll goals completed! 🐙

Твердження 2.1.6 (4 не дорівнює нулю)

theorem Nat.four_ne : (4:Nat) ≠ 0 := by⊢ 4 ≠ 0
  -- За визначенням, 4 = 3++.
  change 3++ ≠ 0⊢ 3++ ≠ 0
  -- За аксіомою 2.3, 3++ не є нулем.
  exact succ_ne _All goals completed! 🐙

Аксіома 2.4 (Різні натуральні числа мають різних наступників). Порівняйте із Mathlib-овським Nat.succ_inj {a b : ℕ} : a.succ = b.succ ↔ a = bNat.succ_inj.

theorem Nat.succ_cancel {n m:Nat} (hnm: n++ = m++) : n = m := byn:Natm:Nathnm:n++ = m++⊢ n = m
  rwa [succ.injEq]n:Natm:Nathnm:n = m⊢ n = m at hnm

Аксіома 2.4 (Різні натуральні числа мають різних наступників). Порівняйте із Mathlib-овським Nat.succ_ne_succ {m n : ℕ} : m.succ ≠ n.succ ↔ m ≠ nNat.succ_ne_succ.

theorem Nat.succ_ne_succ (n m:Nat) : n ≠ m → n++ ≠ m++ := byn:Natm:Nat⊢ n ≠ m → n++ ≠ m++
  intro hn:Natm:Nath:n ≠ m⊢ n++ ≠ m++
  contrapose! hn:Natm:Nath:n++ = m++⊢ n = m
  exact succ_cancel hAll goals completed! 🐙

Твердження 2.1.8 (6 не дорівнює 2)

theorem Nat.six_ne_two : (6:Nat) ≠ 2 := by⊢ 6 ≠ 2
-- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  by_contra hh:6 = 2⊢ False
  change 5++ = 1++ at hh:5++ = 1++⊢ False
  replace h := succ_cancel hh:5 = 1⊢ False
  change 4++ = 0++ at hh:4++ = 0++⊢ False
  replace h := succ_cancel hh:4 = 0⊢ False
  have := four_neh:4 = 0this:4 ≠ 0⊢ False
  contradictionAll goals completed! 🐙

Ви також можете довести такого типу результат використовуючи тактику Decidable.decide (p : Prop) [h : Decidable p] : Booldecide

theorem Nat.six_ne_two' : (6:Nat) ≠ 2 := by⊢ 6 ≠ 2
  decideAll goals completed! 🐙

Аксіома 2.5 (принцип математичної індукції). Тактика unknown identifier 'induction'induction (або unknown identifier 'induction''induction') в Mathlib служить заміною для цієї аксіоми.

theorem Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ n, P n → P (n++)) :
    ∀ n, P n := byP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)⊢ ∀ (n : Nat), P n
  intro nP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)n:Nat⊢ P n
  induction n with
  | zero =>zeroP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)⊢ P zero exact hbaseAll goals completed! 🐙
  | succ n ih =>succP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)n:Natih:P n⊢ P (n++) exact hind _ ihAll goals completed! 🐙

Рекурсія. Аналогічно до вбудованого методу Mathlib Nat.rec.{u} {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) (t : ℕ) : motive tNat.rec ассоційованого із натуральними числами Mathlib

abbrev Nat.recurse (f: Nat → Nat → Nat) (c: Nat) : Nat → Nat := fun n ↦ match n with
| 0 => c
| n++ => f n (recurse f c n)

Твердження 2.1.16 (рекурсивне визначення). Порівняйте із Mathlib-овським Nat.rec_zero.{u_1} {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) : Nat.rec h0 h 0 = h0Nat.rec_zero.

theorem Nat.recurse_zero (f: Nat → Nat → Nat) (c: Nat) : Nat.recurse f c 0 = c := byf:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c rflAll goals completed! 🐙

Твердження 2.1.16 (рекурсивне визначення). Порівняйте із Mathlib-овським Nat.rec_add_one.{u_1} {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ) : Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)Nat.rec_add_one.

theorem Nat.recurse_succ (f: Nat → Nat → Nat) (c: Nat) (n: Nat) :
    recurse f c (n++) = f n (recurse f c n) := byf:Nat → Nat → Natc:Natn:Nat⊢ recurse f c (n++) = f n (recurse f c n) rflAll goals completed! 🐙

Твердження 2.1.16 (рекурсивне визначення).

theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) :
    (a 0 = c ∧ ∀ n, a (n++) = f n (a n)) ↔ a = recurse f c := byf:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) ↔ a = recurse f c
  constructormpf:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) → a = recurse f cmprf:Nat → Nat → Natc:Nata:Nat → Nat⊢ a = recurse f c → a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)
  .mpf:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) → a = recurse f c intro ⟨ h0, hsucc ⟩mpf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ a = recurse f c
    -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
    apply funextmp.hf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ ∀ (x : Nat), a x = recurse f c x; apply inductionmp.h.hbasef:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ a 0 = recurse f c 0mp.h.hindf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ ∀ (n : Nat), a n = recurse f c n → a (n++) = recurse f c (n++)
    .mp.h.hbasef:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ a 0 = recurse f c 0 exact h0All goals completed! 🐙
    intro n hnmp.h.hindf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)n:Nathn:a n = recurse f c n⊢ a (n++) = recurse f c (n++)
    rw [hsucc n, recurse_succ, hn]All goals completed! 🐙
  intro hmprf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)
  rw [h]mprf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ recurse f c 0 = c ∧ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n)
  constructormpr.leftf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ recurse f c 0 = cmpr.rightf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n)
  .mpr.leftf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ recurse f c 0 = c exact recurse_zero _ _All goals completed! 🐙
  exact recurse_succ _ _All goals completed! 🐙

Твердження 2.1.16 (рекурсивне визначення).

theorem Nat.recurse_uniq (f: Nat → Nat → Nat) (c: Nat) :
    ∃! (a: Nat → Nat), a 0 = c ∧ ∀ n, a (n++) = f n (a n) := byf:Nat → Nat → Natc:Nat⊢ ∃! a, a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)
  apply ExistsUnique.intro (recurse f c)h₁f:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c ∧ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n)h₂f:Nat → Nat → Natc:Nat⊢ ∀ (y : Nat → Nat), (y 0 = c ∧ ∀ (n : Nat), y (n++) = f n (y n)) → y = recurse f c
  .h₁f:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c ∧ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n) constructorh₁.leftf:Nat → Nat → Natc:Nat⊢ recurse f c 0 = ch₁.rightf:Nat → Nat → Natc:Nat⊢ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n)
    .h₁.leftf:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c exact recurse_zero _ _All goals completed! 🐙
    .h₁.rightf:Nat → Nat → Natc:Nat⊢ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n) exact recurse_succ _ _All goals completed! 🐙
  intro ah₂f:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) → a = recurse f c
  exact (eq_recurse _ _ a).mpAll goals completed! 🐙

end Chapter2