refactor(goal): A state can have multiple parents

2025-06-25 13:07:47 -07:00 · 2025-06-25 13:07:47 -07:00 · 0b731273b2
parent 8e35926b5c
commit 0b731273b2
10 changed files with 130 additions and 134 deletions
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@ -530,16 +530,14 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava

 protected def GoalState.serializeGoals
      (state: GoalState)
-      (parent: Option GoalState := .none)
      (options: @&Protocol.Options := {}):
    MetaM (Array Protocol.Goal):= do
  state.restoreMetaM
  let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
  goals.mapM fun goal => do
    match state.mctx.findDecl? goal with
    | .some mvarDecl =>
-      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none)
      pure serializedGoal
    | .none => throwError s!"Metavariable does not exist in context {goal.name}"

@ -606,7 +604,9 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
    userNameToString : Name → String
      | .anonymous => ""
      | other => s!"[{other}]"
-    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
+    parentHasMVar (mvarId: MVarId): Bool := match parent? with
+      | .some state => state.mctx.decls.contains mvarId
+      | .none => true

 initialize
  registerTraceClass `Pantograph.Delate
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -19,29 +19,38 @@ inductive Site where
 instance : Coe MVarId Site where
  coe := .focus

-protected def Site.runTacticM (site : Site) { m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m]
-  (f : m α) : m α :=
+/-- Executes a `TacticM` on a site and return affected goals -/
+protected def Site.runTacticM (site : Site)
+  { m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m] [MonadMCtx m] [MonadError m]
+  (f : m α) : m (α × List MVarId) :=
  match site with
  | .focus goal => do
    Elab.Tactic.setGoals [goal]
-    f
+    let a ← f
+    return (a, [goal])
  | .prefer goal => do
-    let otherGoals := (← Elab.Tactic.getUnsolvedGoals).filter (· != goal)
+    let prev ← Elab.Tactic.getUnsolvedGoals
+    let otherGoals := prev.filter (· != goal)
    Elab.Tactic.setGoals (goal :: otherGoals)
-    f
-  | .unfocus => f
+    let a ← f
+    return (a, ← prev.filterM (·.isAssignedOrDelayedAssigned))
+  | .unfocus => do
+    let prev ← Elab.Tactic.getUnsolvedGoals
+    let a ← f
+    return (a, ← prev.filterM (·.isAssignedOrDelayedAssigned))

 /--
-Represents an interconnected set of metavariables, or a state in proof search
+Kernel view of the state of a proof
 -/
 structure GoalState where
+  -- Captured `TacticM` state
  savedState : Elab.Tactic.SavedState

-  -- The root hole which is the search target
+  -- The root goal which is the search target
  root: MVarId

-  -- Parent state metavariable source
-  parentMVar?: Option MVarId := .none
+  -- Parent goals assigned to produce this state
+  parentMVars : List MVarId := []

  -- Any goal associated with a fragment has a partial tactic which has not
  -- finished executing.
@ -60,7 +69,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
  return {
    root := root.mvarId!,
    savedState,
-    parentMVar? := .none,
  }
@[export pantograph_goal_state_create_from_mvars_m]
 protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
@ -69,7 +77,6 @@ protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): Met
  return {
    root,
    savedState,
-    parentMVar? := .none,
  }
 protected def GoalState.goals (state: GoalState): List MVarId :=
  state.savedState.tactic.goals
@ -93,8 +100,9 @@ protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: Met
  mvarId.withContext m |>.run' (← read) state.metaState
 protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
  Meta.mapMetaM <| state.withContext' mvarId
+/-- Uses context of the first parent -/
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
+  Meta.mapMetaM <| state.withContext' state.parentMVars[0]!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
  Meta.mapMetaM <| state.withContext' state.root

@ -115,16 +123,6 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
  state.restoreElabM
  Elab.Tactic.setGoals [goal]

-@[export pantograph_goal_state_focus]
-protected def GoalState.focus (state : GoalState) (goal : MVarId): Option GoalState := do
-  return {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := [goal] },
-    },
-  }
-
 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
@[export pantograph_goal_state_immediate_resume]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
@ -186,17 +184,19 @@ protected def GoalState.isSolved (goalState : GoalState) : Bool :=
    | .some e => ¬ e.hasExprMVar
    | .none => true
  goalState.goals.isEmpty && solvedRoot
-@[export pantograph_goal_state_parent_expr]
-protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar?
-  let expr := goalState.mctx.eAssignment.find! parent
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
@[export pantograph_goal_state_get_mvar_e_assignment]
 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
+@[export pantograph_goal_state_parent_exprs]
+protected def GoalState.parentExprs (state : GoalState) : List Expr :=
+  state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get!
+protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
+  state.parentMVars.length == 1
+protected def GoalState.parentExpr! (state : GoalState) : Expr :=
+  assert! state.parentMVars.length == 1
+  (state.getMVarEAssignment state.parentMVars[0]!).get!

 deriving instance BEq for DelayedMetavarAssignment

@ -232,6 +232,8 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
      else
        id
    | id => id
+  let mapMVar : MVarId → MVarId
+    | { name } => ⟨mapId name⟩
  let rec mapLevel : Level → Level
    | .succ x => .succ (mapLevel x)
    | .max l1 l2 => .max (mapLevel l1) (mapLevel l2)
@ -245,7 +247,7 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
  let mapDelayedAssignment (d : DelayedMetavarAssignment) : CoreM DelayedMetavarAssignment := do
    let { mvarIdPending, fvars } := d
    return {
-      mvarIdPending := ⟨mapId mvarIdPending.name⟩,
+      mvarIdPending := mapMVar mvarIdPending,
      fvars := ← fvars.mapM mapExpr,
    }
  let mapLocalDecl (ldecl : LocalDecl) : CoreM LocalDecl := do
@ -376,18 +378,21 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
        meta := ← m.run',
      },
    },
+    parentMVars := dst.parentMVars ++ src.parentMVars.map mapMVar,
    fragments,
  }

 --- Tactic execution functions ---

-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
+/--
+These descendants serve as "seed" mvars. If a MVarError's mvar is related to one
+of these seed mvars, it means an error has occurred when a tactic was executing
+on `src`. `evalTactic`, will not capture these mvars, so we need to manually
+find them and save them into the goal list. See the rationales document for the
+inspiration of this function.
+-/
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
-  -- These descendants serve as "seed" mvars. If a MVarError's mvar is related
-  -- to one of these seed mvars, it means an error has occurred when a tactic
-  -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
-  -- need to manually find them and save them into the goal list.
-
+  -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
  let descendants ←  Meta.getMVars (.mvar src)
  --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
  let mut alreadyVisited : MVarIdSet := {}
@ -411,28 +416,29 @@ Set `guardMVarErrors` to true to capture mvar errors. Lean will not
 automatically collect mvars from text tactics (vide
 `test_tactic_failure_synthesize_placeholder`)
 -/
-protected def GoalState.step' { α } (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
+protected def GoalState.step' { α } (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
  : Elab.TermElabM (α × GoalState) := do
-  unless (← getMCtx).decls.contains goal do
-    throwError s!"Goal is not in context: {goal.name}"
-  goal.checkNotAssigned `GoalState.step
-  let (a, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+  let ((a, parentMVars), { goals }) ← site.runTacticM tacticM
+    |>.run { elaborator := .anonymous }
+    |>.run state.savedState.tactic
  let nextElabState ← MonadBacktrack.saveState
  --Elab.Term.synthesizeSyntheticMVarsNoPostponing

  let goals ← if guardMVarErrors then
-      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
+      parentMVars.foldlM (init := goals) λ goals parent => do
+        let errors ← collectAllErroredMVars parent
+        return mergeMVarLists goals errors
    else
      pure goals
  let state' := {
    state with
    savedState := { term := nextElabState, tactic := { goals }, },
-    parentMVar? := .some goal,
+    parentMVars,
  }
  return (a, state')
-protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
+protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
  : Elab.TermElabM GoalState :=
-  Prod.snd <$> GoalState.step' state goal tacticM guardMVarErrors
+  Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors

 /-- Response for executing a tactic -/
 inductive TacticResult where
@ -539,12 +545,12 @@ protected def GoalState.conv (state : GoalState) (goal : MVarId) :
      Elab.TermElabM TacticResult := do
  if let .some (.conv ..) := state.fragments[goal]? then
    return .invalidAction "Already in conv state"
-  goal.checkNotAssigned `GoalState.conv
  withCapturingError do
-    let (fragment, state') ← state.step' goal Fragment.enterConv
+    let (fragments, state') ← state.step' goal Fragment.enterConv
    return {
      state' with
-      fragments := state'.fragments.insert goal fragment
+      fragments := fragments.fold (init := state'.fragments) λ acc goal fragment =>
+        acc.insert goal fragment
    }

 /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -117,10 +117,10 @@ def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState :

@[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
-  runMetaM <| state.serializeGoals (parent := .none) options
+  runMetaM <| state.serializeGoals options

@[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
+def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
  : CoreM Protocol.GoalPrintResult := runMetaM do
  state.restoreMetaM

@ -130,9 +130,10 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
        serializeExpression options (← instantiateAll expr)
    else
      pure .none
-  let parent? ← if parentExpr then
-      state.parentExpr?.mapM λ expr => state.withParentContext do
-        serializeExpression options (← instantiateAll expr)
+  let parentExprs? ← if parentExprs then
+      .some <$> state.parentMVars.mapM λ parent => parent.withContext do
+        let val := state.getMVarEAssignment parent |>.get!
+        serializeExpression options (← instantiateAll val)
    else
      pure .none
  let goals ← if goals then
@ -148,7 +149,7 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
  let env ← getEnv
  return {
    root?,
-    parent?,
+    parentExprs?,
    goals,
    extraMVars,
    rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -308,8 +308,8 @@ structure GoalPrint where

  -- Print root?
  rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
-  parentExpr?: Option Bool := .some False
+  -- Print the parent expressions
+  parentExprs?: Option Bool := .some False
  -- Print goals?
  goals?: Option Bool := .some False
  -- Print values of extra mvars?
@ -319,7 +319,7 @@ structure GoalPrintResult where
  -- The root expression
  root?: Option Expression := .none
  -- The filling expression of the parent goal
-  parent?: Option Expression := .none
+  parentExprs?: Option (List Expression) := .none
  goals: Array Goal := #[]
  extraMVars: Array Expression := #[]

--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -103,7 +103,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
      tactic
    }
    root,
-    parentMVar?,
+    parentMVars,
    fragments,
  } := goalState
  Pantograph.pickle path (
@ -115,7 +115,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
    tactic,

    root,
-    parentMVar?,
+    parentMVars,
    fragments,
  )

@ -131,7 +131,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    tactic,

    root,
-    parentMVar?,
+    parentMVars,
    fragments,
  ), region) ← Pantograph.unpickle (
    PHashMap Name ConstantInfo ×
@ -142,7 +142,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    Elab.Tactic.State ×

    MVarId ×
-    Option MVarId ×
+    List MVarId ×
    FragmentMap
  ) path
  let env ← env.replay (Std.HashMap.ofList map₂.toList)
@ -162,7 +162,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
      tactic,
    },
    root,
-    parentMVar?,
+    parentMVars,
    fragments,
  }
  return (goalState, region)
--- a/Pantograph/Tactic/Fragment.lean
+++ b/Pantograph/Tactic/Fragment.lean
@ -15,30 +15,38 @@ namespace Pantograph
 inductive Fragment where
  | calc (prevRhs? : Option Expr)
  | conv (rhs : MVarId) (dormant : List MVarId)
+  -- This goal is spawned from a `conv`
+  | convSentinel (parent : MVarId)
  deriving BEq
 abbrev FragmentMap := Std.HashMap MVarId Fragment
 def FragmentMap.empty : FragmentMap := Std.HashMap.emptyWithCapacity 2

 protected def Fragment.map (fragment : Fragment) (mapExpr : Expr → CoreM Expr) : CoreM Fragment :=
-  let mapMVarId (mvarId : MVarId) : CoreM MVarId :=
+  let mapMVar (mvarId : MVarId) : CoreM MVarId :=
    return (← mapExpr (.mvar mvarId)) |>.mvarId!
  match fragment with
  | .calc prevRhs? => return .calc (← prevRhs?.mapM mapExpr)
  | .conv rhs dormant => do
-    let rhs' ← mapMVarId rhs
-    let dormant' ← dormant.mapM mapMVarId
+    let rhs' ← mapMVar rhs
+    let dormant' ← dormant.mapM mapMVar
    return .conv rhs' dormant'
+  | .convSentinel parent => do
+    return .convSentinel (← mapMVar parent)

 protected def Fragment.enterCalc : Elab.Tactic.TacticM Fragment := do
  return .calc .none
-protected def Fragment.enterConv : Elab.Tactic.TacticM Fragment := do
+protected def Fragment.enterConv : Elab.Tactic.TacticM FragmentMap := do
  let goal ← Elab.Tactic.getMainGoal
-  let rhs ← goal.withContext do
-    let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
-    Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
-    pure rhs.mvarId!
+  goal.checkNotAssigned `GoalState.conv
+  let (rhs, newGoal) ← goal.withContext do
+    let target ← instantiateMVars (← goal.getType)
+    let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor target
+    pure (rhs.mvarId!, newGoal.mvarId!)
+  Elab.Tactic.replaceMainGoal [newGoal]
  let otherGoals := (← Elab.Tactic.getGoals).filter (· != goal)
-  return conv rhs otherGoals
+  return FragmentMap.empty
+    |>.insert goal (.conv rhs otherGoals)
+    |>.insert newGoal (.convSentinel goal)

 protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
  : Elab.Tactic.TacticM FragmentMap :=
@ -47,11 +55,10 @@ protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : F
    Elab.Tactic.setGoals [goal]
    return fragments.erase goal
  | .conv rhs otherGoals => do
-    -- FIXME: Only process the goals that are descendants of `goal`
-    let goals := (← Elab.Tactic.getGoals).filter λ goal => true
-      --match fragments[goal]? with
-      --| .some f => fragment == f
-      --| .none => false -- Not a conv goal from this
+    let goals := (← Elab.Tactic.getGoals).filter λ descendant =>
+      match fragments[descendant]? with
+      | .some s => (.convSentinel goal) == s
+      | _ => false -- Not a conv goal from this
    -- Close all existing goals with `refl`
    for mvarId in goals do
      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
@ -65,6 +72,8 @@ protected def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : F

    Elab.Tactic.liftMetaTactic1 (·.replaceTargetEq targetNew proof)
    return fragments.erase goal
+  | .convSentinel _ =>
+    return fragments.erase goal

 protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String)
  : Elab.Tactic.TacticM FragmentMap := goal.withContext do
