Extensibella Example: exactEval:list

Language Specification

File: syntax.sos

[Reduce File] [Raw File] 
Module exactEval:list

Builds on exactEval:host

/*Expressions*/
expr ::= ...
       | nil(typ) /*need type for type uniqueness*/
       | cons(expr, expr)
       | head(expr)
       | tail(expr)
       | null(expr)
       | index(expr, expr) /*lst[i]*/
       | length(expr)


------------------------------------------------------- [Proj-Nil]
Names |{expr}- nil(Ty) ~~>
               recBuild(consRecFieldExprs("null", true,
                        nilRecFieldExprs))


------------------------------------------------- [Proj-Cons]
Names |{expr}- cons(E1, E2) ~~>
         recBuild(
           consRecFieldExprs("null", false,
           consRecFieldExprs("head", E1,
           consRecFieldExprs("tail", E2,
                             nilRecFieldExprs))))


---------------------------------------------------- [Proj-Null]
Names |{expr}- null(E) ~~> recFieldAccess(E, "null")


---------------------------------------------------- [Proj-Head]
Names |{expr}- head(E) ~~> recFieldAccess(E, "head")


---------------------------------------------------- [Proj-Tail]
Names |{expr}- tail(E) ~~> recFieldAccess(E, "tail")


fresh_name "I" Names SaveI
fresh_name "L" Names SaveL
-------------------------------------------- [Proj-Index]
Names |{expr}- index(Lst, Index) ~~>
           stmtExpr(
              seq(declare(intTy, SaveL, Lst),
              seq(declare(intTy, SaveI, Index),
              /*kill it if the index is < 0;
                maintains eval back from proj*/
              seq(ifThenElse(greater(num(0), name(SaveI)),
                     printVal(errorExpr(stringLit("Die"), intTy)),
                     noop),
                  while(greater(name(SaveI), num(0)),
                     seq(assign(SaveL, recFieldAccess(name(SaveL),
                                                      "tail")),
                         assign(SaveI, minus(name(SaveI), num(1)))))))),
              recFieldAccess(name(SaveL), "head"))


fresh_name "L" Names SaveL
fresh_name "Len" Names Len
------------------------------ [Proj-Length]
Names |{expr}- length(E) ~~>
           stmtExpr(
              seq(declare(intTy, SaveL, E),
              seq(declare(intTy, Len, num(0)),
                  while(not(recFieldAccess(name(SaveL), "null")),
                     seq(assign(SaveL, recFieldAccess(name(SaveL),
                                                      "tail")),
                         assign(Len, plus(name(Len), num(1))))))),
              name(Len))




/*Statements*/
stmt ::= ...
       | listUpdate(string, expr, expr) /*lst[i] = e*/
       | listForeach(string, expr, stmt) /*foreach(x : l){ body }*/


fresh_name "I" L::Names SaveI
fresh_name "Hold" L::Names Hold
fresh_name "E" L::Names SaveE
fresh_name "C" L::Names Copy
---------------------------------------- [Proj-ListUpdate]
Names |{stmt}- listUpdate(L, I, E) ~~>
   scopeStmt(
      /*compute value of I for use in computation*/
      seq(declare(intTy, SaveI, I),
      /*save value of E to put in list later*/
      seq(declare(intTy, SaveE, E),
      /*this is to get the ctx into the right order for eval;
        after one run of the loop, SaveI will be before SaveE, and we
        want the order to be consistent for proofs*/
      seq(assign(SaveI, name(SaveI)),
      /*create a list for holding the things before place I;
        type does not matter, so long as it is declared*/
      seq(declare(intTy, Hold, nil(intTy)),
      /*pull I things off the front of L and hold them in stack Hold*/
      seq(while(and(not(eq(name(SaveI), num(0))),
                    not(null(name(L)))), /*check L didn't fake end*/
                seq(assign(SaveI, minus(name(SaveI), num(1))),
                seq(declare(intTy, Copy, name(L)),
                /*need to do this instead of cons to maintain any
                  other fields beyond head, tail, and null*/
                seq(recUpdate(Copy, ["tail"], name(Hold)),
                seq(assign(Hold, name(Copy)),
                    assign(L, tail(name(L)))))))),
      /*check for fake ending of L before the update location;
        kills execution if it is invalid*/
      seq(ifThenElse(null(name(L)),
             declare(intTy, Copy,
                     errorExpr(stringLit("Invalid update"), intTy)),
             noop),
      /*place the new value in position I, removing the old one*/
      seq(recUpdate(L, ["head"], name(SaveE)),
      /*place the old things back on list L from stack Hold*/
          while(not(null(name(Hold))),
                /*same as above; maintains any other fields*/
                seq(declare(intTy, Copy, name(Hold)),
                seq(recUpdate(Copy, ["tail"], name(L)),
                seq(assign(L, name(Copy)),
                    assign(Hold, tail(name(Hold)))))))))))))))
/*The purpose of checking whether L.null is true is to ensure we have
  the projection constraint for the back direction for evaluation,
  that the original evaluates if the projection does.  For this we
  need to know that we have L.null = false to build back the
  updateListIndex we need, which requires this for the sake of proving
  the corresponding forward version of the projection constraint.  Oh
  what a tangled web we weave when first we practice to prove
  projection constraints.*/
/*{
    int SaveI = I;
    int SaveE = E;
    SaveI = SaveI;
    int Hold = [];
    while SaveI != 0 && !null(L){
      SaveI = SaveI - 1;
      int Copy = L;
      Copy.tail = Hold;
      Hold = Copy;
      L = tail(L);
    }
    if null(L){
      int Copy = error("Invalid update");
    }
    else{}
    L = SaveE::tail(L);
    while !null(Hold){
      int Copy = Hold;
      Copy.tail = L;
      L = Copy;
      Hold = tail(Hold);
    }
  }*/


fresh_name "L" X::Names SaveL
----------------------------------------------- [Proj-ListForeach]
Names |{stmt}- listForeach(X, L, Body) ~~>
    scopeStmt(
       /*compute list for use in computation;
         as before, types don't matter*/
       seq(declare(intTy, SaveL, L),
           while(not(null(name(SaveL))),
              seq(declare(intTy, X, head(name(SaveL))),
              seq(assign(SaveL, tail(name(SaveL))),
                  Body)))))
/*{
    int SaveL = l;
    while !null(SaveL){
      int X = head(SaveL);
      SaveL = tail(SaveL);
      Body
    }
  }*/




/*Types*/
typ ::= ...
      | listTy(typ)


