在Coq中证明平等就是反身性 [英] Proof in Coq that equality is reflexivity

问题描述

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

The HOTT book writes on page 51:
... we can prove by path induction on p: x = y that

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

有人可以告诉我如何在Coq中证明这一点吗?

Can someone show me how to prove this in Coq?

推荐答案

实际上，有可能 在Coq中证明这一结果:

Actually, it is possible to prove this result in 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:

Here, I've used a semicolon tuple notation to express dependent pairs; in Coq, {x : T & T x} is the sigma type \sum_{x : T} T x. There is also a slightly easier-to-read variant, where we do not mention y:

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

如果您不习惯手工编写证明条款，那么这段代码可能看起来有些神秘，但是它确实可以完成HoTT书中所说的:通过路径归纳进行操作.这里缺少一些关键信息，即进行路径归纳所需的 type批注. Coq可以推断出这些，但是我们可以要求它通过打印该术语来告诉我们它们的含义.对于hott51'，我们得到以下内容(经过一些重写):

If you're not used to writing proof terms by hand, this code might look a bit mysterious, but it is doing exactly what the HoTT book says: proceeding by path induction. There's one crucial bit of information that is missing here, which are the type annotations needed to do path induction. Coq is able to infer those, but we can ask it to tell us what they are explicitly by printing the term. For hott51', we get the following (after some rewriting):

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的返回类型中，x和e都被概括为y'和e'. 唯一可能的原因是因为我们将x成对包装.考虑一下如果我们尝试证明UIP会发生什么情况:

The important detail there is that in the return type of the match, both x and e are generalized to y' and e'. The only reason this is possible is because we wrapped x in a pair. Consider what would happen if we tried proving 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在这里抱怨说:

Here, Coq complains, saying:

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的返回类型中，e'具有类型x = y'，其中y'是通用的.这意味着等式e' = eq_refl是错误类型的，因为右侧必须具有类型x = x或y' = y'.

What this error message is saying is that, in the return type of the match, the e' has type x = y', where y' is generalized. This means that the equality e' = eq_refl is ill-typed, because the right-hand side must have type x = x or y' = y'.

这篇关于在Coq中证明平等就是反身性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！