PAYATHON 2026

Lean 4 如何判断证明分支是否穷尽，为什么两种通配写法表现不同？

数据阿明

结论

match 中的 | _, _ => 要在一般模式下提供分支证明；cases 中的 | _ => 则将同一段 tactic 分别用于剩余的构造子目标。

第一种写法的通配模式覆盖了剩余输入，但 simp 仍可能无法完成分支证明。就这里的证明结构而言，通配分支没有为 simp 提供足够具体的构造子信息。

题目没有提供完整报错和 Lean 版本，因此不能确定实际编译时最先出现哪条错误。下面假定嵌套 match 的缩进正确，讨论其证明语义。

match 的通配分支为什么会卡住？

加法分支使用了下面的模式：

match e1, e2 with
| (const n₁), (const n₂) => simp [simpConst, eval]
| _, _ => simp [simpConst, eval]

求值时，Lean 按顺序选择第一个匹配的分支。两个参数都是 const 时，会选择第一行。官方教程的通配符与重叠模式介绍了这种重叠模式的行为。

检查第二行的证明时，_ 不会自动附带“前面所有模式都不成立”这样的假设，也不会提供“e1 和 e2 不可能同时为 const”的证明。

在这个分支中，两个参数仍是一般的 Expr。需要证明的目标本质上是：

eval v (simpConst (plus e1 e2)) = eval v (plus e1 e2)

而 simpConst (plus e1 e2) 的结果取决于两个参数是否都是 const：

  • 都是 const 时，返回合并后的常量。
  • 其他情况下，返回原表达式。

由于两个参数的构造子尚未确定，simp [simpConst, eval] 无法仅凭通配模式选定相应的计算分支。通常也不能指望 simp 自动枚举任意归纳类型变量的构造子。

这个一般目标仍然成立，但当前的 simp 无法完成证明；乘法分支也是如此。Lean 的模式匹配 tactic 文档说明，每个分支都必须证明将匹配模式代入后得到的目标。

cases 的默认分支为什么可以通过？

cases e 会先根据 Expr 的四个构造子产生目标：

const n
var n
plus e1 e2
times e1 e2

cases 会在各目标中用相应的构造子替换被拆分的表达式，具体机制可参见官方的 cases 说明。

题目中能通过的版本已经分别处理了 plus 和 times。最后这一行：

| _ => simp [simpConst, eval]

会分别处理剩下的 const 目标和 var 目标，相当于：

| const n => simp [simpConst, eval]
| var n => simp [simpConst, eval]

这两个目标各自保留了具体的构造子信息。执行 simp 时，目标中的表达式已确定为 const n 或 var n。在这两种情况下，simpConst 都直接返回输入，等式随即化简完成。

如何修改证明？

可以沿用题目中已经成功的 cases 思路，明确写出外层四种情况：

theorem simpConst_eq (v : Nat → Nat) :
    ∀ e : Expr, eval v (simpConst e) = eval v e := by
  intro e
  cases e with
  | const n =>
      simp [simpConst, eval]
  | var n =>
      simp [simpConst, eval]
  | plus e1 e2 =>
      cases e1 <;> cases e2 <;> simp [simpConst, eval]
  | times e1 e2 =>
      cases e1 <;> cases e2 <;> simp [simpConst, eval]

其中：

cases e1 <;> cases e2 <;> simp [simpConst, eval]

这行命令先拆分 e1，再对产生的每个目标拆分 e2，最后对每个组合执行 simp。两个参数各有四种构造子，因此会处理 16 种顶层构造子组合，不需要手写 16 段相同的化简代码。

如果希望保留外层 match，也可以直接在 plus 和 times 分支内使用上述 cases 命令，不再编写内部的重叠通配模式。

如何判断是覆盖问题还是证明问题？

排查时要分开看两件事：

  1. 模式是否覆盖所有可能输入。缺少某个构造子情况，才属于覆盖不完整。
  2. 每个分支的证明是否完成。模式已经覆盖输入，但仍留下目标，属于分支证明没有结束。

可以在通配分支中临时插入 trace_state，查看 tactic 实际拿到了哪些变量、假设和目标。通配分支在文本上位于某个分支之后，并不意味着上下文中已有排除前面模式的假设。

当前 simpConst 只折叠顶层的常量加法和乘法，不递归处理子表达式，因此这个证明不需要对子表达式使用归纳假设。如果以后把函数改成递归优化，证明结构也需要重新考虑。

原代码中的 def sampleVal : Nat → Nat 省略了函数体，是一个占位声明，不能作为完整定义直接编译；它没有参与上述定理，可以从最小示例中移除。嵌套 match 也要保留正确缩进，避免解析问题影响对证明错误的判断。

备注：内容仅供参考。