coq - 外延相等谓词和普遍量化应用的相等性

Question

我正在尝试使用有充分依据的固定点来定义递归谓词，并有义务显示 F_ext当用 Fix_eq 重写时。 CPDT说大多数此类义务都可以通过简单的自动化证明来解除，但不幸的是，对于我的谓词来说，情况似乎并非如此。

我已将问题简化为以下引理(来自 Proper (pointwise_relation A eq ==> eq) (@all A))。没有 additional axioms 是否可以在 Coq 中证明？

Lemma ext_fa:
  forall (A : Type) (f g : A -> Prop),
    (forall x, f x = g x) ->
    (forall x, f x) = (forall x, g x).

它可以用谓词或函数的外延性来表示，但由于结论比通常的结论弱(f = g)，我天真地认为无需使用额外的东西就可以产生证明公理。毕竟等式两边只涉及f和g的应用；如何辨别任何内在差异？

我错过了一个简单的证明还是引理无法证明？

Answer 1

您可能对 this code I wrote a while ago 感兴趣，其中包含不同数量参数的 Fix_eq 变体，并且不依赖于函数外延性。请注意，您不需要更改 Fix_F，而只需证明 Fix_eq 的变体即可。

<小时/>

为了回答您提出的问题，而不是解决您的上下文，您提出的引理称为“forall extensionality”。

它存在于Coq.Logic.FunctionalExtensionality中，其中用函数外延性公理来证明。标准库版本使用公理来证明这个引理这一事实至少有力地证明了 Coq 中没有公理就无法证明它。

这是该事实的证明草图。由于 Coq 是强标准化*，所以空上下文中的每个 x = y 证明在判断上都等于 eq_refl。也就是说，如果您可以在空上下文中证明x = y，则x和y是可转换的。令 f x := inhabited (Vector.t (x + 1)) 并令 g x := inhabited (Vector.t (1 + x))。通过对x 进行归纳，可以直接证明forall x, f x = g x。因此，如果你的引理在没有公理的情况下是正确的，我们可以获得以下证明:

(forall x, inhabited (Vector.t (x + 1))) = (forall x, inhabited (Vector.t (1 + x)))

在空上下文中，因此 eq_refl 应该证明这个陈述。我们可以很容易地检查并发现 eq_refl 并没有证明这个说法。所以你的引理ext_fa在没有公理的情况下是无法证明的。

请注意，Coq 中对函数相等性和类型相等性的规定严重不足。本质上，在 Coq 中唯一可以证明相等的类型(或函数)是判断相等的类型(或者更准确地说，可以表示为应用于可证明相等的封闭项的两个判断相等的 lambda 的类型)。唯一可以证明不相等的类型是可证明非同构的类型。您可以证明不相等的唯一函数是那些在您提供的域的某些具体元素上可证明不同的函数。你可以证明的等式和你可以证明的不等式之间有很大的空间，如果没有公理，你就无法在这个空间里谈论任何事情。

*Coq 实际上并没有很强的规范化，因为共归纳存在一些问题。但以此为模，它正在强烈标准化。