Commit 2891ccae authored by Ralf Jung's avatar Ralf Jung
Browse files

generalize lifting lemmas: better support view shifts that take a step

parent 5874f41e
Pipeline #4017 failed with stage
in 3 minutes and 7 seconds
......@@ -76,7 +76,7 @@ Lemma wp_fork E e Φ :
Φ (LitV LitUnit) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
- by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
- by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
- intros; inv_head_step; eauto.
Qed.
......@@ -86,7 +86,7 @@ Lemma wp_rec E f x erec e1 e2 Φ :
Closed (f :b: x :b: []) erec
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof.
intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork' (App _ _)
(subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -96,7 +96,7 @@ Lemma wp_un_op E op e v v' Φ :
un_op_eval op v = Some v'
Φ v' WP UnOp op e @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (UnOp op _) (of_val v'))
intros. rewrite -(wp_lift_pure_det_head_step_no_fork' (UnOp op _) (of_val v'))
-?wp_value'; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -106,7 +106,7 @@ Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
bin_op_eval op v1 v2 = Some v'
(Φ v') WP BinOp op e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val v'))
intros. rewrite -(wp_lift_pure_det_head_step_no_fork' (BinOp op _ _) (of_val v'))
-?wp_value'; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -114,14 +114,14 @@ Qed.
Lemma wp_if_true E e1 e2 Φ :
WP e1 @ E {{ Φ }} WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Proof.
apply wp_lift_pure_det_head_step_no_fork; eauto.
apply wp_lift_pure_det_head_step_no_fork'; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_if_false E e1 e2 Φ :
WP e2 @ E {{ Φ }} WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
Proof.
apply wp_lift_pure_det_head_step_no_fork; eauto.
apply wp_lift_pure_det_head_step_no_fork'; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -130,7 +130,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
Φ v1 WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ? [v2 ?].
rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1) -?wp_value; eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork' (Fst _) e1) -?wp_value; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -139,7 +139,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
Φ v2 WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros [v1 ?] ?.
rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2) -?wp_value; eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork' (Snd _) e2) -?wp_value; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -148,7 +148,7 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
WP App e1 e0 @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros [v0 ?].
rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e1 e0)); eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork' (Case _ _ _) (App e1 e0)); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -157,7 +157,7 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
WP App e2 e0 @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros [v0 ?].
rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork' (Case _ _ _) (App e2 e0)); eauto.
intros; inv_head_step; eauto.
Qed.
......
......@@ -12,11 +12,11 @@ Implicit Types v : val.
Implicit Types e : expr.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Lemma wp_ectx_bind {E e} K Φ :
Lemma wp_ectx_bind {E Φ} K e :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. apply: weakestpre.wp_bind. Qed.
Lemma wp_lift_head_step E Φ e1 :
Lemma wp_lift_head_step {E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
head_reducible e1 σ1
......@@ -30,14 +30,15 @@ Proof.
iApply "H". by eauto.
Qed.
Lemma wp_lift_pure_head_step E Φ e1 :
Lemma wp_lift_pure_head_step {E E' Φ} e1 :
( σ1, head_reducible e1 σ1)
( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs σ1 = σ2)
( e2 efs σ, head_step e1 σ e2 σ efs
(|={E,E'}=> e2 efs σ, head_step e1 σ e2 σ efs
WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
iIntros (??) "H". iApply wp_lift_pure_step; eauto.
iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro.
iIntros (????). iApply "H". eauto.
Qed.
......@@ -70,21 +71,32 @@ Proof.
by iApply big_sepL_nil.
Qed.
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :
( σ1, head_reducible e1 σ1)
( σ1 e2' σ2 efs',
head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' efs = efs')
(WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
(|={E,E'}=> WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
Lemma wp_lift_pure_det_head_step_no_fork {E E' Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 e2' σ2 efs',
head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}.
(|={E,E'}=> WP e2 @ E {{ Φ }}) WP e1 @ E {{ Φ }}.
Proof using Hinh.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
Qed.
Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 e2' σ2 efs',
head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}.
Proof using Hinh.
intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
rewrite -step_fupd_intro //.
Qed.
End wp.
......@@ -21,21 +21,24 @@ Lemma wp_lift_step E Φ e1 :
Proof. by rewrite wp_unfold /wp_pre=> ->. Qed.
(** Derived lifting lemmas. *)
Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
( σ1, reducible e1 σ1)
( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs σ1 = σ2)
( e2 efs σ, prim_step e1 σ e2 σ efs
(|={E,E'}=> e2 efs σ, prim_step e1 σ e2 σ efs
WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof.
iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
{ eapply reducible_not_val, (Hsafe inhabitant). }
iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
iIntros (σ1) "Hσ". iMod "H" as "H".
iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
destruct (Hstep σ1 e2 σ2 efs); auto; subst.
iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
iMod "Hclose" as "_". iFrame "Hσ". iMod "H" as "H". iApply "H"; auto.
Qed.
(* Atomic steps don't need any mask-changing business here, one can
use the generic lemmas here. *)
Lemma wp_lift_atomic_step {E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E}=
......@@ -54,13 +57,16 @@ Proof.
by iApply wp_value.
Qed.
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
( σ1, reducible e1 σ1)
( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' efs = efs')
(WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
(|={E,E'}=> WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}.
Proof.
iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
{ by intros; eapply Hpuredet. }
(* TODO: Can we make this nicer? iNext for fupd, for example, could help. *)
  • See #48 (closed), there we also decided that we do not want to have an iNext-like tactic for mask changing updates.

  • I planned to add a comment in that issue. ;) I think having such a tactic would be really useful for things like executing mask-changing view shifts. We could decide not to touch the persistent context for view shifts, then the suer has to keep things in the spatial context if they want to use this magic -- seems fine to me.

  • Alright, it probably should not be part of iNext or iModIntro then. Could you describe what you had in mind precisely in that issue?

  • Concretely, what I am doing there is executing view shifts that take a step. In the simplest possible case, my goal is |={E,E'}▷=> Q, and I have an assumption named "H" of the form |={E,E'}▷=> P. I want to strip the view shift that takes a step from both sides, so that I end up with goal |={E}=> Q and assumption P. Currently, I do iMod "H" as "H". iModIntro. iNext. iMod "H" as "H".. That's rather long. However, I just realized I can remove the as "H" as iMod defaults to re-using the old name (nice :). This leaves me with iMod "H". iModIntro. iNext. iMod "H"..

    So, thinking about it, I think I don't want or need iNext to do anything with mask-changing view shift, iMod does this just fine. The only thing I do not like about iMod "H". iModIntro. iNext. iMod "H". is the intermediate iModIntro. But that's not specific to this case, that comes up in more places. Maybe there are some situations in which it makes sense to do iModIntro automatically?

  • In this case, you could have used monotonicity .w.r.t wand of step taking fancy updates. I have done this in 84c05235.

    In general, you are right that we often do iMod ...; iModIntro. We could have syntax for that. Suggestions?

  • Hm, I have to say I prefer the iMod-based version over the iApply with monotonicity. It feels more natural, somehow.

Please register or sign in to reply
iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro.
by iIntros (e' efs' σ (_&->&->)%Hpuredet).
Qed.
End lifting.
  • In general, you are right that we often do iMod ...; iModIntro. We could have syntax for that. Suggestions?

    iMod!? iModFinal? Or maybe even iModIntro ...?

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