Module matchEval:translation Builds on matchEval:host /* We define here a "translation" from the language to itself. This represents an extension translating to another language (e.g. translating to assembly) and lets us explore what we can and cannot prove about a translation, but without the overhead of defining another language. */ Judgment transE : expr* expr Fixed Judgment transRF : recFieldExprs recFieldExprs Fixed Judgment transA : args args /*The [[string]] argument here needs to be passed down for translation in the default rule.*/ Judgment transS : [[string]] stmt* stmt [[string]] /*updates knowns*/ Judgment transF : fun* fun Fixed Judgment transFuns : [fun] [fun] Judgment transP : program* program /*turn a nested list into a flat one*/ Fixed Judgment join : [[A]] [A] -------------------- [TE-Num] transE num(I) num(I) transE E1 E11 transE E2 E21 ---------------------------------- [TE-Plus] transE plus(E1, E2) plus(E11, E21) transE E1 E11 transE E2 E21 ------------------------------------ [TE-Minus] transE minus(E1, E2) minus(E11, E21) transE E1 E11 transE E2 E21 ---------------------------------- [TE-Mult] transE mult(E1, E2) mult(E11, E21) transE E1 E11 transE E2 E21 -------------------------------- [TE-Div] transE div(E1, E2) div(E11, E21) ---------------- [TE-True] transE true true ------------------ [TE-False] transE false false transE E1 E11 transE E2 E21 -------------------------------- [TE-And] transE and(E1, E2) and(E11, E21) transE E1 E11 transE E2 E21 ------------------------------ [TE-Or] transE or(E1, E2) or(E11, E21) transE E E1 --------------------- [TE-Not] transE not(E) not(E1) transE E1 E11 transE E2 E21 ---------------------------------------- [TE-Greater] transE greater(E1, E2) greater(E11, E21) transE E1 E11 transE E2 E21 ------------------------------ [TE-Eq] transE eq(E1, E2) eq(E11, E21) -------------------------------- [TE-String] transE stringLit(S) stringLit(S) transE E1 E11 transE E2 E21 -------------------------------------------- [TE-StringApp] transE appString(E1, E2) appString(E11, E21) ---------------------- [TE-Name] transE name(X) name(X) transA A A1 ----------------------------- [TE-Call] transE call(F, A) call(F, A1) transRF RF RF1 --------------------------------- [TE-RecBuild] transE recBuild(RF) recBuild(RF1) transE E E1 ------------------------------------------------- [TE-RecFieldAccess] transE recFieldAccess(E, F) recFieldAccess(E1, F) transE E E1 ----------------------------------------- [TE-ErrorExpr] transE errorExpr(E, Ty) errorExpr(E1, Ty) |{expr}- E ~~> E_P transE E_P E1 -------------- [TE-Default]* transE E E1 ========================================= [TRF-Nil] transRF nilRecFieldExprs nilRecFieldExprs transE E E1 transRF RF RF1 ======================================= [TRF-Cons] {transRF consRecFieldExprs(F, E, RF) consRecFieldExprs(F, E1, RF1)} ====================== [TA-Nil] transA nilArgs nilArgs transE E E1 transA A A1 ====================================== [TA-Cons] transA consArgs(E, A) consArgs(E1, A1) ---------------------------- [TS-Noop] transS Names noop noop Names transS Names S1 S11 Names1 transS Names1 S2 S21 Names2 --------------------------------------------- [TS-Seq] transS Names seq(S1, S2) seq(S11, S21) Names2 transE E E1 --------------------------------------------------------- [TS-Declare] {transS Scope::Names declare(Ty, X, E) declare(Ty, X, E1) (X::Scope)::Names} transE E E1 --------------------------------------------- [TS-Assign] transS Names assign(X, E) assign(X, E1) Names transE E E1 ------------------------------------------- [TS-RecUpdate] {transS Names recUpdate(Rec, Fs, E) recUpdate(Rec, Fs, E1) Names} transE Cond Cond1 transS []::Names Th Th1 NamesTh transS []::Names El El1 NamesEl ------------------------------------------------ [TS-If] {transS Names ifThenElse(Cond, Th, El) ifThenElse(Cond1, Th1, El1) Names} transE Cond Cond1 transS []::Names Body Body1 Names1 -------------------------------------------------------- [TS-While] transS Names while(Cond, Body) while(Cond1, Body1) Names transS []::Names S S1 Names1 --------------------------------------------- [TS-ScopeStmt] transS Names scopeStmt(S) scopeStmt(S1) Names transE E E1 ------------------------------------------- [TS-Print] transS Names printVal(E) printVal(E1) Names join Names N N |{stmt}- S ~~> S_P transS Names S_P S1 Names1 -------------------------- [TS-Default]* transS Names S S1 Names1 ========== [Join-Nil] join [] [] join SRest Rest S ++ Rest = N =============== [Join-Cons] join S::SRest N paramTys Params PTys domain PTys Names transS [RetVar::Names] Body Body1 Names1 ------------------------------------------------------ [TF-Fun] {transF fun(F, RetTy, RetVar, InitVal, Params, Body) fun(F, RetTy, RetVar, InitVal, Params, Body1)} |{fun}- F ~~> F_P transF F_P F1 ----------------- [TF-Default]* transF F F1 =============== [TFs-Nil] transFuns [] [] transF F F1 transFuns Rest Rest1 =========================== [TFs-Cons] transFuns F::Rest F1::Rest1 transFuns Funs Funs1 transF Main Main1 ------------------------------------------------ [TP-Program] transP program(Funs, Main) program(Funs1, Main1) |{program}- P ~~> P_P transP P_P P1 --------------------- [TP-Default]* transP P P1
Click on a command or tactic to see a detailed view of its use.
Module matchEval:translation. Prove_Constraint matchEval:host:proj_expr_unique. Prove_Constraint matchEval:host:proj_expr_is. Prove_Constraint matchEval:host:proj_stmt_unique. Prove_Constraint matchEval:host:proj_stmt_is. Prove_Constraint matchEval:host:proj_stmt_other. 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. Prove_Constraint matchEval:host:proj_typ_is. Prove_Constraint matchEval:host:proj_value_unique. Prove_Constraint matchEval:host:proj_value_is. 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. Add_Proj_Rel matchEval:host:is_stmt. Prove_Ext_Ind matchEval:host:is_stmt. Prove matchEval:host:is_args_nilArgs_or_consArgs. Prove matchEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. Prove matchEval:host:vars_unique. Prove matchEval:host:vars_is. Prove matchEval:host:vars_exist, matchEval:host:varsArgs_exist, matchEval:host:varsRecFields_exist. Prove_Constraint matchEval:host:proj_expr_vars. Prove matchEval:host:typeOf_isTy. Prove matchEval:host:stmtOK_isCtx. Prove matchEval:host:stmtOK_keep_scopes. Prove matchEval:host:stmtOK_older_scopes_same. Prove matchEval:host:stmtOK_first_scope_lookup_same. Prove matchEval:host:typeOf_unique. Prove matchEval:host:stmtOK_unique. Prove matchEval:host:paramTy_is. Prove matchEval:host:getFunInfo_is. Prove matchEval:host:paramTy_exists. Prove matchEval:host:getFunInfo_exists. Prove matchEval:host:matchInt_is. Prove matchEval:host:matchString_is. Prove matchEval:host:matchRec_is. Prove matchEval:host:evalExpr_isValue, matchEval:host:evalStmt_isCtx, matchEval:host:evalArgs_isValue, matchEval:host:evalRecFields_isValue. Prove matchEval:host:evalExpr_isOutput, matchEval:host:evalStmt_isOutput, matchEval:host:evalArgs_isOutput, matchEval:host:evalRecFields_isOutput. Prove matchEval:host:paramName_is. Prove matchEval:host:getFunEvalInfo_is. Prove matchEval:host:evalProgram_isOutput. Prove matchEval:host:evalStmt_names_same. Prove matchEval:host:matchInt_unique. Prove matchEval:host:matchTrue_matchFalse_exclusive. Prove matchEval:host:matchString_unique. Prove matchEval:host:matchRec_unique. 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. Prove matchEval:host:matchRec_matchFalse_exclusive. 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. Add_Ext_Size matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt. Add_Proj_Rel matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt. 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. 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. 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. Prove_Constraint matchEval:host:proj_matchInt. Prove_Constraint matchEval:host:proj_matchTrue. Prove_Constraint matchEval:host:proj_matchFalse. Prove_Constraint matchEval:host:proj_matchString. Prove_Constraint matchEval:host:proj_matchRec. 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. 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. Prove_Constraint matchEval:host:matchTrue_proj. Prove_Constraint matchEval:host:matchFalse_proj. Prove_Constraint matchEval:host:matchString_proj. Prove_Constraint matchEval:host:matchRec_proj. 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. Prove_Constraint matchEval:host:proj_evalExpr_forward. Prove_Constraint matchEval:host:proj_evalStmt_forward. Prove_Ext_Ind matchEval:host:evalExpr, matchEval:host:evalArgs, matchEval:host:evalRecFields, matchEval:host:evalStmt. 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. Prove matchEval:host:matchRec_typePres. Prove matchEval:host:evalExpr_typePres, matchEval:host:evalStmt_typePres, matchEval:host:evalArgs_typePres, matchEval:host:evalRecFields_typePres. 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. Prove matchEval:host:evalProgram_output_forms. Prove matchEval:host:paramName_exists. Prove matchEval:host:getFunEvalInfo_exists. /******************************************************************** _______ _ _ _ |__ __| | | | | (_) | |_ __ __ _ _ __ ___| | __ _| |_ _ ___ _ __ | | '__/ _` | '_ \/ __| |/ _` | __| |/ _ \| '_ \ | | | | (_| | | | \__ \ | (_| | |_| | (_) | | | | |_|_| \__,_|_| |_|___/_|\__,_|\__|_|\___/|_| |_| _____ _ / ____| | | | | ___ _ __ _ __ ___ ___| |_ _ __ ___ ___ ___ | | / _ \| '__| '__/ _ \/ __| __| '_ \ / _ \/ __/ __| | |___| (_) | | | | | __/ (__| |_| | | | __/\__ \__ \ \_____\___/|_| |_| \___|\___|\__|_| |_|\___||___/___/ Translation Correctness ********************************************************************/ /******************************************************************** Is relations for translation ********************************************************************/ Theorem join_is : forall L J, is_list (is_list is_string) L -> join L J -> is_list is_string J. [Show Proof] Extensible_Theorem transE_is : forall E T, IsE : is_expr E -> Trans : transE E T -> is_expr T on Trans as IH_E also transA_is : forall A T, IsA : is_args A -> Trans : transA A T -> is_args T on Trans as IH_A, transRF_is : forall RF T, IsRF : is_recFieldExprs RF -> Trans : transRF RF T -> is_recFieldExprs T on Trans as IH_RF. [Show Proof] Extensible_Theorem transS_is : forall Names S T Names', IsS : is_stmt S -> IsNames : is_list (is_list is_string) Names -> Trans : transS Names S T Names' -> is_stmt T on Trans as IH_S, transS_isNames : forall Names S T Names', IsS : is_stmt S -> IsNames : is_list (is_list is_string) Names -> Trans : transS Names S T Names' -> is_list (is_list is_string) Names' on Trans as IH_C. [Show Proof] Theorem domain_is_tys : forall L D, is_list (is_pair is_string is_typ) L -> domain L D -> is_list is_string D. [Show Proof] Extensible_Theorem transF_is : forall F T, IsF : is_fun F -> Trans : transF F T -> is_fun T on Trans. [Show Proof] Theorem transFuns_is : forall Fs Ts, is_list is_fun Fs -> transFuns Fs Ts -> is_list is_fun Ts. [Show Proof] Extensible_Theorem transP_is : forall P T, IsP : is_program P -> Trans : transP P T -> is_program T on Trans. [Show Proof] /******************************************************************** Older scopes in translation names are not changed ********************************************************************/ Extensible_Theorem transS_old_scopes : forall Names Scope S S' Names', IsS : is_stmt S -> IsNames : is_list (is_list is_string) (Scope::Names) -> Trans : transS (Scope::Names) S S' Names' -> exists Scope', Names' = Scope'::Names on Trans. [Show Proof] /******************************************************************** Projection is unique under ctx_names ********************************************************************/ Theorem mem_names[K, V] : forall (EE : list (list (pair K V))) N X, names EE N -> mem X N -> exists V, mems (X, V) EE. [Show Proof] Theorem mems_names[K, V] : forall EE N (X : K) (V : V), names EE N -> mems (X, V) EE -> mem X N. [Show Proof] Theorem mem_join[A] : forall (L : list (list A)) J X, join L J -> mem X J -> mems X L. [Show Proof] Theorem mems_join[A] : forall L J (X : A), join L J -> mems X L -> mem X J. [Show Proof] Define ctx_names : list (list (pair K I)) -> list (list K) -> prop by ctx_names [] []; ctx_names (A::ARest) (B::BRest) := (forall K I, mem (K, I) A -> mem K B) /\ (forall K, mem K B -> exists I, mem (K, I) A) /\ ctx_names ARest BRest. Theorem ctx_names_add[K, I] : forall A B AS BS (K : K) (I : I), ctx_names (AS::A) (BS::B) -> ctx_names (((K, I)::AS)::A) ((K::BS)::B). [Show Proof] Theorem ctx_names_add_scope[K, I] : forall (A : list (list (pair K I))) B, ctx_names A B -> ctx_names ([]::A) ([]::B). [Show Proof] Theorem ctx_names_lookupScopes[K, I] : forall A B (K : K) (I : I), ctx_names A B -> lookupScopes K A I -> mems K B. [Show Proof] Theorem ctx_names_replaceScopes : forall A B X V A', is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list is_string) B -> ctx_names A B -> replaceScopes X V A A' -> ctx_names A' B. [Show Proof] Theorem ctx_names_mems_fwd[K, V] : forall EE N (X : K) (V : V), ctx_names EE N -> mems (X, V) EE -> mems X N. [Show Proof] Theorem ctx_names_mem_back[K, V] : forall EE N (X : K), ctx_names EE N -> mems X N -> exists (V : V), mems (X, V) EE. [Show Proof] Theorem proj_stmt_unique_ctx_names : forall S SA SB Names NA EE NB, is_stmt S -> is_list (is_list is_string) Names -> is_list (is_list (is_pair is_string is_value)) EE -> ctx_names EE Names -> join Names NA -> names EE NB -> NA |{stmt}- S ~~> SA -> NB |{stmt}- S ~~> SB -> SA = SB. [Show Proof] /******************************************************************** Evaluation and translation names are related ********************************************************************/ Theorem ctx_names_scopes_same : forall N EE_A EE_B, is_list (is_list (is_pair is_string is_value)) EE_A -> is_list (is_list (is_pair is_string is_value)) EE_B -> ctx_names EE_B N -> scopes_same EE_A EE_B -> ctx_names EE_A N. [Show Proof] Extensible_Theorem evalStmt_trans_ctx_names : forall Names S T Names' FE Scope EE EE' O, IsS : is_stmt S -> 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)) (Scope::EE) -> IsNames : is_list (is_list is_string) Names -> Ctxs : ctx_names (Scope::EE) Names -> Trans : transS Names S T Names' -> Ev : evalStmt FE (Scope::EE) S EE' O -> ctx_names EE' Names' on Ev. [Show Proof] /******************************************************************** Evaluation of original and translated terms is related ********************************************************************/ Define rel_FE : list (pair string (pair string (pair value (pair (list string) stmt)))) -> list (pair string (pair string (pair value (pair (list string) stmt)))) -> prop by rel_FE FE FE_T := (forall F RetVar RVVal PNames Body, lookup FE F (RetVar, RVVal, PNames, Body) -> exists Body_T Names, lookup FE_T F (RetVar, RVVal, PNames, Body_T) /\ transS [RetVar::PNames] Body Body_T Names) /\ (forall F RetVar RVVal PNames Body_T, lookup FE_T F (RetVar, RVVal, PNames, Body_T) -> exists Body Names, lookup FE F (RetVar, RVVal, PNames, Body) /\ transS [RetVar::PNames] Body Body_T Names). Theorem zip_ctx_names[A, B] : forall A B (Z : list (pair A B)), zip A B Z -> ctx_names [Z] [A]. [Show Proof] %all values in A are related to the values for corresponding names in %B by projedVal Define projedCtxs : list (list (pair string value)) -> list (list (pair string value)) -> prop by projedCtxs [] []; projedCtxs (A::ARest) (B::BRest) := (forall X VB, lookup B X VB -> exists VA, lookup A X VA) /\ (forall X VA, lookup A X VA -> exists VB, lookup B X VB) /\ (forall X VA VB, lookup A X VA -> lookup B X VB -> projedVal VA VB) /\ projedCtxs ARest BRest. Theorem projedCtxs_add_scope : forall A B, projedCtxs A B -> projedCtxs ([]::A) ([]::B). [Show Proof] Theorem projedCtxs_lookupScopes_exists : forall A B X VB, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> projedCtxs A B -> lookupScopes X B VB -> exists VA, lookupScopes X A VA /\ projedVal VA VB. [Show Proof] Theorem projedCtxs_lookupScopes : forall A B X VA VB, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> projedCtxs A B -> lookupScopes X A VA -> lookupScopes X B VB -> projedVal VA VB. [Show Proof] Theorem projedCtxs_replaceScopes_exists : forall A B X VA VB RB, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> projedCtxs A B -> projedVal VA VB -> replaceScopes X VB B RB -> exists RA, replaceScopes X VA A RA /\ projedCtxs RA RB. [Show Proof] Theorem projedCtxs_replaceScopes : forall A B X VA VB RA RB, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> projedCtxs A B -> projedVal VA VB -> replaceScopes X VA A RA -> replaceScopes X VB B RB -> projedCtxs RA RB. [Show Proof] Theorem scopes_same_projedCtxs : forall A B C, scopes_same A B -> projedCtxs B C -> projedCtxs A C. [Show Proof] Theorem projedCtxs_scopes_same : forall A B C, projedCtxs A B -> scopes_same B C -> projedCtxs A C. [Show Proof] Define projedArgs : list value -> list value -> prop by projedArgs [] []; projedArgs (VA::ARest) (VB::BRest) := projedVal VA VB /\ projedArgs ARest BRest. Theorem zip_projedArgs : forall N VA VB ZA ZB, projedArgs VA VB -> zip N VA ZA -> zip N VB ZB -> projedCtxs [ZA] [ZB]. [Show Proof] Extensible_Theorem trans_evalExpr_same : forall E T EE EE_T FE FE_T V V_T O O_T, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> RFE : rel_FE FE FE_T -> PC : projedCtxs EE EE_T -> Trans : transE E T -> Ev : evalExpr FE EE E V O -> EvT : evalExpr FE_T EE_T T V_T O_T -> projedVal V V_T /\ O = O_T on Ev as IH_E, trans_evalStmt_same : forall S T Names Names' Scope EE EE_T FE FE_T EE' EE_T' O O_T, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> PC : projedCtxs (Scope::EE) EE_T -> Ctxs : ctx_names (Scope::EE) Names -> Trans : transS Names S T Names' -> Ev : evalStmt FE (Scope::EE) S EE' O -> EvT : evalStmt FE_T EE_T T EE_T' O_T -> O = O_T on Ev as IH_S, trans_evalStmt_relCtxs : forall S T Names Names' Scope EE EE_T FE FE_T EE' EE_T' O O_T, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> PC : projedCtxs (Scope::EE) EE_T -> Ctxs : ctx_names (Scope::EE) Names -> Trans : transS Names S T Names' -> Ev : evalStmt FE (Scope::EE) S EE' O -> EvT : evalStmt FE_T EE_T T EE_T' O_T -> projedCtxs EE' EE_T' on Ev as IH_S_C, trans_evalArgs_same : forall A T EE EE_T FE FE_T V V_T O O_T, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> RFE : rel_FE FE FE_T -> PC : projedCtxs EE EE_T -> Trans : transA A T -> Ev : evalArgs FE EE A V O -> EvT : evalArgs FE_T EE_T T V_T O_T -> projedArgs V V_T /\ O = O_T on Ev as IH_A, trans_evalRecFields_same : forall RF T EE EE_T FE FE_T V V_T O O_T, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> RFE : rel_FE FE FE_T -> PC : projedCtxs EE EE_T -> Trans : transRF RF T -> Ev : evalRecFields FE EE RF V O -> EvT : evalRecFields FE_T EE_T T V_T O_T -> projedFields V V_T /\ O = O_T on Ev as IH_RF. [Show Proof] Theorem paramTys_paramNames : forall Ps PTys D PNs, paramTys Ps PTys -> domain PTys D -> paramNames Ps PNs -> D = PNs. [Show Proof] Extensible_Theorem trans_getFunEvalInfo_rel : forall F Name RetVar RVVal PNames Body F_T Name_T RetVar_T RVVal_T PNames_T Body_T, IsF : is_fun F -> Trans : transF F F_T -> GFEI : getFunEvalInfo F Name RetVar RVVal PNames Body -> GFEI_T : getFunEvalInfo F_T Name_T RetVar_T RVVal_T PNames_T Body_T -> exists N, Name = Name_T /\ RetVar = RetVar_T /\ RVVal = RVVal_T /\ PNames = PNames_T /\ transS [RetVar::PNames] Body Body_T N on Trans. [Show Proof] Theorem trans_getFunEvalCtx_rel_FE : forall Fs Fs_T FE FE_T, is_list is_fun Fs -> transFuns Fs Fs_T -> getFunEvalCtx Fs FE -> getFunEvalCtx Fs_T FE_T -> rel_FE FE FE_T. [Show Proof] /******************************************************************** If the original evaluates, so does the translation ********************************************************************/ Theorem projedCtxs_lookupScopes_exists_forward : forall A B X VA, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> projedCtxs A B -> lookupScopes X A VA -> exists VB, lookupScopes X B VB /\ projedVal VA VB. [Show Proof] Theorem projedArgs_zip[N] : forall A B (N : list N) Z, projedArgs A B -> zip N A Z -> exists Z', zip N B Z'. [Show Proof] Theorem projedFields_lookup_exists : forall FA FB X VA, projedFields FA FB -> lookup FA X VA -> exists VB, lookup FB X VB /\ projedVal VA VB. [Show Proof] Theorem projedCtxs_replaceScopes_exists_forward: forall A B X VA VB RA, is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> is_string X -> projedCtxs A B -> projedVal VA VB -> replaceScopes X VA A RA -> exists RB, replaceScopes X VB B RB /\ projedCtxs RA RB. [Show Proof] Theorem projedFields_replaceRecVal_exists_forward : forall F VA VB FA RA FB, projedFields FA FB -> projedVal VA VB -> replaceRecVal F VA FA RA -> exists RB, replaceRecVal F VB FB RB /\ projedFields RA RB. [Show Proof] Theorem projedFields_updateRecFields_exists_forward : forall FA FB Fs VA VB RA, is_list (is_pair is_string is_value) FA -> projedFields FA FB -> projedVal VA VB -> updateRecFields Fs VA FA RA -> exists RB, updateRecFields Fs VB FB RB /\ projedFields RA RB. [Show Proof] Theorem projedVal_recVal : forall Fs V, projedVal (recVal Fs) V -> exists Fs', V = recVal Fs'. [Show Proof] Theorem projedVal_intVal : forall I V, projedVal (intVal I) V -> V = intVal I. [Show Proof] Theorem projedVal_stringVal : forall S V, projedVal (stringVal S) V -> V = stringVal S. [Show Proof] Theorem projedVal_trueVal : forall V, projedVal trueVal V -> V = trueVal. [Show Proof] Theorem projedVal_falseVal : forall V, projedVal falseVal V -> V = falseVal. [Show Proof] Extensible_Theorem trans_evalExpr_forward : forall E T EE EE_T FE FE_T V O, IsE : is_expr E -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> RFE : rel_FE FE FE_T -> PC : projedCtxs EE EE_T -> Trans : transE E T -> Ev : evalExpr FE EE E V O -> exists V_T, evalExpr FE_T EE_T T V_T O on Ev as IH_E, trans_evalStmt_forward : forall S T Names Names' Scope EE EE_T FE FE_T EE' O, IsS : is_stmt S -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> PC : projedCtxs (Scope::EE) EE_T -> Ctxs : ctx_names (Scope::EE) Names -> Trans : transS Names S T Names' -> Ev : evalStmt FE (Scope::EE) S EE' O -> exists EE_T', evalStmt FE_T EE_T T EE_T' O on Ev as IH_S, trans_evalArgs_forward : forall A T EE EE_T FE FE_T V O, IsA : is_args A -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> RFE : rel_FE FE FE_T -> PC : projedCtxs EE EE_T -> Trans : transA A T -> Ev : evalArgs FE EE A V O -> exists V_T, evalArgs FE_T EE_T T V_T O on Ev as IH_A, trans_evalRecFields_forward : forall RF T EE EE_T FE FE_T V O, IsRF : is_recFieldExprs RF -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsFE_T : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE_T -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsEE_T : is_list (is_list (is_pair is_string is_value)) EE_T -> RFE : rel_FE FE FE_T -> PC : projedCtxs EE EE_T -> Trans : transRF RF T -> Ev : evalRecFields FE EE RF V O -> exists V_T, evalRecFields FE_T EE_T T V_T O on Ev as IH_RF. [Show Proof] Extensible_Theorem trans_getFunEvalInfo_forward : forall F F_T Name RetVar RVVal PNames Body, IsF : is_fun F -> Trans : transF F F_T -> GFEI : getFunEvalInfo F Name RetVar RVVal PNames Body -> exists Body_T, getFunEvalInfo F_T Name RetVar RVVal PNames Body_T on Trans. [Show Proof] Theorem trans_getFunEvalCtx_forward : forall Fs Fs_T FE, is_list is_fun Fs -> transFuns Fs Fs_T -> getFunEvalCtx Fs FE -> exists FE_T, getFunEvalCtx Fs_T FE_T. [Show Proof] Theorem projedCtxs_reflexive : forall L, is_list (is_list (is_pair is_string is_value)) L -> projedCtxs L L. [Show Proof] /*Programs evaluate the same with the same arguments*/ Extensible_Theorem trans_evalProgram_forward : forall P P_T A O, IsP : is_program P -> IsA : is_list is_value A -> Trans : transP P P_T -> Ev : evalProgram A P O -> evalProgram A P_T O on Trans. [Show Proof] /* We can't prove the backward direction as we don't know anything about the evaluation of an original term based on its projection evaluating. Thus it could be we translate a program for the purpose of running it, and that translation evaluates in situations where the original would not. */ /* Note something we might want to prove here but don't is that a term translates under certain circumstances. We can prove any term built entirely by constructors introduced by the host language translates. However, we cannot prove this generically for constructors that might be introduced by other extensions. Such constructors would translate via projection, and the host language has not required a projection exist for extension syntax in general under any circumstances. It does require expressions and statements project if they evaluate, as part of the projection version of the evaluation relations, and thus we know any expression or statement that evaluates also translates. However, we do not have this knowledge for functions or programs, and thus cannot say their translations exist. Thus we must be satisfied with saying things about the behavior of the translation and the original only when we know the translation exists. */