有理数的“小于”在 Coq 中可以判定吗？

Question

在 Coq 标准库中，“小于”关系对于自然数 ( lt_dec) 和整数 ( Z_lt_dec) 是可判定的。然而，当我搜索 ( Search ({ _ _ _ } + {~ _ _ _ })) 时，我找不到 aQ_le_dec或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您想要的结果。