Commit 29c4fcf6 authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent names for `fill` lemmas of `LanguageCtx`.

Use `_inv` for the reverse direction.
parent eb200cc0
......@@ -470,7 +470,7 @@ Proof.
lazymatch K with
| [] => fail
| _ => apply (prim_step_matched_by_erased_steps_ectx K);
apply IH; [done| by eapply (not_stuck_fill (fill K))]
apply IH; [done| by eapply (not_stuck_fill_inv (fill K))]
end
in
reshape_expr e tac
......@@ -587,11 +587,11 @@ Proof.
end.
apply (prim_step_matched_by_erased_steps_ectx [ResolveMCtx _ _]).
apply IH; [rewrite !app_length /=; lia|done|
by eapply (not_stuck_fill (fill [ResolveMCtx _ _])); simpl].
by eapply (not_stuck_fill_inv (fill [ResolveMCtx _ _])); simpl].
- (** e1 is of the form ([Resolve] e1_ e1_2 e13) and e1_3 takes a prim_step. *)
apply (prim_step_matched_by_erased_steps_ectx [ResolveRCtx _ _]).
apply IH; [rewrite !app_length /=; lia|done|
by eapply (not_stuck_fill (fill [ResolveRCtx _ _])); simpl].
by eapply (not_stuck_fill_inv (fill [ResolveRCtx _ _])); simpl].
Qed.
Lemma erased_prim_step_prim_step e1 σ1 κ e2 σ2 efs:
......
......@@ -153,12 +153,18 @@ Section language.
Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
reducible e σ reducible (K e) σ.
Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed.
Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ :
to_val e = None reducible (K e) σ reducible e σ.
Proof.
intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
Qed.
Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
reducible_no_obs e σ reducible_no_obs (K e) σ.
Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed.
Lemma reducible_no_obs_fill_inv `{!@LanguageCtx Λ K} e σ :
to_val e = None reducible_no_obs (K e) σ reducible_no_obs e σ.
Proof.
intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
......@@ -166,19 +172,22 @@ Section language.
Qed.
Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
to_val e = None irreducible e σ irreducible (K e) σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed.
Lemma irreducible_fill_inv `{!@LanguageCtx Λ K} e σ :
irreducible (K e) σ irreducible e σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
Lemma not_stuck_fill K `{!@LanguageCtx Λ K} e σ :
Lemma not_stuck_fill_inv K `{!@LanguageCtx Λ K} e σ :
not_stuck (K e) σ not_stuck e σ.
Proof.
rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
- auto using fill_not_val.
- destruct (decide (to_val e = None)); auto using reducible_fill.
- destruct (decide (to_val e = None)); auto using reducible_fill_inv.
Qed.
Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
stuck e σ stuck (K e) σ.
Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill. Qed.
Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. Qed.
Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
t1 t1' step (t1,σ1) κ (t2,σ2) t2', t2 t2' step (t1',σ1) κ (t2',σ2).
......
......@@ -186,7 +186,7 @@ Proof.
iApply (twp_pre_mono with "[] IH"). by iIntros "!>" (E e Φ') "[_ ?]". }
rewrite /twp_pre fill_not_val //.
iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
{ destruct s; eauto using reducible_no_obs_fill. }
{ destruct s; eauto using reducible_no_obs_fill_inv. }
iIntros (κ e2 σ2 efs Hstep).
iMod ("IH" $! κ (K e2) σ2 efs with "[]") as (?) "(Hσ & IH & IHefs)"; eauto using fill_step.
iModIntro. iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
......@@ -199,7 +199,7 @@ Proof.
iIntros "H". iLöb as "IH" forall (E e Φ).
rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
{ destruct s; last done. eauto using reducible_no_obs_reducible. }
{ destruct s; eauto using reducible_no_obs_reducible. }
iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
iApply step_fupd_intro; [set_solver+|]. iNext.
iFrame "Hσ". iSplitL "H". by iApply "IH".
......
......@@ -160,8 +160,7 @@ Proof.
{ apply of_to_val in He as <-. by iApply fupd_wp. }
rewrite wp_unfold /wp_pre fill_not_val //.
iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
{ iPureIntro. destruct s; last done.
unfold reducible in *. naive_solver eauto using fill_step. }
{ destruct s; eauto using reducible_fill. }
iIntros (e2 σ2 efs Hstep).
destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
......@@ -177,7 +176,7 @@ Proof.
{ apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
rewrite fill_not_val //.
iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
{ destruct s; eauto using reducible_fill. }
{ destruct s; eauto using reducible_fill_inv. }
iIntros (e2 σ2 efs Hstep).
iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment