ssreflect假设被排除在中间吗？

我正在阅读ssreflect教程,内容如下:

下面,我们通过将命题陈述翻译成布尔对应物来证明...,这很容易用暴力证明.这种证明技术称为反射.Ssreflect的设计允许和ssreflect的精神建议广泛使用这种技术.

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

它看起来就是这种情况,因为所有布尔值都满足EM如果是这样,这将是遵循ssreflect样式的一个很大的假设.

另外,我不太了解下面的"本地"或"小规模"部分:

由于它通常在本地用于有效处理样张的小部分(而不是在整个校样结构中使用),这称为小规模反射,因此名称为ssreflect.

小部件与整体打样结构的含义是什么？这是否意味着我们可以在本地假设EM有时没有伤害并且一般不使用EM,或者这里的本地是否意味着其他东西？

另外,我在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只涉及可判定类型"的说法.虽然库的大部分是基于可判定的(布尔)谓词,但还有许多其他的假设没有做出或者在某些公理的存在下非常有用.