5

我正在阅读 ssreflect 教程，内容如下：

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

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

看起来确实如此，因为所有布尔值都满足 EM 如果是这样，那么对于遵循 ssreflect 样式来说，这将是一个很大的假设。

另外，我不太了解它下面的“本地”或“小规模”部分：

由于它通常在本地用于有效地处理小部分证明（而不是在整体证明结构中使用），因此这称为小规模反射，因此称为 ssreflect。

小部分与整体证明结构是什么意思。这是否意味着我们有时可以在本地假设 EM 而不会造成任何伤害，并且通常不使用 EM，或者这里的 local 是否意味着其他东西？

另外，我在 Coq 方面经验不足，不太明白这种“蛮力”风格在“布尔对应物”（主要基于case我目前所读到的分析）如何比普通的 Coq 方式更有效。对我来说，蛮力不是很直观，也不容易事先猜到，直到你看到结果。

有什么具体的例子来说明这里的效率吗？

4

2 回答 2

7

Ssreflect 不假设排中，但库的大部分是建立在布尔命题上的，即 type 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 只关注可判定类型”的说法。虽然大部分库都基于可判定（布尔）谓词，但还有许多其他的假设没有做出这种假设，或者在某些公理的存在下可能非常有用。

于 2016-01-28T00:52:52.253 回答
4

Ssreflect 通常不假定排中，您将无法证明

forall A: Prop, A \/ ~A

但是，ssreflect 只关心可判定类型：可以判定相等的类型，通常表示为

Definition decidable (T:Type) := forall x y:T, {x = y}+{x <> y}.

在考克。这意味着对于 type 的任何两个元素T，您可以获得一个建设性的（在 中Set，而不是Prop像被排除的中间那样的）证明它们相等或不同。因此，大多数推理都可以在bool而不是在 中完成Prop，因此您有某种受限制的排中形式，仅适用于布尔语句。

于 2015-12-30T07:58:10.787 回答