11
$\begingroup$

Bug introduced in 9.0 or earlier and fixed in 10.2


Reduce[
  ForAll[
     {multiplicant, summandA, summandB}, 
     Element[{multiplicant, summandA, summandB}, Reals], 
     multiplicant*summandA - multiplicant*summandB == multiplicant*(summandA - summandB)]]
True

Duh. So obvious.

Well, it seems it's not obvious enough for Mathematica. See:

    Multiplicant[x_] := 1/((1 + x^2)*(2 + x^2))

    SummandA[x_] := 2*x*(2 + x^2)*Log[2 + x^2]

    SummandB[x_] := 2*x*(1 + x^2)*Log[1 + x^2]

    Reduce[ForAll[
        x, Element[x, Reals],
        Multiplicant[x]*SummandA[x] - Multiplicant[x]*SummandB[x] == 
        Multiplicant[x]*(SummandA[x] - SummandB[x])]]
False

WHAAAT...?!?!

By the law of the distribution of multiplication over addition the correct result of Out[5] should be True.

Or, the other possibility is that my brain got Shrouded in the Shadows of Shades and thus is unable to work properly.

Or, the other other possibility is that I simply cannot use Mma properly and the above sample is alimented with some kind of PEBKAC.

Could you very kindly help me figure out which one of the above three ideas is correct?

Thanks in advance!

$\endgroup$
  • $\begingroup$ This is very peculiar behavior, which I can reproduce on 10.0.2 on a Mac. It's especially weird since FullSimplify[ ExpandAll[ Multiplicant[x]*SummandA[x] - Multiplicant[x]*SummandB[x] - Multiplicant[x]*(SummandA[x] - SummandB[x])]] yields 0 (even without the assumption that x is in Reals). $\endgroup$ – evanb Mar 4 '15 at 22:07
14
$\begingroup$

It is a bug in Reduce.

It affects cases when the input contains a univariate equation f==g inside the ForAll quantifier, f-g is not an explicit polynomial, and Together[f-g] is zero.

Thank you for pointing it out.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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