Analysis I, Section 2.1: The Peano Axioms

This file is a translation of Section 2.1 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 the "Chapter 2" natural numbers, Chapter2.Nat : TypeChapter2.Nat, abbreviated as Nat : TypeNat within the Chapter2 namespace. (In the book, the natural numbers are treated in a purely axiomatic fashion, as a type that obeys the Peano axioms; but here we take advantage of Lean's native inductive types to explicitly construct a version of the natural numbers that obey those axioms. One could also proceed more axiomatically, as is done in Section 3 for set theory: see the epilogue to this chapter.)
Establishment of the Peano axioms for Chapter2.Nat : TypeChapter2.Nat.
Recursive definitions for Chapter2.Nat : TypeChapter2.Nat.

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

namespace Chapter2

Assumption 2.6 (Existence of natural numbers). Here we use an explicit construction of the natural numbers (using an inductive type). For a more axiomatic approach, see the epilogue to this chapter.

inductive Nat where
| zero : Nat
| succ : Nat → Nat
deriving Repr, DecidableEq  -- this allows `decide` to work on `Nat`

Axiom 2.1 (0 is a natural number)

instance Nat.instZero : Zero Nat := ⟨ zero ⟩

0 : Nat

/-- Axiom 2.2 (Successor of a natural number is a natural number) -/
postfix:100 "++" => Nat.succ

fun n => n++ : Nat → Nat

Definition 2.1.3 (Definition of the numerals 0, 1, 2, etc.). Note: to avoid ambiguity, one may need to use explicit casts such as (0:Nat), (1:Nat), etc. to refer to this chapter's version of the natural numbers.

instance Nat.instOfNat {n:_root_.Nat} : OfNat Nat n where
  ofNat := _root_.Nat.rec 0 (fun _ n ↦ n++) n

instance Nat.instOne : One Nat := ⟨ 1 ⟩lemma Nat.zero_succ : 0++ = 1 := by⊢ 0++ = 1 rflAll goals completed! 🐙

1 : Nat

lemma Nat.one_succ : 1++ = 2 := by⊢ 1++ = 2 rflAll goals completed! 🐙

2 : Nat

Proposition 2.1.4 (3 is a natural number)

lemma Nat.two_succ : 2++ = 3 := by⊢ 2++ = 3 rflAll goals completed! 🐙

3 : Nat

Axiom 2.3 (0 is not the successor of any natural number). Compare with Lean's Nat.succ_ne_zero (n : ℕ) : n.succ ≠ 0Nat.succ_ne_zero.

theorem Nat.succ_ne (n:Nat) : n++ ≠ 0 := byn:Nat⊢ n++ ≠ 0
  by_contra hn:Nath:n++ = 0⊢ False
  injection hAll goals completed! 🐙

Proposition 2.1.6 (4 is not equal to zero)

theorem Nat.four_ne : (4:Nat) ≠ 0 := by⊢ 4 ≠ 0
  -- By definition, 4 = 3++.
  change 3++ ≠ 0⊢ 3++ ≠ 0
  -- By axiom 2.3, 3++ is not zero.
  exact succ_ne _All goals completed! 🐙

Axiom 2.4 (Different natural numbers have different successors). Compare with Mathlib's Nat.succ_inj {a b : ℕ} : a.succ = b.succ ↔ a = bNat.succ_inj.

theorem Nat.succ_cancel {n m:Nat} (hnm: n++ = m++) : n = m := byn:Natm:Nathnm:n++ = m++⊢ n = m
  injection hnmAll goals completed! 🐙

Axiom 2.4 (Different natural numbers have different successors). Compare with Mathlib's Chapter2.Nat.succ_ne_succ (n m : Nat) : n ≠ m → n++ ≠ m++Nat.succ_ne_succ.

theorem Nat.succ_ne_succ (n m:Nat) : n ≠ m → n++ ≠ m++ := byn:Natm:Nat⊢ n ≠ m → n++ ≠ m++
  intro hn:Natm:Nath:n ≠ m⊢ n++ ≠ m++
  contrapose! hn:Natm:Nath:n++ = m++⊢ n = m
  exact succ_cancel hAll goals completed! 🐙

Proposition 2.1.8 (6 is not equal to 2)

theorem Nat.six_ne_two : (6:Nat) ≠ 2 := by⊢ 6 ≠ 2
-- this proof is written to follow the structure of the original text.
  by_contra hh:6 = 2⊢ False
  change 5++ = 1++ at hh:5++ = 1++⊢ False
  apply succ_cancel at hh:5 = 1⊢ False
  change 4++ = 0++ at hh:4++ = 0++⊢ False
  apply succ_cancel at hh:4 = 0⊢ False
  have := four_neh:4 = 0this:?_mvar.8344 := Chapter2.Nat.four_ne⊢ False
  contradictionAll goals completed! 🐙

One can also prove this sort of result by the Decidable.decide (p : Prop) [h : Decidable p] : Booldecide tactic

theorem Nat.six_ne_two' : (6:Nat) ≠ 2 := by⊢ 6 ≠ 2
  decideAll goals completed! 🐙

Axiom 2.5 (Principle of mathematical induction). The Unknown identifier `induction`induction (or Unknown identifier `induction'`induction') tactic in Mathlib serves as a substitute for this axiom.

theorem Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ n, P n → P (n++)) :
    ∀ n, P n := byP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)⊢ ∀ (n : Nat), P n
  intro nP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)n:Nat⊢ P n
  induction n with
  | zero =>zeroP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)⊢ P zero exact hbaseAll goals completed! 🐙
  | succ n ih =>succP:Nat → Prophbase:P 0hind:∀ (n : Nat), P n → P (n++)n:Natih:P n⊢ P (n++) exact hind _ ihAll goals completed! 🐙

