# Library IZF.IZF_nat

Require Import IZF_logic.

To define the type of natural numbers, we introduce an extra universe Typ0 *below* the universe Typ1 (so that we are now working in the PTS lambda-omega.3).
Another possibility would be to consider an axiomatized type of natural numbers (as in the author's LICS submission).

Definition Typ0 : Typ1 := Type.

# The type of Church numerals in Typ1

## Definition of natural numbers

Notice that the following definition is *predicative*, and the dependent product ranging over all X:Typ0 builds a type in the next universe Typ1. In practice, this "predicativisation" of the type of natural numbers induces some minor changes in the implementation of the predecessor function.

Definition nat : Typ1 := X : Typ0, X → (XX) → X.
Definition O : nat := fun X x fx.
Definition S (n : nat) : nat := fun X x ff (n X x f).

A natural number is `well-formed' if it is in the smallest class containing zero and closed under the successor function.

Definition wf_nat (n : nat) : Prop :=
P : natProp, P O → ( p : nat, P pP (S p)) → P n.

## The predecessor function

For any type X : Typ0, we define the pseudo-square (sqr X) : Typ0 and the constructor (pair X) : X->X->(sqr X) by setting:

Definition sqr (X : Typ0) : Typ0 := (XXX) → X.
Definition pair (X : Typ0) (x y : X) : sqr X := fun ff x y.

The corresponding projections

Definition fst (X : Typ0) (p : sqr X) : X := p (fun x _x).
Definition snd (X : Typ0) (p : sqr X) : X := p (fun _ yy).

enjoy the expected definitional equalities:
(fst X (pair X x y)) = x and (snd X (pair X x y)) = y.
Now, consider an arbitrary function f : X->X. From this function, we define a function (step X f) : (sqr X)->(sqr X) that maps the pair (x, y) to the pair (y, (f y)) by setting:

Definition step (X : Typ0) (f : XX) (p : sqr X) :
sqr X := pair X (snd X p) (f (snd X p)).

If we iterate the function (step X f) from an arbitrary pair of the form (x, x), we obtain
(step X f)^0 (x, x) = (x, x) (step X f)^1 (x, x) = (x, (f x)) (step X f)^2 (x, x) = ((f x), (f (f x)) ... (step X f)^n (x, x) = ((f ... (f x) ...), (f ... (f x) ...)) ^^^^^^^^ ^^^^^^^^ n-1 times n times
By extracting the first component of the result and abstracting it w.r.t. the variables X:Typ0, x:X and f:X->X, we thus obtain the predecessor of Church numeral n. This is how the predecessor function is implemented:

Definition pred (n : nat) : nat :=
fun X x ffst X (n (sqr X) (pair X x x) (step X f)).

We easily check the following definitional equalities:

Lemma pred_O : eq nat (pred O) O.
Proof eq_refl nat O.

Lemma pred_SO : eq nat (pred (S O)) O.
Proof eq_refl nat O.

The following equality is really definitional! "I can see it, but I don't believe it"...

Lemma pred_SSn : n : nat, eq nat (pred (S (S n))) (S (pred (S n))).
Proof fun neq_refl nat (pred (S (S n))).

From this, we prove that the predecessor cancels a previous application of the successor function (by induction)

Lemma pred_S : n : nat, wf_nat neq nat (pred (S n)) n.

Proof.
intros n Hn; apply Hn; clear Hn n.
apply pred_O.
intros n H; pattern n at 2 in |- ×.
apply H; apply pred_SSn.
Qed.

# Deriving Peano's axioms

## First axiom of Peano

Lemma wf_nat_O : wf_nat O.

Proof fun P HO HSHO.

## Second axiom of Peano

Lemma wf_nat_S : n : nat, wf_nat nwf_nat (S n).

Proof fun n H P HO HSHS n (H P HO HS).

## Third axiom of Peano

Lemma eq_S_O : n : nat, wf_nat neq nat (S n) Obot.

Proof fun n _ HH (fun pp Prop bot (fun _top)) top_intro.

Lemma eq_O_S : n : nat, wf_nat neq nat O (S n) → bot.

Proof fun n _ HH (fun pp Prop top (fun _bot)) top_intro.

Note that in the proofs of the two lemmas above, the assumption (wf_nat n) is not used.

## Fourth axiom of Peano

Lemma eq_S_S :
n : nat,
wf_nat n p : nat, wf_nat peq nat (S n) (S p) → eq nat n p.

Proof.
intros n Hn p Hp H.
apply (pred_S n Hn).
apply (pred_S p Hp).
apply H; apply eq_refl.
Qed.

## Fifth axiom of Peano

Lemma nat_ind :
P : natProp,
P O
( p : nat, wf_nat pP pP (S p)) →
n : nat, wf_nat nP n.

Proof.
intros P HO HS n Hn.
apply (and_snd (wf_nat n) (P n)).
apply Hn; clear Hn n.
apply and_intro; [ exact wf_nat_O | assumption ].
intros n H; apply H; clear H.
intros H1 H2; apply and_intro.
apply wf_nat_S; assumption.
apply HS; assumption.
Qed.

Lemma nat_ind' :
n : nat,
wf_nat n
P : natProp,
P O → ( p : nat, wf_nat pP pP (S p)) → P n.

Proof fun n Hn P HO HSnat_ind P HO HS n Hn.

# Ordering

Definition le (n m : nat) : Prop :=
P : natProp, P n → ( p : nat, P pP (S p)) → P m.

This relation is reflexive and transitive, and closed under the successor function. Notice that these lemmas do not rely on the well-formedness assumption:

Lemma le_refl : n : nat, le n n.

Proof fun n P H _H.

Lemma le_trans : n1 n2 n3 : nat, le n1 n2le n2 n3le n1 n3.

Proof fun n1 n2 n3 H1 H2 P Hn1 HSH2 P (H1 P Hn1 HS) HS.

Lemma le_S : n m : nat, le n mle n (S m).

Proof fun n m H P Hn HSHS m (H P Hn HS).

The successor of a natural number cannot be less than or equal to zero:

Lemma le_Sn_O : n : nat, le (S n) Obot.

Proof
fun n H
H (fun kk Prop bot (fun _top)) top_intro (fun _ _top_intro).

Inversion lemma for (le n m):

Lemma le_inv :
n m : nat,
le n mor (eq nat n m) (ex nat (fun kand (le n k) (eq nat m (S k)))).

Proof.
intros n m H; apply H; clear H m.
apply or_inl; apply eq_refl.
intros m H; apply H; clear H; intro H.
apply or_inr; apply ex_intro with m; apply and_intro.
apply H; apply le_refl. apply H; apply eq_refl.
apply H; clear H; intros k H; apply H; clear H; intros H1 H2.
apply or_inr; apply ex_intro with (S k); apply and_intro.
apply le_S; assumption. apply H2; apply eq_refl.
Qed.

Lemma le_n_Sm :
n : nat,
wf_nat n
m : nat, wf_nat mle n (S m) → or (le n m) (eq nat n (S m)).

Proof.
intros n Hn m Hm H.
apply (le_inv n (S m) H); clear H; intro H.
apply or_inr; assumption.
apply H; clear H; intros k H.
apply H; clear H; intros H1 H2.
generalize (le_trans _ _ _ Hn H1).
intro Hk; change (wf_nat k) in Hk.
apply (eq_sym _ _ _ (eq_S_S m Hm k Hk H2)).
apply or_inl; assumption.
Qed.

## Strict ordering

Definition lt (n m : nat) : Prop := le (S n) m.

Lemma lt_n_Sn : n : nat, lt n (S n).

Proof fun nle_refl (S n).

Lemma lt_S : n m : nat, lt n mlt n (S m).

Proof fun n mle_S (S n) m.

Lemma lt_n_O : n : nat, lt n Obot.

Proof le_Sn_O.

Lemma lt_n_Sm :
n : nat,
wf_nat n
m : nat, wf_nat mlt n (S m) → or (lt n m) (eq nat n m).

Proof.
intros n Hn m Hm H.
apply (le_n_Sm (S n) (wf_nat_S n Hn) m Hm H); clear H; intro H.
apply or_inl; assumption. apply or_inr; apply eq_S_S; assumption.
Qed.