/*Strictly speaking, an empty list doesn't have the head or tail
  fields*/
--------------------------------------------- [Proj-ListTy]
|{typ}- listTy(T) ~~>
        recTy(consRecFieldTys("null", boolTy,
              consRecFieldTys("head", T,
              consRecFieldTys("tail", listTy(T),
              nilRecFieldTys))))

File: vars.sos

[Reduce File] [Raw File] 
Module exactEval:list

/********************************************************************
 Expression Variables
 ********************************************************************/

--------------- [V-Nil]
vars nil(Ty) []


vars E1 V1
vars E2 V2
V1 ++ V2 = V
------------------- [V-Cons]
vars cons(E1, E2) V


vars E V
-------------- [V-Head]
vars head(E) V


vars E V
-------------- [V-Tail]
vars tail(E) V


vars E V
-------------- [V-Null]
vars null(E) V


vars L VL
vars I VI
VL ++ VI = V
------------------ [V-Index]
vars index(L, I) V


vars E V
---------------- [V-Length]
vars length(E) V





/********************************************************************
 Statement Names
 ********************************************************************/

------------------------ [EN-Nil]
exprNames Ctx nil(Ty) []


exprNames Ctx E1 N1
exprNames Ctx E2 N2
N1 ++ N2 = N
---------------------------- [EN-Cons]
exprNames Ctx cons(E1, E2) N


exprNames Ctx E N
----------------------- [EN-Head]
exprNames Ctx head(E) N


exprNames Ctx E N
----------------------- [EN-Tail]
exprNames Ctx tail(E) N


exprNames Ctx E N
----------------------- [EN-Null]
exprNames Ctx null(E) N


exprNames Ctx E1 N1
exprNames Ctx E2 N2
N1 ++ N2 = N
----------------------------- [EN-Index]
exprNames Ctx index(E1, E2) N


exprNames Ctx E N
------------------------- [EN-Length]
exprNames Ctx length(E) N




mems L Ctx
exprNames Ctx I NI
exprNames Ctx E NE
NI ++ NE = N
--------------------------------------- [SN-ListUpdate-Ignore]
stmtNames Ctx listUpdate(L, I, E) N Ctx


not_mems L Ctx
exprNames Ctx I NI
exprNames Ctx E NE
NI ++ NE = N
------------------------------------------ [SN-ListUpdate-Take]
stmtNames Ctx listUpdate(L, I, E) L::N Ctx


exprNames Ctx L NL
stmtNames [I]::Ctx Body NB Ctx1
NL ++ NB = N
------------------------------------------- [SN-ListForeach]
stmtNames Ctx listForeach(I, L, Body) N Ctx

File: typing.sos

[Reduce File] [Raw File] 
Module exactEval:list

/********************************************************************
 Expression Typing
 ********************************************************************/

------------------------------- [T-Nil]
typeOf FC TC nil(Ty) listTy(Ty)


typeOf FC TC E1 Ty
typeOf FC TC E2 listTy(Ty)
------------------------------------ [T-Cons]
typeOf FC TC cons(E1, E2) listTy(Ty)


typeOf FC TC E listTy(Ty)
------------------------- [T-Head]
typeOf FC TC head(E) Ty


typeOf FC TC E listTy(Ty)
------------------------------- [T-Tail]
typeOf FC TC tail(E) listTy(Ty)


typeOf FC TC E listTy(Ty)
--------------------------- [T-Null]
typeOf FC TC null(E) boolTy


typeOf FC TC L listTy(Ty)
typeOf FC TC I intTy
--------------------------- [T-Index]
typeOf FC TC index(L, I) Ty


typeOf FC TC E listTy(Ty)
---------------------------- [T-Length]
typeOf FC TC length(E) intTy



/********************************************************************
 Statement Typing
 ********************************************************************/

lookupScopes L TC listTy(Ty)
typeOf FC TC I intTy
typeOf FC TC E Ty
----------------------------------- [T-ListUpdate]
stmtOK FC TC listUpdate(L, I, E) TC


typeOf FC TC L listTy(Ty)
stmtOK FC [(X, Ty)]::TC Body TC1
--------------------------------------- [T-ListForeach]
stmtOK FC TC listForeach(X, L, Body) TC





/********************************************************************
 Value Typing
 ********************************************************************/

valueType V boolTy
----------------------------------------------- [VT-ListNil]
valueType recVal([("null", V)]) listTy(Ty)


valueType NV boolTy
valueType HV Ty
valueType TV listTy(Ty)
---------------------------------------------- [VT-ListCons]
{valueType recVal([("null", NV), ("head", HV),
                   ("tail", TV)]) listTy(Ty)}

File: eval.sos

[Reduce File] [Raw File] 
Module exactEval:list

/********************************************************************
 Expression Evaluation
 ********************************************************************/

-------------------------------------------------------- [E-Nil]
evalExpr FE EE nil(Ty) recVal([("null", trueVal)]) EE []


evalExpr FE EE E1 V1 EE1 O1
evalExpr FE EE1 E2 V2 EE2 O2
O1 ++ O2 = O
--------------------------------------------- [E-Cons]
{evalExpr FE EE cons(E1, E2)
    recVal([("null", falseVal), ("head", V1),
            ("tail", V2)]) EE2 O}


evalExpr FE EE E recVal(Fields) EE1 O
lookup Fields "head" Hd
------------------------------------- [E-Head]
evalExpr FE EE head(E) Hd EE1 O


evalExpr FE EE E recVal(Fields) EE1 O
lookup Fields "tail" Tl
------------------------------------- [E-Tail]
evalExpr FE EE tail(E) Tl EE1 O


evalExpr FE EE E recVal(Fields) EE1 O
lookup Fields "null" V
------------------------------------- [E-Null]
evalExpr FE EE null(E) V EE1 O


evalExpr FE EE L LV EE1 O1
evalExpr FE EE1 I intVal(Idx) EE2 O2
listIndex LV Idx V
O1 ++ O2 = O
------------------------------------ [E-Index]
evalExpr FE EE index(L, I) V EE2 O


evalExpr FE EE E V EE1 O
listLength V I
---------------------------------------- [E-Length]
evalExpr FE EE length(E) intVal(I) EE1 O


Fixed Judgment listIndex : value int value
Fixed Judgment listLength : value int

lookup Fields "head" V
============================ [LI-0]
listIndex recVal(Fields) 0 V


N - 1 = I
lookup Fields "tail" Tl
listIndex Tl I V
============================ [LI-Step]
listIndex recVal(Fields) N V