Recursion. Analogous to the inbuilt Mathlib method Chapter2.Nat.rec.{u} {motive : Nat → Sort u} (zero : motive Nat.zero) (succ : (a : Nat) → motive a → motive (a++)) (t : Nat) : motive tNat.rec associated to the Mathlib natural numbers

abbrev Nat.recurse (f: Nat → Nat → Nat) (c: Nat) : Nat → Nat := fun n ↦ match n with
| 0 => c
| n++ => f n (recurse f c n)

Proposition 2.1.16 (recursive definitions). Compare with Mathlib's Nat.rec_zero.{u_1} {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) : _root_.Nat.rec h0 h 0 = h0Nat.rec_zero.

theorem Nat.recurse_zero (f: Nat → Nat → Nat) (c: Nat) : Nat.recurse f c 0 = c := byf:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c rflAll goals completed! 🐙

Proposition 2.1.16 (recursive definitions). Compare with Mathlib's Nat.rec_add_one.{u_1} {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ) : _root_.Nat.rec h0 h (n + 1) = h n (_root_.Nat.rec h0 h n)Nat.rec_add_one.

theorem Nat.recurse_succ (f: Nat → Nat → Nat) (c: Nat) (n: Nat) :
    recurse f c (n++) = f n (recurse f c n) := byf:Nat → Nat → Natc:Natn:Nat⊢ recurse f c (n++) = f n (recurse f c n) rflAll goals completed! 🐙

Proposition 2.1.16 (recursive definitions).

theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) :
    (a 0 = c ∧ ∀ n, a (n++) = f n (a n)) ↔ a = recurse f c := byf:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) ↔ a = recurse f c
  constructormpf:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) → a = recurse f cmprf:Nat → Nat → Natc:Nata:Nat → Nat⊢ a = recurse f c → a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)
  .mpf:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) → a = recurse f c intro ⟨ h0, hsucc ⟩mpf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ a = recurse f c
    -- this proof is written to follow the structure of the original text.
    apply funextmp.hf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ ∀ (x : Nat), a x = recurse f c x; apply inductionmp.h.hbasef:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ a 0 = recurse f c 0mp.h.hindf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ ∀ (n : Nat), a n = recurse f c n → a (n++) = recurse f c (n++)
    .mp.h.hbasef:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)⊢ a 0 = recurse f c 0 exact h0All goals completed! 🐙
    intro n hnmp.h.hindf:Nat → Nat → Natc:Nata:Nat → Nath0:a 0 = chsucc:∀ (n : Nat), a (n++) = f n (a n)n:Nathn:a n = recurse f c n⊢ a (n++) = recurse f c (n++)
    rw [hsucc n, recurse_succ, hn]All goals completed! 🐙
  intro hmprf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)
  rw [h]mprf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ recurse f c 0 = c ∧ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n)
  constructormpr.leftf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ recurse f c 0 = cmpr.rightf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n) -- could also use `split_ands` or `and_intros` here
  .mpr.leftf:Nat → Nat → Natc:Nata:Nat → Nath:a = recurse f c⊢ recurse f c 0 = c exact recurse_zero _ _All goals completed! 🐙
  exact recurse_succ _ _All goals completed! 🐙

Proposition 2.1.16 (recursive definitions).

theorem Nat.recurse_uniq (f: Nat → Nat → Nat) (c: Nat) :
    ∃! (a: Nat → Nat), a 0 = c ∧ ∀ n, a (n++) = f n (a n) := byf:Nat → Nat → Natc:Nat⊢ ∃! a, a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)
  apply ExistsUnique.intro (recurse f c)h₁f:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c ∧ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n)h₂f:Nat → Nat → Natc:Nat⊢ ∀ (y : Nat → Nat), (y 0 = c ∧ ∀ (n : Nat), y (n++) = f n (y n)) → y = recurse f c
  .h₁f:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c ∧ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n) constructorh₁.leftf:Nat → Nat → Natc:Nat⊢ recurse f c 0 = ch₁.rightf:Nat → Nat → Natc:Nat⊢ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n) -- could also use `split_ands` or `and_intros` here
    .h₁.leftf:Nat → Nat → Natc:Nat⊢ recurse f c 0 = c exact recurse_zero _ _All goals completed! 🐙
    .h₁.rightf:Nat → Nat → Natc:Nat⊢ ∀ (n : Nat), recurse f c (n++) = f n (recurse f c n) exact recurse_succ _ _All goals completed! 🐙
  intro ah₂f:Nat → Nat → Natc:Nata:Nat → Nat⊢ (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) → a = recurse f c
  exact (eq_recurse _ _ a).mpAll goals completed! 🐙

end Chapter2