Module looseEval:list Builds on looseEval: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] |{expr}- nil(Ty) ~~> num(0) ------------------------------------ [Proj-Cons] |{expr}- cons(E1, E2) ~~> eq(E1, E2) ---------------------- [Proj-Null] |{expr}- null(E) ~~> E ---------------------- [Proj-Head] |{expr}- head(E) ~~> E ---------------------- [Proj-Tail] |{expr}- tail(E) ~~> E --------------------------------------------- [Proj-Index] |{expr}- index(Lst, Index) ~~> eq(Lst, Index) ------------------------ [Proj-Length] |{expr}- length(E) ~~> E /*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 ---------------------------------------- [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(greater(name(SaveI), num(0)), seq(assign(SaveI, minus(name(SaveI), num(1))), seq(assign(Hold, cons(head(name(L)), name(Hold))), assign(L, tail(name(L)))))), /*place the new value in position I, removing the old one*/ seq(assign(L, cons(name(SaveE), tail(name(L)))), /*place the old things back on list L from stack Hold*/ while(not(null(name(Hold))), seq(assign(L, cons(head(name(Hold)), name(L))), assign(Hold, tail(name(Hold)))))))))))) /*{ int SaveI = I; int SaveE = E; SaveI = SaveI; int Hold = []; while SaveI > 0{ SaveI = SaveI - 1; Hold = head(L)::Hold; L = tail(L); } L = SaveE::tail(L); while !null(Hold){ L = head(Hold)::L; 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) ----------------------- [Proj-ListTy] |{typ}- listTy(T) ~~> T /*Values*/ value ::= ... | nilVal | consVal(value, value) ------------------------------ [Proj-NilVal] |{value}- nilVal ~~> intVal(0) --------------------------------------------- [Proj-ConsVal] |{value}- consVal(Hd, Tl) ~~> recVal(consRecFieldVals("head", Hd, consRecFieldVals("tail", Tl, nilRecFieldVals)))
Module looseEval: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
Module looseEval: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 ********************************************************************/ --------------------------- [VT-Nil] valueType nilVal listTy(Ty) valueType Hd Ty valueType Tl listTy(Ty) ------------------------------------ [VT-Cons] valueType consVal(Hd, Tl) listTy(Ty)
Module looseEval:list /******************************************************************** Expression Evaluation ********************************************************************/ -------------------------------- [E-Nil] evalExpr FE EE nil(Ty) nilVal [] evalExpr FE EE E1 V1 O1 evalExpr FE EE E2 V2 O2 O1 ++ O2 = O --------------------------------------------- [E-Cons] evalExpr FE EE cons(E1, E2) consVal(V1, V2) O evalExpr FE EE E consVal(Hd, Tl) O ---------------------------------- [E-Head] evalExpr FE EE head(E) Hd O evalExpr FE EE E consVal(Hd, Tl) O ---------------------------------- [E-Tail] evalExpr FE EE tail(E) Tl O evalExpr FE EE E nilVal O -------------------------------- [E-Null-True] evalExpr FE EE null(E) trueVal O evalExpr FE EE E consVal(Hd, Tl) O ---------------------------------- [E-Null-False] evalExpr FE EE null(E) falseVal O evalExpr FE EE L LV O1 evalExpr FE EE I intVal(Idx) O2 listIndex LV Idx V O1 ++ O2 = O ------------------------------- [E-Index] evalExpr FE EE index(L, I) V O evalExpr FE EE E V O listLength V I ------------------------------------ [E-Length] evalExpr FE EE length(E) intVal(I) O /*we make these fixed because there aren't any other type of list values that it would make sense to add; they are already precluded by the definitions above, like E-Null-*, E-Head, E-Tail*/ Fixed Judgment listIndex : value int value Fixed Judgment listLength : value int ============================ [LI-0] listIndex consVal(V, Tl) 0 V N - 1 = I listIndex Tl I V ============================= [LI-Step] listIndex consVal(Hd, Tl) N V =================== [LL-Nil] listLength nilVal 0 listLength Tl I I + 1 = N ============================ [LL-Cons] listLength consVal(Hd, Tl) N /******************************************************************** Statement Evaluation ********************************************************************/ lookupScopes L EE LV evalExpr FE EE I intVal(N) O1 evalExpr FE EE E V O2 updateListIndex LV N V LV2 /*make the new list*/ replaceScopes L LV2 EE EE1 /*put it in its place*/ O1 ++ O2 = O ---------------------------------------- [E-ListUpdate] evalStmt FE EE listUpdate(L, I, E) EE1 O evalExpr FE EE L LV O1 iterateList FE EE LV X Body EE1 O2 O1 ++ O2 = O -------------------------------------------- [E-ListForeach] evalStmt FE EE listForeach(X, L, Body) EE1 O /*original list, index, new value, new list*/ Fixed Judgment updateListIndex : value int value value ========================================================== [ULI-0] updateListIndex consVal(VOld, Tl) 0 VNew consVal(VNew, Tl) N - 1 = I updateListIndex Tl I V TlNew ==================================================== [ULI-Step] updateListIndex consVal(X, Tl) N V consVal(X, TlNew) /*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]} ------------------------------------- [IL-Nil] iterateList FE EE nilVal X Body EE [] evalStmt FE [(X, Hd)]::EE Body Scope::EE1 O1 iterateList FE EE1 Tl X Body EE2 O2 O1 ++ O2 = O ---------------------------------------------- [IL-Cons] iterateList FE EE consVal(Hd, Tl) X Body EE2 O /* Why don't we have an actual rule, perhaps projecting V and iterating over that? That doesn't work because the use of null in the condition of the while loop to which listForeach projects does not look through the projection, and thus we cannot prove what we need for Ext_Ind for listForeach. */ 1 = 0 -------------------------------- [IL-Default]* iterateList FE EE V X Body EE1 O
Click on a command or tactic to see a detailed view of its use.
Module looseEval:list. Prove_Constraint looseEval:host:proj_expr_unique. [Show Proof] Prove_Constraint looseEval:host:proj_expr_is. [Show Proof] Prove_Constraint looseEval:host:proj_stmt_unique. [Show Proof] Prove_Constraint looseEval:host:proj_stmt_is. [Show Proof] Prove_Constraint looseEval:host:proj_stmt_other. [Show Proof] Prove_Constraint looseEval:host:proj_fun_unique. Prove_Constraint looseEval:host:proj_fun_is. Prove_Constraint looseEval:host:proj_param_unique. Prove_Constraint looseEval:host:proj_param_is. Prove_Constraint looseEval:host:proj_program_unique. Prove_Constraint looseEval:host:proj_program_is. Prove_Constraint looseEval:host:proj_typ_unique. [Show Proof] Prove_Constraint looseEval:host:proj_typ_is. [Show Proof] Prove_Constraint looseEval:host:proj_value_unique. [Show Proof] Prove_Constraint looseEval:host:proj_value_is. [Show Proof] /******************************************************************** Decidable Equality ********************************************************************/ Add_Proj_Rel looseEval:host:is_expr, looseEval:host:is_args, looseEval:host:is_recFieldExprs. Prove_Ext_Ind looseEval:host:is_expr, looseEval:host:is_args, looseEval:host:is_recFieldExprs. [Show Proof] Add_Proj_Rel looseEval:host:is_stmt. Prove_Ext_Ind looseEval:host:is_stmt. [Show Proof] Prove looseEval:host:is_args_nilArgs_or_consArgs. Prove looseEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. Add_Proj_Rel looseEval:host:is_value, looseEval:host:is_recFieldVals. Prove_Ext_Ind looseEval:host:is_value, looseEval:host:is_recFieldVals. [Show Proof] Prove looseEval:host:is_value_intVal_or_not. [Show Proof] Prove looseEval:host:is_value_trueVal_or_not. [Show Proof] Prove looseEval:host:is_value_falseVal_or_not. [Show Proof] Prove looseEval:host:is_value_stringVal_or_not. [Show Proof] Prove looseEval:host:is_value_recVal_or_not. [Show Proof] Extensible_Theorem is_value_nilVal_or_not : forall V, IsV : is_value V -> nilVal = V \/ (nilVal = V -> false) on IsV. [Show Proof] Extensible_Theorem is_value_consVal_or_not : forall V, IsV : is_value V -> (exists V1 V2, consVal V1 V2 = V) \/ ((exists V1 V2, consVal V1 V2 = V) -> false) on IsV. [Show Proof] Prove looseEval:host:is_recFieldVals_nil_or_cons. Prove looseEval:host:is_value_eq_or_not, looseEval:host:is_recFieldVals_eq_or_not. [Show Proof] /******************************************************************** Variables ********************************************************************/ Prove looseEval:host:vars_unique. [Show Proof] Prove looseEval:host:vars_is. [Show Proof] Prove looseEval:host:vars_exist, looseEval:host:varsArgs_exist, looseEval:host:varsRecFields_exist. [Show Proof] Prove_Constraint looseEval:host:proj_vars. [Show Proof] /******************************************************************** Typing ********************************************************************/ Prove looseEval:host:typeOf_isTy. [Show Proof] Prove looseEval:host:stmtOK_isCtx. [Show Proof] Prove looseEval:host:stmtOK_keep_scopes. [Show Proof] Prove looseEval:host:stmtOK_older_scopes_same. [Show Proof] Prove looseEval:host:stmtOK_first_scope_lookup_same. [Show Proof] Prove looseEval:host:typeOf_unique. [Show Proof] Prove looseEval:host:stmtOK_unique. [Show Proof] Prove looseEval:host:paramTy_is. Prove looseEval:host:getFunInfo_is. Prove looseEval:host:paramTy_exists. Prove looseEval: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, listLength L I -> is_integer I. [Show Proof] Theorem updateListIndex_is : forall L I V L', is_value L -> is_value V -> updateListIndex L I V L' -> is_value L'. [Show Proof] Prove looseEval:host:evalExpr_isValue, looseEval:host:evalStmt_isCtx, looseEval:host:evalArgs_isValue, looseEval: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 looseEval:host:evalExpr_isOutput, looseEval:host:evalStmt_isOutput, looseEval:host:evalArgs_isOutput, looseEval: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 looseEval:host:paramName_is. Prove looseEval:host:getFunEvalInfo_is. Prove looseEval:host:evalProgram_isOutput. Prove looseEval:host:evalStmt_names_same with iterateList_names_same : 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 -> names_same EE EE' on IL as IH_IL. [Show Proof] Add_Ext_Size looseEval:host:evalExpr, looseEval:host:evalArgs, looseEval:host:evalRecFields, looseEval:host:evalStmt with iterateList FE EE V X Body EE' O. Add_Proj_Rel looseEval:host:evalExpr, looseEval:host:evalArgs, looseEval:host:evalRecFields, looseEval:host:evalStmt with iterateList FE EE V X Body EE' O. Theorem listIndex_geq_0 : forall L I V, listIndex L I V -> is_integer I -> 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 looseEval:host:evalExpr_rel, looseEval:host:evalStmt_newNameScopes_output, looseEval:host:evalStmt_newNameScopes, looseEval:host:evalArgs_rel, looseEval:host:evalRecFields_rel 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] Prove looseEval:host:evalExpr_rel_exists_ES, looseEval:host:evalStmt_newNameScopes_exists_ES, looseEval:host:evalArgs_rel_exists_ES, looseEval:host:evalRecFields_rel_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 looseEval:host:evalExpr_scopes_same, looseEval:host:evalStmt_scopes_same, looseEval:host:evalStmt_scopes_same_ctx, looseEval:host:evalArgs_scopes_same, looseEval:host:evalRecFields_scopes_same 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 looseEval:host:evalExpr_scopes_same_exists, looseEval:host:evalStmt_scopes_same_exists, looseEval:host:evalArgs_scopes_same_exists, looseEval: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 append_nil_output : forall O, is_list is_value O -> O ++ [] = O. [Show Proof] Prove_Constraint looseEval:host:proj_evalExpr_exists. [Show Proof] Extensible_Theorem iterateList_to_while : forall FE EE V X Body EE' O Names L, 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 : names EE Names -> Fr : 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 on IL. [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 nilVal; listy (consVal Hd Tl) := listy Tl. %flip first list onto second, producing third Define flipOnto : value -> value -> value -> prop by flipOnto nilVal L L; flipOnto (consVal H T) L L' := flipOnto T (consVal H L) L'. Theorem eval_update_loop2 : forall (Hold SaveI SaveE L : string) V H 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, consVal H HoldL), (SaveI, intVal 0), (SaveE, V)]::G) -> (Hold = SaveI -> false) -> (Hold = L -> false) -> (SaveI = SaveE -> false) -> (SaveI = L -> false) -> (Hold = SaveE -> false) -> (SaveE = L -> false) -> lookupScopes L ([(Hold, consVal H HoldL), (SaveI, intVal 0), (SaveE, V)]::G) LVal -> exists G' LV, <evalStmt {P}> FE ([(Hold, consVal H HoldL), (SaveI, intVal 0), (SaveE, V)]::G) (while (not (null (name Hold))) (seq (assign L (cons (head (name Hold)) (name L))) (assign Hold (tail (name Hold))))) ([(Hold, nilVal), (SaveI, intVal 0), (SaveE, V)]::G') [] /\ replaceScopes L LV G G' /\ flipOnto (consVal H HoldL) LVal LV. [Show Proof] Theorem proj_listUpdate_eval : forall OldL I V NewL Hold HoldL SaveI SaveE G FE L, updateListIndex OldL I V NewL -> (Hold = SaveI -> false) -> (Hold = L -> false) -> (SaveI = SaveE -> false) -> (SaveI = L -> false) -> (Hold = SaveE -> false) -> (SaveE = L -> 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) -> lookupScopes L ([(Hold, HoldL), (SaveI, intVal I), (SaveE, V)]::G) OldL -> exists G' LV, <evalStmt {P}> FE ([(Hold, HoldL), (SaveI, intVal I), (SaveE, V)]::G) (seq (while (greater (name SaveI) (num 0)) (seq (assign SaveI (minus (name SaveI) (num 1))) (seq (assign Hold (cons (head (name L)) (name Hold))) (assign L (tail (name L)))))) (seq (assign L (cons (name SaveE) (tail (name L)))) (while (not (null (name Hold))) (seq (assign L (cons (head (name Hold)) (name L))) (assign Hold (tail (name Hold))))))) ([(Hold, nilVal), (SaveI, intVal 0), (SaveE, V)]::G') [] /\ replaceScopes L LV G G' /\ flipOnto HoldL NewL LV. [Show Proof] Prove_Constraint looseEval:host:proj_evalStmt_exists. [Show Proof] Prove_Constraint looseEval:host:proj_evalStmt_rel. [Show Proof] Prove_Ext_Ind looseEval:host:evalExpr, looseEval:host:evalArgs, looseEval:host:evalRecFields, looseEval: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 looseEval:host:paramName_unique. Prove_Constraint looseEval:host:proj_paramName_forward. Prove_Constraint looseEval:host:proj_paramName_back. Prove looseEval:host:getFunEvalInfo_unique. Prove_Constraint looseEval:host:proj_getFunEvalInfo_forward. Prove_Constraint looseEval:host:proj_getFunEvalInfo_back. Prove looseEval:host:evalProgram_unique. Prove_Constraint looseEval:host:proj_evalProgram. Prove_Constraint looseEval:host:proj_evalProgram_back. Theorem listIndex_typePres : forall L I V Ty, valueType L (listTy Ty) -> listIndex L I V -> valueType V Ty. [Show Proof] Theorem updateListIndex_typePres : forall L I V L' Ty, valueType L (listTy Ty) -> valueType V Ty -> updateListIndex L I V L' -> valueType L' (listTy Ty). [Show Proof] Prove looseEval:host:evalExpr_typePres, looseEval:host:evalStmt_typePres, looseEval:host:evalArgs_typePres, looseEval: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 looseEval:host:paramTy_paramName_same. Prove looseEval:host:funOK_getFunEvalInfo_related. Prove looseEval:host:evalExpr_output_forms, looseEval:host:evalStmt_output_forms, looseEval:host:evalArgs_output_forms, looseEval: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 looseEval:host:evalProgram_output_forms. Prove looseEval:host:paramName_exists. Prove looseEval:host:getFunEvalInfo_exists.