5

Is there a way to automatically prove simple inequalities like 1/2 >= 0?, i.e.

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

Example test: /2 >= 0.

I haven't much experience with ring or field, and I am having trouble with even proving simple equalities such as 1/2 = 2/4.

What I am looking for is something like omega but works for real numbers and inequalities.

Improve this question
2
  • 2
    @Johan, I rolled back the tag change from real-number to floating-point because I intended ask about the real real numbers, not their floating-point approximations.
    – thor
    Commented Mar 19, 2016 at 18:44
  • The problem is that real-number only has 7 hits on it, so I think you'd better look for a tag that is in regular use. I'm sure there is a synonym that covers what you want.
    – Johan
    Commented Mar 19, 2016 at 18:50

1 Answer 1

Reset to default
3

The tools you are looking for are described in the chapter on Omega of the reference manual and deal with various arithmetic goals over ordered rings: (non)-linear integer arithmetic, and linear rational / real arithmetic.

They are defined in the Psatz module and may require you to install some external solvers. In this case, lra does not (AFAICT) have external dependencies and discharges the test goal.

Improve this answer

Not the answer you're looking for? Browse other questions tagged or ask your own question.