coq - 标准库证明中定义的 Z.le 是否无关紧要？

Question

在Coq标准库中，有一个名为comparison的枚举类型。具有三个元素 Eq,Lt,Gt .这用于定义 ZArith 中的小于或小于或等于运算符。 : m < n定义为 m ?= n = Lt和 m <= n定义为 m ?= n <> Gt .凭借 Hedberg 定理(标准库中的 UIP_dec)我可以证明 <与证据无关，但我遇到了 <= 的问题，因为它被定义为否定的。我觉得这特别烦人，因为如果 <=在 IMO 中以更自然的方式 ( m ?= n = Lt \/ m ?= n = Eq ) 定义，我将能够很好地证明证据无关性。

上下文: 我正在使用一些以前编写的 Coq 文件，在这些文件中，作者使用证明无关性作为全局公理以避免引入 setoids，出于美学原因，我宁愿不使用公理。在我看来，我的选择是:

1. 希望最终Z.le当前定义的仍然与证据无关

2. 使用我自己的定义，以便证明无关性是可证明的(不太令人满意，因为我想尽可能坚持标准库)

3. 用 setoids 返工

Answer 1

不，这在 Coq 中是不可证明的。它取决于函数外延性公理，即 (forall x, f x = g x) -> f = g。在这个假设下很容易证明所有否定都是证明无关的(因为 False 是证明无关的)，并且如果没有它就很难证明任何否定都是证明无关的。