Додавання

Аналіз 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 "вручну" в наступних кількох розділах для педагогічних цілей.

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

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

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

namespace Chapter2

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

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

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

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

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

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

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

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

Порівняйте із Mathlib-овським Chapter2.Nat.one_add (m : Nat) : 1 + m = m++Nat.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

Лема 2.2.2 (n + 0 = n). Порівняйте із Mathlib-овським Chapter2.Nat.add_zero (n : Nat) : 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-овським Chapter2.Nat.add_succ (n m : Nat) : n + m++ = (n + m)++Nat.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-овським Chapter2.Nat.succ_eq_add_one (n : Nat) : n++ = 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-овським Chapter2.Nat.add_comm (n m : Nat) : 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-овським Chapter2.Nat.add_assoc (a b c : Nat) : a + b + c = a + (b + c)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-овським Chapter2.Nat.add_left_cancel (a b c : Nat) (habc : a + b = a + c) : b = cNat.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:?_mvar.2309 := Chapter2.Nat.succ_cancel _fvar.2300⊢ 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

Ця ілюстрація тактики Unknown identifier `abel`abel взята не з підручника.

example (a b c d:Nat) : (a+b)+(c+0+d) = (b+c)+(d+a) := bya:Natb:Natc:Natd:Nat⊢ a + b + (c + 0 + d) = b + c + (d + a) abelAll goals completed! 🐙

Визначення 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-овським Chapter2.Nat.add_pos_left {a : Nat} (b : Nat) (ha : a.IsPos) : (a + b).IsPosNat.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:(_fvar.4023 + _fvar.4071)++ ≠ 0 := Chapter2.Nat.succ_ne ?_mvar.4176⊢ (a + b)++.IsPos
  exact thisAll goals completed! 🐙

Порівняйте із Mathlib-овським Chapter2.Nat.add_pos_right {a : Nat} (b : Nat) (ha : a.IsPos) : (b + a).IsPosNat.add_pos_right

Ця теорема є наслідком попередньої теореми та add_comm.{u_1} {G : Type u_1} [AddCommMagma G] (a b : G) : a + b = b + aadd_comm, а Unknown identifier `grind`grind може автоматично знаходити такі докази.

theorem Nat.add_pos_right {a:Nat} (b:Nat) (ha: a.IsPos) : (b + a).IsPos := bya:Natb:Natha:a.IsPos⊢ (b + a).IsPos
  grind [add_comm, add_pos_left]All goals completed! 🐙

Наслідок 2.2.9 (якщо сума дорівнює нулю, тоді доданки дорівнюють нулю). Порівняйте із Mathlib-овським Chapter2.Nat.add_eq_zero (a b : Nat) (hab : a + b = 0) : a = 0 ∧ b = 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
  obtain ha | hb := hinla: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
    observe : (a + b).IsPosinla: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
  observe : (a + b).IsPosinra:Natb:Nathab:a + b = 0hb:b.IsPosthis:(a + b).IsPos⊢ False
  contradictionAll goals completed! 🐙

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

Лема 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

