Executable Specification

[View trans]

Reasoning

[View ch_sem_pres]

Click on a command or tactic to see a detailed view of its use.

%%%%%%%%%%%%%%%%
% Proof for semantics preservation of code hoisting for STLC with recursion
% Date  : November 08, 2015
%%%%%%%%%%%%%%%%

Specification "trans".

Import "eval". [View eval]
Import "ch_typ_pres". [View ch_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_ch   : ty -> nat -> tm' -> tm' -> prop,
       equiv_ch : ty -> nat -> tm' -> tm' -> prop by
  sim_ch 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_ch T N V V';
  equiv_ch tnat K (nat' N) (nat' N);
  equiv_ch tunit K unit' unit';
  equiv_ch (prod T1 T2) K (pair' V1 V2) (pair' V1' V2') := 
    equiv_ch T1 K V1 V1' /\ equiv_ch T2 K V2 V2';
  equiv_ch (arr' T1 T2) z (abs' R) (abs' R') :=
     {tm' (abs' R)} /\ {tm' (abs' R')};
  equiv_ch (arr' T1 T2) (s K) (abs' R) (abs' R') :=
     equiv_ch (arr' T1 T2) K (abs' R) (abs' R') /\
     forall V V', equiv_ch T1 K V V' -> sim_ch T2 K (R V) (htm nil (hbase (R' V')));
  equiv_ch (arr T1 T2) z (clos' (abs' R) VE)
                      (clos' (abs' R') VE') :=
    {tm' (clos' (abs' R) VE)} /\ {tm' (clos' (abs' R') VE')} /\
    {val' VE} /\ {val' VE'};
  equiv_ch (arr T1 T2) (s K) (clos' (abs' R) VE)
                          (clos' (abs' R') VE') :=
    equiv_ch (arr T1 T2) K (clos' (abs' R) VE) (clos' (abs' R') VE') /\
    forall V1 V1' V2 V2', 
      equiv_ch T1 K V1 V1' -> equiv_ch (arr T1 T2) K V2 V2' ->
        sim_ch T2 K (R (pair' V2 (pair' V1 VE))) 
                 (htm nil (hbase (R' (pair' V2' (pair' V1' VE'))))).

Theorem equiv_ch_val1 : forall T K V V',
  {is_cty T} -> {is_nat K} -> equiv_ch T K V V' -> {val' V}.

Theorem equiv_ch_val2 : forall T K V V',
  {is_cty T} -> {is_nat K} -> equiv_ch T K V V' -> {val' V'}.

Theorem equiv_ch_tm1 : forall T K V V',
  {is_cty T} -> {is_nat K} -> equiv_ch T K V V' -> {tm' V}.

Theorem equiv_ch_tm2 : forall T K V V',
  {is_cty T} -> {is_nat K} -> equiv_ch T K V V' -> {tm' V'}.

Theorem equiv_ch_arr'_abs : forall T1 T K R V,
  {is_nat K} -> equiv_ch (arr' T1 T) K (abs' R) V -> 
    exists R', V = (abs' R').

Theorem equiv_ch_arr_clos : forall T1 T K F E V,
  {is_nat K} -> equiv_ch (arr T1 T) K (clos' (abs' F) E) V -> 
    exists F' E', V = (clos' (abs' F') E').

% Equivalence relations are closed under decressing indexes
Theorem equiv_ch_closed : forall T K J V V', 
  {is_cty T} -> {is_nat K} -> equiv_ch T K V V' -> le J K -> equiv_ch T J V V'.

