Library IZF.IZF_nat
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).
The type of Church numerals in Typ1
Definition of natural numbers
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.
The predecessor function
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:
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:
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.
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.
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.
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.
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.