Coq中证明自定义mult_n_O'定理时Unify错误的原因咨询

问题背景 #

我正在学习《Software Foundations》第一章，尝试编写如下简单定理（作为内置定理mult_n_O的自定义实现）：

Theorem mult_n_O' : forall n : nat, 0 = n * 0.
Proof. intros n. reflexivity. Qed.

执行reflexivity步骤时，遇到错误：Unable to unify "n * 0" with "0"。需要解释该错误的成因，以及为何该定理与内置mult_n_O表述一致却仍出现此问题。

错误成因 #

• Coq的reflexivity策略仅能直接证明语法结构完全相同的两个项相等。n * 0和0在语法上并不匹配：
  • Coq中自然数乘法*的递归定义为：0 * m = 0，S n * m = m + (n * m)。对于任意自然数变量n，n * 0无法直接触发递归定义的简化分支——因为递归定义的第一个分支仅针对左操作数为0的场景，而这里左操作数是未实例化的变量n，没有对应的规则能直接将其简化为0。
• reflexivity不会自动展开递归定义或调用已有引理，只做最基础的字面语法匹配。

内置mult_n_O的证明逻辑 #

内置的mult_n_O定理并非用reflexivity直接证明，而是通过归纳法覆盖所有自然数的情况：

1. 基例（n = 0）：0 * 0直接符合乘法递归定义的第一个分支，等于0，此时reflexivity可以生效；
2. 归纳步骤（n = S k）：先利用乘法定义将(S k) * 0展开为0 + (k * 0)，再结合加法单位元引理plus_n_O（m + 0 = m）和归纳假设k * 0 = 0，最终推导出(S k)*0 = 0。

正确的自定义证明示例 #

Theorem mult_n_O' : forall n : nat, 0 = n * 0.
Proof.
  induction n as [|k IHk].
  - reflexivity. (* 处理n=0的基例 *)
  - simpl. rewrite -> IHk. reflexivity. (* 处理n=S k的归纳步骤 *)
Qed.

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