Executable Specification

[View trans]

Reasoning

[View cc_sem_pres]

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}.

Theorem equiv_cc_val' : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {val' V'}.

Theorem equiv_cc_tm : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {tm V}.

Theorem equiv_cc_tm' : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cc T K V V' -> {tm' V'}.

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'.

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)))).
  
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))).

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'.

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'.
 
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').

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').

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').
        

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').

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').

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').


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'.

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'.

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. 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'. 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}. 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}. 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. 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. 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. % 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'}. 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'}. 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)}. Theorem mapvar_sync : forall Vs Map X M E, {mapvar Vs Map} -> {memb (map X (M E)) (Map E)} -> {memb X Vs}. 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'. % 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'. Theorem mapvar_prune_tm' : forall FVs ML, nabla (x:tm'), {mapvar FVs (ML x)} -> exists ML', ML = y\ML'. 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'. % 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'. 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}. 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}. % 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)}.