coq - 为什么 UIP 在 Coq 中无法证明？为什么 match 构造泛化类型？

Question

如果需要，必须在 Coq 中公理地添加 UIP(以及公理 K 等等价物):

uip : ∀ A (x y: A) (p q: x = y), p = q

这是令人惊讶的，因为从只有一个构造函数的相等性定义来看，这似乎是显而易见的。 (这当然取决于 Coq 中的归纳定义捕获其类型的所有元素的解释)。

当一个人试图证明 UIP 时，就会陷入自反子情况:

uip_refl : ∀ A (x: A) (h: x = x), h = eq_refl x

我们可能希望以下术语是一个合适的证明术语:

fun A (x: A) (h: x = x) =>
  match h as h0 in (_ = a) return (h0 = eq_refl x) with
    | eq_refl _ => eq_refl (eq_refl x)
  end 

这失败了，因为它类型错误。我们知道 h: x = x，但是当我们匹配术语时，我们丢失了自反性信息并且它被泛化为 h0: x = a。因此，我们的返回类型 h0 = eq_refl x 类型错误。

为什么 match 构造在这里泛化了我们的类型？非泛化替代方案是否易于处理？

Answer 1

Would a non-generalizing alternative be tractable?

这样的比赛是有先例的。它在 Coq 的现成扩展中提供(在 Program 中；它也是 Equations 插件中的一个选项)。 Agda 还以类似的方式对模式匹配进行类型检查(如果启用了 --with-K，which is the default)。

正如您所展示的，您可以使用它来定义 UIP，因此不采用 UIP 的所有原因都会延续到不采用该匹配项。相反，可以使用 UIP 将该匹配项编译为一个项，就像 Program and Equations 所做的那样。

不过，我无法真正解释为什么“泛化”会有所不同。我敢打赌，答案就在 Conor McBride 的论文中。