From 6ed013065da355fed4c530a48b88690b6f3ae56a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 29 Jan 2026 18:58:40 +0100
Subject: [PATCH 1/5] feat: implement imodintro

---
 PORTING.md                                    |   6 +-
 src/Iris/BI/DerivedLaws.lean                  |   6 +
 src/Iris/BI/Instances.lean                    |   3 +
 src/Iris/ProofMode/Classes.lean               |   6 +
 src/Iris/ProofMode/Instances.lean             |  23 +++
 src/Iris/ProofMode/InstancesUpdates.lean      |   4 +
 src/Iris/ProofMode/Modalities.lean            |  66 ++++----
 src/Iris/ProofMode/ModalityInstances.lean     |  38 +++--
 src/Iris/ProofMode/Patterns/IntroPattern.lean |   3 +
 src/Iris/ProofMode/Tactics.lean               |   1 +
 src/Iris/ProofMode/Tactics/Basic.lean         |   5 +
 src/Iris/ProofMode/Tactics/Intro.lean         |  11 +-
 src/Iris/ProofMode/Tactics/ModIntro.lean      | 144 ++++++++++++++++++
 src/Iris/Tests/Tactics.lean                   |  74 +++++++++
 14 files changed, 339 insertions(+), 51 deletions(-)
 create mode 100644 src/Iris/ProofMode/Tactics/ModIntro.lean

diff --git a/PORTING.md b/PORTING.md
index da5be018f..59e85ad81 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -269,7 +269,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `class_instances_updates.v` (InstancesUpdates.lean)
   - [x] Basic instances for bupd
   - [ ] Basic instances for fupd
-  - [ ] FromModal bupd
+  - [x] FromModal bupd
   - [ ] FromModal fupd
   - [ ] ElimModal bupd
   - [ ] ElimModal fupd
@@ -353,7 +353,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] iRight
   - [x] iSplit(L/R)
   - [x] iExists
-  - [ ] iModIntro
+  - [x] iModIntro
   - [ ] iNext (with later credits)
   - [ ] iMod
   - [ ] iDestruct (Lean: icases)
@@ -385,7 +385,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] IModalElim
   - [ ] IRewrite
   - [ ] IPureIntro
-  - [ ] IModalIntro
+  - [x] IModalIntro
   - [ ] ISimpl
   - [ ] IDone
   - [ ] IForall
diff --git a/src/Iris/BI/DerivedLaws.lean b/src/Iris/BI/DerivedLaws.lean
index 6babd42ab..0f1dc4147 100644
--- a/src/Iris/BI/DerivedLaws.lean
+++ b/src/Iris/BI/DerivedLaws.lean
@@ -966,6 +966,9 @@ instance intuitionistically_affine [BI PROP] (P : PROP) : Affine iprop(□ P) :=
 instance intuitionistically_persistent [BI PROP] (P : PROP) : Persistent iprop(□ P) :=
   inferInstanceAs (Persistent iprop(<affine> _))
 
+instance intuitionisticallyIf_persistent [BI PROP] (P : PROP) : Persistent iprop(□?true P) :=
+  inferInstanceAs (Persistent iprop(□ _))
+
 theorem intuitionistically_def [BI PROP] {P : PROP} : iprop(□ P) = iprop(<affine> <pers> P) := rfl
 
 theorem intuitionistically_elim_emp [BI PROP] {P : PROP} : □ P ⊢ emp := affinely_elim_emp
@@ -1403,6 +1406,9 @@ theorem intuitionisticallyIf_congr {p : Bool} [BI PROP] {P Q : PROP}
     (h : P ⊣⊢ Q) : □?p P ⊣⊢ □?p Q :=
   ⟨intuitionisticallyIf_mono h.1, intuitionisticallyIf_mono h.2⟩
 
+instance (priority := default + 10) intuitionisticallyIf_true_affine [BI PROP] (P : PROP) :
+    Affine iprop(□?true P) := inferInstanceAs (Affine iprop(□ _))
+
 instance intuitionisticallyIf_affine (p : Bool) [BI PROP] (P : PROP) [Affine P] :
     Affine iprop(□?p P) := by
   cases p <;> simp [intuitionisticallyIf] <;> infer_instance
