Peano's axioms by Lean

I have started learning how to write proofs using Lean. For my editor, I decided to go with VSCode (Official Installation Guide). I did try editors from JetBrains, but I gave up on them because the lack of code completion made the experience quite painful.

For my learning material, I am using "Introduction to Lean from Scratch: Hands-on Development of Formal Mathematics Libraries." This is a Japanese textbook on Lean 4. and I will be summarizing what I learn while transcribing the code. This first step covers Peano's Axioms.

What are Peano's Axioms?

Peano's axioms define the natural numbers. While it is tempting to intuitively describe them as "numbers that go on indefinitely like 1, 2, 3...", such a definition cannot be programmed. To handle natural numbers rigorously in Lean, they must be formally defined, just like in Peano's axioms.

The five Peano axioms are as follows:

1. 0 is a natural number.
2. There exists a function succ from natural numbers to natural numbers (e.g., succ(0) = 1).
3. The function succ yields different results for different natural numbers (injectivity).
4. 0 is never the result of the succ function.
5. The principle of mathematical induction holds. That is, if a statement holds for 0, and if assuming it holds for an arbitrary n implies it also holds for n+1, then the statement holds for all natural numbers.

In mathematics, a statement is called a proposition, and a proposition whose truth depends on a variable n is called a predicate.

Building Our Own Natural Numbers in Lean

Lean comes with a built-in natural number type called Nat, but for the sake of learning, let's start by defining our own MyNat.

inductive MyNat where
    | zero
    | succ(n : MyNat)

Apparently, this snippet alone is enough to complete the definition of natural numbers that satisfy Peano's axioms. Let's verify if that's true. Axioms 1 and 2 are satisfied because we defined them exactly as they are. On the other hand, you might wonder about the injectivity of succ (Axiom 3) and the fact that 0 never appears as a result of succ (Axiom 4), since we didn't explicitly define them. However, these properties are automatically guaranteed by Lean's inductive type system.

Let's clarify what the where keyword and the | (pipe) mean here:

• The where keyword indicates the start of a scope, essentially saying, "From here on out, this is the concrete content (the list of constructors) for this data type."
• The | (pipe) is used to declare a single, new, independent constructor (a way to build a value).

You can check that both zero and succ belong to the MyNat type using the following commands:

#check MyNat.zero
#check MyNat.succ

Defining Addition

Next up is addition. We use match to branch into cases: if n = 0, it returns m; if n matches succ n, it returns succ (add m n). This definition follows Peano arithmetic exactly.

def MyNat.add(m n : MyNat): MyNat :=
    match n with
    | .zero => m
    | .succ n => succ (add m n)

While := represents a definition, using = treats the statement as a proposition, as shown below. By using #check, you can see that even equations like "1 + 1 = 2" are represented as Prop (the type of propositions) in the world of Lean.

#check MyNat.add .one .one = .two

The #reduce command evaluates and displays the reduced result of an expression. Reduction means rewriting an expression into its most fundamental form using constructors—in other words, breaking it down to the combination of its axioms.

#reduce MyNat.add .one .one
#reduce MyNat.two

Proving a Proposition

We can prove "1 + 1 = 2" as follows. The example command is used to write an anonymous proof, whereas you would use theorem if you wanted to save it for later use.

example : MyNat.add .one .one = .two := by
    rfl

rfl is a keyword used for automated proofs. Short for Reflexivity, rfl makes Lean accept that "this equation is correct because the evaluated results of the left-hand side and the right-hand side are identical." If you see Goals accomplished! in the VSCode infoview, your proof is successful.

You can also prove the exact same proposition by rewriting the expression step by step:

example : MyNat.add .one .one = .two := by
    change MyNat.succ (MyNat.add .one .zero) = .two
    change MyNat.succ .one = .two
    change MyNat.succ .one = MyNat.succ .one
    trivial

Building the Project

By modifying lakefile.lean as shown below, you can add LearnLean to the build targets.

@[default_target]
lean_lib «LearnLean» where
    globs := #[.submodules `LearnLean]

Running lake build will compile the project like this:

LearnLean % lake build
ℹ [2/3] Built LearnLean.NaturalNumber
info: LearnLean/NaturalNumber.lean:7:0: MyNat.zero : MyNat
info: LearnLean/NaturalNumber.lean:8:0: MyNat.succ (n : MyNat) : MyNat
info: LearnLean/NaturalNumber.lean:9:0: MyNat.zero.succ : MyNat
info: LearnLean/NaturalNumber.lean:21:0: MyNat.one.add MyNat.one = MyNat.two : Prop
info: LearnLean/NaturalNumber.lean:26:0: MyNat.succ (MyNat.succ MyNat.zero)
info: LearnLean/NaturalNumber.lean:27:0: MyNat.succ (MyNat.succ MyNat.zero)
Build completed successfully (3 jobs).