Extensibella: Extensibella Example: lambda

Language Specification

File: syntax.sos

Module lambda_calculus:typing

Builds on lambda_calculus:host

e ::= ...
    | tyabs(string, ty, e)

ty ::= intTy
     | arrowTy(ty, ty)

Projection ty :


----------------------------------------- [Proj-Tyabs]
|{e}- tyabs(X, Ty, Body) ~~> abs(X, Body)




------------------------------------ [E-Tyabs]
eval tyabs(X, Ty, Body) abs(X, Body)



----------------------------------------- [S-Tyabs-Eq]
subst X R tyabs(X, Ty, Body) abs(X, Body)


X != Y
subst X R Body B
-------------------------------------- [S-Tyabs-NEq]
subst X R tyabs(Y, Ty, Body) abs(Y, B)

File: typing.sos

[Reduce File] [Raw File]

Module lambda_calculus:typing

Judgment typeOf : [(string, ty)] e* ty

lookup G X Ty
------------------ [T-Var]
typeOf G var(X) Ty


typeOf (X, Ty1)::G Body Ty2
--------------------------------------- [T-Abs]
typeOf G abs(X, Body) arrowTy(Ty1, Ty2)


typeOf (X, Ty1)::G Body Ty2
---------------------------------------------- [T-Tyabs]
typeOf G tyabs(X, Ty1, Body) arrowTy(Ty1, Ty2)


typeOf G E1 arrowTy(Ty1, Ty2)
typeOf G E2 Ty1
----------------------------- [T-App]
typeOf G app(E1, E2) Ty2


---------------------- [T-Int]
typeOf G intE(I) intTy


typeOf G E1 intTy
typeOf G E2 intTy
--------------------------- [T-Plus]
typeOf G plus(E1, E2) intTy


|{e}- E ~~> E_T
typeOf G E_T Ty
--------------- [T-D]*
typeOf G E Ty

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module lambda_calculus:typing.


Prove_Constraint lambda_calculus:host:proj_is. [Show Proof]

%tyabs
 case Hyp1. search.


Add_Proj_Rel lambda_calculus:host:is_e.

Prove_Ext_Ind lambda_calculus:host:is_e. [Show Proof]

%tyabs
 apply IH to R3. search.


Prove_Constraint lambda_calculus:host:proj_same. [Show Proof]

%tyabs
 case Hyp1. search.


Prove lambda_calculus:host:subst_exists. [Show Proof]

%tyabs
 Or: apply is_string_eq_or_not to IsX IsE1. Eq: case Or.
   %X = S
    search.
   %X != S
    apply IH to IsE3 IsX IsR. search.


Prove lambda_calculus:host:subst_is. [Show Proof]

%S-Tyabs-Eq
 case IsE. search.
%S-Tyabs-NEq
 Is: case IsE. apply IH to _ _ _ S2. search.


Prove lambda_calculus:host:eval_is. [Show Proof]

%E-Tyabs
 Is: case IsE. search.


Prove lambda_calculus:host:subst_unique. [Show Proof]

%S-Tyabs-Eq
 SB: case SB.
   %S-Tyabs-Eq
    search.
   %S-Tyabs-NEq
    apply SB to _.
%S-Tyabs-NEq
 SB: case SB.
   %S-Tyabs-Eq
    apply SA1 to _.
   %S-Tyabs-NEq
    Is: case IsE. apply IH to _ _ _ SA2 SB1. search.


Prove lambda_calculus:host:eval_unique. [Show Proof]

%E-Tyabs
 case EvB. search.


Prove_Constraint lambda_calculus:host:proj_subst. [Show Proof]

%tyabs
 S: case S.
   %S-Tyabs-Eq
    search.
   %S-Tyabs-NEq
    search.

Prove_Constraint lambda_calculus:host:proj_subst_same. [Show Proof]

%tyabs
 S: case S.
   %S-Tyabs-Eq
    S': case S'.
      %S-Abs-Eq
       search.
      %S-Abs-NEq
       apply S' to _.
   %S-Tyabs-NEq
    S': case S'.
      %S-Abs-Eq
       apply S to _.
      %S-Abs-NEq
       case IsE. apply subst_unique to _ _ _ S1 S'1. search.


Prove_Constraint lambda_calculus:host:proj_eval. [Show Proof]

%tyabs
 case Ev. search.

Prove_Constraint lambda_calculus:host:proj_eval_same. [Show Proof]

%tyabs
 case Ev. case Ev'. search.


Add_Ext_Size lambda_calculus:host:eval.
Add_Proj_Rel lambda_calculus:host:eval.


Prove_Ext_Ind lambda_calculus:host:eval. [Show Proof]

%E-Tyabs
 search.


