对Nat类型`plus`函数第二个参数添加模式匹配的探讨

这是个非常好的问题！你提出的这种多分支模式匹配的plus实现思路完全符合直觉，但标准库的plus之所以只针对第一个参数做递归拆解，主要有以下几个原因：

1. 递归结构的一致性与数学对应 #

Nat的定义本身是单参数递归构造的：Z是零，S n是n的后继。标准库的plus实现严格遵循了这个结构——每次递归都只拆解第一个参数的构造子，直到触底到Z。这种写法和数学上自然数加法的归纳定义完全对应：

• 0加任何数等于该数（plus Z right = right）
• 后继数加另一个数，等于另一个数加原数的后继（plus (S left) right = S (plus left right)）
  这种一致性让函数的逻辑更清晰，也更容易和数学证明中的归纳步骤对齐。

2. 冗余匹配的可推导性 #

你添加的plus left Z = left其实是可以通过现有规则推导出来的冗余定义：

• 当left是Z时，已经被第一条规则plus Z right = right覆盖，结果就是Z；
• 当left是S k时，递归调用plus k Z，最终会走到第一条规则返回Z，再经过层层S包装，结果就是S k也就是left。
  对于Idris这类依赖类型语言来说，冗余的模式匹配会增加编译器的检查负担——它需要验证这些额外规则和现有规则没有冲突，甚至可能需要你手动解决匹配歧义（比如plus Z Z同时匹配第一条和第二条规则的情况）。

3. 归纳证明的简洁性（反直觉的优势） #

你觉得多一条规则会让证明更简便，但实际上标准库的单参数递归实现反而更利于归纳证明。比如要证明plus n Z = n：

• 基例：n=Z时，plus Z Z = Z，符合结论；
• 归纳步骤：假设plus k Z = k，那么plus (S k) Z = S (plus k Z) = S k，直接得证。
  如果用你的三规则实现，虽然能直接用plus left Z = left得到结论，但在证明更复杂的性质（比如加法交换律plus n m = plus m n）时，单参数递归的结构会让归纳步骤更统一，不需要额外处理第二个参数为Z的分支，反而减少了证明的复杂度。

4. 模式匹配的完整性检查 #

Idris会严格检查函数的模式匹配是否覆盖了所有可能的输入情况。标准库的plus只有两个规则，编译器能轻松验证它覆盖了Nat的所有组合；而你的三规则实现中，plus left Z和plus Z right存在重叠的匹配场景（left=Z且right=Z），这时候编译器会要求你明确优先级或者证明规则的一致性，反而增加了额外的开发成本。

当然，这并不意味着你的实现思路有问题！如果在自己的项目中，为了提升代码可读性而添加这条冗余规则是完全可行的——只要你通过等式证明（比如plus_left_Z : (n : Nat) -> plus n Z = n）来验证它和标准库实现的等价性，就能兼顾可读性和逻辑严谨性。

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