Merge branch 'joe/inv_tac' into 'gen_proofmode'

General Invariant Tactic

See merge request FP/iris-coq!116

ProofMode.md

@@ -170,8 +170,11 @@ Rewriting / simplification
 Iris
 ----
 
-- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
-  for closing the invariant is put in a hypothesis named `Hclose`.
+- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
+   a namespace N or an identifier "H". Open the invariant indicated by S.  The
+   selection pattern `selpat` is used for any auxiliary assertions needed to
+   open the invariant (e.g. for cancelable or non-atomic invariants). The update
+   for closing the invariant is put in a hypothesis named `Hclose`.
 
 Miscellaneous
 -------------

theories/base_logic/lib/cancelable_invariants.v

@@ -90,6 +90,18 @@ Section proofs.
       + 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 (|={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'.
+  Proof.
+    rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
+    iApply (Helim with "[- $H2]"); first done.
+    iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
+    by iFrame.
+  Qed.
 End proofs.
 
 Typeclasses Opaque cinv_own cinv.

theories/base_logic/lib/invariants.v

 From iris.base_logic.lib Require Export fancy_updates.
-From stdpp Require Export  namespaces.
+From stdpp Require Export namespaces.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics coq_tactics intro_patterns.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -94,6 +94,17 @@ Proof.
   iApply "HP'". iFrame.
 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 (|={E,E∖↑N}=> R) R Q Q') →
+  ElimInv (↑N ⊆ E) (inv N P) True (▷ P) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
+Proof.
+  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
+  iApply (Helim with "[$H2]"); first done.
+  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
+Qed.
+
 Lemma inv_open_timeless E N P `{!Timeless P} :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
 Proof.
@@ -101,29 +112,3 @@ Proof.
   iIntros "!> {$HP} HP". iApply "Hclose"; auto.
 Qed.
 End inv.
-
-Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  let Htmp := iFresh in
-  let patback := intro_pat.parse_one Hclose in
-  let pat := constr:(IList [[IIdent Htmp; patback]]) in
-  iMod (inv_open _ N with "[#]") as pat;
-    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
-    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
-    |tac Htmp].
-
-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" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestructHyp H as (x1) pat) Hclose.
-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.
-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.
-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.

theories/base_logic/lib/na_invariants.v

@@ -110,4 +110,16 @@ Section proofs.
       + iFrame. iApply "Hclose". iNext. iLeft. by 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 (|={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'.
+  Proof.
+    rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
+    iApply (Helim with "[- $H2]"); first done.
+    iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
+    by iFrame.
+  Qed.
 End proofs.

theories/proofmode/classes.v

 From iris.bi Require Export bi.
+From stdpp Require Import namespaces.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -467,6 +468,32 @@ Proof. by apply as_valid. Qed.
 Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P → φ.
 Proof. by apply as_valid. Qed.
 
+(* Input: [P]; Outputs: [N],
+   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
+Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
+Arguments IntoInv {_} _%I _.
+Hint Mode IntoInv + ! - : 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.
+
+   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).
+*)
+Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
+  elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ Pclose -∗ Q') ⊢ Q.
+Arguments ElimInv {_} _ _ _%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
 definitions opaque for type class search. For example, when using `iDestruct`,
@@ -512,3 +539,8 @@ Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
 Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
   ElimModal φ P P' Q Q' → ElimModal φ (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.

theories/proofmode/coq_tactics.v

@@ -209,6 +209,16 @@ Proof.
   repeat apply sep_mono=>//; apply affinely_persistently_if_flag_mono; by destruct q1.
 Qed.
 
+Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
+  envs_lookup_delete rp j Δ = Some (p1, P, Δ') →
+  envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') →
+  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
+Proof. rewrite //= => -> //= -> //=. Qed.
+
+Lemma envs_lookup_delete_list_nil Δ rp :
+  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
+Proof. done. Qed.
+
 Lemma envs_lookup_snoc Δ i p P :
   envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
 Proof.
@@ -1159,6 +1169,22 @@ Proof.
   rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
   rewrite HΔ affinely_persistently_if_elim. by eapply elim_modal.
 Qed.
+
+(** * Invariants *)
+Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Pclose Q Q' :
+  envs_lookup_delete false i Δ = Some (p, P, Δ') →
+  ElimInv φ P Pin Pout Pclose Q Q' →
+  φ →
+  (∀ R, ∃ Δ'',
+    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ 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 affinely_persistently_if_elim -assoc wand_curry. auto.
+Qed.
 End bi_tactics.
 
 Section sbi_tactics.

theories/proofmode/tactics.v

 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
 From iris.bi Require Export bi big_op.
+From stdpp Require Import namespaces.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From stdpp Require Import hlist pretty.
@@ -1864,6 +1865,92 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
 
+(** * Invariant *)
+
+(* Finds a hypothesis in the context that is an invariant with
+   namespace [N].  To do so, we check whether for each hypothesis
+   ["H":P] we can find an instance of [IntoInv P N] *)
+Tactic Notation "iAssumptionInv" constr(N) :=
+  let rec find Γ i :=
+    lazymatch Γ with
+    | Esnoc ?Γ ?j ?P' =>
+      first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
+    end in
+  lazymatch goal with
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some _ =>
+     first [find Γp i|find Γs i]; env_reflexivity
+  end.
+
+(* 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) :=
+  iStartProof;
+  let pats := spec_pat.parse pats in
+  lazymatch pats with
+  | [_] => idtac
+  | _ => fail "iInv: exactly one specialization pattern should be given"
+  end;
+  let H := iFresh in
+  lazymatch type of select with
+  | string =>
+     eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
+     first by (iAssumptionCore || fail "iInv: invariant" select "not found")
+  | ident  =>
+     eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
+     first by (iAssumptionCore || fail "iInv: invariant" select "not found")
+  | namespace =>
+     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;
+    [apply _ ||
+     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;
+       tac H
+    )].
+
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+  iInvCore N with "[$]" as ltac:(tac) Hclose.
+
+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" "(" simple_intropattern(x1) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestructHyp H as (x1) pat) Hclose.
+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.
+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.
+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.
+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.
+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.
+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.
+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.
+
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 
 (* Make sure that by and done solve trivial things in proof mode *)

theories/tests/proofmode_iris.v

 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import base_logic lib.invariants.
+From iris.base_logic Require Import base_logic.
+From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
 Section base_logic_tests.
   Context {M : ucmraT}.
@@ -48,7 +49,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{invG Σ}.
+  Context `{invG Σ, cinvG Σ, na_invG Σ}.
 
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
@@ -58,4 +59,152 @@ Section iris_tests.
     iApply ("H" with "[% //] [$] [> HQ] [> //]").
     by iApply inv_alloc.
   Qed.
+
+  Lemma test_iInv_0 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Proof.
+    iIntros "#H".
+    iInv N as "#H2" "Hclose".
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  Lemma test_iInv_1 N E P:
+    ↑N ⊆ E →
+    inv N (bi_persistently P) ={E}=∗ ▷ P.
+  Proof.
+    iIntros (?) "#H".
+    iInv N as "#H2" "Hclose".
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  Lemma test_iInv_2 γ p N P:
+    cinv N γ (bi_persistently P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
+  Proof.
+    iIntros "(#?&?)".
+    iInv N as "(#HP&Hown)" "Hclose".
+    iMod ("Hclose" with "HP").
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  Lemma test_iInv_3 γ p1 p2 N P:
+    cinv N γ (bi_persistently P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
+      ={⊤}=∗ 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.
+  Qed.
+
+  Lemma test_iInv_4 t N E1 E2 P:
+    ↑N ⊆ E2 →
+    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+         ⊢ |={⊤}=> 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.
+  Qed.
+
+  (* test named selection of which na_own to use *)
+  Lemma test_iInv_5 t N E1 E2 P:
+    ↑N ⊆ E2 →
+    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ 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.
+  Qed.
+
+  Lemma test_iInv_6 t N E1 E2 P:
+    ↑N ⊆ E1 →
+    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ 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.
+  Qed.
+
+  (* test robustness in presence of other invariants *)
+  Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 →
+    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ 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.
+  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.
+  Qed.
+
+  (* test selection by hypothesis name instead of namespace *)
+  Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 →
+    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ 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.
+  Qed.
+
+  (* test selection by hypothesis name instead of namespace *)
+  Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 →
+    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+      ={⊤}=∗ 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.
+  Qed.
+
+  (* test selection by ident name *)
+  Lemma test_iInv_11 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Proof.
+    let H := iFresh in
+    (iIntros H; iInv H as "#H2" "Hclose").
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  (* error messages *)
+  Lemma test_iInv_12 N P: inv N (bi_persistently P) ={⊤}=∗ True.
+  Proof.
+    iIntros "H".
+    Fail iInv 34 as "#H2" "Hclose".
+    Fail iInv nroot as "#H2" "Hclose".
+    Fail iInv "H2" as "#H2" "Hclose".
+    done.
+  Qed.
+
+  (* test destruction of existentials when opening an invariant *)
+  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.
+  Qed.
 End iris_tests.