我正在形式化一个语法，它本质上是一个布尔表达式。在 coq 中，您可以在 Prop 或更明确地在 bool 中获得类似布尔值的东西。
例如，我可以这样写：
true && true
或者
True /\ True
问题是，在证明中（这是我真正关心的），我可以在域 bool 中进行案例分析，但在 Prop 中这是不可能的（因为我认为所有成员都不可枚举）。即使对于非常简单的证明，放弃这种策略和类似的重写策略似乎也是一个巨大的缺点。
一般来说，在什么情况下会选择 Prop 而不是 bool 进行形式化？我意识到这是一个广泛的问题，但我觉得 Coq 手册中没有充分解决这个问题。我对人们在两条路线上的真实经历很感兴趣。
对此有很多不同的看法。我个人的看法是，通常最好不要做出这种选择：拥有两个版本的属性是有意义的，一个版本在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 命题（当然，只要我们能够证明两者在逻辑上是等价的）。例如，如果我们希望有一个与布尔属性相关的自定义归纳原理，我们可以寻找一个等效的公式作为归纳定义的命题。
数学组件库是遵循这种风格的开发的一个很好的例子。事实上，因为它在那里如此普遍，所以该库提供了一种特殊的视图机制来编写像上面这样的转换引理并应用它们。在普通 Coq 中，我们还可以使用rewrite策略更方便地应用逻辑等价。
当然，在很多情况下，拥有相同属性的两种配方是没有意义的。有时，你被迫使用Prop，因为你关心的属性是不可判定的。有时，您可能会觉得将您的财产写入其中不会获得任何好处Prop，并且可能仅将其保留为布尔值。
除了上面链接的软件基础章节之外，这个答案还更深入地讨论了bool和之间的区别。Prop