Simulating conversion tactic with evalTactic

Stream: lean4

[Leni Aniva]

Consider this example

example : ∀ (a b c : Nat), a * (b * c) = a * (c * b) := by
  intro a b c
  conv =>
    lhs
    congr
    rfl
    rw [Nat.mul_comm]

After conv =>, the current proof state shows the conversion goal | a * (b * c) = a * (c * b). I would like to simulate this with Tactic.evalTactic:

import Lean

open Lean Elab Term Meta

def start_tactic_state (goal : String)
    (x : Tactic.SavedState → MVarId → Tactic.TacticM Unit) : CoreM Unit := do
  MetaM.run' <| TermElabM.run' <| do
  let .ok syn := Parser.runParserCategory (← getEnv) `term goal (fileName := "<stdin>") | failure
  let expr ← elabType syn
  synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  let g := (← mkFreshExprMVar expr).mvarId!
  let goals ← Tactic.run g do
      IO.println "Tactic state started"
      x (← saveState) g
  if goals.isEmpty then
    IO.println "goals accomplished"
  else
    let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
    IO.println s!"goals not solved: {goals}"

def execute_tactic (state : Tactic.SavedState) (g : MVarId) (tactic : String) :
    Tactic.TacticM (Tactic.SavedState × List MVarId) := do
  state.restore
  Tactic.setGoals [g]
  let .ok stx :=
    Parser.runParserCategory (← getEnv) `tactic tactic (fileName := "<stdin>") | failure
  try
    Tactic.evalTactic stx
  catch e =>
    IO.println s!"{← e.toMessageData.toString}"
    return (state, [g])
  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← (messages.map Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return (state, [g])
  let unsolvedGoals ← Tactic.getUnsolvedGoals
  let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
  IO.println s!"Tactic succeeded with goals {goals}"
  return (← saveState, unsolvedGoals)

def proof_1: CoreM Unit := do
  start_tactic_state "∀ (p q: Prop), p ∨ q → q ∨ p" fun state g => do
    let (state, [g]) ← execute_tactic state g "intro p q h" | failure
    let (state, [g1, g2]) ← execute_tactic state g "cases h" | failure
    let (state, [g1]) ← execute_tactic state g1 "apply Or.inr" | failure
    let (state, []) ← execute_tactic state g1 "assumption" | failure
    let (state, [g2]) ← execute_tactic state g2 "apply Or.inl" | failure
    let (_, []) ← execute_tactic state g2 "assumption" | failure

def proof_2: CoreM Unit := do
  start_tactic_state "∀ (a b c: Nat), a * (b * c) = a * (c * b)" fun state g => do
    let (state, [g]) ← execute_tactic state g "intro a b c" | failure
    let (state, [g1]) ← execute_tactic state g "conv => lhs" | failure


def main: IO Unit := do
  let env ← importModules
    (imports := [{ module := Name.str .anonymous "Init", runtimeOnly := false }])
    (opts := {})
    (trustLevel := 1)
  let coreContext : Core.Context := {
    currNamespace := Name.anonymous,
    openDecls := [],     -- No 'open' directives needed
    fileName := "<onion>",
    fileMap := { source := "", positions := #[0], lines := #[1] }
  }
  discard <| proof_2.toIO coreContext { env := env }

However, this outputs

Tactic state started
Tactic succeeded with goals [a b c : Nat
⊢ a * (b * c) = a * (c * b)]
Tactic succeeded with goals [a b c : Nat
⊢ a * (b * c) = a * (c * b)]
goals not solved: [a b c : Nat
⊢ a * (b * c) = a * (c * b)]

which shows that the state has exited conversion mode. If I replace conv => lhs by conv, The tactic fails.

Is there a way to interactively view the result of conversion mode?