COQ身份术语不是eq

COQ身份术语不是eq_refl(COQ identity term which is not eq_refl)

我仍然想知道COQ中的相等类型eq的术语与eq_refl不同eq_refl 。

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

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

这个术语在语法上与eq_refl不同，但是它计算到eq_refl 。

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

PS它不是作业问题;-)

I am still wondering what it means that a term of the equality type eq in COQ can be different from eq_refl.

Is the following term an example for this?

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

This term is syntactically different from eq_refl, but nevertheless it computes to eq_refl.

Does there exist examples of terms which do not compute to eq_refl ?

P.S. Its not a homework question ;-)

最满意答案

正如你所指出的那样， (fun x => eq_refl x) 2实际上与eq_refl 2不同，因为两个表达式都计算相同的东西。

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

是否存在任何类型T和术语xy : T ，这样在空上下文中存在@eq T xy的证明e ，其不计算到@eq_refl T z （其中z : T是计算x和y的结果） ？

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

请注意，如果删除了在空上下文中键入e的要求，则此操作不再适用。 例如，考虑forall n, n + 0 = n的证明项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这样，当n并且只有当n是正常形式的Coq项时， P n才成立。

鉴于这一事实，您可能想知道是否在 Coq的逻辑中确定了结果; 那是，

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

或者，用英语解释，“每个平等证明都等于eq_refl ”。 事实证明，这个陈述独立于Coq的逻辑，这意味着它在Coq本身内无法证明也不能被证明。

起初看起来这似乎与我之前所说的相矛盾。 但是回想一下，如果Coq的逻辑与可以在逻辑中证明的结果不矛盾，我们总能为Coq的逻辑添加新的公理。 这意味着假设存在某些类型T ， 某些项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类型，这不能显示。）

As you point out, (fun x => eq_refl x) 2 is not actually different from eq_refl 2, since both expressions compute to the same thing.

Answering your second question is a bit delicate, because it can be interpreted in many different ways. Here's one possibility (which I think is the one you had in mind):

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)?

I believe that the answer to this question is no. It should be possible to prove it formally by arguing that, since Coq's theory is strongly normalizing, e must have a normal form e', and that all normal forms that have type eq must be eq_refl.

Note that, if drop the requirement that e is typed in the empty context, this does not hold anymore. For instance, consider the proof term of 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.

In the successor branch, we use the match to produce a proof of S (n' + 0) = S n' which does not compute to eq_refl. This happens because the match cannot reduce the plus_n_0 n' term, since it's a function applied to a variable. However, if we apply plus_n_0 to any concrete natural number (say, 1729), the resulting proof will compute to eq_refl 1729 (try it!).

Another thing worth pointing out is that, when arguing that every closed proof of equality computes to eq_refl, we had to reason outside of Coq's logic, appealing to a normalization argument that we cannot phrase as a Coq proposition: note that, because Coq identifies terms up to convertibility, there's no way of writing a proposition P : nat -> Prop such that P n holds if and only if n is a Coq term in normal form.

Given this fact, you may wonder if there's anyway of establishing that result inside Coq's logic; that is,

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

or, paraphrased in English, "every proof of equality is equal to eq_refl". As it turns out, this statement is independent of Coq's logic, which means that it cannot be proved nor disproved within Coq itself.

It may seem at first that this contradicts what I said earlier. But recall that we can always add new axioms to Coq's logic if they don't contradict results that can be proved inside the logic. This means that it is perfectly fine to assume that there exists some type T, some term x : T, and some proof e of x = x such that e <> eq_refl x. If we added this axiom, then the argument I gave earlier would no longer apply, since there would be normal forms of equality proofs that would be syntactically different from eq_refl (namely, e).

The fact that we cannot establish this result inside Coq's logic (and similar formal systems, such as Martin-Löf's type theory) is exactly what enables homotopy type theory. HoTT postulates the existence of the univalence axiom, which allows one to produce provably different proofs of equality.

Edit It is important to remember that there are two notions of equality in Coq: definitional equality (i.e., terms that are equal by simplification) and propositional equality (i.e., terms that we can relate by =). Definitionally equal terms are interchangeable for Coq, whereas propositionally equal terms must be exchanged with an explicit rewriting step (or using the match statement, as seen above).

I was a bit lax in the discussion above about the difference between these two variants. There are cases where proofs of equality are propositionally equal even if they aren't so definitionally. For instance, consider the following alternate proof of reflexivity for 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.

The term eq_refl_nat is not definitionally equal to eq_refl: we cannot obtain eq_refl from eq_refl_nat just by simplification. However, both are propositionally equal: as it turns out, for nat, it is possible to show that forall n (e : n = n), e = eq_refl. (As I mentioned above, this cannot be shown for arbitrary Coq types.)