Analysis I, Section 2.2: Addition

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.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

• (Add tip here)

@[reducible, inline]

abbrev Chapter2.Nat.add (n m : Nat) : Nat

Definition 2.2.1. (Addition of natural numbers). Compare with Mathlib's Nat.add

Equations

• n.add m = Chapter2.Nat.recurse (fun (x sum : Chapter2.Nat) => sum++) m n

instance Chapter2.Nat.instAdd : Add Nat

This instance allows for the + notation to be used for natural number addition.

Equations

• Chapter2.Nat.instAdd = { add := Chapter2.Nat.add }

@[simp]

theorem Chapter2.Nat.zero_add (m : Nat) : 0 + m = m

Compare with Mathlib's Nat.zero_add.

theorem Chapter2.Nat.succ_add (n m : Nat) : n++ + m = (n + m)++

Compare with Mathlib's Nat.succ_add.

theorem Chapter2.Nat.one_add (m : Nat) : 1 + m = m++

Compare with Mathlib's Nat.one_add.

theorem Chapter2.Nat.two_add (m : Nat) : 2 + m = m++++

@[simp]

theorem Chapter2.Nat.add_zero (n : Nat) : n + 0 = n

Lemma 2.2.2 (n + 0 = n). Compare with Mathlib's Nat.add_zero.

theorem Chapter2.Nat.add_succ (n m : Nat) : n + m++ = (n + m)++

Lemma 2.2.3 (n+(m++) = (n+m)++). Compare with Mathlib's Nat.add_succ.

theorem Chapter2.Nat.succ_eq_add_one (n : Nat) : n++ = n + 1

n++ = n + 1 (Why?). Compare with Mathlib's Nat.succ_eq_add_one

theorem Chapter2.Nat.add_comm (n m : Nat) : n + m = m + n

Proposition 2.2.4 (Addition is commutative). Compare with Mathlib's Nat.add_comm

theorem Chapter2.Nat.add_assoc (a b c : Nat) : a + b + c = a + (b + c)

Proposition 2.2.5 (Addition is associative) / Exercise 2.2.1 Compare with Mathlib's Nat.add_assoc.

theorem Chapter2.Nat.add_left_cancel (a b c : Nat) (habc : a + b = a + c) : b = c

Proposition 2.2.6 (Cancellation law). Compare with Mathlib's Nat.add_left_cancel.

instance Chapter2.Nat.addCommMonoid : AddCommMonoid Nat

(Not from textbook) Nat can be given the structure of a commutative additive monoid. This permits tactics such as abel to apply to the Chapter 2 natural numbers.

Equations

• One or more equations did not get rendered due to their size.

def Chapter2.Nat.IsPos (n : Nat) : Prop

Definition 2.2.7 (Positive natural numbers).

Equations

• n.IsPos = (n ≠ 0)

theorem Chapter2.Nat.isPos_iff (n : Nat) : n.IsPos ↔ n ≠ 0

theorem Chapter2.Nat.add_pos_left {a : Nat} (b : Nat) (ha : a.IsPos) : (a + b).IsPos

Proposition 2.2.8 (positive plus natural number is positive). Compare with Mathlib's Nat.add_pos_left.

theorem Chapter2.Nat.add_pos_right {a : Nat} (b : Nat) (ha : a.IsPos) : (b + a).IsPos

Compare with Mathlib's Nat.add_pos_right.

This theorem is a consequence of the previous theorem and add_comm, and grind can automatically discover such proofs.

theorem Chapter2.Nat.add_eq_zero (a b : Nat) (hab : a + b = 0) : a = 0 ∧ b = 0

Corollary 2.2.9 (if sum vanishes, then summands vanish). Compare with Mathlib's Nat.add_eq_zero.

theorem Chapter2.Nat.uniq_succ_eq (a : Nat) (ha : a.IsPos) : ∃! b : Nat, b++ = a

Lemma 2.2.10 (unique predecessor) / Exercise 2.2.2

instance Chapter2.Nat.instLE : LE Nat

Definition 2.2.11 (Ordering of the natural numbers). This defines the ≤ notation on the natural numbers.

Equations

• Chapter2.Nat.instLE = { le := fun (n m : Chapter2.Nat) => ∃ (a : Chapter2.Nat), m = n + a }

instance Chapter2.Nat.instLT : LT Nat

Definition 2.2.11 (Ordering of the natural numbers). This defines the < notation on the natural numbers.

Equations

• Chapter2.Nat.instLT = { lt := fun (n m : Chapter2.Nat) => n ≤ m ∧ n ≠ m }

theorem Chapter2.Nat.le_iff (n m : Nat) : n ≤ m ↔ ∃ (a : Nat), m = n + a

theorem Chapter2.Nat.lt_iff (n m : Nat) : n < m ↔ (∃ (a : Nat), m = n + a) ∧ n ≠ m

theorem Chapter2.Nat.ge_iff_le (n m : Nat) : n ≥ m ↔ m ≤ n

Compare with Mathlib's ge_iff_le.

theorem Chapter2.Nat.gt_iff_lt (n m : Nat) : n > m ↔ m < n

Compare with Mathlib's gt_iff_lt.

theorem Chapter2.Nat.le_of_lt {n m : Nat} (hnm : n < m) : n ≤ m

