我仍然想知道eqCOQ 中相等类型的术语可以与eq_refl.
下面的术语是一个例子吗？
((fun x:nat => eq_refl x) 2).
该术语在语法上与 不同eq_refl，但它计算为eq_refl。
是否存在不计算为的术语示例eq_refl？
PS 这不是作业问题;-)
正如您所指出的，实际上与(fun x => eq_refl x) 2并没有什么不同eq_refl 2，因为两个表达式计算的结果相同。
回答你的第二个问题有点微妙，因为它可以有很多不同的解释。这是一种可能性（我认为这是您想到的一种）：
是否有任何类型
T和术语x y : T，这样是有证据e的@eq T x y在不空方面没有计算到@eq_refl T z（这里z : T是计算的结果x和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，我们不得不原因外勒柯克的逻辑，呼吁归一化的说法，我们不能词组作为勒柯克命题：需要注意的是，因为勒柯克识别方面达到对于可转换性，没有办法写出这样的命题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是不definitionally等于eq_refl：我们无法获得eq_refl从eq_refl_nat通过简化而已。然而，两者在命题上是相等的：事实证明，对于nat，可以证明forall n (e : n = n), e = eq_refl。（正如我上面提到的，这不能针对任意 Coq 类型显示。）