Extensibella Example: walkthrough:host

Language Specification

File: def.sos

[Reduce File] [Raw File] 
Module walkthrough:host

tm ::= var(string)
     | abs(string, ty, tm)
     | app(tm, tm)

Projection tm : [(string, ty)]

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

Projection ty :



Judgment eval : tm* tm
Judgment subst : string tm tm* tm
Judgment value : tm*

eval T1 T11
----------------------------- [E-App-Step1]
eval app(T1, T2) app(T11, T2)


value T1
eval T2 T21
----------------------------- [E-App-Step2]
eval app(T1, T2) app(T1, T21)


value T2
subst X T2 Body V
-------------------------------- [E-App-Subst]
eval app(abs(X, Ty, Body), T2) V


Extensibella_Stand_In {
  Ctx |{tm}- T ~~> T_T
  eval T_T T2
  -------------------- [E-Q]
  eval T T1
}



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


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


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


------------------------------------- [S-Abs-Eq]
subst X R abs(X, Ty, B) abs(X, Ty, B)


subst X R T1 S1
subst X R T2 S2
--------------------------------- [S-App]
subst X R app(T1, T2) app(S1, S2)



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



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

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


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


typeOf Ctx T1 arrowTy(Ty1, Ty2)
typeOf Ctx T2 Ty1
------------------------------- [T-App]
typeOf Ctx app(T1, T2) Ty2

Reasoning

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

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

Module walkthrough:host.

Extensible_Theorem
  typeOf_unique : forall Ctx T TyA TyB,
    TyA : typeOf Ctx T TyA ->
    TyB : typeOf Ctx T TyB ->
    TyA = TyB
  on TyA. [Show Proof]



Extensible_Theorem
  ty_lookup : forall Ctx1 Ctx2 T Ty,
    Ty : typeOf Ctx1 T Ty ->
    L : (forall X XTy, lookup Ctx1 X XTy -> lookup Ctx2 X XTy) ->
    typeOf Ctx2 T Ty
  on Ty. [Show Proof]



Theorem empty_ty_any : forall T Ty Ctx,
  typeOf [] T Ty -> typeOf Ctx T Ty. [Show Proof]



Extensible_Theorem
  subst_type_preservation : forall T Ctx X XTy Ty R S,
    TTy : typeOf ((X, XTy)::Ctx) T Ty ->
    S : subst X R T S ->
    RTy : typeOf [] R XTy ->
    typeOf Ctx S Ty
  on S. [Show Proof]



Extensible_Theorem
  type_preservation : forall T Ty T',
    Ty : typeOf [] T Ty ->
    Ev : eval T T' ->
    typeOf [] T' Ty
  on Ev. [Show Proof]



Projection_Constraint proj_type_same : forall G T Ty T_T,
  G |{tm}- T ~~> T_T -> typeOf G T Ty -> typeOf G T_T Ty.


Ext_Size eval T T'.

Proj_Rel eval T T'.

Ext_Ind forall G T T' Ty, eval T T' with Ty : typeOf G T Ty. [Show Proof]
Back to example home