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

%%%%%%%%%%%%%%%%
% Proof for semantics preservation of CPS transformation on STLC with recursion
%%%%%%%%%%%%%%%%

Specification "trans".

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

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.
intros. case H1. case H2. apply nstep_trans to H3 H4. search.
Theorem step*_inst : forall M1 M2 M, nabla (x:tm),
  step* (M1 x) (M2 x) -> step* (M1 M) (M2 M).
intros. case H1. inst H2 with n1 = M. search.
% 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}.
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_cps_val2 : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cps 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_cps_tm1 : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cps 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_cps_tm2 : forall T K V V',
  {is_sty T} -> {is_nat K} -> equiv_cps 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_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').
induction on 1. intros. case H1.
  case H2. search. 
  case H2. backchain IH.

% 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'.
induction on 1. induction on 2. intros. case H1(keep). 
  case H3. search.
  case H3. search.
  case H3. unfold. backchain IH. backchain IH. search. search. search. search.
  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.
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'.
intros. case H3. unfold. search. search. intros.
  apply lt_le_compose to H7 H2.
  apply H6 to _ H8 H9 with K1 = K1. search.
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'.
induction on 1. intros. case H3 (keep). case H1.
  search.
  unfold. 
    apply equiv_cps_arr_closed to _ _ H3 with J = N. backchain le_succ. backchain le_refl. 
      apply IH to H7 _ H8. search.
    intros. backchain H6. unfold. exists z. backchain add_comm.
 
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'))).
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 with K = K. backchain H12.
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')).
intros. case H1. apply equiv_cps_arr_cond to _ H4 with K = K. backchain H10.
  backchain equiv_cps_closed with K = N2. backchain lt_to_le.
  backchain equiv_cps_closed with K = N1. backchain lt_to_le.

% 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'.
intros. case H1. apply H5 to _ H2 H3. exists V'. split.
  search. 
  apply add_arg2_det to H4 H7. search.
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'.
intros. unfold. intros. case H3.
  apply sim_cps_nstep to H2 H4 _ _. 
  apply step*_trans to H1 H7. search.
% 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.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H5 H4. search.
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.
 
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H5 H4. search.
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'.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H5 H3. search.
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'.
induction on 3. intros. case H3.
  search.
  unfold. 
    backchain equiv_cps_closed. case H2. search.
    backchain IH. case H2. search.

