关于何时使用 Prop 和何时使用 bool 的一般建议

Question

我正在形式化一个语法，它本质上是一个基于布尔表达式的语法。在 coq 中，您可以在 Prop 中或更明确地在 bool 中获得类似布尔值的东西。

例如，我可以写：

true && true

或

True /\ True

问题是在证明中（这是我真正关心的）我可以在域 bool 中进行案例分析，但在 Prop 中这是不可能的（因为我想所有成员都是不可枚举的）。即使对于非常简单的证明，放弃这种策略和类似的重写策略似乎也是一个巨大的缺点。

一般情况下，在什么情况下会选择 Prop 而不是 bool 进行形式化？我意识到这是一个广泛的问题，但我觉得 Coq 手册中没有充分解决这个问题。我对人们在这两条路上的真实经历很感兴趣。

Answer 1

对此有很多不同的看法。我个人的看法是，你最好不要做出这种选择：有两个版本的属性是有意义的，一个在 Prop 中，另一个在 bool 中。

你为什么要这个？正如您所指出的，布尔值支持证明和函数中的案例分析，而一般命题则不支持。但是，Prop 在某些情况下使用起来更方便。假设您有一个类型 T 具有有限多个值。我们可以写一个程序

all : (T -> bool) -> bool

决定布尔值属性 P : T -> bool 是否包含 T 的所有元素。想象一下，我们知道 all P = true，对于某些属性 P。我们可能想使用这个事实来得出 P x = true 对应某个值 x 的结论。为此，我们需要证明关于 all:

的引理

allP : forall P : T -> bool,
         all P = true <-> (forall x : T, P x = true)

这个引理连接相同属性的两个不同表述：一个布尔引理和一个命题引理。在证明中对all进行推理时，我们可以调用allP在两者之间自由转换。我们也可以有不同的转换引理：

allPn : forall P,
          all P = false <-> (exists x, P x = false)

事实上，我们可以自由选择任何 Coq 命题来与布尔计算相关（当然，只要我们能够证明两者在逻辑上是等价的).例如，如果我们想要一个与布尔值相关联的自定义归纳原理属性，我们可以寻找一个等价的公式作为归纳定义的命题。

Mathematical Components 库是遵循这种风格的一个很好的开发示例。事实上，因为它在那里如此普遍，图书馆提供了一种特殊的 view 机制来编写转换引理，如上面的那样并应用它们。在普通 Coq 中，我们还可以使用 rewrite 策略来更方便地应用逻辑等价。

当然，在很多情况下，相同属性有两个公式是没有意义的。有时，你不得不使用Prop，因为你关心的属性是不可判定的。有时，您可能会觉得在 Prop 中写入属性不会有任何好处，并且可能只将其保留为布尔值。

除了 Software Foundations chapter linked above, 更深入地讨论了 bool 和 Prop 之间的区别。

General Advice about When to Use Prop and When to use bool