5.3.1. 基本 API🔗

-- [示意]
getGoals : TacticM (List MVarId)            -- 获取全部目标（含可能已解决的）
setGoals (gs : List MVarId) : TacticM Unit  -- 设置全部目标
getMainGoal : TacticM MVarId                -- 获取第一个目标（主目标）
getUnsolvedGoals : TacticM (List MVarId)    -- 过滤掉已赋值的目标

getGoals 和 setGoals 是最底层的操作——它们直接读写 tactic state 中的目标列表，不做任何过滤或检查。getMainGoal 则是 getGoals 的便利包装：它取出列表的第一个元素，如果列表为空就抛出 "no goals" 错误。

getUnsolvedGoals 值得特别关注。它不仅获取目标列表，还会对每个目标调用 MVarId.isAssigned，只保留尚未赋值的目标。这在你处理完一批目标后特别有用——你不需要手动追踪哪些目标已经被解决，只需在最后调用 getUnsolvedGoals 就能得到干净的列表。

5.3.2. 常见模式🔗

-- [示意]
-- 模式 1（推荐）：用 replaceMainGoal 替换主目标
elab "my_tactic" : tactic => do
  let goal ← getMainGoal
  -- ... 处理 goal，产生 newGoals ...
  replaceMainGoal newGoals

模式 1 是最常见的 tactic 结构。replaceMainGoal newGoals 会把主目标从列表中移除，并把 newGoals 插到列表前面、其余目标保留在后面。这遵循了 Lean 的惯例：新子目标总是排在前面，这样用户会按"深度优先"的顺序处理它们。

为什么推荐 replaceMainGoal？ 它在内部完成了"取出其余目标、拼接新目标"的逻辑，等价于：

-- [示意]
-- replaceMainGoal 的等价手写版（不推荐，仅供理解）
let rest := (← getGoals).erase goal
setGoals (newGoals ++ rest)

直接用 replaceMainGoal 更简洁、不容易出错，应作为模式 1 的首选写法。

-- [示意]
-- 模式 2：处理所有目标
elab "my_tactic_all" : tactic => do
  let goals ← getGoals
  let mut remaining := []
  for g in goals do
    -- ... 尝试处理 g ...
    if !(← g.isAssigned) then
      remaining := remaining ++ [g]
  setGoals remaining

模式 2 遍历所有目标并逐一处理。在循环结束后，用 isAssigned 过滤掉已解决的目标。这里有一个微妙之处：处理某个目标时可能会间接影响其他目标，比如 unification 可能会把两个目标中共享的元变量统一起来。所以即使你没有显式处理某个目标，它也可能在循环中途变成"已解决"的。

-- [示意]
-- 模式 3：交换目标顺序
elab "swap" : tactic => do
  let goals ← getGoals
  match goals with
- g1 :: g2 :: rest => setGoals (g2 :: g1 :: rest)：_ => throwError "swap requires at least 2 goals"

模式 3 展示了目标列表操作的灵活性：你可以任意重新排列目标的顺序。实际上 Lean 内置的 rotate_left、rotate_right、swap 等 tactic 就是这样实现的——纯粹的列表操作，不涉及任何证明项的构造。

5.5.1. 基本用法🔗

