Library Encoding
Fixpoint size (t : term) :=
match t with
| var n => 1
| app s t => size s + size t
| lam s => 1 + size s
end.
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.
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.
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.
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.
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.