Formalising Peano axioms

Stream: new members

[Miguel Marco]

Hi everybody,

I have recently started to look into lean, and, as a learning exercise, I decided to try to formalize Peano axioms in Lean.

The idea became motivated by an introductory course about sets and numbers that is taught by my department, so I thought it owuld be nice to prepare some material to show to the students (or instructors) of the course, that fits the corresponding syllabus.

So they way it is taught, is by assuming some naive set theory, and then stating the following axioms:

1. There exists a set named $\N$
2. There exists an element $0\in\mathbb{N}$
3. There is an injective function $s:\mathbb{N}\to\mathbb{N}$
4. There is no $n\in \mathbb{N}$ such that $s(n)=0$
5. If a subset $S\subseteq \mathbb{N}$ satisfies that $0\in S$ and $n\in S \Rightarrow s(s)\in S$, then $S=\mathbb{N}$

And from there, we go to prove several properties by induction, define the sum and so on.

I know that the "right" way to do this in Lean is to use the inductive type $\mathbb{N}$, but since i would like the material to follow the course, i tried to somehow mimic enough of naive set theory instead of making the students switch to think in terms of type theory.

This was my attempt so far:

notation `Conjunto` := Type  -- this is just to use a notation familiar to students

constant N : Conjunto   --  This would be the way to introduce  axiom 1
constant cero : N  --  same for axiom 2

constant sig: N → N
axiom siginy : ∀ n:N, ∀ m:N, (sig n = sig m) → n = m   -- these two lines together would be axiom 3

axiom ceronosig : ∀ n:N, ¬ (sig n = cero)  -- axiom 4

axiom induction : ∀ S:(N → Prop), (S cero ∧ (∀ n:N, S n → S (sig n))) → (∀ n:N, S n ) --   this is the way I found to introduce axiom 5
                  -- It is not exactly the statement of the axiom, since we deal with predicates instead of subsets
                  --  but it could be acceptable to reinstate the axiom in these terms

So the idea is to be able to use this setting to prove properties by induction. My first attempt was to prove the existence of a predecessor for naturals that are not cero:

theorem anterior : ∀ n:N, ( (n = cero)  ∨ (∃ m:N, sig m = n) ):=
begin
  intro n,

So now my goal is

n: N
⊢ n = cero ∨ ∃ (m : N), sig m = n

so far so good.

Now I want to introduce a predicate to apply the induction axiom. I try this:

let P1 : Prop :=  ∀  m:N, ((m = cero ) ∨ (∃ m2:N, sig m2 = m) ),

hoping to get a hypothesis like ∀ m:N, ((m = cero ) ∨ (∃ m2:N, sig m2 = m) ) , but what i get is just P1 : Prop, which i cannot use to prove the goal.

Is there a way to introduce a hypothesis with the type i want? Or is there a better way to formalize my five axioms(that stick to the idea of naive set theory) and prove theorems by inducton?

[Huỳnh Trần Khanh]

I don't think declaring axioms like in your code is a good idea. this is because Lean is extremely bad at handling axioms and constants. try using variables or typeclasses instead, similar to the suggestions in the #new members > Sebastian Zivota thread

[Huỳnh Trần Khanh]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Sebastian.20Zivota/near/263149134

[Eric Wieser]

You want have : ∀ ..., not let p : Prop := ∀ ...

[Huỳnh Trần Khanh]

assuming "conjunto" means set, mathlib has a model of ZFC that you can use https://leanprover-community.github.io/mathlib_docs/set_theory/zfc.html

[Eric Wieser]

I find it unlikely that the zfc formalization will be at all helpful here

[Patrick Johnson]

Proof of anterior:

theorem anterior : ∀ (n : N), n = cero ∨ ∃ (m : N), sig m = n :=
begin
  apply induction, split,
  { left, refl },
  { rintro n h, right, use n },
end

[Eric Wieser]

Huỳnh Trần Khanh said:

I don't think declaring axioms like in your code is a good idea. this is because Lean is extremely bad at handling axioms and constants.

I don't think the last half of this statement is true, but certainly the first half is. One way to avoid using axioms is to use a class instead:

notation `Conjunto` := Type  -- this is just to use a notation familiar to students

class is_N (N : Conjunto) :=   --  This would be the way to introduce  axiom 1
(cero : N)  --  same for axiom 2
(sig : N → N)
(siginy : ∀ n:N, ∀ m:N, (sig n = sig m) → n = m)   -- these two lines together would be axiom 3
(ceronosig : ∀ n:N, ¬ (sig n = cero))  -- axiom 4
(induction : ∀ S:(N → Prop), (S cero ∧ (∀ n:N, S n → S (sig n))) → (∀ n:N, S n )) --   this is the way I found to introduce axiom 5
                  -- It is not exactly the statement of the axiom, since we deal with predicates instead of subsets
                  --  but it could be acceptable to reinstate the axiom in these terms

