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. (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, but we leave this as an exercise for the reader.)
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.

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#check (0:Nat)

0 : Nat

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

fun n => n++ : Nat → Nat#check (fun n ↦ n++)

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#check (1:Nat)

1 : Nat

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

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#check (3:Nat)

3 : Nat

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

theorem Nat.succ_ne (n:Nat) : n++ ≠ 0 := byn:Nat⊢ n++ ≠ 0
  by_contra hn:Nath:n++ = 0⊢ False
  simp only [reduceCtorEq] at 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)

theorem Nat.succ_cancel {n m:Nat} (hnm: n++ = m++) : n = m := byn:Natm:Nathnm:n++ = m++⊢ n = m
  rwa [succ.injEq]n:Natm:Nathnm:n = m⊢ n = m at hnm

Axiom 2.4 (Different natural numbers have different successors)

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
  replace h := succ_cancel hh:5 = 1⊢ False
  change 4++ = 0++ at hh:4++ = 0++⊢ False
  replace h := succ_cancel hh:4 = 0⊢ False
  have := four_neh:4 = 0this:4 ≠ 0⊢ False
  contradictionAll goals completed! 🐙

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

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

Axiom 2.5 (principle of mathematical induction).

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 => exact hbaseAll goals completed! 🐙
  | succ n ih => exact hind _ ihAll goals completed! 🐙

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

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

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