From 39c26949af1ee26ce6109803d342eadcc5019f93 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Sun, 28 Jun 2026 17:41:23 +0200
Subject: [PATCH 01/20] Start implementing `ieval`, `isimp` and `iunfold`

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 40 +++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 Iris/Iris/ProofMode/Tactics/Eval.lean

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
new file mode 100644
index 000000000..684625193
--- /dev/null
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -0,0 +1,40 @@
+/-
+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
+
+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)
+    (selPats : Option <| List SelPat) : ProofModeM Q($e ⊢ $goal) := do
+  sorry
+
+elab "ieval " tac:tacticSeq : tactic => do
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iEvalCore hyps goal tac none
+    mvar.assign pf
+
+elab "ieval " tacs:tacticSeq " in " spats:(colGt ppSpace selPat)* : tactic => do
+  let selPats ← liftMacroM <| SelPat.parse spats
+  ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
+    let pf ← iEvalCore hyps goal tacs selPats
+    mvar.assign pf
+
+macro "isimp" : tactic => `(tactic| ieval simp)
+
+macro "isimp" " in " spats:(colGt ppSpace selPat)* : tactic =>
+  `(tactic| ieval simp in $spats*)
+
+macro "iunfold " hs:ident,+ : tactic => `(tactic| ieval (unfold $hs*))
+
+macro "iunfold " hs:ident,+ " in " spats:(colGt ppSpace selPat)* : tactic =>
+  `(tactic| ieval (unfold $hs*) in $spats*)

From 27ab402c9e6e56b9c9d9772e2026d4bce62582ca Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 09:52:16 +0200
Subject: [PATCH 02/20] Require non-empty selection pattern

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 684625193..d0bff3c88 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -15,23 +15,27 @@ open Lean Elab Tactic Meta Qq
 
 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)
-    (selPats : Option <| List SelPat) : ProofModeM Q($e ⊢ $goal) := do
-  sorry
+    (selTargets : Option <| List SelTarget) : ProofModeM Q($e ⊢ $goal) := do
+  match selTargets with
+  | none => sorry
+  | some selTargets => sorry
 
 elab "ieval " tac:tacticSeq : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     let pf ← iEvalCore hyps goal tac none
     mvar.assign pf
 
-elab "ieval " tacs:tacticSeq " in " spats:(colGt ppSpace selPat)* : tactic => do
+elab "ieval " tacs:tacticSeq " in " spats:(colGt ppSpace selPat)+ : tactic => do
   let selPats ← liftMacroM <| SelPat.parse spats
