Coq 证明相等性是自反性

Question

HOTT 书第 51 页写道：
...我们可以通过对 p 的路径归纳来证明：x = y

 $(x, y, p) =_{ \sum_{(x,y:A)} (x=y)} (x, x, refl x)$ .

谁能告诉我如何在 Coq 中证明这一点？

Answer 1

简单的回答：你不能。 Coq 中 x = y 的所有证明都不是 eq_refl x 的实例。您将不得不假设身份证明的唯一性才能得到这样的结果。这是一个非常好的公理，但它仍然是归纳构造微积分中的一个公理。

Answer 2

实际上，可以在 Coq 中证明这个结果：

Notation "y ; z" := (existT _ y z) (at level 80, right associativity).

Definition hott51 T x y e :
  (x; y; e) = (x; x; eq_refl) :> {x : T & {y : T & x = y} } :=
  match e with
  | eq_refl => eq_refl
  end.

在这里，我使用了分号元组表示法来表示依赖对；在 Coq 中，{x : T & T x} 是 sigma 类型 \sum_{x : T} T x。还有一个更容易阅读的变体，我们没有提到 y:

Definition hott51' T x e : (x; e) = (x; eq_refl) :> {y : T & x = y} :=
  match e with
  | eq_refl => eq_refl
  end.

如果您不习惯手写证明项，这段代码可能看起来有点神秘，但它确实按照 HoTT 书中所说的那样进行：通过路径归纳进行。这里缺少一个关键信息，即进行路径归纳所需的 类型注释 。 Coq 能够推断出这些，但我们可以要求它通过打印术语明确地告诉我们它们是什么。对于 hott51'，我们得到以下内容（经过一些重写）：

hott51' = 
fun (T : Type) (x : T) (e : x = x) =>
match e as e' in _ = y' return (y'; e') = (x; eq_refl) with
| eq_refl => eq_refl
end
     : forall (T : Type) (x : T) (e : x = x),
       (x; e) = (x; eq_refl)

重要的细节是，在 match 的 return 类型中，x 和 e 都泛化为 y' 和 e'。 这是可能的唯一原因 是因为我们将 x 包裹成一对。考虑一下如果我们尝试证明 UIP 会发生什么：

Fail Definition uip T (x : T) (e : x = x) : e = eq_refl :=
  match e as e' in _ = y' return e' = eq_refl with
  | eq_refl => eq_refl
  end.

在这里，Coq 抱怨说：

The command has indeed failed with message:
In environment
T : Type
x : T
e : x = x
y' : T
e' : x = y'
The term "eq_refl" has type "x = x" while it is expected to have type
 "x = y'" (cannot unify "x" and "y'").

此错误消息的意思是，在 match 的 return 类型中，e' 的类型为 x = y'，其中 y'是广义的。这意味着等式 e' = eq_refl 是错误类型的，因为右侧的类型必须是 x = x 或 y' = y'.

Coq 证明相等性是自反性

Proof in Coq that equality is reflexivity

equality

coq

type-theory