feat: ieval, isimp and iunfold

Iris/Iris/ProofMode/Expr.lean

@@ -434,6 +434,24 @@ def Hyps.replace : m (Option ((e' : Q($prop)) × Hyps bi e' × Q($e ⊢ $e'))) :
   let some ⟨_, hyps', pf⟩ ← hyps.replaceCore bi e ivar repl | return none
   return some ⟨_, hyps', q(replace_finish $pf)⟩
 
+def Hyps.evalReplace [Monad m] [MonadLiftT MetaM m]
+    {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (ivar : IVarId)
+    (repl : (ty : Q($prop)) → m ((ty' : Q($prop)) × Q($ty ⊢ $ty'))) :
+    ∀ {e}, Hyps bi e → m (Option ((e' : Q($prop)) × Hyps bi e' × Q($e ⊢ $e')))
+  | _, .emp _ => return none
+  | _, .hyp _ name ivar' p ty _ =>
+      if ivar == ivar' then do
+        let ⟨ty', h⟩ ← repl ty
+        return some ⟨_, .mkHyp bi name ivar p ty',
+                     q(intuitionisticallyIf_mono (p := $p) $h)⟩
+      else return none
+  | _, .sep _ _ _ _ lhs rhs => do
+      if let some ⟨_, lhs', h⟩ ← lhs.evalReplace ivar repl then
+        return some ⟨_, .mkSep lhs' rhs, q(sep_mono_left $h)⟩
+      if let some ⟨_, rhs', h⟩ ← rhs.evalReplace ivar repl then
+        return some ⟨_, .mkSep lhs rhs', q(sep_mono_right $h)⟩
+      return none
+
 end replace
 
 section dependency

Iris/Iris/ProofMode/Porting.lean

@@ -19,9 +19,9 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iStopProof" ported "istop"
 #rocq_concept proofmode "Tactics" "iRename" ported "irename"
 #rocq_concept proofmode "Tactics" "iClear" ported "iclear"
-#rocq_concept proofmode "Tactics" "iEval" missing ""
-#rocq_concept proofmode "Tactics" "iSimpl" missing ""
-#rocq_concept proofmode "Tactics" "iUnfold" missing ""
+#rocq_concept proofmode "Tactics" "iEval" ported "ieval"
+#rocq_concept proofmode "Tactics" "iSimpl" ported "isimp"
+#rocq_concept proofmode "Tactics" "iUnfold" ported "iunfold"
 #rocq_concept proofmode "Tactics" "iExact" ported "iexact"
 #rocq_concept proofmode "Tactics" "iAssumption" ported "iassumption"
 #rocq_concept proofmode "Tactics" "iAssumptionCoq" ignored "weird tactic"

Iris/Iris/ProofMode/Tactics.lean

@@ -7,6 +7,7 @@ public meta import Iris.ProofMode.Tactics.Basic
 public meta import Iris.ProofMode.Tactics.Cases
 public meta import Iris.ProofMode.Tactics.Clear
 public meta import Iris.ProofMode.Tactics.Combine
+public meta import Iris.ProofMode.Tactics.Eval
 public meta import Iris.ProofMode.Tactics.Exact
 public meta import Iris.ProofMode.Tactics.ExFalso
 public meta import Iris.ProofMode.Tactics.Exists

Iris/Iris/ProofMode/Tactics/Eval.lean

@@ -0,0 +1,121 @@
+/-
+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.Patterns.SelPattern
+public meta import Iris.ProofMode.ProofModeM
+
+namespace Iris.ProofMode
+
+public meta section
+open Lean Elab Tactic Meta Qq BI
+
+/-- For iteratively applying the tactic sequences to selection targets in the context -/
+private structure EvalState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (e : Q($prop)) where
+  {newE : Q($prop)}
+  (newHyps : Hyps bi newE)
+  (pf : Q($e ⊢ $newE))
+
+/--
+  Apply the tactic sequence `tac` to transform `ty` into `newTy`, with the
+  Boolean value `isGoal` indicating whether `ty` is the proof goal.
+-/
+private def iEvalOne {u} {prop : Q(Type u)} (bi : Q(BI $prop))
+    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (isGoal : Bool) (ty : Q($prop)) :
+    ProofModeM <| (newTy : Q($prop)) × if isGoal then Q($newTy ⊢ $ty) else Q($ty ⊢ $newTy) := do
+  -- Find the new proposition obtained upon applying the tactic sequence
+  let newTy : Q($prop) ←
+    withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
+      let m ← mkFreshExprSyntheticOpaqueMVar <|
+        match isGoal with | true => q($newTy ⊢ $ty) | false => q($ty ⊢ $newTy)
+      let [g] ← evalTacticAt tac m.mvarId!
+      | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+      let some #[_, _, lhs, rhs] ← g.getType <&> (·.appM? ``Entails)
+      | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
+      return if isGoal then rhs else lhs
+
+  let pf ← match isGoal with
+  -- The tactic sequence results in the proof goal being *strengthened*
+  | true => mkFreshExprSyntheticOpaqueMVar q($newTy ⊢ $ty)
+  -- The tactic sequence results in the hypothesis being *weakened*
+  | false => mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
+  match ← evalTacticAt tac pf.mvarId! with
+  | [] => pure ()
+  | [g] => g.assign (q(.rfl) : Q($newTy ⊢ $newTy))
+  | _ => throwError "ieval: the supplied tactic produces more than one subgoal"
+
+  return ⟨newTy, pf⟩
+
+/--
+  Apply the tactic sequence `tac` to either the proof goal (when `selTargets`
+  is `none`) or the hypotheses in the context specified by the selection targets.
+-/
+private def iEvalCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (selTargets : Option <| List SelTarget) : ProofModeM Q($e ⊢ $goal) := do
+  match selTargets with
+  -- No selection pattern given, apply the tactics to the proof goal
+  | none =>
+    let ⟨newGoal, (pf : Q($newGoal ⊢ $goal))⟩ ← iEvalOne bi tac true goal
+    let pf' ← addBIGoal hyps newGoal
+    return q($(pf').trans $pf)
+  -- Selection patterns given, apply the tactics to the chosen hypotheses
+  | some selTargets =>
+    let mut evalState : EvalState e := { newHyps := hyps, pf := q(.rfl) }
+    -- Iteratively apply the supplied tactic sequence to the selection targets
+    for selTarget in selTargets do
+      evalState ← match selTarget.kind with
+      | .pure _ =>
+        throwError "ieval: pure hypotheses in the selection pattern is not supported"
+      | .ipm ivar =>
+        let some ⟨newE, newHyps, pf⟩ ← evalState.newHyps.evalReplace ivar (iEvalOne bi tac false ·)
+        | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context"
+        pure { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
+    let pf' ← addBIGoal evalState.newHyps goal
+    return q($(evalState.pf).trans $pf')
+
+/--
+  `ieval (tac)` applies the tactic sequence `tac` to the proof goal.
+-/
+elab "ieval " "(" tac:tacticSeq ")" : tactic => do
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iEvalCore hyps goal tac none
+    mvar.assign pf
+
+/--
+  `ieval (tac) in spats` applies the tactic sequence `tac` to the Iris
+  hypotheses chosen by the selection pattern `spats`. Pure hypotheses are not
+  supported by this tactic.
+-/
+elab "ieval " "(" tacs:tacticSeq ")" " in " spats:(colGt ppSpace selPat)+ : tactic => do
+  let selPats ← liftMacroM <| SelPat.parse spats
+
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let selTargets ← SelPat.resolve hyps selPats
+    let pf ← iEvalCore hyps goal tacs selTargets
+    mvar.assign pf
+
+/-- `isimp` applies `simp` to the proof goal. This is shorthand for `ieval (simp)`. -/
+macro "isimp" : tactic => `(tactic| ieval (simp))
+
+/--
+  `isimp in spats` applies `simp` to the Iris hypotheses chosen by the
+  selection pattern `spats`. Pure hypotheses are not supported by this tactic.
+  This is shorthand for `ieval (simp) in spats`.
+-/
+macro "isimp" " in " spats:(colGt ppSpace selPat)+ : tactic =>
+  `(tactic| ieval (simp) in $spats*)
+
+/-- `iunfold hs` applies `unfold hs` to the proof goal. This is shorthand for `ieval (unfold)`. -/
+macro "iunfold " hs:ident,+ : tactic => `(tactic| ieval (unfold $hs*))
+
+/--
+  `iunfold hs in spats` applies `unfold hs` to the Iris hypotheses chosen by
+  the selection pattern `spats`. Pure hypotheses are not supported by this tactic.
+  This is shorthand for `ieval (unfold hs) in spats`.
+-/
+macro "iunfold " hs:ident,+ " in " spats:(colGt ppSpace selPat)* : tactic =>
+  `(tactic| ieval (unfold $hs*) in $spats*)

Iris/Iris/Tests/Tactics.lean

@@ -2776,3 +2776,75 @@ example (P Q : PROP) :
   iloeb as IH
 
 end iloeb
+
+section ieval
+
+/-- Tests `ieval` and `isimp` to simplify the goal and specific Iris hypotheses. -/
+example [BI PROP] {u v w x y z : Nat} :
+    ⌜(x + y) + 3 = 4⌝ ∗ ⌜(w + z) + 1 = Nat.succ 2⌝ ∗ ⌜(u + v) = v⌝
+    ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ ∗ ⌜w + z = 2⌝ ∗ ⌜u = 0⌝ := by
+  iintro ⟨H1, H2, H3⟩
+  -- Simplify `(x + y) + 3 = 4` as `x + y = 1`
+  isimp in H1
+  isplitl [H1]
+  -- Simplify `(x + y).succ = 2` as `x + y = 1`
+  · isimp
+    iexact H1
+  -- Simplify the goal `w + z + 1 = Nat.succ 2` as `w + z = 2` and `u + v = v` as `u = 0`
+  · ieval (simp) in H2 H3
+    iframe
+
+/- Tests `isimp` with a pure hypothesis in the selection pattern -/
+/-- error: ieval: pure hypotheses in the selection pattern is not supported -/
+#guard_msgs in
+example [BI PROP] {x y : Nat} :
+    ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by
+  iintro #H
+  isimp in %x H
+
+/- Tests `isimp` with the simplification failing -/
+/-- error: `simp` made no progress -/
+#guard_msgs in
+example [BI PROP] {x y : Nat} : ⌜x = 0⌝ ⊢@{PROP} ⌜x = 0⌝ := by
+  iintro #H
+  isimp in H
+
+private def def1 := 10
+private def def2 := def1
+
+/-- Tests `iunfold` to unfold definitions in an Iris hypothesis and a proof goal -/
+example [BI PROP] : ⌜def2 = 10⌝ ⊢@{PROP} ⌜10 = 10⌝ ∗ ⌜def2 = 10⌝ := by
+  iintro #H
+  -- Unfold definitions in an Iris hypothesis
+  iunfold def2, def1 in H
+  iframe H
+  -- Unfold definitions in the proof goal
+  iunfold def2, def1
+  ipureintro
+  .rfl
+
+/- Tests `ieval` where the supplied tactic solves the goal completely -/
+/-- error: ieval: the supplied tactic does not produce exactly one subgoal -/
+#guard_msgs in
+example [BI PROP] {x y : Nat} (_ : False) :
+    ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by
+  iintro H
+  ieval (contradiction) in H
+
+/- Tests `ieval` where the supplied tactic produces more than one subgoal -/
+/-- error: ieval: the supplied tactic does not produce exactly one subgoal -/
+#guard_msgs in
+example [BI PROP] {x y : Nat} (h : False) :
+    ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by
+  iintro H
+  ieval (cases x) in H
+
+/- Tests `ieval` where the given tactic breaks the Iris entailment -/
+/-- error: ieval: the goal is not Iris entailment upon applying the supplied tactic -/
+#guard_msgs in
+example [BI PROP] {x y : Nat} :
+    ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by
+  iintro H
+  ieval (exfalso) in H
+
+end ieval

Iris/tactics.md

@@ -57,6 +57,9 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti
 ## Rewriting and Induction
 
 - `irewrite [`*rules*`]` (`at` *H* | `at ⊢`)? — Rewrite with internal equalities (`≡`). Each rule is a [*pmTerm*](#proof-mode-terms), optionally prefixed with `←` for right-to-left rewriting. Rewrites in the goal by default or in hypothesis *H*. Supports `(occs := ...)` config. Example: `irewrite [← Heq $$ %b] at H`.
+- `ieval (`*tac*`)` (`in` [*selPats*](#selection-patterns))? — applies the tactic *tac* to the Iris hypotheses chosen by the selection pattern, if given, or otherwise to proof goal. The tactic *tac* should be a reduction or rewriting tactic such as `simp`, `dsimp` or `unfold`. Note that this tactic does not support pure hypotheses in the selection pattern, in which case *tac* should be used directly.
+- `isimp` (`in` [*selPats*](#selection-patterns))? — applies `simp` to the Iris hypotheses chosen by the selection pattern, if given, or otherwise to proof goal. This is a shorthand for `ieval (simp)`.
+- `iunfold` *x₁*`,` ...`,` *xₙ* (`in` [*selPats*](#selection-patterns))? — applies `unfold` with the arguments *x₁*`,` ...`,` *xₙ* to the Iris hypotheses chosen by the selection pattern, if given, or otherwise to proof goal. This is a shorthand for `ieval (unfold` *x₁*`,` ...`,` *xₙ*`)`.
 - `iloeb as` *IH* (`generalizing` [*selPats*](#selection-patterns))? — Löb induction: adds the induction hypothesis *IH* (guarded by `▷`) to the intuitionistic context. All spatial hypotheses — plus anything selected by [*selPats*](#selection-patterns), including pure variables via `%x` — are generalized into the induction hypothesis.
 
 ## Solving Simple Goals