diff --git a/src/Iris/BI/Instances.lean b/src/Iris/BI/Instances.lean
index 923436c69..37e3c0620 100644
--- a/src/Iris/BI/Instances.lean
+++ b/src/Iris/BI/Instances.lean
@@ -36,3 +36,6 @@ instance sep_intuitionistic [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuition
 
 instance intuitionistically_intuitionistic [BI PROP] (P : PROP) : Intuitionistic iprop(□ P) where
   intuitionistic := intuitionistically_idem.2
+
+instance intuitionisticallyIf_true_intuitionistic [BI PROP] (P : PROP) : Intuitionistic iprop(□?true P)
+  := inferInstanceAs (Intuitionistic iprop(□ P))
diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 9b135979b..5509f4051 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -5,6 +5,7 @@ Authors: Lars König
 -/
 import Iris.BI
 import Iris.ProofMode.SynthInstance
+import Iris.ProofMode.Modalities
 
 namespace Iris.ProofMode
 open Iris.BI
@@ -147,4 +148,9 @@ class IntoExcept0 [BI PROP] (P : PROP) (Q : outParam PROP) where
   into_except0 : P ⊢ ◇ Q
 export IntoExcept0 (into_except0)
 
+@[ipm_class]
+class FromModal {PROP1 PROP2} [BI PROP1] [BI PROP2] (φ : outParam $ Prop) (M : outParam $ Modality PROP1 PROP2) (sel : semiOutParam PROP1) (P : PROP2) (Q : outParam $ PROP1) where
+  from_modal : φ → M.M Q ⊢ P
+export FromModal (from_modal)
+
 end Iris.ProofMode
diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean
index 108e310ca..dd1798f2d 100644
--- a/src/Iris/ProofMode/Instances.lean
+++ b/src/Iris/ProofMode/Instances.lean
@@ -5,6 +5,7 @@ Authors: Lars König, Mario Carneiro
 -/
 import Iris.BI
 import Iris.ProofMode.Classes
+import Iris.ProofMode.ModalityInstances
 import Iris.Std.TC
 
 namespace Iris.ProofMode
@@ -618,3 +619,25 @@ instance fromPure_absorbingly (a : Bool) [BI PROP] (P : PROP) (φ : Prop)
     [h : FromPure a P φ] : FromPure false iprop(<absorb> P) φ where
   from_pure := absorbingly_affinely_intro_of_persistent.trans <|
     absorbingly_mono <| affinely_affinelyIf.trans h.1
+
+-- FromModal
+instance (priority := default + 10) fromModal_affinely [BI PROP] (P : PROP) :
+  FromModal True modality_affinely iprop(<affine> P) iprop(<affine> P) P where
+  from_modal := by simp [modality_affinely]
+
+instance (priority := default + 10) fromModal_persistently [BI PROP] (P : PROP) :
+  FromModal True modality_persistently iprop(<pers> P) iprop(<pers> P) P where
+  from_modal := by simp [modality_persistently]
+
+instance (priority := default + 20) fromModal_intuitionistically [BI PROP] (P : PROP) :
+  FromModal True modality_intuitionistically iprop(□ P) iprop(□ P) P where
+  from_modal := by simp [modality_intuitionistically]
+
+@[ipm_backtrack]
+instance (priority := default + 30) fromModal_intuitionistically_affine_bi [BI PROP] [BIAffine PROP] (P : PROP) :
+  FromModal True modality_persistently iprop(□ P) iprop(□ P) P where
+  from_modal := by simp [modality_persistently]; apply intuitionistically_iff_persistently.2
+
+instance fromModal_absorbingly [BI PROP] (P : PROP) :
+  FromModal True modality_id iprop(<absorb> P) iprop(<absorb> P) P where
+  from_modal := by simp [modality_id]; apply absorbingly_intro
diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean
index 18c26c66e..199e780dc 100644
--- a/src/Iris/ProofMode/InstancesUpdates.lean
+++ b/src/Iris/ProofMode/InstancesUpdates.lean
@@ -57,3 +57,7 @@ instance intoForall_bupd [BIUpdate PROP] (P : PROP) (Φ : α → PROP)
 instance isExcept0_bupd [BIUpdate PROP] (P : PROP)
     [h : IsExcept0 P] : IsExcept0 iprop(|==> P) where
   is_except0 := bupd_except0.trans <| BIUpdate.mono h.1
+
+instance fromModal_bupd [BIUpdate PROP] (P : PROP) :
+    FromModal True modality_id iprop(|==> P) iprop(|==> P) P where
+  from_modal := by simp [modality_id]; exact BIUpdate.intro
diff --git a/src/Iris/ProofMode/Modalities.lean b/src/Iris/ProofMode/Modalities.lean
index e6bcaaf25..48125cf87 100644
--- a/src/Iris/ProofMode/Modalities.lean
+++ b/src/Iris/ProofMode/Modalities.lean
@@ -1,55 +1,53 @@
 /-
 Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus de Medeiros
+Authors: Markus de Medeiros, Michael Sammler
 -/
 import Iris.BI
 
 namespace Iris.ProofMode
 open Iris.BI
 
-inductive ModalityAction (PROP1 PROP2 : Type u) : Type u where
-| isEmpty   : ModalityAction PROP1 PROP2
-| forall    : PROP1 = PROP2 → (PROP1 → Prop) → ModalityAction PROP1 PROP2
-| transform : (PROP2 → PROP1 → Prop) → ModalityAction PROP1 PROP2
-| clear     : ModalityAction PROP1 PROP2
-| id        : PROP1 = PROP2 → ModalityAction PROP1 PROP2
+inductive ModalityAction (PROP1 : Type u) : Type u → Type (u + 1) where
+| isEmpty {PROP2} : ModalityAction PROP1 PROP2
+| forall : (PROP1 → Prop) → ModalityAction PROP1 PROP1
+| transform {PROP2} : (PROP2 → PROP1 → Prop) → ModalityAction PROP1 PROP2
+| clear {PROP2} : ModalityAction PROP1 PROP2
+| id : ModalityAction PROP1 PROP1
 
 namespace ModalityAction
 
-variable [BI PROP1] [BI PROP2] (s : ModalityAction PROP1 PROP2)
+variable [BI PROP1] [h2 : BI PROP2] (s : ModalityAction PROP1 PROP2)
 
 @[simp]
-def intuitionistic_action_spec (M : PROP1 → PROP2) : Prop :=
-  match s with
-  | .isEmpty => True
-  | .forall Hconv C =>
-      (∀ P, C P → iprop(□ P) ⊢ Hconv ▸ M iprop(□ P)) ∧
-      (∀ P Q, iprop(M P ∧ M Q) ⊢ M iprop(P ∧ Q))
-  | .transform C =>
-      (∀ P Q, C P Q → iprop(□ P) ⊢ M iprop(□ Q)) ∧
-      (∀ P Q, iprop(M P ∧ M Q) ⊢ M iprop(P ∧ Q))
-  | .clear => True
-  | .id H => ∀ P, iprop(□ P) ⊢ M (H ▸ iprop(□ P))
-
-@[simp]
-def spatial_action_spec (M : PROP1 → PROP2) : Prop :=
-  match s with
-  | .isEmpty => True
-  | .forall Hconv C => ∀ P, C P → P ⊢ Hconv ▸ M P
-  | .transform C => ∀ P Q, C P Q → P ⊢ M Q
-  | .clear => ∀ P, Absorbing (M P)
-  | .id Hconv => ∀ P, P ⊢ (Hconv ▸ M P)
+def action_spec (p : Bool) : (PROP1 → PROP2) → Prop :=
+  match s, h2 with
+  | .isEmpty, _ => λ _ => True
+  | .forall C, _ => λ M =>
+      (∀ P, C P → iprop(□?p P) ⊢ M iprop(□?p P))
+      -- For p = true, Iris Rocq also has the following condition, but we don't need it:
+      -- ∧ (∀ P Q, iprop(M P ∧ M Q) ⊢ M iprop(P ∧ Q))
+  | .transform C, _ => λ M =>
+      (∀ P Q, C P Q → iprop(□?p P) ⊢ M iprop(□?p Q))
+      -- For p = true, Iris Rocq also has the following condition, but we don't need it:
+      -- ∧ (∀ P Q, iprop(M P ∧ M Q) ⊢ M iprop(P ∧ Q))
+  | .clear, _ => λ M => if p then True else ∀ P, Absorbing (M P)
+  | .id, _ => λ M => ∀ P, iprop(□?p P) ⊢ M (iprop(□?p P))
 
 end ModalityAction
 
-class IsModal [BI PROP1] [BI PROP2] (M : PROP1 → PROP2)
-    (iaction saction : ModalityAction PROP1 PROP2) where
-  spec_intuitionistic : iaction.intuitionistic_action_spec M
-  spec_spatial : saction.spatial_action_spec M
+structure Modality PROP1 PROP2 [BI PROP1] [BI PROP2] where
+  M : PROP1 → PROP2
+  action : Bool → ModalityAction PROP1 PROP2
+  spec : ∀ p, (action p).action_spec p M
   emp : iprop(emp) ⊢ M iprop(emp)
   mono : ∀ {P Q}, (P ⊢ Q) → M P ⊢ M Q
   sep : ∀ {P Q}, iprop(M P ∗ M Q) ⊢ M iprop(P ∗ Q)
 
-instance [BI PROP] : IsModal (PROP1 := PROP) id (.id rfl) (.id rfl) := by
-  constructor <;> simp
+def modality_id [BI PROP] : Modality PROP PROP where
+  M := id
+  action _ := .id
+  spec := by simp
+  emp := by simp
+  mono := by simp
+  sep := by simp
diff --git a/src/Iris/ProofMode/ModalityInstances.lean b/src/Iris/ProofMode/ModalityInstances.lean
index 1aa1e9d20..33e410a4f 100644
--- a/src/Iris/ProofMode/ModalityInstances.lean
+++ b/src/Iris/ProofMode/ModalityInstances.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus de Medeiros
+Authors: Markus de Medeiros, Michael Sammler
 -/
 import Iris.BI
 import Iris.BI.DerivedLaws
@@ -14,23 +14,41 @@ section Modalities
 
 variable [BI PROP]
 
-instance : IsModal (PROP1 := PROP) persistently (.id rfl) .clear where
-  spec_intuitionistic _ := persistent
-  spec_spatial P := persistently_absorbing P
+def modality_persistently : Modality PROP PROP where
+  M := persistently
+  action
+  | true => .id
+  | false => .clear
+  spec
+  | true => λ _ => persistent
+  | false => λ P => persistently_absorbing P
   emp := persistently_emp_2
   mono := (persistently_mono ·)
   sep := persistently_sep_2
 
-instance : IsModal (PROP1 := PROP) affinely (.id rfl) (.forall rfl Affine) where
-  spec_intuitionistic _ := affinely_intro .rfl
-  spec_spatial _ _ := affinely_intro .rfl
+unif_hint [BIBase PROP] (P   : PROP) where |- iprop(□?false P) ≟ iprop(P)
+unif_hint [BIBase PROP] (P   : PROP) where |- iprop(□?true P) ≟ iprop(□ P)
+
+def modality_affinely : Modality PROP PROP where
+  M := affinely
+  action
+  | true => .id
+  | false => .forall Affine
+  spec
+  | true => λ _ => affinely_intro .rfl
+  | false => λ _ _ => affinely_intro .rfl
   emp := affinely_intro .rfl
   mono := (affinely_mono ·)
   sep := affinely_sep_2
 
-instance : IsModal (PROP1 := PROP) intuitionistically (.id rfl) .isEmpty where
-  spec_intuitionistic _ := intuitionistic
-  spec_spatial := trivial
+def modality_intuitionistically : Modality PROP PROP where
+  M := intuitionistically
+  action
+  | true => .id
+  | false => .isEmpty
+  spec
+  | true => λ _ => intuitionistic
+  | false => trivial
   emp := intuitionistic
   mono := (intuitionistically_mono ·)
   sep := intuitionistically_sep_2
diff --git a/src/Iris/ProofMode/Patterns/IntroPattern.lean b/src/Iris/ProofMode/Patterns/IntroPattern.lean
index fb43da3cd..64780e78a 100644
--- a/src/Iris/ProofMode/Patterns/IntroPattern.lean
+++ b/src/Iris/ProofMode/Patterns/IntroPattern.lean
@@ -11,12 +11,15 @@ open Lean
 declare_syntax_cat introPat
 
 syntax icasesPat : introPat
+syntax "!>" : introPat
 
 inductive IntroPat
   | intro (case : iCasesPat)
+  | modintro
   deriving Repr, Inhabited
 
 partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do
   match ← expandMacros term with
   | `(introPat| $case:icasesPat) => return (term, .intro (← iCasesPat.parse case))
+  | `(introPat| !>) => return (term, .modintro)
   | _ => Macro.throwUnsupported
diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index 7518ccc18..93aecba91 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -10,6 +10,7 @@ import Iris.ProofMode.Tactics.Exists
 import Iris.ProofMode.Tactics.Have
 import Iris.ProofMode.Tactics.Intro
 import Iris.ProofMode.Tactics.LeftRight
+import Iris.ProofMode.Tactics.ModIntro
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.Rename
 import Iris.ProofMode.Tactics.Specialize
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index cb8d7c4da..d28b88c55 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -11,6 +11,11 @@ import Iris.ProofMode.SynthInstance
 namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI Std
 
+def iSolveSideconditionAt (m : MVarId) : ProofModeM Unit := do
+  let gs ← evalTacticAt (← `(tactic | trivial)) m
+  if !gs.isEmpty then
+    throwError "isolvesidecondition: failed to solve sidecondition {← m.getType}"
+
 elab "istart" : tactic => do
   let (mvar, _) ← startProofMode (← getMainGoal)
   replaceMainGoal [mvar]
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index a59bc7718..0419d8270 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -5,6 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler
 -/
 import Iris.ProofMode.Patterns.IntroPattern
 import Iris.ProofMode.Tactics.Cases
+import Iris.ProofMode.Tactics.ModIntro
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
@@ -44,12 +45,14 @@ private theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP}
 private theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
     [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans from_wand
 
-variable {prop : Q(Type u)} (bi : Q(BI $prop)) in
-partial def iIntroCore
+partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)}
     {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) :
     ProofModeM (Q($P ⊢ $Q)) := do
   match pats with
   | [] => addBIGoal hyps Q
+  | (ref, .modintro) :: pats =>
+    withRef ref do
+    iModIntroCore hyps Q (← `(_)) (iIntroCore · · pats)
   | (ref, .intro (.pure n)) :: pats =>
     withRef ref do
     let v ← mkFreshLevelMVar
@@ -107,7 +110,7 @@ elab "iintro" pats:(colGt introPat)* : tactic => do
   -- parse syntax
   let pats ← liftMacroM <| pats.mapM <| IntroPat.parse
 
-  ProofModeM.runTactic λ mvar { bi, hyps, goal, .. } => do
-  let pf ← iIntroCore bi hyps goal pats.toList
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+  let pf ← iIntroCore hyps goal pats.toList
 
   mvar.assign pf
diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean
new file mode 100644
index 000000000..2b2e33681
--- /dev/null
+++ b/src/Iris/ProofMode/Tactics/ModIntro.lean
@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.ProofMode.Tactics.Basic
+import Iris.ProofMode.Modalities
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+/-- Reified version of ModalityAction -/
+inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where
+| isEmpty
+| forall (C : Q($PROP1 → Prop))
+| transform (C : Q($PROP2 → $PROP1 → Prop))
+| clear
+| id
+
+def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) :
+  ProofModeM (ModalityActionQ prop1 prop2) := do
+  let act ← whnf q($act)
+  match_expr act with
+  | ModalityAction.isEmpty _ _ => return .isEmpty
+  | ModalityAction.forall _ C => return .forall C
+  | ModalityAction.transform _ _ C => return .transform C
+  | ModalityAction.clear _ _ => return .clear
+  | ModalityAction.id _ => return .id
+  | _ => throwError "imodintro: unknown modality action {act}"
+
+private theorem modaction_forall [BI PROP] {p P} (M : Modality PROP PROP) {C} (h : M.action p = .forall C) (hC : C P)
+  : □?p P ⊢ M.M iprop(□?p P) := by
+    have hs := M.spec p
+    rw [h] at hs
+    apply (hs _ hC)
+
+private theorem modaction_transform [BI PROP1] [BI PROP2] {p P Q} (M : Modality PROP1 PROP2) {C} (h : M.action p = .transform C) (hC : C P Q)
+  : □?p P ⊢ M.M iprop(□?p Q) := by
+    have hs := M.spec p
+    rw [h] at hs
+    apply (hs _ _ hC)
+
+private theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1 PROP2) (h : M.action p = .clear)
+  : □?p P ⊢ M.M emp :=
+  match p, h  with
+  | true, _ => affine.trans M.emp
+  | false, h => by
+    have hs := M.spec false
+    simp [h] at hs
+    apply Entails.trans (sep_emp.2.trans (sep_mono true_intro M.emp)) absorbing
+
+private theorem modaction_id [BI PROP] {p P} (M : Modality PROP PROP) (h : M.action p = .id)
+  : □?p P ⊢ M.M iprop(□?p P) := by
+    have hs := M.spec p
+    rw [h] at hs
+    apply hs
+
+
+private theorem modaction_sep_emp_l [BI PROP1] [bi2: BI PROP2] {elhs erhs erhs'} {M : Modality PROP1 PROP2}
+  (h1 : elhs ⊢ M.M emp) (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(erhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono emp_sep.1)
+
+private theorem modaction_sep_emp_r [BI PROP1] [bi2: BI PROP2] {elhs elhs' erhs} {M : Modality PROP1 PROP2}
+  (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M emp) : elhs ∗ erhs ⊢ M.M iprop(elhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono sep_emp.1)
+
+private theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'} {M : Modality PROP1 PROP2}
+  (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(elhs' ∗ erhs') := (sep_mono h1 h2).trans M.sep
+
+
+private def iModAction {prop1 : Q(Type u)} (bi1 : Q(BI $prop1)) {e}
+  (hyps : @Hyps u prop2 bi2 e) (M : Q(Modality $prop1 $prop2)) (act : Bool → ModalityActionQ prop1 prop2) :
+  ProofModeM ((e' : _) × Hyps bi1 e' × Q($e ⊢ $(M).M $e')) :=
+  match hyps with
+  | .emp _ => return ⟨_, .mkEmp bi1, q($(M).emp)⟩
+  | .hyp _ name uniq p ty _ =>
+    let p' := isTrue p
+    match act p' with
+    | .isEmpty => throwError "imodintro: {if p' then "intuitionistic" else "spatial"} context is not empty"
+    | .forall C => do
+      have : $prop1 =Q $prop2 := ⟨⟩
+      have : $bi1 =Q $bi2 := ⟨⟩
+      let .some hC ← trySynthInstanceQ q($C $ty)
+        | throwError "imodintro: hypothesis {name} : {ty} does not satisfy {C}"
+      have heq : Q(@ModalityAction.forall $prop1 $C = .forall $C) := q(Eq.refl (ModalityAction.forall $C))
+      have heq : Q($(M).action $p = .forall $C) := heq
+      return ⟨_, .mkHyp bi1 name uniq p ty, q(modaction_forall $M $heq $hC)⟩
+    | .transform C => do
+      let ty' ← mkFreshExprMVarQ q($prop1)
+      let .some hC ← trySynthInstanceQ q($C $ty $ty')
+        | throwError "imodintro: cannot transform hypothesis {name} : {ty} with {C}"
+      have heq : Q(@ModalityAction.transform $prop1 $prop2 $C = .transform $C) := q(Eq.refl (ModalityAction.transform $C))
+      have heq : Q($(M).action $p = .transform $C) := heq
+      return ⟨_, .mkHyp bi1 name uniq p ty', q(modaction_transform $M $heq $hC)⟩
+    | .clear =>
+       have heq : Q(@ModalityAction.clear $prop1 $prop2 = .clear) := q(Eq.refl (ModalityAction.clear))
+       have heq : Q($(M).action $p = @ModalityAction.clear $prop1 $prop2) := heq
+       return ⟨_, .mkEmp bi1, q(modaction_clear $M $heq)⟩
+    | .id =>
+      have : $prop1 =Q $prop2 := ⟨⟩
+      have : $bi1 =Q $bi2 := ⟨⟩
+      have heq : Q(@ModalityAction.id $prop1 = .id) := q(Eq.refl (ModalityAction.id))
+      have heq : Q($(M).action $p = .id) := heq
+      return ⟨_, .mkHyp bi1 name uniq p ty, q(modaction_id $M $heq)⟩
+  | .sep _ _ _ _ lhs rhs => do
+    let ⟨_, lhs', pflhs⟩ ← iModAction bi1 lhs M act
+    let ⟨_, rhs', pfrhs⟩ ← iModAction bi1 rhs M act
+    -- TODO: make pruning emp part of mkSep?
+    if let .emp _ := lhs' then
+      -- TODO: why do we need to specify bi2 here?
+      return ⟨_, rhs', q(modaction_sep_emp_l (bi2:=$bi2) $pflhs $pfrhs)⟩
+    if let .emp _ := rhs' then
+      return ⟨_, lhs', q(modaction_sep_emp_r (bi2:=$bi2) $pflhs $pfrhs)⟩
+    return ⟨_, .mkSep lhs' rhs', q(modaction_sep (bi2:=$bi2) $pflhs $pfrhs)⟩
+
+private theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q]
+  (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P :=
+    (h1.trans (M.mono h2)).trans (from_modal sel hΦ)
+
+def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSyntax `term)
+  (k : ∀ {prop' bi' P}, @Hyps u prop' bi' P → ∀ Q : Q($prop'), ProofModeM Q($P ⊢ $Q))
+   : ProofModeM (Q($e ⊢ $goal)) := do
+    let prop1 : Quoted q(Type u) ← mkFreshExprMVarQ q(Type u)
+    let bi1 : Quoted q(BI $prop1) ← mkFreshExprMVarQ q(BI $prop1)
+    let Φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
+    let M : Q(Modality $prop1 $prop) ← mkFreshExprMVarQ q(Modality $prop1 $prop)
+    let sel : Q($prop1) ← elabTermEnsuringTypeQ (← `(term | iprop($sel))) prop1
+    let Q : Quoted q($prop1) ← mkFreshExprMVarQ q($prop1)
+    let .some _ ← ProofModeM.trySynthInstanceQ q(@FromModal $prop1 $prop $bi1 $bi $Φ $M $sel $goal $Q)
+      | throwError "imodintro: {goal} is not a modality{if sel.isMVar then m!"" else m!" matching {sel}"}"
+    let hΦ : Q($Φ) ← mkFreshExprMVarQ q($Φ)
+    iSolveSideconditionAt hΦ.mvarId!
+    let iact ← ModalityActionQ.parse q($(M).action true)
+    let sact ← ModalityActionQ.parse q($(M).action false)
+    let ⟨_, hyps', pf⟩ ← iModAction bi1 hyps M (λ p => if p then iact else sact)
+    let pf' ← k hyps' Q
+    return q(modintro (sel:=$sel) $pf $pf' $hΦ)
+
+elab "imodintro" colGt sel:term : tactic => do
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+  let pf ← iModIntroCore hyps goal sel addBIGoal
+
+  mvar.assign pf
+
+macro "imodintro" : tactic => `(tactic | imodintro _)
+macro "inext" : tactic => `(tactic | imodintro (▷^[_] _))
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index c5e8b7bd9..ed618e48b 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1286,3 +1286,77 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   icases H with ⟨HA, HB⟩
 
 end cases
+
+section imodintro
+
+/-- Tests `imodintro` for absorbing (intuitionistic: id, spatial: id) -/
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP2
+
+/-- Tests `iintro` for introducing modalities -/
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
+  iintro ⟨□HP1, HP2⟩ !>
+  iexact HP2
+
+/-- Tests `imodintro` for persistently (intuitionistic: id, spatial: clear) -/
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <pers> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP1
+
+/-- Tests `imodintro` for affinely (intuitionistic: id, spatial: forall Affine) -/
+example [BI PROP] (P : PROP) : □ P ∗ <affine> P ⊢ <affine> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP2
+
+/- Tests `imodintro` for affinely (intuitionistic: id, spatial: forall Affine) failing -/
+/-- error: imodintro: hypothesis HP2 : P does not satisfy Affine -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <affine> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+
+/-- Tests `imodintro` for intuitionistically (intuitionistic: id, spatial: isEmpty) -/
+example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ □ P := by
+  iintro ⟨□HP1, □HP2⟩
+  imodintro
+  iexact HP2
+
+/- Tests `imodintro` for intuitionistically (intuitionistic: id, spatial: isEmpty) failing -/
+/-- error: imodintro: spatial context is not empty -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ □ P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+
+/-- Tests `imodintro` for bupd (intuitionistic: id, spatial: id) -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : □ P ∗ P ⊢ |==> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP2
+
+/-- Tests `imodintro` with specifying the pattern -/
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro (<absorb> _)
+  iexact HP2
+
+/- Tests `imodintro` for no modality -/
+/-- error: imodintro: P is not a modality -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+
+/- Tests `imodintro` with specifying the wrong pattern -/
+set_option pp.mvars false in
+/-- error: imodintro: iprop(<absorb> P) is not a modality matching iprop(□ ?_) -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro (□ _)
+
+end imodintro

From e06618fc3c1195e12c7197a2f7565a86dd1cb96f Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Fri, 30 Jan 2026 10:18:47 +0100
Subject: [PATCH 2/5] feat: add instances for Later and Plainly

---
 PORTING.md                                |  17 +--
 src/Iris/ProofMode.lean                   |   3 +
 src/Iris/ProofMode/Classes.lean           |  19 ++-
 src/Iris/ProofMode/ClassesMake.lean       |  15 +++
 src/Iris/ProofMode/InstancesLater.lean    |  79 ++++++++++++
 src/Iris/ProofMode/InstancesMake.lean     |  30 +++++
 src/Iris/ProofMode/InstancesPlainly.lean  | 145 ++++++++++++++++++++++
 src/Iris/ProofMode/ModalityInstances.lean |  21 ++++
 src/Iris/Std/TC.lean                      |  21 ++++
 src/Iris/Tests/Tactics.lean               |  25 ++++
 10 files changed, 367 insertions(+), 8 deletions(-)
 create mode 100644 src/Iris/ProofMode/ClassesMake.lean
 create mode 100644 src/Iris/ProofMode/InstancesMake.lean
 create mode 100644 src/Iris/ProofMode/InstancesPlainly.lean

diff --git a/PORTING.md b/PORTING.md
index 59e85ad81..7026ed580 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -260,12 +260,16 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `class_instances_internal_eq.v`
 - [ ] `class_instances_later.v` (InstancesLater.lean)
   - [x] basic instances
-  - [ ] FromModal
+  - [x] FromModal
   - [ ] ElimModal
   - [ ] AddModal
-  - [ ] IntoLater
+  - [x] IntoLater
 - [ ] `class_instances_make.v`
-- [ ] `class_instances_plainly.v`
+- [ ] `class_instances_plainly.v` (InstancesPlainly.lean)
+  - [x] basic instances
+  - [x] FromModal
+  - [ ] IntoExcept0
+  - [ ] IntoLaterN
 - [ ] `class_instances_updates.v` (InstancesUpdates.lean)
   - [x] Basic instances for bupd
   - [ ] Basic instances for fupd
@@ -283,7 +287,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] FromPure
   - [ ] IntoInternalEq
   - [x] IntoPersistent
-  - [ ] FromModal
+  - [x] FromModal
   - [x] FromAffinely
   - [x] IntoAbsorbingly
   - [x] IntoWand
@@ -307,8 +311,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] AddModal
   - [ ] Frame
   - [x] IntoExcept0
-  - [ ] MaybeIntoLaterN
-  - [ ] IntoLaterN
+  - [x] MaybeIntoLaterN / IntoLaterN
   - [ ] IntoEmbed
   - [x] AsEmpValid
   - [ ] AsEmpValid0
@@ -318,7 +321,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] ElimInv
 - [ ] `classes_make.v`
 - [ ] `coq_tactics.v` / `ltac_tactics.v` (split into the files in Tactics/)
-  - [ ] iSolveSideCondition
+  - [x] iSolveSideCondition
   - [ ] iStartProof
     - [x] basic
     - [ ] with bi specified
diff --git a/src/Iris/ProofMode.lean b/src/Iris/ProofMode.lean
index 675a75a3b..f2462941b 100644
--- a/src/Iris/ProofMode.lean
+++ b/src/Iris/ProofMode.lean
@@ -1,8 +1,11 @@
 import Iris.ProofMode.Classes
+import Iris.ProofMode.ClassesMake
 import Iris.ProofMode.Display
 import Iris.ProofMode.Expr
 import Iris.ProofMode.Instances
 import Iris.ProofMode.InstancesLater
+import Iris.ProofMode.InstancesMake
+import Iris.ProofMode.InstancesPlainly
 import Iris.ProofMode.InstancesUpdates
 import Iris.ProofMode.Patterns
 import Iris.ProofMode.Tactics
diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 5509f4051..f4be6f803 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.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
+Authors: Lars König, Michael Sammler
 -/
 import Iris.BI
 import Iris.ProofMode.SynthInstance
@@ -153,4 +153,21 @@ class FromModal {PROP1 PROP2} [BI PROP1] [BI PROP2] (φ : outParam $ Prop) (M :
   from_modal : φ → M.M Q ⊢ P
 export FromModal (from_modal)
 
+
+/-- `IntoLaterN` turns `P` into `▷^[n] Q`.
+The Boolean [only_head] indicates whether laters should only be stripped in
+head position or also below other logical connectives. For [inext] it should
+strip laters below other logical connectives, but this should not happen while
+framing.
+
+The Rocq version uses an `MaybeIntoLaterN` typeclass that avoids unfolding definitions
+for searches that do not make progress. But this is not necessary in Lean since Lean
+TC synthesis does not unfold definitions by default.
+
+This classes is deliberately not an ipm_class to use the more efficient TC synthesis.
+-/
+class IntoLaterN [BI PROP] (only_head : Bool) (n : Nat) (P : PROP) (Q : outParam PROP) where
+  into_laterN : P ⊢ ▷^[n] Q
+export IntoLaterN (into_laterN)
+
 end Iris.ProofMode
diff --git a/src/Iris/ProofMode/ClassesMake.lean b/src/Iris/ProofMode/ClassesMake.lean
new file mode 100644
index 000000000..235e4781e
--- /dev/null
+++ b/src/Iris/ProofMode/ClassesMake.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.BI
+import Iris.ProofMode.SynthInstance
+
+namespace Iris.ProofMode
+open Iris.BI
+
+/-- The class [MakeLaterN n P Q] is used to compute `lP := ▷^n P`. -/
+class MakeLaterN [BI PROP] (n : Nat) (P : PROP) (lP : outParam PROP) where
+  make_laterN : ▷^[n] P ⊣⊢ lP
+export MakeLaterN (make_laterN)
diff --git a/src/Iris/ProofMode/InstancesLater.lean b/src/Iris/ProofMode/InstancesLater.lean
index 8f8737856..91468484c 100644
--- a/src/Iris/ProofMode/InstancesLater.lean
+++ b/src/Iris/ProofMode/InstancesLater.lean
@@ -5,6 +5,8 @@ Authors: Michael Sammler
 -/
 import Iris.BI
 import Iris.ProofMode.Classes
+import Iris.ProofMode.ClassesMake
+import Iris.ProofMode.ModalityInstances
 import Iris.Std.TC
 
 namespace Iris.ProofMode
@@ -214,6 +216,20 @@ instance isExcept0_except0 [BI PROP] (P : PROP) : IsExcept0 iprop(◇ P) where
 instance isExcept0_later [BI PROP] (P : PROP) : IsExcept0 iprop(▷ P) where
   is_except0 := except0_later
 
+/-- FromModal -/
+
+instance fromModal_later [BI PROP] (P : PROP) :
+  FromModal True (modality_laterN 1) iprop(▷^[1] P) iprop(▷ P) P where
+  from_modal _ := .rfl
+
+instance fromModal_laterN [BI PROP] (P : PROP) n :
+  FromModal True (modality_laterN n) iprop(▷^[n] P) iprop(▷^[n] P) P where
+  from_modal _ := .rfl
+
+instance fromModal_except0 [BI PROP] (P : PROP) :
+  FromModal True modality_id iprop(◇ P) iprop(◇ P) P where
+  from_modal _ := except0_intro
+
 /-- IntoExcept0 -/
 
 instance intoExcept0_except0 [BI PROP] (P : PROP) : IntoExcept0 iprop(◇ P) P where
@@ -243,5 +259,68 @@ instance intoExcept0_persistently [BI PROP] (P Q : PROP)
     [h : IntoExcept0 P Q] : IntoExcept0 iprop(<pers> P) iprop(<pers> Q) where
   into_except0 := (persistently_mono h.1).trans except0_persistently.2
 
+/-- IntoLaterN -/
+instance (priority := low) intoLaterN_default [BI PROP] only_head n (P : PROP) :
+  IntoLaterN only_head n P P where
+  into_laterN := laterN_intro n
+
+instance (priority := high) intoLaterN_default_0 [BI PROP] only_head (P : PROP) :
+  IntoLaterN only_head 0 P P where
+  into_laterN := laterN_intro 0
+
+instance intoLaterN_later [BI PROP] only_head n n' m' (P Q lQ : PROP)
+    [h1 : NatCancel n 1 n' m']
+    [h2 : IntoLaterN only_head n' P Q]
+    [h3 : MakeLaterN m' Q lQ] : IntoLaterN only_head n iprop(▷ P) lQ where
+  into_laterN := (later_mono h2.1).trans $ (later_laterN _).2.trans $ by
+    rw [h1.1]
+    apply (laterN_add _ _).1.trans (laterN_mono _ h3.1.1)
+
+instance intoLaterN_laterN [BI PROP] only_head n m n' m' (P Q lQ : PROP)
+    [h1 : NatCancel n m n' m']
+    [h2 : IntoLaterN only_head n' P Q]
+    [h3 : MakeLaterN m' Q lQ] : IntoLaterN only_head n iprop(▷^[m] P) lQ where
+  into_laterN := (laterN_mono _ h2.1).trans $ (laterN_add _ _).2.trans $ by
+    rw [Nat.add_comm, h1.1]
+    apply (laterN_add _ _).1.trans (laterN_mono _ h3.1.1)
+
+instance intoLaterN_and [BI PROP] n (P1 P2 Q1 Q2 : PROP)
+    [h1 : IntoLaterN false n P1 Q1] [h2 : IntoLaterN false n P2 Q2] :
+    IntoLaterN false n iprop(P1 ∧ P2) iprop(Q1 ∧ Q2) where
+  into_laterN := (and_mono h1.1 h2.1).trans (laterN_and n).2
+
+instance intoLaterN_forall [BI PROP] n (Φ Ψ : α → PROP)
+    [h : ∀ x, IntoLaterN false n (Φ x) (Ψ x)] : IntoLaterN false n iprop(∀ x, Φ x) iprop(∀ x, Ψ x) where
+  into_laterN := (forall_mono fun x => (h x).1).trans (laterN_forall n).2
+
+instance intoLaterN_exists [BI PROP] n (Φ Ψ : α → PROP)
+    [h : ∀ x, IntoLaterN false n (Φ x) (Ψ x)] : IntoLaterN false n iprop(∃ x, Φ x) iprop(∃ x, Ψ x) where
+  into_laterN := (exists_mono fun x => (h x).1).trans (laterN_exists_2 n)
+
+instance intoLaterN_or [BI PROP] n (P1 P2 Q1 Q2 : PROP)
+    [h1 : IntoLaterN false n P1 Q1] [h2 : IntoLaterN false n P2 Q2] :
+    IntoLaterN false n iprop(P1 ∨ P2) iprop(Q1 ∨ Q2) where
+  into_laterN := (or_mono h1.1 h2.1).trans (laterN_or n).2
+
+instance intoLaterN_affinely [BI PROP] n (P Q : PROP)
+    [h : IntoLaterN false n P Q] : IntoLaterN false n iprop(<affine> P) iprop(<affine> Q) where
+  into_laterN := (affinely_mono h.1).trans (laterN_affinely_2 n)
+
+instance intoLaterN_intuitionistically [BI PROP] n (P Q : PROP)
+    [h : IntoLaterN false n P Q] : IntoLaterN false n iprop(□ P) iprop(□ Q) where
+  into_laterN := (intuitionistically_mono h.1).trans (laterN_intuitionistically_2 n)
+
+instance intoLaterN_absorbingly [BI PROP] n (P Q : PROP)
+    [h : IntoLaterN false n P Q] : IntoLaterN false n iprop(<absorb> P) iprop(<absorb> Q) where
+  into_laterN := (absorbingly_mono h.1).trans (laterN_absorbingly n).2
+
+instance intoLaterN_persistently [BI PROP] n (P Q : PROP)
+    [h : IntoLaterN false n P Q] : IntoLaterN false n iprop(<pers> P) iprop(<pers> Q) where
+  into_laterN := (persistently_mono h.1).trans (laterN_persistently n).2
+
+instance intoLaterN_sep [BI PROP] n (P1 P2 Q1 Q2 : PROP)
+    [h1 : IntoLaterN false n P1 Q1] [h2 : IntoLaterN false n P2 Q2] :
+    IntoLaterN false n iprop(P1 ∗ P2) iprop(Q1 ∗ Q2) where
+  into_laterN := (sep_mono h1.1 h2.1).trans (laterN_sep n).2
 
 end Iris.ProofMode
diff --git a/src/Iris/ProofMode/InstancesMake.lean b/src/Iris/ProofMode/InstancesMake.lean
new file mode 100644
index 000000000..a70cbaf34
--- /dev/null
+++ b/src/Iris/ProofMode/InstancesMake.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.BI
+import Iris.ProofMode.ClassesMake
+
+namespace Iris.ProofMode
+open Iris.BI
+
+/- MakeLaterN -/
+
+instance makeLaterN_0 [BI PROP] (P : PROP) : MakeLaterN 0 P P where
+  make_laterN := .rfl
+
+instance makeLaterN_1 [BI PROP] (P : PROP) : MakeLaterN 1 P iprop(▷ P) where
+  make_laterN := .rfl
+
+instance (priority := low) makeLaterN_default [BI PROP] n (P : PROP) :
+  MakeLaterN n P iprop(▷^[n] P) where
+  make_laterN := .rfl
+
+instance (priority := high) makeLaterN_True [BI PROP] n :
+  MakeLaterN (PROP:=PROP) n iprop(True) iprop(True) where
+  make_laterN := laterN_true n
+
+instance (priority := high) makeLaterN_emp [BI PROP] [BIAffine PROP] n :
+  MakeLaterN (PROP:=PROP) n iprop(emp) iprop(emp) where
+  make_laterN := laterN_emp n
diff --git a/src/Iris/ProofMode/InstancesPlainly.lean b/src/Iris/ProofMode/InstancesPlainly.lean
new file mode 100644
index 000000000..ffa3f7cec
--- /dev/null
+++ b/src/Iris/ProofMode/InstancesPlainly.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.BI
+import Iris.ProofMode.Classes
+import Iris.ProofMode.ModalityInstances
+import Iris.Std.TC
+
+namespace Iris.ProofMode
+open Iris.BI Iris.Std
+
+/-- FromAssumption -/
+
+instance fromAssumption_plainly_l_true [BI PROP] [BIPlainly PROP] (P Q : PROP)
+    [h : FromAssumption true .in P Q] : FromAssumption true .in iprop(■ P) Q where
+  from_assumption := intuitionistically_plainly_elim.trans h.1
+
+instance fromAssumption_plainly_l_false [BI PROP] [BIPlainly PROP] [BIAffine PROP] (P Q : PROP)
+    [h : FromAssumption true .in P Q] : FromAssumption false .in iprop(■ P) Q where
+  from_assumption := BIPlainly.elim_persistently.trans <|
+    intuitionistically_iff_persistently.2.trans h.1
+
+/-- FromPure -/
+
+instance fromPure_plainly [BI PROP] [BIPlainly PROP] (P : PROP) (φ : Prop)
+    [h : FromPure false P φ] : FromPure false iprop(■ P) φ where
+  from_pure := plainly_pure.2.trans (BIPlainly.mono h.1)
+
+/-- IntoPure -/
+
+instance intoPure_plainly [BI PROP] [BIPlainly PROP] (P : PROP) (φ : Prop)
+    [h : IntoPure P φ] : IntoPure iprop(■ P) φ where
+  into_pure := (BIPlainly.mono h.1).trans plainly_elim
+
+/-- IntoWand -/
+
+instance intoWand_plainly_true [BI PROP] [BIPlainly PROP] (q : Bool) ioP ioQ (R P Q : PROP)
+    [h : IntoWand true q R ioP P ioQ Q] : IntoWand true q iprop(■ R) ioP P ioQ Q where
+  into_wand := intuitionistically_plainly_elim.trans h.1
+
+instance intoWand_plainly_false [BI PROP] [BIPlainly PROP] (q : Bool) ioP ioQ (R P Q : PROP)
+    [Absorbing R] [h : IntoWand false q R ioP P ioQ Q] :
+    IntoWand false q iprop(■ R) ioP P ioQ Q where
+  into_wand := plainly_elim.trans h.1
+
+/-- FromAnd -/
+
+instance fromAnd_plainly [BI PROP] [BIPlainly PROP] (P Q1 Q2 : PROP)
+    [h : FromAnd P Q1 Q2] : FromAnd iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  from_and := plainly_and.2.trans (BIPlainly.mono h.1)
+
+/-- FromSep -/
+
+instance fromSep_plainly [BI PROP] [BIPlainly PROP] (P Q1 Q2 : PROP)
+    [h : FromSep P Q1 Q2] : FromSep iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  from_sep := plainly_sep_2.trans (BIPlainly.mono h.1)
+
+/-- IntoAnd -/
+
+instance intoAnd_plainly [BI PROP] [BIPlainly PROP] (p : Bool) (P Q1 Q2 : PROP)
+    [h : IntoAnd p P Q1 Q2] : IntoAnd p iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  into_and := by
+    cases p <;> simp only [intuitionisticallyIf, Bool.false_eq_true, ↓reduceIte]
+    · exact (BIPlainly.mono h.1).trans plainly_and.1
+    · apply (intuitionistically_idem).2.trans (intuitionistically_mono _)
+      apply (intuitionistically_plainly.trans (BIPlainly.mono h.1)).trans _
+      apply Entails.trans _ (plainly_and.1)
+      apply BIPlainly.mono
+      apply intuitionistically_elim
+
+/-- IntoSep -/
+
+instance intoSep_plainly [BI PROP] [BIPlainly PROP] [BIPositive PROP] (P Q1 Q2 : PROP)
+    [h : IntoSep P Q1 Q2] : IntoSep iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  into_sep := (BIPlainly.mono h.1).trans plainly_sep.1
+
+instance intoSep_plainly_affine [BI PROP] [BIPlainly PROP] (P Q1 Q2 : PROP)
+    [h : IntoSep P Q1 Q2]
+    [TCOr (Affine Q1) (Absorbing Q2)] [TCOr (Affine Q2) (Absorbing Q1)] :
+    IntoSep iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  into_sep := (BIPlainly.mono (h.1.trans sep_and)).trans <|
+    plainly_and.1.trans and_sep_plainly.1
+
+/-- FromOr -/
+
+instance fromOr_plainly [BI PROP] [BIPlainly PROP] (P Q1 Q2 : PROP)
+    [h : FromOr P Q1 Q2] : FromOr iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  from_or := plainly_or_2.trans (BIPlainly.mono h.1)
+
+/-- IntoOr -/
+
+instance intoOr_plainly [BI PROP] [BIPlainly PROP] [BIPlainlyExists PROP] (P Q1 Q2 : PROP)
+    [h : IntoOr P Q1 Q2] : IntoOr iprop(■ P) iprop(■ Q1) iprop(■ Q2) where
+  into_or := (BIPlainly.mono h.1).trans plainly_or.1
+
+/-- FromExists -/
+
+instance fromExists_plainly [BI PROP] [BIPlainly PROP] (P : PROP) (Φ : α → PROP)
+    [h : FromExists P Φ] : FromExists iprop(■ P) (fun a => iprop(■ Φ a)) where
+  from_exists := plainly_exists_2.trans (BIPlainly.mono h.1)
+
+/-- IntoExists -/
+
+instance intoExists_plainly [BI PROP] [BIPlainly PROP] [BIPlainlyExists PROP] (P : PROP)
+    (Φ : α → PROP) [h : IntoExists P Φ] :
+    IntoExists iprop(■ P) (fun a => iprop(■ Φ a)) where
+  into_exists := (BIPlainly.mono h.1).trans plainly_exists_1
+
+/-- IntoForall -/
+
+instance intoForall_plainly [BI PROP] [BIPlainly PROP] (P : PROP) (Φ : α → PROP)
+    [h : IntoForall P Φ] : IntoForall iprop(■ P) (fun a => iprop(■ Φ a)) where
+  into_forall := (BIPlainly.mono h.1).trans plainly_forall.1
+
+/-- FromForall -/
+
+instance fromForall_plainly [BI PROP] [BIPlainly PROP] (P : PROP) (Φ : α → PROP)
+    [h : FromForall P Φ] : FromForall iprop(■ P) (fun a => iprop(■ Φ a)) where
+  from_forall := plainly_forall.2.trans (BIPlainly.mono h.1)
+
+/-- FromModal -/
+
+instance fromModal_plainly [BI PROP] [BIPlainly PROP] (P : PROP) :
+  FromModal True modality_plainly iprop(■ P) iprop(■ P) P where
+  from_modal := by simp [modality_plainly]
+
+/- IntoExcept0 -/
+
+/- TODO
+instance intoExcept0_plainly [BI PROP] [BIPlainly PROP] [BIPlainlyExists PROP] (P Q : PROP)
+    [h : IntoExcept0 P Q] : IntoExcept0 iprop(■ P) iprop(■ Q) where
+  into_except0 := (BIPlainly.mono h.1).trans except0_plainly.2
+-/
+
+/- IntoLaterN -/
+
+/- TODO
+instance intoLaterN_plainly [BI PROP] [BIPlainly PROP] (n : Nat) (P Q : PROP)
+    [h : IntoLaterN false n P Q] : IntoLaterN false n iprop(■ P) iprop(■ Q) where
+  into_laterN := (BIPlainly.mono h.1).trans (laterN_plainly n).2
+-/
+
+end Iris.ProofMode
diff --git a/src/Iris/ProofMode/ModalityInstances.lean b/src/Iris/ProofMode/ModalityInstances.lean
index 33e410a4f..37b326b66 100644
--- a/src/Iris/ProofMode/ModalityInstances.lean
+++ b/src/Iris/ProofMode/ModalityInstances.lean
@@ -6,6 +6,7 @@ Authors: Markus de Medeiros, Michael Sammler
 import Iris.BI
 import Iris.BI.DerivedLaws
 import Iris.ProofMode.Modalities
+import Iris.ProofMode.Classes
 
 namespace Iris.ProofMode
 open Iris.BI
@@ -53,4 +54,24 @@ def modality_intuitionistically : Modality PROP PROP where
   mono := (intuitionistically_mono ·)
   sep := intuitionistically_sep_2
 
+def modality_plainly [BIPlainly PROP] : Modality PROP PROP where
+  M := plainly
+  action
+  | true => .forall Plain
+  | false => .clear
+  spec
+  | true => λ _ _ => (intuitionistically_mono Plain.plain).trans intuitionistically_plainly
+  | false => λ _ => plainly_absorbing _
+  emp := plainly_emp_2
+  mono := (BIPlainly.mono ·)
+  sep := plainly_sep_2
+
+def modality_laterN (n : Nat) : Modality PROP PROP where
+  M := BIBase.laterN n
+  action := λ _ => .transform (IntoLaterN false n)
+  spec := λ _ _ _ h => (intuitionisticallyIf_mono (h.1)).trans (laterN_intuitionisticallyIf_2 n)
+  emp := laterN_intro n
+  mono := (laterN_mono n ·)
+  sep := (laterN_sep n).2
+
 end Modalities
diff --git a/src/Iris/Std/TC.lean b/src/Iris/Std/TC.lean
index bf2b2747e..f55d0f416 100644
--- a/src/Iris/Std/TC.lean
+++ b/src/Iris/Std/TC.lean
@@ -50,4 +50,25 @@ unif_hint (b : Bool) where
 unif_hint (b : Bool) where
   |- true && b ≟ b
 
+/-- Type class for natural number cancellation. Given a number `n` and a number `m` that should
+be cancelled (subtracted) from `n`, compute a new `n'` and a remainder `m'` that could not be cancelled. -/
+class NatCancel (n m : Nat) (n' m' : outParam Nat) : Prop where
+  nat_cancel : n' + m = n + m'
+export NatCancel (nat_cancel)
+
+instance (priority := low) : NatCancel n m n m where
+  nat_cancel := by simp
+
+instance (priority := high) : NatCancel 0 m 0 m where
+  nat_cancel := rfl
+
+instance (priority := high) : NatCancel n 0 n 0 where
+  nat_cancel := Nat.add_zero n
+
+instance (priority := high) : NatCancel n n 0 0 where
+  nat_cancel := by simp
+
+instance [h : NatCancel n m n' m'] : NatCancel (n + 1) (m + 1) n' m' where
+  nat_cancel := by have := h.nat_cancel; grind
+
 end Iris.Std
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index ed618e48b..44dd8098d 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1332,12 +1332,37 @@ example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ □ P := by
   iintro ⟨□HP1, HP2⟩
   imodintro
 
+/-- Tests `imodintro` for plain (intuitionistic: .forall Plain, spatial: clear) -/
+example [BI PROP] [BIPlainly PROP] (P : PROP) [Plain P] : □ P ∗ P ⊢ ■ P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP1
+
 /-- Tests `imodintro` for bupd (intuitionistic: id, spatial: id) -/
 example [BI PROP] [BIUpdate PROP] (P : PROP) : □ P ∗ P ⊢ |==> P := by
   iintro ⟨□HP1, HP2⟩
   imodintro
   iexact HP2
 
+/-- Tests `imodintro` for later (both: transform) -/
+example [BI PROP] (P : PROP) : □ ▷ P ∗ ▷ P ⊢ ▷ P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP2
+
+/-- Tests `imodintro` for later n (both: transform) -/
+example [BI PROP] (P : PROP) : □ ▷^[n] P ∗ ▷^[n] P ⊢ ▷^[n] P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP2
+
+/-- Tests `imodintro` for complex later n (both: transform) -/
+example [BI PROP] (P : PROP) : □ ▷^[n] P ∗ ▷^[n] P ⊢ ▷^[n] P := by
+  iintro H
+  imodintro
+  icases H with ⟨-, HP2⟩
+  iexact HP2
+
 /-- Tests `imodintro` with specifying the pattern -/
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
   iintro ⟨□HP1, HP2⟩

From 40aeb0988ca7110374da475340fd98d3bef34fa3 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Fri, 30 Jan 2026 14:42:35 +0100
Subject: [PATCH 3/5] feat: add imod

---
 PORTING.md                                    | 12 +++---
 src/Iris/BI/Lib/BUpdPlain.lean                | 16 ++++---
 src/Iris/Examples/IProp.lean                  | 14 ++-----
 src/Iris/ProofMode/Classes.lean               |  5 +++
 src/Iris/ProofMode/Instances.lean             | 15 +++++++
 src/Iris/ProofMode/InstancesLater.lean        |  6 +++
 src/Iris/ProofMode/InstancesUpdates.lean      | 14 +++++++
 src/Iris/ProofMode/Patterns/CasesPattern.lean |  3 ++
 src/Iris/ProofMode/Tactics.lean               |  1 +
 src/Iris/ProofMode/Tactics/Cases.lean         |  9 ++++
 src/Iris/ProofMode/Tactics/Mod.lean           | 33 +++++++++++++++
 src/Iris/Tests/Tactics.lean                   | 42 +++++++++++++++++++
 12 files changed, 144 insertions(+), 26 deletions(-)
 create mode 100644 src/Iris/ProofMode/Tactics/Mod.lean

diff --git a/PORTING.md b/PORTING.md
index 7026ed580..9a2335e6a 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -251,7 +251,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] instances for big ops
   - [ ] MaybeCombineSepAs instances
   - [ ] CombineSepGives instances
-  - [ ] ElimModal instances
+  - [x] ElimModal instances
   - [ ] AddModal instances
   - [ ] ElimInv instances
 - [ ] `class_instances_cmra.v`
@@ -261,7 +261,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `class_instances_later.v` (InstancesLater.lean)
   - [x] basic instances
   - [x] FromModal
-  - [ ] ElimModal
+  - [x] ElimModal
   - [ ] AddModal
   - [x] IntoLater
 - [ ] `class_instances_make.v`
@@ -275,7 +275,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] Basic instances for fupd
   - [x] FromModal bupd
   - [ ] FromModal fupd
-  - [ ] ElimModal bupd
+  - [x] ElimModal bupd
   - [ ] ElimModal fupd
   - [ ] AddModal bupd
   - [ ] AddModal fupd
@@ -307,7 +307,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] CombineSepAs
   - [ ] MaybeCombineSepAs
   - [ ] CombineSepGives
-  - [ ] ElimModal
+  - [x] ElimModal
   - [ ] AddModal
   - [ ] Frame
   - [x] IntoExcept0
@@ -368,7 +368,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
     - [ ] all intro patterns (see below)
   - [ ] iInduction
   - [ ] iLöb
-  - [ ] iAssert (Lean: ihave _ : _)
+  - [x] iAssert (Lean: ihave _ : _)
   - [ ] iRewrite
   - [ ] iInv
   - [ ] iAccu
@@ -385,7 +385,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] IPure
   - [x] IIntuitionistic
   - [x] ISpatial
-  - [ ] IModalElim
+  - [x] IModalElim
   - [ ] IRewrite
   - [ ] IPureIntro
   - [x] IModalIntro
diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean
index 9b574ae4f..d54ad1737 100644
--- a/src/Iris/BI/Lib/BUpdPlain.lean
+++ b/src/Iris/BI/Lib/BUpdPlain.lean
@@ -4,6 +4,7 @@ import Iris.Algebra.Updates
 import Iris.ProofMode.Classes
 import Iris.ProofMode.Tactics
 import Iris.ProofMode.Display
+import Iris.ProofMode.InstancesUpdates
 
 namespace Iris
 open Iris.Std BI
@@ -40,12 +41,10 @@ theorem BUpdPlain_mono {P Q : PROP} : (P ⊢ Q) → (BUpdPlain P ⊢ BUpdPlain Q
   intros H
   unfold BUpdPlain
   iintro R %HQR Hp
-  have H1 : ⊢ iprop(Q -∗ ■ HQR) -∗ iprop(P -∗ ■ HQR) := by
-    iintro H Hp
-    iapply H
-    iapply H $$ Hp
   iapply R
-  iapply H1 $$ Hp
+  iintro HP
+  iapply Hp
+  iapply H $$ HP
 
 theorem BUpdPlain_idemp {P : PROP} : BUpdPlain (BUpdPlain P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
@@ -68,15 +67,14 @@ theorem BUpdPlain_plainly {P : PROP} : BUpdPlain iprop(■ P) ⊢ (■ P) := by
   unfold BUpdPlain
   iintro H
   iapply H
-  exact wand_rfl
+  iapply wand_rfl
 
 /- BiBUpdPlainly entails the alternative definition -/
 theorem BUpd_BUpdPlain [BIUpdate PROP] [BIBUpdatePlainly PROP] {P : PROP} : (|==> P) ⊢ BUpdPlain P := by
   unfold BUpdPlain
   iintro HP %_ Hx
-  iapply bupd_elim
-  iapply bupd_wand_l
-  isplitl [Hx] <;> iassumption
+  imod HP
+  iapply Hx $$ HP
 
 -- We get the usual rule for frame preserving updates if we have an [own]
 -- connective satisfying the following rule w.r.t. interaction with plainly.
diff --git a/src/Iris/Examples/IProp.lean b/src/Iris/Examples/IProp.lean
index 968d9c0fd..829637304 100644
--- a/src/Iris/Examples/IProp.lean
+++ b/src/Iris/Examples/IProp.lean
@@ -31,19 +31,11 @@ example : ⊢ |==> ∃ (γ0 γ1 : GName) (s0 s1 : String),
   let v1 : F0.ap (IProp GF) := toAgree ⟨"string1"⟩
 
   -- Allocate the resources
-  refine emp_sep.mpr.trans <| (sep_mono (iOwn_alloc v1 (fun _ => trivial)) .rfl).trans ?_
-  refine emp_sep.mpr.trans <| (sep_mono (iOwn_alloc v0 (fun _ => trivial)) .rfl).trans ?_
-
-  -- Eliminate the bupds (by hand, until iMod is implemented)
-  refine BIUpdate.frame_r.trans ?_
-  refine BIUpdate.mono (sep_mono .rfl BIUpdate.frame_r) |>.trans ?_
-  refine BIUpdate.mono bupd_frame_l |>.trans ?_
-  refine BIUpdate.trans.trans ?_
-  refine BIUpdate.mono ?_
+  imod iOwn_alloc v1 (fun _ => trivial) with ⟨%γ1, Hγ1⟩
+  imod iOwn_alloc v0 (fun _ => trivial) with ⟨%γ0, Hγ0⟩
+  imodintro
 
   -- Complete the Iris proof
-  istart
-  iintro ⟨⟨%γ0, Hγ0⟩, ⟨%γ1, Hγ1⟩, -⟩
   iexists γ0, γ1, "string0", "string1"
   isplitl [Hγ0]
   · iexact Hγ0
diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index f4be6f803..9c743d86d 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -153,6 +153,11 @@ class FromModal {PROP1 PROP2} [BI PROP1] [BI PROP2] (φ : outParam $ Prop) (M :
   from_modal : φ → M.M Q ⊢ P
 export FromModal (from_modal)
 
+@[ipm_class]
+class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outParam Bool) (P : PROP) (P' : outParam PROP) (Q : PROP) (Q' : outParam PROP) where
+  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
+export ElimModal (elim_modal)
+
 
 /-- `IntoLaterN` turns `P` into `▷^[n] Q`.
 The Boolean [only_head] indicates whether laters should only be stripped in
diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean
index dd1798f2d..000bb6bcc 100644
--- a/src/Iris/ProofMode/Instances.lean
+++ b/src/Iris/ProofMode/Instances.lean
@@ -641,3 +641,18 @@ instance (priority := default + 30) fromModal_intuitionistically_affine_bi [BI P
 instance fromModal_absorbingly [BI PROP] (P : PROP) :
   FromModal True modality_id iprop(<absorb> P) iprop(<absorb> P) P where
   from_modal := by simp [modality_id]; apply absorbingly_intro
+
+-- ElimModal
+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
+   elim_modal hφ := by
+     apply wand_intro ((sep_assoc.1.trans $ sep_mono_r $ wand_elim $ wand_intro' $ wand_intro' $ sep_assoc.2.trans _).trans (h.1 hφ))
+     apply (sep_mono_l sep_comm.1).trans (sep_assoc.1.trans $ wand_elim' $ wand_elim' .rfl)
+
+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
+  elim_modal hφ := forall_intro λ a => Entails.trans (sep_mono_r (wand_mono_r (forall_elim a))) ((h a).1 hφ)
+
+instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] :
+  ElimModal True p false iprop(<absorb> P) P Q Q where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans $ absorbingly_sep_l.1.trans $ absorbing_absorbingly.1.trans wand_elim_r
diff --git a/src/Iris/ProofMode/InstancesLater.lean b/src/Iris/ProofMode/InstancesLater.lean
index 91468484c..cf80210d9 100644
--- a/src/Iris/ProofMode/InstancesLater.lean
+++ b/src/Iris/ProofMode/InstancesLater.lean
@@ -259,6 +259,12 @@ instance intoExcept0_persistently [BI PROP] (P Q : PROP)
     [h : IntoExcept0 P Q] : IntoExcept0 iprop(<pers> P) iprop(<pers> Q) where
   into_except0 := (persistently_mono h.1).trans except0_persistently.2
 
+/-- ElimModal -/
+@[ipm_backtrack]
+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
+  elim_modal _ := ((sep_mono ((intuitionisticallyIf_mono into_except0).trans except0_intuitionisticallyIf_2) except0_intro).trans $ except0_sep.2.trans (except0_mono wand_elim_r)).trans is_except0
+
 /-- IntoLaterN -/
 instance (priority := low) intoLaterN_default [BI PROP] only_head n (P : PROP) :
   IntoLaterN only_head n P P where
diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean
index 199e780dc..9571edf6c 100644
--- a/src/Iris/ProofMode/InstancesUpdates.lean
+++ b/src/Iris/ProofMode/InstancesUpdates.lean
@@ -61,3 +61,17 @@ instance isExcept0_bupd [BIUpdate PROP] (P : PROP)
 instance fromModal_bupd [BIUpdate PROP] (P : PROP) :
     FromModal True modality_id iprop(|==> P) iprop(|==> P) P where
   from_modal := by simp [modality_id]; exact BIUpdate.intro
+
+instance elimModal_bupd [BIUpdate PROP] p (P Q : PROP) :
+  ElimModal True p false iprop(|==> P) P iprop(|==> Q) iprop(|==> Q) where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans $ bupd_frame_r.trans $ (BIUpdate.mono wand_elim_r).trans BIUpdate.trans
+
+@[ipm_backtrack]
+instance elimModal_bupd_plain_goal [BIUpdate PROP] [BIPlainly PROP] [BIBUpdatePlainly PROP] p (P Q : PROP) [Plain Q] :
+  ElimModal True p false iprop(|==> P) P Q Q where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans $ bupd_frame_r.trans $ (BIUpdate.mono wand_elim_r).trans bupd_elim
+
+@[ipm_backtrack]
+instance elimModal_bupd_plain [BIUpdate PROP] [BIPlainly PROP] [BIBUpdatePlainly PROP] p (P Q : PROP) [Plain P] :
+  ElimModal True p p iprop(|==> P) P Q Q where
+  elim_modal _ := (sep_mono_l (intuitionisticallyIf_mono bupd_elim)).trans wand_elim_r
diff --git a/src/Iris/ProofMode/Patterns/CasesPattern.lean b/src/Iris/ProofMode/Patterns/CasesPattern.lean
index 9bd87e03a..90d7072b9 100644
--- a/src/Iris/ProofMode/Patterns/CasesPattern.lean
+++ b/src/Iris/ProofMode/Patterns/CasesPattern.lean
@@ -17,6 +17,7 @@ syntax "(" icasesPatAlts ")" : icasesPat
 syntax "⌜" binderIdent "⌝" : icasesPat
 syntax "□" icasesPat : icasesPat
 syntax "∗" icasesPat : icasesPat
+syntax ">" icasesPat : icasesPat
 
 macro "%" pat:binderIdent : icasesPat => `(icasesPat| ⌜$pat⌝)
 macro "#" pat:icasesPat : icasesPat => `(icasesPat| □ $pat)
@@ -32,6 +33,7 @@ inductive iCasesPat
   | pure           (pat : TSyntax ``binderIdent)
   | intuitionistic (pat : iCasesPat)
   | spatial        (pat : iCasesPat)
+  | mod            (pat : iCasesPat)
   deriving Repr, Inhabited
 
 partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do
@@ -46,6 +48,7 @@ where
   | `(icasesPat| ⌜$pat⌝) => some <| .pure pat
   | `(icasesPat| □$pat) => go pat |>.map .intuitionistic
   | `(icasesPat| ∗$pat) => go pat |>.map .spatial
+  | `(icasesPat| >$pat) => go pat |>.map .mod
   | `(icasesPat| ($pat)) => goAlts pat
   | _ => none
   goAlts : TSyntax ``icasesPatAlts → Option iCasesPat
diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean
index 93aecba91..c5b37ed56 100644
--- a/src/Iris/ProofMode/Tactics.lean
+++ b/src/Iris/ProofMode/Tactics.lean
@@ -10,6 +10,7 @@ import Iris.ProofMode.Tactics.Exists
 import Iris.ProofMode.Tactics.Have
 import Iris.ProofMode.Tactics.Intro
 import Iris.ProofMode.Tactics.LeftRight
+import Iris.ProofMode.Tactics.Mod
 import Iris.ProofMode.Tactics.ModIntro
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.Rename
diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index e1b803852..d8da1a553 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -9,6 +9,7 @@ import Iris.ProofMode.Tactics.Basic
 import Iris.ProofMode.Tactics.Clear
 import Iris.ProofMode.Tactics.Pure
 import Iris.ProofMode.Tactics.HaveCore
+import Iris.ProofMode.Tactics.Mod
 
 namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
@@ -222,6 +223,11 @@ partial def iCasesCore
     iCasesSpatial bi P Q A' p fun B' =>
       iCasesCore hyps Q q(false) B' B' ⟨⟩ arg @k
 
+  | .mod arg =>
+    iModCore bi P Q p A' fun p' A' Q' =>
+      have ⟨A'', eq⟩ := mkIntuitionisticIf bi p' A'
+      iCasesCore hyps Q' p' A'' A' eq arg @k
+
 elab "icases" colGt pmt:pmTerm "with" colGt pat:icasesPat : tactic => do
   -- parse syntax
   let pmt ← liftMacroM <| PMTerm.parse pmt
@@ -236,6 +242,9 @@ elab "icases" colGt pmt:pmTerm "with" colGt pat:icasesPat : tactic => do
 
   mvar.assign q(($pf).trans $pf2)
 
+macro "imod" colGt pmt:pmTerm "with" colGt pat:icasesPat : tactic => `(tactic | icases $pmt with >$pat)
+macro "imod" colGt hyp:ident : tactic => `(tactic | imod $hyp:ident with $hyp:ident)
+
 -- TODO: remove these shortcuts if they are not used
 macro "iintuitionistic" hyp:ident : tactic => `(tactic | icases $hyp:ident with □$hyp:ident)
 macro "ispatial" hyp:ident : tactic => `(tactic | icases $hyp:ident with ∗$hyp:ident)
diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean
new file mode 100644
index 000000000..bcf6ebe88
--- /dev/null
+++ b/src/Iris/ProofMode/Tactics/Mod.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.ProofMode.Tactics.Basic
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+private theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q']
+  (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q :=
+    (sep_comm.1.trans (sep_mono_r (wand_intro h1))).trans (he.1 hΦ)
+
+def iModCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q : Q($prop)) (p : Q(Bool)) (A : Q($prop))
+   (k : (p' : Q(Bool)) → (A' Q' : Q($prop)) → ProofModeM Q($P ∗ □?$p' $A' ⊢ $Q'))
+   : ProofModeM (Q($P ∗ □?$p $A ⊢ $Q)) := do
+    let Φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
+    let p' : Q(Bool) ← mkFreshExprMVarQ q(Bool)
+    let A' : Q($prop) ← mkFreshExprMVarQ q($prop)
+    let Q' : Q($prop) ← mkFreshExprMVarQ q($prop)
+    let .some _ ← ProofModeM.trySynthInstanceQ q(ElimModal $Φ $p $p' $A $A' $Q $Q')
+      | throwError "imod: {A} is not a modality"
+    let hΦ : Q($Φ) ← mkFreshExprMVarQ q($Φ)
+    iSolveSideconditionAt hΦ.mvarId!
+    let p'' : Q(Bool) ← instantiateMVars p
+    have : $p'' =Q $p' := ⟨⟩
+    let A'' ← instantiateMVarsQ A'
+    have : $A'' =Q $A' := ⟨⟩
+    let Q'' ← instantiateMVarsQ Q'
+    have : $Q'' =Q $Q' := ⟨⟩
+    let pf ← k p'' A'' Q''
+    return q(mod $pf $hΦ)
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 44dd8098d..4ce556900 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1385,3 +1385,45 @@ example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
   imodintro (□ _)
 
 end imodintro
+
+section imod
+
+/-- Tests `imod` for bupd -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ |==> P := by
+  iintro HP
+  imod HP
+  iexact HP
+
+/-- Tests `imod` removing later before timeless propositions -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) [Timeless P] : ▷ P ⊢ ◇ P := by
+  iintro HP
+  imod HP
+  iexact HP
+
+/-- Tests `imod` for bupd under wand -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ emp -∗ |==> P := by
+  iintro HP
+  imod HP
+  iintro _
+  iexact HP
+
+/-- Tests `imod` with destructuring pattern -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> (P ∗ emp) ⊢ |==> P := by
+  iintro HP
+  imod HP with ⟨HP, _⟩
+  iexact HP
+
+/-- Tests `icases` with mod pattern -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : emp ∗ |==> P ⊢ |==> P := by
+  iintro HP
+  icases HP with ⟨_, >HP⟩
+  iexact HP
+
+/- Tests `imod` for no modality -/
+/-- error: imod: P is not a modality -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : P ⊢ P := by
+  iintro HP
+  imod HP
+
+end imod

From b8bffd96bc7ac4680b1cc1b6b351aae9c8288636 Mon Sep 17 00:00:00 2001
From: Zongyuan Liu <liuzongyuan0505@gmail.com>
Date: Mon, 2 Feb 2026 00:35:54 +0100
Subject: [PATCH 4/5] Add comments and stylistic changes

---
 src/Iris/ProofMode/Classes.lean           |  4 +-
 src/Iris/ProofMode/ModalityInstances.lean |  4 +-
 src/Iris/ProofMode/Tactics/Cases.lean     |  4 +-
 src/Iris/ProofMode/Tactics/Mod.lean       | 21 ++++++-
 src/Iris/ProofMode/Tactics/ModIntro.lean  | 67 +++++++++++++++++------
 src/Iris/Tests/Tactics.lean               | 31 +++++++++++
 6 files changed, 105 insertions(+), 26 deletions(-)

diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 9c743d86d..7ab75b303 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -148,11 +148,13 @@ class IntoExcept0 [BI PROP] (P : PROP) (Q : outParam PROP) where
   into_except0 : P ⊢ ◇ Q
 export IntoExcept0 (into_except0)
 
+/-- `FromModal` turns a goal `P : PROP2` into a modality `M : PROP1 → PROP2` applied to `Q : PROP1` under condition `φ`. -/
 @[ipm_class]
 class FromModal {PROP1 PROP2} [BI PROP1] [BI PROP2] (φ : outParam $ Prop) (M : outParam $ Modality PROP1 PROP2) (sel : semiOutParam PROP1) (P : PROP2) (Q : outParam $ PROP1) where
   from_modal : φ → M.M Q ⊢ P
 export FromModal (from_modal)
 
+/-- `ElimModal` turns `□?p P` into `□?p' P'` and `Q` into `Q'` under condition `φ`. -/
 @[ipm_class]
 class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outParam Bool) (P : PROP) (P' : outParam PROP) (Q : PROP) (Q' : outParam PROP) where
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
@@ -169,7 +171,7 @@ The Rocq version uses an `MaybeIntoLaterN` typeclass that avoids unfolding defin
 for searches that do not make progress. But this is not necessary in Lean since Lean
 TC synthesis does not unfold definitions by default.
 
-This classes is deliberately not an ipm_class to use the more efficient TC synthesis.
+This classes is deliberately not an `ipm_class` to use the more efficient TC synthesis.
 -/
 class IntoLaterN [BI PROP] (only_head : Bool) (n : Nat) (P : PROP) (Q : outParam PROP) where
   into_laterN : P ⊢ ▷^[n] Q
diff --git a/src/Iris/ProofMode/ModalityInstances.lean b/src/Iris/ProofMode/ModalityInstances.lean
index 37b326b66..e532e6ece 100644
--- a/src/Iris/ProofMode/ModalityInstances.lean
+++ b/src/Iris/ProofMode/ModalityInstances.lean
@@ -27,8 +27,8 @@ def modality_persistently : Modality PROP PROP where
   mono := (persistently_mono ·)
   sep := persistently_sep_2
 
-unif_hint [BIBase PROP] (P   : PROP) where |- iprop(□?false P) ≟ iprop(P)
-unif_hint [BIBase PROP] (P   : PROP) where |- iprop(□?true P) ≟ iprop(□ P)
+unif_hint [BIBase PROP] (P : PROP) where |- iprop(□?false P) ≟ iprop(P)
+unif_hint [BIBase PROP] (P : PROP) where |- iprop(□?true P) ≟ iprop(□ P)
 
 def modality_affinely : Modality PROP PROP where
   M := affinely
diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index d8da1a553..d3aea23da 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -157,9 +157,9 @@ def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p
   let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B' $A' $p)
   return q(spatial_elim (A := $A') $(← k B'))
 
-theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h
+private theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h
 
-  -- TODO: Why does this function require both A and A' instead of just A'?
+-- TODO: Why does this function require both A and A' instead of just A'?
 variable {u : Level} {prop : Q(Type u)} (bi : Q(BI $prop)) in
 partial def iCasesCore
     {P} (hyps : Hyps bi P) (Q : Q($prop)) (p : Q(Bool))
diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean
index bcf6ebe88..b70f9d649 100644
--- a/src/Iris/ProofMode/Tactics/Mod.lean
+++ b/src/Iris/ProofMode/Tactics/Mod.lean
@@ -12,6 +12,18 @@ private theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal
   (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q :=
     (sep_comm.1.trans (sep_mono_r (wand_intro h1))).trans (he.1 hΦ)
 
+/--
+Eliminate a modality from `A` by transforming the goal from `P ∗ □?p A ⊢ Q` to `P ∗ □?p' A' ⊢ Q'`,
+where `p'`, `A'`, and `Q'` are determined by `ElimModal`.
+
+Parameters:
+- `P`: Context
+- `Q`: Goal
+- `p`: Persistence flag of `A`
+- `k`: Continuation that proves `P ∗ □?p' A' ⊢ Q'`, given the transformed `p'`, `A'`, and `Q'`
+
+Returns a proof of `P ∗ □?p A ⊢ Q`
+-/
 def iModCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q : Q($prop)) (p : Q(Bool)) (A : Q($prop))
    (k : (p' : Q(Bool)) → (A' Q' : Q($prop)) → ProofModeM Q($P ∗ □?$p' $A' ⊢ $Q'))
    : ProofModeM (Q($P ∗ □?$p $A ⊢ $Q)) := do
@@ -19,15 +31,18 @@ def iModCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q : Q($prop)) (p : Q(Bool
     let p' : Q(Bool) ← mkFreshExprMVarQ 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')
       | throwError "imod: {A} is not a modality"
     let hΦ : Q($Φ) ← mkFreshExprMVarQ q($Φ)
     iSolveSideconditionAt hΦ.mvarId!
-    let p'' : Q(Bool) ← instantiateMVars p
-    have : $p'' =Q $p' := ⟨⟩
+    let p'' : Q(Bool) ← instantiateMVars p'
     let A'' ← instantiateMVarsQ A'
-    have : $A'' =Q $A' := ⟨⟩
     let Q'' ← instantiateMVarsQ Q'
+    -- establish defeq for type refinement
+    have : $p'' =Q $p' := ⟨⟩
+    have : $A'' =Q $A' := ⟨⟩
     have : $Q'' =Q $Q' := ⟨⟩
+    -- show `P ∗ □?p' A' ⊢ Q'`
     let pf ← k p'' A'' Q''
     return q(mod $pf $hΦ)
diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean
index 2b2e33681..e5b3c43a5 100644
--- a/src/Iris/ProofMode/Tactics/ModIntro.lean
+++ b/src/Iris/ProofMode/Tactics/ModIntro.lean
@@ -10,14 +10,14 @@ namespace Iris.ProofMode
 open Lean Elab Tactic Meta Qq BI Std
 
 /-- Reified version of ModalityAction -/
-inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where
+private inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where
 | isEmpty
 | forall (C : Q($PROP1 → Prop))
 | transform (C : Q($PROP2 → $PROP1 → Prop))
 | clear
 | id
 
-def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) :
+private def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) :
   ProofModeM (ModalityActionQ prop1 prop2) := do
   let act ← whnf q($act)
   match_expr act with
@@ -66,7 +66,21 @@ private theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'}
   (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(elhs' ∗ erhs') := (sep_mono h1 h2).trans M.sep
 
 
-private def iModAction {prop1 : Q(Type u)} (bi1 : Q(BI $prop1)) {e}
+/--
+Applies modality actions to transform proof mode context.
+
+# Parameters
+- `hyps` - Context in `prop2`
+- `M` - Modality being introduced (`prop1 → prop2`)
+- `act` - Modality action depending on persistence flag
+
+# Returns
+A tuple containing:
+- Transformed context term
+- Transformed context `hyps'` in `prop1`
+- Proof of `hyps ⊢ M hyps'`
+-/
+private def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e}
   (hyps : @Hyps u prop2 bi2 e) (M : Q(Modality $prop1 $prop2)) (act : Bool → ModalityActionQ prop1 prop2) :
   ProofModeM ((e' : _) × Hyps bi1 e' × Q($e ⊢ $(M).M $e')) :=
   match hyps with
@@ -80,6 +94,7 @@ private def iModAction {prop1 : Q(Type u)} (bi1 : Q(BI $prop1)) {e}
       have : $bi1 =Q $bi2 := ⟨⟩
       let .some hC ← trySynthInstanceQ q($C $ty)
         | throwError "imodintro: hypothesis {name} : {ty} does not satisfy {C}"
+      -- bridge through defeq since `M.action` cannot unify directly with the pattern (same in other cases)
       have heq : Q(@ModalityAction.forall $prop1 $C = .forall $C) := q(Eq.refl (ModalityAction.forall $C))
       have heq : Q($(M).action $p = .forall $C) := heq
       return ⟨_, .mkHyp bi1 name uniq p ty, q(modaction_forall $M $heq $hC)⟩
@@ -101,36 +116,52 @@ private def iModAction {prop1 : Q(Type u)} (bi1 : Q(BI $prop1)) {e}
       have heq : Q($(M).action $p = .id) := heq
       return ⟨_, .mkHyp bi1 name uniq p ty, q(modaction_id $M $heq)⟩
   | .sep _ _ _ _ lhs rhs => do
-    let ⟨_, lhs', pflhs⟩ ← iModAction bi1 lhs M act
-    let ⟨_, rhs', pfrhs⟩ ← iModAction bi1 rhs M act
+    let ⟨_, lhs', pflhs⟩ ← iModAction lhs M act
+    let ⟨_, rhs', pfrhs⟩ ← iModAction rhs M act
     -- TODO: make pruning emp part of mkSep?
     if let .emp _ := lhs' then
-      -- TODO: why do we need to specify bi2 here?
-      return ⟨_, rhs', q(modaction_sep_emp_l (bi2:=$bi2) $pflhs $pfrhs)⟩
+      return ⟨_, rhs', q(modaction_sep_emp_l $pflhs $pfrhs)⟩
     if let .emp _ := rhs' then
-      return ⟨_, lhs', q(modaction_sep_emp_r (bi2:=$bi2) $pflhs $pfrhs)⟩
-    return ⟨_, .mkSep lhs' rhs', q(modaction_sep (bi2:=$bi2) $pflhs $pfrhs)⟩
+      return ⟨_, lhs', q(modaction_sep_emp_r $pflhs $pfrhs)⟩
+    return ⟨_, .mkSep lhs' rhs', q(modaction_sep $pflhs $pfrhs)⟩
 
 private theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q]
   (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P :=
     (h1.trans (M.mono h2)).trans (from_modal sel hΦ)
 
+/-- Introduce a modality by applying modality actions to transform hypotheses.
+
+# Parameters
+- `hyps` : Context
+- `goal` - Goal
+- `sel` - Selector term to match against specific modality patterns
+- `k` - Continuation that receives the transformed context `P` and goal `Q`,
+  and produces a proof of `P ⊢ Q`
+
+# Returns
+Proof term of `hyps ⊢ goal`
+-/
 def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSyntax `term)
   (k : ∀ {prop' bi' P}, @Hyps u prop' bi' P → ∀ Q : Q($prop'), ProofModeM Q($P ⊢ $Q))
    : ProofModeM (Q($e ⊢ $goal)) := do
-    let prop1 : Quoted q(Type u) ← mkFreshExprMVarQ q(Type u)
-    let bi1 : Quoted q(BI $prop1) ← mkFreshExprMVarQ q(BI $prop1)
-    let Φ : Q(Prop) ← mkFreshExprMVarQ q(Prop)
-    let M : Q(Modality $prop1 $prop) ← mkFreshExprMVarQ q(Modality $prop1 $prop)
-    let sel : Q($prop1) ← elabTermEnsuringTypeQ (← `(term | iprop($sel))) prop1
-    let Q : Quoted q($prop1) ← mkFreshExprMVarQ q($prop1)
-    let .some _ ← ProofModeM.trySynthInstanceQ q(@FromModal $prop1 $prop $bi1 $bi $Φ $M $sel $goal $Q)
+    let prop' : Q(Type u) ← mkFreshExprMVarQ q(Type u)
+    let bi' ← mkFreshExprMVarQ q(BI $prop')
+    let Φ ← mkFreshExprMVarQ q(Prop)
+    let M ← mkFreshExprMVarQ q(Modality $prop' $prop)
+    let sel ← elabTermEnsuringTypeQ (← `(term | iprop($sel))) prop'
+    let Q ← mkFreshExprMVarQ q($prop')
+    -- `M Q ⊢ goal`
+    let .some _ ← ProofModeM.trySynthInstanceQ q(@FromModal $prop' $prop $bi' $bi $Φ $M $sel $goal $Q)
       | throwError "imodintro: {goal} is not a modality{if sel.isMVar then m!"" else m!" matching {sel}"}"
-    let hΦ : Q($Φ) ← mkFreshExprMVarQ q($Φ)
+    -- show the side condition
+    let hΦ ← mkFreshExprMVarQ q($Φ)
     iSolveSideconditionAt hΦ.mvarId!
+    -- pre-compute the actions
     let iact ← ModalityActionQ.parse q($(M).action true)
     let sact ← ModalityActionQ.parse q($(M).action false)
-    let ⟨_, hyps', pf⟩ ← iModAction bi1 hyps M (λ p => if p then iact else sact)
+    -- perform modality actions, get transformed context `hyps'` and `pf : hyps ⊢ M hyps'`
+    let ⟨_, hyps', pf⟩ ← iModAction hyps M (λ p => if p then iact else sact)
+    -- get proof `hyps' ⊢ Q`
     let pf' ← k hyps' Q
     return q(modintro (sel:=$sel) $pf $pf' $hΦ)
 
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 4ce556900..87289d660 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1356,6 +1356,12 @@ example [BI PROP] (P : PROP) : □ ▷^[n] P ∗ ▷^[n] P ⊢ ▷^[n] P := by
   imodintro
   iexact HP2
 
+/-- Tests `imodintro` for later n (NatCancel) -/
+example [BI PROP] (P : PROP) : □ ▷^[5] P ∗ ▷^[3] P ⊢ ▷^[4] P := by
+  iintro ⟨□HP1, HP2⟩
+  imodintro
+  iexact HP2
+
 /-- Tests `imodintro` for complex later n (both: transform) -/
 example [BI PROP] (P : PROP) : □ ▷^[n] P ∗ ▷^[n] P ⊢ ▷^[n] P := by
   iintro H
@@ -1384,6 +1390,13 @@ example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
   iintro ⟨□HP1, HP2⟩
   imodintro (□ _)
 
+/-- Tests `imodintro` with nested modalities -/
+example [BI PROP] (P : PROP) : □ P ⊢ □ <pers> P := by
+  iintro □HP
+  imodintro
+  imodintro
+  iexact HP
+
 end imodintro
 
 section imod
@@ -1426,4 +1439,22 @@ example [BI PROP] (P : PROP) : P ⊢ P := by
   iintro HP
   imod HP
 
+/-- Tests `imod` eliminating nested modalities -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> |==> P ⊢ |==> P := by
+  iintro HP
+  imod HP
+  imod HP
+  iexact HP
+
 end imod
+
+section inext
+
+/- Tests `inext` failing on non-later goal -/
+/-- error: imodintro: P is not a modality matching iprop(▷^[?m.31]?m.32) -/
+#guard_msgs in
+example [BI PROP] (P : PROP) : P ⊢ P := by
+  iintro HP
+  inext
+
+end inext

From 4892db112581770527b171ce1b10bc0b1d3910e8 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 2 Feb 2026 08:45:03 +0100
Subject: [PATCH 5/5] tweak

---
 src/Iris/Tests/Tactics.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 87289d660..76aa13313 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1451,7 +1451,8 @@ end imod
 section inext
 
 /- Tests `inext` failing on non-later goal -/
-/-- error: imodintro: P is not a modality matching iprop(▷^[?m.31]?m.32) -/
+set_option pp.mvars false in
+/-- error: imodintro: P is not a modality matching iprop(▷^[?_]?_) -/
 #guard_msgs in
 example [BI PROP] (P : PROP) : P ⊢ P := by
   iintro HP