New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv...

New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hclose

theories/base_logic/lib/auth.v

@@ -144,8 +144,7 @@ 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 (?) "[Hinv Hγf]". rewrite /auth_ctx.
-    iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
+    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
     (* 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

theories/base_logic/lib/cancelable_invariants.v

@@ -83,21 +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]".
-    iMod (inv_open with "Hinv") as "[[HP | >Hγ'] Hclose]"; first done.
+    iInv N as "[HP | >Hγ']" "Hclose".
     - iIntros "!> {$Hγ}". iSplitL "HP".
-      + iApply "HP'". done.
+      + iNext. 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 E N γ P p Q Q' :
-    AccElim 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'.
+  Global Instance elim_inv_cinv E N γ P p :
+    IntoAcc (X:=unit) (cinv N γ P)
+            (↑N ⊆ E) (cinv_own γ p) E (E∖↑N)
+            (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
   Proof.
-    rewrite /ElimInv /AccElim. iIntros (Helim ?) "(#Hinv & Hown & Hcont)".
-    iApply (Helim with "Hcont"). clear Helim. rewrite -assoc.
+    rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
+    rewrite exist_unit -assoc.
     iApply (cinv_open with "Hinv"); done.
   Qed.
 End proofs.

theories/base_logic/lib/invariants.v

@@ -109,12 +109,12 @@ Qed.
 
 Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
-Global Instance elim_inv_inv E N P Q Q' :
-  AccElim E (E∖↑N) (▷ P) (▷ P) None Q Q' →
-  ElimInv (↑N ⊆ E) (inv N P) True (▷ P) Q Q'.
+Global Instance elim_inv_inv E N P :
+  IntoAcc (X:=unit) (inv N P) 
+          (↑N ⊆ E) True E (E∖↑N) (λ _, ▷ P)%I (λ _, ▷ P)%I (λ _, None)%I.
 Proof.
-  rewrite /ElimInv /AccElim. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
-  iApply (Hopener with "Hcont"). iApply inv_open; done.
+  rewrite /IntoAcc /accessor exist_unit.
+  iIntros (?) "#Hinv _". iApply inv_open; done.
 Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :
@@ -123,4 +123,5 @@ Proof.
   iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
   iIntros "!> {$HP} HP". iApply "Hclose"; auto.
 Qed.
+
 End inv.

theories/base_logic/lib/na_invariants.v

@@ -101,7 +101,7 @@ 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 $] $]".
-    iMod (inv_open with "Hinv") as "[[[$ >Hdis]|>Htoki2] Hclose]"; first done.
+    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
     - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
       iIntros "!> [HP $]".
       iInv N as "[[_ >Hdis2]|>Hitok]".
@@ -113,14 +113,14 @@ Section proofs.
 
   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':
-    AccElim 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)) Q Q'.
+  Global Instance elim_inv_na p F E N P :
+    IntoAcc (X:=unit) (na_inv p N P)
+            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) 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 /AccElim. iIntros (Helim (?&?)) "(#Hinv & Hown & Hcont)".
-    iApply (Helim with "Hcont"). clear Helim. rewrite -assoc /=.
+    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
+    rewrite exist_unit -assoc /=.
     iApply (na_inv_open with "Hinv"); done.
   Qed.
 End proofs.

theories/base_logic/lib/sts.v

@@ -156,8 +156,7 @@ Section sts.
       ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
       ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
   Proof.
