mathcomp/ssreflect中是否支持经典逻辑

Question

例如，coq在其标准库中有一个经典包，其中包含经典逻辑中的引理，如与所有和存在相关的引理(https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html)。

我的问题是，在mathcomp或ssreflect本身中是否有类似的支持。到目前为止，我在https://github.com/coq/stdlib2/blob/master/src/bool.v#L548中找到的只是一些定义和引理

谢谢

Answer 1

我不认为在基本的mathcomp库中有类似的东西。最接近的可能是ssrbool中的classically运算符，它模仿直觉逻辑中的经典推理。然而，实验mathcomp分析库假设了经典公理，并具有与您提到的(https://github.com/math-comp/analysis/blob/master/theories/boolp.v)类似的结果。