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

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

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

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

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

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

inductive Chapter2.Nat : Type

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

• zero : Nat
• succ : Nat → Nat

instance Chapter2.instReprNat : Repr Nat

Equations

• Chapter2.instReprNat = { reprPrec := Chapter2.reprNat✝ }

instance Chapter2.instDecidableEqNat : DecidableEq Nat

Equations

• Chapter2.instDecidableEqNat = Chapter2.decEqNat✝

instance Chapter2.Nat.instZero : Zero Nat

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

Equations

• Chapter2.Nat.instZero = { zero := Chapter2.Nat.zero }

def Chapter2.«term_++» : Lean.TrailingParserDescr

Аксіома 2.2 (Наступник натурального числа також є натуральним числом)

Equations

• Chapter2.«term_++» = Lean.ParserDescr.trailingNode `Chapter2.«term_++» 100 100 (Lean.ParserDescr.symbol "++")

instance Chapter2.Nat.instOfNat {n : ℕ} : OfNat Nat n

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

Equations

• Chapter2.Nat.instOfNat = { ofNat := Nat.rec 0 (fun (x : ℕ) (n : Chapter2.Nat) => n++) n }

instance Chapter2.Nat.instOne : One Nat

Equations

• Chapter2.Nat.instOne = { one := 1 }

theorem Chapter2.Nat.zero_succ : 0++ = 1

theorem Chapter2.Nat.one_succ : 1++ = 2

theorem Chapter2.Nat.two_succ : 2++ = 3

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

theorem Chapter2.Nat.succ_ne (n : Nat) : n++ ≠ 0

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

theorem Chapter2.Nat.four_ne : 4 ≠ 0

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

theorem Chapter2.Nat.succ_cancel {n m : Nat} (hnm : n++ = m++) : n = m

Аксіома 2.4 (Різні натуральні числа мають різних наступників). Порівняйте із Mathlib-овським Nat.succ_inj.

theorem Chapter2.Nat.succ_ne_succ (n m : Nat) : n ≠ m → n++ ≠ m++

Аксіома 2.4 (Різні натуральні числа мають різних наступників). Порівняйте із Mathlib-овським Nat.succ_ne_succ.

theorem Chapter2.Nat.six_ne_two : 6 ≠ 2

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

theorem Chapter2.Nat.six_ne_two' : 6 ≠ 2

Ви також можете довести такого типу результат використовуючи тактику decide

theorem Chapter2.Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ (n : Nat), P n → P (n++)) (n : Nat) : P n

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

@[reducible, inline]

abbrev Chapter2.Nat.recurse (f : Nat → Nat → Nat) (c : Nat) : Nat → Nat

Рекурсія. Аналогічно до вбудованого методу Mathlib Nat.rec ассоційованого із натуральними числами Mathlib

Equations

• Chapter2.Nat.recurse f c Chapter2.Nat.zero = c
• Chapter2.Nat.recurse f c (a++) = f a (Chapter2.Nat.recurse f c a)

theorem Chapter2.Nat.recurse_zero (f : Nat → Nat → Nat) (c : Nat) : recurse f c 0 = c

Твердження 2.1.16 (рекурсивне визначення). Порівняйте із Mathlib-овським Nat.rec_zero.

theorem Chapter2.Nat.recurse_succ (f : Nat → Nat → Nat) (c n : Nat) : recurse f c (n++) = f n (recurse f c n)

Твердження 2.1.16 (рекурсивне визначення). Порівняйте із Mathlib-овським Nat.rec_add_one.

theorem Chapter2.Nat.eq_recurse (f : Nat → Nat → Nat) (c : Nat) (a : Nat → Nat) : (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) ↔ a = recurse f c

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

theorem Chapter2.Nat.recurse_uniq (f : Nat → Nat → Nat) (c : Nat) : ∃! a : Nat → Nat, a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)

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