# Library CL1

Require Import Framework.

Implicit Types rho : type_context.

Implicit Types x y z : var.

Implicit Types u v : inttype -> Prop.

Term syntax of combinatory logic
Inductive CL : Type :=
| S
| K
| app (a b : CL).

Implicit Types a b c : CL.
Coercion app : CL >-> Funclass.

Type syntax of CL

Inductive simpletype : Type :=
| base (x : var) : simpletype
| arr (A B : simpletype) : simpletype.
Notation "A --> B" := (arr A B).

Implicit Types A B C : simpletype.

Typing relation of CL: Note absence of context
Inductive CL_ty : CL -> simpletype -> Prop :=
| CLS A B C : CL_ty S ((A --> B --> C) --> (A --> B) --> A --> C)
| CLK A B : CL_ty K (A --> B --> A)
| CLapp a b A B : CL_ty a (A --> B) -> CL_ty b A -> CL_ty (a b) B.

Interpret variables according to valuation, arrow types as functional product
Fixpoint int_ty A sigma := match A with
| base x => sigma x
| arr A B => prod (int_ty A sigma) (int_ty B sigma)
end.

Notation "[[ A ]] sigma" := (int_ty A sigma) (at level 1).

Obviously, this yields realizor predicates
Lemma int_ty_rp : rp_preservation simpletype int_ty.
hnf.
induction T ; simpl ; auto using prod_realizable.
Qed.

Reduction relation of CL
Inductive cl_step : CL -> CL -> Prop :=
| cl_stepS a b c : cl_step (S a b c) (a c (b c))
| cl_stepK a b : cl_step (K a b) a
| cl_step_appL a b c : cl_step a b -> cl_step (a c) (b c)
| cl_step_appR a b c : cl_step b c -> cl_step (a b) (a c).

Compile to equivalent terms

Fixpoint CLC a := match a with
| S => Lam (Lam (Lam (TVar 2 (TVar 0) (TVar 1 (TVar 0)))))
| K => Lam (Lam (TVar 1))
| app a b => CLC a (CLC b)
end.

The compiler is consistent

Lemma CLC_c : compiler_consistency _ CLC cl_step.
intros a b. induction 1 ; simpl.
- econstructor 2. auto using step_appL, step_beta.
econstructor 2. eauto using step_appL, step_beta.
constructor. asimpl. eauto using step_beta_eq.
- econstructor 2. auto using step_appL, step_beta.
constructor. asimpl. eauto using step_beta_eq.
- now apply steps_appL.
- now apply steps_appR.
Qed.

The compiler is adequate

Lemma in_int_ty : cadequacy simpletype int_ty CL CLC (fun _ _ => CL_ty).
hnf.
simpl.
intros rho sigma rho_val sigma_val a A clt.
induction clt ; simpl in *.
- constructor ; eauto using int_IF, closure_filter ; intros vf Af.
constructor ; eauto using int_IF, closure_filter ; intros vg Ag.
constructor ; eauto using int_IF, closure_filter ; intros vx Ax.
assert (IFilter vf) by apply Af.
assert (IFilter vg) by apply Ag.
assert (IFilter vx) by eauto using only_filter, int_ty_rp.
assert (realizorPredicate [[C]]sigma) by auto using int_ty_rp.
assert (rpA : realizorPredicate [[A]]sigma) by auto using int_ty_rp.
assert (rpABC : realizorPredicate (prod [[A]]sigma (prod [[B]]sigma [[C]]sigma))) by auto using int_ty_rp, prod_realizable.
assert (rpAB : realizorPredicate (prod [[A]]sigma [[B]]sigma)) by auto using int_ty_rp, prod_realizable.
assert (exists (A : inttype), vf A) by now apply rpABC.
assert (exists (A : inttype), vg A) by now apply rpAB.
assert (exists (A : inttype), vx A) by now apply rpA.
rewrite <- ! int_lam, ! int_st, ! int_x ; auto using valid_up.
simpl.
now apply Af, Ag.
- constructor ; eauto using int_IF, closure_filter ; intros vf Af.
constructor ; eauto using int_IF, closure_filter ; intros vg Ag.
assert (rpA : realizorPredicate [[A]]sigma) by auto using int_ty_rp.
assert (rpB : realizorPredicate [[B]]sigma) by auto using int_ty_rp.
assert (IFilter vf) by now apply rpA.
assert (IFilter vg) by now apply rpB.
assert (exists (A : inttype), vf A) by now apply rpA.
assert (exists (A : inttype), vg A) by now apply rpB.
rewrite <- ! int_lam, ! int_x ; auto using valid_up.
- assert (rpB : realizorPredicate [[B]]sigma) by auto using int_ty_rp.
rewrite ! int_st ; auto.
now apply IHclt1.
Qed.

The CL typing has no context and thus ignores the type contexts and valuations

Lemma CL_valid : validation _ _ CL_ty (fun _ _ => CL_ty).
split.
- intros ty. exists top_rho, top_sigma. intuition ; eauto 6 using top_rho_valid, top_sigma_valuation.
- intros [? [? [? [? tyt] ] ] ]. auto.
Qed.

CL terminates

Corollary CL_stlc t A : CL_ty t A -> TSN _ cl_step t.
apply tsn with int_ty CLC (fun _ _ => CL_ty) ; auto using in_int_ty, int_ty_rp, CL_valid, CLC_c.
Qed.