@ -125,5 +134,19 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String)
    | .none => return .empty
  | .conv .. => do
    throwError "Direct operation on conversion tactic parent goal is not allowed"
+  | fragment@(.convSentinel _) => do
+    let tactic ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `conv)
+      (input := s)
+      (fileName := ← getFileName) with
+      | .ok stx => pure $ stx
+      | .error error => throwError error
+    let oldGoals ← Elab.Tactic.getGoals
+    -- Label newly generated goals as conv sentinels
+    Elab.Tactic.evalTactic tactic
+    let newGoals := (← Elab.Tactic.getUnsolvedGoals).filter λ g => ¬ (oldGoals.contains g)
+    return newGoals.foldl (init := FragmentMap.empty) λ acc g =>
+      acc.insert g fragment

 end Pantograph
--- a/Repl.lean
+++ b/Repl.lean
@ -340,14 +340,16 @@ def execute (command: Protocol.Command): MainM Json := do
        | true, .some false => pure nextGoalState
        | false, _ => pure nextGoalState
      let nextStateId ← newGoalState nextGoalState
-      let parentExpr := nextGoalState.parentExpr?.get!
-      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+      let parentExprs := nextGoalState.parentExprs
+      let hasSorry := parentExprs.any (·.hasSorry)
+      let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·)
+      let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
      return {
        nextStateId? := .some nextStateId,
        goals? := .some goals,
        messages? := .some messages,
-        hasSorry := parentExpr.hasSorry,
-        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
+        hasSorry,
+        hasUnsafe,
      }
    | .ok (.parseError message) =>
      return { messages? := .none, parseError? := .some message }
@ -389,7 +391,7 @@ def execute (command: Protocol.Command): MainM Json := do
    let result ← liftMetaM <| goalPrint
        goalState
        (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
+        (parentExprs := args.parentExprs?.getD False)
        (goals := args.goals?.getD False)
        (extraMVars := args.extraMVars?.getD #[])
        (options := state.options)
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -88,10 +88,10 @@ def test_tactic : Test := do
   ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
  step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
-  step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
+  step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
   ({
     root? := .some { pp? := "fun x => ?m.11"},
-     parent? := .some { pp? := .some "fun x => ?m.11" },
+     parentExprs? := .some [{ pp? := .some "fun x => ?m.11" }],
   }: Protocol.GoalPrintResult)
  step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
   ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -77,7 +77,7 @@ def test_identity: TestM Unit := do
  addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
    #[inner])
  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")

 -- Individual test cases
@ -117,41 +117,6 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
  addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty

  return ()
-def test_delta_variable: TestM Unit := do
-  let options: Protocol.Options := { noRepeat := true }
-  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
-  addTest $ LSpec.check "Start goal" state?.isSome
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  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.tacticOn (goalId := 0) (tactic := "intro m") with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
-    #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
-  return ()
-  where
-- Like `buildGoal` but allow certain variables to be elided.
-  buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
-    {
-      target := { pp? := .some target},
-      vars := (nameType.map fun x => ({
-        userName := x.fst,
-        type? := x.snd.map (λ type => { pp? := type }),
-      })).toArray
-    }

 example (w x y z : Nat) (p : Nat → Prop)
        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
@ -212,8 +177,8 @@ def test_or_comm: TestM Unit := do
    | .none => do
      addTest $ assertUnreachable "Goal could not parse"
      return ()
-  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
-  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
+  checkTrue "(0 parent)" state0.parentMVars.isEmpty
+  checkTrue "(0 root)" state0.rootExpr?.isNone

  let tactic := "intro p q h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
@ -237,11 +202,11 @@ def test_or_comm: TestM Unit := do
        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
      ]
    }])
-  checkTrue "(1 parent)" state1.parentExpr?.isSome
+  checkTrue "(1 parent)" state1.hasUniqueParent
  checkTrue "(1 root)" $ ¬ state1.isSolved

  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
  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.tacticOn (goalId := 0) (tactic := tactic) with
@ -256,11 +221,11 @@ def test_or_comm: TestM Unit := do
  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
    #[caseL, caseR])
-  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
+  checkTrue "(2 parent exists)" state2.hasUniqueParent
  checkTrue "(2 root)" $ ¬ state2.isSolved

  let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr!)
  let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
  let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
  let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
@ -276,7 +241,7 @@ def test_or_comm: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr!)
  let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
@ -286,7 +251,7 @@ def test_or_comm: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
+  let state4_1parent ← instantiateAll state4_1.parentExpr!
  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
  checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
  let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
@ -600,7 +565,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
    ("identity", test_identity),
    ("Nat.add_comm", test_nat_add_comm false),
    ("Nat.add_comm manual", test_nat_add_comm true),
-    ("Nat.add_comm delta", test_delta_variable),
    ("arithmetic", test_arith),
    ("Or.comm", test_or_comm),
    ("conv", test_conv),
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -87,12 +87,12 @@ def test_pickling_env_extensions : TestM Unit := do
      let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
      pure (type, value)
    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
-    let parentExpr := state1.parentExpr?.get!
+    let parentExpr := state1.parentExpr!
    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
    goalStatePickle state1 statePath
  let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
    let (state1, _) ← goalStateUnpickle statePath (← getEnv)
-    let parentExpr := state1.parentExpr?.get!
+    let parentExpr := state1.parentExpr!
    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma

  return ()