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

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

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

Example test: /2 >= 0.

我对戒指或战场没什么经验,I am having trouble with even proving simple equalities such as 1/2 = 2/4.

我正在寻找的是欧米茄,但适用于实数和不平等.

您正在寻找的工具在参考手册的 the chapter on Omega中描述,并处理有序环上的各种算术目标:(非) – 线性整数算术和线性有理/实数算术.

它们在Psatz模块中定义,可能需要您安装一些外部解算器.在这种情况下,lra不会(AFAICT)具有外部依赖性并且排除测试目标.