Extensible_Theorem
  type_weakening : forall G E Ty G',
    IsE : is_e E ->
    Ty : typeOf G E Ty ->
    Lkp : (forall X XTy, lookup G X XTy -> lookup G' X XTy) ->
    typeOf G' E Ty
  on Ty. [Show Proof]

%T-Var
 apply Lkp to Ty1. search.
%T-Abs
 Is: case IsE. apply IH to _ Ty1 _ with G' = (X, Ty1)::G'.
   intros L. L: case L.
     %Lkp-Here
      search.
     %Lkp-Later
      apply Lkp to L1. search.
 search.
%T-Tyabs
 Is: case IsE. apply IH to _ Ty1 _ with G' = (X, Ty1)::G'.
   intros L. L: case L.
     %Lkp-Here
      search.
     %Lkp-Later
      apply Lkp to L1. search.
 search.
%T-App
 Is: case IsE. apply IH to _ Ty1 _. apply IH to _ Ty2 _. search.
%T-Int
 search.
%T-App
 case IsE. apply IH to _ Ty1 Lkp. apply IH to _ Ty2 Lkp. search.
%T-D
 apply proj_is to Ty1 IsE. apply IH to _ Ty2 _. search.

Theorem any_ctx : forall E Ty G,
  is_e E -> typeOf [] E Ty -> typeOf G E Ty. [Show Proof]

intros Is Ty. backchain type_weakening with G = []. intros L. case L.


Extensible_Theorem
  tyabs_or_not : forall E,
    IsE : is_e E ->
    (exists X Ty B, E = tyabs X Ty B) \/
    ((exists X Ty B, E = tyabs X Ty B) -> false)
  on IsE. [Show Proof]

%var
 right. intros E. case E.
%abs
 right. intros E. case E.
%app
 right. intros E. case E.
%int
 search.
%plus
 search.
%tyabs
 search.
%other
 right. intros E. case E.


Extensible_Theorem
  subst_type_preservation : forall X R E S G TyE TyX G',
    IsE : is_e E ->
    IsX : is_string X ->
    IsR : is_e R ->
    S : subst X R E S ->
    TyE : typeOf G E TyE ->
    TyR : typeOf [] R TyX ->
    Lkp : lookup G X TyX ->
    Slct : select (X, TyX) G' G ->
    typeOf G' S TyE
  on TyE. [Show Proof]

%T-Var
 S: case S.
   %T-Var-Eq
    apply any_ctx to _ TyR with G = G'.
    apply lookup_unique to Lkp TyE1. search.
   %T-Var-NEq
    NEq: assert X1 = X -> false. intros E. case E. backchain S.
    apply select_lookup to TyE1 Slct NEq. search.
%T-Abs
 Is: case IsE. S: case S.
   %T-Abs-Eq
    L: assert forall Z ZTy,
          lookup ((X1, Ty1)::G) Z ZTy -> lookup ((X1, Ty1)::G') Z ZTy.
      intros L. L: case L.
        %Lkp-Here
         search.
        %Lkp-Later
         NEq: assert Z = X1 -> false. intros E. case E. backchain L.
         apply select_lookup to L1 Slct NEq. search.
    apply type_weakening to _ TyE1 L. search.
   %T-Abs-NEq
    assert X1 = X -> false. intros E. case E. backchain S.
    apply IH to _ _ _ S1 TyE1 _ _ _ with G' = (X1, Ty1)::G'. search.
%T-Tyabs
 Is: case IsE. S: case S.
   %T-Abs-Eq
    L: assert forall Z ZTy,
          lookup ((X1, Ty1)::G) Z ZTy -> lookup ((X1, Ty1)::G') Z ZTy.
      intros L. L: case L.
        %Lkp-Here
         search.
        %Lkp-Later
         NEq: assert Z = X1 -> false. intros E. case E. backchain L.
         apply select_lookup to L1 Slct NEq. search.
    apply type_weakening to _ TyE1 L. search.
   %T-Abs-NEq
    assert X1 = X -> false. intros E. case E. backchain S.
    apply IH to _ _ _ S1 TyE1 _ _ _ with G' = (X1, Ty1)::G'. search.
%T-App
 Is: case IsE. S: case S. apply IH to _ _ _ S TyE1 _ _ _.
 apply IH to _ _ _ S1 TyE2 _ _ _. search.
%T-Int
 case S. search.
%T-Plus
 case IsE. S: case S. apply IH to _ _ _ S TyE1 _ _ _.
 apply IH to _ _ _ S1 TyE2 _ _ _. search.
%T-D
 ST: apply proj_subst to TyE1 _ _ _ S. apply proj_is to TyE1 _.
 apply proj_subst_same to TyE1 _ _ _ S ST.
 apply IH to _ _ _ ST TyE2 _ _ _. search.


Extensible_Theorem
  type_preservation : forall E Ty V,
    IsE : is_e E ->
    Ty : typeOf [] E Ty ->
    Ev : eval E V ->
    typeOf [] V Ty
  on Ev. [Show Proof]

%E-Abs
 search.
%E-App
 Is: case IsE. Ty: case Ty. AbsTy: apply IH to _ Ty Ev1.
 Ty': case AbsTy. apply IH to _ Ty1 Ev2. apply eval_is to _ Ev2.
 IsAbs: apply eval_is to _ Ev1. case IsAbs.
 TyB: apply subst_type_preservation to _ _ _ Ev3 Ty' _ _ _.
 apply subst_is to _ _ _ Ev3. apply IH to _ TyB Ev4. search.
%E-Int
 case Ty. search.
%E-Plus
 case Ty. search.
%E-Tyabs
 case Ty. search.
%E-Q
 Ty: case Ty. apply proj_same to Ev1 Ty. apply proj_is to Ty _.
 apply IH to _ Ty1 Ev2. search.

/*
  Note we do not have type uniqueness because abs(X, var(X)) could
  have any arrow type.

  We also cannot prove progress because, in the generic case,
  we could show the projection would evaluate, but we do not have a
  projection constraint that would allow us to lift this back to the
  new syntax.
*/

Extensibella Example: lambda_calculus:typing

Language Specification

File: syntax.sos

File: typing.sos

Reasoning