Extensibella: Extensibella Example: mtc:lambda

Language Specification

File: defs.sos

Module mtc:lambda

Builds on mtc:shared_declarations

e ::= ...
    | abs(string, ty, e)
    | app(e, e)
    | var(string)

v ::= ...
    | closure([(string, v)], string, e)

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


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


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


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



-------------------------------------- [E-Abs]
eval G abs(X, Ty1, E) closure(G, X, E)


eval G E1 closure(GC, X, Body)
eval G E2 V2
eval (X, V2)::GC Body V
------------------------------ [E-App]
eval G app(E1, E2) V


lookup G X V
--------------- [E-Var]
eval G var(X) V



typeOfCtx TG G
typeOf (X, Ty1)::TG E Ty2
-------------------------------------------- [VT-Closure]
valueType closure(G, X, E) arrowTy(Ty1, Ty2)



evalStep E1 E11
--------------------------------- [ES-App-Step1]
evalStep app(E1, E2) app(E11, E2)


value E1
evalStep E2 E21
--------------------------------- [ES-App-Step2]
evalStep app(E1, E2) app(E1, E21)


value E2
subst X E2 E1 E
---------------------------------- [ES-App-Subst]
evalStep app(abs(X, Ty, E1), E2) E



------------------- [V-Abs]
value abs(X, Ty, E)



------------------------------------- [S-Abs-Same]
subst X R abs(X, Ty, E) abs(X, Ty, E)


X != Y
subst X R E E1
-------------------------------------- [S-Abs-Diff]
subst X R abs(Y, Ty, E) abs(Y, Ty, E1)


subst X R E1 E11
subst X R E2 E21
----------------------------------- [S-App]
subst X R app(E1, E2) app(E11, E21)


------------------ [S-Var-Same]
subst X R var(X) R


X != Y
----------------------- [S-Var-Diff]
subst X R var(Y) var(Y)



-------------------------------------- [C-ArrowTy]
canon arrowTy(Ty1, Ty2) abs(X, Ty1, E)






---------------------------- [Proj-Abs]
|{e}- abs(X, Ty, E) ~~> nilE


-------------------------- [Proj-App]
|{e}- app(E1, E2) ~~> nilE


--------------------- [Proj-Var]
|{e}- var(X) ~~> nilE


------------------------------- [Proj-Closure]
|{v}- closure(G, X, E) ~~> nilV


---------------------------------- [Proj-ArrowTy]
|{ty}- arrowTy(Ty1, Ty2) ~~> nilTy

Reasoning

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

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

Module mtc:lambda.

Theorem typeOfCtx_lookups : forall TG EG X Ty V,
  typeOfCtx TG EG -> lookup TG X Ty -> lookup EG X V ->
  valueType V Ty. [Show Proof]

induction on 2. intros TOC LT LV. LT: case LT.
  %Lkp-Here
   LV: case LV.
     %Lkp-Here
      case TOC. search.
     %Lkp-Later
      case TOC. apply LV to _.
  %Lkp-Later
   LV: case LV.
     %Lkp-Here
      case TOC. apply LT to _.
     %Lkp-Later
      TOC: case TOC. apply IH to _ LT1 LV1. search.


Prove mtc:shared_declarations:type_preservation. [Show Proof]

%E-Abs
 case Ty. search.
%E-App
 Ty: case Ty. VT1: apply IH to _ Ty Ev1. VT2: apply IH to _ Ty1 Ev2.
 VTC: case VT1. apply IH to _ VTC1 Ev3. search.
%E-Var
 Ty: case Ty. apply typeOfCtx_lookups to _ Ty Ev1. search.


Prove mtc:shared_declarations:value_evalStep_false. [Show Proof]

%V-Abs
 case Ev.


Prove mtc:shared_declarations:subst_unique. [Show Proof]

%S-Abs-Same
 SB: case SB.
   %S-Abs-Same
    search.
   %S-Abs-Diff
    apply SB to _.
%S-Abs-Diff
 SB: case SB.
   %S-Abs-Same
    apply SA1 to _.
   %S-Abs-Diff
    apply IH to SA2 SB1. search.
%S-App
 SB: case SB. apply IH to SA1 SB. apply IH to SA2 SB1. search.
%S-Var-Same
 SB: case SB.
   %S-Var-Same
    search.
   %S-Var-Diff
    apply SB to _.
%S-Var-Diff
 SB: case SB.
   %S-Var-Same
    apply SA1 to _.
   %S-Var-Diff
    search.


Prove mtc:shared_declarations:evalStep_unique. [Show Proof]

