From 6ac8cfebcf1ca03716a06a5381e9c4f9e82ab5aa Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 13:48:59 +0200
Subject: [PATCH 1/7] Create new function `Hyps.buildAccuProof` for `iaccu`

---
 Iris/Iris/ProofMode/Expr.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index c9f86ea0b..51eea500f 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -189,6 +189,23 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
   | _, .hyp _ _ ivar p _ _ => if isTrue p then [ivar] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds
 
+/--
+  Given any hypotheses `hyps` representing `e`, filter in all spatial hypotheses
+  and prove that `e` implies the set of spatial hypotheses.
+-/
+def Hyps.buildAccuProof {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) :
+    (spatial : Q($prop)) × Q($e ⊢ $spatial) :=
+  match hyps with
+  | .emp _ => ⟨q(iprop(emp)), q(.rfl)⟩
+  | .hyp _ _ _ p ty _ =>
+    match matchBool p with
+    | .inl _ => ⟨q(iprop(emp)), q(intuitionistically_elim_emp)⟩
+    | .inr _ => ⟨ty, q(.rfl)⟩
+  | .sep _ _ _ _ lhs rhs =>
+    let ⟨tyL, pfL⟩ := lhs.buildAccuProof
+    let ⟨tyR, pfR⟩ := rhs.buildAccuProof
+    ⟨q(iprop($tyL ∗ $tyR)), q(sep_mono $pfL $pfR)⟩
+
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
   | _, .emp _ => none

From daf3bb5743ee3cf82d8ab9f1d7b5c7490ee0e59a Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 13:53:59 +0200
Subject: [PATCH 2/7] Implement `iaccu`

---
 Iris/Iris/ProofMode/Tactics.lean      |  1 +
 Iris/Iris/ProofMode/Tactics/Accu.lean | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 Iris/Iris/ProofMode/Tactics/Accu.lean

diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index 361255881..52b514f41 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/Iris/Iris/ProofMode/Tactics.lean
@@ -1,6 +1,7 @@
 /- A description of the tactics can be found in `tactics.md`. -/
 module
 
+public meta import Iris.ProofMode.Tactics.Accu
 public meta import Iris.ProofMode.Tactics.Apply
 public meta import Iris.ProofMode.Tactics.Assumption
 public meta import Iris.ProofMode.Tactics.Basic
diff --git a/Iris/Iris/ProofMode/Tactics/Accu.lean b/Iris/Iris/ProofMode/Tactics/Accu.lean
new file mode 100644
index 000000000..1d6d14a07
--- /dev/null
+++ b/Iris/Iris/ProofMode/Tactics/Accu.lean
@@ -0,0 +1,20 @@
+/-
+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.ProofModeM
+
+namespace Iris.ProofMode
+
+public meta section
+open Lean Elab Tactic Meta Qq
+
+elab "iaccu" : tactic => do
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    if !goal.isMVar then
+      throwError m!"iaccu: {goal} is not a metavariable"
+    let ⟨_, pf⟩ := hyps.buildAccuProof
+    mvar.assign pf

From d2f59d7b62d9cc2d811392e3fe884614f5699675 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 14:52:54 +0200
Subject: [PATCH 3/7] Add tests for `iaccu`, use `isDefEq` to unify
 metavariables

---
 Iris/Iris/ProofMode/Tactics/Accu.lean |  8 +++++++-
 Iris/Iris/Tests/Tactics.lean          | 22 ++++++++++++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Accu.lean b/Iris/Iris/ProofMode/Tactics/Accu.lean
index 1d6d14a07..fac631df0 100644
--- a/Iris/Iris/ProofMode/Tactics/Accu.lean
+++ b/Iris/Iris/ProofMode/Tactics/Accu.lean
@@ -16,5 +16,11 @@ elab "iaccu" : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     if !goal.isMVar then
       throwError m!"iaccu: {goal} is not a metavariable"
-    let ⟨_, pf⟩ := hyps.buildAccuProof
+
+    let ⟨spatial, pf⟩ := hyps.buildAccuProof
+
+    let defEq ← isDefEq goal spatial
+    if !defEq then
+      throwError "iaccu: could not assign goal metavariable to {spatial}"
+
     mvar.assign pf
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..6fa671d71 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2776,3 +2776,25 @@ example (P Q : PROP) :
   iloeb as IH
 
 end iloeb
