From 82d99ccf9bf37106fc76d0b131738cd56fce1f9f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 6 Sep 2024 21:07:12 -0700
Subject: [PATCH] refactor: Use `MVarId` across the board

---
 Pantograph.lean           | 91 +++++++++++++++++++++------------------
 Pantograph/Goal.lean      | 75 ++++++++++++++------------------
 Pantograph/Library.lean   | 31 ++++++-------
 Pantograph/Protocol.lean  |  3 ++
 Test/Common.lean          |  4 +-
 Test/Metavar.lean         | 22 +++++-----
 Test/Proofs.lean          | 90 +++++++++++++++++++-------------------
 Test/Tactic/Prograde.lean | 40 ++++++++---------
 8 files changed, 178 insertions(+), 178 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 35ab117..7cedab8 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -1,5 +1,6 @@
 import Lean.Data.HashMap
 import Pantograph.Compile
+import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Library
@@ -23,6 +24,11 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
 
+def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
+  metaM.run'
+def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
+  termElabM.run' (ctx := Condensed.elabContext) |>.run'
+
 def execute (command: Protocol.Command): MainM Lean.Json := do
   let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
     match Lean.fromJson? command.payload with
@@ -87,6 +93,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         noRepeat := args.noRepeat?.getD options.noRepeat,
         printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
         printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
+        automaticMode := args.automaticMode?.getD options.automaticMode,
       }
     }
     return .ok {  }
@@ -95,7 +102,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
+    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
       | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
@@ -114,47 +121,47 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       return .ok { stateId, root := goalState.root.name.toString }
   goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
     let state ← get
