Ask Your Question
3

Proof inequality given some assumptions on the variables

asked 2016-06-07 18:08:24 -0500

Lux gravatar image

updated 2016-06-09 04:21:32 -0500

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 flag offensive close merge delete

1 answer

Sort by ยป oldest newest most voted
1

answered 2016-06-10 17:17:50 -0500

tmonteil gravatar image

updated 2016-06-11 07:47:47 -0500

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]
Error RPFACTREAD: Digit was expected.
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/s
edit flag offensive delete link more

Comments

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?

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

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

1 follower

Stats

Asked: 2016-06-07 18:06:41 -0500

Seen: 93 times

Last updated: Jun 11 '16