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

Question

有没有办法自动证明简单的不等式1/2 >= 0？，即

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

Example test: /2 >= 0.

ring我对or没有太多经验，field甚至在证明简单的等式方面也遇到了麻烦，例如1/2 = 2/4.

我正在寻找的是类似omega但适用于实数和不等式的东西。

Answer 1

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

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