Extensibella: Extensibella Example: stlc:let

Language Specification

File: def.sos

Module stlc:let

Builds on stlc:host

tm ::= ...
     | let(string, tm, tm)


typeOf Ctx T1 Ty
----------------------------------------------------- [Proj-Let]
Ctx |{tm}- let(X, T1, T2) ~~> app(abs(X, Ty, T2), T1)



eval T1 T11
----------------------------------- [E-Let-Step]
eval let(X, T1, T2) let(X, T11, T2)


value T1
subst X T1 T2 V
--------------------- [E-Let-Subst]
eval let(X, T1, T2) V



X != Y
subst X R T1 S1
subst X R T2 S2
--------------------------------------- [S-Let-NEq]
subst X R let(Y, T1, T2) let(Y, S1, S2)


subst X R T1 S1
--------------------------------------- [S-Let-Eq]
subst X R let(X, T1, T2) let(X, S1, T2)



typeOf Ctx T1 Ty1
typeOf (X, Ty1)::Ctx T2 Ty2
----------------------------- [T-Let]
typeOf Ctx let(X, 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 stlc:let.

Prove_Constraint stlc:host:proj_ty_is.


Prove stlc:host:type_is. [Show Proof]

%T-Let
 Is: case IsT. apply IH to _ Is1 Ty1. apply IH to _ Is2 Ty2. search.


Prove_Constraint stlc:host:proj_is. [Show Proof]

%Proj-Let
 case IsT. apply type_is to _ _ Proj1. search.


Prove stlc:host:type_unique. [Show Proof]

%T-Let
 TyB: case TyB. case IsT. apply IH to _ _ TyA1 TyB.
 apply type_is to _ _ TyA1. apply IH to _ _ TyA2 TyB1. search.


Prove_Constraint stlc:host:proj_ty_unique.


Prove_Constraint stlc:host:proj_tm_unique. [Show Proof]

%Proj-Let
 case Hyp1. case Hyp2. apply type_unique to _ _ Hyp4 H1. search.


Prove stlc:host:subst_is. [Show Proof]

%S-Let-NEq
 Is: case IsT. apply IH to _ _ _ S2. apply IH to _ _ _ S3. search.
%S-Let-Eq
 Is: case IsT. apply IH to _ _ _ S1. search.


Prove stlc:host:eval_is. [Show Proof]

%E-Let-Step
 Is: case IsT. apply IH to _ Ev1. search.
%E-Let-Subst
 Is: case IsT. apply subst_is to _ _ _ Ev2. search.


Prove stlc:host:subst_unique. [Show Proof]

%S-Let-NEq
 SB: case SB.
   %S-Let-NEq
    apply IH to SA2 SB1. apply IH to SA3 SB2. search.
   %S-Let-Eq
    apply SA1 to _.
%S-Let-Eq
 SB: case SB.
   %S-Let-NEq
    apply SB to _.
   %S-Let-Eq
    apply IH to SA1 SB. search.


Prove stlc:host:value_eval_false.


Prove stlc:host:eval_unique. [Show Proof]

%E-Let-Step
 EvB: case EvB.
   %E-Let-Step
    apply IH to EvA1 EvB. search.
   %E-Let-Subst
    apply value_eval_false to EvB EvA1.
%E-Let-Subst
 EvB: case EvB.
   %E-Let-Step
    apply value_eval_false to EvA1 EvB.
   %E-Let-Subst
    apply subst_unique to EvA2 EvB1. search.


Prove stlc:host:ty_lookup. [Show Proof]

%T-Let
 apply IH to Ty1 L. apply IH to Ty2 _ with Ctx2 = (X, Ty1)::Ctx2.
   intros Lkp. Lkp: case Lkp.
     %Lkp-Here
      search.
     %Lkp-Later
      apply L to Lkp1. search.
 search.


Prove stlc:host:subst_type_preservation. [Show Proof]

%S-Let-NEq
 Ty: case TTy. apply IH to Ty S2 RTy.
 Ty': apply ty_lookup to Ty1 _ with Ctx2 = (X, XTy)::(Y, Ty1)::Ctx.
   intros L. L: case L.
     %Lkp-Here
      search.
     %Lkp-Later
      L: case L1.
        %Lkp-Here
         search.
        %Lkp-Later
         search.
 apply IH to Ty' S3 RTy. search.
%S-Let-Eq
 Ty: case TTy. apply IH to Ty S1 RTy.
 apply ty_lookup to Ty1 _ with Ctx2 = (X, Ty1)::Ctx.
   intros L. L: case L.
     %Lkp-Here
      search.
     %Lkp-Later
      L: case L1.
        %Lkp-Here
         apply L to _.
        %Lkp-Later
         search.
 search.


Prove stlc:host:type_preservation. [Show Proof]

%E-Let-Step
 Ty: case Ty. apply IH to Ty Ev1. search.
%E-Let-Subst
 Ty: case Ty. apply subst_type_preservation to Ty1 Ev2 Ty. search.


Prove stlc:host:subst_total. [Show Proof]

%let
 Or: apply is_string_eq_or_not to IsX IsT1. E: case Or.
   %X = S
    apply IH to IsT2 IsX with R = R. search.
   %X != S
    apply IH to IsT2 IsX with R = R. apply IH to IsT3 IsX with R = R.
    search.


Prove stlc:host:canonical_forms.


Prove stlc:host:progress. [Show Proof]

%T-Let
 Is: case IsT. Or: apply IH to _ Ty1. EV: case Or.
   %eval T1 T'
    search.
   %value T1
    apply subst_total to Is2 Is with R = T1. search.