Executable Specification

[View trans]

Reasoning

[View cg_sem_pres]

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

%%%%%%%%%%%%%%%%
% (WIP) Proof for semantics preservation of code generation transformation on STLC with recursion
%%%%%%%%%%%%%%%%

Specification "trans".

Import "eval". [View eval]
Import "subst". [View subst]

Define sim : ty -> nat -> tm' -> (tm' -> tm') -> state -> tm' -> prop,
       equiv : ty -> nat -> tm' -> state -> tm' -> prop by
  sim T I M K S M' := 
    forall J V, le J I -> {nstep' J M V} -> {val' V} ->
      exists N V' S' N', {nstep'' N' S M' S' (K V')} /\ 
                         {add J N I} /\ equiv T N V S' V';
  equiv tnat I (nat' N) S (nat' N);
  equiv tunit I unit' S unit';
  equiv (prod T1 T2) I (pair' V1 V2) (st N H) (loc' L) :=
    exists V1' V2', {lookup_heap H L (pair' V1' V2')} /\
      equiv T1 I V1 (st N H) V1' /\ equiv T2 I V2 (st N H) V2' /\
      {tm' V1} /\ {tm' V2} /\ {tm' V1'} /\ {tm' V2'};
  equiv (arr' T1 T2) z (abs' R) S (abs' R') :=
     {tm' (abs' R)} /\ {tm' (abs' R')};
  equiv (arr' T1 T2) (s K) (abs' R) S (abs' R') :=
     equiv (arr' T1 T2) K (abs' R) S (abs' R') /\
     forall V V', equiv T1 K V S V' -> sim T2 K (R V) (x\x) S (R' V');
  equiv (arr T1 T2) z (clos' (abs' R) VE) (st N H) (loc' L) :=
    exists R' VE', {lookup_heap H L (pair' (abs' R') VE')} /\
      {tm' (clos' (abs' R) VE)} /\ {tm' (pair' (abs' R') VE')} /\
      {val' VE} /\ {val' VE'};
  equiv (arr T1 T2) (s K) (clos' (abs' R) VE) (st N H) (loc' L) :=
    equiv (arr T1 T2) K (clos' (abs' R) VE) (st N H) (loc' L) /\
    exists R' VE', {lookup_heap H L (pair' (abs' R') VE')} /\
      forall V1 V1' V2 V2', 
        equiv T1 K V1 (st N H) V1' -> equiv (arr T1 T2) K V2 (st N H) V2' ->
          sim T2 K (R (pair' V2 (pair' V1 VE))) (x\x) (st N H)
                   (R' (pair' V2' (pair' V1' VE'))).


Define cg_ctx : olist -> prop by
  cg_ctx nil;
  nabla x, cg_ctx ((pi k\ cgen x k (k x)) :: L) := cg_ctx L.

Define vars_of_cg_ctx : olist -> list tm' -> prop by
  vars_of_cg_ctx nil nil;
  nabla x, vars_of_cg_ctx ((pi k\ cgen x k (k x)):: L) (x :: L') :=
    vars_of_cg_ctx L L'.

% Semantics preservation
% Theorem cg_sem_pres : forall ML ML' L CL Vs M T K K' M' P P' I S,
%   {is_nat I} -> ctx' L -> cg_ctx CL -> 
%   vars_of_ctx' L Vs -> vars_of_cg_ctx CL Vs ->
%   subst' ML -> subst' ML' -> subst_equiv L I ML S ML' ->
%   {L |- of' M T} -> {CL |- cgen M K M'} -> 
%   app_subst ML M P -> app_subst ML' M' P' ->    
%   (nabla x, app_subst ML' (K x) (K' x)) ->
%     sim T I P K' S P'.
% skip.

% Theorem nat_sem_pres : forall P P' V,
%   {of'' P tnat} -> {hcgen P P'} -> {eval'' P V} -> 
%     exists St,{eval''' P' St V}.
% intros. case H2. case H1.

% Define fun_equiv : olist -> nat -> list (map tm' tm') -> state -> list (map tm' tm') -> prop by
%   subst_equiv nil I nil S nil;
%   nabla x, subst_equiv (of' x T :: L) I (map x V :: ML) S (map x V' :: ML') :=
%     equiv T I V S V' /\ subst_equiv L I ML S ML'.


Define step* : tm -> tm -> prop by
  step* M M' := exists N, {nstep N M M'}.

% Evaluation lemmas
Theorem step*_trans : forall M1 M2 M3,
  step* M1 M2 -> step* M2 M3 -> step* M1 M3.

Theorem step*_inst : forall M1 M2 M, nabla (x:tm),
  step* (M1 x) (M2 x) -> step* (M1 M) (M2 M).

% Simulation and equivalence relations
Define sim_cps : ty -> nat -> tm -> (tm -> tm) -> tm -> prop,
       equiv_cps : ty -> nat -> tm -> tm -> prop by
  sim_cps T I M K M' := 
    forall J V, le J I -> {nstep J M V} -> {val V} ->
      exists N V', step* M' (K V') /\ {add J N I} /\ equiv_cps T N V V';
  equiv_cps tnat I (nat N) (nat N);
  equiv_cps tunit I unit unit;
  equiv_cps (prod T1 T2) I (pair V1 V2) (pair V1' V2') :=
    equiv_cps T1 I V1 V1' /\ equiv_cps T2 I V2 V2' /\
    {tm V1} /\ {tm V2} /\ {tm V1'} /\ {tm V2'};
  equiv_cps (arr T1 T2) z (fix f\x\ R f x) (fix f\p\ R' f p) :=
        {tm (fix R)} /\ {tm (fix R')};
  equiv_cps (arr T1 T2) (s I) (fix f\x\ R f x) (fix f\p\ R' f p) :=
    equiv_cps (arr T1 T2) I (fix f\x\ R f x) (fix f\p\ R' f p) /\
    forall V1 V1' V2 V2' K, 
      equiv_cps T1 I V1 V1' -> equiv_cps (arr T1 T2) I V2 V2' -> 
        sim_cps T2 I (R V2 V1) K (R' V2' (pair (fix f\K) V1')).
   
Theorem equiv_cps_val1 : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cps T K V V' -> {val V}.

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

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

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

Theorem equiv_cps_arr_val2 : forall T1 T K R V,
  {is_nat K} -> equiv_cps (arr T1 T) K (fix R) V -> 
    exists R', V = (fix R').


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

Define equiv_cps_arr : ty -> nat -> tm -> tm -> prop by
  equiv_cps_arr (arr T1 T2) I (fix f\x\ R f x) (fix f\p\ R' f p) :=
    {tm (fix R)} /\ {tm (fix R')} /\
    forall J V1 V1' V2 V2' K, lt J I ->
      equiv_cps T1 J V1 V1' -> equiv_cps (arr T1 T2) J V2 V2' -> 
        sim_cps T2 J (R V2 V1) K (R' V2' (pair (fix f\K) V1')).

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

Theorem equiv_cps_arr_to_equiv_cps : forall T K M M',
  {is_nat K} -> {is_sty T} -> equiv_cps_arr T K M M' -> equiv_cps T K M M'.
 
Theorem equiv_cps_arr_cond : forall I T1 T2 R R' K,
  {is_nat I} -> equiv_cps (arr T1 T2) I (fix R) (fix R') ->
  (forall J V1 V1' V2 V2', lt J I ->
      equiv_cps T1 J V1 V1' -> equiv_cps (arr T1 T2) J V2 V2' ->
        sim_cps T2 J (R V2 V1) K (R' V2' (pair (fix f\K) V1'))).

Theorem app_equiv_cps_arr : forall T1 T R R' N1 N2 V1 V1' I K,
  {is_sty (arr T1 T)} -> {is_nat N1} -> {is_nat N2} -> 
    equiv_cps (arr T1 T) N1 (fix R) (fix R') -> 
    equiv_cps T1 N2 V1 V1' -> lt I N1 -> lt I N2 ->
      sim_cps T I (R (fix R) V1) K (R' (fix R') (pair (fix f\K) V1')).


% Simulatoin lemmas
Theorem sim_cps_nstep : forall T K M M' J I V N,
  sim_cps T I M K M' -> {nstep J M V} -> {val V} -> {add J N I} -> 
    exists V', step* M' (K V') /\ equiv_cps T N V V'.

Theorem sim_cps_closed_step* : forall T I K M M' M1',
  step* M1' M' -> sim_cps T I K M M' -> sim_cps T I K M M1'.

% Equivalence between substitutions
Define subst_equiv_cps : olist -> nat -> list (map tm tm) -> list (map tm tm) -> prop by
  subst_equiv_cps nil I nil nil;
  nabla x, subst_equiv_cps (of x T :: L) I (map x V :: ML) (map x V' :: ML') :=
    equiv_cps T I V V' /\ subst_equiv_cps L I ML ML'.

Theorem subst_equiv_cps_vars : forall L Vs ML ML' I,
  vars_of_sctx L Vs -> subst_equiv_cps L I ML ML' -> vars_of_subst ML Vs.

Theorem subst_equiv_cps_vars' : forall L Vs ML ML' I,
  vars_of_sctx L Vs -> subst_equiv_cps L I ML ML' -> vars_of_subst ML' Vs.

Theorem subst_equiv_cps_mem : forall L ML ML' M T I,
  subst_equiv_cps L I ML ML' -> member (of M T) L -> exists V V',
     member (map M V) ML /\ member (map M V') ML' /\ equiv_cps T I V V'.

Theorem subst_equiv_cps_closed : forall L K J ML ML',
  {is_nat K} -> sctx L -> subst_equiv_cps L K ML ML' -> le J K -> subst_equiv_cps L J ML ML'.

Import "cps_typ_pres". [View cps_typ_pres]

% Simulation theorems
Theorem sim_cps_pred : forall I M M' K, 
  sim_cps tnat I M (x\let (pred x) (v\K v)) M' ->
    sim_cps tnat I (pred M) K M'.

Theorem sim_cps_ifz : forall I T K' M1 M2 M3 M2' M3' M',
  {is_nat I} -> {is_sty T} -> 
  sim_cps T I M2 (x\app (fix f\K') x) (M2' (fix f\K')) ->
  sim_cps T I M3 (x\app (fix f\K') x) (M3' (fix f\K')) ->
  sim_cps tnat I M1 (x1\let (fix f\K') (k\ifz x1 (M2' k) (M3' k))) M' ->
  sim_cps T I (ifz M1 M2 M3) K' M'.

Theorem sim_cps_plus : forall I M1 M2 M2' M' K, nabla x1,
  {is_nat I} -> sim_cps tnat I M1 M2' M' -> 
  sim_cps tnat I M2 (x2\let (plus x1 x2) (v\K v)) (M2' x1)-> 
    sim_cps tnat I (plus M1 M2) K M'.

Theorem sim_cps_unit : forall I K,
   sim_cps tunit I unit K (K unit).

Theorem sim_cps_pair : forall I T1 T2 M1 M2 M2' M' K, nabla x1,
  {is_nat I} -> {is_sty T1} -> {is_sty T2} ->
    sim_cps T1 I M1 M2' M' -> sim_cps T2 I M2 (x2\let (pair x1 x2) (v\K v)) (M2' x1)-> 
    sim_cps (prod T1 T2) I (pair M1 M2) K M'.
  
Theorem sim_cps_fst : forall T1 T2 K I M M',
  {is_nat I} -> {is_sty (prod T1 T2)} -> 
  sim_cps (prod T1 T2) I M (x\let (fst x) (v\K v)) M' ->
    sim_cps T1 I (fst M) K M'.

Theorem sim_cps_snd : forall T1 T2 K I M M',
  {is_nat I} -> {is_sty (prod T1 T2)} -> 
  sim_cps (prod T1 T2) I M (x\let (snd x) (v\K v)) M' ->
    sim_cps T2 I (snd M) K M'.

Theorem sim_cps_app : forall T1 T I K' M1 M' M2 M2', nabla x1,
  {is_nat I} -> {is_sty (arr T1 T)} -> sim_cps (arr T1 T) I M1 M2' M' -> 
    sim_cps T1 I M2 (x2\let (fix (f\K')) (k\let (pair k x2) (p\app x1 p))) (M2' x1) ->
    sim_cps T I (app M1 M2) K' M'.
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. assert exists N1, {add J1 N1 N3}. backchain k_minus_n1. case H17. assert exists N2, {add J2 N2 N3}. backchain k_minus_n2. case H19. % Get equivalent arguments assert exists V1', step* M' (M2' V1') /\ equiv_cps (arr T1 T) (s N1) (fix R) V1'. backchain sim_cps_nstep. backchain add_s. case H21. assert exists V2', step* (M2' n1) (let (fix (f\K')) (k\let (pair k V2') (p\app n1 p))) /\ equiv_cps T1 (s N2) V2 V2'. backchain sim_cps_nstep. backchain add_s. case H24. % Get a number of steps for evaluating of the reduced beta-redex 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'1 (s N1). backchain sum_complement_to_lt1 with N1 = J1, N2 = J2, N = N3. case H1. search. assert lt K'1 (s N2). backchain sum_complement_to_lt2 with N1 = J1, N2 = J2, N = N3. case H1. search. case H1. case H2. apply add_arg2_isnat to _ H18. apply add_arg2_isnat to _ H20. apply equiv_cps_arr_val2 to _ H23. apply equiv_cps_tm2 to _ _ H26. apply sclosed_tm_prune to H38. assert sim_cps T K'1 (R (fix R) V2) K' (R' (fix R') (pair (fix f\K') M'1)). backchain app_equiv_cps_arr with T1 = T1, N1 = s N1, N2 = s N2, R = R, R' = R', K = K'. % Apply the simulation relation to get the equivalence relation between values. assert exists V', step* (R' (fix R') (pair (fix (f\K')) M'1)) (K' V') /\ equiv_cps T N V V'. backchain sim_cps_nstep. case H40. % Finish this case exists N. exists V'. split. apply equiv_cps_val2 to _ _ H26. apply step*_inst to H25 with M = (fix R'). backchain step*_trans with M2 = (R' (fix R') (pair (fix (f\K')) M'1)). backchain step*_trans with M2 = (let (fix (f\K')) (k\let (pair k M'1) (p\app (fix R') p))). backchain step*_trans with M2 = M2' (fix R'). search 7. search. search.
% Semantics preservation Theorem cps_sem_pres : forall ML ML' TL CL VL M T K K' M' P P' I, {is_nat I} -> {is_sty T} -> sctx TL -> cctx CL -> vars_of_sctx TL VL -> vars_of_cctx CL VL -> subst ML -> subst ML' -> subst_equiv_cps TL I ML ML' -> {TL |- of M T} -> {CL |- cps M K M'} -> app_subst ML M P -> app_subst ML' M' P' -> (nabla x, app_subst ML' (K x) (K' x)) -> sim_cps T I P K' P'.
induction on 11. intros. case H11. % Case: M = nat N apply sof_nat_inv to _ H10. apply subst_closed_tm_eq to _ H12. case H14. apply subst_inst to _ H15 with V = (nat N). apply app_subst_det to H13 H16. unfold. intros. apply nstep_val_inv to _ H18. search. % Case: M = pred M1 assert exists M2, P = pred M2 /\ app_subst ML M1 M2. backchain app_subst_pred_comm. case H16. case H14. case H10. assert sim_cps tnat I M2 (x\let (pred x) (v\K' v)) P'. backchain IH with M = M1, M' = M', K = (x\let (pred x) (v\K v)), ML = ML, ML' = ML'. intros. backchain app_subst_let_compose with x = n2. backchain app_subst_pred_compose. backchain subst_nabla. backchain sim_cps_pred. % Context case apply sctx_focus_inv to _ _ H19. case H21. % Case: M = plus M1 M2 assert exists M3 M4, P = plus M3 M4 /\ app_subst ML M1 M3 /\ app_subst ML M2 M4. backchain app_subst_plus_comm. case H17. assert exists M4', app_subst ML' (M2' n1) M4'. backchain app_subst_exists. case H20. case H10. case H14. % Applying the inductive hypothesis assert sim_cps tnat I M4 (x2\let (plus n1 x2) (v\K' v)) (M4' n1). backchain IH with M = M2, M' = (M2' n1), K = (x2\let (plus n1 x2) (v\K v)), ML = ML, ML' = ML'. intros. backchain app_subst_let_compose with x = n3. backchain app_subst_plus_compose. backchain subst_nabla. backchain subst_nabla. assert sim_cps tnat I M3 M4' P'. backchain IH with M = M1, M' = M', K = M2', ML = ML, ML' = ML'. % Complete this case backchain sim_cps_plus with x1 = n1. % Context case apply sctx_focus_inv to _ _ H22. case H24. % Case: M = ifz M1 M2 M3 assert exists M4 M5 M6, P = ifz M4 M5 M6 /\ app_subst ML M1 M4 /\ app_subst ML M2 M5 /\ app_subst ML M3 M6. backchain app_subst_ifz_comm. case H18. case H10. case H14. assert exists M5', app_subst ML' (M2' n1) (M5'). backchain app_subst_exists. case H26. assert exists M6', app_subst ML' (M3' n1) M6'. backchain app_subst_exists. case H28. assert app_subst ML' (fix f\K) (fix f\K'). backchain app_subst_fix_compose. apply app_subst_inst to H30 H27. apply app_subst_inst to H30 H29. % Apply I.H. assert sim_cps tnat I M4 (x1\let (fix f\K') (k\ifz x1 (M5' k) (M6' k))) P'. backchain IH with M = M1, M' = M', K = (x1\let (fix f\K) (k\ifz x1 (M2' k) (M3' k))), ML = ML, ML' = ML'. intros. backchain app_subst_let_compose. backchain app_subst_ifz_compose. backchain subst_nabla. assert sim_cps T I M5 (x\app (fix f\K') x) (M5' (fix f\K')). inst H15 with n1 = (fix f\K). backchain IH with M = M2, M' = (M2' (fix f\K)), K = (x\app (fix f\K) x), ML = ML, ML' = ML'. intros. backchain app_subst_app_compose. backchain subst_nabla. assert sim_cps T I M6 (x\app (fix f\K') x) (M6' (fix f\K')). inst H16 with n1 = (fix f\K). backchain IH with M = M3, M' = (M3' (fix f\K)), K = (x\app (fix f\K) x), ML = ML, ML' = ML'. intros. backchain app_subst_app_compose. backchain subst_nabla. % Finish this case backchain sim_cps_ifz with M1 = M4, M2 = M5, M3 = M6, M2' = M5', M3' = M6', M' = P'. % Context case apply sctx_focus_inv to _ _ H22. case H24. % Case: M = unit apply subst_closed_tm_eq to _ H12. apply app_subst_meta_app_comm to H13 with R = K. apply subst_closed_tm_eq to _ H15. case H14. apply app_subst_det to H16 H17. apply sof_unit_inv to _ H10. backchain sim_cps_unit. % Case: M = pair M1 M2 assert exists M3 M4, P = pair M3 M4 /\ app_subst ML M1 M3 /\ app_subst ML M2 M4. backchain app_subst_pair_comm. case H17. assert exists M4', app_subst ML' (M2' n1) M4'. backchain app_subst_exists. case H20. apply sof_pair_inv to _ H10. case H2. case H10. case H14. % Applying the inductive hypothesis assert sim_cps T2 I M4 (x2\let (pair n1 x2) (v\K' v)) (M4' n1). backchain IH with M = M2, M' = (M2' n1), K = (x2\let (pair n1 x2) (v\K v)), ML = ML, ML' = ML'. intros. backchain app_subst_let_compose with x = n3. backchain app_subst_pair_compose. backchain subst_nabla. backchain subst_nabla. assert sim_cps T1 I M3 M4' P'. backchain IH with M = M1, M' = M', K = M2', ML = ML, ML' = ML'. % Complete this case backchain sim_cps_pair with x1 = n1. % Context case apply sctx_focus_inv to _ _ H24. case H26. % Case: M = fst M1 apply app_subst_fst_comm to H12. case H10. case H14. assert sim_cps (prod T T2) I M1' (x\let (fst x) (v\K' v)) P'. backchain IH with M = M1, M' = M', K = (x\let (fst x) (v\K v)), ML = ML, ML' = ML'. backchain sof_is_sty. intros. backchain app_subst_let_compose with x = n2. backchain app_subst_fst_compose. backchain subst_nabla. backchain sim_cps_fst with T1 = T, T2 = T2. backchain sof_is_sty. % Context case apply sctx_focus_inv to _ _ H17. case H19. % Case: M = snd M1 apply app_subst_snd_comm to H12. case H10. case H14. assert sim_cps (prod T1 T) I M1' (x\let (snd x) (v\K' v)) P'. backchain IH with M = M1, M' = M', K = (x\let (snd x) (v\K v)), ML = ML, ML' = ML'. backchain sof_is_sty. intros. backchain app_subst_let_compose with x = n2. backchain app_subst_snd_compose. backchain subst_nabla. backchain sim_cps_snd with T1 = T1, T2 = T. backchain sof_is_sty. % Context case apply sctx_focus_inv to _ _ H17. case H19. % Case: M = let M1 R 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 H17. case H10. assert exists R1', app_subst ML' (R' n1) R1'. backchain app_subst_exists. case H22. apply sof_is_sty to _ H20. % Get the simulation relation for let arguments assert sim_cps T1 I M2 R1' P'. backchain IH with M = M1, M' = M', K = R', ML = ML, ML' = ML'. % Get the equivalence relation for argument values unfold. intros. apply nstep_let_inv to _ H27. case H26. case H33. apply add_assoc to H29 H34. apply sim_cps_nstep to H25 H30 H31 _ with N = (s N23). backchain add_s. case H1. case H14. assert {is_nat N23}. backchain add_arg2_isnat. apply equiv_cps_tm1 to _ _ H38. apply equiv_cps_val1 to _ _ H38. apply equiv_cps_tm2 to _ _ H38. apply equiv_cps_val2 to _ _ H38. % Get the simulation relation for the body expressions % with binders substituted for argument values assert sim_cps T N23 (R1 V1) K' (R1' V'). backchain IH with M = R n1, M' = R' n1, K = K, ML = map n1 V1 :: ML, ML' = map n1 V' :: ML', TL = of n1 T1 :: TL, CL = (pi k\cps n1 k (k n1)) :: CL, VL = n1 :: VL. unfold. backchain equiv_cps_closed with K = s N23. backchain le_succ. backchain le_refl. backchain subst_equiv_cps_closed with K = s N3. apply add_comm to _ H36. backchain le_succ. backchain explct_meta_subst_comm with n = n1, M = R, E = R1. backchain explct_meta_subst_comm with n = n1, M = R', E = R1'. % Get the equivlance relation between evaluated body expressions assert exists V'', step* (R1' V') (K' V'') /\ equiv_cps T N V V''. backchain sim_cps_nstep. case H47. apply step*_trans to H37 H48. search. % Context case apply sctx_focus_inv to _ _ H20. case H22. % Case: M = (fix R) % Communtativity of substitutions for fixed-points assert exists R1, P = fix R1 /\ nabla f x, app_subst ML (R f x) (R1 f x). backchain app_subst_fix_comm. case H16. case H14. assert exists R1', nabla f k x, app_subst ML' (R' f k x) (R1' f k x). apply app_subst_exists to H8 with M = (R' n1 n2 n3). search. case H19. assert P' = (let (fix (f\p\let (fst p) (k\let (snd p) (x\R1' f k x)))) K'). apply app_subst_let_comm to H13. apply app_subst_det to H18 H22. apply app_subst_fix_comm to H21. apply app_subst_let_comm to H23. apply app_subst_fst_comm to H24. apply subst_nabla to H8 with x = n2. apply app_subst_det to H26 H27. apply app_subst_let_comm to H25. apply app_subst_snd_comm to H28. apply app_subst_det to H26 H30. assert app_subst ML' (R' n1 n2 n3) (R4 n2 n1 n4 n3). apply app_subst_det to H20 H31. search. case H21. % Inversion of typing case H10. case H2. % Get the equivalence relation between the fixed-point and its CPS form unfold. intros. apply nstep_val_inv to _ H27. exists I. exists (fix (f\p\let (fst p) (k\let (snd p) (x\R1' f k x)))). split. search. search. % Prove the equivalence relation assert equiv_cps_arr (arr T1 T2) I (fix R1) (fix (f\p\let (fst p) (k\let (snd p) (x\R1' f k x)))). unfold. % Prove the source fixed-point is closed under substitution apply sctx_to_tm_sctx to _ H5. assert {SL, tm n1, tm n2 |- tm (R n1 n2)}. backchain sof_to_tm with L = of n2 T1 :: of n1 (arr T1 T2) :: TL, Vs = n2::n1::VL, T = T2. backchain subst_result_closed_tm with L = SL, M = fix R, Vs = VL, ML = ML. backchain subst_equiv_cps_vars. % Prove the target fixed-point is closed under substitution apply cps_sctx_exists to H3 with S = T2. assert exists T1', cps_ty T2 T1 T1'. backchain cps_ty_exists. case H30. assert exists T2', cps_ty T2 T2 T2'. backchain cps_ty_exists. case H32. assert {TL', of n2 (arr (prod (arr T2' T2) T1') T2), of n3 T1', pi x\ of x T2' => of (app n1 x) T2 |- of (R' n2 n1 n3) T2}. backchain cps_typ_pres with TL = of n3 T1 :: of n2 (arr T1 T2) :: TL, CL = (pi k\cps n3 k (k n3)) :: (pi k\cps n2 k (k n2)) :: CL, M = R n2 n3, M' = R' n2 n1 n3, K = y\app n1 y, T = T2, S = T2. assert {of n1 (arr T2' T2) |- pi x\of x T2' => of (app n1 x) T2}. cut H34 with H35. apply cps_ty_pres to _ _ H31. apply cps_ty_pres to _ _ H33. assert {TL' |- of (fix (f\p\let (fst p) (k\let (snd p) (x\R' f k x)))) (arr (prod (arr T2' T2) T1') T2)}. assert app_subst ML' (fix (f\p\let (fst p) (k\let (snd p) (x\R' f k x)))) (fix (f\p\let (fst p) (k\let (snd p) (x\R1' f k x)))). backchain app_subst_fix_compose with f = n1, x = n2. backchain app_subst_let_compose with x = n3. backchain app_subst_fst_compose. backchain subst_nabla. backchain app_subst_let_compose with x = n4. backchain app_subst_snd_compose. backchain subst_nabla. backchain subst_result_closed_tm' with L = TL', M = (fix (f\p\let (fst p) (k\let (snd p) (x\R' f k x)))), T = (arr (prod (arr T2' T2) T1') T2), Vs = VL, ML = ML'. backchain cps_sctx_pres with S = T2. backchain cps_sctx_vars_sync. backchain subst_equiv_cps_vars'. % Prove simulation intros. case H29. apply add_arg1_isnat to H32. apply equiv_cps_tm1 to _ _ H30. apply equiv_cps_tm2 to _ _H30. apply equiv_cps_val1 to _ _ H30. apply equiv_cps_val2 to _ _H30. apply equiv_cps_tm1 to _ _ H31. apply equiv_cps_tm2 to _ _H31. apply equiv_cps_val1 to _ _ H31. apply equiv_cps_val2 to _ _H31. assert sim_cps T2 J1 (R1 V2 V1) (y\app n1 y) (R1' V2' n1 V1'). backchain IH with M = R n2 n3, M' = R' n2 n1 n3, K = (y\app n1 y), ML = map n3 V1 :: map n2 V2 :: ML, ML' = map n3 V1' :: map n2 V2' :: ML', TL = of n3 T1 :: of n2 (arr T1 T2) :: TL, CL = (pi k\cps n3 k (k n3)) ::(pi k\cps n2 k (k n2)) :: CL, VL = n3 :: n2 :: VL. unfold. search. unfold. search. backchain subst_equiv_cps_closed with K = I. backchain explct_meta_subst_comm with n = n3, M = R n2, E = R1 V2. backchain explct_meta_subst_comm with n = n2, M = x\R x n3, E = x\ R1 x n3. backchain explct_meta_subst_comm with n = n3, M = R' n2 n1, E = R1' V2' n1. backchain explct_meta_subst_comm with n = n2, M = x\R' x n1 n3, E = x\ R1' x n1 n3. intros. unfold. unfold. backchain app_subst_app_compose. backchain subst_nabla. backchain subst_nabla. unfold. intros. case H43. apply add_arg2_isnat to _ H46. apply sim_cps_nstep to H42 H44 H45 H46. apply equiv_cps_val2 to _ _ H49. apply equiv_cps_tm2 to _ _ H49. apply sclosed_tm_prune to H51. apply step*_inst to H48 with M = (fix f\K1). exists N1. exists M'1. split. backchain step*_trans with M2 = (app (fix (f\K1)) M'1). backchain step*_trans with M2 = (R1' V2' (fix (f\K1)) V1'). search 8. search. search. backchain equiv_cps_arr_to_equiv_cps. % Context case apply sctx_focus_inv to _ _ H22. case H24. % Case: M = @ M1 M2 % Communtativity of substitutions for applications assert exists M3 M4, P = app M3 M4 /\ app_subst ML M1 M3 /\ app_subst ML M2 M4. backchain app_subst_app_comm. case H17. case H14. assert exists M4', app_subst ML' (M2' n1) M4'. backchain app_subst_exists. case H21. case H10. apply sof_is_sty to _ H24. % Apply I.H. assert sim_cps T1 I M4 (x2\let (fix (f\K')) (k\let (pair k x2) (p\app n1 p))) (M4' n1). backchain IH with M = M2, M' = (M2' n1), K = (x2\let (fix (f\K)) (k\let (pair k x2) (p\app n1 p))), ML = ML, ML' = ML'. intros. backchain app_subst_let_compose with x = n3. backchain app_subst_fix_compose with f = n1, x = n2. backchain app_subst_let_compose with x = n4. backchain app_subst_pair_compose. backchain subst_nabla. backchain subst_nabla. backchain app_subst_app_compose. backchain subst_nabla. backchain subst_nabla. assert sim_cps (arr T1 T) I M3 M4' P'. backchain IH with M = M1, M' = M', K = M2', ML = ML, ML' = ML'. % Finish this case backchain sim_cps_app with T1 = T1, M2' = M4', x1 = n1. % Context case apply sctx_focus_inv to _ _ H23. case H25. % Case: M = x apply cctx_mem to H4 H16. case H15. apply sctx_var_mem to _ H10 _. apply subst_equiv_cps_mem to H9 H18. apply subst_var_eq to _ H19 H12. assert exists K1' M1', P' = K1' M1' /\ app_subst ML' M M1' /\ nabla x, app_subst ML' (K x) (K1' x). backchain app_subst_meta_app_comm. case H22. apply subst_var_eq to _ H20 H23. case H14. apply app_subst_det to H24 H25. unfold. intros. case H26. apply nstep_val_inv to _ H27. backchain equiv_cps_val1. search.
Theorem cps_sem_pres_base : forall M K M' V, {of M tnat} -> {cps M K M'} -> {eval M V} -> step* M' (K V). Theorem cps_nat_sem_pres : forall M M' V, {of M tnat} -> {cps' M M'} -> {eval M V} -> {eval M' V}. % Semantics preservation % Theorem cg_sem_pres : forall ML ML' L CL Vs M T K K' M' P P' I S, % {is_nat I} -> ctx' L -> cg_ctx CL -> % vars_of_ctx' L Vs -> vars_of_cg_ctx CL Vs -> % subst' ML -> subst' ML' -> subst_equiv L I ML S ML' -> % {L |- of' M T} -> {CL |- cgen M K M'} -> % app_subst ML M P -> app_subst ML' M' P' -> % (nabla x, app_subst ML' (K x) (K' x)) -> % sim T I P K' S P'. % skip. % Theorem nat_sem_pres : forall P P' V, % {of'' P tnat} -> {hcgen P P'} -> {eval'' P V} -> % exists St,{eval''' P' St V}. % intros. case H2. case H1. % Define fun_equiv : olist -> nat -> list (map tm' tm') -> state -> list (map tm' tm') -> prop by % subst_equiv nil I nil S nil; % nabla x, subst_equiv (of' x T :: L) I (map x V :: ML) S (map x V' :: ML') := % equiv T I V S V' /\ subst_equiv L I ML S ML'. Theorem cg_nat_sem_pres : forall M M' V, {of'' M tnat} -> {hcgen M M'} -> {eval'' M V} -> {eval'' M' V}.