feat: ieval, isimp and iunfold

Iris/Iris/ProofMode/Expr.lean

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

@@ -8,6 +8,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,133 @@
+/-
+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 Lean.Parser.Tactic
+
+/-- 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`, which is strengthened when
+  it is the goal or weakened when it is a hypothesis in the context.
+
+  When `isGoal` is `true`, the tactic sequence results in the proof goal being *strengthened*.
+  When `isGoal` is `false`, the tactic sequence results in the hypothesis being *weakened*.
+
+  The function returns the new expression and a proof that the expression
+  is strengthened/weakened.
+-/
+private def iEvalOne {u} {prop : Q(Type u)} (bi : Q(BI $prop))
+    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (isGoal : Bool) (ty : Q($prop)) :
+    ProofModeM <| Q($prop) × Expr := do
+  let m : Q($prop) ← mkFreshExprMVar q($prop)
+  let pf ← mkFreshExprSyntheticOpaqueMVar <| if isGoal then q($m ⊢ $ty) else q($ty ⊢ $m)
+  let [g] ← evalTacticAt tac pf.mvarId!
+    | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+  let some #[_, _, lhs, rhs] ← g.getType <&> (·.appM? ``Entails)
+    | throwError "ieval: the goal is not Iris entailment upon applying the supplied tactic"
+  let newTy : Q($prop) := if isGoal then rhs else lhs
+  m.mvarId!.assign newTy
+  g.assign (q(.rfl) : Q($newTy ⊢ $newTy))
+  return ⟨m, 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 (isGoal := true) bi tac 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 fun ty => do
+          let ⟨newTy, pf⟩ ← iEvalOne (isGoal := false) bi tac ty
+          return ⟨newTy, (pf : Q($ty ⊢ $newTy))⟩
+        | 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)`.
+
+  `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`.
+
+  One can also use `isimp [h₁, h₂, …, hₙ]`, `isimp [*]` and
+  `isimp only [h₁, h₂, …, hₙ]` for the tactic behaviour corresponding to
+  `simp [h₁, h₂, …, hₙ]`, `simp [*]` and `simp only [h₁, h₂, …, hₙ]`,
+  respectively.
+-/
+syntax "isimp" optConfig (discharger)? (&" only")? (simpArgs)?
+  (" in " (colGt ppSpace selPat)+)? : tactic
+
+private def elabSimp (simp : TSyntax `tactic)
+    (spats : Option (TSyntaxArray `selPat)) : TacticM Unit :=
+  match spats with
+  | none       => do evalTactic (← `(tactic| ieval ($simp:tactic)))
+  | some spats => do evalTactic (← `(tactic| ieval ($simp:tactic) in $spats*))
+
+elab_rules : tactic
+  | `(tactic| isimp $cfg* $[$disch]? $[[$args,*]]? $[in $spats*]?) => do
+      elabSimp (← `(tactic| simp $cfg* $[$disch]? $[[$args,*]]?)) spats
+  | `(tactic| isimp $cfg* $[$disch]? only $[[$args,*]]? $[in $spats*]?) => do
+      elabSimp (← `(tactic| simp $cfg* $[$disch]? only $[[$args,*]]?)) 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

@@ -2856,6 +2856,95 @@ example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n)
 
 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
+
+/-- Tests `isimp` with variants of `simp` -/
+example [BI PROP] {m n p q : Nat} (h1 : m = n + 1) (h2 : r = t) (h3 : s = t) :
+    ⌜p + q = q + p⌝ ⊢@{PROP} ⌜m - 1 = n⌝ ∗ ⌜r = s⌝ ∗ ⌜q + p = p + q⌝ := by
+  iintro H
+  isplitr
+  -- Simplification with a hypothesis
+  · isimp [h1]
+    itrivial
+  · isplitr
+    -- Simplification with all rules annotated with `[simp]` and all hypotheses
+    · isimp [*]
+      itrivial
+    -- Simplification only with specific rules
+    · isimp only [Nat.add_comm] in H
+      isimp only [Nat.add_comm]
+      iexact 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
+
 section iaccu
 
 /-- Tests `iaccu` with spatial hypotheses `HQ`, `HR1`, `HR2` and `HT`. -/

Iris/tactics.md

@@ -59,6 +59,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` (*configItem*)\* (*discharger*)? (`only`)? (`[` *h₁*`,` ...`,` *hₙ* `]` | `[*]`)? (`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)`. One can also use `[*]` to include all hypotheses in the pure context for simplification, or explicitly specify the lemmas and hypotheses *h₁*, ..., *hₙ*. The optional keyword `only` stipulates the use of only these lemmas and hypotheses. Similar to the built-in tactic `simp`, one can also specify additional configurations (*configItem*) or include a tactic to discharge the side conditions on conditional rewrite rules (*discharger*).
+- `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. For every hypothesis *H* in *selPats*, all hypotheses dependent on *H* must also be included in *selPats*.
 - `iloeb as` *IH* `generalizing!` [*selPats*](#selection-patterns) — same as `iloeb as` *IH* `generalizing` [*selPats*](#selection-patterns), except that for every hypothesis *H* in [*selPats*](#selection-patterns), all hypotheses dependent on *H* are implicitly also generalised.
 - `iinduction` *e* (`using` *r*)? (`with` (*tac*)? `|` *constr₁* `=>` *tac₁* `|` ... `|` *constrₙ* `=>` *tacₙ*)? — All spatial hypotheses, as well as pure/intuitionistic hypotheses dependent on *e*, are generalised and included as premises in the induction hypotheses. The induction principle is determined by the recursor name *r*, if given, or otherwise the default induction principle is chosen. The `with` clause enables alternative names to be given to variables and induction hypotheses. Each of *constr₁*, ..., *constrₙ* is the constructor name followed by the alternative names. Alternative names can be replaced with holes (`_`) for them to remain inaccessible. Each of *tac₁*, ..., *tacₙ* is either a tactic sequence for the induction subgoal or a hole (`_` or `?_`); the latter defers the induction subgoal. The tactic *tac* is optionally given, which is the first tactic applied to all induction subgoals.