-    iIntros (?) "[Hinv Hγf]". rewrite /sts_ctx.
-    iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
+    iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
     (* 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

theories/base_logic/lib/viewshifts.v

@@ -72,8 +72,7 @@ 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 (?) "#[Hinv Hvs] !# HP".
-  iMod (inv_open with "Hinv") as "[HR Hclose]"; first done.
+  iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
   iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
   by iApply "Hclose".
 Qed.

theories/bi/derived_laws_bi.v

@@ -219,6 +219,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.

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 "#Hinv"; first eauto.
+    iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; 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,8 +78,7 @@ Section increment_client.
     { iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
       iIntros "!#" (E) "% _".
       assert (E = ⊤) as -> by set_solver.
-      iMod (inv_open with "Hinv") as "[>H↦ Hclose]"; first done.
-      iDestruct "H↦" as (x) "H↦".
+      iInv nroot as (x) ">H↦" "Hclose".
       iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
       iExists _. iFrame. iSplit.
       { iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.

theories/program_logic/weakestpre.v

@@ -405,25 +405,26 @@ Section proofmode_classes.
     AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  Global Instance acc_elim_wp E1 E2 P P' (P'' : option _) e s Φ :
+  Global Instance acc_elim_wp {X} E1 E2 α β γ e s Φ :
     Atomic (stuckness_to_atomicity s) e →
-    AccElim E1 E2 P P' P'' (WP e @ s; E1 {{ Φ }})
-              (WP e @ s; E2 {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+    AccElim (X:=X) E1 E2 α β γ (WP e @ s; E1 {{ Φ }})
+            (λ x, WP e @ s; E2 {{ v, β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
   Proof.
     intros ?. rewrite /AccElim. 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".
+    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 acc_elim_wp_nonatomic E P P' (P'' : option _) e s Φ :
-    AccElim E E P P' P'' (WP e @ s; E {{ Φ }})
-            (WP e @ s; E {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+  Global Instance acc_elim_wp_nonatomic {X} E α β γ e s Φ :
+    AccElim (X:=X) E E α β γ (WP e @ s; E {{ Φ }})
+            (λ x, WP e @ s; E {{ v, β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
   Proof.
     rewrite /AccElim. 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".
+    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.

theories/proofmode/class_instances_sbi.v

@@ -552,15 +552,46 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
 Proof. by rewrite /AddModal !embed_fupd. Qed.
 
 (* AccElim *)
-Global Instance acc_elim_vs `{BiFUpd PROP} E1 E2 E P P' (P'' : option PROP) Q :
+Global Instance acc_elim_vs `{BiFUpd PROP} {X} E1 E2 E α β γ Q :
   (* FIXME: Why %I? AccElim sets the right scopes! *)
-  AccElim E1 E2 P P' P''
-          (|={E1,E}=> Q) (|={E2}=> (P' ∗ (coq_tactics.maybe_wand P'' (|={E1,E}=> Q))))%I.
-Proof.
-  rewrite /AccElim 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".
+  AccElim (X:=X) E1 E2 α β γ
+          (|={E1,E}=> Q)
+          (λ x, |={E2}=> (β x ∗ (coq_tactics.maybe_wand (γ x) (|={E1,E}=> Q))))%I.
+Proof.
+  rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
+  iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
+  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
+Qed.
+
+(* IntoAcc *)
+(* TODO: We could have instances from "unfolded" accessors with or without
+   the first binder. *)
+
+(* ElimInv *)
+Global Instance elim_inv_acc_without_close `{BiFUpd PROP} φ Pinv Pin
+       E1 E2 α β γ Q (Q' : () → PROP) :
+  IntoAcc (X:=unit) Pinv φ Pin E1 E2 α β γ →
+  AccElim (X:=unit) E1 E2 α β γ Q Q' →
+  ElimInv φ Pinv Pin (α ()) None Q (Q' ()).
+Proof.
+  rewrite /AccElim /IntoAcc /ElimInv.
+  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iApply (Helim with "[Hcont]").
+  - rewrite right_id. iIntros ([]). done.
+  - iApply (Hacc with "Hinv Hin"). done.
+Qed.
+
+Global Instance elim_inv_acc_with_close `{BiFUpd PROP} φ Pinv Pin
+       E1 E2 α β γ Q Q' :
+  IntoAcc (X:=unit) Pinv φ Pin E1 E2 α β γ →
+  (∀ R, ElimModal True false false (|={E1,E2}=> R) R Q Q') →
+  ElimInv φ Pinv Pin (α ()) (Some (β () ={E2,E1}=∗ default emp (γ ()) id))%I Q Q'.
+Proof.
+  rewrite /AccElim /IntoAcc /ElimInv.
+  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iMod (Hacc with "Hinv Hin") as ([]) "[Hα Hclose]"; first done.
+  iApply "Hcont". simpl. iSplitL "Hα"; done.
 Qed.
 
 (* IntoLater *)

theories/proofmode/classes.v

@@ -513,40 +513,74 @@ Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
 Arguments IntoInv {_} _%I _.
 Hint Mode IntoInv + ! - : typeclass_instances.
 
-(** Typeclass for assertions around which accessors can be elliminated.
-    Inputs: [Q], [P], [P'], [P'']
-    Outputs: [Q']
-    In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
-
-    Elliminates an accessor [|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ P'')] in goal [Q'],
-    turning the goal into [Q'] with a new assumption [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). [φ] is a Coq-level
-    side-condition that will be attempted to be discharged by solve_ndisj. *)
-Class AccElim `{BiFUpd PROP} E1 E2 (P P' : PROP) (P'' : option PROP) (Q Q' : PROP) :=
-  acc_elim : ((P -∗ Q') -∗ (|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ default emp P'' id)) -∗ Q).
-Arguments AccElim {_} {_} _ _ _%I _%I _%I _%I : simpl never.
-Arguments acc_elim {_} {_} _ _ _%I _%I _%I _%I {_}.
-Hint Mode AccElim + + - - ! ! ! ! - : typeclass_instances.
-
-(* Input: [Pinv]
+(** Accessors.
+    This definition only exists for the purpose of the proof mode; a truly
+    usable and general form would use telescopes and also allow binders for the
+    closing view shift.  [γ] is an [option] to make it easy for AccElim
+    instances to recognize the [emp] case and make it look nicer. *)
+Definition accessor `{BiFUpd PROP} {X : Type} (E1 E2 : coPset)
+           (α β : X → PROP) (γ : X → option PROP) : PROP :=
+  (|={E1,E2}=> ∃ x, α x ∗ (β x ={E2,E1}=∗ default emp (γ x) id))%I.
+
+(* Typeclass for assertions around which accessors can be elliminated.
+   Inputs: [Q], [α], [β], [γ]
+   Outputs: [Q']
+   In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
+
+   Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
+   into [Q'] with a new assumption [α x]. *)
+Class AccElim `{BiFUpd PROP} {X : Type} E1 E2 (α β : X → PROP) (γ : X → option PROP)
+      (Q : PROP) (Q' : X → PROP) :=
+  acc_elim : ((∀ x, α x -∗ Q' x) -∗ accessor E1 E2 α β γ -∗ Q).
+Arguments AccElim {_} {_} {_} _ _ _%I _%I _%I _%I : simpl never.
+Arguments acc_elim {_} {_} {_} _ _ _%I _%I _%I _%I {_}.
+Hint Mode AccElim + + ! - - ! ! ! ! - : typeclass_instances.
+
+(* Turn [P] into an accessor.
+   Inputs:
+   - [Pacc]: the assertion to be turned into an accessor (e.g. an invariant)
+   Outputs:
+   - [Pin]: additional logic assertion needed for starting the accessor.
+   - [φ]: additional Coq assertion needed for starting the accessor.
+   - [X] [α], [β], [γ]: the accessor parameters.
+   In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
+*)
+Class IntoAcc `{BiFUpd PROP} (Pacc : PROP) (φ : Prop) (Pin : PROP)
+      {X : Type} E1 E2 (α β : X → PROP) (γ : X → option PROP) :=
+  into_acc : φ → Pacc -∗ Pin -∗ accessor E1 E2 α β γ.
+Arguments IntoAcc {_} {_} _%I _ _%I {_} _ _ _%I _%I _%I : simpl never.
+Arguments into_acc {_} {_} _%I _ _%I {_} _ _ _%I _%I _%I {_} : simpl never.
+Hint Mode IntoAcc + - ! - - - - - - - - : typeclass_instances.
+
+(* The typeclass used for the [iInv] tactic.
+   Input: [Pinv]
    Arguments:
    - [Pinv] is an invariant assertion
-   - [Pin] is an additional assertion needed for opening an invariant
+   - [Pin] is an additional logic assertion needed for opening an invariant
+   - [φ] is an additional Coq assertion needed for opening an invariant
    - [Pout] is the assertion obtained by opening the invariant
+   - [Pclose] is the closing view shift.  It must be (Some _) or None
+     when doing typeclass search as instances are allowed to make a
+     case distinction on whether the user wants a closing view-shift or not.
    - [Q] is a goal on which iInv may be invoked
    - [Q'] is the transformed goal that must be proved after opening the invariant.
 
-   There are similarities to the definition of ElimModal, however we
-   want to be general enough to support uses in settings where there
-   is not a clearly associated instance of ElimModal of the right form
-   (e.g. to handle Iris 2.0 usage of iInv).
+   Most users will never want to instantiate this; there is a general instance
+   based on [AccElim] and [IntoAcc].  However, logics like Iris 2 that support
+   invariants but not mask-changing fancy updates can use this class directly to
+   still benefit from [iInv].
+
+   TODO: Add support for a binder (like accessors have it).
+
+   This is defined on sbi instead of bi as typeclass search otherwise
+   fails (e.g. in the iInv as used in cancelable_invariants.v)
 *)
-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.
-Hint Mode ElimInv + - ! - - ! - : typeclass_instances.
+Class ElimInv {PROP : sbi} (φ : Prop)
+      (Pinv Pin : PROP) (Pout : PROP) (Pclose : option PROP) (Q Q' : PROP) :=
+  elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ default emp Pclose id -∗ Q') ⊢ Q.
+Arguments ElimInv {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_inv {_} _ _%I _%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
@@ -594,6 +628,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 Q Q' : PROP) :
-  ElimInv φ Pinv Pin Pout Q Q' →
-  ElimInv φ (tc_opaque Pinv) Pin Pout Q Q' := id.
+Instance elim_inv_tc_opaque {PROP : sbi} φ Pinv Pin Pout Pclose Q Q' :
+  ElimInv (PROP:=PROP) φ Pinv Pin Pout Pclose Q Q' →
+  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.

theories/proofmode/coq_tactics.v

@@ -746,6 +746,7 @@ Proof.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
   rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
+
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -1075,22 +1076,6 @@ Proof.
   rewrite HΔ. by eapply elim_modal.
 Qed.
 
-(** * Invariants *)
-Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Q Q' :
-  envs_lookup_delete false i Δ = Some (p, P, Δ') →
-  ElimInv φ P Pin Pout Q Q' →
-  φ →
-  (∀ R, ∃ Δ'',
-    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. auto.
-Qed.
-
 (** * Accumulate hypotheses *)
 Lemma tac_accu Δ P :
   prop_of_env (env_spatial Δ) = P →
@@ -1339,6 +1324,22 @@ Implicit Types Γ : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
+(** * Invariants *)
+Lemma tac_inv_elim Δ Δ' i j φ p Pinv Pin Pout (Pclose : option PROP) Q Q' :
+  envs_lookup_delete false i Δ = Some (p, Pinv, Δ') →
+  ElimInv φ Pinv Pin Pout Pclose Q Q' →
+  φ →
+  (∀ R, ∃ Δ'',
+    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ maybe_wand Pclose 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 maybe_wand_sound -assoc wand_curry. auto.
+Qed.
+
 (** * Rewriting *)
 Lemma tac_rewrite Δ i p Pxy d Q :
   envs_lookup i Δ = Some (p, Pxy) →

theories/proofmode/ltac_tactics.v

@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 Export ident.
 
 Declare Reduction env_cbv := cbv [
-  option_bind
+  option_bind from_option (* TODO: Can we make these (and maybe_wand) reduce only if applied to a constructor? *)
   beq ascii_beq string_beq positive_beq Pos.succ ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
@@ -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) :=
+Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) open_constr(Hclose) :=
   iStartProof;
   let pats := spec_pat.parse pats in
   lazymatch pats with
@@ -1895,48 +1895,67 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) :
   | _ => fail "iInv: exactly one specialization pattern should be given"
   end;
   let H := iFresh in
+  let Pclose_pat :=
+    match Hclose with
+    | Some _ => open_constr:(Some _)
+    | None => open_constr:(None)
+    end in
   lazymatch type of select with
   | string =>
-     eapply tac_inv_elim with _ select H _ _ _ _ _ _;
+     eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
      first by (iAssumptionCore || fail "iInv: invariant" select "not found")
   | ident  =>
-     eapply tac_inv_elim with _ select H _ _ _ _ _ _;
+     eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
      first by (iAssumptionCore || fail "iInv: invariant" select "not found")
   | namespace =>
-     eapply tac_inv_elim with _ _ H _ _ _ _ _ _;
+     eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat);
      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; env_cbv;
        iIntro H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
+       match Hclose with
+       | Some ?Hcl => iIntros Hcl
+       | None => idtac
+       end;
        tac H
     )].
 
+(* Without closing view shift *)
+Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) :=
+  iInvCore N with pats as ltac:(tac) (@None string).
+(* Without pattern *)
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+  iInvCore N with "[$]" as ltac:(tac) Hclose.
+(* Without both *)
 Tactic Notation "iInvCore" constr(N) "as" tactic(tac) :=
-  iInvCore N with "[$]" as ltac:(tac).
+  iInvCore N with "[$]" as ltac:(tac) (@None string).
 
-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) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1) pat).
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    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)
+(* With everything *)
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as pat) (Some Hclose).
+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) (Some Hclose).
+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) (Some Hclose).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat).
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
+    constr(pat) constr(Hclose) :=
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) (Some Hclose).
+
+(* Without closing view shift *)
 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) ")"
@@ -1954,7 +1973,43 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(