%ES-App-Step1
 EvB: case EvB.
   %ES-App-Step1
    apply IH to EvA1 EvB. search.
   %ES-App-Step2
    apply value_evalStep_false to EvB EvA1.
   %ES-App-Subst
    case EvA1.
%ES-App-Step2
 EvB: case EvB.
   %ES-App-Step1
    apply value_evalStep_false to EvA1 EvB.
   %ES-App-Step2
    apply IH to EvA2 EvB1. search.
   %ES-App-Subst
    apply value_evalStep_false to EvB EvA2.
%ES-App-Subst
 EvB: case EvB.
   %ES-App-Step1
    case EvB.
   %ES-App-Step2
    apply value_evalStep_false to EvA1 EvB1.
   %ES-App-Subst
    apply subst_unique to EvA2 EvB1. search.


Prove mtc:shared_declarations:ty_lookup. [Show Proof]

%T-Abs
 apply IH to Ty1 _ with G2 = (X, Ty1)::G2.
   intros L'. L': case L'.
     %Lkp-Here
      search.
     %Lkp-Later
      apply L to L'1. search.
 search.
%T-App
 apply IH to Ty1 L. apply IH to Ty2 L. search.
%T-Var
 apply L to Ty1. search.


Prove mtc:shared_declarations:subst_preservation. [Show Proof]

%S-Abs-Same
 Ty: case Ty. apply ty_lookup to Ty _ with G2 = (X, Ty1)::TG.
   intros L. L: case L.
     %Lkp-Here
      search.
     %Lkp-Later
      L': case L1.
        %Lkp-Here
         apply L to _.
        %Lkp-Later
         search.
 search.
%S-Abs-Diff
 Ty: case Ty.
 Ty': apply ty_lookup to Ty _ with G2 = (X, XTy)::(Y, Ty1)::TG.
   intros L. L: case L.
     %Lkp-Here
      search.
     %Lkp-Later
      L': case L1.
        %Lkp-Here
         search.
        %Lkp-Later
         search.
 apply IH to Ty' S2 RTy. search.
%S-App
 Ty: case Ty. apply IH to Ty S1 RTy. apply IH to Ty1 S2 RTy. search.
%S-Var-Same
 Ty: case Ty. L: case Ty.
   %Lkp-Here
    backchain empty_ty_any.
   %Lkp-Later
    apply L to _.
%S-Var-Diff
 Ty: case Ty. L: case Ty.
   %Lkp-Here
    apply S1 to _.
   %Lkp-Later
    search.


Prove mtc:shared_declarations:evalStep_type_preservation. [Show Proof]

%ES-App-Step1
 Ty: case Ty. apply IH to Ty Ev1. search.
%ES-App-Step2
 Ty: case Ty. apply IH to Ty1 Ev2. search.
%ES-App-Subst
 Ty: case Ty. Ty: case Ty. apply subst_preservation to Ty Ev2 Ty1.
 search.


Prove mtc:shared_declarations:canonical_form. [Show Proof]

%V-Abs
 case Ty. search.


Prove mtc:shared_declarations:subst_is. [Show Proof]

%S-Abs-Same
 search.
%S-Abs-Diff
 Is: case IsE. apply IH to _ _ S2. search.
%S-App
 case IsE. apply IH to _ _ S1. apply IH to _ _ S2. search.
%S-Var-Same
 search.
%S-Var-Diff
 search.


Prove mtc:shared_declarations:evalStep_is. [Show Proof]

%ES-App-Step1
 case IsE. apply IH to _ Ev1. search.
%ES-App-Step2
 case IsE. apply IH to _ Ev2. search.
%ES-App-Subst
 Is: case IsE. case Is. apply subst_is to _ _ Ev2. search.


Prove mtc:shared_declarations:subst_total. [Show Proof]

%abs
 Or: apply is_string_eq_or_not to IsX IsE1. case Or.
   %X = S
    search.
   %X != S
    apply IH to IsE3 IsX IsR. search.
%app
 apply IH to IsE1 IsX IsR. apply IH to IsE2 IsX IsR. search.
%var
 Or: apply is_string_eq_or_not to IsX IsE1. case Or.
   %X = S
    search.
   %X != S
    search.


Prove mtc:shared_declarations:progress. [Show Proof]

%T-Abs
 search.
%T-App
 Is: case IsE. Or1: apply IH to _ Ty1. Or2: apply IH to _ Ty2.
 Ev1: case Or1.
   %value E1
    Ev2: case Or2.
      %value E2
       C: apply canonical_form to Ev1 Ty1. case C. IsAbs: case Is.
       apply subst_total to IsAbs2 IsAbs Is1. search.
      %evalStep E2 E'
       search.
   %evalStep E1 E'
    search.
%T-Var
 case Ty1.