Coq中有理数的“小于”关系是否具备可判定性？

结论 #

有理数的小于、小于等于关系本身是可判定的，你搜索不到对应引理是标准库命名规则和模块加载的问题，并非没有实现。

具体说明 #

• 有理数小于等于的判定引理名为 Qle_dec，不是你猜测的Q_le_dec，它的类型为 forall q1 q2 : Q, {q1 <= q2} + {~ q1 <= q2}，完全匹配你搜索的sumbool结构。
• 对应的小于判定引理为 Qlt_dec，类型为 forall q1 q2 : Q, {q1 < q2} + {~ q1 < q2}。
• 这两个引理都定义在QArith库的QOrdered子模块中，如果你没有提前执行Require Import QArith.加载完整的有理数算术库，仅加载了基础的有理数定义模块，Search命令会无法检索到未加载模块的内容。

判定逻辑说明 #

有理数的序判定可以直接归约到整数序判定：任意两个有理数q1 = a1 / b1、q2 = a2 / b2（其中b1、b2均为正整数），q1 <= q2等价于a1 * b2 <= a2 * b1，乘正整数不改变不等号方向，而整数的小于等于关系已经被证明可判定，因此有理数的序关系必然可判定，不存在理论上的不可判定问题。

内容的提问来源于stack exchange，提问作者LogicChains