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 → (X → X) → X.
Definition O : nat := fun X x f ⇒ x.
Definition S (n : nat) : nat := fun X x f ⇒ f (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 : nat → Prop, P O → (∀ p : nat, P p → P (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 := (X → X → X) → X.
Definition pair (X : Typ0) (x y : X) : sqr X := fun f ⇒ f 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 _ y ⇒ y).

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 : X → X) (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 f ⇒ fst 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 n ⇒ eq_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 n → eq 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 HS ⇒ HO.

Second axiom of Peano

Lemma wf_nat_S : ∀ n : nat, wf_nat n → wf_nat (S n).

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

Third axiom of Peano

Lemma eq_S_O : ∀ n : nat, wf_nat n → eq nat (S n) O → bot.

Proof fun n _ H ⇒ H (fun p ⇒ p Prop bot (fun _ ⇒ top)) top_intro.

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

Proof fun n _ H ⇒ H (fun p ⇒ p 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 p → eq 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 : nat → Prop,
P O →
(∀ p : nat, wf_nat p → P p → P (S p)) →
∀ n : nat, wf_nat n → P 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 : nat → Prop,
P O → (∀ p : nat, wf_nat p → P p → P (S p)) → P n.

Proof fun n Hn P HO HS ⇒ nat_ind P HO HS n Hn.

Ordering

Definition le (n m : nat) : Prop :=
∀ P : nat → Prop, P n → (∀ p : nat, P p → P (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 n2 → le n2 n3 → le n1 n3.

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

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

Proof fun n m H P Hn HS ⇒ HS 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) O → bot.

Proof
fun n H ⇒
H (fun k ⇒ k Prop bot (fun _ ⇒ top)) top_intro (fun _ _ ⇒ top_intro).

Inversion lemma for (le n m):

Lemma le_inv :
∀ n m : nat,
le n m → or (eq nat n m) (ex nat (fun k ⇒ and (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 m → le 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 n ⇒ le_refl (S n).

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

Proof fun n m ⇒ le_S (S n) m.

Lemma lt_n_O : ∀ n : nat, lt n O → bot.

Proof le_Sn_O.

Lemma lt_n_Sm :
∀ n : nat,
wf_nat n →
∀ m : nat, wf_nat m → lt 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.