+
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
-    let pf ← iEvalCore hyps goal tacs selPats
+    let selTargets ← SelPat.resolve hyps selPats
+    let pf ← iEvalCore hyps goal tacs selTargets
     mvar.assign pf
 
 macro "isimp" : tactic => `(tactic| ieval simp)
 
-macro "isimp" " in " spats:(colGt ppSpace selPat)* : tactic =>
+macro "isimp" " in " spats:(colGt ppSpace selPat)+ : tactic =>
   `(tactic| ieval simp in $spats*)
 
 macro "iunfold " hs:ident,+ : tactic => `(tactic| ieval (unfold $hs*))

From 5c784fa93ab5067ab8a432a3fc44abab0fda3fb3 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 10:35:37 +0200
Subject: [PATCH 03/20] Introduce `iEvalHyps` and `iEvalGoal`

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index d0bff3c88..9886e4a90 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -13,12 +13,32 @@ namespace Iris.ProofMode
 public meta section
 open Lean Elab Tactic Meta Qq
 
+private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (hyps : Hyps bi e)
+    (selTargets : List SelTarget) :
+    ProofModeM <| (newE : Q($prop)) × (newHyps : Hyps bi newE) × Q($e ⊢ $newE) := do
+  sorry
+
+private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (goal : Q($prop)) :
+    ProofModeM <| (newGoal : Q($prop)) × Q($newGoal ⊢ $goal) := do
+  sorry
+
 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
-  | none => sorry
-  | some selTargets => sorry
+  -- No selection pattern given, apply the tactics to the proof goal
+  | none =>
+    let ⟨newGoal, pf⟩ ← iEvalGoal 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 ⟨_, newHyps, pf⟩ ← iEvalHyps tac hyps selTargets
+    let pf' ← addBIGoal newHyps goal
+    return q($(pf).trans $pf')
 
 elab "ieval " tac:tacticSeq : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do

From 7d2a8750806fc205e894f8012820be9d259b9809 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 11:27:32 +0200
Subject: [PATCH 04/20] Towards implementing `iEvalGoal`, add a relevant test

---
 Iris/Iris/ProofMode/Tactics.lean      |  1 +
 Iris/Iris/ProofMode/Tactics/Eval.lean | 23 ++++++++++++++++++++---
 Iris/Iris/Tests/Tactics.lean          | 12 ++++++++++++
 3 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index 361255881..554936b34 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/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
diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 9886e4a90..c64ff5262 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -11,19 +11,36 @@ public meta import Iris.ProofMode.ProofModeM
 namespace Iris.ProofMode
 
 public meta section
-open Lean Elab Tactic Meta Qq
+open Lean Elab Tactic Meta Qq BI
+
+theorem eval_refl [BI PROP] (P : PROP) : P ⊢ P := .rfl
 
 private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
     (hyps : Hyps bi e)
     (selTargets : List SelTarget) :
     ProofModeM <| (newE : Q($prop)) × (newHyps : Hyps bi newE) × Q($e ⊢ $newE) := do
-  sorry
+  throwUnsupportedSyntax
 
 private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (goal : Q($prop)) :
     ProofModeM <| (newGoal : Q($prop)) × Q($newGoal ⊢ $goal) := do
-  sorry
+  let newGoal : Q($prop) ←
+    withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newGoal => do
+      let m ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
+      let [g] ← evalTacticAt tac m.mvarId!
+      | throwError "ieval: error"
+      let some #[_, _, _, newGoal] ← g.getType <&> (·.appM? ``Entails)
+      | throwError "ieval: error"
+      return newGoal
+
+  let pf : Q($newGoal ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
+  match ← evalTacticAt tac pf.mvarId! with
+  | [] => pure ()
+  | [g] => g.assign q(eval_refl $newGoal)
+  | _ => throwError "ieval: error"
+
+  return ⟨newGoal, pf⟩
 
 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)
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..98568659c 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2776,3 +2776,15 @@ example (P Q : PROP) :
   iloeb as IH
 
 end iloeb
+
+section ieval
+
+/-- Tests `isimp` to simplify the goal and the hypothesis `H` separately. -/
+example [BI PROP] {x y : Nat} :
+    ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} iprop(⌜Nat.succ (x + y) = 2⌝) := by
+  iintro #H
+  isimp
+  simp -- isimp in H
+  itrivial
+
+end ieval

From 46cebf6bee32e0bd3759c64dfbf5a2f636794d76 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 13:12:03 +0200
Subject: [PATCH 05/20] Introduce `EvalState` for iterative handling of
 selection targets

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index c64ff5262..b76875bc4 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -15,12 +15,27 @@ open Lean Elab Tactic Meta Qq BI
 
 theorem eval_refl [BI PROP] (P : PROP) : P ⊢ P := .rfl
 
+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))
+
+private def iEvalHypsOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
+    (evalState : @EvalState u prop bi e)
+    (selTarget : SelTarget) :
+    ProofModeM <| @EvalState u prop bi e := do
+  sorry
+
 private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
     (hyps : Hyps bi e)
     (selTargets : List SelTarget) :
-    ProofModeM <| (newE : Q($prop)) × (newHyps : Hyps bi newE) × Q($e ⊢ $newE) := do
-  throwUnsupportedSyntax
+    ProofModeM <| @EvalState u prop bi e := do
+  let mut evalState : EvalState e := { newE := e, newHyps := hyps, pf := q(.rfl) }
+  for selTarget in selTargets do
+    evalState ← iEvalHypsOne tac evalState selTarget
+  return evalState
 
 private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (goal : Q($prop)) :
@@ -53,9 +68,9 @@ private def iEvalCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     return q($(pf').trans $pf)
   -- Selection patterns given, apply the tactics to the chosen hypotheses
   | some selTargets =>
-    let ⟨_, newHyps, pf⟩ ← iEvalHyps tac hyps selTargets
-    let pf' ← addBIGoal newHyps goal
-    return q($(pf).trans $pf')
+    let evalState ← iEvalHyps tac hyps selTargets
+    let pf' ← addBIGoal evalState.newHyps goal
+    return q($(evalState.pf).trans $pf')
 
 elab "ieval " tac:tacticSeq : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do

From 9115175b72fb8e48a0e18b2665bab7133bbf62a5 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 13:41:02 +0200
Subject: [PATCH 06/20] Towards implementing `iEvalHypsOne`

---
 Iris/Iris/ProofMode/Expr.lean         | 18 +++++++++++++++++
 Iris/Iris/ProofMode/Tactics/Eval.lean | 28 +++++++++++++++++++++++++--
 Iris/Iris/Tests/Tactics.lean          |  2 +-
 3 files changed, 45 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean
index c9f86ea0b..1ade48dcf 100644
--- a/Iris/Iris/ProofMode/Expr.lean
+++ b/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
diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index b76875bc4..b30d66b51 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -25,14 +25,38 @@ private def iEvalHypsOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (evalState : @EvalState u prop bi e)
     (selTarget : SelTarget) :
     ProofModeM <| @EvalState u prop bi e := do
-  sorry
+  match selTarget.kind with
+  | .pure fvar =>
+    return evalState
+  | .ipm ivar =>
+    let some ⟨newE, newHyps, pf⟩ ← evalState.newHyps.evalReplace ivar <|
+      fun ty => do
+        let newTy : Q($prop) ←
+          withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
+            let m ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
+            let [g] ← evalTacticAt tac m.mvarId!
+            | throwError "ieval: error"
+            let some #[_, _, _, newTy] ← g.getType <&> (·.appM? ``Entails)
+            | throwError "ieval: error"
+            return newTy
+
+        let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
+        match ← evalTacticAt tac pf.mvarId! with
+        | [] => pure ()
+        | [g] => g.assign q(eval_refl $newTy)
+        | _ => throwError "ieval: error"
+
+        return ⟨newTy, pf⟩
+    | throwError "ieval: error"
+
+    return { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
 
 private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
     (hyps : Hyps bi e)
     (selTargets : List SelTarget) :
     ProofModeM <| @EvalState u prop bi e := do
-  let mut evalState : EvalState e := { newE := e, newHyps := hyps, pf := q(.rfl) }
+  let mut evalState : EvalState e := { newHyps := hyps, pf := q(.rfl) }
   for selTarget in selTargets do
     evalState ← iEvalHypsOne tac evalState selTarget
   return evalState
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 98568659c..0441d1d7b 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2784,7 +2784,7 @@ example [BI PROP] {x y : Nat} :
     ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} iprop(⌜Nat.succ (x + y) = 2⌝) := by
   iintro #H
   isimp
-  simp -- isimp in H
+  isimp in H
   itrivial
 
 end ieval

From e986d836bc1dbc333a844bbf4269e302280704b0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 13:59:34 +0200
Subject: [PATCH 07/20] Complete `ieval` implementation

---
 Iris/Iris/ProofMode/Tactics/Eval.lean |  6 +++---
 Iris/Iris/Tests/Tactics.lean          | 10 +++++++++-
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index b30d66b51..ce463c368 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -26,8 +26,8 @@ private def iEvalHypsOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (selTarget : SelTarget) :
     ProofModeM <| @EvalState u prop bi e := do
   match selTarget.kind with
-  | .pure fvar =>
-    return evalState
+  | .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
@@ -36,7 +36,7 @@ private def iEvalHypsOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
             let m ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
             let [g] ← evalTacticAt tac m.mvarId!
             | throwError "ieval: error"
-            let some #[_, _, _, newTy] ← g.getType <&> (·.appM? ``Entails)
+            let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
             | throwError "ieval: error"
             return newTy
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 0441d1d7b..7e21e2b64 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2783,8 +2783,16 @@ section ieval
 example [BI PROP] {x y : Nat} :
     ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} iprop(⌜Nat.succ (x + y) = 2⌝) := by
   iintro #H
-  isimp
   isimp in H
+  isimp
   itrivial
 
+/- 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} iprop(⌜Nat.succ (x + y) = 2⌝) := by
+  iintro #H
+  isimp in %x H
+
 end ieval

From 19976350e4ef81c50c18ca1a17e120ca4e49bd7e Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 14:16:53 +0200
Subject: [PATCH 08/20] Add tests for `ieval` and `isimp`

---
 Iris/Iris/ProofMode/Tactics/Eval.lean |  8 +++----
 Iris/Iris/Tests/Tactics.lean          | 30 ++++++++++++++++++++-------
 2 files changed, 26 insertions(+), 12 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index ce463c368..123864143 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -96,12 +96,12 @@ private def iEvalCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     let pf' ← addBIGoal evalState.newHyps goal
     return q($(evalState.pf).trans $pf')
 
-elab "ieval " tac:tacticSeq : tactic => do
+elab "ieval " "(" tac:tacticSeq ")" : tactic => do
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     let pf ← iEvalCore hyps goal tac none
     mvar.assign pf
 
-elab "ieval " tacs:tacticSeq " in " spats:(colGt ppSpace selPat)+ : tactic => do
+elab "ieval " "(" tacs:tacticSeq ")" " in " spats:(colGt ppSpace selPat)+ : tactic => do
   let selPats ← liftMacroM <| SelPat.parse spats
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
@@ -109,10 +109,10 @@ elab "ieval " tacs:tacticSeq " in " spats:(colGt ppSpace selPat)+ : tactic => do
     let pf ← iEvalCore hyps goal tacs selTargets
     mvar.assign pf
 
-macro "isimp" : tactic => `(tactic| ieval simp)
+macro "isimp" : tactic => `(tactic| ieval (simp))
 
 macro "isimp" " in " spats:(colGt ppSpace selPat)+ : tactic =>
-  `(tactic| ieval simp in $spats*)
+  `(tactic| ieval (simp) in $spats*)
 
 macro "iunfold " hs:ident,+ : tactic => `(tactic| ieval (unfold $hs*))
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 7e21e2b64..9ac3ec415 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2779,20 +2779,34 @@ end iloeb
 
 section ieval
 
