coq - 在 COQ 中使用功能扩展的缺点是什么

Question

将公理添加到 COQ 通常会使证明更容易，但也会引入一些副作用。例如，通过使用经典公理，人们离开了直觉主义领域，证明不再是可计算的。我的问题是，使用函数外延公理的缺点是什么？

Answer 1

对我来说，使用功能扩展性的缺点与在 Coq 中使用任何其他公理或多或少相同:它增加了系统的复杂性以及我们需要信任的程度。尽管在理论上我们非常了解使用这些众所周知的公理的逻辑后果(例如，必须避免哪些公理组合以确保一致性)，但在实践中我们有时会措手不及。例如，它是 recently found out命题外延公理与 Coq 8.4 版中的理论不一致，尽管它被广泛认为是一致的。这个看似自然的公理只是说等价命题是相等的，并在许多 Coq 开发中采用:

Axiom propositional_extensionality :
  forall P Q : Prop, (P <-> Q) -> P = Q.  

在回答 linked above ，Andrej Bauer 认为这种脆弱性可能与这些没有计算规则的公理有关，这与 Coq 理论的其余部分相反。

除了这个一般性评论之外，我还听到人们说默认情况下具有功能扩展性可能是不可取的，因为它将函数等同于非常不同的计算行为(例如，冒泡排序和快速排序)，并且我们可能想对这些差异进行推理。我个人并不认同这个论点，因为 Coq 已经将许多计算方式非常不同的值等同起来，例如 0和 47^1729 - 47 mod 1729 .我不知道不想承担功能扩展性的其他原因。