您如何在Coq中证明（e：p = p）= eq_refl？

Question

我正在尝试证明这一点：

Lemma eq_eq: forall (U: Type) (p: U) (eqv: p = p), eq_refl = eqv.

但是似乎似乎没有办法。问题是类型p = p在相同条件下等于，然后尝试匹配其实例。如果不是这种情况，那么很容易证明带有单个构造函数的类型的项等于该构造函数。

Lemma eq_tt: forall (U: Type) (x: unit), tt = x.
Proof
  fun (U: Type) (x: unit) =>
    match x as x'
      return tt = x'
      with tt => eq_refl
    end.

但是当您对我的问题尝试相同的策略时，它会失败。

Lemma eq_eq: forall (U: Type) (p: U) (eqv: p = p), eq_refl = eqv.
Proof
  fun (U: Type) (p: U) (eqv: p = p) =>
    match eqv as e
      in _ = p'
      return eq_refl = e
      with eq_refl => eq_refl
    end.

此操作失败，术语“ e”的类型为“ p = p'”，而预期类型为“ p = p”（无法统一“ p'”和“ p”）。

问题是，这里的return子句在内部将其转换为谓词函数，如下所示：

fun (p': U) (e: p = p') =>
  eq_refl = e

无法进行类型检查，因为我们现在失去了e相等性中两个术语之间的约束，而eq_refl则需要该约束。

是否有解决此问题的方法？我想念什么吗？

Answer 1

您提出的引理正是uniqueness of identity proofs (UIP)的陈述。首次证明，MLTT与Hofmann and Streicher's groupoid model（pdf链接）中的UIP取反是一致的。在此模型中，类型被解释为类群，其中身份类型x = y是类群中从x到y的态射集。在此模型中，可以有多个不同的e: x = y。

[最近，homotopy type theory已经接受了这一观点。类型被解释为∞-类群，而不是单纯的类群，不仅在x和y之间存在多个相等性，而且在身份p q: x = y之间也可能具有多个身份，等等。

可以说，没有上面提到的UIP或Axiom K之类的额外公理就无法证明您的引理。