Compare with Mathlib's Nat.le_of_lt.

theorem Chapter2.Nat.le_iff_lt_or_eq (n m : Nat) : n ≤ m ↔ n < m ∨ n = m

Compare with Mathlib's Nat.le_iff_lt_or_eq.

theorem Chapter2.Nat.succ_gt_self (n : Nat) : n++ > n

Compare with Mathlib's Nat.lt_succ_self.

theorem Chapter2.Nat.ge_refl (a : Nat) : a ≥ a

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

(a) (Order is reflexive). Compare with Mathlib's Nat.le_refl.

theorem Chapter2.Nat.le_refl (a : Nat) : a ≤ a

theorem Chapter2.Nat.ge_trans {a b c : Nat} (hab : a ≥ b) (hbc : b ≥ c) : a ≥ c

(b) (Order is transitive). The obtain tactic will be useful here. Compare with Mathlib's Nat.le_trans.

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

theorem Chapter2.Nat.ge_antisymm {a b : Nat} (hab : a ≥ b) (hba : b ≥ a) : a = b

(c) (Order is anti-symmetric). Compare with Mathlib's Nat.le_antisymm.

theorem Chapter2.Nat.add_ge_add_right (a b c : Nat) : a ≥ b ↔ a + c ≥ b + c

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_right.

theorem Chapter2.Nat.add_ge_add_left (a b c : Nat) : a ≥ b ↔ c + a ≥ c + b

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_left.

theorem Chapter2.Nat.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + c

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_right.

theorem Chapter2.Nat.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + b

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_left.

theorem Chapter2.Nat.lt_iff_succ_le (a b : Nat) : a < b ↔ a++ ≤ b

(e) a < b iff a++ ≤ b. Compare with Mathlib's Nat.succ_le_iff.

theorem Chapter2.Nat.lt_iff_add_pos (a b : Nat) : a < b ↔ ∃ (d : Nat), d.IsPos ∧ b = a + d

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

theorem Chapter2.Nat.ne_of_lt (a b : Nat) : a < b → a ≠ b

If a < b then a ̸= b,

theorem Chapter2.Nat.ne_of_gt (a b : Nat) : a > b → a ≠ b

if a > b then a ̸= b.

theorem Chapter2.Nat.not_lt_of_gt (a b : Nat) : a < b ∧ a > b → False

If a > b and a < b then contradiction

theorem Chapter2.Nat.not_lt_self {a : Nat} (h : a < a) : False

theorem Chapter2.Nat.lt_of_le_of_lt {a b c : Nat} (hab : a ≤ b) (hbc : b < c) : a < c

theorem Chapter2.Nat.zero_le (a : Nat) : 0 ≤ a

This lemma was a why? statement from Proposition 2.2.13, but is more broadly useful, so is extracted here.

theorem Chapter2.Nat.trichotomous (a b : Nat) : a < b ∨ a = b ∨ a > b

Proposition 2.2.13 (Trichotomy of order for natural numbers) / Exercise 2.2.4 Compare with Mathlib's trichotomous. Parts of this theorem have been placed in the preceding Lean theorems.

def Chapter2.Nat.decLe (a b : Nat) : Decidable (a ≤ b)

(Not from textbook) Establish the decidability of this order computably. The portion of the proof involving decidability has been provided; the remaining sorries involve claims about the natural numbers. One could also have established this result by the classical tactic followed by exact Classical.decRel _, but this would make this definition (as well as some instances below) noncomputable.

Compare with Mathlib's Nat.decLe.

Equations

• One or more equations did not get rendered due to their size.
• Chapter2.Nat.zero.decLe x✝ = isTrue ⋯

instance Chapter2.Nat.decidableRel : DecidableRel fun (x1 x2 : Nat) => x1 ≤ x2

Equations

• Chapter2.Nat.decidableRel = Chapter2.Nat.decLe

instance Chapter2.Nat.instLinearOrder : LinearOrder Nat

(Not from textbook) Nat has the structure of a linear ordering. This allows for tactics such as order and calc to be applicable to the Chapter 2 natural numbers.

Equations

• One or more equations did not get rendered due to their size.

instance Chapter2.Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat

(Not from textbook) Nat has the structure of an ordered monoid. This allows for tactics such as gcongr to be applicable to the Chapter 2 natural numbers.

theorem Chapter2.Nat.strong_induction {m₀ : Nat} {P : Nat → Prop} (hind : ∀ m ≥ m₀, (∀ (m' : Nat), m₀ ≤ m' ∧ m' < m → P m') → P m) (m : Nat) : m ≥ m₀ → P m

Proposition 2.2.14 (Strong principle of induction) / Exercise 2.2.5 Compare with Mathlib's Nat.strong_induction_on.

theorem Chapter2.Nat.backwards_induction {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P (m++) → P m) (hn : P n) (m : Nat) : m ≤ n → P m

Exercise 2.2.6 (backwards induction) Compare with Mathlib's Nat.decreasingInduction.

theorem Chapter2.Nat.induction_from {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P m → P (m++)) : P n → ∀ m ≥ n, P m

Exercise 2.2.7 (induction from a starting point) Compare with Mathlib's Nat.le_induction.