Extensibella: Extensibella Example: lambda

Language Specification

File: syntax.sos

Module lambda_calculus:bool

Builds on lambda_calculus:host

e ::= ...
    | trueE
    | falseE
    | if(e, e, e)

-------------------------------------------- [Proj-True]
|{e}- trueE ~~> abs("a", abs("b", var("a")))


--------------------------------------------- [Proj-False]
|{e}- falseE ~~> abs("a", abs("b", var("b")))


--------------------------------------------- [Proj-If]
|{e}- if(Cond, T, F) ~~> app(app(Cond, T), F)

File: eval.sos

[Reduce File] [Raw File]

Module lambda_calculus:bool

--------------------------------------- [E-True]
eval trueE abs("a", abs("b", var("a")))


---------------------------------------- [E-False]
eval falseE abs("a", abs("b", var("b")))


eval app(app(Cond, T), F) V
--------------------------- [E-If]
eval if(Cond, T, F) V



-------------------------------------------- [S-True]
subst X R trueE abs("a", abs("b", var("a")))


--------------------------------------------- [S-False]
subst X R falseE abs("a", abs("b", var("b")))


subst X R Cond CS
subst X R T TS
subst X R F FS
--------------------------------------------- [S-If]
subst X R if(Cond, T, F) app(app(CS, TS), FS)

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:bool.


Prove_Constraint lambda_calculus:host:proj_is. [Show Proof]

%true
 search 6.
%false
 search 6.
%if
 case Hyp1. search.


Add_Proj_Rel lambda_calculus:host:is_e.

Prove_Ext_Ind lambda_calculus:host:is_e. [Show Proof]

%true
 unfold. exists abs "a" (abs "b" (var "a")). search 7.
%false
 unfold. exists abs "a" (abs "b" (var "b")). search 7.
%if
 apply IH to R1. apply IH to R2. apply IH to R3. search.


Prove_Constraint lambda_calculus:host:proj_same. [Show Proof]

%true
 case Hyp1. search.
%false
 case Hyp1. search.
%if
 case Hyp1. search.


Prove lambda_calculus:host:subst_exists. [Show Proof]

%true
 search.
%false
 search.
%if
 apply IH to IsE1 _ IsR. apply IH to IsE2 _ IsR.
 apply IH to IsE3 _ IsR. search.


Prove lambda_calculus:host:subst_is. [Show Proof]

%S-True
 search 7.
%S-False
 search 7.
%S-If
 Is: case IsE. apply IH to _ _ _ S1. apply IH to _ _ _ S2.
 apply IH to _ _ _ S3. search.


Prove lambda_calculus:host:eval_is. [Show Proof]

%E-True
 search 7.
%E-False
 search 7.
%E-If
 Is: case IsE. IsC: apply IH to _ Ev1. search.


Prove lambda_calculus:host:subst_unique. [Show Proof]

%S-True
 case SB. search.
%S-False
 case SB. search.
%S-If
 SB: case SB. Is: case IsE. apply IH to _ _ _ SA1 SB.
 apply IH to _ _ _ SA2 SB1. apply IH to _ _ _ SA3 SB2. search.


Prove lambda_calculus:host:eval_unique. [Show Proof]

%E-True
 case EvB. search.
%E-False
 case EvB. search.
%E-If
 EvB: case EvB. Is: case IsE. apply IH to _ EvA1 EvB. search.


Prove_Constraint lambda_calculus:host:proj_subst. [Show Proof]

%true
 OrA: apply is_string_eq_or_not to IsX _ with S2 = "a".
 OrB: apply is_string_eq_or_not to IsX _ with S2 = "b". A: case OrA.
   %X = "a"
    search.
   %X != "a"
    B: case OrB.
      %X = "b"
       search.
      %X != "b"
       search.
%false
 OrA: apply is_string_eq_or_not to IsX _ with S2 = "a".
 OrB: apply is_string_eq_or_not to IsX _ with S2 = "b". A: case OrA.
   %X = "a"
    search.
   %X != "a"
    B: case OrB.
      %X = "b"
       search.
      %X != "b"
       search.
%if
 Is: case IsE. S: case S. search.


Prove_Constraint lambda_calculus:host:proj_subst_same. [Show Proof]

%true
 case S. S': case S'.
   %S-Abs-Eq
    search.
   %S-Abs-NEq
    T: case S'1.
      %S-Abs-Eq
       search.
      %S-Abs-NEq
       U: case T1.
         %S-Var-Eq
          apply S' to _.
         %S-Var-NEq
          search.
%false
 case S. S': case S'.
   %S-Abs-Eq
    search.
   %S-Abs-NEq
    T: case S'1.
      %S-Abs-Eq
       search.
      %S-Abs-NEq
       U: case T1.
         %S-Var-Eq
          apply T to _.
         %S-Var-NEq
          search.
%if
 S: case S. S': case S'. S'': case S'. Is: case IsE.
 apply subst_unique to _ _ _ S S''.
 apply subst_unique to _ _ _ S1 S''1.
 apply subst_unique to _ _ _ S2 S'1. search.


Prove_Constraint lambda_calculus:host:proj_eval. [Show Proof]

%true
 search.
%false
 search.
%if
 Ev: case Ev. search.


Prove_Constraint lambda_calculus:host:proj_eval_same. [Show Proof]

%true
 case Ev. case Ev'. search.
%false
 case Ev. case Ev'. search.
%if
 Ev: case Ev. case IsE. apply eval_unique to _ Ev' 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]

%true
 unfold. exists abs "a" (abs "b" (var "a")). search 7.
%false
 unfold. exists abs "a" (abs "b" (var "b")). search 7.
%if
 apply ext_size_is_int_eval to R2. L: apply lt_plus_one to R1 _.
 apply ext_size_pos_eval to R2. Acc: case Acc. A: apply Acc to _ L.
 apply IH to R2 A. exists app (app Cond T) F. search.

Extensibella Example: lambda_calculus:bool

Language Specification

File: syntax.sos

File: eval.sos

Reasoning