automation - 如何自动证明Coq中实数的简单不等式？

有没有一种方法可以自动证明像1/2 >= 0这样的简单不等式，即

Require Export Coq.Reals.RIneq.
Local Open Scope Z_scope.
Local Open Scope R_scope.

Example test: /2 >= 0.

我对ring或field和I am having trouble with even proving simple equalities such as 1/2 = 2/4没有太多的经验。

我正在寻找的是类似omega的东西，但可以处理实数和不等式。

最佳答案

您正在寻找的工具在参考手册的the chapter on Omega中进行了描述，并针对有序环处理了各种算术目标：（非）线性整数算术和线性有理/实数算术。

它们在Psatz模块中定义，可能需要您安装一些外部求解器。在这种情况下，lra不（AFAICT）具有外部依赖性，并实现了test目标。

关于automation - 如何自动证明Coq中实数的简单不等式？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/34387602/