Lean证明分支覆盖判定逻辑及两种写法差异解惑

先给出问题涉及的核心定义：

inductive Expr where
  | const : Nat → Expr
  | var : Nat → Expr
  | plus : Expr → Expr → Expr
  | times : Expr → Expr → Expr
deriving Repr
open Expr

def eval (v : Nat → Nat) (e:Expr) : Nat :=
  match e with
  | const n     => n
  | var n       => v n
  | plus e₁ e₂  => (eval v e₁) + (eval v e₂)
  | times e₁ e₂ => (eval v e₁) * (eval v e₂)

def simpConst : Expr → Expr
  | plus (const n₁) (const n₂)  => const (n₁ + n₂)
  | times (const n₁) (const n₂) => const (n₁ * n₂)
  | e                           => e

问题场景 #

以下证明因分支覆盖问题无法编译：

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

错误提示：未明确列出e1、e2的所有分支，通配符| _, _ => simp [...]过于宽泛。

而如下版本可正常运行：

theorem simpConst_eq4 (v : Nat → Nat) (e : Expr) : eval v (simpConst e) = eval v e := by
  cases e with
  | plus e1 e2 => 
    cases e1 <;> cases e2 <;> simp [simpConst, eval]
  | times e1 e2 => 
    cases e1 <;> cases e2 <;> simp [simpConst, eval]
  | _ => simp [simpConst, eval]

疑问解答 #

1. 为什么cases中的通配符| _ => ...能覆盖const和var分支？ #

Lean的cases tactic处理归纳类型时，允许用通配符_匹配所有未被显式列出的构造器。在这个例子里，我们显式处理了plus和times两个构造器的分支，剩下的const和var会自动被通配符分支覆盖。

Lean会自动统计当前归纳类型的所有构造器数量，对比显式列出的分支，确认未列出的都被通配符涵盖，因此不会判定为分支遗漏。

2. 为什么两种通配符写法的分支覆盖判定结果不同？ #

失败证明的问题根源

第一个证明里的嵌套match e1, e2 with使用| _, _ => ...通配符时，Lean对多归纳类型值的match分支检查更严格：它要求你要么显式列出所有可能的构造器组合，要么用结构化的分支遍历方式（比如cases），而直接用宽泛的通配符无法让Lean确认你已经覆盖了所有情况。

e1和e2都是Expr类型，各自有4种构造器，组合起来有16种可能。| _, _只是一个笼统的匹配，没有明确告知Lean你已经考虑了所有组合，因此被判定为分支覆盖不明确。

成功证明的合法逻辑

第二个证明使用cases e1 <;> cases e2是Lean认可的结构化分支覆盖方式：

• cases e1会遍历e1的所有4种构造器
• <;>是链式tactic操作符，会把后续的cases e2应用到cases e1生成的每个分支上，进而遍历e2的所有4种构造器
• 这相当于显式枚举了e1和e2的所有16种组合，Lean能明确确认所有分支都被覆盖，因此不会报错。

简单来说：外层cases的通配符是针对单一归纳类型的剩余构造器，Lean能明确统计；而嵌套match的通配符针对多归纳类型的组合，Lean无法确认你是否遗漏了特定组合，因此不允许这种写法。

内容的提问来源于stack exchange，提问作者Igott