diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean
index ae7c216dd..91a9753cd 100644
--- a/Iris/Iris/BI/BIBase.lean
+++ b/Iris/Iris/BI/BIBase.lean
@@ -54,6 +54,8 @@ syntax "⌜" term "⌝" : term
 syntax:35 term:36 " ∗ " term:35 : term
 /-- Separating implication. -/
 syntax:25 term:26 " -∗ " term:25 : term
+/-- Separating implication with an optional wand premise. -/
+syntax:25 term:26 " -∗? " term:25 : term
 /-- Persistency modality. `persistently` is a primitive of BI. -/
 syntax:max "<pers> " term:40 : term
 /-- Later modality. `later` is a primitive of BI. -/
@@ -163,6 +165,18 @@ delab_rule iff
 delab_rule wandIff
   | `($_ $P $Q) => do ``(iprop($(← unpackIprop P) ∗-∗ $(← unpackIprop Q)))
 
+@[simp, rocq_alias bi_wandM]
+def wandM [BIBase PROP] (mP : Option PROP) (Q : PROP) : PROP :=
+  match mP with
+  | none => Q
+  | some P => iprop(P -∗ Q)
+
+macro_rules
+  | `(iprop($mP -∗? $Q)) => ``(wandM $mP iprop($Q))
+
+delab_rule wandM
+  | `($_ $mP $Q) => do ``(iprop($mP -∗? $(← unpackIprop Q)))
+
 /-- Affine modality.
 ```
 def affinely (P) := emp ∧ P
diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
index 2e71ef58c..e4efb8eea 100644
--- a/Iris/Iris/BI/DerivedLaws.lean
+++ b/Iris/Iris/BI/DerivedLaws.lean
@@ -1041,6 +1041,12 @@ theorem emp_or [BI PROP] {P : PROP} [Affine P] : emp ∨ P ⊣⊢ emp := ⟨or_e
 theorem emp_wand [BI PROP] {P : PROP} : (emp -∗ P) ⊣⊢ P :=
   ⟨emp_sep.mpr.trans wand_elim_right, wand_intro_left emp_sep.mp⟩
 
+@[rocq_alias bi.wandM_sound]
+theorem wandM_sound [BI PROP] {mP : Option PROP} {Q : PROP} :
+    (mP -∗? Q) ⊣⊢ (mP.getD emp -∗ Q) := by
+  cases mP <;> simp [BIBase.wandM]
+  exact emp_wand.symm
+
 @[rocq_alias bi.or_emp]
 theorem or_emp [BI PROP] {P : PROP} [Affine P] : P ∨ emp ⊣⊢ emp := or_comm.trans emp_or
 
diff --git a/Iris/Iris/Instances/Lib/CInvariants.lean b/Iris/Iris/Instances/Lib/CInvariants.lean
index ff321c0a5..547d7dea1 100644
--- a/Iris/Iris/Instances/Lib/CInvariants.lean
+++ b/Iris/Iris/Instances/Lib/CInvariants.lean
@@ -20,7 +20,7 @@ public import Iris.Std.List
 
 namespace Iris
 
-open BI CMRA OFE Iris Std LawfulSet Excl COFE
+open BI CMRA OFE Iris Std LawfulSet Excl COFE ProofMode
 
 /-! # Cancelable Invariants -/
 
@@ -289,6 +289,27 @@ theorem cancel (E : CoPset) (N : Namespace) (γ : GName) (P : IProp GF) (Hsub :
   imodintro
   iexact HP
 
+@[rocq_alias into_inv_cinv]
+instance intoInv_cinv (N : Namespace) (γ : GName) (P : IProp GF) :
+    IntoInv (cinv N γ P) N := {}
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_acc_cinv]
+instance intoAcc_cinv (E : CoPset) (N : Namespace) (γ : GName) (P : IProp GF) (p : Qp) :
+    IntoAcc (X := Unit) (cinv N γ P) (↑N ⊆ E) (own γ p) (fupd E (E \ ↑N)) (fupd (E \ ↑N) E)
+      (fun _ => iprop(▷ P ∗ own γ p)) (fun _ => iprop(▷ P)) (λ _ => none) where
+  into_acc := by
+    dsimp only [accessor, Option.getD]
+    iintro %x #Hinv Hown
+    imod acc x $$ Hinv Hown with ⟨HP, Hγ, Hcl⟩
+    imodintro
+    iexists ()
+    isplitl [HP Hγ]
+    · iframe
+    · iintro HP
+      iapply (BIFUpdate.mono true_emp.mp)
+      iapply Hcl $$ HP
+
 end CancelableInvariant
 end Iris
 end
diff --git a/Iris/Iris/Instances/Lib/Invariants.lean b/Iris/Iris/Instances/Lib/Invariants.lean
index 66c14409a..ebdecdf5b 100644
--- a/Iris/Iris/Instances/Lib/Invariants.lean
+++ b/Iris/Iris/Instances/Lib/Invariants.lean
@@ -87,7 +87,26 @@ theorem except_0_inv (N : Namespace) (P : IProp GF) : ⊢ ◇ inv N P -∗ inv N
 instance is_except_0_inv (N : Namespace) (P : IProp GF) : IsExcept0 (inv N P) where
   is_except0 := by iintro H; iapply except_0_inv $$ H
 
--- TODO: into_inv_inv, into_acc_inv
+@[rocq_alias into_inv_inv]
+instance intoInv_inv (N : Namespace) (P : IProp GF) : IntoInv (inv N P) N := {}
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_acc_inv]
+instance intoAcc_inv (N : Namespace) (P : IProp GF) E :
+    IntoAcc (X := Unit) (inv N P) (↑N ⊆ E) iprop(True) (fupd E (E \ ↑N)) (fupd (E \ ↑N) E)
+      (λ _ => iprop(▷ P)) (λ _ => iprop(▷ P)) (λ _ => none) where
+  into_acc := by
+    dsimp only [inv, accessor, Option.getD]
+    iintro %x #Hinv -
+    imod Hinv $$ %E [] with ⟨HP, Hclose⟩
+    · itrivial
+    · iexists ()
+      imodintro
+      isplitl [HP]
+      · iassumption
+      · iintro HP
+        iapply (BIFUpdate.mono true_emp.mp)
+        iapply Hclose $$ HP
 
 end Instances
 
