coq - 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)

我鼓励你查一下。