ssreflect 是否假设排除中间值？
Does ssreflect assume excluded middle?
我正在阅读 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）？
看起来是这样，因为所有的布尔值都满足E.M。如果是这样，这将是遵循 ssreflect 风格的一个重要假设。
此外，我不太理解下面的 "local" 或 "small scale" 部分：
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.
小部件是什么意思v.s。整体证明结构。这是否意味着我们可以假设 E.M。局部有时没有伤害，不要使用 E.M。一般而言，还是这里的 local 有其他含义？
此外，我在 Coq 方面经验不足，不太了解 "brute force" 风格在 "boolean counterparts" 上的表现如何（主要基于 case 我阅读的分析到目前为止）比香草 Coq 方式更有效。对我来说，蛮力不是很直观，在看到结果之前不容易事先猜测。
有什么具体的例子可以说明这里的效率吗？
Ssreflect 一般不假设排中律，你无法证明
forall A: Prop, A \/ ~A
然而ssreflect只关心decidable类型：可以判断是否相等的类型，通常表示为
Definition decidable (T:Type) := forall x y:T, {x = y}+{x <> y}.
在 Coq 中。这意味着对于 T 类型的任意两个元素，您可以获得构造性的（在 Set 中，而不是在 Prop 中，如排中）证明它们相等或不同。因此，大部分推理可以在 bool 中完成，而不是在 Prop 中完成，所以你有某种限制形式的排中律，仅适用于布尔语句。
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 只关注可判定类型”的说法。虽然大部分库都基于可判定（布尔）谓词，但还有许多其他库没有做出这种假设，或者在存在某些公理的情况下可能非常有用。
我正在阅读 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）？
看起来是这样，因为所有的布尔值都满足E.M。如果是这样，这将是遵循 ssreflect 风格的一个重要假设。
此外，我不太理解下面的 "local" 或 "small scale" 部分：
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.
小部件是什么意思v.s。整体证明结构。这是否意味着我们可以假设 E.M。局部有时没有伤害，不要使用 E.M。一般而言，还是这里的 local 有其他含义？
此外，我在 Coq 方面经验不足，不太了解 "brute force" 风格在 "boolean counterparts" 上的表现如何（主要基于 case 我阅读的分析到目前为止）比香草 Coq 方式更有效。对我来说，蛮力不是很直观，在看到结果之前不容易事先猜测。
有什么具体的例子可以说明这里的效率吗？
Ssreflect 一般不假设排中律，你无法证明
forall A: Prop, A \/ ~A
然而ssreflect只关心decidable类型：可以判断是否相等的类型，通常表示为
Definition decidable (T:Type) := forall x y:T, {x = y}+{x <> y}.
在 Coq 中。这意味着对于 T 类型的任意两个元素，您可以获得构造性的（在 Set 中，而不是在 Prop 中，如排中）证明它们相等或不同。因此，大部分推理可以在 bool 中完成，而不是在 Prop 中完成，所以你有某种限制形式的排中律，仅适用于布尔语句。
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 只关注可判定类型”的说法。虽然大部分库都基于可判定（布尔）谓词，但还有许多其他库没有做出这种假设，或者在存在某些公理的情况下可能非常有用。