Analysis I, Section 2.1

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
• 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" for pedagogical purposes.

inductive Chapter2.Nat : Type

Assumption 2.6 (Existence of natural numbers)

• zero : Nat
• succ : Nat → Nat

instance Chapter2.instReprNat : Repr Nat

Equations

• Chapter2.instReprNat = { reprPrec := Chapter2.reprNat✝ }

instance Chapter2.instDecidableEqNat : DecidableEq Nat

Equations

• Chapter2.instDecidableEqNat = Chapter2.decEqNat✝

instance Chapter2.Nat.zero_inst : Zero Nat

Axiom 2.1 (0 is a natural number)

Equations

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

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

Equations

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

instance Chapter2.Nat.ofnat_inst {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.ofnat_inst = { ofNat := Nat.rec 0 (fun (x : ℕ) (n : Chapter2.Nat) => n++) n }

instance Chapter2.Nat.one_inst : One Nat

Equations

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

theorem Chapter2.zero_succ : 0++ = 1

theorem Chapter2.one_succ : 1++ = 2

theorem Chapter2.two_succ : 2++ = 3

Proposition 2.1.4 (3 is a natural number)

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

Axiom 2.3 (0 is not the successor of any natural number)

theorem Chapter2.four_ne : 4 ≠ 0

Proposition 2.1.6 (4 is not equal to zero)

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

Axiom 2.4 (Different natural numbers have different successors)

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

Axiom 2.4 (Different natural numbers have different successors)

theorem Chapter2.six_ne_two : 6 ≠ 2

Proposition 2.1.8 (6 is not equal to 2)

theorem Chapter2.six_ne_two' : 6 ≠ 2

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

theorem Chapter2.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).

@[reducible, inline]

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

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.recurse_zero (f : Nat → Nat → Nat) (c : Nat) : Nat.recurse f c 0 = c

Proposition 2.1.16 (recursive definitions).

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

Proposition 2.1.16 (recursive definitions).

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

Proposition 2.1.16 (recursive definitions).

theorem Chapter2.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).