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, abbreviated as Nat 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.
• Recursive definitions for Chapter2.Nat.

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" in the next few sections for pedagogical purposes.

inductive Chapter2.Nat : Type

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.

• zero : Nat
• succ : Nat → Nat

def Chapter2.instReprNat.repr : Nat → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Chapter2.instReprNat.repr Chapter2.Nat.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chapter2.Nat.zero")).group prec✝

@[implicit_reducible]

instance Chapter2.instReprNat : Repr Nat

Equations

• Chapter2.instReprNat = { reprPrec := Chapter2.instReprNat.repr }

@[implicit_reducible]

instance Chapter2.instDecidableEqNat : DecidableEq Nat

Equations

• Chapter2.instDecidableEqNat = Chapter2.instDecidableEqNat.decEq

def Chapter2.instDecidableEqNat.decEq (x✝ x✝¹ : Nat) : Decidable (x✝ = x✝¹)

Equations

• Chapter2.instDecidableEqNat.decEq Chapter2.Nat.zero Chapter2.Nat.zero = isTrue ⋯
• Chapter2.instDecidableEqNat.decEq Chapter2.Nat.zero (a++) = isFalse ⋯
• Chapter2.instDecidableEqNat.decEq (a++) Chapter2.Nat.zero = isFalse ⋯
• Chapter2.instDecidableEqNat.decEq (a++) (b++) = if h : a = b then h ▸ have inst := Chapter2.instDecidableEqNat.decEq a a; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Chapter2.Nat.instZero : Zero Nat

Axiom 2.1 (0 is a natural number)

Equations

• Chapter2.Nat.instZero = { zero := Chapter2.Nat.zero }

def Chapter2.«term_++» : Lean.TrailingParserDescr

Axiom 2.2 (Successor of a natural number is a natural number)

Equations

• Chapter2.«term_++» = Lean.ParserDescr.trailingNode `Chapter2.«term_++» 100 100 (Lean.ParserDescr.symbol "++")

@[implicit_reducible]

instance Chapter2.Nat.instOfNat {n : ℕ} : OfNat Nat n

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.

Equations

• Chapter2.Nat.instOfNat = { ofNat := Nat.rec 0 (fun (x : ℕ) (n : Chapter2.Nat) => n++) n }

@[implicit_reducible]

instance Chapter2.Nat.instOne : One Nat

Equations

• Chapter2.Nat.instOne = { one := 1 }

theorem Chapter2.Nat.zero_succ : 0++ = 1

theorem Chapter2.Nat.one_succ : 1++ = 2

theorem Chapter2.Nat.two_succ : 2++ = 3

Proposition 2.1.4 (3 is a natural number)

theorem Chapter2.Nat.succ_ne (n : Nat) : n++ ≠ 0

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

theorem Chapter2.Nat.four_ne : 4 ≠ 0

Proposition 2.1.6 (4 is not equal to zero)

theorem Chapter2.Nat.succ_cancel {n m : Nat} (hnm : n++ = m++) : n = m

Axiom 2.4 (Different natural numbers have different successors). Compare with Mathlib's Nat.succ_inj.

theorem Chapter2.Nat.succ_ne_succ (n m : Nat) : n ≠ m → n++ ≠ m++

Axiom 2.4 (Different natural numbers have different successors). Compare with Mathlib's Nat.succ_ne_succ.

theorem Chapter2.Nat.six_ne_two : 6 ≠ 2

Proposition 2.1.8 (6 is not equal to 2)

theorem Chapter2.Nat.six_ne_two' : 6 ≠ 2

One can also prove this sort of result by the decide tactic

theorem Chapter2.Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ (n : Nat), P n → P (n++)) (n : Nat) : P n

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

@[reducible, inline]

abbrev Chapter2.Nat.recurse (f : Nat → Nat → Nat) (c : Nat) : Nat → Nat

Recursion. Analogous to the inbuilt Mathlib method Nat.rec associated to the Mathlib natural numbers

Equations

• Chapter2.Nat.recurse f c Chapter2.Nat.zero = c
• Chapter2.Nat.recurse f c (a++) = f a (Chapter2.Nat.recurse f c a)

theorem Chapter2.Nat.recurse_zero (f : Nat → Nat → Nat) (c : Nat) : recurse f c 0 = c

Proposition 2.1.16 (recursive definitions). Compare with Mathlib's Nat.rec_zero.

theorem Chapter2.Nat.recurse_succ (f : Nat → Nat → Nat) (c n : Nat) : recurse f c (n++) = f n (recurse f c n)

Proposition 2.1.16 (recursive definitions). Compare with Mathlib's Nat.rec_add_one.

theorem Chapter2.Nat.eq_recurse (f : Nat → Nat → Nat) (c : Nat) (a : Nat → Nat) : (a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)) ↔ a = recurse f c

Proposition 2.1.16 (recursive definitions).

theorem Chapter2.Nat.recurse_uniq (f : Nat → Nat → Nat) (c : Nat) : ∃! a : Nat → Nat, a 0 = c ∧ ∀ (n : Nat), a (n++) = f n (a n)

Proposition 2.1.16 (recursive definitions).