lookup Fields "null" trueVal
============================ [LL-Nil]
listLength recVal(Fields) 0


lookup Fields "null" falseVal
lookup Fields "tail" Tl
listLength Tl I
I + 1 = N
============================= [LL-Cons]
listLength recVal(Fields) N



/********************************************************************
 Statement Evaluation
 ********************************************************************/

evalExpr FE EE I intVal(N) EE1 O1
evalExpr FE EE1 E V EE2 O2
lookupScopes L EE2 LV /*lookup after I and E changes to make proj eval right*/
updateListIndex LV N V LV2 /*make the new list*/
replaceScopes L LV2 EE2 EE3 /*put it in its place*/
O1 ++ O2 = O
---------------------------------------- [E-ListUpdate]
evalStmt FE EE listUpdate(L, I, E) EE3 O


evalExpr FE EE L LV EE1 O1
iterateList FE EE1 LV X Body EE2 O2
O1 ++ O2 = O
-------------------------------------------- [E-ListForeach]
evalStmt FE EE listForeach(X, L, Body) EE2 O



                  /*original list, index, new value, new list*/
Fixed Judgment updateListIndex : value int value value

/*we need to check the null field to get projection evaluation to
  follow from this, as it requires the null field; otherwise it is not
  needed*/
lookup Fields "null" falseVal
replaceRecVal "head" VNew Fields NewFields
======================================================= [ULI-0]
updateListIndex recVal(Fields) 0 VNew recVal(NewFields)


/*we need to check the null field to get projection evaluation to
  follow from this, as it requires the null field; otherwise it is not
  needed*/
lookup Fields "null" falseVal
N - 1 = I
lookup Fields "tail" Tl
updateListIndex Tl I V TlNew
replaceRecVal "tail" TlNew Fields NewFields
==================================================== [ULI-Step]
updateListIndex recVal(Fields) N V recVal(NewFields)



/*execute the body once for each element of the list:
     iterateList (fun ctx) (init eval ctx) (list val) (name for list elements)
                 (loop body) (final eval ctx) (printed output)*/
Judgment iterateList : {[(string, (string, value, [string], stmt))] [[(string, value)]]
                        value* string stmt [[(string, value)]] [value]}

lookup Fields "null" trueVal
--------------------------------------------- [IL-Nil]
iterateList FE EE recVal(Fields) X Body EE []


lookup Fields "null" falseVal
lookup Fields "head" Hd
evalStmt FE [(X, Hd)]::EE Body Scope::EE1 O1
lookup Fields "tail" Tl
iterateList FE EE1 Tl X Body EE2 O2
O1 ++ O2 = O
--------------------------------------------- [IL-Cons]
iterateList FE EE recVal(Fields) X Body EE2 O


/*shouldn't have any extension-introduced constructors, so default
  rule should never hold*/
1 = 0
-------------------------------- [IL-Default]*
iterateList FE EE V X Body EE1 O

Reasoning

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

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

Module exactEval:list.

/********************************************************************
 Basic Projection Constraints
 ********************************************************************/
Prove_Constraint exactEval:host:proj_expr_unique. [Show Proof]

Prove_Constraint exactEval:host:proj_expr_is. [Show Proof]

Prove_Constraint exactEval:host:proj_expr_other. [Show Proof]


Prove_Constraint exactEval:host:proj_stmt_unique. [Show Proof]

Prove_Constraint exactEval:host:proj_stmt_is. [Show Proof]

Prove_Constraint exactEval:host:proj_stmt_other. [Show Proof]


Prove_Constraint exactEval:host:proj_fun_unique.
Prove_Constraint exactEval:host:proj_fun_is.

Prove_Constraint exactEval:host:proj_param_unique.
Prove_Constraint exactEval:host:proj_param_is.

Prove_Constraint exactEval:host:proj_program_unique.
Prove_Constraint exactEval:host:proj_program_is.

Prove_Constraint exactEval:host:proj_typ_unique. [Show Proof]

Prove_Constraint exactEval:host:proj_typ_is. [Show Proof]





/********************************************************************
 Decidable Equality
 ********************************************************************/
Add_Proj_Rel exactEval:host:is_expr,
             exactEval:host:is_args,
             exactEval:host:is_recFieldExprs,
             exactEval:host:is_stmt.

Prove_Ext_Ind exactEval:host:is_expr,
              exactEval:host:is_args,
              exactEval:host:is_recFieldExprs,
              exactEval:host:is_stmt. [Show Proof]


Prove exactEval:host:is_args_nilArgs_or_consArgs.
Prove exactEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs.




/********************************************************************
 Variables
 ********************************************************************/
Prove exactEval:host:vars_unique. [Show Proof]


Prove exactEval:host:vars_is. [Show Proof]



Prove exactEval:host:vars_exist,
      exactEval:host:varsArgs_exist,
      exactEval:host:varsRecFields_exist. [Show Proof]





/********************************************************************
 Statement Names
 ********************************************************************/
Prove exactEval:host:stmtNames_is,
      exactEval:host:stmtNames_isCtx,
      exactEval:host:exprNames_is. [Show Proof]



Prove exactEval:host:stmtNames_unique,
      exactEval:host:exprNames_unique. [Show Proof]



Prove exactEval:host:stmtNames_keep_older. [Show Proof]



Prove exactEval:host:stmtNames_exists,
      exactEval:host:exprNames_exists,
      exactEval:host:argsNames_exists,
      exactEval:host:recFieldNames_exists. [Show Proof]



Prove exactEval:host:stmtNames_not_in_ctx,
      exactEval:host:exprNames_not_in_ctx. [Show Proof]



Prove exactEval:host:stmtNames_relatedCtxs,
      exactEval:host:stmtNames_relatedCtxs_ctx_fwd,
      exactEval:host:stmtNames_relatedCtxs_ctx_back,
      exactEval:host:exprNames_relatedCtxs. [Show Proof]



Prove exactEval:host:stmtNames_increaseCtxs,
      exactEval:host:stmtNames_increaseCtxs_ctxs,
      exactEval:host:exprNames_increaseCtxs. [Show Proof]



Theorem exprNames_mem : forall Ctx X N,
  mems X Ctx -> exprNames Ctx (name X) N -> N = []. [Show Proof]


Prove_Constraint exactEval:host:proj_exprNames. [Show Proof]



Theorem mems_append_right[X] : forall A B C (X : X),
  A ++ B = C -> mems X B -> mems X C. [Show Proof]


Prove_Constraint exactEval:host:proj_stmtNames. [Show Proof]



Prove_Constraint exactEval:host:proj_stmtNames_names_forward. [Show Proof]



