与Coq中的bool和Prop有密切关系吗？

Question

是否有将Prop转换为bool的方法？我知道forall a b : nat, a <? b -> a < b，但是这东西是否完全有效：forall a b: nat, a < b -> a <? b？如果没有，我应该添加任何限制以使其成为现实吗？并且，对于同时具有Prop和bool的其他运算符，是否可以这种方式进行转换？

Answer 1

在Prop中的谓词与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)

我鼓励您查找。