与 Coq 中的 bools 和 Prop 有很强的关系吗？

Question

有什么方法可以将 Prop 转换为 bool 吗？我知道forall a b : nat, a <? b -> a < b，但是这件事是否有效：forall a b: nat, a < b -> a <? b？如果没有，我是否应该添加任何限制以使其成为现实？并且，对于其他既有Prop和bool对应物的算子，能不能这样转换呢？

Answer 1

在谓词 inProp和 one in之间存在关系bool意味着所讨论的属性是可判定的。基本上你有一个函数来决定属性是true还是false。

并非所有命题都是这种情况（除非你假设一些包含它的原则），但确实适用于<?和<。由于reflect谓词，这种关系通常被具体化。

Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true 
| ReflectF : ~ P -> reflect P false.

在你的情况下，你有

Nat.ltb_spec0: forall x y : nat, reflect (x < y) (x <? y)

我鼓励你查一下。