diff --git a/Iris/Iris/Instances/Lib/NaInvariants.lean b/Iris/Iris/Instances/Lib/NaInvariants.lean
index 67d437076..c58eec68d 100644
--- a/Iris/Iris/Instances/Lib/NaInvariants.lean
+++ b/Iris/Iris/Instances/Lib/NaInvariants.lean
@@ -17,7 +17,7 @@ public import Iris.Std.CoPset
 
 namespace Iris
 
-open BI CMRA OFE Iris Std LawfulSet DisjointLeibnizSet COFE
+open BI CMRA OFE Iris Std LawfulSet DisjointLeibnizSet COFE ProofMode
 
 abbrev NaInvF : OFunctorPre :=
   ProdOF (constOF (DisjointLeibnizSet CoPset)) (constOF (DisjointLeibnizSet PosSet))
@@ -221,6 +221,24 @@ nonrec theorem inv_acc {p : NaInvPoolName} {E F : CoPset} {N : Namespace} {P : I
     icases Hbad with %Hbad
     exact Hbad i ⟨mem_singleton.mpr rfl, mem_singleton.mpr rfl⟩ |>.elim
 
+@[rocq_alias into_inv_na]
+instance intoInv_na (N : Namespace) (P : IProp GF) :
+    IntoInv (inv p N P) N := {}
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_acc_na]
+instance intoAcc_na (p : NaInvPoolName) (E F : CoPset) (N : Namespace) (P : IProp GF) :
+    IntoAcc (X := Unit) (inv p N P) (↑N ⊆ E ∧ ↑N ⊆ F) (own p F) (fupd E E) (fupd E E)
+    (fun _ => iprop(▷ P ∗ own p (F \ ↑N))) (fun _ => iprop(▷ P ∗ own p (F \ ↑N)))
+              (λ _ => some (own p F)) where
+  into_acc := by
+    dsimp only [accessor, Option.getD]
+    intro ⟨hE, hF⟩
+    iintro #Hinv Hown
+    imod inv_acc hE hF $$ Hinv Hown with ⟨_, Hown, _⟩
+    iexists ()
+    iframe
+
 end NonAtomicInvariant
 end Iris
 end
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index 896ca484a..36fe1f326 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -8,13 +8,14 @@ public import Iris.Algebra
 public import Iris.Instances.Lib.FUpd
 public import Iris.BI
 public import Iris.BI.WeakestPre
+public import Iris.BI.DerivedLaws
 public import Iris.ProofMode
 public import Iris.ProgramLogic.Language
 public import Iris.Std.CoPset
 
 namespace Iris
 
-open ProgramLogic Language.Notation Std
+open ProgramLogic Language.Notation Std Iris.BI
 
 @[expose] public section
 
@@ -681,4 +682,40 @@ instance elimModalFupdWpAtomic_wrongMask :
     p false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
   elim_modal := nofun
 
+@[rocq_alias elim_acc_wp_atomic]
+instance (priority := low) elimAcc_wp_atomic {X} (E₁ E₂ : CoPset) α β (γ : X → Option (IProp GF)) :
+    ElimAcc (Language.Atomic ↑s e) (fupd E₁ E₂) (fupd E₂ E₁) α β γ
+      (WP e @ s ; E₁ {{ Φ }})
+      (fun x => WP e @ s ; E₂ {{ v, |={E₂}=> β x ∗ (γ x -∗? Φ v) }}) where
+  elim_acc := by
+    dsimp only [accessor, BIBase.wandM, Option.getD]
+    iintro %atomic Hinner >⟨%x, Hα, Hclose⟩
+    iapply wp_wand $$ [Hinner Hα]
+    · iapply Hinner $$ Hα
+    · iintro %v >⟨Hβ, HΦ⟩
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      imodintro
+      cases (γ x) with
+      | none => iexact HΦ
+      | some P => iapply HΦ $$ Hclose
+
+@[rocq_alias elim_acc_wp_nonatomic]
+instance elimAcc_wp_nonatomic {X} E (α β : X → IProp GF) (γ : X → Option (IProp GF)) :
+    ElimAcc True (fupd E E) (fupd E E) α β γ (WP e @ s ; E {{ Φ }})
+    (fun x => WP e @ s ; E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }}) where
+  elim_acc := by
+    dsimp only [accessor, BIBase.wandM, Option.getD]
+    iintro %_ Hinner >⟨%x, Hα, Hclose⟩
+    iapply wp_fupd
+    iapply wp_wand $$ [Hinner Hα]
+    · iapply Hinner $$ Hα
+    · iintro %v >⟨Hβ, HΦ⟩
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      imodintro
+      cases (γ x) with
+      | none => iexact HΦ
+      | some P => iapply HΦ $$ Hclose
+
 end ProofModeClasses
diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index ac2ca161b..3e1fea0a9 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -8,6 +8,7 @@ module
 public import Iris.BI
 public meta import Iris.ProofMode.SynthInstance
 public import Iris.ProofMode.Modalities
+public import Iris.Std.Namespaces
 
 @[expose] public section
 
@@ -180,8 +181,9 @@ export FromModal (from_modal)
 
 /-- `ElimModal` turns `□?p P` into `□?p' P'` and `Q` into `Q'` under condition `φ`. -/
 @[ipm_class, rocq_alias ElimModal]
