feat: iaccu

Iris/Iris/ProofMode/Expr.lean

@@ -205,6 +205,35 @@ 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 {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) : (spatialProps : Q($prop)) × Q($e ⊢ $spatialProps) :=
+  let ⟨spatialProps, pf⟩ := buildAccuProofAux hyps (e' := q(iprop(emp))) q(iprop(emp)) q(.rfl)
+  let pf : Q($e ⊢ $spatialProps) := q(sep_emp.mpr.trans $pf)
+  ⟨spatialProps, pf⟩
+  where
+    buildAccuProofAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e e' : Q($prop)}
+      (hyps : Hyps bi e) (spatialProps : Q($prop)) (pf : Q($e' ⊢ $spatialProps)) :
+      (newSpatialProps : Q($prop)) × Q($e ∗ $e' ⊢ $newSpatialProps) :=
+    match hyps with
+    | .emp _ => ⟨spatialProps, q(emp_sep.mp.trans $pf)⟩
+    | .hyp _ _ _ p ty _ =>
+      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, pfR⟩ := buildAccuProofAux rhs spatialProps pf
+      let ⟨spatialPropsLR, pfLR⟩ := buildAccuProofAux lhs spatialPropsR pfR
+      ⟨q($spatialPropsLR), q(sep_assoc.mp.trans $pfLR)⟩
+
 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

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 ""

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

Iris/Iris/ProofMode/Tactics/Accu.lean

@@ -0,0 +1,32 @@
+/-
+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
+
+/--
+  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
+      throwError m!"iaccu: {goal} is not a metavariable"
+
+    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}"
+
+    mvar.assign pf

Iris/Iris/Tests/Tactics.lean

@@ -2856,6 +2856,36 @@ example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n)
 
 end iloeb
 
+section iaccu
+
+/-- 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
+  · ipureintro <;> rfl
+
+/-- Tests `iaccu` where there is no spatial hypothesis in the context. -/
+example [BI PROP] (P Q R : PROP) :
+    (□ P -∗ □ Q -∗ □ R -∗ ∃ S, S ∧ ⌜S = iprop(emp)⌝) := by
+  iintro #HP #HQ #HR
+  iexists ?_
+  isplit
+  · 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
+
 section iinduction
 
 /-- Inductively defined binary tree data structure -/

Iris/tactics.md

@@ -46,6 +46,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