Library Nat
Require Export Tactics.
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.
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.
- eapply Add_rec_0.
- now rewrite Add_rec_S, IHn, Succ_correct.
Qed.
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.