Как автоматически доказать простое неравенство действительных чисел в 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 или же fieldи у меня возникают проблемы даже с доказательством простых равенств, таких как1/2 = 2/4,

Я ищу что-то вроде omega но работает на реальные цифры и неравенства.

Answer 1

Инструменты, которые вы ищете, описаны в главе о Omega справочного руководства и касаются различных арифметических целей над упорядоченными кольцами: (не)-линейная целочисленная арифметика и линейная рациональная / вещественная арифметика.

Они определены в Psatz модуль и может потребовать от вас установить некоторые внешние решатели. В этом случае, lra не имеет (AFAICT) внешних зависимостей и разряжает test Цель.