# Library Encoding

Require Export Bool Nat.

# Size of terms

Fixpoint size (t : term) :=
match t with
| var n => 1
| app s t => size s + size t
| lam s => 1 + size s
end.

# Properties of the encoding for nat

Lemma enc_injective m n : enc m = enc n -> m = n.

Proof.

revert n; induction m; intros n; destruct n; inversion 1; eauto.

Qed.

Fixpoint unenc (s : term) :=
match s with
| lam (lam #1) => Some 0
| lam (lam (app #0 s)) => match unenc s with Some n => Some (S n) | x=>x end
| _ => None
end.

Lemma unenc_correct m : (unenc (enc m)) = Some m.

Proof.

induction m; simpl; now try rewrite IHm.

Qed.

Lemma unenc_correct2 t n : unenc t = Some n -> enc n = t.

Proof.

revert n.
eapply (size_induction (f := size) (p := (fun t => forall n, unenc t = Some n -> enc n = t))). clear t. intros t IHt n H.
destruct t; try now inv H.

destruct t; try now inv H.

destruct t; try now inv H.

destruct n0; try now inv H.
destruct n0; try now inv H.
destruct t1; try now inv H.
destruct n0; try now inv H.
simpl in H.
destruct (unenc t2) eqn:A.
specialize (IHt t2).

assert (B : size t2 < size (Î» (Î» #0 t2))).
simpl. omega.
eapply IHt in B.

destruct n.
inv H. inversion H. subst n0.
simpl.
repeat f_equal. eassumption. eassumption. inv H.
Qed.

Lemma dec_enc t : dec (exists n, t = enc n).

Proof.

destruct (unenc t) eqn:H.

- left.
exists n. now eapply unenc_correct2 in H.
- right.
intros [n A]. rewrite A in H. rewrite unenc_correct in H. inv H.
Qed.

# Encoding for terms

Fixpoint tenc (t : term) :=
lam ( lam ( lam (
match t with
| var n => (var 2) (enc n)
| app s t => (var 1) (tenc s) (tenc t)
| lam s => (var 0) (tenc s)
end
))).

Lemma tenc_cls s : closed (tenc s).

Proof.

induction s; intros k u; simpl.

- now rewrite enc_cls.

- now rewrite IHs1, IHs2.

- now rewrite IHs.

Qed.

Lemma tenc_lam s : lambda (tenc s).

Proof.

destruct s; eexists; reflexivity.

Qed.

Hint Resolve tenc_lam tenc_cls : cbv.

Hint Rewrite tenc_cls : cbv.

Lemma tenc_injective s t : tenc s = tenc t -> s = t.

Proof.

revert t; induction s; intros t; destruct t; inversion 1.

- eauto using enc_injective.

- erewrite IHs1, IHs2; eauto.

- erewrite IHs; eauto.

Qed.

Lemma tenc_inj s t : tenc s == tenc t -> s = t.

Proof.

intros.
destruct (tenc_lam t), (tenc_lam s). rewrite H0, H1 in H.
eapply eq_lam in H.
eapply tenc_injective. congruence.
Qed.

# Interalized encoding combinators

Definition Var : term := .\"n"; .\"v","a","l"; "v" "n".

Definition App : term := .\"s","t"; .\"v","a","l"; "a" "s" "t".

Definition Lam : term := .\"s"; .\"v","a","l"; "l" "s".

Hint Unfold App Lam Var : cbv.

Lemma App_correct s t : App (tenc s) (tenc t) == tenc (s t).

Proof.

crush.

Qed.

Lemma Lam_correct s : Lam (tenc s) == tenc (lam s).

Proof.

crush.

Qed.

Lemma Var_correct n : Var (enc n) == tenc (#n).

Proof.

crush.

Qed.

# Interalized encoding of natural numbers

Definition P := R( .\"P", "n"; "n" !(tenc Zero) (.\"n"; !Lam (!Lam (!App !(tenc 0) ("P" "n"))))).

Hint Unfold P : cbv.

Lemma P_correct n : P (enc n) == tenc(enc n).

Proof.

induction n; crush.

Qed.

# Interalized term encoding

Definition Q := R( .\"Q", "s"; "s" (.\"n"; !Lam (!Lam (!Lam (!App !(tenc 2) (!P "n")))))
(.\"s","t"; !Lam (!Lam (!Lam (!App (!App !(tenc 1) ("Q" "s")) ("Q" "t")))))
(.\"s"; !Lam (!Lam (!Lam (!App !(tenc 0) ("Q" "s"))))) ).

Lemma Q_rec_var n : Q (tenc (# n)) == Lam (Lam (Lam (App (tenc #2) (P (enc n))))).

Proof.

crush.

Qed.

Lemma Q_rec_app s t : Q (tenc (app s t)) == Lam (Lam (Lam (App (App (tenc #1) (Q (tenc s))) (Q (tenc t))))).

Proof.

transitivity ((Lam (Lam (Lam (App (App (tenc #1) ((lam (Q #0)) (tenc s))) ((lam (Q #0)) (tenc t))))))).
crush.
now rewrite !Eta; value.

Qed.

Lemma Q_rec_lam s : Q (tenc (lam s)) == Lam (Lam (Lam (App (tenc #0) (Q (tenc s))))).

Proof.

transitivity (Lam (Lam (Lam (App (tenc #0) ((lam (Q #0)) (tenc s)))))).
crush.
now rewrite Eta; value.

Qed.

Lemma Q_correct s : Q (tenc s) == tenc(tenc s).

Proof.

induction s.

- rewrite Q_rec_var, P_correct.
crush.
- rewrite Q_rec_app, IHs1, IHs2.
crush.
- rewrite Q_rec_lam, IHs.
crush.
Qed.