Analysis I, Section 2.2

This file is a translation of Section 2.2 of Analysis I to Lean 4. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Definition of addition and order for the "Chapter 2" natural numbers, Chapter2.Nat
Establishment of basic properties of addition and order

Note: at the end of this chapter, the Chapter2.Nat class will be deprecated in favor of the standard Mathlib class _root_.Nat, or ℕ. However, we will develop the properties of Chapter2.Nat "by hand" for pedagogical purposes.

namespace Chapter2

Definition 2.2.1. (Addition of natural numbers).

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

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

theorem Nat.zero_add (m: Nat) : 0 + m = m := recurse_zero (fun _ sum ↦ sum++) _theorem Nat.succ_add (n m: Nat) : n++ + m = (n+m)++ := byn:Natm:Nat⊢ n++ + m = (n + m)++ rflAll goals completed! 🐙

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

-- sum of two natural numbers is again a natural number
fun n m => n + m : Nat → Nat → Nat#check (fun (n m:Nat) ↦ n + m)

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

/-- Lemma 2.2.2 (n + 0 = n) -/
lemma Nat.add_zero (n:Nat) : n + 0 = n := byn:Nat⊢ n + 0 = n
  -- this proof is written to follow the structure of the original text.
  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! 🐙

/-- Lemma 2.2.3 (n+(m++) = (n+m)++). -/
lemma Nat.add_succ (n m:Nat) : n + (m++) = (n + m)++ := byn:Natm:Nat⊢ n + m++ = (n + m)++
  -- this proof is written to follow the structure of the original text.
  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 (Why?)

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

Proposition 2.2.4 (Addition is commutative)

theorem Nat.add_comm (n m:Nat) : n + m = m + n := byn:Natm:Nat⊢ n + m = m + n
  -- this proof is written to follow the structure of the original text.
  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! 🐙

Proposition 2.2.5 (Addition is associative) / Exercise 2.2.1

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

Proposition 2.2.6 (Cancellation law)

theorem Nat.add_cancel_left (a b c:Nat) (habc: a + b = a + c) : b = c := bya:Natb:Natc:Nathabc:a + b = a + c⊢ b = c
  -- this proof is written to follow the structure of the original text.
  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! 🐙

(Not from textbook) Nat can be given the structure of a commutative additive monoid.

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

Definition 2.2.7 (Positive natural numbers).

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

Proposition 2.2.8 (positive plus natural number is positive).

theorem Nat.pos_add {a:Nat} (b:Nat) (ha: a.isPos) : (a + b).isPos := bya:Natb:Natha:a.isPos⊢ (a + b).isPos
  -- this proof is written to follow the structure of the original text.
  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! 🐙

theorem Nat.add_pos {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 pos_add _ haAll goals completed! 🐙

Corollary 2.2.9 (if sum vanishes, then summands vanish).

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
  -- this proof is written to follow the structure of the original text.
  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 := pos_add _ 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 _ hbinra:Natb:Nathab:a + b = 0hb:b.isPosthis:(a + b).isPos⊢ False
  contradictionAll goals completed! 🐙

/-- Lemma 2.2.10 (unique predecessor) / Exercise 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! 🐙

Definition 2.2.11 (Ordering of the natural numbers)

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

Definition 2.2.11 (Ordering of the natural numbers)

instance Nat.instLT : LT Nat where
  lt n m := (∃ a:Nat, m = n + a) ∧ 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! 🐙

lemma Nat.ge_iff_le (n m:Nat) : n ≥ m ↔ m ≤ n := byn:Natm:Nat⊢ n ≥ m ↔ m ≤ n rflAll goals completed! 🐙lemma Nat.gt_iff_lt (n m:Nat) : n > m ↔ m < n := byn:Natm:Nat⊢ n > m ↔ m < n rflAll goals completed! 🐙lemma Nat.le_of_lt {n m:Nat} (hnm: n < m) : n ≤ m := hnm.1

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

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

Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3

(a) (Order is reflexive).

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

(b) (Order is transitive)

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 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) (Addition preserves order)

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) (Addition preserves order)

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

(d) (Addition preserves order)

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

(d) (Addition preserves order)

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.

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

If a < b then 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! 🐙

if a > b then 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! 🐙

If a > b and a < b then contradiction

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

Proposition 2.2.13 (Trichotomy of order for natural numbers) / Exercise 2.2.4

theorem declaration uses 'sorry'Nat.trichotomous (a b:Nat) : a < b ∨ a = b ∨ a > b := bya:Natb:Nat⊢ a < b ∨ a = b ∨ a > b
  -- this proof is written to follow the structure of the original text.
  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! 🐙

(Not from textbook) The order is decidable. This exercise is only recommended for Lean experts.

instance declaration uses 'sorry'Nat.decidableRel : DecidableRel (· ≤ · : Nat → Nat → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
  sorryAll goals completed! 🐙

(Not from textbook) Nat has the structure of a linear ordering.

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

(Not from textbook) Nat has the structure of an ordered monoid.

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

Proposition 2.2.14 (Strong principle of induction) / Exercise 2.2.5

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

Exercise 2.2.6 (backwards induction)

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

Exercise 2.2.7 (induction from a starting point)

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