Порівняйте із Mathlib-овським le_iff_exists_add.{u} {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b ↔ ∃ c, b = a + cle_iff_exists_add.

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.

@[symm]
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.

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

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

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

Порівняйте із Mathlib-овським Chapter2.Nat.le_iff_lt_or_eq (n m : Nat) : 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 = mpos._@._hyg.1628n:Natm:Nath:n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = mneg._@._hyg.1628n:Natm:Nath:¬n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m
  .pos._@._hyg.1628n:Natm:Nath:n = m⊢ (∃ a, m = n + a) ↔ (∃ a, m = n + a) ∧ n ≠ m ∨ n = m simp [h]pos._@._hyg.1628n: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 := ?_mvar.63377⊢ ∃ 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-овським Chapter2.Nat.le_refl (a : Nat) : a ≤ aNat.le_refl

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

@[refl]
theorem Nat.le_refl (a:Nat) : a ≤ a := a.ge_refl

Тег refl.{u_1} {α : Sort u_1} {r : α → α → Prop} [IsRefl α r] (a : α) : r a arefl дозволяє тактиці rfl.{u} {α : Sort u} {a : α} : a = arfl працювати для нерівностей.

example (a b:Nat): a+b ≥ a+b := bya:Natb:Nat⊢ a + b ≥ a + b rflAll goals completed! 🐙

(b) (Порядок транзітивен). Тут буде корисною тактика Unknown identifier `obtain`obtain. Порівняйте із Mathlib-овським Chapter2.Nat.le_trans {a b c : Nat} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ cNat.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! 🐙

theorem Nat.le_trans {a b c:Nat} (hab: a ≤ b) (hbc: b ≤ c) : a ≤ c := Nat.ge_trans hbc hab

(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-овським Chapter2.Nat.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + cNat.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-овським Chapter2.Nat.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + bNat.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 якщо та лише якщо b = a + d для додатного 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 (le_of_lt h.1) (le_of_lt h.2)).symma:Natb:Nath:a < b ∧ a > bthis:?_mvar.64965 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ False
  have := ne_of_lt _ _ h.1a:Natb:Nath:a < b ∧ a > bthis✝:?_mvar.64965 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:?_mvar.65002 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ False
  contradictionAll goals completed! 🐙

theorem Nat.not_lt_self {a: Nat} (h : a < a) : False := bya:Nath:a < a⊢ False
  apply not_lt_of_gt a aa:Nath:a < a⊢ a < a ∧ a > a
  simp [h]All goals completed! 🐙

theorem Nat.lt_of_le_of_lt {a b c : Nat} (hab: a ≤ b) (hbc: b < c) : a < c := bya:Natb:Natc:Nathab:a ≤ bhbc:b < c⊢ a < c
  rw [lt_iff_add_pos] at *a:Natb:Natc:Nathab:a ≤ bhbc:∃ d, d.IsPos ∧ c = b + d⊢ ∃ d, d.IsPos ∧ c = a + d
  choose d hd using haba:Natb:Natc:Nathbc:∃ d, d.IsPos ∧ c = b + dd:Nathd:b = a + d⊢ ∃ d, d.IsPos ∧ c = a + d
  choose e he1 he2 using hbca:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ ∃ d, d.IsPos ∧ c = a + d
  use d + eha:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ (d + e).IsPos ∧ c = a + (d + e); split_andsh.refine_1a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ (d + e).IsPosh.refine_2a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ c = a + (d + e)
  .h.refine_1a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ (d + e).IsPos exact add_pos_right d he1All goals completed! 🐙
  .h.refine_2a:Natb:Natc:Natd:Nathd:b = a + de:Nathe1:e.IsPoshe2:c = b + e⊢ c = a + (d + e) rw [he2, hd, add_assoc]All goals completed! 🐙

Ця лема була твердженням Unknown identifier `why?`why? з Пропозиції 2.2.13, але є кориснішою в ширшому контексті, тому її винесено окремо.

theorem declaration uses 'sorry'Nat.zero_le (a:Nat) : 0 ≤ a := bya:Nat⊢ 0 ≤ a
  sorryAll 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 observe why : 0 ≤ bhbaseb:Natwhy:0 ≤ b⊢ 0 < b ∨ 0 = b ∨ 0 > b
    rw [le_iff_lt_or_eq] at 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
  obtain case1 | case2 | case3 := ihhind.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 [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.1sorry стосуються тверджень про натуральні числа. Цей результат також можна було б встановити за допомогою тактики Unknown identifier `classical`classical з подальшим використанням Unknown identifier `exact`exact Classical.decRel _, але це зробило б це визначення (а також деякі приклади нижче) необчислювальним.

Порівняйте із Mathlib-овським Chapter2.Nat.decLe (a b : Nat) : Decidable (a ≤ b)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 має структуру лінійне впорядкування. Це дозволяє застосовувати такі тактики, як Unknown identifier `order`order і , до натуральних чисел Розділу 2.

instance Nat.instLinearOrder : LinearOrder Nat where
  le_refl := ge_refl
  le_trans a b c hab hbc := ge_trans hbc hab
  lt_iff_le_not_ge a b := bya:Natb:Nat⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
    constructormpa:Natb:Nat⊢ a < b → a ≤ b ∧ ¬b ≤ ampra:Natb:Nat⊢ a ≤ b ∧ ¬b ≤ a → a < b
    .mpa:Natb:Nat⊢ a < b → a ≤ b ∧ ¬b ≤ a intro hmpa:Natb:Nath:a < b⊢ a ≤ b ∧ ¬b ≤ a; refine ⟨ le_of_lt h, ?_ ⟩mpa:Natb:Nath:a < b⊢ ¬b ≤ a
      by_contra h'mpa:Natb:Nath:a < bh':b ≤ a⊢ False
      exact not_lt_self (lt_of_le_of_lt h' h)All goals completed! 🐙
    rintro ⟨ h1, h2 ⟩mpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ a⊢ a < b
    rw [lt_iff, ←le_iff]mpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ a⊢ a ≤ b ∧ a ≠ b; refine ⟨ h1, ?_ ⟩mpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ a⊢ a ≠ b
    by_contra hmpr.introa:Natb:Nath1:a ≤ bh2:¬b ≤ ah:a = b⊢ False
    subst hmpr.introa:Nath1:a ≤ ah2:¬a ≤ a⊢ False
    contradictionAll goals completed! 🐙
  le_antisymm a b hab hba := ge_antisymm hba hab
  le_total a b := bya:Natb:Nat⊢ a ≤ b ∨ b ≤ a
    obtain h | rfl | h := trichotomous a binla:Natb:Nath:a < b⊢ a ≤ b ∨ b ≤ ainr.inla:Nat⊢ a ≤ a ∨ a ≤ ainr.inra:Natb:Nath:a > b⊢ a ≤ b ∨ b ≤ a
    .inla:Natb:Nath:a < b⊢ a ≤ b ∨ b ≤ a leftinl.ha:Natb:Nath:a < b⊢ a ≤ b; exact le_of_lt hAll goals completed! 🐙
    .inr.inla:Nat⊢ a ≤ a ∨ a ≤ a simp [ge_refl]All goals completed! 🐙
    .inr.inra:Natb:Nath:a > b⊢ a ≤ b ∨ b ≤ a rightinr.inr.ha:Natb:Nath:a > b⊢ b ≤ a; exact le_of_lt hAll goals completed! 🐙
  toDecidableLE := decidableRel

Ця ілюстрація тактики Unknown identifier `order`order взята не з підручника.

example (a b c d:Nat) (hab: a ≤ b) (hbc: b ≤ c) (hcd: c ≤ d)
        (hda: d ≤ a) : a = c := bya:Natb:Natc:Natd:Nathab:a ≤ bhbc:b ≤ chcd:c ≤ dhda:d ≤ a⊢ a = c orderAll goals completed! 🐙

Ця ілюстрація тактики із .

example (a b c d e:Nat) (hab: a ≤ b) (hbc: b < c) (hcd: c ≤ d)
        (hde: d ≤ e) : a + 0 < e := bya:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chcd:c ≤ dhde:d ≤ e⊢ a + 0 < e
  calc
    a + 0 = a := bya:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chcd:c ≤ dhde:d ≤ e⊢ a + 0 = a simpAll goals completed! 🐙
        _ ≤ b := hab
        _ < c := hbc
        _ ≤ d := hcd
        _ ≤ e := hde

(Не з підручника.) Chapter2.Nat : TypeNat має структуру впорядкованого моноїда. Це дозволяє застосовувати такі тактики, як Unknown identifier `gcongr`gcongr, до натуральних чисел Розділу 2.

instance Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat where
  add_le_add_left a b hab c := (add_le_add_left a b c).mp hab

Ця ілюстрація тактики Unknown identifier `gcongr`gcongr взята не з підручника.

example (a b c d e:Nat) (hab: a ≤ b) (hbc: b < c) (hde: d < e) :
  a + d ≤ c + e := bya:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chde:d < e⊢ a + d ≤ c + e
  gcongrh₁a:Natb:Natc:Natd:Nate:Nathab:a ≤ bhbc:b < chde:d < e⊢ a ≤ c
  orderAll 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