我正在阅读ssreflect教程which reads：
下面，我们通过翻译命题陈述来证明...
转换为布尔值，可以使用蛮力轻松证明
力。这种证明技术称为反射。 Ssreflect的设计
允许并反映自己的精神，建议广泛使用这种
技术。
这（反射）是否表示该反射假定为排除的中间位置（forall A:Prop, A \/ ~A）？
看起来是这样，因为所有布尔值都满足E.M.如果是这样，这将是遵循ssreflect样式的一个重要假设。
另外，我不太理解下面的“本地”或“小规模”部分：
由于通常在本地使用，可以有效地处理
证明（而不是在整个证明结构中使用），
这称为小规模反射，因此称为ssreflect。
小零件vs.整体证明结构。这是否意味着我们有时可以在本地假设E.M.而不造成伤害，并且通常不使用E.M.，还是这里的当地含义？
另外，我对Coq的经验不足，也不太了解“布尔值对等物”上的这种“蛮力”风格（主要是根据我到目前为止所读的case分析得出）比香草更有效Coq方式。对我来说，蛮力不是很直观，在您看到结果之前，不容易事先猜测。
有什么具体的例子可以说明效率吗？
最佳答案
Ssreflect不假定排除的中间点，但是库的大部分内容基于布尔命题（即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只与可确定的类型有关”的说法。虽然库的大部分基于可判定（布尔）谓词，但在许多其他假设中，没有进行此假设或在存在某些公理的情况下可能非常有用。