Proof inequality given some assumptions on the variables

I have an inequality in multiple variables and want to show that it is true given that the variables satisfy some conditions (also formulated as inequalities).

I come from Mathematica, where I can write Reduce[Implies[0<x<1, x>x^2], Reals] and get true as the answer. Is Sage (maybe with some optional package) able to verify these kinds of implications?

This is a simplified implication I want to show: $0 < f \leq 1$ and $z \geq \frac{1}{\sqrt{1+0.8f}}$, implies $$\left((z+f)^2-f^2-1\right)^2+\left((z-1+2f)^2-4f^2\right) > 0$$

So far I tried qepcad but the following code just ran forever:

var('z, f'); qf = qepcad_formula;
qepcad( qf.implies(qf.and_(f>0, f<=1, z>=1/(sqrt(1+4*f/5))), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0) )


Are there better ways to formulate my statement using qepcad, are there better packages available or is Sage not able to help me here?

Note that I don't need help for the given example, as I proved this already. However I have similar more complicated implications of the same form which I need to check using some other CAS than Mathematica. Can Coq do this?

edit retag close merge delete

Sort by ยป oldest newest most voted

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). So, a correct way to formulate your statement using qepcad would be the following (note the additional z>=0 because of the square):

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking and/or error handling). I will have a deeper look to the source code and tell if it could be improved. Thanks for reporting anyway.

EDIT

qepcad seem indeed not able to deal with the sqrt, but Sage interace does not handle the error, here is a qepcad session:

Enter a variable list:
(f,z)
Enter the number of free variables:
0
Enter a prenex formula:
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/sqrt(4/5 f + 1)] ==> ((f + z)^2 - f^2 - 1)^2 + (2 f + z - 1)^2 - 4 f^2 > 0]
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/s

more

Thank you very much! Although the above statement can be restated without square roots, my other formulas cannot. Is there another way without using qepcad?

( 2016-06-24 10:08:19 -0500 )edit