2.2.1. CoreM：基础层🔗

Lean.CoreM 是整个系统的地基。它的 State 包含：

structure State where
  env           : Environment      -- 当前环境（所有定义/定理）
  nextMacroScope: MacroScope       -- 宏展开用的作用域计数器
  ngen          : NameGenerator    -- 唯一名字生成器
  traceState    : TraceState       -- trace 信息
  messages      : MessageLog       -- 错误/警告消息

它的 Context 包含：

structure Context where
  fileName      : String           -- 当前文件名
  options       : Options          -- 用户选项（set_option）
  currNamespace : Name             -- 当前命名空间
  maxHeartbeats : Nat              -- 超时限制
  currMacroScope: MacroScope       -- 当前宏作用域

CoreM 能做什么：查询/修改环境、生成新名字、记录消息、读取选项。不能做类型检查或创建元变量。

2.2.2. MetaM：元变量与类型检查🔗

MetaM 在 CoreM 之上添加了：

• LocalContext：当前的局部变量（free variables, FVarId）

• MetavarContext：所有元变量（MVarId）的声明和赋值

• 类型检查缓存：inferType、isDefEq、whnf 的结果缓存

MetaM 是 Lean 元编程的核心层。以下关键操作都在 MetaM 中：

• inferType e：推断表达式 e 的类型

• isDefEq e1 e2：判断两个表达式是否定义等价（可能赋值元变量）

• whnf e：将表达式规约到弱头范式

• mkFreshExprMVar t：创建类型为 t 的新元变量

• forallTelescope T f：展开 ∀ 类型，进入其 body

• lambdaTelescope e f：展开 λ 表达式，进入其 body

2.2.3. TermElabM：项的精化🔗

TermElabM 处理从语法到表达式的转换（elaboration）。当你写 x + 1，elaborator 负责：

• 推断 x 的类型

• 找到合适的 + 实例

• 插入隐式参数

对于 tactic 编写者，TermElabM 主要用于在 tactic 中使用 elabTerm 将语法片段精化为表达式。

2.2.4. TacticM：目标管理🔗

TacticM 是 tactic 的直接运行环境。它的 State 核心很简单：

-- Lean/Elab/Tactic/Basic.lean
structure State where
  goals : List MVarId   -- 当前待证目标列表

abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
abbrev Tactic  := Syntax → TacticM Unit

关键心智模型：一个 tactic 接收一个 goals : List MVarId，执行某些操作后产生新的 goals。"证明完成"就是 goals 变为空列表。

基本的目标操作：

def getGoals : TacticM (List MVarId)      -- 获取当前所有目标
def setGoals (gs : List MVarId) : TacticM Unit  -- 设置目标列表
def getMainGoal : TacticM MVarId          -- 获取第一个目标
def getMainTarget : TacticM Expr          -- 获取第一个目标的类型（命题）

2.3.1. Name🔗

Lean 中一切都有名字。Name 是一个层次化的标识符：

-- `Nat.add` 表示为：
Name.str (Name.str Name.anonymous "Nat") "add"
-- 或用反引号语法：
``Nat.add

在元程序中，你会频繁用到反引号语法来引用名字。

2.3.2. Expr🔗

表达式树，Lean 中所有项的内部表示。详见第二章。

2.3.3. FVarId 与 MVarId🔗

• FVarId（free variable id）：局部上下文中的变量的唯一标识。当你在证明中引入假设 h : P，h 就是一个 FVarId。

• MVarId（metavariable id）：元变量的唯一标识。每个未解决的证明目标就是一个 MVarId。

你可以用 Lean.MVarId 和 Lean.FVarId 在编辑器中悬停查看它们的定义。

2.4.1. 注册：elab 和 macro🔗

在 Lean 4 中，注册一个新 tactic 有两条路：

方式一：macro（语法糖，展开为其他 tactic）

