comparison - Coq 中有理数的“小于”是否可判定？

Question

在 Coq 标准库中，“小于”关系对于自然数 ( lt_dec) 和整数 ( Z_lt_dec) 是可判定的。但是，当我搜索 ( Search ({ _ _ _ } + {~ _ _ _ })) 时，我找不到有理数的Q_le_decor Qle_dec，只能Qeq_dec找到可判定的相等性。

这是因为“小于”关系对于 Coq 中的有理数是不可判定的吗？或者它是可决定的，但决策过程没有在标准库中实现？

Answer 1

快速浏览一下 Coq 的标准库会给出两个引理，尽管不是您搜索的确切形式：

• Q_dec关于比较的可判定性（{x < y } + { x > y } + { x = y }）；
• Q_lt_le_dec ( { x<y } + { y<=x })。

我承认我没有做这个练习，但看起来你可以很容易地从那里得出任何可判定性结果Qle或Qlt你想要的结果。