Click on a command or tactic to see a detailed view of its use.
%%%%%%%%%%%%%%%% % Proof for semantics preservation of closure conversion on STLC with recursion % Date : October 18, 2014 %%%%%%%%%%%%%%%% Specification "trans". Set types on. Import "eval". [View eval] Import "cc_typ_pres". [View cc_typ_pres] Import "subst". [View subst] % Definitions of the simulation relation between closed source and target terms % and the equivalence relation between closed source and target values. % Both are defined as step-indexing logical relations. Define sim_cc : ty -> nat -> tm -> tm' -> prop, equiv_cc : ty -> nat -> tm -> tm' -> prop by sim_cc T K M M' := forall J V, le J K -> {nstep J M V} -> {val V} -> exists V' N, {eval' M' V'} /\ {add J N K} /\ equiv_cc T N V V'; equiv_cc tnat K (nat N) (nat' N); equiv_cc tunit K unit unit'; equiv_cc (prod T1 T2) K (pair V1 V2) (pair' V1' V2') := equiv_cc T1 K V1 V1' /\ equiv_cc T2 K V2 V2'; equiv_cc (arr T1 T2) z (fix R) (clos' (abs' R') VE) := {val' VE} /\ {tm (fix R)} /\ {tm' (clos' (abs' R') VE)}; equiv_cc (arr T1 T2) (s K) (fix R) (clos' (abs' R') VE) := equiv_cc (arr T1 T2) K (fix R) (clos' (abs' R') VE) /\ forall V1 V1' V2 V2', equiv_cc T1 K V1 V1' -> equiv_cc (arr T1 T2) K V2 V2' -> sim_cc T2 K (R V2 V1) (R' (pair' V2' (pair' V1' VE))). Theorem equiv_cc_val : forall T K V V', {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {val V}.induction on 1. induction on 2. intros. case H1(keep). case H3. search. case H3. search. case H3. apply IH to H4 H2 _. apply IH to H5 H2 _. search. case H2. case H3. search. case H3. apply IH1 to H1 H6 H7. search.Theorem equiv_cc_val' : forall T K V V', {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {val' V'}.induction on 1. induction on 2. intros. case H1(keep). case H3. search. case H3. search. case H3. apply IH to H4 H2 _. apply IH to H5 H2 _. search. case H2. case H3. search. case H3. apply IH1 to H1 H6 H7. search.Theorem equiv_cc_tm : forall T K V V', {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {tm V}.induction on 1. induction on 2. intros. case H1(keep). case H3. search. case H3. search. case H3. apply IH to H4 H2 _. apply IH to H5 H2 _. search. case H2. case H3. search. case H3. apply IH1 to H1 H6 H7. search.Theorem equiv_cc_tm' : forall T K V V', {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {tm' V'}.induction on 1. induction on 2. intros. case H1(keep). case H3. search. case H3. search. case H3. apply IH to H4 H2 _. apply IH to H5 H2 _. search. case H2. case H3. search. case H3. apply IH1 to H1 H6 H7. search.Theorem equiv_cc_arr_val' : forall T1 T K R V, {is_nat K} -> equiv_cc (arr T1 T) K (fix R) V -> exists R' VE, V = clos' (abs' R') VE /\ {val' VE}. % Equivalence relations are closed under decressing indexes Theorem equiv_cc_closed : forall T K J V V', {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> le J K -> equiv_cc T J V V'.induction on 1. induction on 2. intros. case H1(keep). case H3. search. case H3. search. case H3. unfold. backchain IH. backchain IH. apply le_to_lt to _ H4. case H7. search. case H2(keep). apply lt_z_absurd to H8. apply lt_pred_le to _ H8. case H3. apply IH1 to H1 H9 H11 H10. search.Theorem equiv_cc_arr_cond : forall K T1 T2 R R' VE, {is_nat K} -> equiv_cc (arr T1 T2) K (fix R) (clos' (abs' R') VE) -> (forall J V1 V1' V2 V2', lt J K -> equiv_cc T1 J V1 V1' -> equiv_cc (arr T1 T2) J V2 V2' -> sim_cc T2 J (R V2 V1) (R' (pair' V2' (pair' V1' VE)))).induction on 1. intros. case H1. apply lt_z_absurd to H3. apply lt_pred_le to _ H3. apply le_to_lt to _ H7. case H8. case H2. backchain H10. case H2. apply IH to H6 H10. backchain H12.Theorem app_equiv_cc_arr : forall T1 T R F VE N1 N2 V1 V1' K, {is_sty (arr T1 T)} -> {is_nat N1} -> {is_nat N2} -> equiv_cc (arr T1 T) N1 (fix R) (clos' (abs' F) VE) -> equiv_cc T1 N2 V1 V1' -> lt K N1 -> lt K N2 -> sim_cc T K (R (fix R) V1) (F (pair' (clos' (abs' F) VE) (pair' V1' VE))).intros. case H1. apply equiv_cc_arr_cond to _ H4. backchain H10. backchain equiv_cc_closed with K = N2. backchain lt_to_le. backchain equiv_cc_closed with K = N1. backchain lt_to_le.Define equiv_cc_arr : ty -> nat -> tm -> tm' -> prop by equiv_cc_arr (arr T1 T2) K (fix R) (clos' (abs' R') VE) := {val' VE} /\ {tm (fix R)} /\ {tm' (clos' (abs' R') VE)} /\ forall J V1 V1' V2 V2', lt J K -> equiv_cc T1 J V1 V1' -> equiv_cc (arr T1 T2) J V2 V2' -> sim_cc T2 J (R V2 V1) (R' (pair' V2' (pair' V1' VE))). Theorem equiv_cc_arr_closed : forall J K T M M', {is_nat K} -> le J K -> equiv_cc_arr T K M M' -> equiv_cc_arr T J M M'.intros. case H3. unfold. search. search. search. intros. apply lt_le_compose to H8 H2. apply H7 to _ H9 H10. search.Theorem equiv_cc_arr_to_equiv_cc : forall T K M M', {is_nat K} -> {is_sty T} -> equiv_cc_arr T K M M' -> equiv_cc T K M M'.induction on 1. intros. case H3 (keep). case H1. search. unfold. apply equiv_cc_arr_closed to _ _ H3 with J = N. backchain le_succ. backchain le_refl. apply IH to H8 _ H9. search. intros. backchain H7. unfold. exists z. backchain add_comm.Theorem sim_cc_val_tm' : forall V T K M' V', {val V} -> {eval' M' V'} -> equiv_cc T K V V' -> sim_cc T K V M'. Theorem sim_cc_nat : forall K N, sim_cc tnat K (nat N) (nat' N). Theorem sim_cc_pred : forall K M M', sim_cc tnat K M M' -> sim_cc tnat K (pred M) (pred' M').intros. case H1. unfold. intros. apply nstep_pred_inv to H5 H4. case H3. case H8. assert {add J1 (s N1) (s N3)}. backchain add_s. apply H2 to _ H6 _ with J = J1. case H13. exists (nat' N'). exists N1. split. backchain eval'_pred_fwd. search. search.Theorem sim_cc_plus : forall K M1 M2 M1' M2', {is_nat K} -> sim_cc tnat K M1 M1' -> sim_cc tnat K M2 M2' -> sim_cc tnat K (plus M1 M2) (plus' M1' M2').intros. unfold. intros. apply nstep_plus_inv to H6 H5. assert le J1 K. apply add_s to H7. apply le_trans to _ H4. search. case H2. apply H12 to H11 H8 _. case H15. assert le J2 K. apply add_comm to _ H7. case H4. apply add_arg1_isnat to H16. case H17. search. apply add_s to H16. apply le_trans to _ H4. search. case H3. apply H17 to H16 H9 _. case H20. apply eval'_plus_fwd to H13 H18 H10. case H4. search.Theorem sim_cc_ifz : forall K T M M1 M2 M' M1' M2', {is_nat K} -> {is_sty T} -> sim_cc tnat K M M' -> sim_cc T K M1 M1' -> sim_cc T K M2 M2' -> sim_cc T K (ifz M M1 M2) (ifz' M' M1' M2').intros. unfold. intros. apply nstep_ifz_inv to _ _ H7. case H6. backchain add_arg1_isnat. case H11. % M evals to 0 apply le_trans to H9 H6. case H3. apply H15 to _ H12 _. apply le_trans to H10 H6. case H4. apply H20 to _ H13 _. case H18. case H6. exists V'1. exists N3. split. backchain eval'_ifz_fwd1. search. backchain equiv_cc_closed with K = N2. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = I, N1' = J. backchain add_arg2_isnat. % M evals to (s N) apply le_trans to H9 H6. case H3. apply H15 to _ H12 _. apply le_trans to H10 H6. case H5. apply H20 to _ H13 _. case H18. case H6. exists V'1. exists N3. split. backchain eval'_ifz_fwd2. search. backchain equiv_cc_closed with K = N2. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = I, N1' = J. backchain add_arg2_isnat.Theorem sim_cc_unit : forall K, sim_cc tunit K unit unit'. Theorem sim_cc_pair : forall T1 T2 K M1 M2 M1' M2', {is_nat K} -> {is_sty T1} -> {is_sty T2} -> sim_cc T1 K M1 M1' -> sim_cc T2 K M2 M2' -> sim_cc (prod T1 T2) K (pair M1 M2) (pair' M1' M2').intros. unfold. intros. apply nstep_pair_inv to _ H7. case H8. case H6 (keep). apply le_trans to _ H6. case H4. apply H16 to _ H10 _. assert le J1 J. unfold. exists I. backchain add_comm. backchain add_arg1_isnat. apply le_trans to H20 H6. case H5. apply H22 to _ H11 _. exists (pair' V' V'1). exists N. split. backchain eval'_pair_fwd. search. unfold. backchain equiv_cc_closed with K = N1. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = I, N1' = J. backchain add_arg2_isnat. backchain equiv_cc_closed with K = N2. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = J1, N1' = J. backchain add_arg2_isnat.Theorem sim_cc_fst : forall T1 T2 K M M', {is_nat K} -> {is_sty (prod T1 T2)} -> sim_cc (prod T1 T2) K M M' -> sim_cc T1 K (fst M) (fst' M').intros. unfold. intros. apply nstep_fst_inv to H6 H5. case H3. apply H9 to _ H8 _. case H4. case H10. apply add_s to H11. search. case H4. case H12. exists V1'. exists N1. split. backchain eval'_fst_fwd. search. apply add_le_complement to _ _ H11 H13. backchain le_succ. backchain le_refl. backchain add_arg1_isnat. backchain add_arg2_isnat. backchain equiv_cc_closed with K = N. case H2. search. backchain add_arg2_isnat.Theorem sim_cc_snd : forall T1 T2 K M M', {is_nat K} -> {is_sty (prod T1 T2)} -> sim_cc (prod T1 T2) K M M' -> sim_cc T2 K (snd M) (snd' M').intros. unfold. intros. apply nstep_snd_inv to H6 H5. case H3. apply H9 to _ H8 _. case H4. case H10. apply add_s to H11. search. case H4. case H12. exists V2'. exists N1. split. backchain eval'_snd_fwd. search. apply add_le_complement to _ _ H11 H13. backchain le_succ. backchain le_refl. backchain add_arg1_isnat. backchain add_arg2_isnat. backchain equiv_cc_closed with K = N. case H2. search. backchain add_arg2_isnat.Theorem sim_cc_nstep : forall T K M M' J I V, sim_cc T K M M' -> {nstep J M V} -> {val V} -> {add J I K} -> exists V', {eval' M' V'} /\ equiv_cc T I V V'.intros. case H1. apply H5 to _ H2 H3. exists V'. split. search. assert I = N. backchain add_arg2_det. case H9. search.Theorem sim_cc_closed_nstep' : forall T K N M M' M1', {nstep' N M1' M'} -> sim_cc T K M M' -> sim_cc T K M M1'.intros. unfold. intros. case H3. apply sim_cc_nstep to H2 H4 _ _. apply nstep'_eval_closed to _ H7. search.Theorem sim_cc_app : forall T1 T K M1 M1' M2 M2', {is_nat K} -> {is_sty (arr T1 T)} -> sim_cc (arr T1 T) K M1 M1' -> sim_cc T1 K M2 M2' -> sim_cc T K (app M1 M2) (let' M1' (g\ open' g (f\e\app' f (pair' g (pair' M2' e))))).intros. unfold. intros. % Invert the application evaluation assert exists J1 J2 J3 J23 J123 V2 R, {add J2 J3 J23} /\ {add J1 J23 J123} /\ J = s J123 /\ {nstep J1 M1 (fix R)} /\ {nstep J2 M2 V2} /\ {val V2} /\ {nstep J3 (R (fix R) V2) V}. backchain nstep_app_inv. case H8. % Compute the rest steps case H5. case H15. % N1 = K - J1 - 1 assert exists N1, {add J1 N1 N3}. backchain k_minus_n1. case H17. % N2 = K - J2 - 1 assert exists N2, {add J2 N2 N3}. backchain k_minus_n2. case H19. % Get equivalent arguments assert exists V1', {eval' M1' V1'} /\ equiv_cc (arr T1 T) (s N1) (fix R) V1'. backchain sim_cc_nstep. backchain add_s. case H21. assert exists V2', {eval' M2' V2'} /\ equiv_cc T1 (s N2) V2 V2'. backchain sim_cc_nstep. backchain add_s. case H24. % Get a number of steps for evaluating of the reduced beta-redex % K' = K - 1 - J1 - J2 assert exists K' J12, {add J1 J2 J12} /\ {add J3 N K'} /\ {add J12 K' N3}. backchain k_minus_n12. case H27. % Apply the equivalence relation between fix-point and closure to get a simulation relation assert lt K' (s N1). backchain sum_complement_to_lt1 with N1 = J1, N2 = J2, N = N3. case H1. search. assert lt K' (s N2). backchain sum_complement_to_lt2 with N1 = J1, N2 = J2, N = N3. case H1. search. apply equiv_cc_arr_val' to _ H23. assert {is_nat N1}. backchain add_arg2_isnat. search. assert sim_cc T K' (R (fix R) V2) (R' (pair' (clos' (abs' R') VE) (pair' V2' VE))). backchain app_equiv_cc_arr with T1 = T1, N1 = s N1, N2 = s N2, R = R, F = R'. assert {is_nat N1}. backchain add_arg2_isnat. search. assert {is_nat N2}. backchain add_arg2_isnat. search. % Apply the simulation relation to get the equivalence relation between values. assert exists V', {eval' (R' (pair' (clos' (abs' R') VE) (pair' V2' VE))) V'} /\ equiv_cc T N V V'. backchain sim_cc_nstep. case H35. % Finish this case exists V'. exists N. split. apply eval'_open_fwd to _ H25 H36 with R = R', M1 = (clos' (abs' R') VE). backchain eval'_let_fwd with R = (g\open' g (f\e\app' f (pair' g (pair' M2' e)))). search. search.% Equivalence relation between the source substitution % and the environment value Define subst_env_equiv_cc : olist -> nat -> list (map tm tm) -> tm' -> prop by subst_env_equiv_cc nil K ML unit'; subst_env_equiv_cc (of X T :: L) K ML (pair' V' VE) := exists V, subst_env_equiv_cc L K ML VE /\ member (map X V) ML /\ equiv_cc T K V V'. % Equivalence relation between explicit source and target substitutions. % The typing context has the form (x1:T1, ..., xn:Tn, x1':S1, ..., xm':Sm), % where x1 to xn are variables bound by either let binders or the function % arguments in the enclosing function, and x1' to xm' are free variables of % the enclosing function. Bound source variables x1,...,xn are mapped to % bound target variables y1,...,yn. Free source variables x1',...,xm' are % mapped to projectsions to the environment variable e. % The target substitution maps y1, ..., yn to values mapped from % x1,...,x_n by the source substitution, and e to an environment value % comprising of the values mapped from x1',...,xm' by the source substitution. Define subst_equiv_cc : olist -> nat -> list (map tm tm) -> list (map tm' tm') -> prop by nabla e, subst_equiv_cc L K ML (map e VE :: nil) := subst_env_equiv_cc L K ML VE; nabla x y, subst_equiv_cc (of x T :: L) K (map x V :: ML) (map y V' :: ML') := equiv_cc T K V V' /\ subst_equiv_cc L K ML ML'. Theorem subst_env_equiv_cc_closed : forall L K J ML VE, {is_nat K} -> ctx L -> subst_env_equiv_cc L K ML VE -> le J K -> subst_env_equiv_cc L J ML VE.induction on 3. intros. case H3. search. unfold. exists V. split. backchain IH. case H2. search. search. backchain equiv_cc_closed with K = K. case H2. search.Theorem subst_equiv_cc_closed : forall L K J ML ML', {is_nat K} -> ctx L -> subst_equiv_cc L K ML ML' -> le J K -> subst_equiv_cc L J ML ML'.induction on 3. intros. case H3. unfold. backchain subst_env_equiv_cc_closed. unfold. backchain equiv_cc_closed. case H2. search. backchain IH. case H2. search.Theorem subst_equiv_cc_extend : forall T L K ML ML' V V', nabla x y, subst_equiv_cc L K ML ML' -> equiv_cc T K V V' -> subst_equiv_cc (of x T :: L) K (map x V :: ML) (map y V' :: ML'). Theorem subst_env_equiv_cc_val' : forall L K ML VE, {is_nat K} -> ctx L -> subst_env_equiv_cc L K ML VE -> {val' VE}.induction on 3. intros. case H3. search. case H2. assert {val' VE1}. backchain IH. assert {val' V'}. backchain equiv_cc_val'. search.Theorem subst_env_equiv_cc_tm' : forall L K ML VE, {is_nat K} -> ctx L -> subst_env_equiv_cc L K ML VE -> {tm' VE}.induction on 3. intros. case H3. search. case H2. assert {tm' VE1}. backchain IH. assert {tm' V'}. backchain equiv_cc_tm'. search.Theorem subst_env_equiv_cc_vars_in_subst : forall L K ML VE Vs, subst_env_equiv_cc L K ML VE -> vars_of_ctx L Vs -> vars_in_subst Vs ML. Theorem subst_equiv_cc_vars_in_subst : forall L K Vs ML ML', subst_equiv_cc L K ML ML' -> vars_of_ctx L Vs -> vars_in_subst Vs ML.induction on 1. intros. case H1. backchain subst_env_equiv_cc_vars_in_subst. case H2. unfold. apply IH to H4 H5. backchain vars_in_subst_extend. search.Theorem subst_env_equiv_cc_mem : forall L K ML Vs E X, subst_env_equiv_cc L K ML E -> vars_of_ctx L Vs -> {memb X Vs} -> exists V, member (map X V) ML.induction on 3. intros. case H3. case H2. case H1. search. case H2. case H1. apply IH to H6 H5 H4. search.Theorem subst_equiv_cc_mem : forall L ML ML' K Vs X, subst_equiv_cc L K ML ML' -> vars_of_ctx L Vs -> {memb X Vs} -> exists V, member (map X V) ML.induction on 1. intros. case H1. backchain subst_env_equiv_cc_mem. case H2. case H3. search. apply IH to H5 H6 H7. search.% Accumulate the variables in the target substitutions Theorem eq_memb_rewrite_tm' : forall A B (X:tm) (M':tm' -> tm'), nabla (x:tm'), A = B -> {memb (map X (M' x)) (B x)} -> {memb (map X (M' x)) (A x)}. % Definitions for environments % element in the environment Define env_elem_aux : (tm' -> tm') -> prop by env_elem_aux (x\x); env_elem_aux (x\ snd' (R x)) := env_elem_aux R. Define env_elem : (tm' -> tm') -> prop by env_elem (x\ fst' (R x)) := env_elem_aux R. Theorem env_elem_aux_closed : forall E, nabla (x:tm'), env_elem_aux (E x) -> exists E', E = y\E'. Theorem env_elem_closed : forall E, nabla (x:tm'), env_elem (E x) -> exists E', E = y\E'. Theorem env_elem_aux_extend : forall E, env_elem_aux E -> env_elem_aux (x\ E (snd' x)). Theorem env_elem_extend : forall E, env_elem E -> env_elem (x\ E (snd' x)). Theorem env_elem_aux_eval'_cong : forall E E1 E2 V V', env_elem_aux E -> {eval' E1 V} -> {eval' E2 V} -> {eval' (E E1) V'} -> {eval' (E E2) V'}.induction on 1. intros. case H1. apply eval'_det to H2 H4. search. apply eval'_snd_inv to H4. apply IH to H5 H2 H3 H6. backchain eval'_snd_fwd.Theorem env_elem_eval'_cong : forall E E1 E2 V V', env_elem E -> {eval' E1 V} -> {eval' E2 V} -> {eval' (E E1) V'} -> {eval' (E E2) V'}.intros. case H1. apply eval'_fst_inv to H4. apply env_elem_aux_eval'_cong to H5 H2 H3 H6. backchain eval'_fst_fwd.Theorem mapvar_mem : forall FVs Map X E Env, nabla x, {mapvar FVs Map} -> {memb (map X E) (Map Env)} -> exists E', E = E' Env /\ env_elem E' /\ {memb (map X (E' x)) (Map x)}.induction on 1. intros. case H1. case H2. case H2. exists (x\fst' x). search. apply IH to H3 H4. apply env_elem_closed to H6. exists (x\ E'1 (snd' x)). split. search. apply env_elem_extend to H6. search. inst H7 with n1 = snd' n1. search.Theorem mapvar_sync : forall Vs Map X M E, {mapvar Vs Map} -> {memb (map X (M E)) (Map E)} -> {memb X Vs}.induction on 1. intros. case H1. case H2. case H2. search. apply mapvar_mem to H3 H4. apply env_elem_closed to H6. apply IH to H3 H7 with M = E'1, Map = Map1. search.Theorem eq_rewrite_eval' : forall (A : tm' -> tm') B C V, nabla x, A x = B x -> {eval' (B C) V} -> {eval' (A C) V}. % Semantics preservation lemma for transforming free variables Theorem fvar_sem_pres : forall L Vs Map ML K VE X T M' V, nabla e, {is_nat K} -> ctx L -> subst ML -> subst_env_equiv_cc L K ML VE -> vars_of_ctx L Vs -> {mapvar Vs Map} -> member (of X T) L -> {memb (map X (M' e)) (Map e)} -> app_subst ML X V -> exists V', {eval' (M' VE) V'} /\ equiv_cc T K V V'.induction on 6. intros. case H8. case H6. case H5. case H4. apply subst_var_eq to _ H14 H9. exists V'. split. apply equiv_cc_val' to _ _ H15. case H2. search. apply subst_env_equiv_cc_val' to _ _ H13. case H2. search. search. apply ctx_mem_sync to H2 H7 _ with T' = T1. search. case H6. case H5. case H4. apply eq_memb_rewrite_tm' to H11 H10. apply mapvar_mem to H12 H17. apply env_elem_closed to H19. apply env_elem_closed to H19. apply IH to _ _ _ H14 H13 H12 _ H20 H9 with T = T. apply mapvar_sync to H12 H20 with M = E'2, Map = Map1. apply lst_mem_to_ctx_mem to H13 H21. case H7(keep). apply ctx_mem_sync to H2 H7 _ with T' = T2. search. search. case H2. search. assert {eval' (E'2 (snd' (pair' V' VE1))) V'1}. assert {eval' (snd' (pair' V' VE1)) VE1}. apply equiv_cc_val' to _ _ H16. case H2. search. apply subst_env_equiv_cc_val' to _ _ H14. case H2. search. search. assert {eval' VE1 VE1}. apply subst_env_equiv_cc_val' to _ _ H14. case H2. search. backchain eval'_refl. apply env_elem_eval'_cong to H19 H24 H23 H21 with E = E'2. search. apply eq_rewrite_eval' to H18 H23. search.% Compute a mapping from a list containing bound and free variables in the source language and % a list containing corresponding bound variables and an environment parameter in the target language Define to_mapping : list tm -> list tm' -> list (map tm tm') -> prop by to_mapping Vs (E :: nil) (Map E) := {mapvar Vs Map}; to_mapping (X :: Vs) (X' :: Vs') (map X X' :: Map) := to_mapping Vs Vs' Map. Theorem eq_map_list_inv_tm' : forall (A: tm' -> tm' -> list (map tm tm')) B, nabla (x:tm'), A x = B x -> A = B. Theorem eq_map_list_inv_tm : forall (A: tm -> tm' -> list (map tm tm')) B, nabla (x:tm), A x = B x -> A = B. Theorem eq_map_list_rewrite_tm' : forall (A: tm' -> tm' -> list (map tm tm')) B X, A = B -> (z1\z2\ map X (fst' z2) :: (A z1 z2)) = (y\z2\(map X (fst' z2)) :: (B y z2)). Theorem eq_map_list_rewrite_tm : forall (A: tm -> tm' -> list (map tm tm')) B X, A = B -> (z1\z2\(map X (fst' z2)) :: (A z1 z2)) = (y\z2\(map X (fst' z2)) :: (B y z2)). Theorem mapvar_prune_tm : forall FVs ML, nabla (x:tm), {mapvar FVs (ML x)} -> exists ML', ML = y\ML'.induction on 1. intros. case H1. search. apply IH to H3. case H2. exists (z2\ (map FVs1 (fst' z2)) :: (ML' (snd' z2))). apply eq_map_list_inv_tm to H4. backchain eq_map_list_rewrite_tm.Theorem mapvar_prune_tm' : forall FVs ML, nabla (x:tm'), {mapvar FVs (ML x)} -> exists ML', ML = y\ML'.induction on 1. intros. case H1. search. apply IH to H3. case H2. exists (z2\ (map X (fst' z2)) :: (ML' (snd' z2))). apply eq_map_list_inv_tm' to H4. backchain eq_map_list_rewrite_tm'.Theorem vars_of_ctx_prune_tm : forall L Vs, nabla (x:tm), vars_of_ctx L (Vs x) -> exists Vs', Vs = y\Vs'. Theorem vars_of_subst'_prune_tm' : forall ML Vs, nabla (x:tm'), vars_of_subst' ML (Vs x) -> exists Vs', Vs = y\Vs'. Theorem to_mapping_prune_tm : forall Vs Vs' Map, nabla (x:tm), to_mapping Vs Vs' (Map x) -> exists Map', Map = y\Map'. Theorem to_mapping_prune_tm' : forall Vs Vs' Map, nabla (x:tm'), to_mapping Vs Vs' (Map x) -> exists Map', Map = y\Map'. % Semantics preservation lemma for transforming (either bound or free) variables Theorem var_sem_pres : forall L ML ML' K Vs Vs' Map X T V M' M'', {is_nat K} -> ctx L -> subst ML -> subst' ML' -> subst_equiv_cc L K ML ML' -> vars_of_ctx L Vs -> vars_of_subst' ML' Vs' -> to_mapping Vs Vs' Map -> member (of X T) L -> {memb (map X M') Map} -> app_subst ML X V -> app_subst ML' M' M'' -> exists V', {eval' M'' V'} /\ equiv_cc T K V V'.induction on 8. intros. case H8. case H7. case H14. case H5. apply mapvar_prune_tm' to H13. apply fvar_sem_pres to _ _ _ _ _ H13 H9 H10 _. case H12. case H18. search. case H16. case H10. case H6. case H7. case H5. case H15. case H13. case H9. apply subst_var_eq to H3 _ H11. apply subst'_var_eq to H4 _ H12. apply equiv_cc_val' to _ _ H16. case H2. search. apply eval'_refl to H18. search. apply member_prune to H18. case H6. case H7. case H5. case H16. case H13. apply vars_of_ctx_prune_tm to H15. apply vars_of_subst'_prune_tm' to H16. apply to_mapping_prune_tm to H13. apply to_mapping_prune_tm' to H13. apply memb_prune to H14. apply memb_prune to H14. case H11. case H12. case H9. apply IH to _ _ _ _ H18 H15 H16 H13 _ H14 H19 H20. case H4. search. case H3. search. case H2. search. search.% Semantics preservation lemma for mapping variables to environments Theorem mapenv_sem_pres : forall L L' ML ML' K Vs Vs' NFVs Map E E', {is_nat K} -> ctx L -> subst ML -> subst' ML' -> subst_equiv_cc L K ML ML' -> vars_of_ctx L Vs -> vars_of_subst' ML' Vs' -> to_mapping Vs Vs' Map -> prune_ctx NFVs L L' -> {mapenv NFVs Map E} -> app_subst ML' E E' -> exists VE', {eval' E' VE'} /\ subst_env_equiv_cc L' K ML VE'.induction on 10. intros. case H10. case H9. apply app_subst'_unit_comm to H11. search. case H9. apply app_subst'_pair_comm to H11. apply ctx_mem_to_lst_mem to H6 H14. apply subst_equiv_cc_mem to H5 H6 H18. apply subst_var to H3 H19. assert exists V', {eval' M1' V'} /\ equiv_cc T K V V'. backchain var_sem_pres. case H21. apply IH to _ _ _ _ _ _ _ _ H15 H13 H17. assert subst_env_equiv_cc (of X T :: L'1) K ML (pair' V' VE'). assert {eval' (pair' M1' M2') (pair' V' VE')}. backchain eval'_pair_fwd. search.Theorem mapvar_to_lst_mem : forall Vs Map M M' E, {mapvar Vs Map} -> {memb (map M M') (Map E)} -> {memb M Vs}. % Auxiliary lemmas for proving the main theorem Theorem map_mem_to_lst_mem : forall Vs Vs' Map M M', to_mapping Vs Vs' Map -> {memb (map M M') Map} -> {memb M Vs}.induction on 1. intros. case H1. backchain mapvar_to_lst_mem. case H2. search. apply IH to H3 H4. search.Theorem app_subst_var_val : forall L K ML ML' Vs M V, subst ML -> subst_equiv_cc L K ML ML' -> vars_of_ctx L Vs -> {memb M Vs} -> app_subst ML M V -> {val V}.intros. apply subst_equiv_cc_mem to H2 H3 H4. apply subst_var_eq to H1 H6 H5. apply subst_mem to H1 H6. search.% Semantics preservation theorem for closure conversion Theorem cc_sem_pres : forall L ML ML' K Vs Vs' Map T P P' M M', {is_nat K} -> ctx L -> subst ML -> subst' ML' -> subst_equiv_cc L K ML ML' -> vars_of_ctx L Vs -> vars_of_subst' ML' Vs' -> to_mapping Vs Vs' Map -> {L |- of M T} -> {cc Map Vs M M'} -> app_subst ML M P -> app_subst ML' M' P' -> sim_cc T K P P'.% Proof by induction on the closure conversion derivation induction on 10. intros. case H10. % Case: Natural numbers apply subst_closed_tm_eq to _ H11. apply subst'_closed_tm_eq to _ H12. apply of_nat_inv to H2 H9. backchain sim_cc_nat. % Case: Variable apply map_mem_to_lst_mem to _ H13. assert member (of M T) L. apply ctx_name to _ _ H14. backchain of_var_inv. apply var_sem_pres to _ _ _ _ _ _ _ _ H15 H13 _ _. backchain sim_cc_val_tm'. apply app_subst_var_val to _ _ _ _ H11. search. % Case: pred apply app_subst_pred_comm to H11. apply app_subst'_pred_comm to H12. case H9. assert sim_cc tnat K M'' M''1. backchain IH. backchain sim_cc_pred. % Context case apply ctx_focus_inv to _ _ H16. case H18. % Case: plus apply app_subst_plus_comm to H11. apply app_subst'_plus_comm to H12. case H9. assert sim_cc tnat K M1'1 M1'2. backchain IH. assert sim_cc tnat K M2'1 M2'2. backchain IH with M = M2, M' = M2'. backchain sim_cc_plus. % Context case apply ctx_focus_inv to _ _ H19. case H21. % Case: ifz apply app_subst_ifz_comm to H11. apply app_subst'_ifz_comm to H12. case H9. assert sim_cc tnat K M'2 M'3. backchain IH. assert sim_cc T K M1'1 M1'2. backchain IH. assert sim_cc T K M2'1 M2'2. backchain IH with M = M2, M' = M2'. backchain sim_cc_ifz. backchain of_is_sty with M = M1. % context case apply ctx_focus_inv to _ _ H22. case H24. % Case: unit apply subst_closed_tm_eq to _ H11. apply subst'_closed_tm_eq to _ H12. case H9. backchain sim_cc_unit. % Context case apply ctx_focus_inv to _ _ H13. case H15. % Case: pair apply app_subst_pair_comm to H11. apply app_subst'_pair_comm to H12. case H9. assert sim_cc T1 K M1'1 M1'2. backchain IH. assert sim_cc T2 K M2'1 M2'2. backchain IH with M = M2, M' = M2'. backchain sim_cc_pair. backchain of_is_sty. backchain of_is_sty. % Context case apply ctx_focus_inv to _ _ H19. case H21. % Case: fst apply app_subst_fst_comm to H11. apply app_subst'_fst_comm to H12. case H9. assert sim_cc (prod T T2) K M1' M1'1. backchain IH. backchain sim_cc_fst. backchain of_is_sty. % Context case apply ctx_focus_inv to _ _ H16. case H18. % Case: snd apply app_subst_snd_comm to H11. apply app_subst'_snd_comm to H12. case H9. assert sim_cc (prod T1 T) K M1' M1'1. backchain IH. backchain sim_cc_snd with T1 = T1. backchain of_is_sty. % Context case apply ctx_focus_inv to _ _ H16. case H18. % Case: let assert exists M2 R1, P = let M2 R1 /\ app_subst ML M1 M2 /\ nabla x, app_subst ML (R x) (R1 x). backchain app_subst_let_comm. case H15. assert exists M'2 R'1, P' = let' M'2 R'1 /\ app_subst ML' M'1 M'2 /\ nabla x, app_subst ML' (R' x) (R'1 x). backchain app_subst'_let_comm. case H18. case H9. % Get the simulation relation for let arguments assert sim_cc T1 K M2 M'2. backchain IH. % Get the equivalence relation for argument values unfold. intros. apply nstep_let_inv to _ H25. case H24. case H31. apply add_assoc to H27 H32. assert exists V1', {eval' M'2 V1'} /\ equiv_cc T1 (s N23) V1 V1'. backchain sim_cc_nstep. backchain add_s. case H35. apply of_is_sty to _ H21. assert {is_nat N23}. backchain add_arg2_isnat. apply equiv_cc_tm to _ _ H37. apply equiv_cc_tm' to _ _ H37. % Get the simulation relation for the body expressions % with binders substituted for argument values assert sim_cc T (s N23) (R1 V1) (R'1 V1'). backchain IH with L = of n1 T1 :: L, ML = (map n1 V1) :: ML, ML' = (map n2 V1') :: ML', Vs = n1 :: Vs, Vs' = n2 :: Vs', Map = (map n1 n2) :: Map, T = T, M = (R n1), M' = (R' n2). case H1. backchain ctx_extend. backchain subst'_extend. case H36. search. backchain subst_equiv_cc_extend. backchain subst_equiv_cc_closed. unfold. exists K1. backchain add_comm. backchain add_s. backchain explct_meta_subst_comm with E = R1. backchain explct_meta_subst'_comm with E = R'1. % Get the equivlance relation between evaluated body expressions assert exists V', {eval' (R'1 V1') V'} /\ equiv_cc T (s N) V V'. backchain sim_cc_nstep. backchain add_s. % Finish the proof by evaluation lemmas and % closedness of equivalence relations under decreasing indexes case H43. exists V'. exists N. split. backchain eval'_let_fwd. search. assert {is_nat N}. backchain add_arg2_isnat. backchain equiv_cc_closed with K = s N. backchain of_is_sty. unfold. exists (s z). backchain add_comm. % context case apply ctx_focus_inv to _ _ H21. case H23. % Case: fix-point % Type of the fix-point is preserved in a new context containing % only free variables in it. assert exists L', prune_ctx FVs L L' /\ {L' |- of (fix R) T}. backchain fvars_typing_pres with L = L, Vs = Vs, FVs = FVs. case H17. assert ctx L'. backchain prune_ctx_pres. case H19. assert vars_of_ctx L' FVs. backchain prune_ctx_vars_of. apply is_sty_str to _ H22. case H24 (keep). % Communtativity of substitutions for fix-point and closures assert exists R1, P = fix R1 /\ nabla f x, app_subst ML (R f x) (R1 f x). backchain app_subst_fix_comm. case H27. assert exists F' E', P' = clos' F' E' /\ app_subst ML' (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e))))) F' /\ app_subst ML' E E'. backchain app_subst'_clos_comm. case H29. % The code part of the closure is closed assert {tm' (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e)))))}. assert {tm' n5, tm' n3, tm' n4 |- tm' (R' n3 n4 n5)}. apply reified_env_exists to H20. assert {of' n5 Ty, of' n3 (arr T1 T2), of' n4 T1 |- of' (R' n3 n4 n5) T2}. backchain cc_clos_code_typ_pres with SL = L', R = R, FVs = FVs, Map = NMap, x = n2, f = n1, y = n4, g = n3, e = n5. backchain of'_to_tm' with T = T2, L = of' n4 T1 :: of' n3 (arr T1 T2) :: of' n5 Ty :: nil, Vs = n4 :: n3 :: n5 :: nil. apply sty_to_cty to H25. apply sty_to_cty to H26. apply reified_env_sty to _ H32. apply sty_to_cty to H36. search. search 7. % Explicit substitution has no effect on the code part because it is a closed term assert (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e))))) = F'. backchain subst'_closed_tm_eq. case H33. % Get the equivalence relation between the current source substitution and % the evaluated environment argument assert exists VE', {eval' E' VE'} /\ subst_env_equiv_cc L' K ML VE'. backchain mapenv_sem_pres. case H34. % Prove the equivalence relation between the fixed point and the converted closure assert equiv_cc (arr T1 T2) K (fix R1) (clos' (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e))))) VE'). assert equiv_cc_arr (arr T1 T2) K (fix R1) (clos' (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e))))) VE'). unfold. case H35. search. apply ctx_to_tm_ctx to H2 H6. apply of_to_tm to _ _ _ _ H9. apply subst_equiv_cc_vars_in_subst to H5 _. apply subst_result_closed_tm_alt to _ _ H39 _ H40 H11. search. assert {tm' VE'}. backchain subst_env_equiv_cc_tm' with L = L'. search. intros. assert {is_nat J}. case H37. backchain add_arg1_isnat. apply equiv_cc_tm to _ _ H38. apply equiv_cc_tm' to _ _ H38. apply equiv_cc_tm to _ _ H39. apply equiv_cc_tm' to _ _ H39. assert sim_cc T2 J (R1 V2 V1) (R' V2' V1' VE'). backchain IH with L = of n2 T1 :: of n1 (arr T1 T2) :: L', M = R n1 n2, M' = R' n3 n4 n5, Vs = (n2 :: n1 :: FVs), Vs' = (n4 :: n3 :: n5 :: nil), Map = (map n2 n4 :: map n1 n3 :: NMap n5), ML = (map n2 V1 :: map n1 V2 :: ML), ML' = (map n4 V1' :: map n3 V2' :: map n5 VE' :: nil). backchain ctx_extend. backchain ctx_extend. backchain subst_extend. backchain subst_extend. backchain equiv_cc_val with T = arr T1 T2, K = J. backchain equiv_cc_val with T = T1, K = J. backchain subst'_extend. backchain subst'_extend. backchain subst'_extend. case H35. backchain subst_env_equiv_cc_tm' with L = L'. backchain subst_env_equiv_cc_val' with L = L'. backchain equiv_cc_val' with T = arr T1 T2, K = J. backchain equiv_cc_val' with T = T1, K = J. backchain subst_equiv_cc_extend. backchain subst_equiv_cc_extend. unfold. backchain subst_env_equiv_cc_closed. backchain lt_to_le. backchain explct_meta_subst_comm with E = R1 V2. backchain explct_meta_subst_comm with E = x\ R1 x n2. assert exists N, {nstep' N (let' (fst' (pair' V2' (pair' V1' VE'))) (g\let' (fst' (snd' (pair' V2' (pair' V1' VE')))) (y\let' (snd' (snd' (pair' V2' (pair' V1' VE')))) (e\R' g y e)))) (R' V2' V1' VE')}. apply equiv_cc_val' to _ _ H38. apply equiv_cc_val' to _ _ H39. apply subst_env_equiv_cc_val' to _ _ H36. search 11. case H46. backchain sim_cc_closed_nstep' with N = N, M' = (R' V2' V1' VE'). backchain equiv_cc_arr_to_equiv_cc. % Prove the simulation relation from the equivalence relation unfold. intros. apply nstep_val_inv to _ H39. exists (clos' (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e))))) VE'). exists K. split. backchain eval'_clos_fwd. search. search. % Context case apply ctx_focus_inv to _ _ H21. case H23. % Case: application % Commutativity of substitutions. assert exists M3 M4, P = app M3 M4 /\ app_subst ML M1 M3 /\ app_subst ML M2 M4. backchain app_subst_app_comm. case H15. assert exists M3' M4', P' = (let' M3' (g\ open' g (f\e\app' f (pair' g (pair' M4' e))))) /\ app_subst ML' M1' M3' /\ app_subst ML' M2' M4'. apply app_subst'_let_comm to H12. apply app_subst'_open_comm to H19. apply app_subst_prune to H21. apply subst'_nabla to H4 with x = n1. apply app_subst_det to H20 H22. search. case H18. case H9. % Get the simulation relation of sub-expressions assert sim_cc (arr T1 T) K M3 M3'. backchain IH. assert sim_cc T1 K M4 M4'. backchain IH. % Finish this case apply of_is_sty to _ H21. backchain sim_cc_app. % Context case apply ctx_focus_inv to _ _ H21. case H23.Define sim_cc' : ty -> tm -> tm' -> prop by sim_cc' T M M' := forall K, {is_nat K} -> sim_cc T K M M'. Define equiv_cc' : ty -> tm -> tm' -> prop by equiv_cc' T M M' := forall K, {is_nat K} -> equiv_cc T K M M'. Define subst_equiv_cc' : olist -> list (map tm tm) -> list (map tm' tm') -> prop by subst_equiv_cc' L ML ML' := forall K, {is_nat K} -> subst_equiv_cc L K ML ML'. Theorem cc_sem_pres' : forall L ML ML' Vs Vs' Map T P P' M M', ctx L -> subst ML -> subst' ML' -> subst_equiv_cc' L ML ML' -> vars_of_ctx L Vs -> vars_of_subst' ML' Vs' -> to_mapping Vs Vs' Map -> {L |- of M T} -> {cc Map Vs M M'} -> app_subst ML M P -> app_subst ML' M' P' -> sim_cc' T P P'. % Semantics preservation for terms of type natural numbers Theorem cc_nat_sem_pres : forall M M' N, {of M tnat} -> {cc' M M'} -> {eval M (nat N)} -> {eval' M' (nat' N)}.intros. case H3. apply nstep_is_nat to H4. assert sim_cc tnat N1 M M'. backchain cc_sem_pres with L = nil, ML = nil, ML' = (map n1 unit' :: nil), Vs = nil, Vs' = (n1 :: nil), Map = nil, M = M, M' = M'. case H2. search. % Apply the simulation relation to prove the conclusion case H7. apply H8 to _ H4 H5 with J = N1. backchain le_refl. case H11. search.