From eb36249e74f4fefc09f21cf41223b9464cdce68b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Apr 2018 19:16:11 +0200
Subject: [PATCH] accessor-style iInv without Hclose

---
 theories/base_logic/lib/auth.v                |  3 +-
 theories/base_logic/lib/boxes.v               | 20 ++---
 .../base_logic/lib/cancelable_invariants.v    | 24 +++---
 theories/base_logic/lib/invariants.v          |  9 +--
 theories/base_logic/lib/na_invariants.v       | 19 ++---
 theories/base_logic/lib/sts.v                 |  3 +-
 theories/base_logic/lib/viewshifts.v          |  3 +-
 theories/heap_lang/lib/counter.v              | 47 ++++++------
 theories/heap_lang/lib/increment.v            |  5 +-
 theories/heap_lang/lib/spawn.v                | 14 ++--
 theories/heap_lang/lib/spin_lock.v            | 15 ++--
 theories/heap_lang/lib/ticket_lock.v          | 44 +++++------
 theories/program_logic/weakestpre.v           | 22 ++++++
 theories/proofmode/class_instances_sbi.v      | 14 +++-
 theories/proofmode/classes.v                  | 31 ++++++--
 theories/proofmode/coq_tactics.v              | 18 ++++-
 theories/proofmode/ltac_tactics.v             | 63 ++++++++--------
 theories/proofmode/monpred.v                  | 10 +--
 theories/tests/one_shot.v                     | 18 ++---
 theories/tests/proofmode_iris.v               | 73 +++++++------------
 20 files changed, 248 insertions(+), 207 deletions(-)

diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index bd849ac1f..f0a8c87e0 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -144,7 +144,8 @@ Section auth.
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
       ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E∖↑N,E}=∗ auth_own γ b.
   Proof using Type*.
-    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
+    iIntros (?) "[Hinv Hγf]". rewrite /auth_ctx.
+    iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
     (* The following is essentially a very trivial composition of the accessors
        [auth_acc] and [inv_open] -- but since we don't have any good support
        for that currently, this gets more tedious than it should, with us having
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 82739945d..ea423840b 100644
--- 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".
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 762d6e22e..2ce16d7f6 100644
--- 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.
 
@@ -84,23 +83,22 @@ Section proofs.
     cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
     iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
-    iInv N as "[HP | >Hγ']" "Hclose".
+    iMod (inv_open with "Hinv") as "[[HP | >Hγ'] Hclose]"; first done.
     - iIntros "!> {$Hγ}". iSplitL "HP".
-      + iNext. iApply "HP'". done.
+      + iApply "HP'". done.
       + iIntros "HP". iApply "Hclose". iLeft. iNext. by iApply "HP'".
     - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
   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 elim_inv_cinv E N γ P p Q Q' :
+    InvOpener E (E∖↑N) (▷ P ∗ cinv_own γ p) (▷ P) None Q Q' →
+    ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p) (▷ P ∗ cinv_own γ p) Q Q'.
   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 /ElimInv /InvOpener. iIntros (Helim ?) "(#Hinv & Hown & Hcont)".
+    iApply (Helim with "Hcont"). clear Helim. rewrite -assoc.
+    iApply (cinv_open with "Hinv"); done.
   Qed.
 End proofs.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 5ec29362d..81def8c6a 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -110,12 +110,11 @@ 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'.
+  InvOpener E (E∖↑N) (▷ P) (▷ P) None Q Q' →
+  ElimInv (↑N ⊆ E) (inv N P) True (▷ P) Q Q'.
 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 /ElimInv /InvOpener. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
+  iApply (Hopener with "Hcont"). iApply inv_open; done.
 Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c1116ef9c..a1c6d8950 100644
--- 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".
+    iMod (inv_open with "Hinv") as "[[[$ >Hdis]|>Htoki2] Hclose]"; first done.
     - 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') →
