coq - mathcomp/ssreflect 是否支持经典逻辑

Question

例如，coq 在其标准库中有一个 Classical 包，其中包含经典逻辑中的引理，例如与 forall 相关且存在的引理（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 库中没有任何内容。最接近的可能是 中的classically运算符ssrbool，它模仿直觉逻辑中的经典推理。但是，实验性 mathcomp 分析库假定经典公理并具有您提到的结果（https://github.com/math-comp/analysis/blob/master/theories/boolp.v）。