不是 eq_refl 的 COQ 身份术语

Question

我仍然想知道 COQ 中相等类型 eq 的项可以不同于 eq_refl 是什么意思。

下面这个词是不是一个例子？

((fun x:nat => eq_refl x) 2).

此术语在句法上与 eq_refl 不同，但计算结果为 eq_refl。

是否存在无法计算为 eq_refl 的术语示例？

P.S。这不是作业问题 ;-)

Answer 1

正如您所指出的，(fun x => eq_refl x) 2 与 eq_refl 2 实际上不是，因为两个表达式计算的是同一件事。

回答你的第二个问题有点微妙，因为它可以用许多不同的方式来解释。这是一种可能性（我认为这是您想到的一种可能性）：

Are there any type T and terms x y : T, such that there is a proof e of @eq T x y in the empty context that does not compute to @eq_refl T z (where z : T is the result of computing x and y)?

我相信这个问题的答案是否定的。应该可以正式地证明它，因为 Coq 的理论是强规范化的，e 必须有一个范式 e'，并且所有类型为 eq 的范式必须是eq_refl.

请注意，如果放弃在空上下文中键入 e 的要求，则不再适用。例如，考虑 forall n, n + 0 = n.

的证明项

Fixpoint plus_n_0 n : n + 0 = n :=
  match n return n + 0 = n with
  | 0 => eq_refl 0
  | S n' => match plus_n_0 n' in _ = m return S (n' + 0) = S m with
            | eq_refl => eq_refl (S (n' + 0))
            end
  end.

在后继分支中，我们使用 match 生成 S (n' + 0) = S n' 的证明，该证明 而不是 计算为 eq_refl。发生这种情况是因为 match 不能减少 plus_n_0 n' 项，因为它是一个应用于变量的函数。但是，如果我们将 plus_n_0 应用于任何具体的自然数（例如，1729），结果证明将计算为 eq_refl 1729（试试吧！）。

另一件值得指出的事情是，当争论每个封闭的相等性证明计算为 eq_refl 时，我们不得不在 Coq 的逻辑之外推理，诉诸我们不能将其表述为 Coq 命题的规范化论证：请注意，因为 Coq 识别可转换的术语，所以无法编写命题 P : nat -> Prop 使得 P n 成立当且仅当 n 是标准形式的 Coq 术语。

考虑到这一事实，您可能想知道是否可以在 Coq 的逻辑中建立该结果；也就是说，

forall T (x : T) (e : x = x), e = eq_refl x,

或者，用英语解释，"every proof of equality is equal to eq_refl"。事实证明，这个陈述 独立于 Coq 的逻辑，这意味着它无法在 Coq 本身内被证明或反驳。

乍一看这似乎与我之前所说的相矛盾。但是请记住，如果新公理不与逻辑内部可以证明的结果相矛盾，我们总是可以向 Coq 的逻辑中添加新的公理。这意味着假设存在 some 类型 T、some 项 x : T 和证明 x = x 的 e 使得 e <> eq_refl x。如果我们添加这个公理，那么我之前给出的论点将不再适用，因为将存在语法上不同于 eq_refl（即 e）的正常形式的等式证明。

我们无法在 Coq 的逻辑（以及类似的形式系统，例如 Martin-Löf 的类型理论）中建立这个结果的事实正是同伦类型理论得以实现的原因。 HoTT 假设单价公理的存在，它允许人们产生可证明的不同的平等证明。

编辑重要的是要记住 Coq 中有两个相等的概念：定义相等（即相等的项通过简化）和命题相等（即，我们可以通过=关联的术语）。对于 Coq，定义上相等的术语可以互换，而命题上相等的术语必须通过显式重写步骤进行交换（或使用 match 语句，如上所示）。

我在上面关于这两个变体之间的区别的讨论中有点松懈。在某些情况下，相等性证明在命题上是相等的，即使它们在定义上并非如此。例如，考虑以下 nat 的自反性替代证明：

Fixpoint eq_refl_nat (n : nat) : n = n :=
  match n return n = n with
  | 0 => eq_refl 0
  | S n' => match eq_refl_nat n' in _ = m return S n' = S m with
            | eq_refl => eq_refl (S n')
            end
  end.

术语eq_refl_nat不是在定义上等于eq_refl：我们不能仅通过简化从eq_refl_nat获得eq_refl .然而，两者在命题上相等：事实证明，对于 nat，可以证明 forall n (e : n = n), e = eq_refl。（正如我上面提到的，这不能显示为任意 Coq 类型。）

不是 eq_refl 的 COQ 身份术语

COQ identity term which is not eq_refl

equality

coq