-- [示意]
elab "try_or_skip" : tactic => do
  let state ← saveState
  try
    evalTactic (← `(tactic| assumption))
  catch _ =>
    restoreState state
    -- assumption 失败了，恢复状态，什么都不做

这里的流程是：先把当前完整状态保存到 state，然后尝试执行 assumption。如果 assumption 成功，皆大欢喜，state 就被丢弃了。如果 assumption 抛出异常（说明它无法解决当前目标），catch 会捕获异常，调用 restoreState state 回退到尝试之前的状态。

5.5.2. saveState 保存了什么？🔗

saveState 保存的是完整的 Meta.State 和 Core.State，其中最重要的部分是 MetavarContext——它记录了所有元变量的赋值情况以及 universe 约束。这意味着 restoreState 不仅会回退目标列表，还会撤销所有 unification 产生的副作用。

为什么这很重要？因为 tactic 执行过程中，apply 或 unify 可能会给一些元变量赋值，而这些元变量可能不仅仅属于当前目标——它们可能是多个目标共享的。如果你只回退目标列表而不回退 MetavarContext，那些共享的元变量就会残留着"试探性赋值"，导致后续的 tactic 行为异常。restoreState 通过一次性回退整个状态来避免这个问题。

5.5.3. 更高层的封装：tryTactic?🔗

-- [示意]
-- 尝试执行 tac，失败则恢复状态并返回 none
def tryTactic? (tac : TacticM α) : TacticM (Option α) := do
  let s ← saveState
  try
    let r ← tac
    return some r
  catch _ =>
    restoreState s
    return none

tryTactic? 把"试一试"的模式封装成了返回 Option 的函数。如果 tac 成功，返回 some r；如果失败，恢复状态并返回 none。调用者可以用 match 或 if let 来分支处理，而不需要手动写 try/catch/restoreState。

这个模式在编写"先试策略 A，不行试策略 B"的 tactic 时特别有用：

-- [示意]
elab "try_simp_then_omega" : tactic => do
  if let some _ ← tryTactic? (evalTactic (← `(tactic| simp))) then
    return  -- simp 成功，结束
  if let some _ ← tryTactic? (evalTactic (← `(tactic| omega))) then
    return  -- omega 成功，结束
  throwError "neither simp nor omega worked"

5.6.1. 方式 1：用 evalTactic 执行语法🔗

-- [示意]
elab "my_combo" : tactic => do
  evalTactic (← `(tactic| simp))
  evalTactic (← `(tactic| ring))

evalTactic 接受一个 Syntax 参数（通过 `(tactic| ...) 引用构造），然后像用户在交互模式中输入这个 tactic 一样执行它。这是最通用的方式——任何用户能在 by 块中写的 tactic，你都能通过 evalTactic 调用。

它的缺点是间接性：每次调用都要经过语法解析和 tactic 分发（elaborate），比直接调用底层 API 函数慢一些。但在大多数场景下，这点开销可以忽略不计。

5.6.2. 方式 2：直接调用实现函数🔗

-- [示意]
import Lean.Elab.Tactic.Simp

elab "simp_then_check" : tactic => do
  evalTactic (← `(tactic| simp))
  let goals ← getUnsolvedGoals
  if goals.isEmpty then
    logInfo "simp closed everything!"
  else
    logInfo m!"simp left {goals.length} goals"

虽然这个例子仍然用了 evalTactic，但你也可以直接调用 simp 的底层 API（如 Lean.Meta.Simp.simp）来获得更细粒度的控制——比如指定 simp lemma 集合、控制展开深度等。直接调用底层函数的好处是性能更好、控制更精细；缺点是你需要了解该 tactic 的内部 API，而这些 API 不一定有稳定的接口保证。

选择建议：如果你只是想"在我的 tactic 中途调用一下 simp"，用 evalTactic 就够了。如果你需要精细控制或者性能敏感，再考虑直接调用底层 API。

5.7.1. 问题背景🔗

在 tactic 编程中，有一个容易踩的坑：局部上下文不匹配。每个目标（MVarId）都有自己的局部上下文（local context），包含了该目标可见的局部变量和假设。当你调用 getLCtx 获取局部上下文时，拿到的是当前活跃的上下文，而这个上下文不一定是你正在操作的那个目标的上下文。

举个例子：你用 getMainGoal 拿到了目标 g，然后直接调用 getLCtx。如果之前有别的操作切换过上下文，getLCtx 返回的可能不是 g 的上下文，而是之前某个操作遗留下来的上下文。这会导致你在错误的上下文中查找假设，产生难以排查的 bug。

5.7.2. 解决方案🔗

-- [示意]
elab "safe_tactic" : tactic => do
  withMainContext do        -- 自动切换到主目标的上下文
    let target ← getMainTarget
    -- 这里的 getLCtx 保证是主目标的局部上下文
    let lctx ← getLCtx
    -- ... 在正确的上下文中操作 ...

withMainContext 的实现等价于 getMainGoal >>= fun g => g.withContext。它做了两件事：取出主目标，然后在该目标的局部上下文中执行后续代码。这样你在 do 块中调用 getLCtx、getLocalDecl 等 API 时，总是能拿到正确的上下文。

5.7.3. withMainContext vs withContext 的区别🔗

withContext 是更底层的 API：g.withContext do ... 在目标 g 的上下文中执行代码。你需要自己指定是哪个目标。

withMainContext 是语法糖：它自动选择主目标。在大多数 tactic 中，你操作的就是主目标，所以用 withMainContext 更简洁。

但如果你在遍历多个目标（比如模式 2 中的循环），你应该用 g.withContext 而不是 withMainContext——因为循环中的 g 不一定是主目标：

-- [示意]
elab "inspect_all" : tactic => do
  for g in (← getGoals) do
    g.withContext do           -- 用 g 的上下文，而非主目标的
      let target ← g.getType
      let lctx ← getLCtx
      logInfo m!"Goal {g.name} has {lctx.size} local decls, target: {target}"

如果在这个循环里用 withMainContext，每次迭代都会切换到主目标的上下文，而不是当前循环变量 g 的上下文——这几乎肯定不是你想要的。

5.8.1. 4.7.1 忘了更新 goals 列表🔗

症状：你的 tactic 把主目标解决了（给它 assign 了一个证明项），但后续 tactic 仍然试图操作已解决的目标，或者 Lean InfoView 显示的目标没有变化。

原因：你 assign 了目标，但没有调用 setGoals 把已解决的目标从列表中移除。

-- [示意]
-- ❌ 错误写法
elab "bad_exact" : tactic => do
  let goal ← getMainGoal
  goal.assign someProofTerm
  -- 忘了 setGoals！goal 仍在列表中

-- ✅ 正确写法
elab "good_exact" : tactic => do
  let goal ← getMainGoal
  goal.assign someProofTerm
  let remaining ← getUnsolvedGoals  -- 自动过滤已赋值的目标
  setGoals remaining

建议：如果你的 tactic 可能通过 assign 解决目标却没有同步更新列表，可以在最后调用 setGoals (← getUnsolvedGoals) 来清理残留的已解决目标。但这只是一个防御性清理手段，不应作为通用模板——在大多数场景下，优先使用 replaceMainGoal 来精确管理目标列表，而不是依赖最后的"大扫除"。

5.8.2. 4.7.2 saveState 和 restoreState 的正确用法🔗

症状：你用了 try/catch 来回退失败的尝试，但回退后状态仍然不干净——有些元变量残留了赋值。

原因：你在 catch 中忘了 restoreState，或者在 try 块外面保存了状态但在 try 块里面又进行了会影响状态的操作。

-- [示意]
-- ❌ 常见错误：忘了 restoreState
elab "bad_try" : tactic => do
  try
    evalTactic (← `(tactic| apply And.intro))
  catch _ =>
    pure ()  -- 没有 restoreState！
    -- apply 可能已经创建了新的元变量或做了 unification
    -- 这些副作用会残留

-- ✅ 正确写法
elab "good_try" : tactic => do
  let s ← saveState
  try
    evalTactic (← `(tactic| apply And.intro))
  catch _ =>
    restoreState s  -- 完全回退

另一个常见错误是在错误的位置保存状态。如果你在循环中多次保存/恢复，确保每次保存的是当次迭代开始时的状态，而不是循环开始前的总状态——否则每次恢复都会回退到循环起点，丢失前面迭代的成果。

5.8.3. 4.7.3 focus 的副作用🔗

症状：在 focus 块结束后，你发现某些目标"消失了"，或者目标的顺序与预期不同。

原因：focus 在结束时会把 tac 执行后的目标列表和之前"摘走"的 rest 拼接在一起。如果 tac 内部调用了 setGoals 并且不小心把 rest 中的目标也加进去（例如通过某个间接调用），focus 结束后这些目标就会出现两次。

-- [示意]
-- ❌ 可能出问题的用法
elab "focus_danger" : tactic => do
  Lean.Elab.Tactic.focus do
    let allGoals ← getGoals  -- focus 内部，只能看到主目标
    -- 但如果你在这里通过 MetavarContext 获取了其他目标并加到列表中...
    -- focus 结束时会把它们和 rest 拼起来，可能导致重复

建议：在 focus 块内部，不要往目标列表中添加不属于当前 focus 范围的目标。focus 的契约是"进去时只看到主目标，出来时只有新产生的子目标"。遵守这个契约就不会出问题。

5.8.4. 4.7.4 withMainContext vs withContext 的误用🔗

症状：你在遍历多个目标时，每个目标拿到的局部上下文都一样——都是主目标的上下文。

原因：在循环中用了 withMainContext 而不是 g.withContext。详见 4.6 节的讨论。

调试技巧：在循环中加一行 logInfo m!"Processing goal {g.name} in context with {(← getLCtx).size} decls"，如果每次打印的 size 都一样（且不符合预期），说明上下文切换有问题。

5.8.5. 4.7.5 通用调试手段🔗

当 tactic 的行为不符合预期时，以下手段可以帮助你定位问题：

1. logInfo 打印状态：在关键位置打印目标列表的长度和内容。logInfo m!"goals: {← getGoals}" 会显示当前所有目标的 MVarId。

2. isAssigned 检查：在 setGoals 之前，检查每个目标的赋值状态。for g in goals do logInfo m!"{g.name}: assigned={← g.isAssigned}" 可以帮你确认哪些目标已经被解决了。

3. 最小化复现：把 tactic 拆成更小的步骤，在每步之后检查目标状态。这比在整个 tactic 上猜测问题原因要高效得多。

4. trace 系统：Lean 提供了 trace[Meta.Tactic] 等 trace 选项，可以打印 tactic 框架内部的执行细节。通过 set_option trace.Meta.Tactic true 开启。

5.9.1. 热身练习🔗

练习 4.1：rotate_goals

实现一个 tactic rotate_goals，它把目标列表"旋转"一个位置：主目标移到列表末尾，第二个目标变成新的主目标。如果只有一个或零个目标，什么都不做。

提示：你只需要用 getGoals 和 setGoals，加上列表操作。

练习 4.2：count_goals

实现一个 tactic count_goals，它不改变任何状态，只在 InfoView 中打印当前未解决的目标数量。

提示：使用 getUnsolvedGoals 和 logInfo。

5.9.2. Debug 练习🔗

练习 4.3：找出 bug

下面的 tactic 试图对每个目标尝试 assumption，解决能解决的，保留不能解决的。但它有一个 bug——找出来并修复它。

提示：考虑两个问题——（1）evalTactic 默认作用于主目标（即目标列表的第一个元素），而不是循环变量 g——所以循环中每次 assumption 操作的未必是你期望的目标；（2）失败时状态有没有被正确恢复？

5.9.3. 综合练习🔗

练习 4.4：first_success

实现一个 tactic first_success，它接受一个 tactic 列表，对主目标依次尝试每个 tactic，使用第一个成功的。如果全部失败，抛出错误信息列出所有尝试过的 tactic 和它们的错误。

-- [伪代码]
-- 目标行为：
-- first_success [simp, omega, assumption]
-- 等价于：先试 simp，不行试 omega，不行试 assumption，全不行则报错

elab "first_success" : tactic => do
  sorry -- 你的实现

提示：使用 saveState/restoreState 进行回溯。把每次失败的错误信息收集起来，如果全部失败，用 throwError 一次性报告。