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}.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'). % 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. 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'.induction on 3. intros. case H3. search. unfold. backchain equiv_cps_closed. case H2. search. backchain IH. case H2. search.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'.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). 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}. % 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}.