Coq核心类型系统中合一的作用及等式证明相关技术问询

一、核心类型系统里的合一：幕后的算法工具 #

Coq的归纳构造演算（CIC）核心规则文档里确实没直接提合一，但这不代表它不重要——核心规则是描述性的，只定义“什么样的项是合法的”，而合一则是实现这些规则的算法基础，用来解决“两个项能不能通过变量替换变得完全一致”的问题，是类型检查器判断规则是否满足的关键手段。

比如核心的函数应用规则要求“函数的输入类型和参数类型必须一致”，合一就是用来检查这两个类型能不能通过替换变量达成一致的工具；再比如模式匹配规则要求“所有分支的返回类型必须和目标类型兼容”，这里也需要合一处理模式变量和被匹配项的绑定关系。

二、展开到核心语言后，类型检查中的合一作用 #

当你把Coq表层的证明项展开成CIC核心代码时，所有像symmetry、rewrite这类策略生成的语法糖都会被拆解成基于match和refl的底层结构。此时类型检查器要验证每个核心项的合法性，合一主要做两件事：

• 验证类型是否匹配：比如检查函数参数的类型是否符合函数的输入要求，或者模式分支的返回类型是否统一。
• 求解变量绑定：处理模式匹配里的变量替换，确保所有变量的实例化都符合类型约束。

三、以等式对称性证明为例，看合一在哪里生效 #

我们拿forall x y, x = y -> y = x的核心证明项来说，它的底层代码大概是这样的：

fun (x y : nat) (H : x = y) =>
match H in (_ = z) return (z = x) with
| refl e => refl e
end

这里的合一发生在两个关键环节：

1. 模式匹配的类型约束合一 #

类型检查器处理match H in (_ = z) return (z = x)时，首先要确认H的类型x = y和模式_ = z的结构能对上。这时候就会触发合一：把通配符_和x绑定，把模式变量z和y绑定。这一步是为了确定return子句里的z到底对应哪个具体项——说白了就是把z替换成y，让return的目标类型变成y = x。

2. 分支中refl的类型合一 #

进入refl e分支时，类型检查器需要验证这个refl的类型是否符合return子句要求的y = x。而refl e的类型是e = e，所以这里要做的就是合一e = e和y = x。

那e是怎么来的？其实在匹配refl e和H的时候，H作为x = y的证明，它的实际构造子只能是refl t（因为等式类型只有refl这一个构造子）。这时候会把模式里的e和t合一，同时refl t的类型是t = t，而H的类型是x = y，所以还要合一t = t和x = y——这一步直接得出t、x、y是同一个项（因为H证明了x和y相等）。

这么一来，refl e的类型e = e就变成了x = x，而return的目标类型是y = x，由于x和y已经通过合一绑定成同一个项，所以这两个类型是等价的，类型检查就通过了。

说白了，合一就是在模式匹配时，把模式里的变量和被匹配项的对应部分“粘”在一起，同时验证粘完之后的类型是否符合要求——这个过程是类型检查器自动做的，所以核心规则里不会写，但却是实现规则必不可少的步骤。

补充：核心规则与合一的关系 #

核心规则是“声明式”的，只说“如果存在某个替换让类型匹配，那这个项就是合法的”；而合一是“算法式”的，用来找到这个替换（或者证明找不到）。就像数学公理不会告诉你怎么证明它，合一是实现这些公理的“操作工具”。

内容的提问来源于stack exchange，提问作者yiyuan-cao