General invariant tactic.

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 P' Q Q' :
+    ElimModal True (|={E,E∖↑N}=> (▷ P ∗ cinv_own γ p) ∗ (▷ P ={E∖↑N,E}=∗ True))%I P' Q Q' →
+    ElimInv (↑N ⊆ E) N (cinv N γ P) [cinv_own γ p] P' Q Q'.
+  Proof.
+    rewrite /ElimInv/ElimModal.
+    iIntros (Helim ?) "(#H1&(Hown&_)&H2)".
+    iApply Helim; auto. iFrame "H2".
+    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,19 @@ 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 P' Q Q' :
+  ElimModal True (|={E,E∖↑N}=> ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True))%I P' Q Q' →
+  ElimInv (↑N ⊆ E) N (inv N P) [] P' Q Q'.
+Proof.
+  rewrite /ElimInv/ElimModal.
+  iIntros (Helim ?) "(#H1&_&H2)".
+  iApply Helim; auto; iFrame.
+  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto. 
+  iFrame. by iModIntro.
+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 +114,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,17 @@ 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 P' Q Q':
+    ElimModal True (|={E}=> (▷ P ∗ na_own p (F∖↑N)) ∗ (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F))%I
+              P' Q Q' →
+    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) N (na_inv p N P) [na_own p F] P' Q Q'.
+  Proof.
+    rewrite /ElimInv/ElimModal.
+    iIntros (Helim (?&?)) "(#H1&(Hown&_)&H2)".
+    iApply Helim; auto. iFrame "H2".
+    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,31 @@ 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`;
+   - `Pinv`, an invariant assertion
+   - `Ps_aux` is a list of additional assertions needed for opening an invariant;
+   - `Pout` is the assertion obtained by opening 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) (N: namespace)
+      (Pinv : PROP) (Ps_aux: list PROP) (Pout Q Q': PROP) :=
+  elim_inv : φ → Pinv ∗ [∗] Ps_aux ∗ (Pout -∗ 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`,

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,20 @@ 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 Δ1 Δ2 Δ3 js j p φ N P' P Ps Q Q' :
+  envs_lookup_delete_list false js Δ1 = Some (p, P :: Ps, Δ2) →
+  ElimInv φ N P Ps P' Q Q' →
+  φ →
+  envs_app false (Esnoc Enil j P') Δ2 = Some Δ3 →
+  envs_entails Δ3 Q' → envs_entails Δ1 Q.
+Proof.
+  rewrite envs_entails_eq => ???? HΔ. rewrite envs_lookup_delete_list_sound //.
+  rewrite envs_app_singleton_sound //=.
+  rewrite HΔ //= affinely_persistently_if_elim //=.
+  rewrite -sep_assoc. by eapply elim_inv.
+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.
@@ -214,6 +215,14 @@ Tactic Notation "iAssumption" :=
            |fail "iAssumption:" Q "not found"]
   end.
 
+Tactic Notation "iAssumptionListCore" :=
+  repeat match goal with
+  | |- envs_lookup_delete_list _ ?ils ?p = Some (_, ?P :: ?Ps, _) =>
+    eapply envs_lookup_delete_list_cons; [by iAssumptionCore |]
+  | |- envs_lookup_delete_list _ ?ils ?p = Some (_, [], _) =>
+    eapply envs_lookup_delete_list_nil
+  end.
+
 (** * False *)
 Tactic Notation "iExFalso" := apply tac_ex_falso.
 
@@ -1864,6 +1873,80 @@ 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).
 
+Tactic Notation "iAssumptionInv" constr(N) :=
+  let rec find Γ i P :=
+    lazymatch Γ with
+    | Esnoc ?Γ ?j ?P' =>
+      first [assert (IntoInv P' N) by apply _; unify P P'; unify i j|find Γ i P]
+    end in
+  match goal with
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+     first [is_evar i; fail 1 | env_reflexivity]
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
+  end.
+
+Tactic Notation "iInvCore" constr(N) "with" constr(Hs) "as" tactic(tac) constr(Hclose) :=
+  let hd_id := fresh "hd_id" in evar (hd_id: ident);
+  let hd_id := eval unfold hd_id in hd_id in
+  let Htmp1 := iFresh in
+  let Htmp2 := iFresh in
+  let patback := intro_pat.parse_one Hclose in
+  eapply tac_inv_elim with _ _ (hd_id :: Hs) Htmp1 _ _ N _  _ _ _;
+  first eapply envs_lookup_delete_list_cons; swap 2 3;
+    [ iAssumptionInv N || fail "iInv: invariant" N "not found"
+    | apply _ ||
+     let I := match goal with |- ElimInv _ ?N ?I  _ _ _ _ => I end in
+     fail "iInv: cannot eliminate invariant " I " with namespace " N
+    | iAssumptionListCore || fail "iInv: other assumptions not found"
+    | try (split_and?; solve [ fast_done | solve_ndisj ])
+    | env_reflexivity |];
+  let pat := constr:(IList [[IIdent Htmp2; patback]]) in
+  iDestruct Htmp1 as pat;
+  tac Htmp2.
+
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+  let tl_ids := fresh "tl_ids" in evar (tl_ids: list ident);
+  let tl_ids := eval unfold tl_ids in tl_ids in
+  iInvCore N with tl_ids as (fun H => tac H) Hclose.
+Tactic Notation "iInvCoreParse" constr(N) "with" constr(Hs) "as" tactic(tac) constr(Hclose) :=
+  let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
+  iInvCore N with Hs as (fun H => tac H) 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) :=
+   iInvCoreParse 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) :=
+   iInvCoreParse 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) :=
+   iInvCoreParse 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) :=
+   iInvCoreParse 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) :=
+   iInvCoreParse 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,89 @@ Section iris_tests.
     iApply ("H" with "[% //] [$] [> HQ] [> //]").
     by iApply inv_alloc.
   Qed.
+
+  Lemma test_iInv_1 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_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 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.
 End iris_tests.