RealField.REAL_ARITH_TAC unable to prove -1r / x - 1 / -x >= 0

[someplaceguy]

I've noticed that RealField.REAL_ARITH_TAC is unable to prove certain goals which naively I would've expected it to prove:

1. -1r / x + -1 * (1 / (-1 * x)) >= 0
2. -1r / x + (-1 / (-1 * x)) >= 0
3. -1r / x + -1 / -x >= 0
4. -1r / x - 1 / -x >= 0

The following goal is somewhat similar to 4 but REAL_ARITH_TAC can prove it: -1r / x + 1 / x >= 0.

cc @binghe

[someplaceguy]

Also, the following succeeds: x <> 0r ==> x < 0 \/ x > 0
But the following fails: x <> 0r ==> 1/x < 0 \/ 1/x > 0

[someplaceguy]

Ah, I think this is nonlinear arithmetic, so it's probably expected. Feel free to close the issue and sorry for the noise!

[mn200]

I think it's arguable either way. I'd expect the big multiplicative blobs to get normalised so that they turn into things like the example that works.

[binghe]

I think it's arguable either way. I'd expect the big multiplicative blobs to get normalised so that they turn into things like the example that works.

I will check if the simplification (pre)steps inside REAL_ARITH can be fixed or improved to get better results. Meanwhile, I think the following result of SCONV (realSimps is loaded) is also not perfect:

> SCONV [] ``-1r / x + -1 * (1 / (-1 * x))``;
val it = |- -1 / x + -1 * (1 / (-1 * x)) = -1 / x + realinv x

I would expect it be zero.

[binghe]

I think currently the normalizer of real expressions thinks -1 / x cannot be further simplified, because it's "minimal". I think it makes sense to let it go further to - inv x (- realinv x).