+
+section iaccu
+
+/-- Tests `iaccu` with spatial hypotheses `HQ`, `HR` and `HT`. -/
+example [BI PROP] (P Q R S T : PROP) :
+    (□ P -∗ Q -∗ R -∗ □ S -∗ T -∗ ∃ U, U ∧ ⌜U = iprop(Q ∗ R ∗ T)⌝) := by
+  iintro #HP HQ HR #HS HT
+  iexists ?_
+  isplit
+  · iaccu
+  · ipureintro <;> rfl
+
+/-- Tests `iaccu` where there is no spatial hypothesis in the context. -/
+example [BI PROP] (P Q R S T : PROP) :
+    (□ P -∗ □ Q -∗ □ R -∗ ∃ S, S ∧ ⌜S = iprop(emp)⌝) := by
+  iintro #HP #HQ #HR
+  iexists ?_
+  isplit
+  · iaccu
+  · ipureintro <;> rfl
+
+end iaccu

From c2cbb06fa426bc8e5140ec41926b95adae0c1e42 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 16:25:56 +0200
Subject: [PATCH 4/7] Re-define `Hyps.buildAccuProof` so that the combined
 proposition is always right-nesting

---
 Iris/Iris/ProofMode/Expr.lean | 35 +++++++++++++++++++++++------------
 Iris/Iris/Tests/Tactics.lean  |  2 +-
 2 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index 51eea500f..fe7340440 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -189,22 +189,33 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
   | _, .hyp _ _ ivar p _ _ => if isTrue p then [ivar] else []
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds
 
