# Library Nat

Require Export Tactics.

# Encoding of natural numbers

Fixpoint enc (n : nat) :=
lam(lam
match n with
| 0 => # 1
| S n => # 0 (enc n)
end).

Lemma enc_lam m :
lambda (enc m).

Proof.

destruct m; eexists; reflexivity.

Qed.

Lemma enc_cls m :
closed (enc m).

Proof.

induction m; intros n u; simpl; try rewrite_closed; reflexivity.

Qed.

Hint Resolve enc_cls enc_lam : cbv.

Hint Rewrite enc_cls : cbv.

Lemma enc_proc m :
proc (enc m).

Proof.

split; eauto with cbv.

Qed.

*Procedures representing zero and the successor-function

Definition Zero : term := .\"z","s"; "z".

Definition Succ : term := .\"n","z","s"; "s" "n".

Hint Unfold Zero Succ : cbv.

Lemma Succ_correct n : Succ (enc n) == enc (S n).

Proof.

crush.

Qed.

# Predecessor

Definition Pred : term := .\"n"; "n" !Zero (.\"n"; "n").

Hint Unfold Pred : cbv.

Lemma Pred_correct n : Pred (enc n) == enc (pred n).

Proof.

destruct n; crush.

Qed.

Definition Add := R (.\ "a", "n", "m"; "n" "m" (.\"n"; !Succ ("a" "n" "m"))).

Hint Unfold Add : cbv.

Lemma Add_rec_0 m :
Add Zero (enc m) == enc m.

Proof.

crush.

Qed.

Hint Unfold convert convert'.

Lemma Add_rec_S n m :
Add (enc (S n)) (enc m) == Succ (Add (enc n) (enc m)).

Proof.

crush.

Qed.

Lemma Add_correct n m :
Add (enc n) (enc m) == enc (n + m).

Proof.

revert m; induction n; intros m.

- now rewrite Add_rec_S, IHn, Succ_correct.

Qed.

# Multiplication

Definition Mul := R(.\ "Mul", "m", "n"; "m" !Zero (.\ "m"; !Add "n" ("Mul" "m" "n"))).

Hint Unfold Mul : cbv.

Lemma Mul_rec_0 m :
Mul Zero (enc m) == Zero.

Proof.

crush.

Qed.

Lemma Mul_rec_S n m :
Mul (enc (S n)) (enc m) == (Add (enc m)) (((lam (Mul #0)) (enc n)) (enc m)).

Proof.

crush.

Qed.

Lemma Mul_correct m n :
Mul (enc n) (enc m) == enc (n * m).

Proof.

induction n.

- eapply Mul_rec_0.

- now rewrite Mul_rec_S, Eta, IHn, Add_correct; value.

Qed.