关于Coq中归纳证明对象模式匹配穷尽性检查算法的问询

在自定义归纳原理nat_ind2的定义中，当注释掉| 1 ⇒ P1分支后，Coq报错提示"Non exhaustive pattern-matching: no clause found for pattern 1"。不少人会疑惑：1并不是nat类型的构造子（nat的构造子只有0和S），Coq是怎么检测到这个分支缺失的？

先明确nat类型的本质 #

nat的核心定义是：

Inductive nat : Set :=
| 0 : nat
| S : nat -> nat.

我们日常写的1只是S 0的语法糖，2是S (S 0)的语法糖，所有大于0的自然数都是通过S构造子递归嵌套得到的。

Coq模式匹配覆盖性的检测逻辑 #

Coq的非穷尽模式匹配检测，本质是检查所有可构造出的目标类型实例，是否都能匹配到至少一个分支，大致遵循以下步骤：

1. 枚举目标类型的构造子：对于nat类型，直接枚举它的两个构造子：0，以及带参数的S _（_代表任意nat类型的参数）。
2. 递归展开构造子的参数：对于S _这种带参数的构造子，Coq会进一步分析参数的所有可能情况：
   • 当参数是0时，整个表达式就是S 0（也就是我们写的1）；
   • 当参数是S n'时，整个表达式就是S (S n')（对应所有≥2的自然数）。
3. 反例搜索验证覆盖性：Coq会主动寻找一个目标类型的实例，无法匹配任何给定的分支。在你注释掉| 1 ⇒ P1分支后，1（即S 0）既不匹配0分支，也不匹配S (S n')分支（后者要求外层是S，且参数本身也是S开头，最小对应2），这个实例就成了未覆盖的反例，触发非穷尽匹配的报错。

换句话说，Coq不会只看你写的模式表面，而是会把语法糖展开，递归遍历所有构造子的组合可能性，确保没有遗漏任何可合法构造出的类型实例。

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