+private def Hyps.buildAccuProofAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e e' : Q($prop)}
+    (hyps : Hyps bi e) (spatialProps : Q($prop))
+    (isEmp : Bool) (pf : Q($e' ⊢ $spatialProps)) :
+    (newSpatialProps : Q($prop)) × Bool × Q($e ∗ $e' ⊢ $newSpatialProps) :=
+  match hyps with
+  | .emp _ => ⟨spatialProps, isEmp, q(emp_sep.mp.trans $pf)⟩
+  | .hyp _ _ _ p ty _ =>
+    match matchBool p, isEmp with
+    | .inl _, _ => ⟨spatialProps, isEmp, q((sep_mono_left intuitionistically_elim_emp).trans (emp_sep.mp.trans $pf))⟩
+    | .inr _, true =>
+      let pf : Q($e' ⊢ iprop(emp)) := pf
+      ⟨ty, false, q((sep_mono_right (P := $e) $pf).trans sep_emp.mp)⟩
+    | .inr _, false => ⟨q(iprop($ty ∗ $spatialProps)), false, q(sep_mono_right $pf)⟩
+  | .sep _ _ _ _ lhs rhs =>
+    let ⟨spatialPropsR, isEmpR, pfR⟩ := rhs.buildAccuProofAux spatialProps isEmp pf
+    let ⟨spatialPropsLR, isEmpLR, pfLR⟩ := lhs.buildAccuProofAux spatialPropsR isEmpR pfR
+    ⟨q($spatialPropsLR), isEmpLR, q(sep_assoc.mp.trans $pfLR)⟩
+
 /--
   Given any hypotheses `hyps` representing `e`, filter in all spatial hypotheses
   and prove that `e` implies the set of spatial hypotheses.
 -/
-def Hyps.buildAccuProof {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) :
-    (spatial : Q($prop)) × Q($e ⊢ $spatial) :=
-  match hyps with
-  | .emp _ => ⟨q(iprop(emp)), q(.rfl)⟩
-  | .hyp _ _ _ p ty _ =>
-    match matchBool p with
-    | .inl _ => ⟨q(iprop(emp)), q(intuitionistically_elim_emp)⟩
-    | .inr _ => ⟨ty, q(.rfl)⟩
-  | .sep _ _ _ _ lhs rhs =>
-    let ⟨tyL, pfL⟩ := lhs.buildAccuProof
-    let ⟨tyR, pfR⟩ := rhs.buildAccuProof
-    ⟨q(iprop($tyL ∗ $tyR)), q(sep_mono $pfL $pfR)⟩
+def Hyps.buildAccuProof {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) : (spatialProps : Q($prop)) × Q($e ⊢ $spatialProps) :=
+  let ⟨spatialProps, _, pf⟩ := hyps.buildAccuProofAux (e' := q(iprop(emp))) q(iprop(emp)) true q(.rfl)
+  let pf : Q($e ⊢ $spatialProps) := q(sep_emp.mpr.trans $pf)
+  ⟨spatialProps, pf⟩
 
 variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in
 def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e)
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 6fa671d71..5b0f6b8fb 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2789,7 +2789,7 @@ example [BI PROP] (P Q R S T : PROP) :
   · ipureintro <;> rfl
 
 /-- Tests `iaccu` where there is no spatial hypothesis in the context. -/
-example [BI PROP] (P Q R S T : PROP) :
+example [BI PROP] (P Q R : PROP) :
     (□ P -∗ □ Q -∗ □ R -∗ ∃ S, S ∧ ⌜S = iprop(emp)⌝) := by
   iintro #HP #HQ #HR
   iexists ?_

From aedd3f60059a7baaa5fcbbe803df3beccdea56c0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 16:43:46 +0200
Subject: [PATCH 5/7] Minor formatting

---
 Iris/Iris/ProofMode/Expr.lean | 29 +++++++++++++++--------------
 Iris/Iris/Tests/Tactics.lean  |  8 ++++----
 2 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index fe7340440..b23cde0bd 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/Iris/Iris/ProofMode/Expr.lean
@@ -190,22 +190,23 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} :
   | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds
 
 private def Hyps.buildAccuProofAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e e' : Q($prop)}
-    (hyps : Hyps bi e) (spatialProps : Q($prop))
-    (isEmp : Bool) (pf : Q($e' ⊢ $spatialProps)) :
-    (newSpatialProps : Q($prop)) × Bool × Q($e ∗ $e' ⊢ $newSpatialProps) :=
+    (hyps : Hyps bi e) (spatialProps : Q($prop)) (pf : Q($e' ⊢ $spatialProps)) :
+    (newSpatialProps : Q($prop)) × Q($e ∗ $e' ⊢ $newSpatialProps) :=
   match hyps with
-  | .emp _ => ⟨spatialProps, isEmp, q(emp_sep.mp.trans $pf)⟩
+  | .emp _ => ⟨spatialProps, q(emp_sep.mp.trans $pf)⟩
   | .hyp _ _ _ p ty _ =>
-    match matchBool p, isEmp with
-    | .inl _, _ => ⟨spatialProps, isEmp, q((sep_mono_left intuitionistically_elim_emp).trans (emp_sep.mp.trans $pf))⟩
-    | .inr _, true =>
-      let pf : Q($e' ⊢ iprop(emp)) := pf
-      ⟨ty, false, q((sep_mono_right (P := $e) $pf).trans sep_emp.mp)⟩
-    | .inr _, false => ⟨q(iprop($ty ∗ $spatialProps)), false, q(sep_mono_right $pf)⟩
+    match matchBool p with
+    | .inl _ =>
+      ⟨spatialProps, q((sep_mono_left intuitionistically_elim_emp).trans (emp_sep.mp.trans $pf))⟩
+    | .inr _ =>
+      if spatialProps == q(iprop(emp)) then
+        let pf : Q($e' ⊢ iprop(emp)) := pf
+        ⟨ty, q((sep_mono_right $pf).trans sep_emp.mp)⟩
+      else ⟨q(iprop($ty ∗ $spatialProps)), q(sep_mono_right $pf)⟩
   | .sep _ _ _ _ lhs rhs =>
-    let ⟨spatialPropsR, isEmpR, pfR⟩ := rhs.buildAccuProofAux spatialProps isEmp pf
-    let ⟨spatialPropsLR, isEmpLR, pfLR⟩ := lhs.buildAccuProofAux spatialPropsR isEmpR pfR
-    ⟨q($spatialPropsLR), isEmpLR, q(sep_assoc.mp.trans $pfLR)⟩
+    let ⟨spatialPropsR, pfR⟩ := rhs.buildAccuProofAux spatialProps pf
+    let ⟨spatialPropsLR, pfLR⟩ := lhs.buildAccuProofAux spatialPropsR pfR
+    ⟨q($spatialPropsLR), q(sep_assoc.mp.trans $pfLR)⟩
 
 /--
   Given any hypotheses `hyps` representing `e`, filter in all spatial hypotheses
@@ -213,7 +214,7 @@ private def Hyps.buildAccuProofAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e
 -/
 def Hyps.buildAccuProof {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (hyps : Hyps bi e) : (spatialProps : Q($prop)) × Q($e ⊢ $spatialProps) :=
-  let ⟨spatialProps, _, pf⟩ := hyps.buildAccuProofAux (e' := q(iprop(emp))) q(iprop(emp)) true q(.rfl)
+  let ⟨spatialProps, pf⟩ := hyps.buildAccuProofAux (e' := q(iprop(emp))) q(iprop(emp)) q(.rfl)
   let pf : Q($e ⊢ $spatialProps) := q(sep_emp.mpr.trans $pf)
   ⟨spatialProps, pf⟩
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 5b0f6b8fb..2936d9781 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2779,10 +2779,10 @@ end iloeb
 
 section iaccu
 
-/-- Tests `iaccu` with spatial hypotheses `HQ`, `HR` and `HT`. -/
-example [BI PROP] (P Q R S T : PROP) :
-    (□ P -∗ Q -∗ R -∗ □ S -∗ T -∗ ∃ U, U ∧ ⌜U = iprop(Q ∗ R ∗ T)⌝) := by
-  iintro #HP HQ HR #HS HT
+/-- Tests `iaccu` with spatial hypotheses `HQ`, `HR1`, `HR2` and `HT`. -/
+example [BI PROP] (P Q R1 R2 S T : PROP) :
+    (□ P -∗ Q -∗ (R1 ∗ R2) -∗ □ S -∗ T -∗ ∃ U, U ∧ ⌜U = iprop(Q ∗ R1 ∗ R2 ∗ T)⌝) := by
+  iintro #HP HQ ⟨HR1, HR2⟩ #HS HT
   iexists ?_
   isplit
   · iaccu

From 006026a3ccdc8fd9c0dea2e3da4240472c824a28 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 17:11:41 +0200
Subject: [PATCH 6/7] One more test for `iaccu`: error message

---
 Iris/Iris/ProofMode/Tactics/Accu.lean | 6 ++++++
 Iris/Iris/Tests/Tactics.lean          | 8 ++++++++
 2 files changed, 14 insertions(+)

diff --git a/Iris/Iris/ProofMode/Tactics/Accu.lean b/Iris/Iris/ProofMode/Tactics/Accu.lean
index fac631df0..76c3d6dc1 100644
--- a/Iris/Iris/ProofMode/Tactics/Accu.lean
+++ b/Iris/Iris/ProofMode/Tactics/Accu.lean
@@ -12,6 +12,11 @@ namespace Iris.ProofMode
 public meta section
 open Lean Elab Tactic Meta Qq
 
+/--
+  Given that the proof goal is a metavariable, `iaccu` combines all hypotheses
+  in the spatial context with the separating conjunction and solves the proof
+  goal by unifying the metavariable with the combined proposition.
+-/
 elab "iaccu" : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     if !goal.isMVar then
@@ -19,6 +24,7 @@ elab "iaccu" : tactic => do
 
     let ⟨spatial, pf⟩ := hyps.buildAccuProof
 
+    -- Assign and unify the metavariable
     let defEq ← isDefEq goal spatial
     if !defEq then
       throwError "iaccu: could not assign goal metavariable to {spatial}"
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 2936d9781..741a365a3 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2797,4 +2797,12 @@ example [BI PROP] (P Q R : PROP) :
   · iaccu
   · ipureintro <;> rfl
 
+/- Tests `iaccu` where the proof goal is not a metavariable -/
+/-- error: iaccu: R is not a metavariable -/
+#guard_msgs in
+example [BI PROP] (P Q R : PROP) :
+    □ P -∗ Q -∗ R := by
+  iintro #HP HQ
+  iaccu
+
 end iaccu

From a016e7cd73086a8e05cc901e92e8609bbf923801 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 17:13:28 +0200
Subject: [PATCH 7/7] Update documentation and porting status

---
 Iris/Iris/ProofMode/Porting.lean | 2 +-
 Iris/tactics.md                  | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..03f41db50 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/Iris/Iris/ProofMode/Porting.lean
@@ -56,7 +56,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iAssert" ported "ihave _ : _"
 #rocq_concept proofmode "Tactics" "iRewrite" ported "irewrite"
 #rocq_concept proofmode "Tactics" "iInv" missing ""
-#rocq_concept proofmode "Tactics" "iAccu" missing ""
+#rocq_concept proofmode "Tactics" "iAccu" ported "iaccu"
 #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial"
 
 #rocq_concept proofmode "Intro Patterns" missing ""
diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..adf1508c5 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -45,6 +45,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 - `ispecialize` [*pmTerm*](#proof-mode-terms) — Specialize a hypothesis according to [*pmTerm*](#proof-mode-terms).
 - `iexact` *H* — Solve the goal with the hypothesis *H*.
 - `iassumption` — Solve the goal with a matching hypothesis from the intuitionistic or spatial context.
+- `iaccu` — Given the goal is a metavariable, solve the goal by combining all hypotheses in the spatial context with the separating conjunction and unifying the metavariable with the combined proposition.
 
 ## Modalities