-/-- Tests `isimp` to simplify the goal and the hypothesis `H` separately. -/
-example [BI PROP] {x y : Nat} :
-    ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} iprop(⌜Nat.succ (x + y) = 2⌝) := by
-  iintro #H
-  isimp in H
-  isimp
-  itrivial
+/-- 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} iprop(⌜Nat.succ (x + y) = 2⌝) := by
+    ⌜(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
+
 end ieval

From f9ea46dcd9b7254de5389c97c3e1c30e5a2c62fc Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 14:28:27 +0200
Subject: [PATCH 09/20] Add a test for `iunfold`

---
 Iris/Iris/Tests/Tactics.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 9ac3ec415..cede57c53 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2809,4 +2809,18 @@ 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
+
 end ieval

From f782157403dd4e613a60066017fc1d45a7de949e Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 14:55:27 +0200
Subject: [PATCH 10/20] More specific error messages with `ieval` for invalid
 inputs

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 14 +++++++-------
 Iris/Iris/Tests/Tactics.lean          | 24 ++++++++++++++++++++++++
 2 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 123864143..706a5a212 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -35,19 +35,19 @@ private def iEvalHypsOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
           withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
             let m ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
             let [g] ← evalTacticAt tac m.mvarId!
-            | throwError "ieval: error"
+            | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
             let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
-            | throwError "ieval: error"
+            | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
             return newTy
 
         let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
         match ← evalTacticAt tac pf.mvarId! with
         | [] => pure ()
         | [g] => g.assign q(eval_refl $newTy)
-        | _ => throwError "ieval: error"
+        | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
 
         return ⟨newTy, pf⟩
-    | throwError "ieval: error"
+    | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context"
 
     return { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
 
@@ -68,16 +68,16 @@ private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
     withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newGoal => do
       let m ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
       let [g] ← evalTacticAt tac m.mvarId!
-      | throwError "ieval: error"
+      | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
       let some #[_, _, _, newGoal] ← g.getType <&> (·.appM? ``Entails)
-      | throwError "ieval: error"
+      | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
       return newGoal
 
   let pf : Q($newGoal ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
   match ← evalTacticAt tac pf.mvarId! with
   | [] => pure ()
   | [g] => g.assign q(eval_refl $newGoal)
-  | _ => throwError "ieval: error"
+  | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
 
   return ⟨newGoal, pf⟩
 
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index cede57c53..0d77d2f5f 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -2823,4 +2823,28 @@ example [BI PROP] : ⌜def2 = 10⌝ ⊢@{PROP} ⌜10 = 10⌝ ∗ ⌜def2 = 10⌝
   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

From a898fe70793f95f007edc48a94acd4646d43a52f Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 14:57:22 +0200
Subject: [PATCH 11/20] Code refactoring: integrate `iEvalHypsOne` into
 `iEvalHyps` inline

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 58 ++++++++++++---------------
 1 file changed, 26 insertions(+), 32 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 706a5a212..04cb32085 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -20,37 +20,6 @@ private structure EvalState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (e : Q($pr
   (newHyps : Hyps bi newE)
   (pf : Q($e ⊢ $newE))
 
-private def iEvalHypsOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
-    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
-    (evalState : @EvalState u prop bi e)
-    (selTarget : SelTarget) :
-    ProofModeM <| @EvalState u prop bi e := do
-  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 : Q($prop) ←
-          withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
-            let m ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
-            let [g] ← evalTacticAt tac m.mvarId!
-            | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-            let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
-            | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
-            return newTy
-
-        let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
-        match ← evalTacticAt tac pf.mvarId! with
-        | [] => pure ()
-        | [g] => g.assign q(eval_refl $newTy)
-        | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-
-        return ⟨newTy, pf⟩
-    | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context"
-
-    return { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
-
 private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
     (hyps : Hyps bi e)
@@ -58,7 +27,32 @@ private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     ProofModeM <| @EvalState u prop bi e := do
   let mut evalState : EvalState e := { newHyps := hyps, pf := q(.rfl) }
   for selTarget in selTargets do
-    evalState ← iEvalHypsOne tac evalState selTarget
+    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 : Q($prop) ←
+            withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
+              let m ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
+              let [g] ← evalTacticAt tac m.mvarId!
+              | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+              let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
+              | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
+              return newTy
+
+          let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
+          match ← evalTacticAt tac pf.mvarId! with
+          | [] => pure ()
+          | [g] => g.assign q(eval_refl $newTy)
+          | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+
+          return ⟨newTy, pf⟩
+      | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context"
+
+      return { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
+
   return evalState
 
 private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}

From 7d1b229d9025c729cc51c42f5f615e12ad8c4ecd Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 14:59:36 +0200
Subject: [PATCH 12/20] Code refactoring: comments

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 40 +++++++++++++++------------
 1 file changed, 22 insertions(+), 18 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 04cb32085..d4cc2ef72 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -20,6 +20,7 @@ private structure EvalState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (e : Q($pr
   (newHyps : Hyps bi newE)
   (pf : Q($e ⊢ $newE))
 
+/-- Iteratively apply the supplied tactic sequence to the selection targets -/
 private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
     (hyps : Hyps bi e)
@@ -31,33 +32,35 @@ private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     | .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 : Q($prop) ←
-            withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
-              let m ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
-              let [g] ← evalTacticAt tac m.mvarId!
-              | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-              let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
-              | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
-              return newTy
-
-          let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
-          match ← evalTacticAt tac pf.mvarId! with
-          | [] => pure ()
-          | [g] => g.assign q(eval_refl $newTy)
-          | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-
-          return ⟨newTy, pf⟩
+      let some ⟨newE, newHyps, pf⟩ ← evalState.newHyps.evalReplace ivar <| fun ty => do
+        -- Find the new hypothesis obtained upon applying the tactic sequence
+        let newTy : Q($prop) ←
+          withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
+            let [g] ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy) >>= (evalTacticAt tac ·.mvarId!)
+            | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+            let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
+            | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
+            return newTy
+
+        -- The tactic sequence results in the proof goal being *weakened*
+        let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
+        match ← evalTacticAt tac pf.mvarId! with
+        | [] => pure ()
+        | [g] => g.assign q(eval_refl $newTy)
+        | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+
+        return ⟨newTy, pf⟩
       | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context"
 
       return { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
 
   return evalState
 
+/-- Apply the supplied tactic sequence to the proof goal -/
 private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (goal : Q($prop)) :
     ProofModeM <| (newGoal : Q($prop)) × Q($newGoal ⊢ $goal) := do
+  -- Find the new proof goal obtained upon applying the tactic sequence
   let newGoal : Q($prop) ←
     withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newGoal => do
       let m ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
@@ -67,6 +70,7 @@ private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
       | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
       return newGoal
 
+  -- The tactic sequence results in the proof goal being *strengthened*
   let pf : Q($newGoal ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
   match ← evalTacticAt tac pf.mvarId! with
   | [] => pure ()

From d8778458d73a59b699ee45f1cff6363406616da0 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 15:16:14 +0200
Subject: [PATCH 13/20] Bug fix: use `pure` instead of `return`

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index d4cc2ef72..5f1164758 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -51,8 +51,7 @@ private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
 
         return ⟨newTy, pf⟩
       | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context"
-
-      return { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
+      pure { newE, newHyps, pf := q($(evalState.pf).trans $pf) }
 
   return evalState
 

From 05bceaecd7aa643d7a44b042d3c56948b4b865c3 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 15:19:12 +0200
Subject: [PATCH 14/20] Eliminate trivial theorem `eval_refl`

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 5f1164758..2295b77af 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -13,8 +13,6 @@ namespace Iris.ProofMode
 public meta section
 open Lean Elab Tactic Meta Qq BI
 
-theorem eval_refl [BI PROP] (P : PROP) : P ⊢ P := .rfl
-
 private structure EvalState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (e : Q($prop)) where
   {newE : Q($prop)}
   (newHyps : Hyps bi newE)
@@ -46,7 +44,7 @@ private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
         let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
         match ← evalTacticAt tac pf.mvarId! with
         | [] => pure ()
-        | [g] => g.assign q(eval_refl $newTy)
+        | [g] => g.assign (q(.rfl) : Q($newTy ⊢ $newTy))
         | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
 
         return ⟨newTy, pf⟩
@@ -73,7 +71,7 @@ private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
   let pf : Q($newGoal ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
   match ← evalTacticAt tac pf.mvarId! with
   | [] => pure ()
-  | [g] => g.assign q(eval_refl $newGoal)
+  | [g] => g.assign (q(.rfl) : Q($newGoal ⊢ $newGoal))
   | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
 
   return ⟨newGoal, pf⟩

From 43ff334bc680ffcf395ac69753f8134aa5ab4be9 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 15:38:15 +0200
Subject: [PATCH 15/20] Factor out repetitive parts of the code as a helper
 function

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 64 ++++++++++++---------------
 1 file changed, 29 insertions(+), 35 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 2295b77af..c7d994f4c 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -18,6 +18,33 @@ private structure EvalState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (e : Q($pr
   (newHyps : Hyps bi newE)
   (pf : Q($e ⊢ $newE))
 
+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 does not produce exactly one subgoal"
+
+  return ⟨newTy, pf⟩
+
 /-- Iteratively apply the supplied tactic sequence to the selection targets -/
 private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
@@ -30,24 +57,7 @@ private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     | .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
-        -- Find the new hypothesis obtained upon applying the tactic sequence
-        let newTy : Q($prop) ←
-          withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newTy => do
-            let [g] ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy) >>= (evalTacticAt tac ·.mvarId!)
-            | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-            let some #[_, _, newTy, _] ← g.getType <&> (·.appM? ``Entails)
-            | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
-            return newTy
-
-        -- The tactic sequence results in the proof goal being *weakened*
-        let pf : Q($ty ⊢ $newTy) ← mkFreshExprSyntheticOpaqueMVar q($ty ⊢ $newTy)
-        match ← evalTacticAt tac pf.mvarId! with
-        | [] => pure ()
-        | [g] => g.assign (q(.rfl) : Q($newTy ⊢ $newTy))
-        | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-
-        return ⟨newTy, pf⟩
+      let some ⟨newE, newHyps, pf⟩ ← evalState.newHyps.evalReplace ivar (@iEvalOne u prop 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) }
 
@@ -58,23 +68,7 @@ private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
     (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (goal : Q($prop)) :
     ProofModeM <| (newGoal : Q($prop)) × Q($newGoal ⊢ $goal) := do
   -- Find the new proof goal obtained upon applying the tactic sequence
-  let newGoal : Q($prop) ←
-    withLocalDeclDQ (← mkFreshUserName .anonymous) q($prop) fun newGoal => do
-      let m ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
-      let [g] ← evalTacticAt tac m.mvarId!
-      | throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-      let some #[_, _, _, newGoal] ← g.getType <&> (·.appM? ``Entails)
-      | throwError m!"ieval: the goal is not Iris entailment upon applying the supplied tactic"
-      return newGoal
-
-  -- The tactic sequence results in the proof goal being *strengthened*
-  let pf : Q($newGoal ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar q($newGoal ⊢ $goal)
-  match ← evalTacticAt tac pf.mvarId! with
-  | [] => pure ()
-  | [g] => g.assign (q(.rfl) : Q($newGoal ⊢ $newGoal))
-  | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
-
-  return ⟨newGoal, pf⟩
+  return ← @iEvalOne u prop bi tac true goal
 
 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)

From be5817a8d4e74090b8f00b80f8401bb3c80ce770 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 15:46:17 +0200
Subject: [PATCH 16/20] Refactor code to avoid repetition

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 50 ++++++++++-----------------
 1 file changed, 19 insertions(+), 31 deletions(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index c7d994f4c..1b8025b1a 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -13,20 +13,24 @@ 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))
 
-private def iEvalOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+/--
+  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 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)
@@ -45,43 +49,27 @@ private def iEvalOne {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
 
   return ⟨newTy, pf⟩
 
-/-- Iteratively apply the supplied tactic sequence to the selection targets -/
-private def iEvalHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
-    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq)
-    (hyps : Hyps bi e)
-    (selTargets : List SelTarget) :
-    ProofModeM <| @EvalState u prop bi e := do
-  let mut evalState : EvalState e := { newHyps := hyps, pf := q(.rfl) }
-  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 u prop 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) }
-
-  return evalState
-
-/-- Apply the supplied tactic sequence to the proof goal -/
-private def iEvalGoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
-    (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (goal : Q($prop)) :
-    ProofModeM <| (newGoal : Q($prop)) × Q($newGoal ⊢ $goal) := do
-  -- Find the new proof goal obtained upon applying the tactic sequence
-  return ← @iEvalOne u prop bi tac true goal
-
 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⟩ ← iEvalGoal tac goal
+    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 evalState ← iEvalHyps tac hyps 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')
 

From 9bd5d0a92967f0991273c74286231ea4bda8bd33 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 15:52:21 +0200
Subject: [PATCH 17/20] Add docstring comments to `iEvalCore` and the tactics

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 1b8025b1a..5a22665d3 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -49,6 +49,10 @@ private def iEvalOne {u} {prop : Q(Type u)} (bi : Q(BI $prop))
 
   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
@@ -73,11 +77,19 @@ private def iEvalCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
     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
 
@@ -86,12 +98,24 @@ elab "ieval " "(" tacs:tacticSeq ")" " in " spats:(colGt ppSpace selPat)+ : tact
     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*)

From 89a12d758bcb101e501720634e5cfd0df1aad23d Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 15:54:12 +0200
Subject: [PATCH 18/20] Update `Porting.lean`

---
 Iris/Iris/ProofMode/Porting.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..adb24733e 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/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"

From aeb11f70df0a3480ea69764fc6ebca4a0556b56d Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 16:01:36 +0200
Subject: [PATCH 19/20] Update `tactics.md`

---
 Iris/tactics.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..e1e7a5b09 100644
--- a/Iris/tactics.md
+++ b/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

From fb43f8c0759c4feb45444430dbd1a561a5e0f7ae Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Tue, 30 Jun 2026 16:06:03 +0200
Subject: [PATCH 20/20] Refine error message

---
 Iris/Iris/ProofMode/Tactics/Eval.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean
index 5a22665d3..24183bfb2 100644
--- a/Iris/Iris/ProofMode/Tactics/Eval.lean
+++ b/Iris/Iris/ProofMode/Tactics/Eval.lean
@@ -45,7 +45,7 @@ private def iEvalOne {u} {prop : Q(Type u)} (bi : Q(BI $prop))
   match ← evalTacticAt tac pf.mvarId! with
   | [] => pure ()
   | [g] => g.assign (q(.rfl) : Q($newTy ⊢ $newTy))
-  | _ => throwError "ieval: the supplied tactic does not produce exactly one subgoal"
+  | _ => throwError "ieval: the supplied tactic produces more than one subgoal"
 
   return ⟨newTy, pf⟩