非eq_refl的COQ身份术语 [英] COQ identity term which is not eq_refl

问题描述

我仍然想知道，COQ中相等类型 eq 的术语可能与 eq_refl 。

以下术语是这个示例吗？

 （（有趣的x：nat => eq_refl x）2）。 
  

此术语与 eq_refl 在语法上有所不同，但无论如何，它的计算结果为 eq_refl 。

是否存在不计算为<$ c $的术语示例c> eq_refl ？

PS它不是一个家庭作业问题；-)

解决方案

正如您所指出的，（fun x => eq_refl x）2 与 eq_refl 2 实际上没有什么区别，因为两个表达式的计算结果相同。 p>

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

是否有任何类型的 T 和条款 xy：T ，因此有<$ c $的证据 e c> @eq T xy 在 not 不计算为 @eq_refl T z （其中 z：T 是计算 x 和 y 的结果）吗？

我相信这个问题的答案是否定的。通过争论，由于Coq的理论正在严格归一化，因此应该可以正式证明这一点， e 必须具有正常形式 e'，并且所有类型为 eq 的普通形式都必须为 eq_refl 。

请注意，如果删除在空上下文中键入 e 的要求，则不再适用。例如，考虑对所有n 的证明项，n + 0 = n 。

  Fixpoint plus_n_0 n：n + 0 = n：= 
匹配n返回n + 0 = n与
 | 0 => eq_refl 0 
 | S n’=>匹配_ = m中的plus_n_0 n’返回S（n’+ 0）= S m与
 | eq_refl => eq_refl（S（n’+ 0））
结束
结束。 
  

在后继分支中，我们使用 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->支撑，使得 P n 成立，且仅当 n 是正常的Coq项时才成立

鉴于这个事实，您可能想知道是否有必要在Coq的逻辑内确定结果？也就是说，

  forall T（x：T）（e：x = x），e = eq_refl x，
  

或者用英语释义，每一个平等证明等于 eq_refl 。事实证明，该语句与Coq的逻辑无关，这意味着它无法在Coq本身内得到证明或证明。

起初似乎与我之前所说的相矛盾。但是请记住，如果新公理与逻辑内部可以证明的结果不矛盾，我们总是可以在它们中添加新的公理。这意味着假设存在 some 类型 T ， some 术语 x：T 和 some 证明 e 的 x = x ，这样 e<> eq_refl x 。如果我们添加此公理，则我先前给出的论点将不再适用，因为存在等同于 eq_refl （即， e ）。

事实上，我们无法在Coq的逻辑（以及类似Martin这样的形式系统）中建立该结果-Löf的类型理论）正是实现同伦类型理论的原因。 HoTT假设存在一元性公理，这使人可以产生可证明的不同的平等证明。

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

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

  Fixpoint eq_refl_nat（n：nat）：n = n：= 
匹配n返回n = n与
 | 0 => eq_refl 0 
 | S n’=>匹配eq_refl_nat n’in _ = m返回S n’= S m与
 | eq_refl => eq_refl（SN）
结束
结束。 
  

术语 eq_refl_nat 不是 在定义上等于 eq_refl ：我们无法从 eq_refl_nat eq_refl c $ c>只是为了简化。但是，两者在命题上都是相等的：事实证明，对于 nat ，有可能表明 forall n（ e：n = n），e = eq_refl 。 （如上所述，对于任意Coq类型都无法显示。）

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

解决方案

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

这篇关于非eq_refl的COQ身份术语的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！