-    match state.goalStates.find? args.stateId with
-    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    | .some goalState => do
-      let nextGoalState?: Except _ GoalState ←
-        match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
-        | .some tactic, .none, .none, .none, .none => do
-          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
-        | .none, .some expr, .none, .none, .none => do
-          pure ( Except.ok (← goalAssign goalState args.goalId expr))
-        | .none, .none, .some type, .none, .none => do
-          let binderName := args.binderName?.getD ""
-          pure ( Except.ok (← goalState.tryHave args.goalId binderName type))
-        | .none, .none, .none, .some pred, .none => do
-          pure ( Except.ok (← goalCalc goalState args.goalId pred))
-        | .none, .none, .none, .none, .some true => do
-          pure ( Except.ok (← goalConv goalState args.goalId))
-        | .none, .none, .none, .none, .some false => do
-          pure ( Except.ok (← goalConvExit goalState))
-        | _, _, _, _, _ => pure (Except.error <|
-          errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied")
-      match nextGoalState? with
-      | .error error => return .error error
-      | .ok (.success nextGoalState) =>
-        let nextStateId := state.nextId
-        set { state with
-          goalStates := state.goalStates.insert state.nextId nextGoalState,
-          nextId := state.nextId + 1,
-        }
-        let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
-        return .ok {
-          nextStateId? := .some nextStateId,
-          goals? := .some goals,
-        }
-      | .ok (.parseError message) =>
-        return .ok { parseError? := .some message }
-      | .ok (.indexError goalId) =>
-        return .error $ errorIndex s!"Invalid goal id index {goalId}"
-      | .ok (.invalidAction message) =>
-        return .error $ errorI "invalid" message
-      | .ok (.failure messages) =>
-        return .ok { tacticErrors? := .some messages }
+    let .some goalState := state.goalStates.find? args.stateId |
+      return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    let .some goal := goalState.goals.get? args.goalId |
+      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
+    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
+      match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
+      | .some tactic, .none, .none, .none, .none => do
+        pure <| Except.ok <| ← goalState.tryTactic goal tactic
+      | .none, .some expr, .none, .none, .none => do
+        pure <| Except.ok <| ← goalState.tryAssign goal expr
+      | .none, .none, .some type, .none, .none => do
+        let binderName := args.binderName?.getD ""
+        pure <| Except.ok <| ← goalState.tryHave goal binderName type
+      | .none, .none, .none, .some pred, .none => do
+        pure <| Except.ok <| ← goalState.tryCalc goal pred
+      | .none, .none, .none, .none, .some true => do
+        pure <| Except.ok <| ← goalState.conv goal
+      | .none, .none, .none, .none, .some false => do
+        pure <| Except.ok <| ← goalState.convExit
+      | _, _, _, _, _ =>
+        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
+        pure $ Except.error $ error
+    match nextGoalState? with
+    | .error error => return .error error
+    | .ok (.success nextGoalState) =>
+      let nextStateId := state.nextId
+      set { state with
+        goalStates := state.goalStates.insert state.nextId nextGoalState,
+        nextId := state.nextId + 1,
+      }
+      let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+      return .ok {
+        nextStateId? := .some nextStateId,
+        goals? := .some goals,
+      }
+    | .ok (.parseError message) =>
+      return .ok { parseError? := .some message }
+    | .ok (.invalidAction message) =>
+      return .error $ errorI "invalid" message
+    | .ok (.failure messages) =>
+      return .ok { tacticErrors? := .some messages }
   goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
     let state ← get
     match state.goalStates.find? args.target with
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index d92a807..0df3a4b 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -30,7 +30,7 @@ structure GoalState where
   convMVar?: Option (MVarId × MVarId) := .none
   -- Previous RHS for calc, so we don't have to repeat it every time
   -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
-  calcPrevRhs?: Option Expr := .none
+  calcPrevRhs?: Option (MVarId × Expr) := .none
 
 @[export pantograph_goal_state_create_m]
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
@@ -147,24 +147,24 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
 @[export pantograph_goal_state_get_mvar_e_assignment]
-protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do
-  let expr ← goalState.mctx.eAssignment.find? mvar
+protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? mvarId
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
 
 --- Tactic execution functions ---
 
-protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
   : Elab.TermElabM GoalState := do
-  unless (← getMCtx).decls.contains mvarId do
-    throwError s!"MVarId is not in context: {mvarId.name}"
-  mvarId.checkNotAssigned `GoalState.step
-  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] }
+  unless (← getMCtx).decls.contains goal do
+    throwError s!"Goal is not in context: {goal.name}"
+  goal.checkNotAssigned `GoalState.step
+  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
   return {
     state with
     savedState := { term := nextElabState, tactic := newGoals },
-    parentMVar? := .some mvarId,
+    parentMVar? := .some goal,
     calcPrevRhs? := .none,
   }
 
@@ -176,25 +176,20 @@ inductive TacticResult where
   | failure (messages: Array String)
   -- Could not parse tactic
   | parseError (message: String)
-  -- The goal index is out of bounds
-  | indexError (goalId: Nat)
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
 /-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
-protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
       Elab.TermElabM TacticResult := do
-  let mvarId ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure $ goal
-    | .none => return .indexError goalId
   try
-    let nextState ← state.step mvarId tacticM
+    let nextState ← state.step goal tacticM
     return .success nextState
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-/-- Execute a string tactic on given state -/
-protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
+/-- Execute a string tactic on given state. Restores TermElabM -/
+protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
     Elab.TermElabM TacticResult := do
   state.restoreElabM
   let tactic ← match Parser.runParserCategory
@@ -204,9 +199,9 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
     (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic
+  state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
 
-protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
+protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let expr ← match Parser.runParserCategory
@@ -216,11 +211,11 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId $ Tactic.evalAssign expr
+  state.tryTacticM goal $ Tactic.evalAssign expr
 
 -- Specialized Tactics
 
-protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let type ← match Parser.runParserCategory
@@ -230,16 +225,13 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId $ Tactic.evalLet binderName.toName type
+  state.tryTacticM goal $ Tactic.evalLet binderName.toName type
 
 /-- Enter conv tactic mode -/
-protected def GoalState.conv (state: GoalState) (goalId: Nat):
+protected def GoalState.conv (state: GoalState) (goal: MVarId):
       Elab.TermElabM TacticResult := do
   if state.convMVar?.isSome then
     return .invalidAction "Already in conv state"
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
   goal.checkNotAssigned `GoalState.conv
   let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
     state.restoreTacticM goal
@@ -298,19 +290,17 @@ protected def GoalState.convExit (state: GoalState):
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) :=
-  if goalId == 1 then
-    state.calcPrevRhs?
+protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
+  let (mvarId, rhs ) ← state.calcPrevRhs?
+  if mvarId == goal then
+    .some rhs
   else
     .none
-protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
+protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   if state.convMVar?.isSome then
     return .invalidAction "Cannot initiate `calc` while in `conv` state"
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
   let `(term|$pred) ← match Parser.runParserCategory
     (env := state.env)
     (catName := `term)
@@ -319,9 +309,10 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
     | .ok syn => pure syn
     | .error error => return .parseError error
   goal.checkNotAssigned `GoalState.tryCalc
-  let calcPrevRhs? := state.calcPrevRhsOf? goalId
-  let target ← instantiateMVars (← goal.getDecl).type
-  let tag := (← goal.getDecl).userName
+  let calcPrevRhs? := state.calcPrevRhsOf? goal
+  let decl ← goal.getDecl
+  let target ← instantiateMVars decl.type
+  let tag := decl.userName
   try
     goal.withContext do
 
@@ -345,7 +336,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
       (userName := tag ++ `calc)
     let mvarBranch := proof.mvarId!
 
-    let calcPrevRhs? := Option.some rhs
+    let calcPrevRhs? := Option.some (goal, rhs)
     let mut proofType ← Meta.inferType proof
     let mut remainder := Option.none
 
@@ -377,19 +368,19 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
     return .failure #[← exception.toMessageData.toString]
 
 
-protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
+protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let recursor ← match (← Compile.parseTermM recursor) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor)
-protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
+  state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
+protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let eq ← match (← Compile.parseTermM eq) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq)
+  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
 
 end Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index c4ce4ff..2b2f223 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -156,41 +156,38 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G
     }
 
 @[export pantograph_goal_tactic_m]
-def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
-  runTermElabM <| state.tryTactic goalId tactic
+def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
+  runTermElabM <| state.tryTactic goal tactic
 @[export pantograph_goal_assign_m]
-def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
-  runTermElabM <| state.tryAssign goalId expr
+def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
+  runTermElabM <| state.tryAssign goal expr
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
   let type ← match (← Compile.parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   runTermElabM do
     state.restoreElabM
-    state.tryTacticM goalId $ Tactic.evalHave binderName.toName type
+    state.tryTacticM goal $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
   let expr ← match (← Compile.parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   runTermElabM do
     state.restoreElabM
-    state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr)
+    state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
 @[export pantograph_goal_let_m]
-def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
-  runTermElabM <| state.tryLet goalId binderName type
+def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
+  runTermElabM <| state.tryLet goal binderName type
 @[export pantograph_goal_conv_m]
-def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult :=
-  runTermElabM <| state.conv goalId
+def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
+  runTermElabM <| state.conv goal
 @[export pantograph_goal_conv_exit_m]
 def goalConvExit (state: GoalState): CoreM TacticResult :=
   runTermElabM <| state.convExit
 @[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
-  runTermElabM <| state.tryCalc goalId pred
-@[export pantograph_goal_focus]
-def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
-  state.focus goalId
+def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
+  runTermElabM <| state.tryCalc goal pred
 
 end Pantograph
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 1a52c8a..223fcfe 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -27,6 +27,8 @@ structure Options where
   printAuxDecls: Bool      := false
   -- See `pp.implementationDetailHyps`
   printImplementationDetailHyps: Bool := false
+  -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
+  automaticMode: Bool := false
   deriving Lean.ToJson
 
 abbrev OptionsT := ReaderT Options
@@ -190,6 +192,7 @@ structure OptionsSet where
   noRepeat?: Option Bool
   printAuxDecls?: Option Bool
   printImplementationDetailHyps?: Option Bool
+  automaticMode?: Option Bool
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
diff --git a/Test/Common.lean b/Test/Common.lean
index 83f2e7b..2d98aca 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -62,13 +62,15 @@ protected def Goal.devolatilize (goal: Goal): Goal :=
 
 end Condensed
 
+def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
+def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
+
 def TacticResult.toString : TacticResult → String
   | .success state => s!".success ({state.goals.length} goals)"
   | .failure messages =>
     let messages := "\n".intercalate messages.toList
     s!".failure {messages}"
   | .parseError error => s!".parseError {error}"
-  | .indexError index => s!".indexError {index}"
   | .invalidAction error => s!".invalidAction {error}"
 
 namespace Test
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 2fcab28..dbaf2cc 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -83,7 +83,7 @@ def test_m_couple: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -92,7 +92,7 @@ def test_m_couple: TestM Unit := do
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   -- Set m to 3
-  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with
+  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -115,7 +115,7 @@ def test_m_couple_simp: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -126,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do
   addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
     #[#["_uniq.38"], #["_uniq.38"], #[]])
 
-  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with
+  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -140,7 +140,7 @@ def test_m_couple_simp: TestM Unit := do
   addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 2", .some "2 ≤ 5"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-  let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with
+  let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -150,7 +150,7 @@ def test_m_couple_simp: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with
+  let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -177,7 +177,7 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -191,7 +191,7 @@ def test_proposition_generation: TestM Unit := do
     addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
 
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
+  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -201,7 +201,7 @@ def test_proposition_generation: TestM Unit := do
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
   let assign := "Eq.refl x"
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with
+  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -220,7 +220,7 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -228,7 +228,7 @@ def test_partial_continuation: TestM Unit := do
   addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
 
-  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with
+  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index ba97ad7..1da21ae 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -91,7 +91,7 @@ def test_identity: TestM Unit := do
       return ()
 
   let tactic := "intro p h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn 0 tactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -118,7 +118,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with
+  let state1 ← match ← state0.tacticOn 0 "intro n m" with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -126,13 +126,13 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
   addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
 
-  match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with
+  match ← state1.tacticOn 0 "assumption" with
   | .failure #[message] =>
     addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
   | other => do
     addTest $ assertUnreachable $ other.toString
 
-  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with
+  let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -150,14 +150,14 @@ def test_delta_variable: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
 
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
     #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
-  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with
+  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -189,14 +189,14 @@ def test_arith: TestM Unit := do
       return ()
 
   let tactic := "intros"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check tactic (state1.goals.length = 1)
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
+  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -204,7 +204,7 @@ def test_arith: TestM Unit := do
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
   let tactic := "assumption"
-  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -239,7 +239,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
 
   let tactic := "intro p q h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -265,7 +265,7 @@ def test_or_comm: TestM Unit := do
     serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
-  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
+  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -289,7 +289,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(2 parent)" (state2parent ==
     s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
 
-  let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -298,7 +298,7 @@ def test_or_comm: TestM Unit := do
     serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
   addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
-  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -307,13 +307,13 @@ def test_or_comm: TestM Unit := do
   let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
-  let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
+  let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
-  let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with
+  let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -327,13 +327,13 @@ def test_or_comm: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
-  let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
-  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -372,7 +372,7 @@ def test_conv: TestM Unit := do
       return ()
 
   let tactic := "intro a b c1 c2 h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -380,7 +380,7 @@ def test_conv: TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[interiorGoal [] "a + b + c1 = b + a + c2"])
 
-  let state2 ← match ← state1.conv (goalId := 0) with
+  let state2 ← match ← state1.conv (state1.get! 0) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -389,7 +389,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
 
   let convTactic := "rhs"
-  let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with
+  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -398,7 +398,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
 
   let convTactic := "lhs"
-  let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with
+  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -407,7 +407,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
 
   let convTactic := "congr"
-  let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with
+  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -419,7 +419,7 @@ def test_conv: TestM Unit := do
     ])
 
   let convTactic := "rw [Nat.add_comm]"
-  let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with
+  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -428,7 +428,7 @@ def test_conv: TestM Unit := do
     #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
 
   let convTactic := "rfl"
-  let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with
+  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -443,7 +443,7 @@ def test_conv: TestM Unit := do
       return ()
 
   let convTactic := "rfl"
-  let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with
+  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -458,7 +458,7 @@ def test_conv: TestM Unit := do
       return ()
 
   let tactic := "exact h"
-  let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with
+  let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -485,7 +485,7 @@ def test_calc: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
   let tactic := "intro a b c d h1 h2"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -493,7 +493,7 @@ def test_calc: TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[interiorGoal [] "a + b = c + d"])
   let pred := "a + b = b + c"
-  let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with
+  let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -503,11 +503,11 @@ def test_calc: TestM Unit := do
       interiorGoal [] "a + b = b + c" (.some "calc"),
       interiorGoal [] "b + c = c + d"
     ])
-  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? 0 |>.isNone)
-  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome)
+  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
+  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
 
   let tactic := "apply h1"
-  let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -518,7 +518,7 @@ def test_calc: TestM Unit := do
       addTest $ expectationFailure "continue" e
       return ()
   let pred := "_ = c + d"
-  let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with
+  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -527,9 +527,9 @@ def test_calc: TestM Unit := do
     #[
       interiorGoal [] "b + c = c + d" (.some "calc")
     ])
-  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? 0 |>.isNone)
+  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
   let tactic := "apply h2"
-  let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
+  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -549,7 +549,7 @@ def test_nat_zero_add: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
   let tactic := "intro n"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -557,7 +557,7 @@ def test_nat_zero_add: TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("n", "Nat")] "n + 0 = n"])
   let recursor := "@Nat.brecOn"
-  let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with
+  let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -571,7 +571,7 @@ def test_nat_zero_add: TestM Unit := do
     ])
 
   let tactic := "exact n"
-  let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with
+  let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -584,7 +584,7 @@ def test_nat_zero_add: TestM Unit := do
       addTest $ assertUnreachable e
       return ()
   let tactic := "exact (λ x => x + 0 = x)"
-  let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -597,7 +597,7 @@ def test_nat_zero_add: TestM Unit := do
       addTest $ assertUnreachable e
       return ()
   let tactic := "intro t h"
-  let state3 ← match ← state2c.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -606,7 +606,7 @@ def test_nat_zero_add: TestM Unit := do
     #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
 
   let tactic := "simp"
-  let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -617,7 +617,7 @@ def test_nat_zero_add: TestM Unit := do
       addTest $ assertUnreachable e
       return ()
   let tactic := "rfl"
-  let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with
+  let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -637,7 +637,7 @@ def test_nat_zero_add_alt: TestM Unit := do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
   let tactic := "intro n"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -645,7 +645,7 @@ def test_nat_zero_add_alt: TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("n", "Nat")] "n + 0 = n"])
   let recursor := "@Nat.brecOn"
-  let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with
+  let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -660,7 +660,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     ])
 
   let tactic := "intro x"
-  let state3m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -668,7 +668,7 @@ def test_nat_zero_add_alt: TestM Unit := do
   addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
   let tactic := "apply Eq"
-  let state3m2 ← match ← state3m.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean
index 22b342e..132718a 100644
--- a/Test/Tactic/Prograde.lean
+++ b/Test/Tactic/Prograde.lean
@@ -55,7 +55,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -64,7 +64,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
     #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
 
   let expr := "Or.inl (Or.inl h)"
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -74,7 +74,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let evalBind := "y"
   let evalExpr := "Or.inl h"
-  let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with
+  let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -94,7 +94,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   }])
 
   let expr := "Or.inl y"
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
+  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
 def test_define_root_expr : TestT Elab.TermElabM Unit := do
   --let rootExpr ← parseSentence "Nat"
   --let state0 ← GoalState.create rootExpr
-  --let .success state1 ← state0.tryTactic (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
   --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
   --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
   let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p x"
-  let .success state1 ← state0.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let binderName := `binder
   let value := "x.fst"
   let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
   let tacticM := Tactic.evalDefine binderName expr
-  let .success state2 ← state1.tryTacticM (goalId := 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
   let tactic := s!"apply {binderName}"
-  let .success state3 ← state2.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let tactic := s!"exact 5"
-  let .success state4 ← state3.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
 
@@ -139,7 +139,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -148,7 +148,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
     #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
 
   let expr := "Or.inl (Or.inl h)"
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -158,7 +158,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let haveBind := "y"
   let haveType := "p ∨ q"
-  let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
+  let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -170,7 +170,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
     ])
 
   let expr := "Or.inl h"
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
+  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -184,7 +184,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
       addTest $ assertUnreachable e
       return ()
   let expr := "Or.inl y"
-  let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
+  let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -199,7 +199,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro a p h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -213,8 +213,8 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let letType := "Nat"
   let expr := s!"let b: {letType} := _; _"
   let result2 ← match specialized with
-    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
-    | false => state1.tryAssign (goalId := 0) (expr := expr)
+    | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
+    | false => state1.tryAssign (state1.get! 0) (expr := expr)
   let state2 ← match result2 with
     | .success state => pure state
     | other => do
@@ -240,7 +240,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
     ])
 
   let tactic := "exact 1"
-  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
@@ -266,14 +266,14 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
     ])
 
   let tactic := "exact h"
-  match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+  match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
   | .failure #[message] =>
     addTest $ LSpec.check tactic  (message = s!"type mismatch\n  h\nhas type\n  a : Prop\nbut is expected to have type\n  {mainTarget} : Prop")
   | other => do
     addTest $ assertUnreachable $ other.toString
 
   let tactic := "exact Or.inl (Or.inl h)"
-  let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+  let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString