Merge branch 'ralf/inv' into 'gen_proofmode'

accessor-style iInv without Hclose See merge request FP/iris-coq!143

Merge branch 'ralf/inv' into 'gen_proofmode'
accessor-style iInv without Hclose See merge request FP/iris-coq!143
032ee4a5 · Ralf Jung · 80e3bc31 · 30cab675 · 032ee4a5 · 032ee4a5
Commit 032ee4a5 authored May 15, 2018 by Ralf Jung
20 changed files
--- a/naming.txt
+++ b/naming.txt
@@ -12,6 +12,7 @@ j
 k
 l
 m : iGst = ghost state
+m* : prefix for option
 n
 o
 p

--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -130,11 +130,11 @@ Lemma slice_delete_empty E q f P Q γ :
 Proof.
  iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
  iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
-  iInv N as (b) "[>Hγ _]" "Hclose".
+  iInv N as (b) "[>Hγ _]".
  iDestruct (big_opM_delete _ f _ false with "Hf")
    as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
-  iMod ("Hclose" with "[Hγ]"); first iExists false; eauto.
+  iModIntro. iSplitL "Hγ"; first iExists false; eauto.
  iModIntro. iNext. iSplit.
  - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
    iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
@@ -147,11 +147,11 @@ Lemma slice_fill E q f γ P Q :
  slice N γ Q -∗ ▷ Q -∗ ▷?q box N f P ={E}=∗ ▷?q box N (<[γ:=true]> f) P.
 Proof.
  iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iInv N as (b') "[>Hγ _]" "Hclose".
+  iInv N as (b') "[>Hγ _]".
  iDestruct (big_opM_delete _ f _ false with "Hf")
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
  iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
-  iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
+  iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
  iModIntro; iNext; iExists Φ; iSplit.
  - by rewrite big_opM_insert_override.
  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
@@ -164,13 +164,13 @@ Lemma slice_empty E q f P Q γ :
  slice N γ Q -∗ ▷?q box N f P ={E}=∗ ▷ Q ∗ ▷?q box N (<[γ:=false]> f) P.
 Proof.
  iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iInv N as (b) "[>Hγ HQ]" "Hclose".
+  iInv N as (b) "[>Hγ HQ]".
  iDestruct (big_opM_delete _ f with "Hf")
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
  iFrame "HQ".
  iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
-  iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
+  iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
  iModIntro; iNext; iExists Φ; iSplit.
  - by rewrite big_opM_insert_override.
  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
@@ -213,9 +213,9 @@ Proof.
  rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
  iApply (@big_sepM_impl with "Hf").
  iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
-  iInv N as (b) "[>Hγ _]" "Hclose".
+  iInv N as (b) "[>Hγ _]".
  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
-  iApply "Hclose". iNext; iExists true. by iFrame.
+  iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
 Qed.

 Lemma box_empty E f P :
@@ -230,10 +230,10 @@ Proof.
  { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
    iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
    assert (true = b) as <- by eauto.
-    iInv N as (b) "[>Hγ HΦ]" "Hclose".
+    iInv N as (b) "[>Hγ HΦ]".
    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
    iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
-    iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
+    iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
    iFrame "HγΦ Hinv". by iApply "HΦ". }
  iModIntro; iSplitL "HΦ".
  - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".

--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -73,9 +73,8 @@ Section proofs.
  Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
  Proof.
    iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
-    iInv N as "[HP|>Hγ']" "Hclose".
-    - iMod ("Hclose" with "[Hγ]") as "_"; first by eauto. iModIntro. iNext.
-      iApply "HP'". done.
+    iInv N as "[HP|>Hγ']".
+    - iModIntro. iFrame "Hγ". iModIntro. iApply "HP'". done.
    - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
  Qed.

@@ -92,15 +91,15 @@ Section proofs.
  Qed.

  Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
-  Global Instance elim_inv_cinv p γ E N P Q Q' :
-    (∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
-    ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p)
-      (▷ P ∗ cinv_own γ p) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+
+  Global Instance into_acc_cinv E N γ P p :
+    IntoAcc (X:=unit) (cinv N γ P)
+            (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
+            (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
  Proof.
-    rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
-    iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
-    iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
-    by iFrame.
+    rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
+    rewrite exist_unit -assoc.
+    iApply (cinv_open with "Hinv"); done.
  Qed.
 End proofs.


--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -109,13 +109,13 @@ Qed.

 Global Instance into_inv_inv N P : IntoInv (inv N P) N.

-Global Instance elim_inv_inv E N P Q Q' :
-  (∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
-  ElimInv (↑N ⊆ E) (inv N P) True (▷ P) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+Global Instance into_acc_inv E N P :
+  IntoAcc (X:=unit) (inv N P) 
+          (↑N ⊆ E) True (fupd E (E∖↑N)) (fupd (E∖↑N) E)
+          (λ _, ▷ P)%I (λ _, ▷ P)%I (λ _, None)%I.
 Proof.
-  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
-  iApply (Helim with "[H2]"); [done|]; simpl. iSplitR "H2"; [|done].
-  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
+  rewrite /IntoAcc /accessor exist_unit.
+  iIntros (?) "#Hinv _". iApply inv_open; done.
 Qed.

 Lemma inv_open_timeless E N P `{!Timeless P} :
@@ -124,4 +124,5 @@ Proof.
  iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!> {$HP} HP". iApply "Hclose"; auto.
 Qed.
+
 End inv.
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -101,25 +101,26 @@ Section proofs.
    rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
    rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
    iDestruct "Htoks" as "[[Htoki $] $]".
-    iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
+    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
      iIntros "!> [HP $]".
-      iInv N as "[[_ >Hdis2]|>Hitok]" "Hclose".
+      iInv N as "[[_ >Hdis2]|>Hitok]".
      + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
        set_solver.
-      + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
+      + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
  Qed.

  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
-  Global Instance elim_inv_na p F E N P Q Q':
-    (∀ R, ElimModal True false false (|={E}=> R)%I R Q Q') →
-    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
-      (▷ P ∗ na_own p (F∖↑N)) (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F) Q Q'.
+
+  Global Instance into_acc_na p F E N P :
+    IntoAcc (X:=unit) (na_inv p N P)
+            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
+            (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
+              (λ _, Some (na_own p F))%I.
  Proof.
-    rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
-    iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
-    iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
-    by iFrame.
+    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
+    rewrite exist_unit -assoc /=.
+    iApply (na_inv_open with "Hinv"); done.
  Qed.
 End proofs.
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -231,6 +231,20 @@ Proof.
  - apply impl_intro_r, impl_elim_r', exist_elim=>x.
    apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
 Qed.
+Lemma forall_unit (Ψ : unit → PROP) :
+  (∀ x, Ψ x) ⊣⊢ Ψ ().
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite (forall_elim ()) //.
+  - apply forall_intro=>[[]]. done.
+Qed.
+Lemma exist_unit (Ψ : unit → PROP) :
+  (∃ x, Ψ x) ⊣⊢ Ψ ().
+Proof.
+  apply (anti_symm (⊢)).
+  - apply exist_elim=>[[]]. done.
+  - rewrite -(exist_intro ()). done.
+Qed.

 Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
 Proof.

--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -46,24 +46,24 @@ Section mono_proof.
    {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
-    iDestruct "Hl" as (γ) "[#Hinv Hγf]".
-    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
-    wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
-    iModIntro. wp_let. wp_op.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
+    iDestruct "Hl" as (γ) "[#? Hγf]".
+    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_let. wp_op.
+    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
    destruct (decide (c' = c)) as [->|].
    - iDestruct (own_valid_2 with "Hγ Hγf")
        as %[?%mnat_included _]%auth_valid_discrete_2.
      iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+      wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
      iApply (own_mono with "Hγf"). apply: auth_frag_mono.
      by apply mnat_included, le_n_S.
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
-      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
+    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
+      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
      rewrite {3}/mcounter; eauto 10.
  Qed.

@@ -71,12 +71,13 @@ Section mono_proof.
    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
  Proof.
    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]".
+    wp_load.
    iDestruct (own_valid_2 with "Hγ Hγf")
      as %[?%mnat_included _]%auth_valid_discrete_2.
    iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
    { apply auth_update, (mnat_local_update _ _ c); auto. }
-    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
  Qed.
 End mono_proof.
@@ -123,19 +124,19 @@ Section contrib_spec.
    {{{ RET #(); ccounter γ q (S n) }}}.
  Proof.
    iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
-    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
-    wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
-    iModIntro. wp_let. wp_op.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
+    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_let. wp_op.
+    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
    destruct (decide (c' = c)) as [->|].
    - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
-      wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      iModIntro. wp_if. by iApply "HΦ".
+      wp_if. by iApply "HΦ".
    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
-      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
+      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
  Qed.

  Lemma read_contrib_spec γ l q n :
@@ -143,9 +144,9 @@ Section contrib_spec.
    {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
  Proof.
    iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
    iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
-    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
  Qed.

@@ -154,9 +155,9 @@ Section contrib_spec.
    {{{ n, RET #n; ccounter γ 1 n }}}.
  Proof.
    iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
+    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
-    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
    by iApply "HΦ".
  Qed.
 End contrib_spec.
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -55,21 +55,21 @@ Proof.
  wp_apply wp_fork; simpl. iSplitR "Hf".
  - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
  - wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
-    iInv N as (v') "[Hl _]" "Hclose".
-    wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
+    iInv N as (v') "[Hl _]".
+    wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
 Qed.

 Lemma join_spec (Ψ : val → iProp Σ) l :
  {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
 Proof.
  iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
-  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
+  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
-  - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
-    iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
+  - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
+    wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
  - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
-    + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
-      iModIntro. wp_match. by iApply "HΦ".
+    + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
+      wp_match. by iApply "HΦ".
    + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.
 End proof.

--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -61,12 +61,12 @@ Section proof.
    {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
  Proof.
    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
-    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
-    - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. iApply ("HΦ" $! false). done.
+    wp_rec. iInv N as ([]) "[Hl HR]".
+    - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
+      iApply ("HΦ" $! false). done.
    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
-      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-      iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+      iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
+      rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
  Qed.

  Lemma acquire_spec γ lk R :
@@ -83,8 +83,9 @@ Section proof.
  Proof.
    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
    iDestruct "Hlock" as (l ->) "#Hinv".
-    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
-    wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
+    wp_store. iSplitR "HΦ"; last by iApply "HΦ".
+    iModIntro. iNext. iExists false. by iFrame.
  Qed.
 End proof.


--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -88,20 +88,18 @@ Section proof.
  Proof.
    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
    iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
-    iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
+    iInv N as (o n) "(Hlo & Hln & Ha)".
    wp_load. destruct (decide (x = o)) as [->|Hneq].
    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-      + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
+      + iModIntro. iSplitL "Hlo Hln Hainv Ht".
        { iNext. iExists o, n. iFrame. }
-        iModIntro. wp_let. wp_op. case_bool_decide; [|done].
-        wp_if.
+        wp_let. wp_op. case_bool_decide; [|done]. wp_if.
        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
      + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
        set_solver.
-    - iMod ("Hclose" with "[Hlo Hln Ha]").
+    - iModIntro. iSplitL "Hlo Hln Ha".
      { iNext. iExists o, n. by iFrame. }
-      iModIntro. wp_let.
-      wp_op. case_bool_decide; [simplify_eq |].
+      wp_let. wp_op. case_bool_decide; [simplify_eq |].
      wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
  Qed.

@@ -110,30 +108,28 @@ Section proof.
  Proof.
    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
    iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
-    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
-    wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
+    iInv N as (o n) "[Hlo [Hln Ha]]".
+    wp_load. iModIntro. iSplitL "Hlo Hln Ha".
    { iNext. iExists o, n. by iFrame. }
-    iModIntro. wp_let. wp_proj. wp_op.
-    wp_bind (CAS _ _ _).
-    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
+    wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
+    iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
-    - wp_cas_suc.
-      iMod (own_update with "Hauth") as "[Hauth Hofull]".
+    - iMod (own_update with "Hauth") as "[Hauth Hofull]".
      { eapply auth_update_alloc, prod_local_update_2.
        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
        apply (seq_set_S_disjoint 0). }
      rewrite -(seq_set_S_union_L 0).
-      iMod ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
      { iNext. iExists o', (S n).
        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
-      iModIntro. wp_if.
+      wp_if.
      iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
      + iFrame. rewrite /is_lock; eauto 10.
      + by iNext.
-    - wp_cas_fail.
-      iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
+    - wp_cas_fail. iModIntro.
+      iSplitL "Hlo' Hln' Hauth Haown".
      { iNext. iExists o', n'. by iFrame. }
-      iModIntro. wp_if. by iApply "IH"; auto.
+      wp_if. by iApply "IH"; auto.
  Qed.

  Lemma release_spec γ lk R :
@@ -142,15 +138,15 @@ Section proof.
    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
    iDestruct "Hγ" as (o) "Hγo".
    wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
-    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
+    iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
    wp_load.
    iDestruct (own_valid_2 with "Hauth Hγo") as
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
-    iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
+    iModIntro. iSplitL "Hlo Hln Hauth Haown".
    { iNext. iExists o, n. by iFrame. }
-    iModIntro. wp_op.
-    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
-    wp_store.
+    wp_op.
+    iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
+    iApply wp_fupd. wp_store.
    iDestruct (own_valid_2 with "Hauth Hγo") as
      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
    iDestruct "Haown" as "[[Hγo' _]|Haown]".
@@ -158,8 +154,8 @@ Section proof.
    iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
    { apply auth_update, prod_local_update_1.
      by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
-    iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last by iApply "HΦ".
-    iNext. iExists (S o), n'.
+    iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
+    iIntros "!> !>". iExists (S o), n'.
    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
  Qed.
 End proof.

--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -404,4 +404,29 @@ Section proofmode_classes.
  Global Instance add_modal_fupd_wp s E e P Φ :
    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
+
+  Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
+    Atomic (stuckness_to_atomicity s) e →
+    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
+            α β γ (WP e @ s; E1 {{ Φ }})
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+  Proof.
+    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+  Qed.
+
+  Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
+    ElimAcc (X:=X) (fupd E E) (fupd E E)
+            α β γ (WP e @ s; E {{ Φ }})
+            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+  Proof.
+    rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+    iApply wp_fupd.
+    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+  Qed.
+
 End proofmode_classes.
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -84,6 +84,11 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.

+(** Copies of some definitions so we can control their unfolding *)
 Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
  match mx with Some x => f x | None => None end.
-Arguments option_bind _ _ _ !_ /.
+Arguments option_bind {_ _} _ !_ / : assert.
+
+Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
+  match mx with None => y | Some x => f x end.
+Arguments from_option {_ _} _ _ !_ / : assert.
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
 From stdpp Require Import nat_cancel