Library Nat

Encoding of natural numbers

Fixpoint enc (n : nat) :=
  match n with
  | 0 ⇒ # 1
  | S n# 0 (enc n)

Lemma enc_lam m :
  lambda (enc m).

Lemma enc_cls m :
  closed (enc m).

Lemma enc_proc m :
  proc (enc m).

*Procedures representing zero and the successor-function

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

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


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

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


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

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

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

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


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

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

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

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