Module matchEval:list Builds on matchEval:host /*Expressions*/ expr ::= ... | nil(typ) /*need type for type uniqueness*/ | cons(expr, expr) | head(expr) | tail(expr) | null(expr) /*Nothing useful to which these can project without conditionals | index(expr, expr) /*lst[i]*/ | length(expr)*/ ------------------------------------------------- [Proj-Nil] |{expr}- nil(Ty) ~~> recBuild(consRecFieldExprs("null", true, nilRecFieldExprs)) ------------------------------------------- [Proj-Cons] |{expr}- cons(E1, E2) ~~> recBuild( consRecFieldExprs("null", false, consRecFieldExprs("head", E1, consRecFieldExprs("tail", E2, nilRecFieldExprs)))) ---------------------------------------------- [Proj-Null] |{expr}- null(E) ~~> recFieldAccess(E, "null") ---------------------------------------------- [Proj-Head] |{expr}- head(E) ~~> recFieldAccess(E, "head") ---------------------------------------------- [Proj-Tail] |{expr}- tail(E) ~~> recFieldAccess(E, "tail") /*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 = E::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) /*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)))) /*Values*/ value ::= ... | nilVal | consVal(value, value) ------------------------------------------------ [Proj-NilVal] |{value}- nilVal ~~> recVal([("null", trueVal)]) ----------------------------------------------------------- [Proj-ConsVal] |{value}- consVal(V1, V2) ~~> recVal([("null", falseVal), ("head", V1), ("tail", V2)])
Module matchEval: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
Module matchEval: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 /******************************************************************** 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 HV Ty valueType TV listTy(Ty) ------------------------------------ [VT-Cons] valueType consVal(HV, TV) listTy(Ty)
Module matchEval: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 ----------------------------------- [MR-Nil] matchRec nilVal [("null", trueVal)] ----------------------------------------------------------- [MR-Cons] {matchRec consVal(V1, V2) [("null", falseVal), ("head", V1), ("tail", V2)]} /******************************************************************** Statement Evaluation ********************************************************************/ lookupScopes L EE LV evalExpr FE EE I VI O1 matchInt VI N 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. If we defined iteration through matching, we wouldn't *need* a default rule, as IL-Nil and IL-Cons would use matchNil and matchCons in their definitions, which would catch any value constructs from other extensions through the default rules for matchNil and matchCons. Thus, in either case, this is the default rule we have. */ 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 matchEval:list. /******************************************************************** Basic Projection Constraints ********************************************************************/ Prove_Constraint matchEval:host:proj_expr_unique. [Show Proof] Prove_Constraint matchEval:host:proj_expr_is. [Show Proof] Prove_Constraint matchEval:host:proj_stmt_unique. [Show Proof] Prove_Constraint matchEval:host:proj_stmt_is. [Show Proof] Prove_Constraint matchEval:host:proj_stmt_other. [Show Proof] Prove_Constraint matchEval:host:proj_fun_unique. Prove_Constraint matchEval:host:proj_fun_is. Prove_Constraint matchEval:host:proj_param_unique. Prove_Constraint matchEval:host:proj_param_is. Prove_Constraint matchEval:host:proj_program_unique. Prove_Constraint matchEval:host:proj_program_is. Prove_Constraint matchEval:host:proj_typ_unique. [Show Proof] Prove_Constraint matchEval:host:proj_typ_is. [Show Proof] Prove_Constraint matchEval:host:proj_value_unique. [Show Proof] Prove_Constraint matchEval:host:proj_value_is. [Show Proof] /******************************************************************** Decidable Equality ********************************************************************/ Add_Proj_Rel matchEval:host:is_expr, matchEval:host:is_args, matchEval:host:is_recFieldExprs. Prove_Ext_Ind matchEval:host:is_expr, matchEval:host:is_args, matchEval:host:is_recFieldExprs. [Show Proof] Add_Proj_Rel matchEval:host:is_stmt. Prove_Ext_Ind matchEval:host:is_stmt. [Show Proof] Prove matchEval:host:is_args_nilArgs_or_consArgs. Prove matchEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. /******************************************************************** Variables ********************************************************************/ Prove matchEval:host:vars_unique. [Show Proof] Prove matchEval:host:vars_is. [Show Proof] Prove matchEval:host:vars_exist, matchEval:host:varsArgs_exist, matchEval:host:varsRecFields_exist. [Show Proof] Prove_Constraint matchEval:host:proj_expr_vars. [Show Proof] /******************************************************************** Typing ********************************************************************/ Prove matchEval:host:typeOf_isTy. [Show Proof] Prove matchEval:host:stmtOK_isCtx. [Show Proof] Prove matchEval:host:stmtOK_keep_scopes. [Show Proof] Prove matchEval:host:stmtOK_older_scopes_same. [Show Proof] Prove matchEval:host:stmtOK_first_scope_lookup_same. [Show Proof] Prove matchEval:host:typeOf_unique. [Show Proof] Prove matchEval:host:stmtOK_unique. [Show Proof] Prove matchEval:host:paramTy_is. Prove matchEval:host:getFunInfo_is. Prove matchEval:host:paramTy_exists. Prove matchEval:host:getFunInfo_exists. /******************************************************************** Evaluation ********************************************************************/ 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 matchEval:host:matchInt_is. Prove matchEval:host:matchString_is. Prove matchEval:host:matchRec_is. [Show Proof] Prove matchEval:host:evalExpr_isValue, matchEval:host:evalStmt_isCtx, matchEval:host:evalArgs_isValue, matchEval: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 matchEval:host:evalExpr_isOutput, matchEval:host:evalStmt_isOutput, matchEval:host:evalArgs_isOutput, matchEval: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 matchEval:host:paramName_is. Prove matchEval:host:getFunEvalInfo_is. Prove matchEval:host:evalProgram_isOutput. Prove matchEval: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] 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, is_value L -> is_value V -> updateListIndex L I V OutA -> updateListIndex L I V OutB -> OutA = OutB. [Show Proof] Prove matchEval:host:matchInt_unique. Prove matchEval:host:matchTrue_matchFalse_exclusive. Prove matchEval:host:matchString_unique. Prove matchEval:host:matchRec_unique. [Show Proof] Prove matchEval:host:matchInt_matchTrue_exclusive. Prove matchEval:host:matchInt_matchFalse_exclusive. Prove matchEval:host:matchInt_matchString_exclusive. Prove matchEval:host:matchInt_matchRec_exclusive. Prove matchEval:host:matchString_matchTrue_exclusive. Prove matchEval:host:matchString_matchFalse_exclusive. Prove matchEval:host:matchString_matchRec_exclusive. Prove matchEval:host:matchRec_matchTrue_exclusive. [Show Proof] Prove matchEval:host:matchRec_matchFalse_exclusive. [Show Proof] Prove matchEval:host:evalExpr_rel, matchEval:host:evalExpr_rel_output, matchEval:host:evalStmt_newNameScopes_output, matchEval:host:evalStmt_newNameScopes, matchEval:host:evalArgs_rel, matchEval:host:evalArgs_rel_output, matchEval:host:evalRecFields_rel, matchEval:host:evalRecFields_rel_output 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 matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt with iterateList FE EE V X Body EE' O. Add_Proj_Rel matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt with iterateList FE EE V X Body EE' O. Prove matchEval:host:evalExpr_rel_exists_ES, matchEval:host:evalStmt_newNameScopes_exists_ES, matchEval:host:evalArgs_rel_exists_ES, matchEval: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 matchEval:host:evalExpr_scopes_same, matchEval:host:evalStmt_scopes_same, matchEval:host:evalStmt_scopes_same_ctx, matchEval:host:evalArgs_scopes_same, matchEval: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 matchEval:host:evalExpr_scopes_same_exists, matchEval:host:evalStmt_scopes_same_exists, matchEval:host:evalArgs_scopes_same_exists, matchEval: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] Prove_Constraint matchEval:host:proj_matchInt. [Show Proof] Prove_Constraint matchEval:host:proj_matchTrue. [Show Proof] Prove_Constraint matchEval:host:proj_matchFalse. [Show Proof] Prove_Constraint matchEval:host:proj_matchString. [Show Proof] Prove_Constraint matchEval:host:proj_matchRec. [Show Proof] Add_Proj_Rel matchEval:host:matchInt. Prove_Ext_Ind matchEval:host:matchInt. Add_Proj_Rel matchEval:host:matchTrue. Prove_Ext_Ind matchEval:host:matchTrue. Add_Proj_Rel matchEval:host:matchFalse. Prove_Ext_Ind matchEval:host:matchFalse. Add_Proj_Rel matchEval:host:matchRec. Prove_Ext_Ind matchEval:host:matchRec. [Show Proof] Add_Proj_Rel matchEval:host:matchString. Prove_Ext_Ind matchEval:host:matchString. Prove matchEval:host:projedVal_is. Prove matchEval:host:projedVal_matchInt. Prove matchEval:host:projedVal_matchString. Prove matchEval:host:projedVal_matchTrue. Prove matchEval:host:projedVal_matchFalse. Prove matchEval:host:projedVal_matchRec. Prove_Constraint matchEval:host:matchInt_proj. [Show Proof] Prove_Constraint matchEval:host:matchTrue_proj. [Show Proof] Prove_Constraint matchEval:host:matchFalse_proj. [Show Proof] Prove_Constraint matchEval:host:matchString_proj. [Show Proof] Prove_Constraint matchEval:host:matchRec_proj. [Show Proof] Prove matchEval:host:matchInt_projedVal. Prove matchEval:host:matchTrue_projedVal. Prove matchEval:host:matchFalse_projedVal. Prove matchEval:host:matchString_projedVal. Prove matchEval:host:matchRec_projedVal. Theorem projedFields_lookup_back : forall Fs Fs' X V', projedFields Fs Fs' -> lookup Fs' X V' -> exists V, lookup Fs X V /\ projedVal V V'. [Show Proof] Prove_Constraint matchEval:host:proj_evalExpr_forward. [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 VI, 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, VI), (SaveE, V)]::G) -> matchInt VI 0 -> (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, VI), (SaveE, V)]::G) LVal -> exists G' LV, <evalStmt {P}> FE ([(Hold, consVal H HoldL), (SaveI, VI), (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, VI), (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 VI, 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 -> matchInt VI I -> 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, VI), (SaveE, V)]::G) -> lookupScopes L ([(Hold, HoldL), (SaveI, VI), (SaveE, V)]::G) OldL -> exists G' LV VI', <evalStmt {P}> FE ([(Hold, HoldL), (SaveI, VI), (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, VI'), (SaveE, V)]::G') [] /\ matchInt VI' 0 /\ replaceScopes L LV G G' /\ flipOnto HoldL NewL LV. [Show Proof] Prove_Constraint matchEval:host:proj_evalStmt_forward. [Show Proof] Prove_Ext_Ind matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval: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 matchEval:host:paramName_unique. Prove_Constraint matchEval:host:proj_paramName_forward. Prove_Constraint matchEval:host:proj_paramName_back. Prove matchEval:host:getFunEvalInfo_unique. Prove_Constraint matchEval:host:proj_getFunEvalInfo_forward. Prove_Constraint matchEval:host:proj_getFunEvalInfo_back. Prove matchEval:host:evalProgram_unique. Prove_Constraint matchEval:host:proj_evalProgram_forward. Prove_Constraint matchEval:host:proj_evalProgram_back. 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 matchEval:host:matchRec_typePres. [Show Proof] Prove matchEval:host:evalExpr_typePres, matchEval:host:evalStmt_typePres, matchEval:host:evalArgs_typePres, matchEval: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 matchEval:host:paramTy_paramName_same. Prove matchEval:host:funOK_getFunEvalInfo_related. Prove matchEval:host:evalExpr_output_forms, matchEval:host:evalStmt_output_forms, matchEval:host:evalArgs_output_forms, matchEval: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 matchEval:host:evalProgram_output_forms. Prove matchEval:host:paramName_exists. Prove matchEval:host:getFunEvalInfo_exists.