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

Question

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

例如，我可以这样写:

true && true

或者

True /\ True

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

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

Answer 1

对此有很多不同的意见。我个人的看法是，你通常最好不要做这个选择:拥​​有两个版本的属性是有意义的，一个在 Prop 中。 ，另一个在 bool .

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

all : (T -> bool) -> bool

决定是否是 bool 属性 P : T -> bool持有 T 的所有元素.假设我们知道 all P = true , 对于某些属性(property) P .我们可能想用这个事实来得出结论 P x = true一些值(value) x .为此，我们需要证明一个关于 all 的引理。 :

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

这个引理连接了相同属性的两种不同的表述: bool 形式和命题形式。推理时 all在证明中，我们可以调用 allP在两者之间自由转换。我们也可以有不同的转换引理:

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

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

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

当然，在很多情况下，具有相同属性的两个公式是没有意义的。有时，您被迫使用 Prop ，因为你关心的属性是不可判定的。有时，您可能会觉得将您的属性(property)写入 Prop 不会有任何收获。 , 并且只能将其保留为 bool 值。

除了 Software Foundations上面链接的章节， this answer讨论 bool 之间的区别和 Prop更深入。