标准库中定义的Z.le是否不相关? [英] Is Z.le as defined in the standard library proof irrelevant?
问题描述
在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)，我将能够证明不相关的证明.
In the Coq standard library, there is an enumerated type called comparison with three elements Eq,Lt,Gt. This is used to define the less-than or less-than-or-equal operators in ZArith: m < n is defined as m ?= n = Lt and m <= n is defined as m ?= n <> Gt. By virtue of Hedberg's theorem (UIP_dec in the standard library) I can prove that < is proof-irrelevant, but I run into issues when it comes to <=, since it is defined negatively. I find this particularly annoying, since if <= were defined in the, IMO, more natural way (m ?= n = Lt \/ m ?= n = Eq) I would be able to prove proof-irrelevance just fine.
上下文:我使用的是以前编写的Coq文件，其中作者使用不相关的证明作为全局公理以避免引入类固醇，出于美学原因，我宁愿不使用公理.在我看来，我的选择是:
Context: I'm using some previously written Coq files where the author uses proof irrelevance as a global axiom to avoid bringing in setoids, and for aesthetic reasons I would prefer to do without axioms. It seems then to me that my options are:
-
希望当前最终定义的
Z.le仍然与证明无关
使用我自己的定义，以便证明不相关的证据(由于我想尽可能地坚持使用标准库，因此不太令人满意)
Use my own definition(s) so that proof irrelevance is provable (less satisfying since I'd like to stick to the standard library as much as possible)
使用setoid重做事物
Rework things with setoids
推荐答案
否，这在Coq中无法得到证明.它取决于函数可扩展性的公理，即(forall x, f x = g x) -> f = g.很容易证明在此假设下所有否定都不是证明相关的(因为False是证明无关紧要的)，并且如果没有它，也很难证明任何否定都不是证明无关紧要的.
No, this is not provable in Coq. It depends on the axiom of function extensionality, which says that (forall x, f x = g x) -> f = g. It's quite easy to prove that all negations are proof irrelevant under this assumption (since False is proof irrelevant), and quite impossible to prove that any negations are proof irrelevant without it.
这篇关于标准库中定义的Z.le是否不相关?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