which you can then use in your anterior as:

open is_N  -- so we don't have to type `is_N.cero`

theorem anterior {N} [is_N N] : -- "if N satisfies our axioms then..."
  ∀ n:N, ( (n = cero)  ∨ (∃ m:N, sig m = n) ):=
begin
  sorry
end

As a bonus, by using class you can then prove that ℕ satisfies these axioms:

instance ℕ_is_N : is_N ℕ :=
{ cero := 0,
  sig := nat.succ,
  siginy := λ _ _, nat.succ.inj,
  ceronosig := nat.succ_ne_zero,
  induction := λ _ ⟨h0, hs⟩, nat.rec h0 hs }

[Kyle Miller]

@Miguel Marco If you rearrange the induction axiom like this, then it's easier to use it to induct on a particular variable (and apply will automatically give you two goals to prove):

axiom induction : ∀ S:(N → Prop), ∀ n:N, S cero → (∀ m:N, S m → S (sig m)) → S n

theorem anterior : ∀ n:N, ( (n = cero)  ∨ (∃ m:N, sig m = n) ):=
begin
  intro n,
  apply induction _ n,
  { left, refl },
  { intros m h,
    right, use m, }
end

[Kyle Miller]

I think writing axioms for small examples like this is perfectly fine. Writing your own axioms should be avoided when you want to be certain that your proofs are correct (like for big projects with many things depending on the axioms), but for a demonstration that doesn't seem to be such a stringent requirement.

That said, it's easy enough to use Lean's nat to prove your axioms are good:

notation `Conjunto` := Type
def N : Conjunto := ℕ
def cero : N := nat.zero
def sig : N → N := nat.succ
def siginy : ∀ n:N, ∀ m:N, (sig n = sig m) → n = m := nat.succ_injective
theorem ceronosig : ∀ n:N, ¬(sig n = cero) := nat.succ_ne_zero
def induction : ∀ S:(N → Prop), ∀ n:N, S cero → (∀ m:N, S m → S (sig m)) → S n := λ _, nat.rec_on

[Kyle Miller]

You can make the induction axiom be in terms of Lean sets:

def induction : ∀ S:set N, ∀ n:N, cero ∈ S → (∀ m:N, m ∈ S → sig m ∈ S) → S n :=
λ S, @nat.rec_on (λ m, m ∈ S)

[Kyle Miller]

Though it seems you have to give the inductive set directly for Lean to not mess up the set membership syntax:

theorem anterior : ∀ n:N, ( (n = cero)  ∨ (∃ m:N, sig m = n) ):=
begin
  intro n,
  apply induction {n':N | n' = cero ∨ ∃ m:N, sig m = n'} n,
  { left, refl },
  { intros m h,
    right, use m, }
end

[Miguel Marco]

Kyle Miller said:

You can make the induction axiom be in terms of Lean sets:

def induction : ∀ S:set N, ∀ n:N, cero ∈ S → (∀ m:N, m ∈ S → sig m ∈ S) → S n :=
λ S, @nat.rec_on (λ m, m ∈ S)

Thanks everybody for the answers. I managed to make something decent from them.

On a second try, using Lean set, I am stuck trying to prove a theorem where my goal is :

a: N
h: a ∈ λ (n : N), O+n = n
⊢ sig a ∈ λ (n : N), O+n = n

I guess that to prove the goal I just have to construct a proof that O+(sig a)=(sig a). But my trouble is how to extract a proof of O+a=a from hypothesis h.

Is there a tactic for that?

[Kevin Buzzard]

h is definitionally equal to 0 + n = n. You could either do dsimp at h (probably even dsimp only at h will work but I can't check because you didn't post a mwe), or change 0+a=a at h.

[Kyle Miller]

@Miguel Marco It looks like you're running into what happens when Lean tries to infer the inductive set for thatinduction axiom -- it turns it into a lambda, losing the set syntax.

It seems like there's a way to get Lean to infer the right thing by using {n' | _} for that argument:

theorem anterior : ∀ n:N, ((n = cero) ∨ (∃ m:N, sig m = n)):=
begin
  intro n,
  apply induction {n' | _} n,
  { left, refl },
  { intros m h,
    right, use m, },
end

You can change n' to whatever you want, and it's how you name the induction variable.

By the way, if you want to make sure you only use the axioms you've defined, keeping Lean from making use of built-in definitional equalities, I think putting this line after all your axioms should work:

attribute [irreducible] N

[Kyle Miller]

To answer your immediate question, h is exactly a proof of O+a = a, and you fix the syntactic oddness with

change O+a = a at h

though it would be better to avoid seeing anything like that in the first place if it can be helped. (Edit: I somehow missed that Kevin already mentioned change.)