Prove_Constraint exactEval:host:proj_stmtNames_names_backward. [Show Proof]





/********************************************************************
 Typing
 ********************************************************************/
Prove exactEval:host:typeOf_isTy,
      exactEval:host:stmtOK_isCtx. [Show Proof]



Prove exactEval:host:stmtOK_keep_scopes. [Show Proof]



Prove exactEval:host:stmtOK_older_scopes_same. [Show Proof]



Prove exactEval:host:stmtOK_first_scope_lookup_same. [Show Proof]



Prove exactEval:host:typeOf_unique,
      exactEval:host:stmtOK_unique. [Show Proof]



Prove exactEval:host:paramTy_is.
Prove exactEval:host:getFunInfo_is.


Prove exactEval:host:paramTy_exists.
Prove exactEval:host:getFunInfo_exists.




/********************************************************************
 Evaluation
 ********************************************************************/
Theorem listIndex_is : forall L I V,
  is_value L -> listIndex L I V -> is_value V. [Show Proof]



Theorem listLength_is : forall L I,
  is_value L -> listLength L I -> is_integer I. [Show Proof]



Theorem updateListIndex_is : forall L I V Out,
  is_value L -> is_value V -> updateListIndex L I V Out ->
  is_value Out. [Show Proof]



Prove exactEval:host:evalExpr_isCtx,
      exactEval:host:evalExpr_isValue,
      exactEval:host:evalStmt_isCtx,
      exactEval:host:evalArgs_isCtx,
      exactEval:host:evalArgs_isValue,
      exactEval:host:evalRecFields_isCtx,
      exactEval:host:evalRecFields_isValue
with
  iterateList_isCtx : forall FE EE V X Body EE' O,
    IsV : is_value V ->
    IsX : is_string X ->
    IsBody : is_stmt Body ->
    IsFE : is_list (is_pair is_string
                   (is_pair is_string
                   (is_pair is_value
                   (is_pair (is_list is_string) is_stmt)))) FE ->
    IsEE : is_list (is_list (is_pair is_string is_value)) EE ->
    IL : iterateList FE EE V X Body EE' O ->
    is_list (is_list (is_pair is_string is_value)) EE'
  on IL as IH_IL. [Show Proof]



Prove exactEval:host:evalExpr_isOutput,
      exactEval:host:evalStmt_isOutput,
      exactEval:host:evalArgs_isOutput,
      exactEval:host:evalRecFields_isOutput
with
  iterateList_isOutput : forall FE EE V X Body EE' O,
    IsV : is_value V ->
    IsX : is_string X ->
    IsBody : is_stmt Body ->
    IsFE : is_list (is_pair is_string
                   (is_pair is_string
                   (is_pair is_value
                   (is_pair (is_list is_string) is_stmt)))) FE ->
    IsEE : is_list (is_list (is_pair is_string is_value)) EE ->
    IL : iterateList FE EE V X Body EE' O ->
    is_list is_value O
  on IL as IH_IL. [Show Proof]



Prove exactEval:host:paramName_is.
Prove exactEval:host:getFunEvalInfo_is.

Prove exactEval:host:evalProgram_isOutput.


Prove exactEval:host:evalExpr_names_same,
      exactEval:host:evalStmt_names_same,
      exactEval:host:evalArgs_names_same,
      exactEval:host:evalRecFields_names_same
with
  iterateList_names_same : forall FE EE V X Body EE' O,
    IsV : is_value V ->
    IsX : is_string X ->
    IsBody : is_stmt Body ->
    IsFE : is_list (is_pair is_string
                   (is_pair is_string
                   (is_pair is_value
                   (is_pair (is_list is_string) is_stmt)))) FE ->
    IsEE : is_list (is_list (is_pair is_string is_value)) EE ->
    IL : iterateList FE EE V X Body EE' O ->
    names_same EE EE'
  on IL as IH_IL. [Show Proof]



Theorem listIndex_geq_0 : forall L I V,
  is_integer I -> listIndex L I V -> I >= 0. [Show Proof]


Theorem listIndex_unique : forall L I VA VB,
  listIndex L I VA -> listIndex L I VB -> VA = VB. [Show Proof]



Theorem listLength_unique : forall L IA IB,
  listLength L IA -> listLength L IB -> IA = IB. [Show Proof]



Theorem updateListIndex_geq_0 : forall L I V Out,
  is_integer I -> updateListIndex L I V Out -> I >= 0. [Show Proof]


Theorem updateListIndex_unique : forall L I V OutA OutB,
  updateListIndex L I V OutA -> updateListIndex L I V OutB ->
  OutA = OutB. [Show Proof]



Prove exactEval:host:evalExpr_newNameScopes,
      exactEval:host:evalExpr_newNameScopes_output,
      exactEval:host:evalExpr_newNameScopes_ctx,
      exactEval:host:evalStmt_newNameScopes_output,
      exactEval:host:evalStmt_newNameScopes,
      exactEval:host:evalArgs_newNameScopes,
      exactEval:host:evalArgs_newNameScopes_output,
      exactEval:host:evalArgs_newNameScopes_ctx,
      exactEval:host:evalRecFields_newNameScopes,
      exactEval:host:evalRecFields_newNameScopes_output,
      exactEval:host:evalRecFields_newNameScopes_ctx
with
  iterateList_newNameScopes_output :
    forall FE EE_A EE_B V X Body EE_A' EE_B' O_A O_B N Len,
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      ILA : iterateList FE EE_A V X Body EE_A' O_A ->
      ILB : iterateList FE EE_B V X Body EE_B' O_B ->
      NNS : newNameScopes N Len EE_A EE_B ->
      O_A = O_B
    on ILA as IH_O_IL,
  iterateList_newNameScopes :
    forall FE EE_A EE_B V X Body EE_A' EE_B' O_A O_B N Len,
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      ILA : iterateList FE EE_A V X Body EE_A' O_A ->
      ILB : iterateList FE EE_B V X Body EE_B' O_B ->
      NNS : newNameScopes N Len EE_A EE_B ->
      newNameScopes N Len EE_A' EE_B'
    on ILA as IH_C_IL. [Show Proof]



Add_Ext_Size exactEval:host:evalExpr, exactEval:host:evalArgs,
             exactEval:host:evalRecFields, exactEval:host:evalStmt
        with iterateList FE EE V X Body EE' O.
Add_Proj_Rel exactEval:host:evalExpr, exactEval:host:evalArgs,
             exactEval:host:evalRecFields, exactEval:host:evalStmt
        with iterateList FE EE V X Body EE' O.


