Extensibella Example: stlc:host

Language Specification

File: def.sos

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

tm ::= var(string)
     | abs(string, ty, tm)
     | app(tm, tm)
     | num(int)
     | plus(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


eval T1 T11
------------------------------- [E-Plus-Step1]
eval plus(T1, T2) plus(T11, T2)


value T1
eval T2 T21
------------------------------- [E-Plus-Step2]
eval plus(T1, T2) plus(T1, T21)


I1 + I2 = I
---------------------------------- [E-Plus-Add]
eval plus(num(I1), num(I2)) num(I)



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)


----------------------- [S-Num]
subst X R num(I) num(I)


subst X R T1 S1
subst X R T2 S2
----------------------------------- [S-Plus]
subst X R plus(T1, T2) plus(S1, S2)



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


------------ [V-Num]
value num(I)



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


----------------------- [T-Num]
typeOf Ctx num(I) intTy


typeOf Ctx T1 intTy
typeOf Ctx T2 intTy
----------------------------- [T-Plus]
typeOf Ctx plus(T1, T2) intTy



/*a value has the form expected for a type
  this is purely for proof purposes; do not use it to define any
     actual language relations*/
Judgment canonicalForm : ty* tm

-------------------------- [CF-Int]
canonicalForm intTy num(I)


---------------------------------------------- [CF-Arrow]
canonicalForm arrowTy(Ty1, Ty2) abs(X, Ty1, B)

Reasoning

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

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

Module stlc:host.

Theorem lookup_ty_is : forall Ctx X Ty,
  is_list (is_pair is_string is_ty) Ctx -> lookup Ctx X Ty ->
  is_ty Ty. [Show Proof]



Projection_Constraint
  proj_ty_is : forall Ty Ty',
    Proj : |{ty}- Ty ~~> Ty' ->
    IsTy : is_ty Ty ->
    is_ty Ty'.


/*
  This goes before proj_is because projection might depend on the
  context, and thus the type, so we might need this to prove that.
*/
Extensible_Theorem
  type_is : forall Ctx T Ty,
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    IsT : is_tm T ->
    Ty : typeOf Ctx T Ty ->
    is_ty Ty
  on Ty. [Show Proof]



Projection_Constraint
  proj_is : forall Ctx T T',
    Proj : Ctx |{tm}- T ~~> T' ->
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    IsT : is_tm T ->
    is_tm T'.


Extensible_Theorem
  type_unique : forall Ctx T TyA TyB,
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    IsT : is_tm T ->
    TyA : typeOf Ctx T TyA ->
    TyB : typeOf Ctx T TyB ->
    TyA = TyB
  on TyA. [Show Proof]



Projection_Constraint proj_ty_unique : forall Ty TyA TyB,
  |{ty}- Ty ~~> TyA -> |{ty}- Ty ~~> TyB -> is_ty Ty -> TyA = TyB.


Projection_Constraint proj_tm_unique : forall Ctx T TA TB,
  Ctx |{tm}- T ~~> TA -> Ctx |{tm}- T ~~> TB ->
  is_tm T -> is_list (is_pair is_string is_ty) Ctx -> TA = TB.


Extensible_Theorem
  subst_is : forall X R T S,
    IsT : is_tm T ->
    IsX : is_string X ->
    IsR : is_tm R ->
    S : subst X R T S ->
    is_tm S
  on S. [Show Proof]



Extensible_Theorem
  eval_is : forall T T',
    IsT : is_tm T ->
    Ev : eval T T' ->
    is_tm T'
  on Ev. [Show Proof]



Extensible_Theorem
  subst_unique : forall X R T VA VB,
    SA : subst X R T VA ->
    SB : subst X R T VB ->
    VA = VB
  on SA. [Show Proof]



Extensible_Theorem
  value_eval_false : forall T V,
    Val : value T ->
    Ev : eval T V ->
    false
  on Val. [Show Proof]



Extensible_Theorem
  eval_unique : forall T VA VB,
    EvA : eval T VA ->
    EvB : eval T VB ->
    VA = VB
  on EvA. [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]



Extensible_Theorem
  subst_total : forall X R T,
    IsT : is_tm T ->
    IsX : is_string X ->
    %explicit decision subst can only use R, not examine it
    %including `is_tm R` could permit tricks to look at it
    exists S, subst X R T S
  on IsT. [Show Proof]



/*
  We can prove a single canonical form lemma by having an extensible
  canonical form relation, then showing it holds for each new type
  introduced in each module.

  We can introduce and prove the canonical form lemmas for integers
  and arrow types (shown below as fixed theorems) here and prove them
  without any problem.  However, if we try to introduce and prove a
  canonical form lemma in an extension, we need to show it also holds
  for a generic construct from another extension.  We can't do that in
  our language because another extension might have introduced a value
  construct having any type from another extension.  While a relation
  to pull apart the form solves that problem, we still don't have a
  way to prove the extension-introduced form relation would hold
  because, in the generic case, the projection might not have the
  same type and then the IH would be unhelpful.

  In summary, directly proving canonical form lemmas for
  extension-introduced types is not possible here, but proving them
  indirectly through this theorem is possible.
 */
Extensible_Theorem
  canonical_forms : forall V Ty,
    V : value V ->
    Ty : typeOf [] V Ty ->
    canonicalForm Ty V
  on V. [Show Proof]


%a couple of useful special cases of canonical_forms
Theorem canonical_form_intTy : forall V,
  value V -> typeOf [] V intTy -> exists I, V = num(I). [Show Proof]


Theorem canonical_form_arrowTy : forall V Ty1 Ty2,
  value V -> typeOf [] V (arrowTy Ty1 Ty2) ->
  exists X B, V = abs X Ty1 B. [Show Proof]



Extensible_Theorem
  progress : forall T Ty,
    IsT : is_tm T ->
    Ty : typeOf [] T Ty ->
    (exists T', eval T T') \/ value T
  on Ty. [Show Proof]
Back to example home