% 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'.
intros. unfold. intros.
  apply nstep_pred_inv to H4 H3. 
  case H2. case H7.
  assert {add J1 (s N1) (s N3)}. backchain add_s.
  apply sim_cps_nstep to H1 H5 _ H9.
  case H11. exists N1. exists (nat N'). split.
    backchain step*_trans with M2 = (let (pred (nat N)) (v\K v)).
    search.
    search.
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'.
intros. unfold. intros. apply nstep_ifz_inv to _ _ H7. case H6. backchain add_arg1_isnat. case H11.
  % M1 evals to 0
  apply le_trans to H9 H6. case H14. apply sim_cps_nstep to H5 H12 _ H15.
    apply le_trans to H10 H6. case H18. apply sim_cps_nstep to H3 H13 _ H19.
    case H17. case H6. exists N3. exists V'1. 
    assert {is_nat N2}.
      backchain add_arg2_isnat.
    split.
      backchain step*_trans with M2 = (app (fix f\K') V'1).
        backchain step*_trans with M2 = (M2' (fix f\K')).
        backchain step*_trans with M2 = (let (fix f\K') (k\ifz (nat z) (M2' k) (M3' k))).
        apply equiv_cps_val2 to _ _ H21. search.
      search.
      backchain equiv_cps_closed with K = N2. 
        backchain add_le_complement with N = I, N1 = I1, N1' = J.
  % M evals to (s N)
  apply le_trans to H9 H6. case H14. apply sim_cps_nstep to H5 H12 _ H15.
    apply le_trans to H10 H6. case H18. apply sim_cps_nstep to H4 H13 _ H19.
    case H17. case H6. exists N3. exists V'1. 
    assert {is_nat N2}.
      backchain add_arg2_isnat.
    split.
      backchain step*_trans with M2 = (app (fix f\K') V'1).
      backchain step*_trans with M2 = (M3' (fix f\K')).
        backchain step*_trans with M2 = (let (fix f\K') (k\ifz (nat (s N)) (M2' k) (M3' k))).
        apply equiv_cps_val2 to _ _ H21. search.
      search.
      backchain equiv_cps_closed with K = N2.
        backchain add_le_complement with N = I, N1 = I1, N1' = J.
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'.
intros. unfold. intros.
  apply nstep_plus_inv to _ H5. case H4. case H11. case H1.
  apply add_assoc to H7 H12.
  assert exists V1', step* M' (M2' V1') /\ 
    equiv_cps tnat (s N23) (nat N1) V1'.
    backchain sim_cps_nstep. backchain add_s.
  case H16.
  apply add_comm to _ H7. backchain add_arg1_isnat.
  apply add_assoc to H19 H12.
  assert exists V2', step* (M2' n1) (let (plus n1 V2') K) /\ 
    equiv_cps tnat (s N5) (nat N2) V2'. 
    backchain sim_cps_nstep. backchain add_s.
  case H22.
  apply add_arg2_isnat to _ H15. apply add_arg2_isnat to _ H21. 
  apply equiv_cps_tm2 to _ _ H24. apply sclosed_tm_prune to H27.
  exists N. exists (nat N3). split.
    apply step*_inst to H23 with M = V1'.
      apply step*_trans to H17 H28.
      apply equiv_cps_val2 to _ _ H18. apply equiv_cps_val2 to _ _ H24.
      case H24. case H18.
      assert step* (let (plus V1' M'1) (v\K v)) (K (nat N3)).
      apply step*_trans to H29 H32. search.
    search.
    search.
Theorem sim_cps_unit : forall I K,
   sim_cps tunit I unit K (K unit).
intros. unfold. intros.
  apply nstep_val_inv to _ H2. search.
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'.
intros. unfold. intros.
  apply nstep_pair_inv to _ H7. case H8. case H6 (keep).
  apply le_trans to _ H6. case H15. 
  assert exists V1', step* M' (M2' V1') /\ equiv_cps T1 N1 V1 V1'. 
    backchain sim_cps_nstep.
  case H17.
  apply add_comm to _ H9. backchain add_arg1_isnat.
  apply le_trans to _ H6 with N1 = J1. case H21. 
  assert exists V2', step* (M2' n1) (let (pair n1 V2') K) /\ equiv_cps T2 N2 V2 V2'. 
    backchain sim_cps_nstep.
  case H23.
  apply add_arg2_isnat to _ H16. apply add_arg2_isnat to _ H22. 
  apply equiv_cps_tm2 to _ _ H25. apply sclosed_tm_prune to H28.
  exists N. exists (pair V1' M'1). split.
    apply step*_inst to H24 with M = V1'.
      apply step*_trans to H18 H29.
      apply equiv_cps_val2 to _ _ H19. apply equiv_cps_val2 to _ _ H25.
      assert step* (let (pair V1' M'1) (v\K v)) (K (pair V1' M'1)).
      apply step*_trans to H30 H33. search.
    search.
    unfold.
      backchain equiv_cps_closed with K = N1. 
        backchain add_le_complement with N = I, N1 = I1, N1' = J.
      backchain equiv_cps_closed with K = N2.
        backchain add_le_complement with N = I, N1 = J1, N1' = J.
      backchain equiv_cps_tm1 with T = T1, K = N1.
      backchain equiv_cps_tm1 with T = T2, K = N2. 
      backchain equiv_cps_tm2 with T = T1, K = N1. 
      backchain equiv_cps_tm2 with T = T2, K = N2.
 
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'.
intros. unfold. intros.
  apply nstep_fst_inv to H6 H5.
  case H4. case H9. apply add_s to H10. 
  apply sim_cps_nstep to H3 H8 _ H11. case H13.
  case H1. case H2. apply add_arg2_isnat to _ H10.
  exists N. exists V1'. split.
    apply equiv_cps_val2 to _ _ H14. apply equiv_cps_val2 to _ _ H15.
      backchain step*_trans with 
        M2 = (let (fst (pair V1' V2')) (v\K v)).
    search.
    backchain equiv_cps_closed with K = s N.
      backchain le_succ. backchain le_refl.
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'.
intros. unfold. intros.
  apply nstep_snd_inv to H6 H5.
  case H4. case H9. apply add_s to H10. 
  apply sim_cps_nstep to H3 H8 _ H11. case H13.
  case H1. case H2. apply add_arg2_isnat to _ H10.
  exists N. exists V2'. split.
    apply equiv_cps_val2 to _ _ H14. apply equiv_cps_val2 to _ _ H15.
      backchain step*_trans with 
        M2 = (let (snd (pair V1' V2')) (v\K v)).
    search.
    backchain equiv_cps_closed with K = s N.
      backchain le_succ. backchain le_refl.
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).
intros.
  case H3. apply nstep_is_nat to H4.
  assert sim_cps tnat N M K M'.
    backchain cps_sem_pres.
  assert exists V', step* M' (K V') /\ equiv_cps tnat z V V'. 
    backchain sim_cps_nstep. backchain add_comm.
  case H8. case H10. search.
Theorem cps_nat_sem_pres : forall M M' V,
  {of M tnat} -> {cps' M M'} -> {eval M V} -> {eval M' V}.
intros. case H2. apply cps_sem_pres_base to H1 H4 H3. 
  case H5. case H3. search.