equality - 不是 eq_refl 的 COQ 标识项

Question

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

下面的术语是一个例子吗？

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

该术语在句法上不同于 eq_refl ，但它计算为 eq_refl .

是否存在不计算到 eq_refl 的术语的例子？ ?

附言这不是家庭作业问题;-)

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,

或者，用英语解释，“每个相等的证明都等于 eq_refl”。事实证明，这个语句独立于 Coq 的逻辑，这意味着它不能在 Coq 本身内被证明或反驳。

乍一看，这似乎与我之前所说的相矛盾。但是请记住，如果新公理与可以在逻辑中证明的结果不矛盾，我们总是可以向 Coq 逻辑添加新公理。这意味着假设存在某种类型 T 完全没问题。 , 一些术语 x : T ，以及一些证明 e的 x = x使得 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来自 eq_refl_nat只是通过简化。然而，两者在命题上是相等的:事实证明，对于 nat ，可以证明 forall n (e : n = n), e = eq_refl . (正如我上面提到的，这不能针对任意 Coq 类型显示。)