anomalous true-false test (2.8.99)

Willard, Daniel Dr

The following program gives an erroneous answer to the ”is” test half-way through, but a correct one at the end. The only difference is in the ”assume” statement just ahead of the test: whether to assume v = or <= 1/(P*q^n).

The answer should be ”true” regardless. What gives? I am using Maple V 5.1 on a PC.

Robert Israel (4.8.99)

Actually Maple’s answer is quite correct in this case: it is not true in general that t(n) >= t(n+1) under the assumptions n>=0,v<=1/(P*q^n).

For example:

> normal(t(1) - t(2)); 
                                          v~ (-81 + 4 v~ ) 
                                 -24 -------------------------- 
                                               2             2 
                                     (27 + 4 v~ ) (243 + 4 v~ )

The sign depends on the sign of v. But you didn’t tell Maple anything that determines that sign. You probably meant to assume in addition that v >= 0.

> additionally(v >= 0); 
> is(t(n) >= t(n+1)); 

The ”assume” facility is rather limited in capabilities, so it’s not really all that surprising when a result is ”FAIL”. In general it’s a very difficult problem to decide when an expression is nonnegative for all values of the variables in some region defined by inequalities. In this particular case, I think I can trace some of Maple’s difficulties to some rather simple deficiencies.

> is(3^n > 0); 

It seems that Maple doesn’t know that a positive power of 3 is positive. In fact it doesn’t even know that this is real. Well, we can tell Maple this:

> additionally(3^n > 0);

Unfortunately, this still doesn’t help. Even though Maple now ”knows” that 3^n > 0, it doesn’t seem able to use that information in other expressions.

> is ((3^n)^2 > 0); 
> assume(x > 0); is(x + 3^n > 0); 

It may actually be better to use ”exp”, which Maple seems to know more about, rather than powers of a specific number. So I’ll change q to exp(lnq), where lnq < 0 (which implies 0 < q < 1).


Helmut Kahovec (6.8.99)

 >The answer should be "true" regardless.

I disagree. In the first case n=1 and v=-1 do not contradict your assumptions. If you substitute them into t(n) and t(n+1) then you get:

In the second case assuming v=1/(p*q^n) is virtually the same as substituting it into t(n)-t(n+1). The latter is zero for all n and thus greater than or equal to zero, anyway:

If you make more specific assumptions about n and v then Maple fails even if _EnvTry is set to ’hard’:

The reason is that Maple cannot determine whether 3^n (or 9^n) is greater than or equal to zero:

This is a weak point of the assume facility, of course.