为什么Agda中p2证明需模式匹配而p1可直接用refl通过校验

Agda对自定义函数会按照子句的书写顺序从上到下匹配参数，只有当参数结构能唯一确定匹配到某条子句时，才会对函数调用执行化简，这个特性是三个证明出现差异的核心原因。

为什么p1可以直接通过检查 #

p1中canonical的调用参数是(a, 0)，完全匹配canonical定义的第一条子句：

canonical (x , 0) = (x , 0)

不管第一个参数a是什么结构，只要第二个参数是字面量0，就一定会匹配到这条子句，函数直接返回(a, 0)，和等号左边完全一致，因此直接用refl就可以完成证明。

为什么p2无法直接通过检查 #

p2中canonical的调用参数是(0, a)，这里的a是未做模式拆分的任意自然数变量：

• 首先匹配第一条子句(x, 0)：因为a的结构未知，Agda无法确定a是不是0，因此无法确定是否匹配第一条子句，也就不能直接跳转匹配第二条子句。
• 此时canonical (0, a)无法做进一步化简，Agda不能确认它的值等于(0, a)，因此直接写refl会触发类型不匹配报错。

为什么p3拆分a之后就可以通过 #

p3对a做了穷尽模式匹配，覆盖了自然数的所有可能情况：

• 当a = 0时，参数为(0, 0)，匹配第一条子句，返回(0, 0)，和等号左边相等。
• 当a = suc a时，第二个参数是suc a，不可能满足第一条子句要求的0，因此会匹配第二条子句canonical (0, y) = (0, y)，返回(0, suc a)，和等号左边相等。

两种情况都可以通过refl证明，因此p3可以正常通过检查。

补充：如果调换canonical前两条子句的书写顺序，先匹配第一个参数为0的情况，再匹配第二个参数为0的情况，那么p2可以直接通过，p1反而需要对第一个参数做模式拆分才能证明。

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