-class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outParam $ Bool) (P : PROP)
-    (P' : outParam $ PROP) (Q : PROP) (Q' : outParam $ PROP) where
+class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool)
+    (p' : outParam $ uncheckedInParam Bool) (P : PROP)
+    (P' : outParam $ uncheckedInParam PROP) (Q : PROP) (Q' : outParam $ PROP) where
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
 export ElimModal (elim_modal)
 
@@ -224,6 +226,38 @@ class CombineSepGives [BI PROP] (P Q : PROP) (R : outParam PROP) where
   combine_sep_gives : P ∗ Q ⊢ <pers> R
 export CombineSepGives (combine_sep_gives)
 
+@[ipm_class, rocq_alias IntoInv]
+class IntoInv [BI PROP] (P : PROP) (N : Namespace)
+
+@[rocq_alias accessor]
+def accessor [BI PROP] {X : Type} (M1 M2 : PROP → PROP) (α β : X → PROP)
+    (mγ : X → Option  PROP) : PROP :=
+  M1 iprop(∃ x, α x ∗ (β x -∗ M2 (mγ x |>.getD emp)))
+
+@[ipm_class, rocq_alias ElimAcc]
+class ElimAcc [BI PROP] {X : Type} (ϕ : outParam Prop) (M1 M2 : PROP → PROP)
+    (α β : X → PROP) (mγ : X → Option PROP) (Q : PROP) (Q' : outParam <| X → PROP) where
+  elim_acc : ϕ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q)
+
+@[ipm_class, rocq_alias IntoAcc]
+class IntoAcc [BI PROP] {X : outParam Type} (Pacc : PROP)
+    (ϕ : outParam Prop) (Pin : outParam <| PROP)
+    (M1 M2 : outParam <| PROP → PROP) (α β : outParam <| X → PROP)
+    (mγ : outParam <| X → Option PROP) where
+  into_acc : ϕ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ
+
+set_option synthInstance.checkSynthOrder false in
+/-- The type class used for the `iinv` tactic. -/
+@[ipm_class, rocq_alias ElimInv]
+class ElimInv [BI PROP] (φ : outParam Prop) (X : outParam Type)
+    (Pinv : PROP) (Pin : outParam PROP) (Pout : outParam <| X → PROP)
+    (close : Bool) (mPclose : outParam <| Option <| X → PROP)
+    (Q : PROP) (Q' : outParam <| X → PROP) where
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, (match mPclose with
+    | some Pclose => iprop(Pout x ∗ Pclose x -∗ Q' x)
+    | none => iprop(Pout x -∗ Q' x))) ⊢ Q
+export ElimInv (elim_inv)
+
 #rocq_ignore elim_inv_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore elim_modal_tc_opaque "No tc_opaque in Lean"
 #rocq_ignore from_and_tc_opaque "No tc_opaque in Lean"
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 8ebc6aa25..4063f46ad 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Mario Carneiro, Alvin Tang
+Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang
 -/
 module
 
@@ -10,6 +10,8 @@ public import Iris.ProofMode.Classes
 public import Iris.ProofMode.ModalityInstances
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
+public import Iris.ProofMode.Tactics
+public import Iris.ProofMode.Display
 
 @[expose] public section
 
@@ -51,6 +53,12 @@ instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 :
 @[rocq_alias from_wand_wand]
 instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩
 
+-- FromWandM
+@[rocq_alias from_wand_wandM]
+instance fromWand_wandM [BI PROP] (mP1 : Option PROP) (P2 : PROP) :
+    FromWand iprop(mP1 -∗? P2) io (mP1.getD emp) P2 where
+  from_wand := wandM_sound.mpr
+
 -- IntoWand
 #rocq_ignore into_wand_wand' "IntoWand' is not used in Lean"
 #rocq_ignore into_wand_impl' "IntoWand' is not used in Lean"
@@ -84,6 +92,13 @@ instance intoWand_and_r (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
 instance intoWand_wandIff (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
     [h : IntoWand p q iprop((R1 -∗ R2) ∧ (R2 -∗ R1)) ioP P' ioQ Q'] : IntoWand p q iprop(R1 ∗-∗ R2) ioP P' ioQ Q' := h
 
+@[rocq_alias into_wand_wandM]
+instance intoWand_wandM (p q : Bool) [BI PROP] (mP' : Option PROP) (P Q : PROP)
+    [h : FromAssumption q ioP P (mP'.getD emp)] :
+    IntoWand p q iprop(mP' -∗? Q) ioP P ioQ Q where
+  into_wand := (intuitionisticallyIf_mono wandM_sound.mp).trans <|
+    (intuitionisticallyIf_mono <| wand_mono_left h.1).trans intuitionisticallyIf_elim
+
 -- The set_option is ok since this is an instance for an IPM class and thus can create mvars.
 set_option synthInstance.checkSynthOrder false in
 @[rocq_alias into_wand_forall]
@@ -846,6 +861,14 @@ instance elimModal_wand [BI PROP] φ p p' (P P' Q Q' R : PROP) [h : ElimModal φ
        wand_intro_left $ sep_assoc.2.trans _).trans (h.1 hφ))
      apply (sep_mono_left sep_comm.1).trans (sep_assoc.1.trans $ wand_elim_swap $ wand_elim_swap .rfl)
 
+@[rocq_alias elim_modal_wandM]
+instance elimModal_wandM [BI PROP] φ p p' (P P' Q Q' : PROP) (mR : Option PROP)
+    [h : ElimModal φ p p' P P' Q Q'] :
+    ElimModal φ p p' P P' iprop(mR -∗? Q) iprop(mR -∗? Q') where
+  elim_modal hφ :=
+    (sep_mono_right <| wand_mono_right wandM_sound.mp).trans <|
+    ((elimModal_wand φ p p' P P' Q Q' (mR.getD emp)).elim_modal hφ).trans wandM_sound.mpr
+
 @[rocq_alias elim_modal_forall]
 instance elimModal_forall [BI PROP] φ p p' P P' (Φ Ψ : α → PROP) [h : ∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)] :
   ElimModal φ p p' P P' iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
@@ -918,3 +941,34 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     [h : CombineSepGives Q1 Q2 P] :
     CombineSepGives iprop(<pers> Q1) iprop(<pers> Q2) iprop(<pers> P) where
   combine_sep_gives := persistently_sep_mpr.trans (persistently_mono h.combine_sep_gives)
+
+@[rocq_alias elim_inv_acc_without_close]
+instance elimInv_acc_without_close [BI PROP] {X : Type}
+    ϕ1 ϕ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : X → PROP)
+    [h1 : IntoAcc Pinv ϕ1 Pin M1 M2 α β mγ]
+    [h2 : ElimAcc ϕ2 M1 M2 α β mγ Q Q'] :
+    ElimInv (ϕ1 ∧ ϕ2) X Pinv Pin α false none Q Q' where
+  elim_inv := by
+    intro ⟨hϕ1, _⟩
+    iintro ⟨Hinv, Hin, Hcont⟩
+    iapply h2.elim_acc $$ [Hcont]
+    · assumption
+    · iassumption
+    · iapply h1.into_acc hϕ1 $$ Hinv Hin
+
+@[rocq_alias elim_inv_acc_with_close]
+instance elimInv_acc_with_close [BI PROP] {X : Type}
+    ϕ1 ϕ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : PROP)
+    [h1 : IntoAcc Pinv ϕ1 Pin M1 M2 α β mγ]
+    [h2 : ∀ R, ElimModal ϕ2 false false (M1 R) R Q Q'] :
+    ElimInv (ϕ1 ∧ ϕ2) X Pinv Pin α true
+            (some (fun x => iprop(β x -∗ M2 (mγ x |>.getD emp))))
+            Q (fun _ => Q') where
+  elim_inv := by
+    intro ⟨hϕ1, _⟩
+    have hAcc := h1.into_acc
+    unfold accessor at hAcc
+    iintro ⟨Hinv, Hin, Hcont⟩
+    imod hAcc hϕ1 $$ Hinv Hin with ⟨%_, Hα, Hclose⟩
+    iapply Hcont
+    isplitl [Hα] <;> iassumption
diff --git a/Iris/Iris/ProofMode/InstancesUpdates.lean b/Iris/Iris/ProofMode/InstancesUpdates.lean
index 30edff808..cc9f41a48 100644
--- a/Iris/Iris/ProofMode/InstancesUpdates.lean
+++ b/Iris/Iris/ProofMode/InstancesUpdates.lean
@@ -1,13 +1,16 @@
 /-
 Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler, Yunsong Yang
+Authors: Michael Sammler, Yunsong Yang, Alvin Tang
 -/
 module
 
 public import Iris.BI
 public import Iris.ProofMode.Classes
+public import Iris.ProofMode.Instances
 public import Iris.Std.TC
+public import Iris.ProofMode.Tactics
+public import Iris.ProofMode.Display
 
 @[expose] public section
 
@@ -200,6 +203,50 @@ instance (priority := low) elimModal_fupd_fupd_wrongMask p E0 E1 E2 E3 (P Q : PR
       p false iprop(|={E1,E2}=> P) iprop(False) iprop(|={E0,E3}=> Q) iprop(False) where
   elim_modal h := by cases h
 
+@[rocq_alias elim_acc_bupd]
+instance elimAcc_bupd {X} (α β : X → PROP) mγ (Q : PROP) :
+    ElimAcc True bupd bupd α β mγ
+    iprop(|==> Q)
+    iprop(fun x => (|==> β x ∗ (mγ x -∗? |==> Q))) where
+  elim_acc := by
+    simp only [accessor, BIBase.wandM]
+    iintro %_ Hinner >⟨%x, Hα, Hclose⟩
+    ispecialize Hinner $$ %x Hα
+    cases (mγ x) with simp_all
+    | none =>
+      icases Hinner with ⟨Hβ, Hfin⟩
+      imod Hβ
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      iexact Hfin
+    | some P =>
+      icases Hinner with ⟨Hβ, Hfin⟩
+      imod Hβ
+      imod Hclose $$ Hβ
+      iapply Hfin
+      iexact Hclose
+
+@[rocq_alias elim_acc_fupd]
+instance elimAcc_fupd {X} E1 E2 E (α β : X → PROP) mγ (Q : PROP) :
+    ElimAcc True (fupd E1 E2) (fupd E2 E1) α β mγ
+    iprop(|={E1,E}=> Q)
+    (fun x => iprop(|={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))) where
+  elim_acc := by
+    simp only [accessor, BIBase.wandM]
+    iintro %_ Hinner >⟨%x, Hα, Hclose⟩
+    ispecialize Hinner $$ %x Hα
+    cases (mγ x) with simp_all
+    | none =>
+      imod Hinner with ⟨Hβ, Hfin⟩
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      iexact Hfin
+    | some p =>
+      imod Hinner with ⟨Hβ, Hfin⟩
+      ispecialize Hclose $$ Hβ
+      imod Hclose
+      iapply Hfin $$ Hclose
+
 end BIFancyUpdate
 
 section SBIFancyUpdate
diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..9ad782cfb 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/Iris/Iris/ProofMode/Porting.lean
@@ -55,7 +55,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iLöb" ported "iloeb"
 #rocq_concept proofmode "Tactics" "iAssert" ported "ihave _ : _"
 #rocq_concept proofmode "Tactics" "iRewrite" ported "irewrite"
-#rocq_concept proofmode "Tactics" "iInv" missing ""
+#rocq_concept proofmode "Tactics" "iInv" ported "iinv"
 #rocq_concept proofmode "Tactics" "iAccu" missing ""
 #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial"
 
diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index 361255881..20ecb0267 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/Iris/Iris/ProofMode/Tactics.lean
@@ -13,6 +13,7 @@ public meta import Iris.ProofMode.Tactics.Exists
 public meta import Iris.ProofMode.Tactics.Frame
 public meta import Iris.ProofMode.Tactics.Have
 public meta import Iris.ProofMode.Tactics.Intro
+public meta import Iris.ProofMode.Tactics.Inv
 public meta import Iris.ProofMode.Tactics.LeftRight
 public meta import Iris.ProofMode.Tactics.Loeb
 public meta import Iris.ProofMode.Tactics.Mod
diff --git a/Iris/Iris/ProofMode/Tactics/Basic.lean b/Iris/Iris/ProofMode/Tactics/Basic.lean
index ce79fb78d..3e0403459 100644
--- a/Iris/Iris/ProofMode/Tactics/Basic.lean
+++ b/Iris/Iris/ProofMode/Tactics/Basic.lean
@@ -29,10 +29,12 @@ def iSolveSidecondition (target : Q(Prop)) (failOnUnsolved := true) : ProofModeM
   | .app (.const ``PMError _) (.lit (.strVal msg)) =>
       throwError "{msg}"
   | _ =>
-      let gs ← evalTacticAt (← `(tactic | trivial)) mvar.mvarId!
+      let gs ← (observing? <|
+        evalTacticAt (← `(tactic | and_intros <;> first | trivial | simp_all)) mvar.mvarId!) <&>
+        (·.getD [mvar.mvarId!])
       if !gs.isEmpty then
         if failOnUnsolved then
-          throwError "isolvesidecondition: failed to solve sidecondition {target}"
+          throwError "iSolveSidecondition: failed to solve side condition {target}"
         else
           for g in gs do addMVarGoal g
       return mvar
diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean
index 9f5ec3854..f6c0467f0 100644
--- a/Iris/Iris/ProofMode/Tactics/Cases.lean
+++ b/Iris/Iris/ProofMode/Tactics/Cases.lean
@@ -48,11 +48,13 @@ theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
   (sep_mono_right <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_left.1.trans <| or_elim h1 h2
 
 theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP}
-    [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)]
+    (instPers: IntoPersistently false A A') (instAffineAbsorbing: TCOr (Affine A) (Absorbing Q))
     (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h
 
-theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A']
-    (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h
+theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} (inst : IntoPersistently true A A')
+    (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q :=
+  let instAffine := @TCOr.l (Affine iprop(□ A)) (Absorbing Q) ⟨(intuitionistically_affine A).affine⟩
+  intuitionistic_elim_spatial ⟨persistently_of_intuitionistically.trans inst.into_persistently⟩ instAffine h
 
 theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p]
     (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q :=
@@ -154,15 +156,15 @@ private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop))
     (k : (B : Q($prop)) → ProofModeM Q($P ∗ □ $B ⊢ $goal)) :
     ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let B ← mkFreshExprMVarQ q($prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A $B)
+  let .some instPers ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A $B)
     | throwError "icases: {A} not persistent"
   match matchBool p with
   | .inl _ =>
-    return q(intuitionistic_elim_intuitionistic $(← k B))
+    return q(intuitionistic_elim_intuitionistic $instPers $(← k B))
   | .inr _ =>
-    let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $goal))
+    let .some instAffineAbsorbing ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $goal))
       | throwError "icases: {A} not affine and the goal not absorbing"
-    return q(intuitionistic_elim_spatial (A := $A) $(← k B))
+    return q(intuitionistic_elim_spatial $instPers $instAffineAbsorbing $(← k B))
 
 /--
 Destruct an affine/spatial hypothesis [A] by removing the affinely wrapper and continuing with
diff --git a/Iris/Iris/ProofMode/Tactics/Frame.lean b/Iris/Iris/ProofMode/Tactics/Frame.lean
index af5be77c3..8204cfe0f 100644
--- a/Iris/Iris/ProofMode/Tactics/Frame.lean
+++ b/Iris/Iris/ProofMode/Tactics/Frame.lean
@@ -117,9 +117,7 @@ def FrameResult.finish {u prop bi origE origGoal} (res : @FrameResult u prop bi
   back with the remaining hypotheses. -/
 def FrameResult.finishClose {u prop bi origE origGoal} (res : @FrameResult u prop bi origE origGoal) :
   ProofModeM ((e : Q($prop)) × (_ : Hyps bi e) × Q($origE ⊢ $e ∗ $origGoal)) := do
-  let {progress, e, hyps, goal, pf} := res
-  if !progress then
-    throwError "iframe: cannot solve {origGoal} by framing"
+  let {e, hyps, goal, pf, ..} := res
   -- try closing the goal for emp or True without calling k
   match goal with
   | ~q(iprop(emp)) =>
diff --git a/Iris/Iris/ProofMode/Tactics/Inv.lean b/Iris/Iris/ProofMode/Tactics/Inv.lean
new file mode 100644
index 000000000..c6aff333b
--- /dev/null
+++ b/Iris/Iris/ProofMode/Tactics/Inv.lean
@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, Alvin Tang
+-/
+module
+
+public meta import Iris.ProofMode.Tactics.Assumption
+public meta import Iris.ProofMode.Tactics.Cases
+public meta import Iris.ProofMode.Tactics.Intro
+public meta import Iris.ProofMode.Patterns.CasesPattern
+public meta import Iris.ProofMode.Patterns.IntroPattern
+public meta import Iris.ProofMode.Patterns.SelPattern
+public meta import Iris.ProofMode.ClassesMake
+
+namespace Iris.ProofMode
+
+public section
+open BI
+
+@[rocq_alias tac_inv_elim]
+theorem tac_inv_elim [BI PROP]
+    {e e' e'' goal : PROP} {ϕ : Prop} {X : Type} {p close : Bool}
+    {Pinv Pin : PROP} {mPclose : Option <| X → PROP} {Pout Q' : X → PROP}
+    (inst : ElimInv ϕ X Pinv Pin Pout close mPclose goal Q')
+    (hϕ : ϕ)
+    (pf : match mPclose with
+      | none => ∀ x, e'' ∗ Pout x ⊢ Q' x
+      | some Pclose => ∀ x, e'' ∗ Pout x ∗ Pclose x ⊢ Q' x)
+    (pfEq : e ⊣⊢ e' ∗ □?p Pinv)
+    (pfPin : e' ∗ (Pin -∗ Pin) ⊢ e'' ∗ Pin) :
+    e ⊢ goal := by
+  have h0 := inst.elim_inv
+  have h1 : e ⊢ Pinv ∗ Pin ∗ e'' := calc
+    e ⊢ e' ∗ □?p Pinv            := pfEq.mp
+    _ ⊢ □?p Pinv ∗ e'            := sep_comm.mp
+    _ ⊢ Pinv ∗ e'                := sep_mono_left intuitionisticallyIf_elim
+    _ ⊢ Pinv ∗ e' ∗ emp          := sep_mono_right sep_emp.mpr
+    _ ⊢ Pinv ∗ e' ∗ (Pin -∗ Pin) := sep_mono_right <| sep_mono_right wand_rfl
+    _ ⊢ Pinv ∗ e'' ∗ Pin         := sep_mono_right pfPin
+    _ ⊢ Pinv ∗ Pin ∗ e''         := sep_mono_right sep_comm.mp
+  cases mPclose with simp_all
+  | none => calc
+    e ⊢ Pinv ∗ Pin ∗ e'' := h1
+    _ ⊢ _ := sep_mono_right <| sep_mono_right <| forall_intro (wand_intro <| pf ·)
+    _ ⊢ goal := h0
+  | some Pclose => calc
+    e ⊢ Pinv ∗ Pin ∗ e'' := h1
+    _ ⊢ _ := sep_mono_right <| sep_mono_right <| forall_intro (wand_intro <| pf ·)
+    _ ⊢ goal := h0
+
+public meta section
+open Lean Elab Tactic Meta Qq BI Std
+
+/--
+  An annotation of `wandM` with `@[reducible]` is useful when `whnf` is called,
+  but `whnf` is not strong enough to simplify occurrences of `wandM` in the
+  proof goal. This funnction is similar to `pm_reduce` in the Rocq version,
+  which forces the reduction of `wandM` (`-∗?`), occurrences of `Option.getD`
+  and pattern matching (`match … with …`).
+-/
+def pmReduce (e : Expr) : ProofModeM Expr := do
+  #[``BIBase.wandM, ``Option.getD].foldlM (·.addDeclToUnfold ·) {} >>=
+  (Simp.mkContext {} #[·] (← getSimpCongrTheorems) >>= (Lean.Meta.dsimp e · <&> Prod.fst))
+
+private def iInvCore {u} {prop : Q(Type u)} {bi} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (ivar : IVarId) (specPat : Option SpecPat)
+    (casesPat : iCasesPat) (closePat : Option iCasesPat) :
+    ProofModeM Q($e ⊢ $goal) := do
+  -- Find the hypothesis from the context
+  let ⟨_, hyps', _, Pinv, _, _, pfEq⟩ := hyps.remove false ivar
+
+  let ϕ ← mkFreshExprMVarQ q(Prop)
+  let Pin : Q($prop) ← mkFreshExprMVarQ q($prop)
+  let X : Q(Type) ← mkFreshExprMVarQ q(Type)
+  let Pout ← mkFreshExprMVarQ q($X → $prop)
+  -- Decide whether to use `elimInv_acc_with_close` or `elimInv_acc_without_close`
+  let close := if closePat.isSome then q(true) else q(false)
+  let mPclose ← mkFreshExprMVarQ q(Option ($X → $prop))
+  let Q' ← mkFreshExprMVarQ q($X → $prop)
+  let some inst ← ProofModeM.trySynthInstanceQ q(ElimInv $ϕ $X $Pinv $Pin $Pout $close $mPclose $goal $Q')
+  | throwError "iinv: invalid invariant {Pinv} (ElimInv type class synthesis failed)"
+
+  let ⟨e'', hyps'', p'', out'', pfPin⟩ ←
+    iSpecializeCore hyps' q(false) q(iprop($Pin -∗ $Pin)) [specPat.getD <| .autoframe .spatial]
+  have : $out'' =Q $Pin := ⟨⟩
+  have : $p'' =Q false := ⟨⟩
+
+  -- Solve side conditions automatically if possible, otherwise add them into the proof state
+  let hϕ ← iSolveSidecondition q($ϕ) false
+
+  -- Simplify occurrences of `wandM`, `Option.getD`, pattern matching, etc.
+  let Pout' : Q($X → $prop) ← pmReduce Pout
+  let Q'' : Q($X → $prop) ← pmReduce Q'
+
+  -- Add the new goal into the proof state upon applying the case destruction patterns
+  match mPclose with
+  | ~q(some $f) =>
+    let f' : Q($X → $prop) ← pmReduce f
+    let pf : Q(∀ x, $e'' ∗ $Pout x ∗ $f x ⊢ $Q' x) ←
+      withLocalDeclDQ (← mkFreshUserName .anonymous) X fun x => do
+        match closePat with
+        | some closePat =>
+          iCasesCore _ hyps'' q($Q'' $x) (.conjunction [casesPat, closePat])
+            q(false) q(iprop($Pout' $x ∗ $f' $x)) >>=
+          (mkLambdaFVars #[x] ·)
+        -- Throw an error if `hclose` is not given, but `mPclose` is not `none`
+        | none => throwError "iinv: missing cases pattern for the closing hypothesis"
+    return q(tac_inv_elim $inst $hϕ $pf $pfEq $pfPin)
+  | ~q(none) =>
+    let pf : Q(∀ x, $e'' ∗ $Pout x ⊢ $Q' x) ←
+      withLocalDeclDQ (← mkFreshUserName .anonymous) X fun x => do
+        iCasesCore _ hyps'' q($Q'' $x) casesPat q(false) q($Pout' $x) >>=
+        (mkLambdaFVars #[x] ·)
+    return q(tac_inv_elim $inst $hϕ $pf $pfEq $pfPin)
+
+/-- Given a `Namespace` value, find a corresponding invariant hypothesis. -/
+private def findInvariantWithNamespace {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (N : Q(Namespace)) (hyps : Hyps bi e) : ProofModeM <| Option IVarId := do
+  match hyps with
+  | .emp _ => return none
+  | .hyp _ _ ivar _ ty _ =>
+    return (← ProofModeM.trySynthInstanceQ q(IntoInv $ty $N)) <&> (fun _ => ivar)
+  | .sep _ _ _ _ lhs rhs =>
+    return (← findInvariantWithNamespace N rhs) <|> (← findInvariantWithNamespace N lhs)
+
+syntax (name := iinv) "iinv " colGt term (" $$ " colGt ppSpace specPat)?
+    " with " colGt icasesPat (colGt icasesPat)? : tactic
+
+/--
+  `iinv H with casesPat` opens an invariant hypothesis `H` and uses the
+  cases pattern `casesPat` to destruct the result without any additional
+  hypothesis for closing the invariant. The type class
+  `elimInv_acc_without_close` is used with this tactic.
+
+  `iinv H with casesPat closePat` opens an invariant hypothesis `H`,
+  uses the cases pattern `casesPat` to destruct the result and generates a
+  hypothesis for closing the invariant, which is destructed by the cases
+  pattern `closePat`. The type class `elimInv_acc_with_close` is used with
+  this tactic.
+
+  Furthermore, the following syntax is available.
+  - `iinv N with casesPat`: similar to `iinv H with casesPat`, where
+    an invariant with the namespace `N` is opened.
+  - `iinv H $$ specPat with casesPat`: similar to `iinv H with casesPat`,
+    with a specialisation pattern `specPat` for resource consumption needed
+    to open the invariant. Without `specPat`, the specialisation pattern is
+    by default the auto-framing of spatial hypotheses.
+-/
+elab_rules : tactic
+  | `(tactic| iinv $t:term $[$$ $spat:specPat]? with $casesPat:icasesPat $[$closePat:icasesPat]?) => do
+    -- Parse the introduction and selection patterns
+    let specPat ← liftMacroM <| spat.mapM SpecPat.parse
+    let casesPat ← liftMacroM <| iCasesPat.parse casesPat
+    let closePat ← liftMacroM <| closePat.mapM iCasesPat.parse
+
+    ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+      -- Find the invariant hypothesis
+      let ivar ← do match ← try? <| hyps.findWithInfo ⟨t⟩ with
+      -- Hypothesis supplied by the user: return the `IVarId` value of the invariant directly
+      | some ivar => pure ivar
+      -- Namespace supplied by the user: use `IntoInv` to find the corresponding hypothesis
+      | none =>
+        let N ← elabTermEnsuringTypeQ t q(Namespace)
+        match ← findInvariantWithNamespace N hyps with
+        | some ivar => pure ivar
+        | none => throwError m!"iinv: invariant hypothesis with the namespace {N} not found"
+
+      let pf ← iInvCore hyps goal ivar specPat casesPat closePat
+      mvar.assign pf
diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean
index 6901ce5a2..295572803 100644
--- a/Iris/Iris/ProofMode/Tactics/Pure.lean
+++ b/Iris/Iris/ProofMode/Tactics/Pure.lean
@@ -5,7 +5,6 @@ Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
 module
 
-public import Iris.ProofMode.Instances
 public meta import Iris.ProofMode.Tactics.Basic
 
 namespace Iris.ProofMode
@@ -14,7 +13,7 @@ public section
 open BI Std
 
 theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
-    [hA : IntoPure A φ] [or : TCOr (Affine A) (Absorbing Q)]
+    (hA : IntoPure A φ) (or : TCOr (Affine A) (Absorbing Q))
     (h : P ⊣⊢ P' ∗ A) (h_entails : φ → P' ⊢ Q) : P ⊢ Q :=
   h.1.trans <| match or with
   | TCOr.l =>
@@ -26,8 +25,9 @@ theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop}
     pure_elim_right fun hφ => (absorbingly_mono <| h_entails hφ).trans absorbing
 
 theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
-    [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q :=
-  pure_elim_spatial h h'
+    (instIntoPure : IntoPure A φ) (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q :=
+  have instAffine := @TCOr.l (Affine iprop(□ A)) (Absorbing Q) ⟨(intuitionistically_affine A).affine⟩
+  pure_elim_spatial ⟨intuitionistically_elim.trans instIntoPure.into_pure⟩ instAffine h h'
 
 public meta section
 open Lean Elab Tactic Meta Qq
@@ -36,7 +36,7 @@ def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
     (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A))
     (k : (φ : Q(Prop)) → Q($φ) → ProofModeM (Q($P' ⊢ $Q))) : ProofModeM (Q($P ⊢ $Q)) := do
   let φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ)
+  let .some instIntoPure ← ProofModeM.trySynthInstanceQ q(IntoPure $A $φ)
     | throwError "ipure: {A} is not pure"
 
   let (name, ref) ← getFreshName name
@@ -47,11 +47,11 @@ def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
 
     match matchBool p with
     | .inl _ =>
-      return (q(pure_elim_intuitionistic $pf $f))
+      return (q(pure_elim_intuitionistic $instIntoPure $pf $f))
     | .inr _ =>
-      let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
+      let .some instAffineAbsorbing ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
         | throwError "ipure: {A} is not affine and the goal not absorbing"
-      return q(pure_elim_spatial (A:=$A) $pf $f)
+      return q(pure_elim_spatial $instIntoPure $instAffineAbsorbing $pf $f)
 
 /--
   `ipure H` moves a pure hypothesis `H` from the Iris context into the regular
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..26ec0b84a 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -11,11 +11,16 @@ public import Iris.Instances.IProp
 public import Iris.Instances.Lib.LaterCredits
 public import Iris.Instances.Lib.Token
 public import Iris.Algebra.CMRA
+public import Iris.Instances.Lib.Invariants
+public import Iris.Instances.Lib.CInvariants
+public import Iris.Instances.Lib.NaInvariants
+public import Iris.ProgramLogic.Language
+public import Iris.ProgramLogic.WeakestPre
 
 @[expose] public section
 
 namespace Iris.Tests
-open BI CMRA DFrac
+open BI CMRA DFrac CancelableInvariant NonAtomicInvariant ProgramLogic
 
 /- This file contains tests with various scenarios for all available tactics. -/
 
@@ -2776,3 +2781,172 @@ example (P Q : PROP) :
   iloeb as IH
 
 end iloeb
+
+section iinv
+
+variable {hlc : HasLC} {GF : BundledGFunctors} [InvGS_gen hlc GF] {N : Namespace}
+
+/--
+  Tests `iinv` with `elimInv_acc_without_close`, `elimAcc_fupd` and
+  `intoAcc_inv` where the side condition is trivial.
+-/
+example {P : IProp GF} : inv N iprop(<pers> P) ={⊤}=∗ ▷ P := by
+  iintro #Hinv
+  iinv Hinv with #H
+  imodintro
+  isplit
+  · iexact H
+  · imodintro
+    inext
+    iexact H
+
+/--
+  Tests `iinv` with `elimInv_acc_with_close`, `elimModal_fupd_fupd` and
+  `intoAcc_inv` where the side condition is trivial.
+-/
+example {P : IProp GF} : inv N iprop(<pers> P) ={⊤}=∗ ▷ P := by
+  iintro #Hinv
+  iinv Hinv with #H Hclose
+  imod Hclose $$ H
+  imodintro
+  inext
+  iexact H
+
+/--
+  Tests `iinv` with `elimInv_acc_without_close`, `elimAcc_fupd` and
+  `intoAcc_inv`, relying on the side condition `↑N ⊆ E`.
+-/
+example {E} {P : IProp GF} {h : ↑N ⊆ E} : inv N iprop(<pers> P) ={E}=∗ ▷ P := by
+  iintro #Hinv
+  iinv Hinv with #H
+  imodintro
+  isplit
+  · iexact H
+  · imodintro
+    inext
+    iexact H
+
+/- Tests `iinv` with an invalid invariant. -/
+/-- error: iinv: invalid invariant P (ElimInv type class synthesis failed) -/
+#guard_msgs in
+example {E : CoPset} {P : IProp GF} : □ P ={E}=∗ ▷ P := by
+  iintro #HP
+  iinv HP with #H
+
+/-- Tests `iinv` with `elimInv_acc_without_close`, `elimAcc_fupd` and `intoAcc_cinv`. -/
+example [CInvG GF]  {γ : GName} {p : Qp} :
+    cinv N γ iprop(<pers> P) ∗ own γ p ⊢@{IProp GF} |={⊤}=> own γ p ∗ ▷ P := by
+  iintro ⟨#Hinv, H⟩
+  iinv Hinv with ⟨#HP, Hown⟩
+  imodintro
+  isplit
+  iexact HP
+  iframe
+  imodintro
+  inext
+  iexact HP
+
+/-- Tests `iinv` with `elimInv_acc_with_close`, `elimModal_fupd_fupd` and `intoAcc_cinv`. -/
+example [CInvG GF] {γ : GName} {p : Qp} :
+    cinv N γ iprop(<pers> P) ∗ own γ p ⊢@{IProp GF} |={⊤}=> own γ p ∗ ▷ P := by
+  iintro ⟨#Hinv, H⟩
+  iinv Hinv with ⟨#HP, Hown⟩ Hclose
+  imod Hclose $$ HP
+  imodintro
+  iframe
+  inext
+  iexact HP
+
+/--
+  Tests `iinv` with `elimInv_acc_without_close`, `elimAcc_fupd`,
+  `intoAcc_cinv` and a specialisation pattern. -/
+example [CInvG GF] {γ : GName} {p1 p2 : Qp} {P : IProp GF} :
+    cinv N γ iprop(<pers> P) ∗ own γ p1 ∗ own γ p2
+    ⊢@{IProp GF} |={⊤}=> own γ p1 ∗ own γ p2 ∗ ▷ P := by
+  iintro ⟨#Hinv, Hown1, Hown2⟩
+  iinv Hinv $$ [Hown2 //] with ⟨#HP, Hown2⟩
+  imodintro
+  iframe HP ∗
+  imodintro
+  inext
+  iexact HP
+
+/-- Tests `iinv` with `elimInv_acc_with_close`, `elimModal_fupd_fupd` and `intoAcc_na`. -/
+example {t : NaInvPoolName} [NaInvG GF] {E1 E2 : CoPset} {P : IProp GF} (h : ↑N ⊆ E1) :
+    NonAtomicInvariant.inv t N iprop(<pers> P) ∗ own t E1 ∗ own t E2
+    ={⊤}=∗ own t E1 ∗ own t E2 ∗ ▷ P := by
+  iintro ⟨#Hinv, Hown1, Hown2⟩
+  iinv Hinv $$ [Hown1 //] with ⟨#HP, Hown1⟩ Hclose
+  imod Hclose $$ [HP Hown1]
+  · iframe
+    iexact HP
+  · iframe
+    imodintro
+    inext
+    iexact HP
+
+/-- Tests the robustness of `iinv` in presence of other invariants. -/
+example {t : NaInvPoolName} [NaInvG GF] {N1 N2 N3 : Namespace} {E1 E2 : CoPset}
+    {P : IProp GF} (h : ↑N3 ⊆ E1) :
+    inv N1 P ∗ NonAtomicInvariant.inv t N3 iprop(<pers> P) ∗ inv N2 P ∗ own t E1 ∗ own t E2
+    ={⊤}=∗ own t E1 ∗ own t E2 ∗ ▷ P := by
+  iintro ⟨#_, #Hinv, #_, Hown1, Hown2⟩
+  iinv Hinv $$ Hown1 with ⟨#HP, Hown1⟩
+  imodintro
+  isplitl [Hown1]
+  · iframe HP ∗
+  · iintro Hown1
+    iframe
+    imodintro
+    inext
+    iexact HP
+
+/--
+  Tests `iinv` with two invariant hypotheses using the same `Namespace` value.
+  The last hypothesis in the context with this `Namespace` value gets chosen.
+-/
+example {t : NaInvPoolName} [NaInvG GF] {N : Namespace} {E1 E2 : CoPset}
+    {P Q : IProp GF} (h : ↑N ⊆ E1) :
+    NonAtomicInvariant.inv t N iprop(<pers> Q) ∗
+    NonAtomicInvariant.inv t N iprop(<pers> P) ∗
+    own t E1 ∗ own t E2 ={⊤}=∗ own t E1 ∗ own t E2 ∗ ▷ P := by
+  iintro ⟨#_, #_, Hown1, Hown2⟩
+  iinv N $$ Hown1 with ⟨#HP, Hown1⟩
+  imodintro
+  isplitl [Hown1]
+  · iframe HP ∗
+  · iintro Hown1
+    iframe
+    imodintro
+    inext
+    iexact HP
+
+/-
+  Tests `iinv` with a valid `Namespace` value that does not correspond to
+  any invariant hypothesis in the context.
+-/
+/-- error: iinv: invariant hypothesis with the namespace N3 not found -/
+#guard_msgs in
+example {t : NaInvPoolName} [NaInvG GF] {N1 N2 N3 : Namespace} {E1 E2 : CoPset}
+    {P Q : IProp GF} (h : ↑N1 ⊆ E1) :
+    NonAtomicInvariant.inv t N1 iprop(<pers> Q) ∗
+    NonAtomicInvariant.inv t N2 iprop(<pers> P) ∗
+    own t E1 ∗ own t E2 ={⊤}=∗ own t E1 ∗ own t E2 ∗ ▷ P := by
+  iintro ⟨#_, #_, Hown1, Hown2⟩
+  iinv N3 $$ Hown1 with ⟨#HP, Hown1⟩
+
+/- Variables to test `iinv` with `WP` -/
+variable {hlc : outParam HasLC} {Expr State Obs Val} [Λ : Language Expr State Obs Val]
+variable {GF : BundledGFunctors}
+variable [IrisGS_gen hlc Expr GF]
+variable {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ : Val → IProp GF} {P : IProp GF}
+
+/-- Tests `iinv` with `elimInv_acc_without_close`, `intoAcc_inv` and `elimAcc_wp_atomic`. -/
+example [Language.Atomic ↑s e] (h : ↑N ⊆ E) :
+    ⊢ inv N P -∗ (▷ P -∗ WP e @ s ; (E \ ↑N) {{ v, |={E \ ↑N}=> ▷ P ∗ Φ v }}) -∗ WP e @ s ; E {{ Φ }} := by
+  iintro #Hinv Hwp
+  iinv Hinv with H
+  iapply Hwp
+  iexact H
+
+end iinv
diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..fbf3ed968 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -66,6 +66,11 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `iexfalso` — Change the goal to `False`.
 - `itrivial` — Try to solve the goal with simple tactics (`iassumption`, `ipureintro` followed by `simp`/`assumption`, ...). Used by the `//` patterns. Extensible by adding `macro_rules` for `itrivial`.
 
+## Iris-Specific Tactics
+
+- `iinv` *H* (`$$` [*specPat*](#specialization-patterns))? `with` [*casesPat*](#cases-patterns) ([*casesPat*](#cases-patterns))? — opens an invariant hypothesis *H* and uses the first cases pattern to destruct the result. The second cases pattern is used for destructing the hypothesis for closing the invariant. The specialisation pattern is used for resource consumption needed for opening the invariant. If the specialisation pattern is not given as part of the tactic, it is, by default, the auto-framing of spatial hypotheses.
+- `iinv` *N* (`$$` [*specPat*](#specialization-patterns))? `with` [*casesPat*](#cases-patterns) ([*casesPat*](#cases-patterns))? — same as above, except that a namespace *N* is given. The last invariant hypothesis in the context of this namespace is chosen.
+
 ## Cases Patterns
 
 - *name* / `_` — Name the hypothesis *name* (or keep it anonymous).