+    InvOpener E E (▷ P ∗ na_own p (F ∖ ↑ N)) (▷ P ∗ na_own p (F ∖ ↑ N))
+              (Some (na_own p F)) 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'.
+      (▷ P ∗ na_own p (F∖↑N)) Q Q'.
   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 /ElimInv /InvOpener. iIntros (Helim (?&?)) "(#Hinv & Hown & Hcont)".
+    iApply (Helim with "Hcont"). clear Helim. rewrite -assoc /=.
+    iApply (na_inv_open with "Hinv"); done.
   Qed.
 End proofs.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 0d8e8ced6..ecf58f3aa 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -156,7 +156,8 @@ Section sts.
       ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
   Proof.
-    iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
+    iIntros (?) "[Hinv Hγf]". rewrite /sts_ctx.
+    iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
     (* The following is essentially a very trivial composition of the accessors
        [sts_acc] and [inv_open] -- but since we don't have any good support
        for that currently, this gets more tedious than it should, with us having
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index e45a87c0c..6f418757b 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -72,7 +72,8 @@ Qed.
 Lemma vs_inv N E P Q R :
   ↑N ⊆ E → inv N R ∗ (▷ R ∗ P ={E∖↑N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q.
 Proof.
-  iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
+  iIntros (?) "#[Hinv Hvs] !# HP".
+  iMod (inv_open with "Hinv") as "[HR Hclose]"; first done.
   iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
   by iApply "Hclose".
 Qed.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 8aee1924b..94252d1bd 100644
--- 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. 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. 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.
+      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]".
+    iApply wp_fupd. 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. 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. 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.
+      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|].
+    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|].
+    iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     by iApply "HΦ".
   Qed.
 End contrib_spec.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 331ba1db0..f4d2d8803 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -68,7 +68,7 @@ Section increment_client.
     WP incr_client #x {{ _, True }}%I.
   Proof using Type*.
     wp_let. wp_alloc l as "Hl". wp_let.
