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

【问题标题】：Is Z.le as defined in the standard library proof irrelevant?标准库证明中定义的 Z.le 是否无关紧要？
【发布时间】：2018-09-21 15:38:15
【问题描述】：

在 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 文件，其中作者使用证明无关性作为全局公理来避免引入 setoid，出于美学原因，我更愿意不使用公理。在我看来，我的选择是：

希望目前定义的 Z.le 最终仍然与证明无关
使用我自己的定义，以便证明不相关性（不太令人满意，因为我想尽可能坚持使用标准库）
用 setoids 返工

【问题讨论】：

4.使用 math-comp 的<=。
鉴于它是以消极的方式制定的，我认为你需要功能扩展来摆脱 UIP。 ://
另一种选择是使用布尔版本<=?（连同强制is_true）。
FWIW，同样的投诉出现在sympa.inria.fr/sympa/arc/coq-club/2012-07/msg00162.html。

标签： coq type-theory

【解决方案1】：

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

【讨论】：