%{
Adapted from the case study on [[Typed combinators soundness and completeness]].

== Syntax ==

}%

% lambda calculus

term : type.                    %name term M x.

app : term -> term -> term.
lam : (term -> term) -> term.


% combinator calculus

comb : type.                    %name comb A y.

s : comb.
k : comb.
i : comb.
capp : comb -> comb -> comb.


%{

== Translation ==

}%

% bracket abstraction

bracket : (comb -> comb) -> comb -> type.
%mode bracket +A -A'.

bracket/var : bracket ([y] y) i.

bracket/i : bracket ([y] i) (capp k i).
bracket/k : bracket ([y] k) (capp k k).
bracket/s : bracket ([y] s) (capp k s).

bracket/app : bracket ([y] capp (A y) (B y)) (capp (capp s A') B')
               <- bracket ([y] A y) A'
               <- bracket ([y] B y) B'.

%block bracket-block : block {y:comb} {bracket/y:bracket ([z] y) (capp k y)}.

%worlds (bracket-block) (bracket _ _).
%total A (bracket A _).


% translation

translate : term -> comb -> type.
%mode translate +M -A.

translate/app : translate (app M N) (capp A B)
                 <- translate M A
                 <- translate N B.

translate/lam : translate (lam ([x] M x)) A'
                 <- ({x} {y} bracket ([z] y) (capp k y)
                            -> translate x y
                            -> translate (M x) (A y))
                 <- bracket ([y] A y) A'.

%block translate-block
        : block {x:term} {y:comb}
                {bracket/y: bracket ([z] y) (capp k y)}
                {translate/x: translate x y}.
%worlds (translate-block) (translate _ _).
%total M (translate M _).

%{

== Equational theory ==

}%

% lambda term equality

teq : term -> term -> type.

% beta
teq/beta : teq (app (lam ([x] M x)) N) (M N).

% extensionality (eta)
teq/ext : teq M M'
           <- ({x:term} teq (app M x) (app M' x)).

% compatibilities
teq/app : teq (app M N) (app M' N')
           <- teq M M'
           <- teq N N'.

teq/lam : teq (lam ([x] M x)) (lam ([x] M' x))
           <- ({x:term} teq (M x) (M' x)).

% equivalence
teq/refl : teq M M.

teq/symm : teq M M'
            <- teq M' M.

teq/trans : teq M M'
             <- teq M N
             <- teq N M'.

%block term-block : block {x:term}.
%worlds (term-block) (teq _ _).


% combinator equality

ceq : comb -> comb -> type.

% betas
ceq/i : ceq (capp i A) A.
ceq/k : ceq (capp (capp k A) _) A.
ceq/s : ceq (capp (capp (capp s A) B) C) (capp (capp A C) (capp B C)).

% extensionality
ceq/ext : ceq A A'
           <- ({y:comb} ceq (capp A y) (capp A' y)).

% compatibility
ceq/app : ceq (capp A B) (capp A' B')
           <- ceq A A'
           <- ceq B B'.

% equivalence
ceq/refl : ceq A A.

ceq/symm : ceq A A'
            <- ceq A' A.

ceq/trans : ceq A A'
             <- ceq A B
             <- ceq B A'.

%block comb-block : block {y:comb}.
%worlds (comb-block) (ceq _ _).



%{

== Correctness of the translation ==

}%

% substitution lemma

subst : bracket ([y] A y) A' -> {C:comb} ceq (capp A' C) (A C) -> type.
%mode subst +Dbrack +C -Dceq.

- : subst (bracket/var : bracket ([y] y) i)
          C
          (ceq/i : ceq (capp i C) C).

- : subst (bracket/i : bracket ([y] i) (capp k i))
          C
          (ceq/k : ceq (capp (capp k i) C) i).

- : subst (bracket/k : bracket ([y] k) (capp k k))
          C
          (ceq/k : ceq (capp (capp k k) C) k).

- : subst (bracket/s : bracket ([y] s) (capp k s))
          C
          (ceq/k : ceq (capp (capp k s) C) s).

- : subst (bracket/app (Dbrack2 : bracket ([y] B y) B')
                       (Dbrack1 : bracket ([y] A y) A'))
          C
          (ceq/trans
              (ceq/app Dceq2 Dceq1)
              ceq/s)
     <- subst Dbrack1 C (Dceq1 : ceq (capp A' C) (A C))
     <- subst Dbrack2 C (Dceq2 : ceq (capp B' C) (B C)).

%block subst-block : block {y:comb} {dbrack: bracket ([z] y) (capp k y)}
                           {thm-subst: {C:comb} subst dbrack C ceq/k}.
%worlds (subst-block) (subst _ _ _).
%total D (subst D _ _).