-    iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
+    iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
     (* FIXME: I am only usign persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional â–¡. *)
     iAssert (□ atomic_update (λ (v: Z), l ↦ #v)
@@ -78,7 +78,8 @@ Section increment_client.
     { iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
       iIntros "!#" (E) "% _".
       assert (E = ⊤) as -> by set_solver.
-      iInv nroot as (x) ">H↦" "Hclose".
+      iMod (inv_open with "Hinv") as "[>H↦ Hclose]"; first done.
+      iDestruct "H↦" as (x) "H↦".
       iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
       iExists _. iFrame. iSplit.
       { iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index f9059566e..4a5f29dec 100644
--- 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. iSplit; last done. iNext. 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.
+  - 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Φ".
+    + iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
+      wp_match. by iApply "HΦ".
     + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
 Qed.
 End proof.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 23b63251c..fda6a03ed 100644
--- 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. 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]").
+      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Φ".
+    iNext. iExists false. by iFrame.
   Qed.
 End proof.
 
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index c108b3f36..94e8ac955 100644
--- 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 "_".
+      + 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]").
+    - 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. 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. 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 "_".
+      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 "_".
+    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,7 +154,7 @@ 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Φ".
+    iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
     iNext. iExists (S o), n'.
     rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 8aa18f95e..e671a953f 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -404,4 +404,26 @@ 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 inv_opener_wp E1 E2 P P' (P'' : option _) e s Φ :
+    Atomic (stuckness_to_atomicity s) e →
+    InvOpener E1 E2 P P' P'' (WP e @ s; E1 {{ Φ }})
+              (WP e @ s; E2 {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+  Proof.
+    intros ?. rewrite /InvOpener. setoid_rewrite coq_tactics.maybe_wand_sound.
+    iIntros "Hinner >[HP Hclose]".
+    iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
+    iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
+  Qed.
+
+  Global Instance inv_opener_wp_nonatomic E P P' (P'' : option _) e s Φ :
+    InvOpener E E P P' P'' (WP e @ s; E {{ Φ }})
+              (WP e @ s; E {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+  Proof.
+    rewrite /InvOpener. setoid_rewrite coq_tactics.maybe_wand_sound.
+    iIntros "Hinner >[HP Hclose]". iApply wp_fupd.
+    iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
+    iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
+  Qed.
+
 End proofmode_classes.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 78b7091f7..fdfdb69a8 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -1,6 +1,6 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes.
+From iris.proofmode Require Import modality_instances classes class_instances_bi ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -551,6 +551,18 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
   AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
 Proof. by rewrite /AddModal !embed_fupd. Qed.
 
+(* InvOpener *)
+Global Instance inv_opener_vs `{BiFUpd PROP} E1 E2 E P P' (P'' : option PROP) Q :
+  (* FIXME: Why %I? ElimInv should set the right scopes! *)
+  InvOpener E1 E2 P P' P''
+            (|={E1,E}=> Q) (|={E2}=> (P' ∗ (coq_tactics.maybe_wand P'' (|={E1,E}=> Q))))%I.
+Proof.
+  rewrite /InvOpener coq_tactics.maybe_wand_sound.
+  iIntros "Hinner >[HP Hclose]".
+  iMod ("Hinner" with "HP") as "[HP Hfin]".
+  iMod ("Hclose" with "HP") as "HP''". by iApply "Hfin".
+Qed.
+
 (* IntoLater *)
 Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
 Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index cf32bcd96..ed0e4d354 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -513,12 +513,27 @@ Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
 Arguments IntoInv {_} _%I _.
 Hint Mode IntoInv + ! - : typeclass_instances.
 
+(** Typeclass for assertions around which invariants can be opened.
+    Inputs: [Q]
+    Outputs: [E1], [E2], [P], [P'], [Q']
+
+    Transforms the goal [Q] into the goal [Q'] where additional assumptions [P]
+    are available, obtaining may require accessing invariants. Later, [P'] has
+    to be given up again to close these invariants again, which will
+    produce [P''].  If [P''] is None, that signifies [emp] and will be used to
+    make the goal shown to the user nicer (i.e., no unnecessary hypothesis is
+    added) *)
+Class InvOpener `{BiFUpd PROP} E1 E2 (P P' : PROP) (P'' : option PROP) (Q Q' : PROP) :=
+  inv_opener : ((P -∗ Q') -∗ (|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ default emp P'' id)) -∗ Q).
+Arguments InvOpener {_} {_} _ _ _%I _%I _%I _%I : simpl never.
+Arguments inv_opener {_} {_} _ _ _%I _%I _%I _%I {_}.
+Hint Mode InvOpener + + - - - - - ! - : typeclass_instances.
+
 (* Input: [Pinv]
    Arguments:
    - [Pinv] is an invariant assertion
    - [Pin] is an additional assertion needed for opening an invariant
    - [Pout] is the assertion obtained by opening the invariant
-   - [Pclose] is the assertion which contains an update modality to close the invariant
    - [Q] is a goal on which iInv may be invoked
    - [Q'] is the transformed goal that must be proved after opening the invariant.
 
@@ -527,11 +542,11 @@ Hint Mode IntoInv + ! - : typeclass_instances.
    is not a clearly associated instance of ElimModal of the right form
    (e.g. to handle Iris 2.0 usage of iInv).
 *)
-Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
-  elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q.
+Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Q Q' : PROP) :=
+  elim_inv : φ → Pinv ∗ Pin ∗ (Pout -∗ Q') ⊢ Q.
 Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
-Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
-Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
+Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I.
+Hint Mode ElimInv + - ! - - ! - : typeclass_instances.
 
 (* We make sure that tactics that perform actions on *specific* hypotheses or
 parts of the goal look through the [tc_opaque] connective, which is used to make
@@ -579,6 +594,6 @@ Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
   ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
 Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
   IntoInv P N → IntoInv (tc_opaque P) N := id.
-Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :
-  ElimInv φ Pinv Pin Pout Pclose Q Q' →
-  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
+Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Q Q' : PROP) :
+  ElimInv φ Pinv Pin Pout Q Q' →
+  ElimInv φ (tc_opaque Pinv) Pin Pout Q Q' := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index d8b0f59fd..f5c42b628 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -136,6 +136,12 @@ Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
   in
   match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
 
+Definition maybe_wand {PROP : bi} (P : option PROP) (Q : PROP) : PROP :=
+  match P with
+  | None => Q
+  | Some P => (P -∗ Q)%I
+  end.
+
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -438,6 +444,10 @@ Proof.
   rewrite /= assoc (comm _ P0 P) IH //.
 Qed.
 
+Lemma maybe_wand_sound (P : option PROP) Q :
+  maybe_wand P Q ⊣⊢ (default emp P id -∗ Q).
+Proof. destruct P; simpl; first done. rewrite emp_wand //. Qed.
+
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).
 Proof. by constructor. Qed.
@@ -1066,19 +1076,19 @@ Proof.
 Qed.
 
 (** * Invariants *)
-Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Pclose Q Q' :
+Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Q Q' :
   envs_lookup_delete false i Δ = Some (p, P, Δ') →
-  ElimInv φ P Pin Pout Pclose Q Q' →
+  ElimInv φ P Pin Pout Q Q' →
   φ →
   (∀ R, ∃ Δ'',
-    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Pclose -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
+    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
     envs_entails Δ'' R) →
   envs_entails Δ Q.
 Proof.
   rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
   rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
   apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
-  rewrite intuitionistically_if_elim -assoc wand_curry. auto.
+  rewrite intuitionistically_if_elim -assoc. auto.
 Qed.
 
 (** * Accumulate hypotheses *)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 49999e5b6..2f2230a2a 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -15,7 +15,7 @@ Declare Reduction env_cbv := cbv [
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
     envs_simple_replace envs_replace envs_split
     envs_clear_spatial envs_clear_persistent envs_incr_counter
-    envs_split_go envs_split prop_of_env].
+    envs_split_go envs_split prop_of_env maybe_wand].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
 Ltac env_reflexivity := env_cbv; exact eq_refl.
@@ -1887,7 +1887,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
 
 (* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
 invariant. *)
-Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
+Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) :=
   iStartProof;
   let pats := spec_pat.parse pats in
   lazymatch pats with
@@ -1897,67 +1897,68 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) c
   let H := iFresh in
   lazymatch type of select with
   | string =>
-     eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
+     eapply tac_inv_elim with _ select H _ _ _ _ _ _;
      first by (iAssumptionCore || fail "iInv: invariant" select "not found")
   | ident  =>
-     eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
+     eapply tac_inv_elim with _ select H _ _ _ _ _ _;
      first by (iAssumptionCore || fail "iInv: invariant" select "not found")
   | namespace =>
-     eapply tac_inv_elim with _ _ H _ _ _ _ _ _ _;
+     eapply tac_inv_elim with _ _ H _ _ _ _ _ _;
      first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
   | _ => fail "iInv: selector" select "is not of the right type "
   end;
     [iSolveTC ||
-     let I := match goal with |- ElimInv _ ?I  _ _ _ _ _ => I end in
+     let I := match goal with |- ElimInv _ ?I  _ _ _ _ => I end in
      fail "iInv: cannot eliminate invariant " I
     |try (split_and?; solve [ fast_done | solve_ndisj ])
     |let R := fresh in intros R; eexists; split; [env_reflexivity|];
      iSpecializePat H pats; last (
-       iApplyHyp H; clear R;
-       iIntros H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
-       iIntros Hclose;
+       iApplyHyp H; clear R; env_cbv;
+       iIntro H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
        tac H
     )].
 
-Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  iInvCore N with "[$]" as ltac:(tac) Hclose.
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) :=
+  iInvCore N with "[$]" as ltac:(tac).
 
-Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" constr(pat) :=
+   iInvCore N as (fun H => iDestructHyp H as pat).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1) pat) Hclose.
+    constr(pat) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1) pat).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
+    simple_intropattern(x2) ")" constr(pat) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
+    constr(pat) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat).
 Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
-Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as pat) Hclose.
+    constr(pat) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as pat).
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat) Hclose.
+    constr(pat) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat).
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
+    simple_intropattern(x2) ")" constr(pat) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat).
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
+    constr(pat) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat).
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
+    constr(pat) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
 