macro "my_rfl" : tactic => `(tactic| rfl)

macro 在语法层面展开，不进入 TacticM。适合简单的 tactic 组合。

方式二：elab（完整的语义实现）

syntax "my_assumption" : tactic

elab_rules : tactic
  | `(tactic| my_assumption) => do
    let goal ← getMainGoal
    let lctx ← getLCtx
    for decl in lctx do
      if ← isDefEq decl.type (← goal.getType) then
        goal.assign decl.toExpr
        return
    throwTacticEx `my_assumption goal "no matching hypothesis"

elab_rules 进入 TacticM，可以完整访问证明状态。

2.4.2. 调用流程🔗

当 Lean 解析 by simp 时：

1. by 关键字触发 tactic block 的解析

2. simp 被匹配到它注册的 elab_rules

3. 当前目标列表作为 TacticM 的状态传入

4. simp 的实现运行，修改目标列表

5. 剩余目标继续处理后续 tactic

2.8.1. 失败 1：unknown identifier 'getMainGoal'🔗

忘记 open 相关命名空间了。确保文件顶部有：

import Lean
open Lean Elab Tactic Meta

这四个命名空间覆盖了日常 tactic 编写的绝大多数 API。

2.8.2. 失败 2：elab_rules 里的模式匹配报错🔗

语法声明和 elab_rules 的模式名字不一致。检查：

-- [示意]
syntax "my_tac" : tactic     -- 这里叫 my_tac

elab_rules : tactic
  | `(tactic| my_tac) => do  -- 这里也必须是 my_tac，不能写成 mytac 或 my-tac
    ...

2.8.3. 失败 3：goal.assign 之后还有目标报错🔗

goal.assign e 只关闭了 goal 这一个目标，但 setGoals 里还留着它。正确做法：赋值后 return（让框架自动清理），或者手动从 goals 列表中移除。

2.8.4. 失败 4：isDefEq 意外修改了元变量🔗

isDefEq 是有副作用的——它会在成功时给元变量赋值。如果你只是想探查相等性而不想赋值，用 withoutModifyingState 包裹：

-- [示意]
let equal ← withoutModifyingState (isDefEq a b)

2.9.1. 练习 1.1（热身）：跑通 trace_goal🔗

在你的 Mathlib 项目里新建 Ch01.lean，复制 1.5 节的 trace_goal 实现，然后验证它能输出当前目标：

import Lean
open Lean Elab Tactic Meta

打开 VS Code 的 Lean Infoview，把光标放在 trace_goal 那一行，你应该能看到目标输出。

2.9.2. 练习 1.2（热身）：识别 Monad 层次🔗

以下操作各属于哪个 Monad 层？填写括号：

 inferType (e : Expr)          → (        )
 logInfo m!"hello"             → (        )
 getMainGoal                   → (        )
 elabTerm stx none             → (        )
 mkFreshExprMVar T             → (        )

参考答案：MetaM、CoreM、TacticM、TermElabM、MetaM。

2.9.3. 练习 1.3（debug）：找出并修复错误🔗

以下 tactic 实现有两处错误，找出来并修复：

-- [可运行] 这段代码有错误，修复后应该能关闭 n = n 这类目标
import Lean
open Lean Elab Meta

elab "close_rfl" : tactic => do
  let goal ← getMainGoal
  let goalType ← goal.getType
  let_expr Eq _ lhs rhs := goalType | throwError "not an equality"
  if ← isDefEq lhs rhs then
    goal.assign (mkConst ``Eq.refl)  -- 错误 1
  else
    throwError "not reflexive"

example : (42 : Nat) = 42 := by close_rfl

提示：

• 错误 1 是 proof term 构造错误——Eq.refl 需要显式传入类型和值两个参数（用 mkApp2）

• 错误 2 是命名空间可见性错误——getMainGoal 在 Tactic 命名空间里，open Lean Elab Meta 少了 Tactic

这两类错误性质不同：一个是 API 调用不完整，一个是符号找不到。以后遇到类似报错时，先判断是哪一类再对症下药。

2.9.4. 练习 1.4（综合）：实现 my_rfl🔗

不用 macro，用完整的 elab_rules 实现一个 my_rfl tactic：如果目标是定义等价的等式（a = b 且 a 和 b 定义等价），用 rfl 关闭；否则给出清晰的错误信息（包含目标内容）。

测试用例：

-- [可运行] 实现 my_rfl 后，以下应全部通过
example : (2 : Nat) + 3 = 5 := by my_rfl     -- 应通过（计算等价）
example : (0 : Nat) + n = n := by my_rfl       -- 应通过（定义等价）
example (h : n = m) : n = m := by my_rfl       -- 应失败

最后一个例子解释：这里的命题 n = m 当然是可证的（用 exact h 就行），但 my_rfl 只能关闭「两侧定义等价」的等式目标，它不会搜索假设中的 h。tactic 的失败不代表命题假，只代表这个 tactic 的适用边界到了。这种边界意识在后面设计和选用 tactic 时非常重要。

下一章，我们深入 Expr——Lean 4 中所有项的内部表示。