在Coq中与bools和Prop有很强的关系吗？
在Coq中与bools和Prop有很强的关系吗？
提问于 2020-03-12 10:03:29
有什么办法把助力转化为嘘声吗？我知道forall a b : nat, a <? b -> a < b，但是这个东西是有效的吗：forall a b: nat, a < b -> a <? b？如果没有，我是否应该增加一些限制，以使这成为现实？而且，对于其他同时拥有Prop和bool的操作符，它们能以这样的方式转换吗？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-12 10:11:33
在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)我鼓励你查一查。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60651682
复制相关文章
相似问题
腾讯云开发者