+(* Miscellaneous *)
 Tactic Notation "iAccu" :=
   iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar"].
 
+(** Automation *)
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 
 (* Make sure that by and done solve trivial things in proof mode *)
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index d3a495e55..31cbbb4bf 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -486,12 +486,12 @@ Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
 Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
 
-Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
-  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out 𝓟close (Q i) (Q' i)) →
-  MakeEmbed 𝓟in Pin → MakeEmbed 𝓟out Pout → MakeEmbed 𝓟close Pclose →
-  ElimInv φ ⎡𝓟inv⎤ Pin Pout Pclose Q Q'.
+Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out Pin Pout Q Q' :
+  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Q i) (Q' i)) →
+  MakeEmbed 𝓟in Pin → MakeEmbed 𝓟out Pout →
+  ElimInv φ ⎡𝓟inv⎤ Pin Pout Q Q'.
 Proof.
-  rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
+  rewrite /MakeEmbed /ElimInv=>H <- <- ?. iStartProof PROP.
   iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
 Qed.
 End sbi.
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index 566f52580..204ef6fff 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -49,15 +49,15 @@ Proof.
   { iNext. iLeft. by iSplitL "Hl". }
   iModIntro. iApply "Hf"; iSplit.
   - iIntros (n) "!#". wp_let.
-    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
-    + wp_cas_suc. iMod (own_update with "Hγ") as "Hγ".
+    iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+    + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
-      iMod ("Hclose" with "[-]"); last eauto.
+      wp_cas_suc. iSplitL; last eauto.
       iNext; iRight; iExists n; by iFrame.
-    + wp_cas_fail. iMod ("Hclose" with "[-]"); last eauto.
+    + wp_cas_fail. iSplitL; last eauto.
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!# /=". wp_seq. wp_bind (! _)%E.
-    iInv N as ">Hγ" "Hclose".
+    iInv N as ">Hγ".
     iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨
        ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
@@ -69,18 +69,18 @@ Proof.
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
-    iMod ("Hclose" with "[Hinv]") as "_"; eauto; iModIntro.
+    iSplitL "Hinv"; first by eauto.
     wp_let. iIntros "!#". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     { by wp_match. }
     wp_match. wp_bind (! _)%E.
-    iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m') "[Hl Hγ]".
+    iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
     { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
-    iMod ("Hclose" with "[Hl]") as "_".
+    iSplitL "Hl".
     { iNext; iRight; by eauto. }
-    iModIntro. wp_match. iApply wp_assert.
+    wp_match. iApply wp_assert.
     wp_op. by case_bool_decide.
 Qed.
 
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index 606dd94a4..dd793e037 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -63,9 +63,8 @@ Section iris_tests.
   Lemma test_iInv_0 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     iIntros "#H".
-    iInv N as "#H2" "Hclose".
-    iMod ("Hclose" with "H2").
-    iModIntro. by iNext.
+    iInv N as "#H2".
+    iModIntro. iSplit; auto.
   Qed.
 
   Lemma test_iInv_1 N E P:
@@ -73,18 +72,16 @@ Section iris_tests.
     inv N (<pers> P) ={E}=∗ ▷ P.
   Proof.
     iIntros (?) "#H".
-    iInv N as "#H2" "Hclose".
-    iMod ("Hclose" with "H2").
-    iModIntro. by iNext.
+    iInv N as "#H2".
+    iModIntro. iSplit; auto.
   Qed.
 
   Lemma test_iInv_2 γ p N P:
     cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
     iIntros "(#?&?)".
-    iInv N as "(#HP&Hown)" "Hclose".
-    iMod ("Hclose" with "HP").
-    iModIntro. iFrame. by iNext.
+    iInv N as "(#HP&Hown)".
+    iModIntro. iSplit; auto with iFrame.
   Qed.
 
   Lemma test_iInv_3 γ p1 p2 N P:
@@ -92,9 +89,8 @@ Section iris_tests.
       ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
   Proof.
     iIntros "(#?&Hown1&Hown2)".
-    iInv N with "[Hown2 //]" as "(#HP&Hown2)" "Hclose".
-    iMod ("Hclose" with "HP").
-    iModIntro. iFrame. by iNext.
+    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
+    iModIntro. iSplit; auto with iFrame.
   Qed.
 
   Lemma test_iInv_4 t N E1 E2 P:
@@ -103,10 +99,8 @@ Section iris_tests.
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N as "(#HP&Hown2)" "Hclose".
-    iMod ("Hclose" with "[HP Hown2]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N as "(#HP&Hown2)".
+    iModIntro. iSplitL "Hown2"; auto with iFrame.
   Qed.
 
   (* test named selection of which na_own to use *)
@@ -116,10 +110,8 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N with "Hown2" as "(#HP&Hown2)" "Hclose".
-    iMod ("Hclose" with "[HP Hown2]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N with "Hown2" as "(#HP&Hown2)".
+    iModIntro. iSplitL "Hown2"; auto with iFrame.
   Qed.
 
   Lemma test_iInv_6 t N E1 E2 P:
@@ -128,10 +120,8 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
-    iInv N with "Hown1" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[HP Hown1]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* test robustness in presence of other invariants *)
@@ -141,18 +131,15 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
-    iInv N3 with "Hown1" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[HP Hown1]").
-    { iFrame. done. }
-    iModIntro. iFrame. by iNext.
+    iInv N3 with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* iInv should work even where we have "inv N P" in which P contains an evar *)
   Lemma test_iInv_8 N : ∃ P, inv N P ={⊤}=∗ P ≡ True ∧ inv N P.
   Proof.
     eexists. iIntros "#H".
-    iInv N as "HP" "Hclose".
-    iMod ("Hclose" with "[$HP]"). auto.
+    iInv N as "HP". iFrame "HP". auto.
   Qed.
 
   (* test selection by hypothesis name instead of namespace *)
@@ -162,9 +149,8 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
-    iInv "HInv" with "Hown1" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[$HP $Hown1]").
-    iModIntro. iFrame. by iNext.
+    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* test selection by hypothesis name instead of namespace *)
@@ -174,27 +160,24 @@ Section iris_tests.
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
-    iInv "HInv" as "(#HP&Hown1)" "Hclose".
-    iMod ("Hclose" with "[$HP $Hown1]").
-    iModIntro. iFrame. by iNext.
+    iInv "HInv" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
   Qed.
 
   (* test selection by ident name *)
   Lemma test_iInv_11 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     let H := iFresh in
-    (iIntros H; iInv H as "#H2" "Hclose").
-    iMod ("Hclose" with "H2").
-    iModIntro. by iNext.
+    (iIntros H; iInv H as "#H2"). auto.
   Qed.
 
   (* error messages *)
   Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=∗ True.
   Proof.
     iIntros "H".
-    Fail iInv 34 as "#H2" "Hclose".
-    Fail iInv nroot as "#H2" "Hclose".
-    Fail iInv "H2" as "#H2" "Hclose".
+    Fail iInv 34 as "#H2".
+    Fail iInv nroot as "#H2".
+    Fail iInv "H2" as "#H2".
     done.
   Qed.
 
@@ -202,9 +185,7 @@ Section iris_tests.
   Lemma test_iInv_13 N:
     inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp.
   Proof.
-    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)" "Hclose".
-    iMod ("Hclose" with "[]").
-    { iNext; iExists O; done. }
-    iModIntro. by iNext.
+    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
+    eauto.
   Qed.
 End iris_tests.
-- 
GitLab