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

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

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

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

Визначення додавання та порядку для натуральних чисел "Розділу 2", Chapter2.Nat : TypeChapter2.Nat
Встановлення основних властивостей додавання та порядку

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

namespace Chapter2

Визначення 2.2.1. (Додавання натуральних чисел. Порівняйте із Mathlib-овським Nat.add : ℕ → ℕ → ℕNat.add

abbrev Nat.add (n m : Nat) : Nat := Nat.recurse (fun _ sum ↦ sum++) m n

Цей екземпляр дозволить нотації використовуватися для додавання натуральних чисел.

instance Nat.instAdd : Add Nat where
  add := add

Порівняйте із Mathlib-овським Nat.zero_add (n : ℕ) : 0 + n = nNat.zero_add

@[simp]
theorem Nat.zero_add (m: Nat) : 0 + m = m := recurse_zero (fun _ sum ↦ sum++) _

Порівняйте із Mathlib-овським Nat.succ_add (n m : ℕ) : n.succ + m = (n + m).succNat.succ_add

theorem Nat.succ_add (n m: Nat) : n++ + m = (n+m)++ := byn:Natm:Nat⊢ n++ + m = (n + m)++ rflAll goals completed! 🐙

Порівняйте із Mathlib-овським Nat.one_add (n : ℕ) : 1 + n = n.succNat.one_add

theorem Nat.one_add (m:Nat) : 1 + m = m++ := bym:Nat⊢ 1 + m = m++
  rw [show 1 = 0++ from rfl, succ_add, zero_add]All goals completed! 🐙

theorem Nat.two_add (m:Nat) : 2 + m = (m++)++ := bym:Nat⊢ 2 + m = m++++
  rw [show 2 = 1++ from rfl, succ_add, one_add]All goals completed! 🐙

example : (2:Nat) + 3 = 5 := by⊢ 2 + 3 = 5
  rw [Nat.two_add, show 3++=4 from rfl, show 4++=5 from rfl]All goals completed! 🐙

-- сума двух натуральних чисел це також натуральне число
fun n m => n + m : Nat → Nat → Nat#check (fun (n m:Nat) ↦ n + m)

fun n m => n + m : Nat → Nat → Nat

Лема 2.2.2 (n + 0 = n). Порівняйте із Mathlib-овським Nat.add_zero (n : ℕ) : n + 0 = nNat.add_zero

@[simp]
lemma Nat.add_zero (n:Nat) : n + 0 = n := byn:Nat⊢ n + 0 = n
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert n⊢ ∀ (n : Nat), n + 0 = n; apply inductionhbase⊢ 0 + 0 = 0hind⊢ ∀ (n : Nat), n + 0 = n → n++ + 0 = n++
  .hbase⊢ 0 + 0 = 0 exact zero_add 0All goals completed! 🐙
  intro n ihhindn:Natih:n + 0 = n⊢ n++ + 0 = n++
  calc
    (n++) + 0 = (n + 0)++ := byn:Natih:n + 0 = n⊢ n++ + 0 = (n + 0)++ rflAll goals completed! 🐙
    _ = n++ := byn:Natih:n + 0 = n⊢ (n + 0)++ = n++ rw [ih]All goals completed! 🐙

Лема 2.2.3 (n+(m++) = (n+m)++). Порівняйте із Mathlib-овським Nat.add_succ (n m : ℕ) : n + m.succ = (n + m).succNat.add_succ

lemma Nat.add_succ (n m:Nat) : n + (m++) = (n + m)++ := byn:Natm:Nat⊢ n + m++ = (n + m)++
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert nm:Nat⊢ ∀ (n : Nat), n + m++ = (n + m)++; apply inductionhbasem:Nat⊢ 0 + m++ = (0 + m)++hindm:Nat⊢ ∀ (n : Nat), n + m++ = (n + m)++ → n++ + m++ = (n++ + m)++
  .hbasem:Nat⊢ 0 + m++ = (0 + m)++ rw [zero_add, zero_add]All goals completed! 🐙
  intro n ihhindm:Natn:Natih:n + m++ = (n + m)++⊢ n++ + m++ = (n++ + m)++
  rw [succ_add, ih]hindm:Natn:Natih:n + m++ = (n + m)++⊢ (n + m)++++ = (n++ + m)++
  rw [succ_add]All goals completed! 🐙

n++ = n + 1 (Чому?). Порівняйте із Mathlib-овським Nat.succ_eq_add_one (n : ℕ) : n.succ = n + 1Nat.succ_eq_add_one

theorem declaration uses 'sorry'Nat.succ_eq_add_one (n:Nat) : n++ = n + 1 := byn:Nat⊢ n++ = n + 1
  sorryAll goals completed! 🐙

Твердження 2.2.4 (Додавання комутативне). Порівняйте із Mathlib-овським Nat.add_comm (n m : ℕ) : n + m = m + nNat.add_comm

theorem Nat.add_comm (n m:Nat) : n + m = m + n := byn:Natm:Nat⊢ n + m = m + n
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert nm:Nat⊢ ∀ (n : Nat), n + m = m + n; apply inductionhbasem:Nat⊢ 0 + m = m + 0hindm:Nat⊢ ∀ (n : Nat), n + m = m + n → n++ + m = m + n++
  .hbasem:Nat⊢ 0 + m = m + 0 rw [zero_add, add_zero]All goals completed! 🐙
  intro n ihhindm:Natn:Natih:n + m = m + n⊢ n++ + m = m + n++
  rw [succ_add]hindm:Natn:Natih:n + m = m + n⊢ (n + m)++ = m + n++
  rw [add_succ, ih]All goals completed! 🐙

Твердження 2.2.5 (Додавання асоціативне) / Вправа 2.2.1 Порівняйте із Mathlib-овським Nat.add_assoc (n m k : ℕ) : n + m + k = n + (m + k)Nat.add_assoc

theorem declaration uses 'sorry'Nat.add_assoc (a b c:Nat) : (a + b) + c = a + (b + c) := bya:Natb:Natc:Nat⊢ a + b + c = a + (b + c)
  sorryAll goals completed! 🐙

Твердження 2.2.6 (Властивість скорочення) Порівняйте із Mathlib-овським Nat.add_left_cancel {n m k : ℕ} : n + m = n + k → m = kNat.add_left_cancel

theorem Nat.add_left_cancel (a b c:Nat) (habc: a + b = a + c) : b = c := bya:Natb:Natc:Nathabc:a + b = a + c⊢ b = c
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert ab:Natc:Nat⊢ ∀ (a : Nat), a + b = a + c → b = c; apply inductionhbaseb:Natc:Nat⊢ 0 + b = 0 + c → b = chindb:Natc:Nat⊢ ∀ (n : Nat), (n + b = n + c → b = c) → n++ + b = n++ + c → b = c
  .hbaseb:Natc:Nat⊢ 0 + b = 0 + c → b = c intro hbchbaseb:Natc:Nathbc:0 + b = 0 + c⊢ b = c
    rwa [zero_add, zero_add]hbaseb:Natc:Nathbc:b = c⊢ b = c at hbc
  intro a ihhindb:Natc:Nata:Natih:a + b = a + c → b = c⊢ a++ + b = a++ + c → b = c
  intro hbchindb:Natc:Nata:Natih:a + b = a + c → b = chbc:a++ + b = a++ + c⊢ b = c
  rw [succ_add, succ_add] at hbchindb:Natc:Nata:Natih:a + b = a + c → b = chbc:(a + b)++ = (a + c)++⊢ b = c
  replace hbc := succ_cancel hbchindb:Natc:Nata:Natih:a + b = a + c → b = chbc:a + b = a + c⊢ b = c
  exact ih hbcAll goals completed! 🐙

(Не із книги) Типу Nat можна дати структуру комутативного адітивного моноїда.

instance Nat.addCommMonoid : AddCommMonoid Nat where
  add_assoc := add_assoc
  add_comm := add_comm
  zero_add := zero_add
  add_zero := add_zero
  nsmul := nsmulRec

Визначення 2.2.7 (Додатні натуральні числе).

def Nat.isPos (n:Nat) : Prop := n ≠ 0

theorem Nat.isPos_iff (n:Nat) : n.isPos ↔ n ≠ 0 := byn:Nat⊢ n.isPos ↔ n ≠ 0 rflAll goals completed! 🐙

Твердження 2.2.8 (Додатне плюс натуральне число буде додатним). Порівняйте із Mathlib-овським Nat.add_pos_left {m : ℕ} (h : 0 < m) (n : ℕ) : 0 < m + nNat.add_pos_left

theorem Nat.add_pos_left {a:Nat} (b:Nat) (ha: a.isPos) : (a + b).isPos := bya:Natb:Natha:a.isPos⊢ (a + b).isPos
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert ba:Natha:a.isPos⊢ ∀ (b : Nat), (a + b).isPos; apply inductionhbasea:Natha:a.isPos⊢ (a + 0).isPoshinda:Natha:a.isPos⊢ ∀ (n : Nat), (a + n).isPos → (a + n++).isPos
  .hbasea:Natha:a.isPos⊢ (a + 0).isPos rwa [add_zero]hbasea:Natha:a.isPos⊢ a.isPos
  intro b habhinda:Natha:a.isPosb:Nathab:(a + b).isPos⊢ (a + b++).isPos
  rw [add_succ]hinda:Natha:a.isPosb:Nathab:(a + b).isPos⊢ (a + b)++.isPos
  have : (a+b)++ ≠ 0 := succ_ne _hinda:Natha:a.isPosb:Nathab:(a + b).isPosthis:(a + b)++ ≠ 0⊢ (a + b)++.isPos
  exact thisAll goals completed! 🐙

Порівняйте із Mathlib-овським Nat.add_pos_right {n : ℕ} (m : ℕ) (h : 0 < n) : 0 < m + nNat.add_pos_right

theorem Nat.add_pos_right {a:Nat} (b:Nat) (ha: a.isPos) : (b + a).isPos := bya:Natb:Natha:a.isPos⊢ (b + a).isPos
  rw [add_comm]a:Natb:Natha:a.isPos⊢ (a + b).isPos
  exact add_pos_left _ haAll goals completed! 🐙

Наслідок 2.2.9 (якщо сума дорівнює нулю, тоді доданки дорівнюють нулю). Порівняйте із Mathlib-овським Nat.add_eq_zero {m n : ℕ} : m + n = 0 ↔ m = 0 ∧ n = 0Nat.add_eq_zero

theorem Nat.add_eq_zero (a b:Nat) (hab: a + b = 0) : a = 0 ∧ b = 0 := bya:Natb:Nathab:a + b = 0⊢ a = 0 ∧ b = 0
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  by_contra ha:Natb:Nathab:a + b = 0h:¬(a = 0 ∧ b = 0)⊢ False
  simp only [not_and_or, ←ne_eq] at ha:Natb:Nathab:a + b = 0h:a ≠ 0 ∨ b ≠ 0⊢ False
  rcases h with ha | hbinla:Natb:Nathab:a + b = 0ha:a ≠ 0⊢ Falseinra:Natb:Nathab:a + b = 0hb:b ≠ 0⊢ False
  .inla:Natb:Nathab:a + b = 0ha:a ≠ 0⊢ False rw [← isPos_iff] at hainla:Natb:Nathab:a + b = 0ha:a.isPos⊢ False
    have : (a + b).isPos := add_pos_left _ hainla:Natb:Nathab:a + b = 0ha:a.isPosthis:(a + b).isPos⊢ False
    contradictionAll goals completed! 🐙
  rw [← isPos_iff] at hbinra:Natb:Nathab:a + b = 0hb:b.isPos⊢ False
  have : (a + b).isPos := add_pos_right _ hbinra:Natb:Nathab:a + b = 0hb:b.isPosthis:(a + b).isPos⊢ False
  contradictionAll goals completed! 🐙

/-
Наступне API для ∃! може бути корисним для наступної проблеми.  Також, тактика `obtain` корисна
для вилучення змінної предіката із кванторів існування; наприклад, `obtain ⟨ x, hx ⟩ := h`
вилучає змінну предіката `x` та доказ `hx : P x` властивості із гіпотези `h : ∃ x, P x`.
-/

existsUnique_of_exists_of_unique.{u_1} {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x)
  (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x#check existsUnique_of_exists_of_unique

existsUnique_of_exists_of_unique.{u_1} {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x)
  (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x

ExistsUnique.exists.{u_1} {α : Sort u_1} {p : α → Prop} : (∃! x, p x) → ∃ x, p x#check ExistsUnique.exists

ExistsUnique.exists.{u_1} {α : Sort u_1} {p : α → Prop} : (∃! x, p x) → ∃ x, p x

ExistsUnique.unique.{u_1} {α : Sort u_1} {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂#check ExistsUnique.unique

ExistsUnique.unique.{u_1} {α : Sort u_1} {p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂

Лема 2.2.10 (унікальний попередник) / Вправа 2.2.2

lemma declaration uses 'sorry'Nat.uniq_succ_eq (a:Nat) (ha: a.isPos) : ∃! b, b++ = a := bya:Natha:a.isPos⊢ ∃! b, b++ = a
  sorryAll goals completed! 🐙

Визначення 2.2.11 (Порядок натуральних чисел) Це визначає операцію на натуральних числах.

instance Nat.instLE : LE Nat where
  le n m := ∃ a:Nat, m = n + a

Визначення 2.2.11 (Порядок натуральних чисел) Це визначає операцію на натуральних числах.

instance Nat.instLT : LT Nat where
  lt n m := n ≤ m ∧ n ≠ m

lemma Nat.le_iff (n m:Nat) : n ≤ m ↔ ∃ a:Nat, m = n + a := byn:Natm:Nat⊢ n ≤ m ↔ ∃ a, m = n + a rflAll goals completed! 🐙

lemma Nat.lt_iff (n m:Nat) : n < m ↔ (∃ a:Nat, m = n + a) ∧ n ≠ m := byn:Natm:Nat⊢ n < m ↔ (∃ a, m = n + a) ∧ n ≠ m rflAll goals completed! 🐙

Порівняйте із Mathlib-овським ge_iff_le.{u_1} {α : Type u_1} [LE α] {x y : α} : x ≥ y ↔ y ≤ xge_iff_le

lemma Nat.ge_iff_le (n m:Nat) : n ≥ m ↔ m ≤ n := byn:Natm:Nat⊢ n ≥ m ↔ m ≤ n rflAll goals completed! 🐙

Порівняйте із Mathlib-овським gt_iff_lt.{u_1} {α : Type u_1} [LT α] {x y : α} : x > y ↔ y < xgt_iff_lt

lemma Nat.gt_iff_lt (n m:Nat) : n > m ↔ m < n := byn:Natm:Nat⊢ n > m ↔ m < n rflAll goals completed! 🐙

Порівняйте із Mathlib-овським Nat.le_of_lt {n m : ℕ} : n < m → n ≤ mNat.le_of_lt

lemma Nat.le_of_lt {n m:Nat} (hnm: n < m) : n ≤ m := hnm.1

Порівняйте із Mathlib-овським Nat.le_iff_lt_or_eq {n m : ℕ} : n ≤ m ↔ n < m ∨ n = mNat.le_iff_lt_or_eq

lemma Nat.le_iff_lt_or_eq (n m:Nat) : n ≤ m ↔ n < m ∨ n = m := byn:Natm:Nat⊢ n ≤ m ↔ n < m ∨ n = m
  rw [Nat.le_iff, Nat.lt_iff]n:Natm:Nat⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m
  by_cases h : n = mposn:Natm:Nath:n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = mnegn:Natm:Nath:¬n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m
  .posn:Natm:Nath:n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m simp [h]posn:Natm:Nath:n = m⊢ ∃ a, m = m + a
    use 0hn:Natm:Nath:n = m⊢ m = m + 0
    rw [add_zero]All goals completed! 🐙
  simp [h]All goals completed! 🐙

example : (8:Nat) > 5 := by⊢ 8 > 5
  rw [Nat.gt_iff_lt, Nat.lt_iff]⊢ (∃ a, 8 = 5 + a) ∧ 5 ≠ 8
  constructorleft⊢ ∃ a, 8 = 5 + aright⊢ 5 ≠ 8
  .left⊢ ∃ a, 8 = 5 + a have : (8:Nat) = 5 + 3 := by⊢ 8 > 5 rflAll goals completed! 🐙
    rw [this]leftthis:8 = 5 + 3⊢ ∃ a, 5 + 3 = 5 + a
    use 3All goals completed! 🐙
  decideAll goals completed! 🐙

Порівняйте із Mathlib-овським Nat.lt_succ_self (n : ℕ) : n < n.succNat.lt_succ_self

theorem declaration uses 'sorry'Nat.succ_gt_self (n:Nat) : n++ > n := byn:Nat⊢ n++ > n
  sorryAll goals completed! 🐙

Твердження 2.2.12 (Базові властивості порядку для натуральних чисел) / Вправа 2.2.3

(a) (Порядок рефлексівен). Порівняйте із Mathlib-овським Nat.le_refl (n : ℕ) : n ≤ nNat.le_refl

theorem declaration uses 'sorry'Nat.ge_refl (a:Nat) : a ≥ a := bya:Nat⊢ a ≥ a
  sorryAll goals completed! 🐙

(b) (Порядок транзітивен). Тут буде корисною тактика unknown identifier 'obtain'obtain. Порівняйте із Mathlib-овським Nat.le_trans {n m k : ℕ} : n ≤ m → m ≤ k → n ≤ kNat.le_trans

theorem declaration uses 'sorry'Nat.ge_trans {a b c:Nat} (hab: a ≥ b) (hbc: b ≥ c) : a ≥ c := bya:Natb:Natc:Nathab:a ≥ bhbc:b ≥ c⊢ a ≥ c
  sorryAll goals completed! 🐙

(c) (Порядок антисіметричен). Порівняйте із Mathlib-овським Nat.le_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m ≤ n) : n = mNat.le_antisymm

theorem declaration uses 'sorry'Nat.ge_antisymm {a b:Nat} (hab: a ≥ b) (hba: b ≥ a) : a = b := bya:Natb:Nathab:a ≥ bhba:b ≥ a⊢ a = b
  sorryAll goals completed! 🐙

(d) (Додавання зберігає порядок). Порівняйте із Mathlib-овським Nat.add_le_add_right {n m : ℕ} (h : n ≤ m) (k : ℕ) : n + k ≤ m + kNat.add_le_add_right

theorem declaration uses 'sorry'Nat.add_ge_add_right (a b c:Nat) : a ≥ b ↔ a + c ≥ b + c := bya:Natb:Natc:Nat⊢ a ≥ b ↔ a + c ≥ b + c
  sorryAll goals completed! 🐙

(d) (Додавання зберігає порядок). Порівняйте із Mathlib-овським Nat.add_le_add_left {n m : ℕ} (h : n ≤ m) (k : ℕ) : k + n ≤ k + mNat.add_le_add_left

theorem Nat.add_ge_add_left (a b c:Nat) : a ≥ b ↔ c + a ≥ c + b := bya:Natb:Natc:Nat⊢ a ≥ b ↔ c + a ≥ c + b
  simp only [add_comm]a:Natb:Natc:Nat⊢ a ≥ b ↔ a + c ≥ b + c
  exact add_ge_add_right _ _ _All goals completed! 🐙

theorem Nat.add_le_add_right (a b c:Nat) : a ≤ b ↔ a + c ≤ b + c := add_ge_add_right _ _ _

theorem Nat.add_le_add_left (a b c:Nat) : a ≤ b ↔ c + a ≤ c + b := add_ge_add_left _ _ _

(e) a < b iff a++ ≤ b. Порівняйте із Mathlib-овським Nat.succ_le_iff {m n : ℕ} : m.succ ≤ n ↔ m < nNat.succ_le_iff

theorem declaration uses 'sorry'Nat.lt_iff_succ_le (a b:Nat) : a < b ↔ a++ ≤ b := bya:Natb:Nat⊢ a < b ↔ a++ ≤ b
  sorryAll goals completed! 🐙

(f) a < b if and only if b = a + d for positive d.

theorem declaration uses 'sorry'Nat.lt_iff_add_pos (a b:Nat) : a < b ↔ ∃ d:Nat, d.isPos ∧ b = a + d := bya:Natb:Nat⊢ a < b ↔ ∃ d, d.isPos ∧ b = a + d
  sorryAll goals completed! 🐙

Якщо a < b тоді a ̸= b,

theorem Nat.ne_of_lt (a b:Nat) : a < b → a ≠ b := bya:Natb:Nat⊢ a < b → a ≠ b
  intro ha:Natb:Nath:a < b⊢ a ≠ b; exact h.2All goals completed! 🐙

Якщо a > b тоді a ̸= b.

theorem Nat.ne_of_gt (a b:Nat) : a > b → a ≠ b := bya:Natb:Nat⊢ a > b → a ≠ b
  intro ha:Natb:Nath:a > b⊢ a ≠ b; exact h.2.symmAll goals completed! 🐙

Якщо a > b та a < b тоді протиріччя

theorem Nat.not_lt_of_gt (a b:Nat) : a < b ∧ a > b → False := bya:Natb:Nat⊢ a < b ∧ a > b → False
  intro ha:Natb:Nath:a < b ∧ a > b⊢ False
  have := (ge_antisymm (Nat.le_of_lt h.1) (Nat.le_of_lt h.2)).symma:Natb:Nath:a < b ∧ a > bthis:a = b⊢ False
  have := ne_of_lt _ _ h.1a:Natb:Nath:a < b ∧ a > bthis✝:a = bthis:a ≠ b⊢ False
  contradictionAll goals completed! 🐙

Твердження 2.2.13 (Тріхотомія порядку для натуральних чисел) / Вправа 2.2.4 Порівняйте із Mathlib-овським trichotomous.{u_1} {α : Sort u_1} {r : α → α → Prop} [IsTrichotomous α r] (a b : α) : r a b ∨ a = b ∨ r b atrichotomous

theorem declaration uses 'sorry'Nat.trichotomous (a b:Nat) : a < b ∨ a = b ∨ a > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert ab:Nat⊢ ∀ (a : Nat), a < b ∨ a = b ∨ a > b; apply inductionhbaseb:Nat⊢ 0 < b ∨ 0 = b ∨ 0 > bhindb:Nat⊢ ∀ (n : Nat), n < b ∨ n = b ∨ n > b → n++ < b ∨ n++ = b ∨ n++ > b
  .hbaseb:Nat⊢ 0 < b ∨ 0 = b ∨ 0 > b have why : 0 ≤ b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b
      sorryAll goals completed! 🐙
    replace why := (Nat.le_iff_lt_or_eq _ _).mp whyhbaseb:Natwhy:0 < b ∨ 0 = b⊢ 0 < b ∨ 0 = b ∨ 0 > b
    tautoAll goals completed! 🐙
  intro a ihhindb:Nata:Natih:a < b ∨ a = b ∨ a > b⊢ a++ < b ∨ a++ = b ∨ a++ > b
  rcases ih with case1 | case2 | case3hind.inlb:Nata:Natcase1:a < b⊢ a++ < b ∨ a++ = b ∨ a++ > bhind.inr.inlb:Nata:Natcase2:a = b⊢ a++ < b ∨ a++ = b ∨ a++ > bhind.inr.inrb:Nata:Natcase3:a > b⊢ a++ < b ∨ a++ = b ∨ a++ > b
  .hind.inlb:Nata:Natcase1:a < b⊢ a++ < b ∨ a++ = b ∨ a++ > b rw [lt_iff_succ_le] at case1hind.inlb:Nata:Natcase1:a++ ≤ b⊢ a++ < b ∨ a++ = b ∨ a++ > b
    rw [Nat.le_iff_lt_or_eq] at case1hind.inlb:Nata:Natcase1:a++ < b ∨ a++ = b⊢ a++ < b ∨ a++ = b ∨ a++ > b
    tautoAll goals completed! 🐙
  .hind.inr.inlb:Nata:Natcase2:a = b⊢ a++ < b ∨ a++ = b ∨ a++ > b have why : a++ > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b sorryAll goals completed! 🐙
    tautoAll goals completed! 🐙
  have why : a++ > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b sorryAll goals completed! 🐙
  tautoAll goals completed! 🐙

(Не із книги) Встановіть алгоритмічну розв'язність для цього порядку обчислювальним шляхом. Частина доказу, що стосується розв'язності, наведена; решта sorry : ?m.18744sorry стосуються тверджень про натуральні числа. Цей результат також можна було б встановити за допомогою тактики unknown identifier 'classical'classical з подальшим використанням unknown identifier 'exact'exact Classical.decRel _, але це зробило б це визначення (а також деякі приклади нижче) необчислювальним.

Порівняйте із Mathlib-овським Nat.decLe (n m : ℕ) : Decidable (n ≤ m)Nat.decLe

def declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Nat.decLe : (a b : Nat) → Decidable (a ≤ b)
  | 0, b =>b:Nat⊢ Decidable (0 ≤ b) byb:Nat⊢ Decidable (0 ≤ b)
    apply isTruehb:Nat⊢ 0 ≤ b
    sorryAll goals completed! 🐙
  | a++, b =>a:Natb:Nat⊢ Decidable (a++ ≤ b) bya:Natb:Nat⊢ Decidable (a++ ≤ b)
    cases decLe a b with
    | isTrue h =>isTruea:Natb:Nath:a ≤ b⊢ Decidable (a++ ≤ b)
      cases decEq a b with
      | isTrue h =>isTrue.isTruea:Natb:Nath✝:a ≤ bh:a = b⊢ Decidable (a++ ≤ b)
        apply isFalseisTrue.isTrue.ha:Natb:Nath✝:a ≤ bh:a = b⊢ ¬a++ ≤ b
        sorryAll goals completed! 🐙
      | isFalse h =>isTrue.isFalsea:Natb:Nath✝:a ≤ bh:¬a = b⊢ Decidable (a++ ≤ b)
        apply isTrueisTrue.isFalse.ha:Natb:Nath✝:a ≤ bh:¬a = b⊢ a++ ≤ b
        sorryAll goals completed! 🐙
    | isFalse h =>isFalsea:Natb:Nath:¬a ≤ b⊢ Decidable (a++ ≤ b)
      apply isFalseisFalse.ha:Natb:Nath:¬a ≤ b⊢ ¬a++ ≤ b
      sorryAll goals completed! 🐙

instance Nat.decidableRel : DecidableRel (· ≤ · : Nat → Nat → Prop) := Nat.decLe

(Не із книги) Nat має структуру лінійне впорядкування.

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Nat.linearOrder : LinearOrder Nat where
  le_refl := ge_refl
  le_trans a b c hab hbc := ge_trans hbc hab
  lt_iff_le_not_le := sorry
  le_antisymm a b hab hba := ge_antisymm hba hab
  le_total := sorry
  toDecidableLE := decidableRel

(Не із книги) Nat має структуру впорядкованого моноїда.

instance Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat where
  add_le_add_left := by⊢ ∀ (a b : Nat), a ≤ b → ∀ (c : Nat), c + a ≤ c + b
    intro a b hab ca:Natb:Nathab:a ≤ bc:Nat⊢ c + a ≤ c + b
    exact (add_le_add_left a b c).mp habAll goals completed! 🐙

Твердження 2.2.14 (Сильний принцип індукції) / Вправа 2.2.5 Порівняйте із Mathlib-овським Nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ m < n, p m) → p n) : p nNat.strong_induction_on

theorem declaration uses 'sorry'Nat.strong_induction {m₀:Nat} {P: Nat → Prop}
  (hind: ∀ m, m ≥ m₀ → (∀ m', m₀ ≤ m' ∧ m' < m → P m') → P m) :
    ∀ m, m ≥ m₀ → P m := bym₀:NatP:Nat → Prophind:∀ m ≥ m₀, (∀ (m' : Nat), m₀ ≤ m' ∧ m' < m → P m') → P m⊢ ∀ m ≥ m₀, P m
  sorryAll goals completed! 🐙

Вправа 2.2.6 (індукція у зворотньому напрямку) Порівняйте із Mathlib-овським Nat.decreasingInduction.{u_1} {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) (self : motive n ⋯) {m : ℕ} (mn : m ≤ n) : motive m mnNat.decreasingInduction

theorem declaration uses 'sorry'Nat.backwards_induction {n:Nat} {P: Nat → Prop}
  (hind: ∀ m, P (m++) → P m) (hn: P n) :
    ∀ m, m ≤ n → P m := byn:NatP:Nat → Prophind:∀ (m : Nat), P (m++) → P mhn:P n⊢ ∀ m ≤ n, P m
  sorryAll goals completed! 🐙

Вправа 2.2.7 (індукція із початкової точки) Порівняйте із Mathlib-овським Nat.le_induction {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop} (base : P m ⋯) (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) (n : ℕ) (hmn : m ≤ n) : P n hmnNat.le_induction

theorem declaration uses 'sorry'Nat.induction_from {n:Nat} {P: Nat → Prop} (hind: ∀ m, P m → P (m++)) :
    P n → ∀ m, m ≥ n → P m := byn:NatP:Nat → Prophind:∀ (m : Nat), P m → P (m++)⊢ P n → ∀ m ≥ n, P m
  sorryAll goals completed! 🐙

end Chapter2