coq - ssreflect 是否假定排中间？

Question

我正在阅读 ssreflect 教程，which reads :

Below, we prove the ... by translating the propositional statement into its boolean counterpart, which is easily proved using brute force. This proof technique is called reflection. Ssreflect’s design allows for and ssreflect’s spirit recommends wide use of such a technique.

这(反射)是否意味着 ssreflect 假定排中间( forall A:Prop, A \/ ~A )？

看起来是这样，因为所有 bool 值都满足 E.M. 如果是这样，这将是遵循 ssreflect 风格的一个重要假设。

另外，我不太明白后面的“本地”或“小规模”部分:

Since it is usually used locally to handle efficiently small parts of the proofs (instead of being used in the overall proof structure), this is called small scale reflection, hence the name ssreflect.

小零件 vs. 小零件是什么意思？整体证明结构。这是否意味着我们可以在本地假设 E.M. 有时没有伤害，并且一般不使用 E.M.，或者这里的本地意味着其他什么？

此外，我在 Coq 方面经验不足，并且不太明白“ bool 对应物”(主要基于 case 到目前为止我所阅读的分析)的这种“蛮力”风格如何比 Vanilla 更有效考克方式。对我来说，蛮力不是很直观，并且在您看到结果之前不容易预先猜测。

任何具体的例子来说明这里的效率？

Answer 1

Ssreflect 不假设排中间，但库的大部分内容都建立在 bool 命题上，即类型 bool ，它确实认为

forall b : bool, b = true \/ b = false

通常使用隐式 is_true 编写上述等效版本。类型转换，如:

forall b : bool, b \/ ~ b.

“可反射”谓词是那些在 bool 中有一个版本的谓词。 ;一个很好的例子是自然数之间的“小于或等于”关系。
在标准 Coq 中， le被编码为归纳类型，而在 ssreflect 中它是一个计算函数 leq: nat -> nat -> bool .
使用 leq由于以下原因，证明函数更“有效”:假设您想证明 102 < 203 .使用标准的 Coq 定义，您将不得不构建一个大的证明项，您必须明确地对证明的每一步进行编码。
然而，对于它的计算对应物，证明只是术语 erefl ，见证算法返回 true .除了 IMO 的许多其他优势外，这在大型证明中至关重要。
最后，我必须不同意“ssreflect 只涉及可判定类型”的说法。虽然大部分库都基于可判定( bool )谓词，但还有许多其他库没有做出这种假设，或者在某些公理的存在下非常有用。