Module exactEval:translation Builds on exactEval: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. */ /*The [[string]] argument here needs to be passed down for translation in the default rules.*/ Judgment transE : [[string]] expr* expr Fixed Judgment transRF : [[string]] recFieldExprs recFieldExprs Fixed Judgment transA : [[string]] args args 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 Names num(I) num(I) transE Names E1 E11 transE Names E2 E21 ---------------------------------------- [TE-Plus] transE Names plus(E1, E2) plus(E11, E21) transE Names E1 E11 transE Names E2 E21 ------------------------------------------ [TE-Minus] transE Names minus(E1, E2) minus(E11, E21) transE Names E1 E11 transE Names E2 E21 ---------------------------------------- [TE-Mult] transE Names mult(E1, E2) mult(E11, E21) transE Names E1 E11 transE Names E2 E21 -------------------------------------- [TE-Div] transE Names div(E1, E2) div(E11, E21) ---------------------- [TE-True] transE Names true true ------------------------ [TE-False] transE Names false false transE Names E1 E11 transE Names E2 E21 -------------------------------------- [TE-And] transE Names and(E1, E2) and(E11, E21) transE Names E1 E11 transE Names E2 E21 ------------------------------------ [TE-Or] transE Names or(E1, E2) or(E11, E21) transE Names E E1 --------------------------- [TE-Not] transE Names not(E) not(E1) transE Names E1 E11 transE Names E2 E21 ---------------------------------------------- [TE-Greater] transE Names greater(E1, E2) greater(E11, E21) transE Names E1 E11 transE Names E2 E21 ------------------------------------ [TE-Eq] transE Names eq(E1, E2) eq(E11, E21) -------------------------------------- [TE-String] transE Names stringLit(S) stringLit(S) transE Names E1 E11 transE Names E2 E21 -------------------------------------------------- [TE-StringApp] transE Names appString(E1, E2) appString(E11, E21) ---------------------------- [TE-Name] transE Names name(X) name(X) transA Names A A1 ----------------------------------- [TE-Call] transE Names call(F, A) call(F, A1) transS []::Names S S1 Names1 transE Names1 E E1 -------------------------------------------- [TE-StmtExpr] transE Names stmtExpr(S, E) stmtExpr(S1, E1) transRF Names RF RF1 --------------------------------------- [TE-RecBuild] transE Names recBuild(RF) recBuild(RF1) transE Names E E1 --------------------------------------- [TE-RecFieldAccess] {transE Names recFieldAccess(E, F) recFieldAccess(E1, F)} transE Names E E1 ----------------------------------------------- [TE-ErrorExpr] transE Names errorExpr(E, Ty) errorExpr(E1, Ty) join Names N N |{expr}- E ~~> E_P transE Names E_P E1 -------------------- [TE-Default]* transE Names E E1 =============================================== [TRF-Nil] transRF Names nilRecFieldExprs nilRecFieldExprs transE Names E E1 transRF Names RF RF1 ============================================= [TRF-Cons] {transRF Names consRecFieldExprs(F, E, RF) consRecFieldExprs(F, E1, RF1)} ============================ [TA-Nil] transA Names nilArgs nilArgs transE Names E E1 transA Names A A1 ============================================ [TA-Cons] transA Names 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 Scope::Names E E1 --------------------------------------------------------- [TS-Declare] {transS Scope::Names declare(Ty, X, E) declare(Ty, X, E1) (X::Scope)::Names} transE Names E E1 --------------------------------------------- [TS-Assign] transS Names assign(X, E) assign(X, E1) Names transE Names E E1 ------------------------------------------- [TS-RecUpdate] {transS Names recUpdate(Rec, Fs, E) recUpdate(Rec, Fs, E1) Names} transE Names 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 Names 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 Names 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 /* To show the translation only evaluates if the original does, we need to know all the names are bound. These relations give us a way to say all the names are bound, by having stmtNames for the bodies of functions be empty. */ Judgment programEmptyNames : program* Fixed Judgment funsEmptyNames : [fun] Fixed Judgment funEmptyNames : fun funsEmptyNames Funs funEmptyNames Main ------------------------------------- [PEN-Program] programEmptyNames program(Funs, Main) |{program}- P ~~> P_P programEmptyNames P_P --------------------- [PEN-Default]* programEmptyNames P ================= [FsEN-Nil] funsEmptyNames [] funEmptyNames F funsEmptyNames Rest ====================== [FsEN-Cons] funsEmptyNames F::Rest getFunEvalInfo F Name RetVar RVVal Params Body stmtNames [RetVar::Params] Body [] NamesOut ============================================== [FEN] funEmptyNames F
Click on a command or tactic to see a detailed view of its use.
Module exactEval:translation. Prove_Constraint exactEval:host:proj_expr_unique. Prove_Constraint exactEval:host:proj_expr_is. Prove_Constraint exactEval:host:proj_expr_other. Prove_Constraint exactEval:host:proj_stmt_unique. Prove_Constraint exactEval:host:proj_stmt_is. Prove_Constraint exactEval:host:proj_stmt_other. 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. Prove_Constraint exactEval:host:proj_typ_is. 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. Prove exactEval:host:is_args_nilArgs_or_consArgs. Prove exactEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. Prove exactEval:host:vars_unique. Prove exactEval:host:vars_is. Prove exactEval:host:vars_exist, exactEval:host:varsArgs_exist, exactEval:host:varsRecFields_exist. Prove exactEval:host:stmtNames_is, exactEval:host:stmtNames_isCtx, exactEval:host:exprNames_is. Prove exactEval:host:stmtNames_unique, exactEval:host:exprNames_unique. Prove exactEval:host:stmtNames_keep_older. Prove exactEval:host:stmtNames_exists, exactEval:host:exprNames_exists, exactEval:host:argsNames_exists, exactEval:host:recFieldNames_exists. Prove exactEval:host:stmtNames_not_in_ctx, exactEval:host:exprNames_not_in_ctx. Prove exactEval:host:stmtNames_relatedCtxs, exactEval:host:stmtNames_relatedCtxs_ctx_fwd, exactEval:host:stmtNames_relatedCtxs_ctx_back, exactEval:host:exprNames_relatedCtxs. Prove exactEval:host:stmtNames_increaseCtxs, exactEval:host:stmtNames_increaseCtxs_ctxs, exactEval:host:exprNames_increaseCtxs. Prove_Constraint exactEval:host:proj_exprNames. Prove_Constraint exactEval:host:proj_stmtNames. Prove_Constraint exactEval:host:proj_stmtNames_names_forward. Prove_Constraint exactEval:host:proj_stmtNames_names_backward. Prove exactEval:host:typeOf_isTy, exactEval:host:stmtOK_isCtx. Prove exactEval:host:stmtOK_keep_scopes. Prove exactEval:host:stmtOK_older_scopes_same. Prove exactEval:host:stmtOK_first_scope_lookup_same. Prove exactEval:host:typeOf_unique, exactEval:host:stmtOK_unique. Prove exactEval:host:paramTy_is. Prove exactEval:host:getFunInfo_is. Prove exactEval:host:paramTy_exists. Prove exactEval:host:getFunInfo_exists. 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. Prove exactEval:host:evalExpr_isOutput, exactEval:host:evalStmt_isOutput, exactEval:host:evalArgs_isOutput, exactEval:host:evalRecFields_isOutput. 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. 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. Add_Ext_Size exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. Add_Proj_Rel exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. 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. Prove exactEval:host:evalExpr_ctx_names, exactEval:host:evalStmt_ctx_names, exactEval:host:evalArgs_ctx_names, exactEval:host:evalRecFields_ctx_names. 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. 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. 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. Prove_Constraint exactEval:host:proj_evalExpr_forward. Prove_Constraint exactEval:host:proj_evalExpr_backward. Prove_Constraint exactEval:host:proj_evalStmt_forward. Prove_Constraint exactEval:host:proj_evalStmt_backward. Prove_Ext_Ind exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. 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. 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. 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. Prove exactEval:host:evalProgram_output_forms. Prove exactEval:host:paramName_exists. Prove exactEval: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 Names E T, IsE : is_expr E -> IsNames : is_list (is_list is_string) Names -> Trans : transE Names E T -> is_expr T on Trans as IH_E, 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_S_C also transA_is : forall Names A T, IsA : is_args A -> IsNames : is_list (is_list is_string) Names -> Trans : transA Names A T -> is_args T on Trans as IH_A, transRF_is : forall Names RF T, IsRF : is_recFieldExprs RF -> IsNames : is_list (is_list is_string) Names -> Trans : transRF Names RF T -> is_recFieldExprs T on Trans as IH_RF. [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] 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_expr_unique_ctx_names : forall E EA EB Names NA EE NB, is_expr E -> 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 |{expr}- E ~~> EA -> NB |{expr}- E ~~> EB -> EA = EB. [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 evalExpr_trans_ctx_names : forall Names E T FE EE V EE' 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 -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsNames : is_list (is_list is_string) Names -> Ctxs : ctx_names EE Names -> Trans : transE Names E T -> Ev : evalExpr FE EE E V EE' O -> ctx_names EE' Names on Ev as IH_E, 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 as IH_S, evalArgs_trans_ctx_names : forall Names A T FE EE V EE' 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 -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsNames : is_list (is_list is_string) Names -> Ctxs : ctx_names EE Names -> Trans : transA Names A T -> Ev : evalArgs FE EE A V EE' O -> ctx_names EE' Names on Ev as IH_A, evalRecFields_trans_ctx_names : forall Names RF T FE EE V EE' 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 -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> IsNames : is_list (is_list is_string) Names -> Ctxs : ctx_names EE Names -> Trans : transRF Names RF T -> Ev : evalRecFields FE EE RF V EE' O -> ctx_names EE' Names on Ev as IH_RF. [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] Extensible_Theorem trans_evalExpr_same : forall E T Names EE EE_T FE FE_T V V_T EE' EE_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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transE Names E T -> Ev : evalExpr FE EE E V EE' O -> EvT : evalExpr FE_T EE_T T V_T EE_T' O_T -> V = V_T /\ O = O_T on Ev as IH_E, trans_evalExpr_relCtxs : forall E T Names EE EE_T FE FE_T V V_T EE' EE_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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transE Names E T -> Ev : evalExpr FE EE E V EE' O -> EvT : evalExpr FE_T EE_T T V_T EE_T' O_T -> scopes_same EE' EE_T' on Ev as IH_E_C, % 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 -> SS : scopes_same (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 -> SS : scopes_same (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 -> scopes_same EE' EE_T' on Ev as IH_S_C, % trans_evalArgs_same : forall A T Names EE EE_T FE FE_T V V_T EE' EE_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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transA Names A T -> Ev : evalArgs FE EE A V EE' O -> EvT : evalArgs FE_T EE_T T V_T EE_T' O_T -> V = V_T /\ O = O_T on Ev as IH_A, trans_evalArgs_relCtxs : forall A T Names EE EE_T FE FE_T V V_T EE' EE_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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transA Names A T -> Ev : evalArgs FE EE A V EE' O -> EvT : evalArgs FE_T EE_T T V_T EE_T' O_T -> scopes_same EE' EE_T' on Ev as IH_A_C, % trans_evalRecFields_same : forall RF T Names EE EE_T FE FE_T V V_T EE' EE_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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transRF Names RF T -> Ev : evalRecFields FE EE RF V EE' O -> EvT : evalRecFields FE_T EE_T T V_T EE_T' O_T -> V = V_T /\ O = O_T on Ev as IH_RF, trans_evalRecFields_relCtxs : forall RF T Names EE EE_T FE FE_T V V_T EE' EE_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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transRF Names RF T -> Ev : evalRecFields FE EE RF V EE' O -> EvT : evalRecFields FE_T EE_T T V_T EE_T' O_T -> scopes_same EE' EE_T' on Ev as IH_RF_C. [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 ********************************************************************/ Extensible_Theorem trans_evalExpr_forward : forall E T Names EE EE_T FE FE_T V EE' 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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transE Names E T -> Ev : evalExpr FE EE E V EE' O -> exists EE_T', evalExpr FE_T EE_T T V EE_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 -> SS : scopes_same (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 Names EE EE_T FE FE_T V EE' 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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transA Names A T -> Ev : evalArgs FE EE A V EE' O -> exists EE_T', evalArgs FE_T EE_T T V EE_T' O on Ev as IH_A, trans_evalRecFields_forward : forall RF T Names EE EE_T FE FE_T V EE' 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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transRF Names RF T -> Ev : evalRecFields FE EE RF V EE' O -> exists EE_T', evalRecFields FE_T EE_T T V EE_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] /*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] /******************************************************************** If the translation evaluates, so does the original ********************************************************************/ /* I don't think we can prove this with both function calls and the generic case. If we have translation be the major induction measure, the generic case can be proven because the projection's translation is smaller and it doesn't matter what size the projection's translation's evaluation is because the major measure has decreased. We can't prove the case for function calls, though, because the function body's translation may be, and almost certainly is, larger. If we have evaluation as the major measure, the call case is fine because the evaluation of the function body is smaller even though the translation may be larger, but the generic case is a problem because the projection evaluation ... Maybe there isn't a problem if evaluation is the major measure, since we still have the same evaluation of the translation, even though the translation comes through projection? */ /* We need to know the original term has empty names in the generic cases below to lift the evaluation back across projection using proj_eval<Ty>_backward. However, this is then required for function bodies as well, so we use this to state it is so. */ Define emptyNames_FE : list (pair string (pair string (pair value (pair (list string) stmt)))) -> prop by emptyNames_FE FE := forall F RetVar RVVal Params Body, mem (F, RetVar, RVVal, Params, Body) FE -> exists EndNames, stmtNames [RetVar::Params] Body [] EndNames. Theorem ctx_names_mems[K, I] : forall (EE : list (list (pair K I))) NA NB X, ctx_names EE NA -> ctx_names EE NB -> mems X NA -> mems X NB. [Show Proof] Extensible_Theorem trans_evalExpr_backward : forall E T Names EE EE_T FE FE_T V EE_T' 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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> ENFE : emptyNames_FE FE -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transE Names E T -> EN : exprNames Names E [] -> Ev : evalExpr FE_T EE_T T V EE_T' O -> exists EE', evalExpr FE EE E V EE' O on Ev as IH_E_E, Trans * as IH_E, trans_evalStmt_backward : forall S T Names Names' Names'' Scope EE EE_T FE FE_T EE_T' 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 -> ENFE : emptyNames_FE FE -> SS : scopes_same (Scope::EE) EE_T -> Ctxs : ctx_names (Scope::EE) Names -> Trans : transS Names S T Names' -> SN : stmtNames Names S [] Names'' -> Ev : evalStmt FE_T EE_T T EE_T' O -> exists EE', evalStmt FE (Scope::EE) S EE' O on Ev as IH_S_E, Trans * as IH_S also trans_evalArgs_backward : forall A T Names EE EE_T FE FE_T V EE_T' 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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> ENFE : emptyNames_FE FE -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transA Names A T -> AN : argsNames Names A [] -> Ev : evalArgs FE_T EE_T T V EE_T' O -> exists EE', evalArgs FE EE A V EE' O on Ev as IH_A_E, Trans * as IH_A, trans_evalRecFields_backward : forall RF T Names EE EE_T FE FE_T V EE_T' 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 -> IsNames : is_list (is_list is_string) Names -> RFE : rel_FE FE FE_T -> ENFE : emptyNames_FE FE -> SS : scopes_same EE EE_T -> Ctxs : ctx_names EE Names -> Trans : transRF Names RF T -> RFN : recFieldNames Names RF [] -> Ev : evalRecFields FE_T EE_T T V EE_T' O -> exists EE', evalRecFields FE EE RF V EE' O on Ev as IH_RF_E, Trans * as IH_RF. [Show Proof] Extensible_Theorem trans_getFunEvalInfo_backward : forall F F_T Name RetVar RVVal PNames Body_T, IsF : is_fun F -> Trans : transF F F_T -> GFEI : getFunEvalInfo F_T Name RetVar RVVal PNames Body_T -> exists Body, getFunEvalInfo F Name RetVar RVVal PNames Body on Trans. [Show Proof] Theorem trans_getFunEvalCtx_backward : forall Fs Fs_T FE_T, is_list is_fun Fs -> transFuns Fs Fs_T -> getFunEvalCtx Fs_T FE_T -> exists FE, getFunEvalCtx Fs FE. [Show Proof] Theorem getFunEvalCtx_funsEmptyNames_emptyNames_FE : forall Fs FE, is_list is_fun Fs -> getFunEvalCtx Fs FE -> funsEmptyNames Fs -> emptyNames_FE FE. [Show Proof] /*Programs evaluate the same with the same arguments*/ Extensible_Theorem trans_evalProgram_backward : forall P P_T A O, IsP : is_program P -> IsA : is_list is_value A -> PEN : programEmptyNames P -> Trans : transP P P_T -> Ev : evalProgram A P_T O -> evalProgram A P O on Trans. [Show Proof] /* The statement of trans_evalProgram_backward is not as pleasing as the statement of trans_evalProgram_forward because of the inclusion of the programEmptyNames premise. A premise like this is necessary, telling us all the names in all the functions are bound, but it would be nice if we could put it in terms of something else, like typing. Unfortunately, the host language did not specify a relationship between typing and stmtNames, so even though this connection probably exists, we do not have it to use here. */ /* Something we could prove here is that the translation is always built entirely from constructs from the host language. We could do this by introducing a fixed relation is relation with rules only for constructs frem the host language. However, since we might want to translate to an extensible language, we want to leave the set of possible constructs open, so we don't do this. */ /* 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. */