diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean
index 9a7f514bd..5274a61fa 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/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean
index 9492c94b2..0e413ae7c 100644
--- a/Iris/Iris/HeapLang/ProofMode.lean
+++ b/Iris/Iris/HeapLang/ProofMode.lean
@@ -230,7 +230,7 @@ public meta def iWpValueHead {u}
   let p' : Q(Bool) ← mkFreshExprMVarQ q(Bool)
   let A' : Q(IProp $GF) ← mkFreshExprMVarQ q(IProp $GF)
   let Q' : Q(IProp $GF) ← mkFreshExprMVarQ q(IProp $GF)
-  if let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $c false $p' iprop(|={$E}=> $goal) $A' $goal $Q') then
+  if let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $c false .out $p' iprop(|={$E}=> $goal) $A' $goal $Q') then
     if let some _ ← try? <| iSolveSidecondition c then
       let pf ← addBIGoal hyps q($goal)
       return some q(tac_wp_value_nofupd (s:=$s) (E:=$E) $pf)
diff --git a/Iris/Iris/Instances/Lib/CInvariants.lean b/Iris/Iris/Instances/Lib/CInvariants.lean
index 8bfff93ba..cf318cca5 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/FUpd.lean b/Iris/Iris/Instances/Lib/FUpd.lean
index 9fcc8dab9..599c96c08 100644
--- a/Iris/Iris/Instances/Lib/FUpd.lean
+++ b/Iris/Iris/Instances/Lib/FUpd.lean
@@ -379,8 +379,8 @@ instance isExcept0_fupd_finally (E : CoPset) (P : IProp GF) : IsExcept0 iprop(|=
     iapply except0_mono fupd_intro $$ H
 
 @[rocq_alias elim_modal_bupd_fupd_finally]
-instance elimModal_bupd_fupd_finally p (E : CoPset) (P Q : IProp GF) :
-    ElimModal True p false iprop(|==> P) P iprop(|={E|}=> Q) iprop(|={E|}=> Q) where
+instance elimModal_bupd_fupd_finally p io (E : CoPset) (P Q : IProp GF) :
+    ElimModal True p io false iprop(|==> P) P iprop(|={E|}=> Q) iprop(|={E|}=> Q) where
   elim_modal _ := by
     iintro ⟨H1, H2⟩
     iapply fupd_fupd_finally E E
@@ -390,8 +390,8 @@ instance elimModal_bupd_fupd_finally p (E : CoPset) (P Q : IProp GF) :
     iapply H2 $$ H1
 
 @[rocq_alias elim_modal_fupd_fupd_finally]
-instance elimModal_fupd_fupd_finally p (E1 E2 : CoPset) (P Q : IProp GF) :
-    ElimModal True p false iprop(|={E1,E2}=> P) P iprop(|={E1|}=> Q) iprop(|={E2|}=> Q) where
+instance elimModal_fupd_fupd_finally p io (E1 E2 : CoPset) (P Q : IProp GF) :
+    ElimModal True p io false iprop(|={E1,E2}=> P) P iprop(|={E1|}=> Q) iprop(|={E2|}=> Q) where
   elim_modal _ := by
     iintro ⟨H1, H2⟩
     iapply fupd_fupd_finally E1 E2
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/LaterCredits.lean b/Iris/Iris/Instances/Lib/LaterCredits.lean
index 0bf9dc67d..f915d6a71 100644
--- a/Iris/Iris/Instances/Lib/LaterCredits.lean
+++ b/Iris/Iris/Instances/Lib/LaterCredits.lean
@@ -429,7 +429,7 @@ open ProofMode
 variable {GF : BundledGFunctors} {hlc : HasLC} [LcGS hlc GF]
 
 @[rocq_alias le_upd.elim_bupd_le_upd]
-instance {P : IProp GF} : ElimModal True p false (bupd P) P (le_upd Q) (le_upd Q) where
+instance {P Q : IProp GF} : ElimModal True p io false (bupd P) P (le_upd Q) (le_upd Q) where
   elim_modal := by
     cases p <;> (dsimp; intro _)
     · iintro ⟨H1, H2⟩
@@ -466,7 +466,7 @@ instance {P : IProp GF} : FromModal True modality_id (le_upd P) (le_upd P) P whe
     iapply le_upd_intro
 
 @[rocq_alias le_upd.elim_modal_le_upd]
-instance {P : IProp GF} : ElimModal True p false (le_upd P) P (le_upd Q) (le_upd Q) where
+instance {P Q : IProp GF} : ElimModal True p io false (le_upd P) P (le_upd Q) (le_upd Q) where
   elim_modal := by
     intro _
     cases p <;> dsimp
diff --git a/Iris/Iris/Instances/Lib/NaInvariants.lean b/Iris/Iris/Instances/Lib/NaInvariants.lean
index 293eecf58..1fcbe0f2c 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 CoPsetDisjL) (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 958c75c39..05cd7c3e0 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
 
@@ -638,7 +639,7 @@ instance isExcept0Wp : IsExcept0 (WP e @ s ; E {{ Φ }}) where
 -- this should have higher priority than elimModalFupdWpAtomic
 @[rocq_alias elim_modal_fupd_wp]
 instance (priority := default + 10) elimModalFupdWp p :
-    ElimModal True p false iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
+    ElimModal True p io false iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
   elim_modal := by
     iintro %_ ⟨H, G⟩
     icases BI.intuitionisticallyIf_elim $$ H with H
@@ -648,11 +649,11 @@ instance (priority := default + 10) elimModalFupdWp p :
 
 @[rocq_alias elim_modal_bupd_wp]
 instance elimModalBupdWp p :
-    ElimModal True p false iprop(|==> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
+    ElimModal True p io false iprop(|==> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where
   elim_modal := by
     rintro ⟨⟩
     refine BI.sep_mono (BI.intuitionisticallyIf_mono (BIUpdateFUpdate.fupd_of_bupd (E := E))) .rfl |>.trans ?_
-    apply elimModalFupdWp _ |>.elim_modal ⟨⟩
+    exact elimModalFupdWp _ |>.elim_modal ⟨⟩ (io := io)
 
 /-- Error message instance for non-mask-changing view shifts.  Also uses a slightly
 different error: we cannot apply `fupd_mask_subseteq` if `e` is not atomic, so
@@ -661,12 +662,12 @@ we tell the user to first add a leading `fupd` and then change the mask of that.
 instance elimModalFupdWp_wrongMask :
     ElimModal (PMError "Goal and eliminated modality must have the same mask.
     Use `iapply fupd_wp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`")
-    p false iprop(|={E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
+    p io false iprop(|={E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
   elim_modal := nofun
 
 @[rocq_alias elim_modal_fupd_wp_atomic]
 instance elimModalFupdWpAtomic :
-    ElimModal (Language.Atomic ↑s e) p false iprop(|={E₁,E₂}=> P) P (WP e @ s ; E₁ {{ Φ }}) (WP e @ s ; E₂ {{ v, |={E₂,E₁}=> Φ v}}) where
+    ElimModal (Language.Atomic ↑s e) p io false iprop(|={E₁,E₂}=> P) P (WP e @ s ; E₁ {{ Φ }}) (WP e @ s ; E₂ {{ v, |={E₂,E₁}=> Φ v}}) where
   elim_modal := by
     rintro atomic; iintro ⟨H, G⟩
     icases BI.intuitionisticallyIf_elim $$ H with H
@@ -678,7 +679,43 @@ instance elimModalFupdWpAtomic :
 instance elimModalFupdWpAtomic_wrongMask :
     ElimModal (PMError "Goal and eliminated modality must have the same mask.
     Use `iapply fupd_wp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`")
-    p false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
+    p io 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 a6227a704..0c7e1e952 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
 
@@ -205,8 +206,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) (io : InOut)
+    (p' : semiOutParamIPM io Bool) (P : PROP)
+    (P' : semiOutParamIPM io PROP) (Q : PROP) (Q' : outParam $ PROP) where
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
 export ElimModal (elim_modal)
 
@@ -249,6 +251,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)
+
 /-
   `IntoIH φ P Q` describes how to turn a pure induction hypothesis `φ` into a proofmode
   hypothesis `Q` under an intuitionistic BI context `□ P`.
diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index 8e0293403..bea4de162 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -184,6 +184,20 @@ partial def Hyps.find? {u prop bi} (name : Name) :
   | _, .hyp _ name' ivar _ ty _ => if name == name' then (ivar, ty) else none
   | _, .sep _ _ _ _ lhs rhs => rhs.find? name <|> lhs.find? name
 
+partial def Hyps.findM? [Monad m] {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Name → IVarId → Q(Bool) → Q($prop) → m Bool) :
+    ∀ {e}, Hyps bi e → m (Option (Name × IVarId × Q(Bool) × Q($prop)))
+  | _, .emp _ => return none
+  | _, .hyp _ name ivar bp ty _ => do
+    if ← p name ivar bp ty then
+      return some (name, ivar, bp, ty)
+    else
+      return none
+  | _, .sep _ _ _ _ lhs rhs => do
+    match ← rhs.findM? p with
+    | some res => return some res
+    | none => lhs.findM? p
+
 partial def Hyps.getDecl? {u prop bi} (ivar : IVarId) {s}:
     @Hyps u prop bi s → Option (Name × IVarId × Q(Bool) × Q($prop))
   | .emp _ => none
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 0bff74e2a..01b5693be 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
 
@@ -12,6 +12,8 @@ public import Iris.ProofMode.ModalityInstances
 public import Iris.ProofMode.Expr
 public import Iris.Std.TC
 public import Iris.Std.RocqPorting
+public import Iris.ProofMode.Tactics
+public import Iris.ProofMode.Display
 
 @[expose] public section
 
@@ -53,6 +55,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) io : 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"
@@ -86,6 +94,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]
@@ -841,21 +856,29 @@ instance fromModal_absorbingly [BI PROP] (P : PROP) :
 
 -- ElimModal
 @[rocq_alias elim_modal_wand]
-instance elimModal_wand [BI PROP] φ p p' (P P' Q Q' R : PROP) [h : ElimModal φ p p' P P' Q Q'] :
-   ElimModal φ p p' P P' iprop(R -∗ Q) iprop(R -∗ Q') where
+instance elimModal_wand [BI PROP] φ p p' io (P P' Q Q' R : PROP) [h : ElimModal φ p io p' P P' Q Q'] :
+   ElimModal φ p io p' P P' iprop(R -∗ Q) iprop(R -∗ Q') where
    elim_modal hφ := by
      apply wand_intro ((sep_assoc.1.trans $ sep_mono_right $ wand_elim $ wand_intro_left $
        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' io (P P' Q Q' : PROP) (mR : Option PROP)
+    [h : ElimModal φ p io p' P P' Q Q'] :
+    ElimModal φ p io 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' io 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
+instance elimModal_forall [BI PROP] φ p p' io P P' (Φ Ψ : α → PROP) [h : ∀ x, ElimModal φ p io p' P P' (Φ x) (Ψ x)] :
+  ElimModal φ p io p' P P' iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
   elim_modal hφ := forall_intro λ a => Entails.trans (sep_mono_right (wand_mono_right (forall_elim a))) ((h a).1 hφ)
 
 @[rocq_alias elim_modal_absorbingly_here]
-instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] :
-  ElimModal True p false iprop(<absorb> P) P Q Q where
+instance elimModal_absorbingly_here [BI PROP] p io (P Q : PROP) [Absorbing Q] :
+  ElimModal True p io false iprop(<absorb> P) P Q Q where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans $ absorbingly_sep_left.1.trans $ absorbing_absorbingly.1.trans wand_elim_right
 
 -- CombineSepAs
@@ -921,6 +944,42 @@ instance combineSepGives_persistently [BI PROP] (Q1 Q2 P : PROP)
     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 .in 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, hϕ2⟩
+    have hAcc := h1.into_acc
+    unfold accessor at hAcc
+    iintro ⟨Hinv, Hin, Hcont⟩
+    iapply (h2 _ |>.elim_modal hϕ2)
+    isplitl [Hinv Hin]
+    · dsimp
+      iapply hAcc hϕ1 $$ Hinv Hin
+    · dsimp
+      iintro ⟨%_, Hα, Hclose⟩
+      iapply Hcont
+      isplitl [Hα] <;> iassumption
+
 @[rocq_alias into_ih_entails]
 instance intoIH_entails [BI PROP] (P Q : PROP) : IntoIH (Entails' P Q) P Q where
   into_ih := λ hpq => intuitionistically_elim.trans hpq
diff --git a/Iris/Iris/ProofMode/InstancesLater.lean b/Iris/Iris/ProofMode/InstancesLater.lean
index 596881c7c..2d80151e8 100644
--- a/Iris/Iris/ProofMode/InstancesLater.lean
+++ b/Iris/Iris/ProofMode/InstancesLater.lean
@@ -314,8 +314,8 @@ instance intoExcept0_persistently [BI PROP] (P Q : PROP)
 
 /-- ElimModal -/
 @[ipm_backtrack, rocq_alias elim_modal_timeless]
-instance (priority := default - 10) elimModal_timeless [BI PROP] p (P P' Q : PROP) [IntoExcept0 P P'] [IsExcept0 Q] :
-  ElimModal True p p P P' Q Q where
+instance (priority := default - 10) elimModal_timeless [BI PROP] p io (P P' Q : PROP) [IntoExcept0 P P'] [IsExcept0 Q] :
+  ElimModal True p io p P P' Q Q where
   elim_modal _ := ((sep_mono ((intuitionisticallyIf_mono into_except0).trans except0_intuitionisticallyIf) except0_intro).trans $ except0_sep.2.trans (except0_mono wand_elim_right)).trans is_except0
 
 /-- IntoLaterN -/
diff --git a/Iris/Iris/ProofMode/InstancesUpdates.lean b/Iris/Iris/ProofMode/InstancesUpdates.lean
index 30edff808..34786e4ad 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
 
@@ -83,8 +86,8 @@ instance fromModal_bupd (P : PROP) :
   from_modal := by simp [modality_id]; exact BIUpdate.intro
 
 @[rocq_alias elim_modal_bupd]
-instance elimModal_bupd p (P Q : PROP) :
-    ElimModal True p false iprop(|==> P) P iprop(|==> Q) iprop(|==> Q) where
+instance elimModal_bupd p io (P Q : PROP) :
+    ElimModal True p io false iprop(|==> P) P iprop(|==> Q) iprop(|==> Q) where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans <|
     bupd_frame_right.trans <| (BIUpdate.mono wand_elim_right).trans BIUpdate.trans
 
@@ -95,14 +98,14 @@ section SBIBasicUpdate
 variable {PROP} [Sbi PROP] [BIUpdate PROP] [BIBUpdateSbi PROP]
 
 @[ipm_backtrack, rocq_alias elim_modal_bupd_plain_goal]
-instance elimModal_bupd_plain_goal [BIAffine PROP] p (P Q : PROP) [Plain Q] :
-    ElimModal True p false iprop(|==> P) P Q Q where
+instance elimModal_bupd_plain_goal [BIAffine PROP] p io (P Q : PROP) [Plain Q] :
+    ElimModal True p io false iprop(|==> P) P Q Q where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans <|
     bupd_frame_right.trans <| (BIUpdate.mono wand_elim_right).trans bupd_elim
 
 @[ipm_backtrack, rocq_alias elim_modal_bupd_plain]
-instance elimModal_bupd_plain [BIAffine PROP] p (P Q : PROP) [Plain P] :
-    ElimModal True p p iprop(|==> P) P Q Q where
+instance elimModal_bupd_plain [BIAffine PROP] p io (P Q : PROP) [Plain P] :
+    ElimModal True p io p iprop(|==> P) P Q Q where
   elim_modal _ := (sep_mono_left (intuitionisticallyIf_mono bupd_elim)).trans wand_elim_right
 
 end SBIBasicUpdate
@@ -181,25 +184,69 @@ instance (priority := low) fromModal_fupd_wrongMask E1 E2 (P : PROP) :
   from_modal h := by cases h
 
 @[rocq_alias elim_modal_bupd_fupd]
-instance elimModal_bupd_fupd p E1 E2 (P Q : PROP) :
-    ElimModal True p false iprop(|==> P) P iprop(|={E1,E2}=> Q) iprop(|={E1,E2}=> Q) where
+instance elimModal_bupd_fupd p io E1 E2 (P Q : PROP) :
+    ElimModal True p io false iprop(|==> P) P iprop(|={E1,E2}=> Q) iprop(|={E1,E2}=> Q) where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans <|
     (sep_mono_left BIUpdateFUpdate.fupd_of_bupd).trans <|
     fupd_frame_right.trans <| (BIFUpdate.mono wand_elim_right).trans BIFUpdate.trans
 
 @[rocq_alias elim_modal_fupd_fupd]
-instance (priority := high) elimModal_fupd_fupd p E1 E2 E3 (P Q : PROP) :
-    ElimModal True p false iprop(|={E1,E2}=> P) P iprop(|={E1,E3}=> Q) iprop(|={E2,E3}=> Q) where
+instance (priority := high) elimModal_fupd_fupd p io E1 E2 E3 (P Q : PROP) :
+    ElimModal True p io false iprop(|={E1,E2}=> P) P iprop(|={E1,E3}=> Q) iprop(|={E2,E3}=> Q) where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans <|
     fupd_frame_right.trans <| (BIFUpdate.mono wand_elim_right).trans BIFUpdate.trans
 
 @[rocq_alias elim_modal_fupd_fupd_wrong_mask]
-instance (priority := low) elimModal_fupd_fupd_wrongMask p E0 E1 E2 E3 (P Q : PROP) :
+instance (priority := low) elimModal_fupd_fupd_wrongMask p io E0 E1 E2 E3 (P Q : PROP) :
     ElimModal (PMError "Goal and eliminated modality must have the same mask.
       Use `BIFUpdate.subset` to adjust the goal mask before using `imod`.")
-      p false iprop(|={E1,E2}=> P) iprop(False) iprop(|={E0,E3}=> Q) iprop(False) where
+      p io 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 af37f1737..f0e038d52 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" ported "iaccu"
 #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial"
 
diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index db5829cc2..274bacd90 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/Iris/Iris/ProofMode/Tactics.lean
@@ -16,6 +16,7 @@ public meta import Iris.ProofMode.Tactics.Frame
 public meta import Iris.ProofMode.Tactics.Have
 public meta import Iris.ProofMode.Tactics.Induction
 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 0797c1396..4b6a20b1d 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 | first | trivial | (simp [*] <;> done))) 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 2c1fae59f..1ded13245 100644
--- a/Iris/Iris/ProofMode/Tactics/Cases.lean
+++ b/Iris/Iris/ProofMode/Tactics/Cases.lean
@@ -47,12 +47,15 @@ theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
     (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q :=
   (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}
+theorem intuitionistic_elim_spatial [BI PROP] {A A' P Q : PROP}
     [IntoPersistently false A A'] [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 :=
+  have : IntoPersistently false iprop(□ A) A' :=
+    ⟨persistently_of_intuitionistically.trans inst.into_persistently⟩
+  intuitionistic_elim_spatial (A := iprop(□ A)) h
 
 theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p]
     (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q :=
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..13f55a57d
--- /dev/null
+++ b/Iris/Iris/ProofMode/Tactics/Inv.lean
@@ -0,0 +1,159 @@
+/-
+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 …`).
+-/
+private def reduceWandM (e : Expr) : ProofModeM Expr := do
+  let simpThms ← #[``BIBase.wandM, ``Option.getD].foldlM (·.addDeclToUnfold ·) {}
+  let simpContext ← Simp.mkContext {} #[simpThms] (← getSimpCongrTheorems)
+  Lean.Meta.dsimp e simpContext <&> 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 := ⟨⟩
+
+  let hϕ ← iSolveSidecondition (failOnUnsolved := false) q($ϕ)
+
+  -- Simplify occurrences of `wandM`, `Option.getD`, pattern matching, etc.
+  let Pout' : Q($X → $prop) ← reduceWandM Pout
+  let Q'' : Q($X → $prop) ← reduceWandM 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) ← reduceWandM f
+    let pf : Q(∀ x, $e'' ∗ $Pout x ∗ $f x ⊢ $Q' x) ←
+      withLocalDeclDQ (← mkFreshUserName .anonymous) X fun x => do
+        match closePat with
+        | some closePat =>
+          let pf' ← iCasesCore _ hyps'' q($Q'' $x) (.conjunction [casesPat, closePat])
+            q(false) q(iprop($Pout' $x ∗ $f' $x))
+          mkLambdaFVars #[x] pf'
+        -- 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
+        let pf' ← iCasesCore _ hyps'' q($Q'' $x) casesPat q(false) q($Pout' $x)
+        mkLambdaFVars #[x] pf'
+    return q(tac_inv_elim $inst $hϕ $pf $pfEq $pfPin)
+
+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.
+
+  `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`.
+
+  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)
+        let some (_, ivar, _, _) ← hyps.findM? fun _ _ _ ty =>
+            return (← ProofModeM.trySynthInstanceQ q(IntoInv $ty $N)).isSome
+          | throwError m!"iinv: invariant hypothesis with the namespace {N} not found"
+        pure ivar
+
+      let pf ← iInvCore hyps goal ivar specPat casesPat closePat
+      mvar.assign pf
diff --git a/Iris/Iris/ProofMode/Tactics/Mod.lean b/Iris/Iris/ProofMode/Tactics/Mod.lean
index df7caf352..46c9c3b85 100644
--- a/Iris/Iris/ProofMode/Tactics/Mod.lean
+++ b/Iris/Iris/ProofMode/Tactics/Mod.lean
@@ -14,7 +14,7 @@ namespace Iris.ProofMode
 public section
 open BI
 
-theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q']
+theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p .out p' A A' Q Q']
   (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q :=
     (sep_comm.1.trans (sep_mono_right (wand_intro h1))).trans (he.1 hΦ)
 
@@ -41,7 +41,7 @@ def iModCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q : Q($prop)) (p : Q(Bool
     let A' : Q($prop) ← mkFreshExprMVarQ q($prop)
     let Q' : Q($prop) ← mkFreshExprMVarQ q($prop)
     -- transform `Q` to `Q'` and `A` to `A'`
-    let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $Φ $p $p' $A $A' $Q $Q')
+    let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $Φ $p .out $p' $A $A' $Q $Q')
       | throwError "imod: {A} is not a modality"
     let hΦ ← iSolveSidecondition q($Φ)
     let p'' : Q(Bool) ← instantiateMVars p'
diff --git a/Iris/Iris/ProofMode/Tactics/Pure.lean b/Iris/Iris/ProofMode/Tactics/Pure.lean
index 6901ce5a2..690d78f1e 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
@@ -26,7 +25,8 @@ 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 :=
+    [inst : IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q :=
+  have : IntoPure iprop(□ A) φ := ⟨intuitionistically_elim.trans inst.into_pure⟩
   pure_elim_spatial h h'
 
 public meta section
@@ -51,7 +51,7 @@ def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop))
     | .inr _ =>
       let .some _ ← 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 (A := $A) $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 f1d3a547b..b40d2ef45 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. -/
 
@@ -2918,6 +2923,175 @@ example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n)
 
 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
+
 section ieval
 
 /-- Tests `ieval` and `isimp` to simplify the goal and specific Iris hypotheses. -/
diff --git a/Iris/tactics.md b/Iris/tactics.md
index 2761762dc..9967f2e95 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -76,6 +76,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).