Prove exactEval:host:evalExpr_newNameScopes_exists_ES,
      exactEval:host:evalStmt_newNameScopes_exists_ES,
      exactEval:host:evalArgs_newNameScopes_exists_ES,
      exactEval:host:evalRecFields_newNameScopes_exists_ES
with
  iterateList_newNameScopes_exists_ES :
    forall FE EE_A EE_B V X Body EE_B' O N Len ES,
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      ILB : <iterateList {ES}> FE EE_B V X Body EE_B' O ES ->
      NNS : newNameScopes N Len EE_A EE_B ->
      exists EE_A', <iterateList {ES}> FE EE_A V X Body EE_A' O ES
    on ILB as IH_IL. [Show Proof]



Prove exactEval:host:evalExpr_ctx_names,
      exactEval:host:evalStmt_ctx_names,
      exactEval:host:evalArgs_ctx_names,
      exactEval:host:evalRecFields_ctx_names
with
  iterateList_ctx_names : forall FE EE V X Body EE' O Ctx N Sc Ctx',
    IsV : is_value V ->
    IsX : is_string X ->
    IsBody : is_stmt Body ->
    IsFE : is_list (is_pair is_string
                   (is_pair is_string
                   (is_pair is_value
                   (is_pair (is_list is_string) is_stmt)))) FE ->
    IsEE : is_list (is_list (is_pair is_string is_value)) EE ->
    IsCtx : is_list (is_list is_string) Ctx ->
    Ctxs : ctx_names EE Ctx ->
    BN : stmtNames ([X]::Ctx) Body N (Sc::Ctx') ->
    IL : iterateList FE EE V X Body EE' O ->
    ctx_names EE' Ctx
  on IL as IH_IL. [Show Proof]



Prove exactEval:host:evalExpr_newNameScopes_exists_back,
      exactEval:host:evalStmt_newNameScopes_exists_back,
      exactEval:host:evalArgs_newNameScopes_exists_back,
      exactEval:host:evalRecFields_newNameScopes_exists_back
with
  iterateList_newNameScopes_exists_back :
    forall FE EE_A EE_B V X Body Ctx EE_A' O N Len Ctx',
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      IsCtx : is_list (is_list is_string) Ctx ->
      %----------
      Ctxs : ctx_names EE_B Ctx ->
      BN : stmtNames ([X]::Ctx) Body [] Ctx' ->
      %----------
      ILA : iterateList FE EE_A V X Body EE_A' O ->
      NNS : newNameScopes N Len EE_A EE_B ->
      exists EE_B', iterateList FE EE_B V X Body EE_B' O
    on ILA as IH_IL. [Show Proof]



Prove exactEval:host:evalExpr_scopes_same,
      exactEval:host:evalExpr_scopes_same_ctx,
      exactEval:host:evalStmt_scopes_same,
      exactEval:host:evalStmt_scopes_same_ctx,
      exactEval:host:evalArgs_scopes_same,
      exactEval:host:evalArgs_scopes_same_ctx,
      exactEval:host:evalRecFields_scopes_same,
      exactEval:host:evalRecFields_scopes_same_ctx
with
  iterateList_scopes_same :
    forall V X Body FE EE_A EE_A' OA EE_B EE_B' OB,
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      SS : scopes_same EE_A EE_B ->
      ILA : iterateList FE EE_A V X Body EE_A' OA ->
      ILB : iterateList FE EE_B V X Body EE_B' OB ->
      OA = OB
    on ILA as IH_IL,
  iterateList_scopes_same_ctx :
    forall V X Body FE EE_A EE_A' OA EE_B EE_B' OB,
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      SS : scopes_same EE_A EE_B ->
      ILA : iterateList FE EE_A V X Body EE_A' OA ->
      ILB : iterateList FE EE_B V X Body EE_B' OB ->
      scopes_same EE_A' EE_B'
    on ILA as IH_IL_C. [Show Proof]



Prove exactEval:host:evalExpr_scopes_same_exists,
      exactEval:host:evalStmt_scopes_same_exists,
      exactEval:host:evalArgs_scopes_same_exists,
      exactEval:host:evalRecFields_scopes_same_exists
with
  iterateList_scopes_same_exists :
    forall V X Body FE EE_A EE_A' O EE_B,
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsA : is_list (is_list (is_pair is_string is_value)) EE_A ->
      IsB : is_list (is_list (is_pair is_string is_value)) EE_B ->
      SS : scopes_same EE_A EE_B ->
      ILA : iterateList FE EE_A V X Body EE_A' O ->
      exists EE_B', iterateList FE EE_B V X Body EE_B' O
  on ILA as IH_IL. [Show Proof]



Theorem is_list_values_append_nil : forall L,
  is_list is_value L -> L ++ [] = L. [Show Proof]


Theorem index_to_while : forall LV IV V FE Ctx I L,
  listIndex LV IV V -> (L = I -> false) -> is_integer IV ->
  exists Fields,
    <evalStmt {ES}> FE ([(I, intVal IV), (L, LV)]::Ctx)
       (while (greater (name I) (num 0))
          (seq (assign L (recFieldAccess (name L) "tail"))
               (assign I (minus (name I) (num 1)))))
       ([(I, intVal 0), (L, recVal Fields)]::Ctx) [] 0 /\
    lookup Fields "head" V. [Show Proof]


Theorem while_to_index : forall LV IV V FE Ctx Ctx' O I L Fields,
  evalStmt FE ([(I, intVal IV), (L, LV)]::Ctx)
     (while (greater (name I) (num 0))
        (seq (assign L (recFieldAccess (name L) "tail"))
             (assign I (minus (name I) (num 1))))) Ctx' O ->
  lookupScopes L Ctx' (recVal Fields) ->
  lookup Fields "head" V ->
  IV >= 0 -> %necessary for E-While-False case to get IV = 0
  is_integer IV -> %necessary for maintaining IV >= 0 for IH
  (L = I -> false) ->
  listIndex LV IV V /\ O = [] /\ exists Scope, Ctx' = Scope::Ctx. [Show Proof]


Theorem length_to_while :
  forall LV StoreLen L Len CurrLen TotalLen FE Ctx,
    listLength LV CurrLen -> (L = Len -> false) ->
    CurrLen + StoreLen = TotalLen -> is_integer StoreLen ->
    is_integer CurrLen ->
    exists Fields,
      <evalStmt {ES}> FE ([(Len, intVal StoreLen), (L, LV)]::Ctx)
         (while (not (recFieldAccess (name L) "null"))
            (seq (assign L (recFieldAccess (name L) "tail"))
                 (assign Len (plus (name Len) (num 1)))))
         ([(Len, intVal TotalLen), (L, recVal Fields)]::Ctx) [] 0 /\
      lookup Fields "null" trueVal. [Show Proof]


Theorem while_to_length :
  forall LV StoreLen L Len FE Ctx Ctx' FinalLen O,
    evalStmt FE ([(Len, intVal StoreLen), (L, LV)]::Ctx)
      (while (not (recFieldAccess (name L) "null"))
         (seq (assign L (recFieldAccess (name L) "tail"))
              (assign Len (plus (name Len) (num 1))))) Ctx' O ->
    lookupScopes Len Ctx' FinalLen -> is_integer StoreLen ->
    (L = Len -> false) ->
    exists Scope TotalLen CurrLen,
       O = [] /\ Ctx' = Scope::Ctx /\ FinalLen = intVal TotalLen /\
       listLength LV CurrLen /\ is_integer CurrLen /\
       CurrLen + StoreLen = TotalLen. [Show Proof]


Extensible_Theorem
  iterateList_dot_null : forall FE EE V X Body EE' O,
    IL : iterateList FE EE V X Body EE' O ->
    exists Fs, V = recVal Fs /\
              (lookup Fs "null" trueVal \/ lookup Fs "null" falseVal)
  on IL. [Show Proof]



Theorem iterateList_to_while : forall FE EE V X Body EE' O Names L,
  is_value V -> is_string X -> is_stmt Body ->
  is_list (is_pair is_string
          (is_pair is_string
          (is_pair is_value
          (is_pair (is_list is_string) is_stmt)))) FE ->
  is_list (is_list (is_pair is_string is_value)) EE ->
  iterateList FE EE V X Body EE' O ->
  names EE Names -> fresh_name "L" (X::Names) L ->
  exists V',
    evalStmt FE ([(L, V)]::EE)
      (while (not (null (name L)))
         (seq (declare intTy X (head (name L)))
         (seq (assign L (tail (name L)))
              Body))) ([(L, V')]::EE') O. [Show Proof]



Theorem while_to_iterateList :
  forall FE EE V X Body Scope' EE' O Names L Ctx Ctx',
    is_value V -> is_string X -> is_stmt Body ->
    is_list (is_pair is_string
            (is_pair is_string
            (is_pair is_value
            (is_pair (is_list is_string) is_stmt)))) FE ->
    is_list (is_list (is_pair is_string is_value)) EE ->
    is_list (is_list is_string) Ctx ->
    names EE Names -> fresh_name "L" (X::Names) L ->
    ctx_names EE Ctx ->
    stmtNames ([X]::Ctx) Body [] Ctx' ->
    evalStmt FE ([(L, V)]::EE)
      (while (not (null (name L)))
         (seq (declare intTy X (head (name L)))
         (seq (assign L (tail (name L)))
              Body))) (Scope'::EE') O ->
    iterateList FE EE V X Body EE' O. [Show Proof]



Theorem lookupScopes_replaceScopes_exists : forall L Key V V',
  is_list (is_list (is_pair is_string is_value)) L -> is_string Key ->
  lookupScopes Key L V -> exists R, replaceScopes Key V' L R. [Show Proof]


Theorem replaceScopes_lookupScopes_same[Key, Item] :
  forall L (Key : Key) (V : Item) R,
    replaceScopes Key V L R -> lookupScopes Key R V. [Show Proof]


Theorem remove_all_twice[K, V] : forall (L : list (pair K V)) K RA RB,
  remove_all L K RA -> remove_all RA K RB -> RA = RB. [Show Proof]


Theorem replaceScopes_twice[Key, Item] :
  forall (L : list (list (pair string value))) K VA RA VB RB,
    replaceScopes K VA L RA -> replaceScopes K VB RA RB ->
    replaceScopes K VB L RB. [Show Proof]


Theorem updateListIndex_is_integer : forall L I V L',
  updateListIndex L I V L' -> is_integer I. [Show Proof]


Theorem updateListIndex_pos : forall L I V L',
  updateListIndex L I V L' -> I >= 0. [Show Proof]


Define listy : value -> prop by
listy (recVal Fields) := lookup Fields "null" trueVal;
listy (recVal Fields) :=
   exists Tl,
     lookup Fields "null" falseVal /\
     lookup Fields "tail" Tl /\ listy Tl.

%flip first list onto second, producing third
Define flipOnto : value -> value -> value -> prop by
flipOnto (recVal Fields) L L := lookup Fields "null" trueVal;
flipOnto (recVal Fields) L L' :=
  exists Fields' T,
    lookup Fields "null" falseVal /\
    lookup Fields "tail" T /\
    replaceRecVal "tail" L Fields Fields' /\
    flipOnto T (recVal Fields') L'.

Theorem lookup_replaceRecVal_exists : forall L F V V',
  lookup L F V -> exists R, replaceRecVal F V' L R. [Show Proof]


Theorem replaceScopes_lookupScopes[Key, Item] :
  forall (X : Key) (V : Item) L R,
    replaceScopes X V L R -> lookupScopes X R V. [Show Proof]


Theorem replaceRecVal_lookup : forall L F V R,
  replaceRecVal F V L R -> lookup R F V. [Show Proof]


Theorem replaceRecVal_lookup_other : forall L F V R F' V',
  replaceRecVal F V L R -> lookup L F' V' -> (F = F' -> false) ->
  lookup R F' V'. [Show Proof]


Theorem replaceRecVal_twice : forall A B C F V1 V2,
  replaceRecVal F V1 A B -> replaceRecVal F V2 B C ->
  replaceRecVal F V2 A C. [Show Proof]


Theorem eval_update_loop2 :
  forall (Hold SaveI SaveE Copy L : string) V HFs HoldL LVal G FE,
    listy HoldL ->
    is_list (is_pair is_string
            (is_pair is_string
            (is_pair is_value
            (is_pair (is_list is_string) is_stmt)))) FE ->
    is_list (is_list (is_pair is_string is_value))
        ([(Hold, recVal HFs), (SaveI, intVal 0), (SaveE, V)]::G) ->
    lookup HFs "tail" HoldL -> lookup HFs "null" falseVal ->
    (Hold = SaveI -> false) -> (Hold = L -> false) ->
    (SaveI = SaveE -> false) -> (SaveI = L -> false) ->
    (Hold = SaveE -> false) -> (SaveE = L -> false) ->
    (Copy = Hold -> false) -> (Copy = L -> false) ->
    (SaveI = Copy -> false) -> (SaveE = Copy -> false) ->
    lookupScopes L ([(Hold, recVal HFs), (SaveI, intVal 0),
                     (SaveE, V)]::G) LVal ->
    exists G' LV HFs',
      <evalStmt {P}> FE
             ([(Hold, recVal HFs), (SaveI, intVal 0), (SaveE, V)]::G)
             (while (not (null (name Hold)))
                 (seq (declare intTy Copy (name Hold))
                 (seq (recUpdate Copy ["tail"] (name L))
                 (seq (assign L (name Copy))
                      (assign Hold (tail (name Hold)))))))
             ([(Hold, recVal HFs'), (SaveI, intVal 0),
               (SaveE, V)]::G') [] /\
      lookup HFs' "null" trueVal /\
      replaceScopes L LV G G' /\
      flipOnto (recVal HFs) LVal LV. [Show Proof]


Theorem proj_listUpdate_eval :
  forall OldL I (Hold SaveI SaveE Copy L : string) HoldL V NewL G FE,
    updateListIndex OldL I V NewL ->
    (Hold = SaveI -> false) -> (Hold = L -> false) ->
    (SaveI = SaveE -> false) -> (SaveI = L -> false) ->
    (Hold = SaveE -> false) -> (SaveE = L -> false) ->
    (Copy = Hold -> false) -> (Copy = L -> false) ->
    (SaveI = Copy -> false) -> (SaveE = Copy -> false) ->
    listy HoldL ->
    I >= 0 ->
    is_list (is_pair is_string
            (is_pair is_string
            (is_pair is_value
            (is_pair (is_list is_string) is_stmt)))) FE ->
    is_list (is_list (is_pair is_string is_value))
       ([(Hold, HoldL), (SaveI, intVal I), (SaveE, V)]::G) ->
    is_string Copy ->
    lookupScopes L ([(Hold, HoldL), (SaveI, intVal I), (SaveE, V)]::G)
                 OldL ->
    exists G' LV HFs,
      <evalStmt {P}> FE
         ([(Hold, HoldL), (SaveI, intVal I), (SaveE, V)]::G)
         (seq (while (exactEval:host:and (not (eq (name SaveI) (num 0)))
                                       (not (null (name L))))
                   (seq (assign SaveI (minus (name SaveI) (num 1)))
                   (seq (declare intTy Copy (name L))
                   (seq (recUpdate Copy ["tail"] (name Hold))
                   (seq (assign Hold (name Copy))
                        (assign L (tail (name L))))))))
           (seq (ifThenElse (null (name L))
                    (declare intTy Copy
                        (errorExpr (stringLit "Invalid update") intTy))
                    noop)
           (seq (recUpdate L ["head"] (name SaveE))
                (while (not (null (name Hold)))
                     (seq (declare intTy Copy (name Hold))
                     (seq (recUpdate Copy ["tail"] (name L))
                     (seq (assign L (name Copy))
                          (assign Hold (tail (name Hold))))))))))
         ([(Hold, recVal HFs), (SaveI, intVal 0), (SaveE, V)]::G') [] /\
      lookup HFs "null" trueVal /\
      replaceScopes L LV G G' /\
      flipOnto HoldL NewL LV. [Show Proof]


Theorem replaceScopes_lookupScopes_other[Key, Item] :
  forall (X : Key) (XV : Item) L R Y YV,
    replaceScopes X XV L R -> lookupScopes Y L YV ->
    (X = Y -> false) -> lookupScopes Y R YV. [Show Proof]


Theorem eval_update_loop2_listy :
  forall (Hold Copy L : string) FE G G' O LVal HVal,
    evalStmt FE G
          (while (not (null (name Hold)))
              (seq (declare intTy Copy (name Hold))
              (seq (recUpdate Copy ["tail"] (name L))
              (seq (assign L (name Copy))
                   (assign Hold (tail (name Hold)))))))
          G' O ->
    (Hold = L -> false) -> (Copy = Hold -> false) ->
    (Copy = L -> false) ->
    lookupScopes L G LVal ->
    lookupScopes Hold G HVal ->
    exists LV, listy HVal /\ flipOnto HVal LVal LV. [Show Proof]


Theorem replaceRecVal_other_val : forall F VA L R VB,
  replaceRecVal F VA L R -> exists R', replaceRecVal F VB L R'. [Show Proof]


Theorem proj_eval_listUpdate :
  forall OldL VI (Hold SaveI SaveE Copy L : string) HoldL V G FE G1 O1
         G2 O2,
    (Hold = SaveI -> false) -> (Hold = L -> false) ->
    (SaveI = SaveE -> false) -> (SaveI = L -> false) ->
    (Hold = SaveE -> false) -> (SaveE = L -> false) ->
    (Copy = Hold -> false) -> (Copy = L -> false) ->
    (SaveI = Copy -> false) -> (SaveE = Copy -> false) ->
    is_list (is_pair is_string
            (is_pair is_string
            (is_pair is_value
            (is_pair (is_list is_string) is_stmt)))) FE ->
    is_list (is_list (is_pair is_string is_value))
       ([(Hold, HoldL), (SaveI, VI), (SaveE, V)]::G) ->
    is_string Copy ->
    lookupScopes L G OldL ->
    evalStmt FE
       ([(Hold, HoldL), (SaveI, VI), (SaveE, V)]::G)
       (while (exactEval:host:and (not (eq (name SaveI) (num 0)))
                                (not (null (name L))))
            (seq (assign SaveI (minus (name SaveI) (num 1)))
            (seq (declare intTy Copy (name L))
            (seq (recUpdate Copy ["tail"] (name Hold))
            (seq (assign Hold (name Copy))
                 (assign L (tail (name L)))))))) G1 O1 ->
    evalExpr FE G1 (null (name L)) falseVal G1 [] ->
    evalStmt FE G1 (recUpdate L ["head"] (name SaveE)) G2 O2 ->
    exists I NewL, VI = intVal I /\ updateListIndex OldL I V NewL. [Show Proof]



Prove_Constraint exactEval:host:proj_evalExpr_forward. [Show Proof]


Prove_Constraint exactEval:host:proj_evalExpr_backward. [Show Proof]



Theorem drop_one[A] : forall (L D : list A),
  drop 1 L D -> exists S, L = S::D. [Show Proof]



Theorem eval_while_names_same : forall C B FE EE EE' O,
  is_expr C -> is_stmt B ->
  is_list (is_pair is_string (is_pair is_string
      (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE ->
  is_list (is_list (is_pair is_string is_value)) EE ->
  evalStmt FE EE (while C B) EE' O ->
  names_same EE EE'. [Show Proof]



Theorem names_lookupScopes : forall Ctx X Names,
  is_list (is_list (is_pair is_string is_value)) Ctx ->
  names Ctx Names -> mem X Names -> exists V, lookupScopes X Ctx V. [Show Proof]



Prove_Constraint exactEval:host:proj_evalStmt_forward. [Show Proof]



Prove_Constraint exactEval:host:proj_evalStmt_backward. [Show Proof]



Prove_Ext_Ind exactEval:host:evalExpr,
              exactEval:host:evalArgs,
              exactEval:host:evalRecFields,
              exactEval:host:evalStmt
with forall FE EE V X Body EE' O,
        iterateList FE EE V X Body EE' O with
           IsFE : is_list (is_pair is_string
                          (is_pair is_string
                          (is_pair is_value
                          (is_pair (is_list is_string) is_stmt)))) FE,
           IsEE : is_list (is_list (is_pair is_string is_value)) EE,
           IsV : is_value V,
           IsX : is_string X,
           IsBody : is_stmt Body
and
  iterateList_to_while_P :
    forall FE SaveL V EE X Body EE' O Names N N',
      IsFE : is_list (is_pair is_string
                     (is_pair is_string
                     (is_pair is_value
                     (is_pair (is_list is_string) is_stmt)))) FE ->
      IsEE : is_list (is_list (is_pair is_string is_value))
                ([(SaveL, V)]::EE) ->
      IsV : is_value V ->
      IsX : is_string X ->
      IsBody : is_stmt Body ->
      IL : <iterateList {ES}> FE EE V X Body EE' O N ->
      /*
        The reason we do `acc (N + 1)` is because we need to use the
        IH for acc to change a derivation of evaluation for the body
        into evalStmt_P, where the derivation is not annotated.  Thus
        we need to know its size is smaller, but that is not
        guaranteed for the iterateList size directly.  However,
        whenever we want to use this, we evaluated the iterateList
        with its larger size, and thus have acc for the size of the
        iterateList derivation + 1.
      */
      Plus : 1 + N = N' ->
      Acc : acc N' ->
      Names : names EE Names ->
      Fr : fresh_name "L" (X::Names) SaveL ->
      %
      exists V',
        <evalStmt {P}> FE ([(SaveL, V)]::EE)
           (while (not (null (name SaveL)))
              (seq (declare intTy X (head (name SaveL)))
              (seq (assign SaveL (tail (name SaveL)))
                   Body))) ([(SaveL, V')]::EE') O
  on Acc as IH_IL_W_A, IL * as IH_IL_W. [Show Proof]



Prove exactEval:host:paramName_unique.
Prove_Constraint exactEval:host:proj_paramName_forward.
Prove_Constraint exactEval:host:proj_paramName_back.
Prove exactEval:host:getFunEvalInfo_unique.
Prove_Constraint exactEval:host:proj_getFunEvalInfo_forward.
Prove_Constraint exactEval:host:proj_getFunEvalInfo_back.

Prove exactEval:host:evalProgram_unique.
Prove_Constraint exactEval:host:proj_evalProgram_forward.
Prove_Constraint exactEval:host:proj_evalProgram_back.


Theorem listIndex_typePres : forall L Ty I V,
  valueType L (listTy Ty) -> listIndex L I V -> valueType V Ty. [Show Proof]



Theorem updateListIndex_typePres : forall L Ty I V Out,
  valueType L (listTy Ty) -> valueType V Ty ->
  updateListIndex L I V Out -> valueType Out (listTy Ty). [Show Proof]



Prove exactEval:host:evalExpr_typePres_ctx,
      exactEval:host:evalExpr_typePres,
      exactEval:host:evalStmt_typePres,
      exactEval:host:evalArgs_typePres_Ctx,
      exactEval:host:evalArgs_typePres,
      exactEval:host:evalRecFields_typePres_Ctx,
      exactEval:host:evalRecFields_typePres
with
  iterateList_typePres : forall V X Body FT ET Ty Sc ET' FE EE EE' O,
    IsV : is_value V ->
    IsX : is_string X ->
    IsBody : is_stmt Body ->
    IsFT : is_list (is_pair is_string
                   (is_pair is_typ (is_list is_typ))) FT ->
    IsET : is_list (is_list (is_pair is_string is_typ)) ET ->
    IsFE : is_list (is_pair is_string
                   (is_pair is_string
                   (is_pair is_value
                   (is_pair (is_list is_string) is_stmt)))) FE ->
    IsEE : is_list (is_list (is_pair is_string is_value)) EE ->
    Ty : stmtOK FT ([(X, Ty)]::ET) Body (Sc::ET') ->
    VTy : valueType V (listTy Ty) ->
    IsTy : is_typ Ty ->
    IL : iterateList FE EE V X Body EE' O ->
    Funs : (forall F RetTy ArgTys ArgNames Body RetVar RVVal,
              lookup FT F (RetTy, ArgTys) ->
              lookup FE F (RetVar, RVVal, ArgNames, Body) ->
              exists Scope TyEnv',
                zip ArgNames ArgTys Scope /\
                valueType RVVal RetTy /\
                stmtOK FT [((RetVar, RetTy)::Scope)] Body TyEnv') ->
    Ctxs : related_all_scopes ET EE ->
    related_all_scopes ET' EE'
  on IL as IH_IL. [Show Proof]



Prove exactEval:host:paramTy_paramName_same.
Prove exactEval:host:funOK_getFunEvalInfo_related.


Prove exactEval:host:evalExpr_output_forms,
      exactEval:host:evalStmt_output_forms,
      exactEval:host:evalArgs_output_forms,
      exactEval:host:evalRecFields_output_forms
with
  iterateList_output_forms : forall V X Body FE EE EE' O,
    IsV : is_value V ->
    IsX : is_string X ->
    IsBody : is_stmt Body ->
    IsFE : is_list (is_pair is_string
                   (is_pair is_string
                   (is_pair is_value
                   (is_pair (is_list is_string) is_stmt)))) FE ->
    IsEE : is_list (is_list (is_pair is_string is_value)) EE ->
    IL : iterateList FE EE V X Body EE' O ->
    output_forms O
  on IL as IH_IL. [Show Proof]



Prove exactEval:host:evalProgram_output_forms.


Prove exactEval:host:paramName_exists.
Prove exactEval:host:getFunEvalInfo_exists.
Back to example home