From 125580b237faf4fe86f258e3d24d5a4ea1de75f4 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sat, 7 Mar 2020 00:59:38 +0100 Subject: [PATCH] Cleanups --- theories/Dot/syn/dropSkips.v | 139 +++++++++++++---------------------- 1 file changed, 52 insertions(+), 87 deletions(-) diff --git a/theories/Dot/syn/dropSkips.v b/theories/Dot/syn/dropSkips.v index 516d10c7c..244551f9b 100644 --- a/theories/Dot/syn/dropSkips.v +++ b/theories/Dot/syn/dropSkips.v @@ -194,9 +194,12 @@ Proof. induction Ki; rewrite /= ?fill_app /=; eauto with f_equal. Qed. *) +Definition simpl_prim_step := (λ e1 e2, prim_step e1 () [] e2 () []). +Notation prim_steps := (rtc simpl_prim_step). + Theorem simulation_skiperase e1 e2 : - prim_step e1 () [] e2 () [] → - rtc (λ e1 e2, prim_step e1 () [] e2 () []) (erase_tm e1) (erase_tm e2). + simpl_prim_step e1 e2 → + prim_steps (erase_tm e1) (erase_tm e2). Proof. inversion 1 as [Ks ???? Hh%head_erase_sim]; simplify_eq/=. rewrite !erase_ctxi_fill. induction Hh; [apply rtc_refl|eapply rtc_l, IHHh]. @@ -209,39 +212,11 @@ From D Require Import iris_extra.det_reduction. Lemma simulation_skiperase' e1 σ1 κ e2 σ2 efs : prim_step e1 σ1 κ e2 σ2 efs → - rtc (λ e1 e2, prim_step e1 () [] e2 () []) (erase_tm e1) (erase_tm e2). + prim_steps (erase_tm e1) (erase_tm e2). Proof. intros Hs; prim_step_inversion Hs. destruct σ1; exact: simulation_skiperase. Qed. - -Theorem simulation_skiperase_erased_step {t1 t2 σ σ'} : - erased_step ([t1], σ) ([t2], σ') → - rtc erased_step ([erase_tm t1], σ) ([erase_tm t2], σ'). -Proof. - rewrite erased_step_prim => /simulation_skiperase' Hstep; destruct σ, σ'. - eapply (rtc_congruence (λ t, ([t], ()))), Hstep => /= e1 e2 Hs. - apply erased_step_prim, Hs. -Qed. - -Theorem simulation_skiperase_erased_steps {t1 t2 σ σ'} : - rtc erased_step ([t1], σ) ([t2], σ') → - rtc erased_step ([erase_tm t1], σ) ([erase_tm t2], σ'). -Proof. - move => Hsteps. - dependent induction Hsteps; first done. - destruct y as [l σ'']; have ?: σ'' = σ by destruct σ, σ''; subst. - move: H (H) => [k Hstep] Hestep. - have [ti ?] := step_inversion Hstep; destruct_and!; simplify_eq. - etrans; first exact: (simulation_skiperase_erased_step Hestep). - exact: IHHsteps. -Qed. - -Corollary simulation_skiperase_erased_steps_vl {t1 v2 σ σ'} : - rtc erased_step ([t1], σ) ([tv v2], σ') → - rtc erased_step ([erase_tm t1], σ) ([tv (erase_vl v2)], σ'). -Proof. exact: (simulation_skiperase_erased_steps (t2 := tv v2)). Qed. - Lemma erased_step_inversion {t1 thp σ σ'} : erased_step ([t1], σ) (thp, σ') → ∃ t2, thp = [t2] ∧ prim_step t1 σ [] t2 σ' []. @@ -264,9 +239,6 @@ Proof. by rewrite elem_of_list_singleton=>->. Qed. -Definition simpl_prim_step := (λ e1 e2, prim_step e1 () [] e2 () []). -Notation prim_steps := (rtc simpl_prim_step). - Lemma erased_prim_steps e1 e2: rtc erased_step ([e1], ()) ([e2], ()) ↔ prim_steps e1 e2. @@ -279,6 +251,29 @@ Proof. exists []; eauto. Qed. +Theorem simulation_skip_erase_prim_steps t1 t2 : + prim_steps t1 t2 → + prim_steps (erase_tm t1) (erase_tm t2). +Proof. + intros Hsteps; dependent induction Hsteps; first done. + etrans; last done. + exact: simulation_skiperase'. +Qed. + +Theorem simulation_skiperase_erased_steps {t1 t2 σ σ'} : + rtc erased_step ([t1], σ) ([t2], σ') → + rtc erased_step ([erase_tm t1], σ) ([erase_tm t2], σ'). +Proof. + uniqueState; rewrite !erased_prim_steps. + exact: simulation_skip_erase_prim_steps. +Qed. + +Corollary simulation_skiperase_erased_steps_vl {t1 v2 σ σ'} : + rtc erased_step ([t1], σ) ([tv v2], σ') → + rtc erased_step ([erase_tm t1], σ) ([tv (erase_vl v2)], σ'). +Proof. exact: (simulation_skiperase_erased_steps (t2 := tv v2)). Qed. + + Lemma fill_prim_steps Ks {eK1 eK2} : prim_steps eK1 eK2 → prim_steps (fill Ks eK1) (fill Ks eK2). @@ -587,15 +582,15 @@ Qed. *) Lemma safe_skiperase {e}: safe e → safe (erase_tm e). Proof. - rewrite /safe => Hsafe ee' thp [] [] Hereds Hin. - have {}Hereds := rtc_erased_step_inversion Hereds Hin. - have /erased_prim_steps Hereds' := Hereds. - destruct (prims_erase_sim_inv e _ Hereds') as [e' [Hreds%erased_prim_steps He]]. - destruct (Hsafe e' [e'] () ()) as [Hv|Hr]; - [done|by rewrite elem_of_list_singleton|left|]; simplify_eq/=. + rewrite /safe => Hsafe ee' /pure_steps_erased'. + destruct dummyState => /erased_prim_steps Hereds'. + destruct (prims_erase_sim_inv e _ Hereds') as [e' [Hreds %erased_prim_steps He]]. + + destruct (Hsafe e') as [Hv|Hr]; + [by apply pure_steps_erased'; destruct dummyState | left|]; simplify_eq/=. - destruct e'; try by [case (is_Some_None Hv)]; eauto. - destruct Hr. - (* pose proof (Hsafe e' thp () ()). *) + (* pose proof (Hsafe e'). *) (* destruct e; simplify_eq/=. pose proof (simulation_skiperase_erased_steps Hred Hin) as Hst. *) Abort. @@ -603,7 +598,7 @@ Abort. Lemma safe_skiperase_inv {e}: safe (erase_tm e) → safe e. Proof. - rewrite /safe => Hsafe e' > Hred Hin. + (* rewrite /safe => Hsafe e' > Hred Hin. pose proof (simulation_skiperase_erased_steps Hred Hin) as Hst. edestruct Hsafe as [Hs|Hs]; [apply Hst|apply elem_of_list_here| |right]. - destruct e'; try by [case (is_Some_None Hs)]; first naive_solver. @@ -615,7 +610,7 @@ Proof. apply _. naive_solver. - - eapply same_skel_reducible, Hs; exact: same_skel_symm_tm. *) + - eapply same_skel_reducible, Hs; exact: same_skel_symm_tm. *) *) Abort. From D.Dot Require Import skeleton_termination. @@ -631,12 +626,12 @@ Proof. exact: IHHr. Qed. -Theorem rtc_erased_step_inversion'' {t1 σ σ' thp} : +(* Theorem rtc_erased_step_inversion'' {t1 σ σ' thp} : rtc erased_step ([t1], σ) (thp, σ') → ∃ t2, thp = [t2]. Proof. move=> Hs; have [t2' ?] := rtc_erased_step_inversion' Hs; subst; eauto. -Qed. +Qed. *) Lemma rtc_erased_steps_det {e v thp}: rtc erased_step ([e], ()) ([tv v], ()) → @@ -644,35 +639,21 @@ Lemma rtc_erased_steps_det {e v thp}: rtc erased_step (thp, ()) ([tv v], ()). Proof. rewrite erased_prim_steps => H1 H2. - destruct (rtc_erased_step_inversion'' H2) as [e']; simplify_eq. + destruct (rtc_erased_step_inversion' H2) as [e']; simplify_eq. move: H2; rewrite !erased_prim_steps => H2. exact: prim_steps_det. Qed. -(* Lemma safe_skiperase1 {e1 v2 σ σ'}: - erased_step ([e1], σ) ([tv v2], σ') → - safe (erase_tm e1). -Proof. - destruct σ, σ'. - rewrite /safe => /simulation_skiperase_erased_step' /= Hsafe e' thp [] [] Hred Hin. - destruct (rtc_erased_step_inversion' Hred) as [e'' ?]; simplify_eq. - move: Hin; rewrite elem_of_list_singleton => ?; subst e''. - pose proof (rtc_erased_steps_det Hsafe Hred) as Hremaining. - destruct (rtc_inv _ _ Hremaining) as [|Hrem]; simplify_eq/=. - - left; eauto. - - right; destruct Hrem as [[thp []] [Hrred%erased_step_inversion _]]. - hnf; naive_solver. -Qed. *) - Lemma safe_erase_to_val {e1 v2}: prim_steps e1 (tv v2) → safe (erase_tm e1). Proof. - rewrite /safe => /erased_prim_steps /simulation_skiperase_erased_steps_vl' - /= Hsafe e' thp [] [] Hred Hin. - destruct (rtc_erased_step_inversion' Hred) as [e'' ?]; simplify_eq. - move: Hin; rewrite elem_of_list_singleton => ?; subst e''. + rewrite /safe => /erased_prim_steps /simulation_skiperase_erased_steps_vl + /= Hsafe e' /pure_steps_erased' Hred. + destruct dummyState. + (* destruct (rtc_erased_step_inversion' Hred) as [e'' ?]; simplify_eq. + move: Hin; rewrite elem_of_list_singleton => ?; subst e''. *) pose proof (rtc_erased_steps_det Hsafe Hred) as Hremaining. destruct (rtc_inv _ _ Hremaining) as [|Hrem]; simplify_eq/=. - left; eauto. @@ -684,12 +665,13 @@ Lemma safe_erase_diverging {e1}: diverges' e1 → safe (erase_tm e1). Proof. - rewrite /safe /diverges' => /= Hdiv ee2 thp [] [] Hred Hin. - destruct (rtc_erased_step_inversion'' Hred) as [e'' ?]; simplify_eq. - have /erased_prim_steps Hereds := (rtc_erased_step_inversion Hred Hin). - move => {Hin Hred}. + rewrite /safe /diverges' => /= Hdiv ee2 /pure_steps_erased'. + case: dummyState => /erased_prim_steps Hereds'. + (* destruct (rtc_erased_step_inversion'' Hred) as [e'' ?]; simplify_eq. + have /erased_prim_steps Hereds := (rtc_erased_step_inversion Hred Hin). *) + (* move => {Hin Hred}. *) (* %erased_prim_steps *) - destruct (prims_erase_sim_inv _ _ Hereds) as [e2 [Hreds He]]; subst. + destruct (prims_erase_sim_inv _ _ Hereds') as [e2 [Hreds He]]; subst. have Hrede2 := Hdiv _ Hreds. (* What now? *) Admitted. @@ -727,23 +709,6 @@ Proof. exact: safe_erase_diverging. Qed. -(* - -Lemma safe_skiperase1 {e1 v2 σ σ'}: - erased_step ([e1], σ) ([tv v2], σ') → - safe (erase_tm e1). -Proof. - destruct σ, σ'. - rewrite /safe => /simulation_skiperase_erased_step' /= Hsafe e' thp [] [] Hred Hin. - destruct (rtc_erased_step_inversion Hred) as [e'' ?]; simplify_eq. - move: Hin; rewrite elem_of_list_singleton => ?; subst e''. - pose proof (rtc_erased_steps_det Hsafe Hred) as Hremaining. - destruct (rtc_inv _ _ Hremaining) as [|Hrem]; simplify_eq/=. - - left; eauto. - - right; destruct Hrem as [[thp []] [Hrred%erased_step_inversion _]]. - hnf; naive_solver. -Qed. *) - (* Lemma fill_erase_expr {e e1 Ks} : erase_tm e = fill Ks e1 → ∃ Ks' e1', Ks