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}.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. case H3. search. search.Theorem equiv_ch_val2 : forall T K V V', {is_cty T} -> {is_nat K} -> equiv_ch 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. case H3. search. search.Theorem equiv_ch_tm1 : forall T K V V', {is_cty T} -> {is_nat K} -> equiv_ch 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. case H2. case H3. search. case H3. apply IH1 to H1 H6 H7. search.Theorem equiv_ch_tm2 : forall T K V V', {is_cty T} -> {is_nat K} -> equiv_ch 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. case H2. case H3. search. case H3. apply IH1 to H1 H6 H7. search.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'.induction on 1. induction on 2. intros. case H1(keep). case H3. search. case H3. search. case H3. unfold. backchain IH. backchain IH. 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. 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_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'.intros. case H3. unfold. search. search. intros. apply lt_le_compose to H7 H2. apply H6 to H9 H8. search.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'.induction on 1. intros. case H3 (keep). case H1. search. unfold. apply equiv_ch_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_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'.induction on 1. intros. case H1. case H2. unfold. search. search. intros. case H5. case H7. case H2. apply IH to H3 H4. case H6. unfold. search. search. intros. case H10. apply add_s_inv to H12. assert le J N. apply le_to_lt to _ H14. case H15. backchain H5. backchain H9.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')))).induction on 1. intros. case H1. apply lt_z_absurd to H3. apply lt_pred_le to _ H3. apply le_to_lt to _ H6. case H7. case H2. backchain H9. case H2. apply IH to H5 H9. backchain H11.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'))).intros. case H1. apply equiv_ch_arr'_cond to _ H4. backchain H10. backchain equiv_ch_closed with K = N2. backchain lt_to_le.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'.intros. case H3. unfold. search. search. search. search. intros. apply lt_le_compose to H9 H2. apply H8 to H12 H10 H11. search.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'.induction on 1. intros. case H2 (keep). case H1. search. unfold. apply equiv_ch_arr_closed to _ _ H2 with J = N. backchain le_succ. backchain le_refl. apply IH to H8 H9. search. intros. backchain H7. unfold. exists z. backchain add_comm.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'.induction on 1. intros. case H1. case H2. unfold. search. search. search. search. intros. case H7. case H10. case H2. apply IH to H3 H4. case H6. unfold. search. search. search. search. intros. case H12. apply add_s_inv to H15. assert le J N. apply le_to_lt to _ H17. case H18. backchain H5. backchain H11.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'))))).intros. case H1. apply equiv_ch_to_equiv_ch_arr to _ H4. case H10. backchain H15. backchain equiv_ch_closed with K = N2. backchain lt_to_le. backchain equiv_ch_closed with K = N1. backchain lt_to_le.%% 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'.intros. case H1. apply H5 to _ H2 H3. exists V'. split. search. assert I = N. backchain add_arg2_det. case H9. search.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'').intros. case H1. unfold. intros. apply nstep'_pred_inv to H6 H5. case H4. case H9. assert {add J1 (s N1) (s N3)}. backchain add_s. apply H3 to _ H7 _ with J = J1. case H14. exists (nat' N'). exists N1. split. backchain eval''_pred_fwd. search. search.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).intros. unfold. intros. apply nstep'_plus_inv to H8 H7. assert le J1 K. apply add_s to H9. apply le_trans to _ H6. search. case H2. apply H14 to H13 H10 _. case H17. assert le J2 K. apply add_comm to _ H9. case H6. apply add_arg1_isnat to H18. case H19. search. apply add_s to H18. apply le_trans to _ H6. search. case H3. apply H19 to H18 H11 _. case H22. apply eval''_plus_fwd to _ H20 H12 H4 H5. case H6. search.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).intros. unfold. intros. apply nstep'_ifz_inv to _ _ H12. case H11. backchain add_arg1_isnat. case H16. % M evals to 0 apply le_trans to H14 H11. case H5. apply H20 to _ H17 _. apply le_trans to H15 H11. case H6. apply H25 to _ H18 _. case H23. case H11. exists V'1. exists N3. split. backchain eval''_ifz_fwd1 with FE3 = FE3. search. backchain equiv_ch_closed with K = N2. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = I, N1' = J. backchain add_arg2_isnat. % M evals to (s N) apply le_trans to H14 H11. case H5. apply H20 to _ H17 _. apply le_trans to H15 H11. case H7. apply H25 to _ H18 _. case H23. case H11. exists V'1. exists N3. split. backchain eval''_ifz_fwd2 with FE2 = FE2. search. backchain equiv_ch_closed with K = N2. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = I, N1' = J. backchain add_arg2_isnat.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).intros. unfold. intros. apply nstep'_pair_inv to _ H9. case H10. case H8 (keep). apply le_trans to _ H8. case H4. apply H18 to _ H12 _. apply add_arg1_isnat to H16. apply add_comm to _ H11. apply le_trans to _ H8 with N1 = J1. case H5. apply H25 to _ H13 _. exists (pair' V' V'1). exists N. split. backchain eval''_pair_fwd. search. unfold. backchain equiv_ch_closed with K = N1. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = I, N1' = J. backchain add_arg2_isnat. backchain equiv_ch_closed with K = N2. backchain add_arg2_isnat. backchain add_le_complement with N = K, N1 = J1, N1' = J. backchain add_arg2_isnat.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'').intros. unfold. intros. apply nstep'_fst_inv to _ H6. case H3. apply H10 to _ H9 _. case H5. case H11. apply add_s to H12. search. case H5. case H13. case H2. apply add_arg2_isnat to _ H12. exists V1'. exists N1. split. backchain eval''_fst_fwd. search. backchain equiv_ch_closed with K = N. apply add_le_complement to _ _ H12 H14. backchain le_succ. backchain le_refl. backchain add_arg1_isnat. search.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'').intros. unfold. intros. apply nstep'_snd_inv to _ H6. case H3. apply H10 to _ H9 _. case H5. case H11. apply add_s to H12. search. case H5. case H13. case H2. apply add_arg2_isnat to _ H12. exists V2'. exists N1. split. backchain eval''_snd_fwd. search. backchain equiv_ch_closed with K = N. apply add_le_complement to _ _ H12 H14. backchain le_succ. backchain le_refl. backchain add_arg1_isnat. search.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).intros. unfold. intros. apply nstep'_clos_inv to _ H9. case H10. case H8 (keep). apply add_assoc to H11 H16. apply sim_ch_nstep to H4 H12 _ H18. apply add_arg2_isnat to _ H16. apply add_result_isnat to _ H17. apply add_comm to _ H18. apply add_assoc to H17 H23. apply sim_ch_nstep to H5 H13 _ H25. % N = K - K1 - K2 exists (clos' V' V'1). exists N. split. backchain eval''_clos_fwd. search. assert equiv_ch_arr (arr T1 T2) N (clos' V1 V2) (clos' V' V'1). apply equiv_ch_to_equiv_ch_arr' to _ H20. case H28. apply add_arg2_isnat to _ H25. apply equiv_ch_val1 to _ _ H27. apply equiv_ch_val2 to _ _ H27. apply equiv_ch_tm1 to _ _ H27. apply equiv_ch_tm2 to _ _ H27. unfold. search. search. search. search. intros. assert le J1 N1. apply lt_to_le to H37. apply le_trans to H40 _ with N3 = N1. search. apply equiv_ch_closed to _ _ H27 H40. assert lt J1 N23. apply add_comm to _ H17. apply lt_le_compose to H37 _ with N3 = N23. search. backchain H31 with V = (pair' V4 (pair' V3 V2)), V' = (pair' V2' (pair' V1' V'1)). % Finish proving the equivalence relation backchain equiv_ch_arr_to_equiv_ch.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'.induction on 3. intros. case H3. search. unfold. backchain equiv_ch_closed. case H2. search. backchain IH. case H2. search.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.induction on 1. intros. case H1. case H2. search. case H2. apply vars_of_ctx'_prune2 to H5. apply IH to H4 H5. search.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'}.induction on 2. intros. case H2. apply app_subst'_hbase_comm to H1. apply app_subst'_meta_app_comm to H3 with R = R, M = M1. exists (hbase M'2). exists R'. intros. split. 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. exists (habs P). exists M''. intros. split. apply app_subst'_habs_compose to H5. search. search. search.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'}.intros. apply app_subst'_htm_comm to H2. apply subst'_hconstr_permute_aux to H5 H3. apply app_subst'_abs_compose to H7. apply subst'_closed_tm_eq to _ H9. apply app_subst'_htm_compose to H4 H6. search.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}.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 M3, M = M4. apply app_subst'_meta_app_comm to H4 with R = x\R n1 x, M = M3. apply app_subst_prune to H7. exists (hbase M'1). exists (hbase M''). exists R'1. intros. split. 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. exists (habs M1'). exists M''. exists (x\y\M''1 y x). intros. split. apply app_subst'_habs_compose to H5. 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'_hbase_comm to H5. exists (hbase M'). exists (habs M2'). exists (x\y\M''1 y x). intros. split. search. apply app_subst'_habs_compose to H6. search. search. search.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}.intros. apply subst'_hcombine_permute_aux to H2 H3. apply app_subst'_abs_compose to H6. apply app_subst'_abs_compose to H8. apply subst'_closed_tm_eq to _ H9. search.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}.intros. apply subst'_hcombine3_permute_aux to H2 H3. apply app_subst'_abs_compose to H7. apply app_subst'_abs_compose to H9. apply app_subst'_abs_compose to H10. apply subst'_closed_tm_eq to _ H11. search.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}.induction on 2. intros. case H2. apply app_subst'_hbase_comm to H1. apply app_subst'_let_comm to H3. exists (hbase M5). exists (x\hbase (R1 x)). split. backchain app_subst'_hbase_compose. intros. backchain app_subst'_hbase_compose. search. apply app_subst'_habs_comm to H1. apply IH to H4 H3. apply app_subst_prune to H6. exists (habs M1'). exists M''. split. apply app_subst'_habs_compose to H5. search. search. search. apply app_subst'_habs_comm to H1. apply IH to H4 H3. apply app_subst_prune to H5. apply app_subst'_hbase_comm to H5. exists (hbase M'). exists (x\ habs (y\ M2' y x)). split. search. intros. apply app_subst'_habs_compose to H6. search. search.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'.induction on 4. intros. case H4. apply app_subst'_list_nil2 to _ H3. exists unit'. split. search. backchain subst'_closed_tm. apply app_subst_list_comm2 to H1 H3. case H1. apply IH to _ _ H7 H5. exists (pair' X' E). split. search. backchain app_subst'_pair_compose.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'}.induction on 2. intros. case H2. apply app_subst'_unit_comm to H3. exists nil. split. backchain app_subst'_list_nil1. search. apply app_subst'_pair_comm to H3. apply IH to _ H4 H6. exists (M1' :: FE'). split. backchain app_subst_list_compose. search.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'}.induction on 2. intros. case H2. exists nil. exists L3'. split. backchain app_subst'_list_nil1. search. search. apply IH to _ H4 H3. apply app_subst_list_comm1 to H6. exists (X' :: L1'). exists L'. split. backchain app_subst_list_compose. search. search.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)}).induction on 2. intros. case H2(keep). apply app_subst_prune to H4. apply rev_prune to H5. apply rev_prune to H5. apply tm'_list_to_tuple_prune to H6. apply app_subst'_hbase_comm to H3. apply app_subst'_app_comm to H7. apply subst'_nabla to H1 with x = n1. apply app_subst_det to H8 H10. apply tm'_list_to_tuple_permute2 to _ H6 H9. apply app_subst_list_prune to H11. apply tm'_list_to_tuple_prune to H12. apply crev_permute to _ H5 H11. apply app_subst_list_nil_comm to H14. apply app_subst'_exists to H1 with M = L n3. exists (x\ hbase (M'' x)). exists L1'. exists M'1. split. intros. backchain app_subst'_hbase_compose. search. search. search. apply app_subst'_habs_comm to H3. apply app_subst'_let_comm to H4. apply app_subst'_fst_comm to H7. apply app_subst_prune to H9. assert app_subst ML (F2 n3 n4 n2) (R5 n4 n3 n2). apply IH to _ H5 H6 H10. apply app_subst_prune to H11. apply app_subst_list_prune to H12. apply app_subst_list_prune to H12. apply app_subst_list_comm1 to H12. apply subst'_nabla to H1 with x = n2. apply app_subst_det to H15 H17. apply app_subst_prune to H11. apply app_subst_list_prune to H16. apply app_subst'_snd_comm to H13. apply app_subst_prune to H18. apply app_subst_prune to H18. exists (x\habs (y\ M''4 y x)). exists M''5. exists M''7. split. intros. apply app_subst'_habs_compose to H11 with x = n2. search. search. search. apply app_subst_det to H9 H18. search.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'}.intros. case H4. assert app_subst ML (R2 n1) (R2' n1). assert app_subst ML (F n2 n3) (F' n2 n3). apply hoist_abs_permute to _ H5 H6 H7. apply app_subst_list_prune to H9. apply app_subst_prune to H10. apply app_subst_prune to H8. apply app_subst_list_nil_comm to H9. apply subst'_nabla to H1 with x = n2. apply app_subst_det to H10 H12. search.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'}.induction on 1. intros. case H1. case H4. search. case H4. case H2. inst H5 with n3 = F1. apply eval'_fst_pair to H3. apply eval'_snd_pair to H3. apply IH to H8 H7 _ H6 with L = x\snd' (L x), E' = E'. apply eval'_let_fwd to H9 H11 with R = F2 E' V. search.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}.induction on 4. intros. case H4(keep). case H3. apply rev_det to H5 H8. apply tm'_list_to_tuple_det to H6 H9. search. apply tm'_ctx_mem to _ H11. case H10. case H3. assert {rev (FE1 :: FA) FE2 FE'}. inst H8 with n1 = FE1. inst H10 with n2 = FE1. cut H13 with H9. apply IH to _ _ H14 H12 H11 _. apply H15 to H7. search. apply tm'_ctx_mem to _ H10. case H9.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'}.induction on 3. intros. case H3. apply app_subst'_list_nil1 to H1. search. apply app_subst_list_comm1 to H2. apply IH to _ H6 H4. exists (X' :: FE1'). exists FE2'. split. backchain app_subst_list_compose. search. search.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}.induction on 2. intros. case H2. case H3. search. case H3. apply IH to _ H5 H6. search. apply ctx'_focus_inv to _ _ H4.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}.induction on 2. intros. case H2. search. apply IH to _ H3. search. apply IH to _ H3. apply IH to _ H4. apply cappend_str to _ H5. apply tm'_list_append_val to H7 H8 H9. search. apply IH to _ H3. apply IH to _ H4. apply IH to _ H5. apply cappend_str to _ H6. apply cappend_str to _ H7. apply tm'_list_append_val to H9 H10 H12. apply tm'_list_append_val to H14 H11 H13. search. search. apply IH to _ H3. apply IH to _ H4. apply cappend_str to _ H5. apply tm'_list_append_val to H7 H8 H9. search. apply IH to _ H3. apply IH to _ H4. apply cappend_str to _ H5. apply tm'_list_append_val to H7 H8 H9. search. apply IH to _ H3. search. apply IH to _ H3. search. apply IH to _ H3. apply IH to _ H4. apply cappend_str to _ H5. apply tm'_list_append_val to H7 H8 H9. search. apply IH to _ H3. search. apply IH to _ H3. apply IH to _ H4. apply cappend_str to _ H5. apply tm'_list_append_val to H7 H8 H9. search. apply IH to _ H3. apply IH to _ H4. apply cappend_str to _ H5. apply tm'_list_append_val to H7 H8 H9. search. apply ch_ctx_mem to _ H4. case H3. search.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)}.intros. case H3. apply nstep'_is_nat to H4. assert sim_ch tnat N1 M (htm FE M'). backchain ch_sem_pres with L = nil, ML = nil, ML' = nil, Vs = nil, M = M, M' = M', FE = FE. apply sim_ch_nstep to H7 H4 _ _ with I = z. backchain add_comm. case H9. search.Theorem cg_nat_sem_pres : forall M M' V, {of'' M tnat} -> {hcgen M M'} -> {eval'' M V} -> {eval'' M' V}.