coq - 统一在 Coq 核心类型系统中的作用是什么？

Question

在对证明项进行类型检查时，在阐述归纳构造微积分的核心语言后，统一如何发挥作用？

具体来说，在处理传递性和对称性等等式的属性时，我发现在证明诸如 forall x y, x = y -> y = x 之类的语句时，理解变量的统一发生在哪里是很有挑战性的通过 refl x x 进行模式匹配。

附加上下文:我知道在 Coq 的扩展语言中统一是必要的，特别是在引入存在变量并隐式实例化它们时。然而，在查看 Coq 核心类型规则的文档时，我找不到任何明确提及统一的内容。

Answer 1

答案很简单:内核中没有统一。

在您提到的特定情况下，您可以查看一个证明术语，它看起来像这样

fun x y (e : x = y) =>
  match e as e' in _ = y' return y' = x with
    | eq_refl => eq_refl
  end

我特意包含了return子句:这就是有趣的事情发生的地方。该子句绑定(bind)多个变量:一个用于归纳类型的每个索引(这里，等式有一个索引，因此有一个绑定(bind)变量 y' )，另一个额外的变量(这里 e' )用于审查者(术语匹配)上，这里 e )。在每个分支中，这些绑定(bind)变量被给定构造函数的特定索引以及该构造函数本身所替换。例如，对于相等只有一个分支，其中 y'替换为 x (和 e' 由 eq_refl )。如果每个分支都针对其 return 子句的“专用版本”进行类型检查，则整个模式匹配具有从 return 子句获得的类型，方法是将索引的变量替换为检查者的索引，最后一个替换为受审查者本身。

总而言之，这种机制可能看起来像统一，因为它涉及同一依赖类型的不同实例:分支中的一个，以及整个模式匹配的一个。但是，虽然在阐述过程中，Coq 可以使用统一来推断 return 子句(减少用户手动给出的麻烦)，但一旦找到合适的子句，就不再有统一了。