Define equiv_ch_arr' : ty -> nat -> tm' -> tm' -> prop by
  equiv_ch_arr' (arr' T1 T2) K (abs' R) (abs' R') :=
    {tm' (abs' R)} /\ {tm' (abs' R')} /\
    forall J V V', lt J K -> equiv_ch T1 J V V' -> 
      sim_ch T2 J (R V) (htm nil (hbase (R' V'))).

Theorem equiv_ch_arr'_closed : forall J K T M M',
  {is_nat K} -> le J K -> equiv_ch_arr' T K M M' -> equiv_ch_arr' T J M M'.

Theorem equiv_ch_arr'_to_equiv_ch : forall T K M M',
  {is_nat K} -> {is_cty T} -> equiv_ch_arr' T K M M' -> equiv_ch T K M M'.
 
Theorem equiv_ch_to_equiv_ch_arr' : forall K T1 T2 M M',
  {is_nat K} -> equiv_ch (arr' T1 T2) K M M' -> equiv_ch_arr' (arr' T1 T2) K M M'.

Theorem equiv_ch_arr'_cond : forall K T1 T2 R R',
  {is_nat K} -> equiv_ch (arr' T1 T2) K (abs' R) (abs' R') ->
  (forall J V1 V1', lt J K ->
      equiv_ch T1 J V1 V1' -> sim_ch T2 J (R V1) (htm nil (hbase (R' V1')))).
  
Theorem app_equiv_ch_arr' : forall T1 T R R' N1 N2 V1 V1' K,
  {is_cty (arr' T1 T)} -> {is_nat N1} -> {is_nat N2} -> 
    equiv_ch (arr' T1 T) N1 (abs' R) (abs' R') -> 
    equiv_ch T1 N2 V1 V1' -> lt K N1 -> lt K N2 ->
      sim_ch T K (R V1) (htm nil (hbase (R' V1'))).

Define equiv_ch_arr : ty -> nat -> tm' -> tm' -> prop by
  equiv_ch_arr (arr T1 T2) K (clos' (abs' R) VE) (clos' (abs' R') VE') :=
    {tm' (clos' (abs' R) VE)} /\ {tm' (clos' (abs' R') VE')} /\
    {val' VE} /\ {val' VE'} /\
    forall J V1 V1' V2 V2', lt J K ->
      equiv_ch T1 J V1 V1' -> equiv_ch (arr T1 T2) J V2 V2' ->
        sim_ch T2 J (R (pair' V2 (pair' V1 VE))) 
                 (htm nil (hbase (R' (pair' V2' (pair' V1' VE'))))).

Theorem equiv_ch_arr_closed : forall J K T M M',
  {is_nat K} -> le J K -> equiv_ch_arr T K M M' -> equiv_ch_arr T J M M'.

Theorem equiv_ch_arr_to_equiv_ch : forall T K M M',
  {is_nat K} -> equiv_ch_arr T K M M' -> equiv_ch T K M M'.
 
Theorem equiv_ch_to_equiv_ch_arr : forall K T1 T2 M M',
  {is_nat K} -> equiv_ch (arr T1 T2) K M M' -> equiv_ch_arr (arr T1 T2) K M M'.

Theorem app_equiv_ch_arr : forall T1 T F E F' E' N1 N2 V1 V1' K,
  {is_cty (arr' T1 T)} -> {is_nat N1} -> {is_nat N2} -> 
    equiv_ch (arr T1 T) N1 (clos' (abs' F) E) (clos' (abs' F') E') -> 
    equiv_ch T1 N2 V1 V1' -> lt K N1 -> lt K N2 ->
      sim_ch T K (F (pair' (clos' (abs' F) E) (pair' V1 E)))
              (htm nil (hbase (F' (pair' (clos' (abs' F') E') (pair' V1' E'))))).


%% Simulation lemmas
Theorem sim_ch_eval''_closed : forall T K M M' M'',
  sim_ch T K M M' -> (forall V, {eval'' M' V} -> {eval'' M'' V}) -> sim_ch T K M M''.

Theorem sim_ch_nstep : forall T K M M' J I V,
  sim_ch T K M M' -> {nstep' J M V} -> {val' V} -> {add J I K} -> 
    exists V', {eval'' M' V'} /\ equiv_ch T I V V'.

Theorem sim_ch_nat' : forall K N,
  sim_ch tnat K (nat' N) (htm nil (hbase (nat' N))).

Theorem sim_ch_pred' : forall K M M' M'' FE,
  sim_ch tnat K M (htm FE M') -> {hconstr M' (x\pred' x) M''} -> 
    sim_ch tnat K (pred' M) (htm FE M'').

Theorem sim_ch_plus' : forall K M1 M2 M1' M2' FE1 FE2 FE P,
  {is_nat K} -> sim_ch tnat K M1 (htm FE1 M1') -> sim_ch tnat K M2 (htm FE2 M2') ->
  {appd FE1 FE2 FE} -> {hcombine M1' M2' (x\y\plus' x y) P} ->
  sim_ch tnat K (plus' M1 M2) (htm FE P).

Theorem sim_ch_ifz' : forall K T M1 M2 M3 M1' M2' M3' FE1 FE2 FE12 FE3 FE P,
  {is_nat K} -> {is_cty T} -> {tm'' (htm FE2 M2')} -> {tm'' (htm FE3 M3')} -> 
  sim_ch tnat K M1 (htm FE1 M1') -> sim_ch T K M2 (htm FE2 M2') -> sim_ch T K M3 (htm FE3 M3') ->
  {appd FE1 FE2 FE12} -> {appd FE12 FE3 FE} ->
  {hcombine3 M1' M2' M3' (x\y\z\ifz' x y z) P} ->
    sim_ch T K (ifz' M1 M2 M3) (htm FE P).

Theorem sim_ch_unit' : forall K,
   sim_ch tunit K unit' (htm nil (hbase unit')).

Theorem sim_ch_pair' : forall K M1 M2 M1' M2' T1 T2 FE1 FE2 FE P,
  {is_nat K} -> {is_cty T1} -> {is_cty T2} ->
  sim_ch T1 K M1 (htm FE1 M1') -> sim_ch T2 K M2 (htm FE2 M2') ->
  {appd FE1 FE2 FE} -> {hcombine M1' M2' (x\y\pair' x y) P} ->
  sim_ch (prod T1 T2) K (pair' M1 M2) (htm FE P).

Theorem sim_ch_fst' : forall T1 T2 K FE M M' M'',
  {is_nat K} -> {is_cty (prod T1 T2)} -> sim_ch (prod T1 T2) K M (htm FE M') -> 
  {hconstr M' (x\fst' x) M''} -> sim_ch T1 K (fst' M) (htm FE M'').

Theorem sim_ch_snd' : forall T1 T2 K FE M M' M'',
  {is_nat K} -> {is_cty (prod T1 T2)} -> sim_ch (prod T1 T2) K M (htm FE M') -> 
  {hconstr M' (x\snd' x) M''} -> sim_ch T2 K (snd' M) (htm FE M'').

Theorem sim_ch_app' : forall K M1 M2 M1' M2' T1 T FE1 FE2 FE P,
  {is_nat K} -> {is_cty (arr' T1 T)} ->
  sim_ch (arr' T1 T) K M1 (htm FE1 M1') -> sim_ch T1 K M2 (htm FE2 M2') ->
  {appd FE1 FE2 FE} -> {hcombine M1' M2' (x\y\app' x y) P} ->
  sim_ch T K (app' M1 M2) (htm FE P).
intros. unfold. intros. % Invert the application evaluation apply nstep'_app_inv to _ H8. % Compute the rest steps case H7. case H16. % N1 = K - J1 - 1 assert exists N1, {add J1 N1 N3}. backchain k_minus_n1. case H18. % N2 = K - J2 - 1 assert exists N2, {add J2 N2 N3}. backchain k_minus_n2. case H20. % Get equivalent arguments assert exists V1', {eval'' (htm FE1 M1') V1'} /\ equiv_ch (arr' T1 T) (s N1) (abs' R) V1'. backchain sim_ch_nstep. backchain add_s. case H22. assert exists V2', {eval'' (htm FE2 M2') V2'} /\ equiv_ch T1 (s N2) V2 V2'. backchain sim_ch_nstep. backchain add_s. case H25. % 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 H28. % Apply the equivalence relation between closures 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. assert {is_nat N1}. backchain add_arg2_isnat. apply equiv_ch_arr'_abs to _ H24. assert sim_ch T K' (R V2) (htm nil (hbase (R' V2'))). backchain app_equiv_ch_arr' with T1 = T1, N1 = s N1, N2 = s N2, R = R, R' = R'. assert {is_nat N2}. backchain add_arg2_isnat. search. % Apply the simulation relation to get the equivalence relation between values. assert exists V', {eval'' (htm nil (hbase (R' V2'))) V'} /\ equiv_ch T N V V'. backchain sim_ch_nstep. case H36. case H37. % Finish this case exists V'. exists N. split. backchain eval''_app_fwd with M1 = M1', M2 = M2', R = R'. search. search.
Theorem sim_ch_clos' : forall K T1 T2 TL F E F' E' FE1 FE2 FE P, {is_nat K} -> {is_cty (arr T1 T2)} -> {is_cty TL} -> sim_ch (arr' (prod (arr T1 T2) (prod T1 TL)) T2) K F (htm FE1 F') -> sim_ch TL K E (htm FE2 E') -> {appd FE1 FE2 FE} -> {hcombine F' E' (x\y\clos' x y) P} -> sim_ch (arr T1 T2) K (clos' F E) (htm FE P). Theorem sim_ch_open' : forall K T1 T2 M1 M2 M1' M2' FE1 FE2 FE P, {is_nat K} -> {is_cty T1} -> {is_cty T2} -> sim_ch (arr T1 T2) K M1 (htm FE1 M1') -> sim_ch T1 K M2 (htm FE2 M2') -> {appd FE1 FE2 FE} -> {hcombine M1' M2' (x\y\ (open' x (f\ e\ app' f (pair' x (pair' y e))))) P} -> sim_ch T2 K (open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) (htm FE P).
intros. unfold. intros. % Invert the open evaluation apply nstep'_open_inv_sp to _ H9. % Use the simulation relations case H8. case H19. case H20. case H1. case H22. apply nstep'_is_nat to H9. case H24. case H25. % J1 = K - K1 - 2 assert exists J1, {add K1 J1 N1} /\ {add K123 N J1}. apply add_comm to _ H13. apply add_assoc to H27 H21. search. case H27. % J2 = K - K2 - 2 assert exists J2 K13 K131, {add K2 J2 N1} /\ {add K1 K3 K13} /\ {add K13 K1 K131} /\ {add K131 N J2}. apply add_arg1_isnat to H12. apply add_comm to _ H11. apply add_assoc to H31 H12. apply add_assoc to H33 H13. apply add_assoc to H35 H21. search. case H30. % Get equivalent arguments assert exists V1', {eval'' (htm FE1 M1') V1'} /\ equiv_ch (arr T1 T2) (s (s J1)) (clos' (abs' F) E) V1'. backchain sim_ch_nstep. backchain add_s. backchain add_s. case H35. assert exists V2', {eval'' (htm FE2 M2') V2'} /\ equiv_ch T1 (s (s J2)) V2 V2'. backchain sim_ch_nstep. backchain add_s. backchain add_s. case H38. % Get a number of steps for evaluating of the reduced beta-redex % K' = K - 2 - K1 - K1 - K2 assert exists K' DK1, {add K3 N K'} /\ {add K' K12 J1} /\ {add K1 K1 DK1} /\ {add K' DK1 J2}. apply add_arg1_isnat to H13. apply add_assoc to H12 H29. apply add_arg1_isnat to H34. apply add_comm to _ H33. apply add_assoc to H45 H34. apply add_assoc to H32 H46. apply add_assoc' to H49 H47. apply add_det to H42 H48. apply add_arg2_isnat to _ H28. apply add_arg2_isnat to _ H31. apply add_comm to _ H43. apply add_comm to _ H51. search. case H41. % Apply the equivalence relation between fix-point and closure to get a simulation relation assert lt K' (s (s J1)). unfold. exists (s K12). backchain add_s. backchain add_s. assert lt K' (s (s J2)). unfold. exists (s DK1). backchain add_s. backchain add_s. apply add_arg2_isnat to _ H28. apply add_arg2_isnat to _ H31. apply equiv_ch_arr_clos to _ H37. assert sim_ch T2 K' (F (pair' (clos' (abs' F) E) (pair' V2 E))) (htm nil (hbase (F' (pair' (clos' (abs' F') E') (pair' V2' E'))))). backchain app_equiv_ch_arr with T1 = T1, N1 = s (s J1), N2 = s (s J2), F = F, F' = F'. % Apply the simulation relation to get the equivalence relation between values. apply sim_ch_nstep to H50 H18 _ _. case H51. % Finish this case exists V'. exists N. split. backchain eval''_open_fwd with M1 = M1', M2 = M2', F = F', E = E'. search. search.
%% Equivalence relation between substitutions Define subst_equiv_ch : olist -> nat -> list (map tm' tm') -> list (map tm' tm') -> prop by subst_equiv_ch nil K nil nil; nabla x, subst_equiv_ch (of' x T :: L) K (map x V :: ML) (map x V' :: ML') := equiv_ch T K V V' /\ subst_equiv_ch L K ML ML'. Theorem subst_equiv_ch_mem : forall L ML ML' M T I, subst_equiv_ch L I ML ML' -> member (of' M T) L -> exists V V', member (map M V) ML /\ member (map M V') ML' /\ equiv_ch T I V V'. Theorem subst_equiv_ch_closed : forall L K J ML ML', {is_nat K} -> ctx' L -> subst_equiv_ch L K ML ML' -> le J K -> subst_equiv_ch L J ML ML'. Theorem subst_equiv_ch_extend : forall T L K ML ML' V V', nabla x, subst_equiv_ch L K ML ML' -> equiv_ch T K V V' -> subst_equiv_ch (of' x T :: L) K (map x V :: ML) (map x V' :: ML'). Theorem subst_equiv_ch_vars_of_subst' : forall L K Vs ML ML', subst_equiv_ch L K ML ML' -> vars_of_ctx' L Vs -> vars_of_subst' ML Vs /\ vars_of_subst' ML' Vs. Theorem subst'_hconstr_permute_aux : forall (ML:list (map tm' tm')) M M' P' R, app_subst ML M' P' -> {hconstr M R M'} -> exists P R', nabla x, app_subst ML M P /\ app_subst ML (R x) (R' x) /\ {hconstr P R' P'}. Theorem subst'_hconstr_permute : forall (ML:list (map tm' tm')) M M' P' FE FE' R, nabla x, {tm' x |- tm' (R x)} -> app_subst ML (htm FE M') (htm FE' P') -> {hconstr M R M'} -> exists P, app_subst ML (htm FE M) (htm FE' P) /\ {hconstr P R P'}. Theorem subst'_hcombine_permute_aux : forall (ML:list (map tm' tm')) M M1 M2 P R, app_subst ML M P -> {hcombine M1 M2 R M} -> exists M1' M2' R', nabla x y, app_subst ML M1 M1' /\ app_subst ML M2 M2' /\ app_subst ML (R x y) (R' x y) /\ {hcombine M1' M2' R' P}. Theorem subst'_hcombine_permute : forall (ML:list (map tm' tm')) M M1 M2 P R, nabla x y, {tm' x, tm' y |- tm' (R x y)} -> app_subst ML M P -> {hcombine M1 M2 R M} -> exists M1' M2', app_subst ML M1 M1' /\ app_subst ML M2 M2' /\ {hcombine M1' M2' R P}. Theorem subst'_hcombine3_permute_aux : forall (ML:list (map tm' tm')) M M1 M2 M3 P R, app_subst ML M P -> {hcombine3 M1 M2 M3 R M} -> exists M1' M2' M3' R', nabla x y z, app_subst ML M1 M1' /\ app_subst ML M2 M2' /\ app_subst ML M3 M3' /\ app_subst ML (R x y z) (R' x y z) /\ {hcombine3 M1' M2' M3' R' P}.
induction on 2. intros. case H2. apply app_subst'_hbase_comm to H1. apply app_subst'_meta_app_comm to H3 with R = x\R x M5 M4, M = M6. apply app_subst'_meta_app_comm to H4 with R = x\R n1 x M4, M = M5. apply app_subst_prune to H7. apply app_subst'_meta_app_comm to H6 with R = x\R n1 n2 x, M = M4. apply app_subst_prune to H9. apply app_subst_prune to H9. exists (hbase M'1). exists (hbase M''). exists (hbase M''2). exists (x\y\z\R'2 y x z). intros. split. backchain app_subst'_hbase_compose. backchain app_subst'_hbase_compose. backchain app_subst'_hbase_compose. search. search. apply app_subst'_habs_comm to H1. apply IH to H4 H3. apply app_subst_prune to H6. apply app_subst_prune to H7. apply app_subst_prune to H8. exists (habs M1'). exists M''. exists M''1. exists (x\y\z\M''2 z y x). intros. split. apply app_subst'_habs_compose to H5. search. search. search. search. search. apply app_subst'_habs_comm to H1. apply IH to H4 H3. apply app_subst_prune to H5. apply app_subst_prune to H7. apply app_subst_prune to H8. apply app_subst'_hbase_comm to H5. exists (hbase M'). exists (habs M2'). exists M''1. exists (x\y\z\M''2 z y x). intros. split. search. apply app_subst'_habs_compose to H6. search. search. search. search. apply app_subst'_habs_comm to H1. apply IH to H4 H3. apply app_subst_prune to H5. apply app_subst_prune to H6. apply app_subst_prune to H8. apply app_subst'_hbase_comm to H5. apply app_subst'_hbase_comm to H6. exists (hbase M'). exists (hbase M'1). exists (habs M3'). exists (x\y\z\M''2 z y x). intros. split. backchain app_subst'_hbase_compose. backchain app_subst'_hbase_compose. apply app_subst'_habs_compose to H7. search. search. search.
Theorem subst'_hcombine3_permute : forall (ML:list (map tm' tm')) M M1 M2 M3 R P, nabla x y z, {tm' x, tm' y, tm' z |- tm' (R x y z)} -> app_subst ML M P -> {hcombine3 M1 M2 M3 R M} -> exists M1' M2' M3', app_subst ML M1 M1' /\ app_subst ML M2 M2' /\ app_subst ML M3 M3' /\ {hcombine3 M1' M2' M3' R P}. Theorem subst'_hcombine_abs_let_permute : forall (ML:list (map tm' tm')) M M1 M2 P, app_subst ML M P -> {hcombine_abs M1 M2 (x\y\ let' x y) M} -> exists M1' M2', app_subst ML M1 M1' /\ (nabla x, app_subst ML (M2 x) (M2' x)) /\ {hcombine_abs M1' M2' (x\y\ let' x y) P}. Theorem tm'_list_to_tuple_permute1 : forall ML FE FE' E', is_list FE -> subst' ML -> app_subst_list ML FE FE' -> {tm'_list_to_tuple FE' E'} -> exists E, {tm'_list_to_tuple FE E} /\ app_subst ML E E'. Theorem tm'_list_to_tuple_permute2 : forall ML FE E' E, subst' ML -> {tm'_list_to_tuple FE E} -> app_subst ML E E' -> exists FE', app_subst_list ML FE FE' /\ {tm'_list_to_tuple FE' E'}. Theorem crev_permute : forall ML (L1:list tm') L2 L3 L3', subst' ML -> {rev L1 L2 L3} -> app_subst_list ML L3 L3' -> exists L1' L2', app_subst_list ML L1 L1' /\ app_subst_list ML L2 L2' /\ {rev L1' L2' L3'}. Theorem hoist_abs_permute : forall ML R1 R2 R2' FA (L:tm' -> tm') F F', nabla g x l, subst' ML -> {hoist_abs R1 g (L l) FA (R2 g) (F l)} -> app_subst ML (R2 g) (R2' g) -> app_subst ML (F l x) (F' l x) -> exists R1' FA' L', (nabla x, app_subst ML (R1 x) (R1' x)) /\ app_subst_list ML FA FA' /\ (nabla l, app_subst ML (L l) (L' l)) /\ (nabla l, {hoist_abs R1' g (L' l) FA' (R2' g) (F' l)}). Theorem abstract_permute : forall ML F F' R1 R2 R2', nabla l x, subst' ML -> app_subst ML (R2 x) (R2' x) -> app_subst ML (F l x) (F' l x) -> {abstract R1 R2 F} -> exists R1', (nabla x, app_subst ML (R1 x) (R1' x)) /\ {abstract R1' R2' F'}. Theorem hoist_abs_eval_fun : forall R R' FA (L:tm' -> tm') F FE E E' V V', nabla g l, {hoist_abs R g (L l) FA (R' g) (F l)} -> {tm'_list_to_tuple FE E} -> {eval' (L E') E} -> {eval'' (htm FE (R V)) V'} -> {eval' (F E' V) V'}. Theorem abstract_eval_fun : forall R R' F FE E V, {val' E} -> {abstract R R' F} -> {tm'_list_to_tuple FE E} -> forall V', {eval'' (htm FE (R V)) V'} -> {eval' (F E V) V'}. Theorem hoist_abs_eval_body : forall SL R R' FA L F FE FE' E, nabla x g, {val' E} -> tm'_ctx SL -> {SL, tm' x |- tm'' (htm FE (R x))} -> {hoist_abs R g L FA (R' g) F} -> {rev FA FE FE'} -> {tm'_list_to_tuple FE' E} -> forall V G, {eval' (app' G E) V} -> {eval'' (htm FE (R' G)) V}. Theorem abstract_eval_body : forall E FE R R' F G V, nabla x, {val' E} -> {tm' x |- tm'' (htm FE (R x))} -> {abstract R R' F} -> {tm'_list_to_tuple FE E} -> {eval' (app' G E) V} -> {eval'' (htm FE (R' G)) V}. Theorem subst'_cappend_permute : forall ML (FE:list tm') FE1 FE2 FE', subst' ML -> app_subst_list ML FE FE' -> {appd FE1 FE2 FE} -> exists FE1' FE2', app_subst_list ML FE1 FE1' /\ app_subst_list ML FE2 FE2' /\ {appd FE1' FE2' FE'}. Theorem tm'_list_to_tuple_typ_pres : forall L FE TE E, ctx' L -> {L |- of''_env FE TE} -> {tm'_list_to_tuple FE E} -> {L |- of' E TE}. Theorem tm'_list_append_val : forall L1 L2 L3, {tm'_list_val L1} -> {tm'_list_val L2} -> {appd L1 L2 L3} -> {tm'_list_val L3}. Theorem ch_env_val : forall L M FE M', ch_ctx L -> {L |- ch M (htm FE M')} -> {tm'_list_val FE}. Theorem app_subst'_list_val_pres : forall (ML:list (map tm' tm')) V V', {tm'_list_val V} -> app_subst_list ML V V' -> {tm'_list_val V'}. Theorem tm'_list_to_tuple_val_pres : forall FE E, {tm'_list_val FE} -> {tm'_list_to_tuple FE E} -> {val' E}. % Semantics preservation theorem for code hoisting Theorem ch_sem_pres : forall L K CL ML ML' M M' T FE FE' P P' Vs, {is_nat K} -> ctx' L -> ch_ctx CL -> vars_of_ctx' L Vs -> vars_of_ch_ctx CL Vs -> subst' ML -> subst' ML' -> subst_equiv_ch L K ML ML' -> {L |- of' M T} -> {CL |- ch M (htm FE M')} -> app_subst ML M P -> app_subst ML' (htm FE M') (htm FE' P') -> sim_ch T K P (htm FE' P').
induction on 10. intros. case H10. % Case: M = (nat' N) apply subst'_closed_tm_eq to _ H11. apply subst'_closed_tm''_eq to _ H12. apply of'_nat_inv to _ H9. backchain sim_ch_nat'. % Case: M = (pred' M1) apply app_subst'_pred_comm to H11. apply hconstr_str to _ H14. apply subst'_hconstr_permute to _ H12 H16. case H9. apply IH to _ _ _ _ _ _ _ _ H19 H13 H15 H17. backchain sim_ch_pred'. % Context case apply ctx'_focus_inv to _ _ H19. case H21. % Case: M = (plus' M1 M2) apply app_subst'_plus_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine_str to _ H16. apply cappend_str to _ H15. apply subst'_hcombine_permute to _ H20 H21. apply subst'_cappend_permute to _ H19 H22. apply app_subst'_htm_compose to H26 H23. apply app_subst'_htm_compose to H27 H24. case H9. apply IH to _ _ _ _ _ _ _ _ H31 H13 H17 H29. apply IH to _ _ _ _ _ _ _ _ H32 H14 H18 H30. backchain sim_ch_plus'. % Context case apply ctx'_focus_inv to _ _ H31. case H33. % Case: M = (ifz' M1 M2 M3) apply app_subst'_ifz_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine3_str to _ H18. apply cappend_str to _ H16. apply cappend_str to _ H17. apply subst'_hcombine3_permute to _ H23 H24. apply subst'_cappend_permute to _ H22 H26. apply subst'_cappend_permute to _ H31 H25. apply app_subst'_htm_compose to H34 H27. apply app_subst'_htm_compose to H35 H28. apply app_subst'_htm_compose to H32 H29. case H9. apply IH to _ _ _ _ _ _ _ _ H40 H13 H19 H37. apply IH to _ _ _ _ _ _ _ _ H41 H14 H20 H38. apply IH to _ _ _ _ _ _ _ _ H42 H15 H21 H39. apply ctx'_to_tm'_ctx to H2 H4. apply subst_equiv_ch_vars_of_subst' to H8 H4. apply ch_typ_pres to _ _ _ _ H42 H15. apply of''_to_tm'' to _ _ H46 H47 H50. apply subst'_result_closed_tm'' to _ H51 _ _ H49 H39. apply ch_typ_pres to _ _ _ _ H41 H14. apply of''_to_tm'' to _ _ H46 H47 H53. apply subst'_result_closed_tm'' to _ H54 _ _ H49 H38. backchain sim_ch_ifz' with FE2 = FE2'1, FE3 = FE2'. backchain of'_is_cty. % Context case apply ctx'_focus_inv to _ _ H40. case H42. % Case: M = unit apply subst'_closed_tm_eq to _ H11. apply subst'_closed_tm''_eq to _ H12. case H9. backchain sim_ch_unit'. % Context case apply ctx'_focus_inv to _ _ H13. case H15. % Case: M = pair apply app_subst'_pair_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine_str to _ H16. apply cappend_str to _ H15. apply subst'_hcombine_permute to _ H20 H21. apply subst'_cappend_permute to _ H19 H22. apply app_subst'_htm_compose to H26 H23. apply app_subst'_htm_compose to H27 H24. case H9. apply IH to _ _ _ _ _ _ _ _ H31 H13 H17 H29. apply IH to _ _ _ _ _ _ _ _ H32 H14 H18 H30. backchain sim_ch_pair'. backchain of'_is_cty. backchain of'_is_cty. % Context case apply ctx'_focus_inv to _ _ H31. case H33. % Case: M = (let' M1 R) apply app_subst'_let_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine_abs_str to _ H16. apply cappend_str to _ H15. apply subst'_hcombine_abs_let_permute to H20 H21. apply subst'_cappend_permute to _ H19 H22. apply app_subst'_htm_compose to H26 H23. case H9. % Get the simulation relation for let arguments apply IH to _ _ _ _ _ _ _ _ H30 H13 H17 H29. % Get the equivalence relation for argument values unfold. intros. apply nstep'_let_inv to _ H34. case H33. case H40. apply add_assoc to H36 H41. apply add_s to H43. apply sim_ch_nstep to H32 H37 _ H44. % Get the simulation relation for the body expressions % with binders substituted for argument values apply of'_is_cty to _ H30. assert {is_nat N23}. backchain add_arg2_isnat. apply equiv_ch_tm1 to _ _ H46. apply equiv_ch_tm2 to _ _ H46. assert app_subst (map n1 V1 :: ML) (R n1) (R1 V1). backchain explct_meta_subst'_comm with E = R1. assert app_subst (map n1 V' :: ML') (R' n1) (M2' V'). backchain explct_meta_subst'_comm with E = M2'. assert app_subst_list (map n1 V' :: ML') FE2 FE2'. apply app_subst'_htm_compose to H53 H52. apply IH to _ _ _ _ _ _ _ _ H31 H14 H51 H54 with K = (s N23). unfold. search. backchain subst_equiv_ch_closed. unfold. exists K1. backchain add_comm. backchain subst'_extend. backchain equiv_ch_val2 with V = V1, K = s N23. % Get the equivlance relation between evaluated body expressions apply sim_ch_nstep to H55 H39 _ _ with I = (s N). backchain add_s. % Finish the proof by evaluation lemmas and % closedness of equivalence relations under decreasing indexes exists V'1. exists N. split. apply eval''_let_fwd to H45 H56 H25 _ with M2 = M2'. search. search. assert {is_nat N}. backchain add_arg2_isnat. backchain equiv_ch_closed with K = s N. backchain of'_is_cty. unfold. exists (s z). backchain add_comm. % Context case apply ctx'_focus_inv to _ _ H30. case H32. % Case: M = (fst' M1) apply app_subst'_fst_comm to H11. apply hconstr_str to _ H14. apply subst'_hconstr_permute to _ H12 H16. case H9. apply IH to _ _ _ _ _ _ _ _ H19 H13 H15 H17. backchain sim_ch_fst'. backchain of'_is_cty. % Context case apply ctx'_focus_inv to _ _ H19. case H21. % Case: M = (snd' M1) apply app_subst'_snd_comm to H11. apply hconstr_str to _ H14. apply subst'_hconstr_permute to _ H12 H16. case H9. apply IH to _ _ _ _ _ _ _ _ H19 H13 H15 H17. backchain sim_ch_snd' with T1 = T1. backchain of'_is_cty. % Context case apply ctx'_focus_inv to _ _ H19. case H21. % Case: M = (app' M1 M2) apply app_subst'_app_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine_str to _ H16. apply cappend_str to _ H15. apply subst'_hcombine_permute to _ H20 H21. apply subst'_cappend_permute to _ H19 H22. apply app_subst'_htm_compose to H26 H23. apply app_subst'_htm_compose to H27 H24. case H9. apply IH to _ _ _ _ _ _ _ _ H31 H13 H17 H29. apply IH to _ _ _ _ _ _ _ _ H32 H14 H18 H30. backchain sim_ch_app' with T1 = T1. backchain of'_is_cty. % Context case apply ctx'_focus_inv to _ _ H31. case H33. % Case: M = (abs' R) apply app_subst'_abs_comm to H11. apply app_subst'_htm_comm to H12. apply app_subst_list_comm1 to H16. apply app_subst'_abs_comm to H18. apply app_subst'_abs_comm to H20. apply app_subst'_habs_comm to H17. % Permutation of substitution and 'abstract' apply abstract_str to _ H14. assert app_subst ML' (R'' n2) (R'4 n2). apply abstract_permute to _ H24 H21 H23. apply app_subst'_htm_compose to H19 H25. % Derive the fact that the body of the hoisted term is closed case H9(keep). apply is_cty_str to _ H29. apply ch_typ_pres to _ _ _ _ H28 H13. apply of''_to_alter_ver to _ H31. apply abstract_body_typ to _ _ H33 H23. apply of'_is_cty to _ H28. apply of''_env_is_cty to _ H32. assert {of''_body (prod (arr' TE (arr' T1 T2)) TE) (habs R'') (arr' T1 T2)}. apply of''_body_to_tm'' to _ _ _ _ H37. % Substitution has no effect on the body of the hoisted term apply app_subst'_habs_compose to H24. apply subst'_closed_tm''_body_eq to H38 H39. apply of''_env_tm'_list to _ H32. % Prove the equivalence relation between the original abstraction % and the hoisted abstraction assert exists FE1', {tm'_list_to_tuple L' FE1'}. apply app_subst_islist_trans to H40 H19. backchain tm'_list_to_tuple_exists. case H41. apply ctx'_to_tm'_ctx to H2 H4. apply subst_equiv_ch_vars_of_subst' to H8 H4. assert equiv_ch (arr' T1 T2) K (abs' R'1) (abs' (R'3 FE1')). assert equiv_ch_arr' (arr' T1 T2) K (abs' R'1) (abs' (R'3 FE1')). unfold. % Source abstraction is closed apply of'_to_tm' to _ _ _ _ H9. apply subst'_result_closed_tm to _ H47 H44 _ H45 H11. search. % Target abstraction is closed apply abstract_fun_typ to _ _ H33 H23. apply tm'_list_to_tuple_permute1 to _ _ H19 H42. apply of''_env_str to _ _ H32. apply tm'_list_to_tuple_typ_pres to _ H50 H48. inst H47 with n2 = E. cut H52 with H51. apply of'_to_tm' to _ _ _ _ H53 with Vs = (n1 :: Vs). assert app_subst ML' (F E n1) (R'3 FE1' n1). apply app_subst_inst to H49 H21. search. apply app_subst'_abs_compose to H55. assert {SL |- tm' (abs' (F E))}. apply subst'_result_closed_tm to _ H57 H44 _ H46 H56. search. % Proving the equivalence relation intros. assert {is_nat J}. case H47. backchain add_arg1_isnat. apply equiv_ch_tm1 to _ _ H48. apply equiv_ch_tm2 to _ _ H48. apply equiv_ch_val1 to _ _ H48. apply equiv_ch_val2 to _ _ H48. assert subst_equiv_ch (of' n1 T1 :: L) J (map n1 V :: ML) (map n1 V' :: ML'). backchain subst_equiv_ch_extend. backchain subst_equiv_ch_closed. backchain lt_to_le. assert app_subst (map n1 V :: ML) (R n1) (R'1 V). backchain explct_meta_subst'_comm with E = R'1. assert app_subst (map n1 V' :: ML') (htm FE1 (R' n1)) (htm L' (R1' V')). backchain explct_meta_subst'_comm with E = (x\ htm L' (R1' x)). apply IH to _ _ _ _ _ _ _ H54 H28 H13 H55 H56. backchain sim_ch_eval''_closed. apply ch_env_val to _ H13. apply app_subst'_list_val_pres to _ H19. apply tm'_list_to_tuple_val_pres to _ H42. apply abstract_eval_fun to _ H26 H42 with V = V'. intros. apply H61 to H62. search. % Finish proving the equivalence relation backchain equiv_ch_arr'_to_equiv_ch. % Prove the simulation relation from the equivalence relation unfold. intros. apply nstep'_val'_inv to _ H49. exists (abs' (R'3 FE1')). exists K. split. apply of''_to_tm'' to _ _ _ _ H31 with Vs = (n1 :: Vs). apply equiv_ch_tm1 to _ _ H47. assert {SL |- tm'' (htm (abs' R'1 :: FE1) (habs R'))}. apply app_subst'_habs_compose to H25. assert app_subst ML' (abs' R'1) (abs' R'1). backchain subst'_closed_tm. apply app_subst_list_compose to H55 H19. apply app_subst'_htm_compose to H56 H54. apply subst'_result_closed_tm'' to _ H53 H44 _ H46 H57. case H58. apply ch_env_val to _ H13. apply app_subst'_list_val_pres to _ H19. apply tm'_list_to_tuple_val_pres to _ H42. apply abstract_eval_body to _ H60 H26 H42 _ with G = (abs' (x\abs' (R'3 x))), V = (abs' (R'3 FE1')). search. search. search. % Context case apply ctx'_focus_inv to _ _ H28. case H30. % Case: M = (clos' M1 M2) apply app_subst'_clos_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine_str to _ H16. apply cappend_str to _ H15. apply subst'_hcombine_permute to _ H20 H21. apply subst'_cappend_permute to _ H19 H22. apply app_subst'_htm_compose to H26 H23. apply app_subst'_htm_compose to H27 H24. case H9. apply IH to _ _ _ _ _ _ _ _ H31 H13 H17 H29. apply IH to _ _ _ _ _ _ _ _ H32 H14 H18 H30. apply of'_is_cty to _ H31. case H35. case H36. case H39. backchain sim_ch_clos' with TL = TL. % Context case apply ctx'_focus_inv to _ _ H31. case H33. % Case: M = (open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) apply app_subst'_open_comm to H11. apply app_subst'_htm_comm to H12. apply hcombine_str to _ H16. apply cappend_str to _ H15. apply subst'_hcombine_permute to _ H20 H21. apply subst'_cappend_permute to _ H19 H22. apply app_subst'_htm_compose to H26 H23. apply app_subst'_htm_compose to H27 H24. case H9. apply IH to _ _ _ _ _ _ _ _ H31 H13 H17 H29. apply IH to _ _ _ _ _ _ _ _ H32 H14 H18 H30. apply of'_is_cty to _ H31. case H35. backchain sim_ch_open'. % Context case apply ctx'_focus_inv to _ _ H31. case H33. % Case: M = x apply ch_ctx_mem to H3 H14. case H13. apply ctx'_var_mem to _ H9 _. apply subst_equiv_ch_mem to H8 H16. apply subst'_var_eq to _ H17 H11. apply app_subst'_htm_comm to H12. apply app_subst_list_nil_comm to H20. apply app_subst'_hbase_comm to H21. apply subst'_var_eq to _ H18 H22. unfold. intros. apply of'_is_cty to _ H9. apply equiv_ch_val1 to _ _ H19. apply nstep'_val'_inv to _ H24. exists V'. exists K. split. apply equiv_ch_val2 to _ _ H19. apply eval'_refl to H28. search. search. search.
Theorem ch_nat_sem_pres : forall M FE M' N, {of' M tnat} -> {ch M (htm FE M')} -> {eval' M (nat' N)} -> {eval'' (htm FE M') (nat' N)}. Theorem cg_nat_sem_pres : forall M M' V, {of'' M tnat} -> {hcgen M M'} -> {eval'' M V} -> {eval'' M' V}.