Merge branch 'jh_state_lifting'

heap_lang/lifting.v

@@ -29,14 +29,10 @@ Lemma wp_alloc_pst E σ e v Φ :
   ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   iIntros {?}  "[HP HΦ]".
-  (* TODO: This works around ssreflect bug #22. *)
-  set (φ (e' : expr []) σ' ef := ∃ l,
-    ef = None ∧ e' = Lit (LitLoc l) ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
-  iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
-    [by intros; subst φ; inv_head_step; eauto 8|].
-  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[Hφ HP]".
-  iDestruct "Hφ" as %(l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
-  iSplit; last done. iApply "HΦ"; by iSplit.
+  iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
+  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]". inv_head_step.
+  match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
+  subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :

program_logic/ectx_lifting.v

 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.program_logic Require Import ownership.
+From iris.proofmode Require Import weakestpre.
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
@@ -17,32 +18,40 @@ Lemma wp_ectx_bind {E e} K Φ :
   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 E1 E2
-    (φ : expr → state → option expr → Prop) Φ e1 σ1 :
+Lemma wp_lift_head_step E1 E2 Φ e1 :
   E2 ⊆ E1 → to_val e1 = None →
-  head_reducible e1 σ1 →
-  (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ∧ ownP σ2) ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
+  (|={E1,E2}=> ∃ σ1, ■ head_reducible e1 σ1 ∧
+       ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ head_step e1 σ1 e2 σ2 ef ∧ ownP σ2)
+                                 ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
   ⊢ WP e1 @ E1 {{ Φ }}.
-Proof. eauto using wp_lift_step. Qed.
+Proof.
+  iIntros {??} "H". iApply (wp_lift_step E1 E2); try done.
+  iPvs "H" as {σ1} "(%&Hσ1&Hwp)". set_solver. iPvsIntro. iExists σ1.
+  iSplit; first by eauto. iFrame. iNext. iIntros {e2 σ2 ef} "[% ?]".
+  iApply "Hwp". by eauto.
+Qed.
 
-Lemma wp_lift_pure_head_step E (φ : expr → option expr → Prop) Φ e1 :
+Lemma wp_lift_pure_head_step E Φ e1 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
-  (▷ ∀ e2 ef, ■ φ e2 ef → WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_pure_step. Qed.
+  (∀ σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
+  (▷ ∀ e2 ef σ, ■ head_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
+  ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  iIntros {???} "H". iApply wp_lift_pure_step; eauto. iNext.
+  iIntros {????}. iApply "H". eauto.
+Qed.
 
-Lemma wp_lift_atomic_head_step {E Φ} e1
-    (φ : expr → state → option expr → Prop) σ1 :
+Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
   atomic e1 →
   head_reducible e1 σ1 →
-  (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
   ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
-    ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
+  ■ head_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_atomic_step. Qed.
+Proof.
+  iIntros {??} "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
+  iIntros {???} "[% ?]". iApply "H". eauto.
+Qed.
 
 Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
   atomic e1 →

program_logic/hoare_lifting.v

@@ -18,80 +18,74 @@ Implicit Types e : expr Λ.
 Implicit Types P Q R : iProp Λ Σ.
 Implicit Types Ψ : val Λ → iProp Λ Σ.
 
-Lemma ht_lift_step E1 E2
-    (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Φ1 Φ2 Ψ e1 σ1 :
+Lemma ht_lift_step E1 E2 P Pσ1 Φ1 Φ2 Ψ e1 :
   E2 ⊆ E1 → to_val e1 = None →
-  reducible e1 σ1 →
-  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧
-   (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
-   (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
-   (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})
+  (P ={E1,E2}=> ∃ σ1, ■ reducible e1 σ1 ∧ ▷ ownP σ1 ★ ▷ Pσ1 σ1) ∧
+    (∀ σ1 e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ ownP σ2 ★ Pσ1 σ1
+                  ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
+    (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧
+    (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})
   ⊢ {{ P }} e1 @ E1 {{ Ψ }}.
 Proof.
-  iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
-  iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
-  iPvs ("Hvs" with "HP") as "[Hσ HP]"; first set_solver.
-  iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"].
-  iSpecialize ("HΦ" $! e2 σ2 ef with "[-]"). by iFrame "Hφ HP Hown".
-  iPvs "HΦ" as "[H1 H2]"; first by set_solver.
-  iPvsIntro. iSplitL "H1".
+  iIntros {??} "#(#Hvs&HΦ&He2&Hef) ! HP".
+  iApply (wp_lift_step E1 E2 _ e1); auto.
+  iPvs ("Hvs" with "HP") as {σ1} "(%&Hσ&HP)"; first set_solver.
+  iPvsIntro. iExists σ1. repeat iSplit. by eauto. iFrame.
+  iNext. iIntros {e2 σ2 ef} "[#Hstep Hown]".
+  iSpecialize ("HΦ" $! σ1 e2 σ2 ef with "[-]"). by iFrame "Hstep HP Hown".
+  iPvs "HΦ" as "[H1 H2]"; first by set_solver. iPvsIntro. iSplitL "H1".
   - by iApply "He2".
   - destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e)).
 Qed.
 
-Lemma ht_lift_atomic_step
-    E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
+Lemma ht_lift_atomic_step E P e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
-  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ _, True }}) ⊢
-  {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
+  (∀ e2 σ2 ef, {{ ■ prim_step e1 σ1 e2 σ2 ef ★ P }} ef ?@ ⊤ {{ _, True }}) ⊢
+  {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2
+                                       ★ ■ prim_step e1 σ1 (of_val v) σ2 ef }}.
 Proof.
-  iIntros {? Hsafe Hstep} "#Hef".
-  set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
-  iApply (ht_lift_step E E φ'  _ P
-    (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I
-    (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
-    try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
+  iIntros {? Hsafe} "#Hef".
+  iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I
+           (λ e2 σ2 ef, ownP σ2 ★ ■ (is_Some (to_val e2) ∧ prim_step e1 σ1 e2 σ2 ef))%I
+           (λ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ P)%I);
+    try by (eauto using atomic_not_val).
   repeat iSplit.
-  - by iIntros "! ?".
-  - iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro.
-    iSplitL "Hown". by iSplit. iSplit. by iDestruct "Hφ" as %[_ ?]. done.
+  - iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro.
+    iSplit. by eauto using atomic_step. iFrame. by auto.
+  - iIntros {? e2 σ2 ef} "! (%&Hown&HP&%)". iPvsIntro. subst.
+    iFrame. iSplit; iPureIntro; auto. split; eauto using atomic_step.
   - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
     iApply wp_value'. iExists σ2, ef. by iSplit.
   - done.
 Qed.
 
-Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 :
+Lemma ht_lift_pure_step E P P' Ψ e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
-  (∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧
-    (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ _, True }})
+  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
+  (∀ e2 ef σ, {{ ■ prim_step e1 σ e2 σ ef ★ P }} e2 @ E {{ Ψ }}) ∧
+    (∀ e2 ef σ, {{ ■ prim_step e1 σ e2 σ ef ★ P' }} ef ?@ ⊤ {{ _, True }})
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
-  iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
-  iApply (wp_lift_pure_step E φ _ e1); auto.
-  iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
+  iIntros {? Hsafe Hpure} "[#He2 #Hef] ! HP". iApply wp_lift_pure_step; auto.
+  iNext; iIntros {e2 ef σ Hstep}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
   - iApply "He2"; by iSplit.
-  - destruct ef as [e|]; last done.
-    iApply ("Hef" $! _ (Some e)); by iSplit.
+  - destruct ef as [e|]; last done. iApply ("Hef" $! _ (Some e)); by iSplit.
 Qed.
 
-Lemma ht_lift_pure_det_step
-    E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 e2 ef :
+Lemma ht_lift_pure_det_step E P P' Ψ e1 e2 ef :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
   {{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }}
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
-  iIntros {? Hsafe Hdet} "[#He2 #Hef]".
-  iApply (ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
-  iSplit; iIntros {e2' ef'}.
-  - iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2".
+  iIntros {? Hsafe Hpuredet} "[#He2 #Hef]".
+  iApply ht_lift_pure_step; eauto. by intros; eapply Hpuredet.
+  iSplit; iIntros {e2' ef' σ}.
+  - iIntros "! [% ?]". edestruct Hpuredet as (_&->&->). done. by iApply "He2".
   - destruct ef' as [e'|]; last done.
-    iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef".
+    iIntros "! [% ?]". edestruct Hpuredet as (_&->&->). done. by iApply "Hef".
 Qed.
 End lifting.

program_logic/lifting.v

 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import wsat ownership.
+From iris.proofmode Require Import pviewshifts.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (_ ⊥ _) => set_solver.
 Local Hint Extern 10 (✓{_} _) =>
@@ -17,41 +18,40 @@ Implicit Types Φ : val Λ → iProp Λ Σ.
 
 Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
 
-Lemma wp_lift_step E1 E2
-    (φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 σ1 :
+Lemma wp_lift_step E1 E2 Φ e1 :
   E2 ⊆ E1 → to_val e1 = None →
-  reducible e1 σ1 →
-  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
-  (|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef,
-    (■ φ e2 σ2 ef ∧ ownP σ2) ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
+  (|={E1,E2}=> ∃ σ1, ■ reducible e1 σ1 ∧ ▷ ownP σ1 ★
+       ▷ ∀ e2 σ2 ef, (■ prim_step e1 σ1 e2 σ2 ef ∧ ownP σ2)
+                     ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
   ⊢ WP e1 @ E1 {{ Φ }}.
 Proof.
-  intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq.
-  uPred.unseal; split=> n r ? Hvs; constructor; auto.
-  intros k Ef σ1' rf ???; destruct (Hvs (S k) Ef σ1' rf)
-    as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
+  intros ? He. rewrite pvs_eq wp_eq.
+  uPred.unseal; split=> n r ? Hvs; constructor; auto. intros k Ef σ1' rf ???.
+  destruct (Hvs (S k) Ef σ1' rf) as (r'&(σ1&Hsafe&r1&r2&?&?&Hwp)&Hws);
+    auto; clear Hvs; cofe_subst r'.
   destruct (wsat_update_pst k (E2 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
   { apply equiv_dist. rewrite -(ownP_spec k); auto. }
   { by rewrite assoc. }
   constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
   destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 k Ef σ2 rf)
     as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
-  { split. by eapply Hstep. apply ownP_spec; auto. }
+  { split. done. apply ownP_spec; auto. }
   { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
   exists r1', r2'; split_and?; try done. by uPred.unseal; intros ? ->.
 Qed.
 
-Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
+Lemma wp_lift_pure_step E Φ e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
-  (▷ ∀ e2 ef, ■ φ e2 ef → WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
+  (▷ ∀ e2 ef σ, ■ prim_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   intros He Hsafe Hstep; rewrite wp_eq; uPred.unseal.
   split=> n r ? Hwp; constructor; auto.
   intros k Ef σ1 rf ???; split; [done|]. destruct n as [|n]; first lia.
   intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
-  destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
+  destruct (Hwp e2 ef σ1 k r) as (r1&r2&Hr&?&?); auto.
   exists r1,r2; split_and?; try done.
   - rewrite -Hr; eauto using wsat_le.
   - uPred.unseal; by intros ? ->.
@@ -60,44 +60,31 @@ Qed.
 (** Derived lifting lemmas. *)
 Import uPred.
 
-Lemma wp_lift_atomic_step {E Φ} e1
-    (φ : expr Λ → state Λ → option (expr Λ) → Prop) σ1 :
+Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
-  (∀ e2 σ2 ef,
-    prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
   ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
-    ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
+    ■ prim_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,
-    is_Some (to_val e2) ∧ φ e2 σ2 ef) _ e1 σ1) //;
-    try by (eauto using atomic_not_val, atomic_step).
-  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2'; apply forall_intro=>σ2'.
-  apply forall_intro=>ef; apply wand_intro_l.
-  rewrite always_and_sep_l -assoc -always_and_sep_l.
-  apply pure_elim_l=>-[[v2 Hv] ?] /=.
-  rewrite -pvs_intro -wp_pvs.
-  rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) pure_equiv //.
-  rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //.
-  by erewrite of_to_val.
+  iIntros {??} "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
+  iPvsIntro. iExists σ1. repeat iSplit; eauto 10 using atomic_step.
+  iFrame. iNext. iIntros {e2 σ2 ef} "[% Hσ2]".
+  edestruct @atomic_step as [v2 Hv%of_to_val]; eauto. subst e2.
+  iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto.
+  iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val.
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
   atomic e1 →
   reducible e1 σ1 →
   (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
-    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
+                  σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
   ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef',
-    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1) //.
-  apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
-  apply wand_intro_l.
-  rewrite always_and_sep_l -assoc -always_and_sep_l to_of_val.
-  apply pure_elim_l=>-[-> [[->] ->]] /=. by rewrite wand_elim_r.
+  iIntros {?? Hdet} "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
+  iFrame. iNext. iIntros {v2' σ2' ef'} "[% Hσ2']".
+  edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
 Qed.
 
 Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
@@ -106,9 +93,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
   ▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  intros.
-  rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef') _ e1) //=.
-  apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
-  by apply impl_intro_l, pure_elim_l=>-[-> ->].
+  iIntros {?? Hpuredet} "?". iApply (wp_lift_pure_step E); try done.
+  by intros; eapply Hpuredet. iNext. by iIntros {e' ef' σ (_&->&->)%Hpuredet}.
 Qed.
 End lifting.