(x - a)(x + a) <= 0 is answered with an interval whose endpoints are in the wrong order for one sign of a, and the solver has no way to say "it depends on the sign of a".
The solution set is [-|a|, |a|]. The solver builds (root1; root2) from the two roots without knowing which is smaller, so one of the two signs of a always comes out as an empty interval.
Measured on e38da2b9
(x - a)(x + a) <= 0 -> [a; -a]
which is [-|a|, |a|] for a < 0 — correct — and empty for a > 0, where the answer is [-a, a].
It reads as correct because sqrt(4a^2) was simplifying to 2a. That is only true for a >= 0, and it is being fixed as part of #752; with it gone the same equation answers
{ a, -a } \/ (sqrt(a^2); -sqrt(a^2))
whose interval is (|a|; -|a|) — empty for either sign, so the endpoints survive and the interior is lost. Neither form is right for both signs. The old one was right for half the cases by resting on an unsound rewrite, and that is the whole of why this had not been noticed.
What it needs
A case split on the sign of a, which the library can express — Piecewise is there, and the solver already produces Providedf conditions elsewhere. Something of the shape
piecewise([-a; a] provided a > 0, [a; -a] provided a < 0, { 0 } provided a = 0)
Until then the honest answer for a symbolic coefficient is arguably the unevaluated inequality rather than an interval that is right half the time.
The concrete cases are unaffected either way: (x - 2)(x + 2) <= 0 gives [-2; 2] and > 0 gives (-oo; -2) \/ (2; +oo), both correct, because a numeric coefficient has a known sign.
Note
SolveInequality.Test pins [a; -a], so this issue is what that test was really recording. It is updated alongside #752 to the new output with a comment pointing here, rather than being quietly deleted — the expectation was evidence, and it is still evidence, just of something other than correctness.
(x - a)(x + a) <= 0is answered with an interval whose endpoints are in the wrong order for one sign ofa, and the solver has no way to say "it depends on the sign ofa".The solution set is
[-|a|, |a|]. The solver builds(root1; root2)from the two roots without knowing which is smaller, so one of the two signs ofaalways comes out as an empty interval.Measured on
e38da2b9which is
[-|a|, |a|]fora < 0— correct — and empty fora > 0, where the answer is[-a, a].It reads as correct because
sqrt(4a^2)was simplifying to2a. That is only true fora >= 0, and it is being fixed as part of #752; with it gone the same equation answerswhose interval is
(|a|; -|a|)— empty for either sign, so the endpoints survive and the interior is lost. Neither form is right for both signs. The old one was right for half the cases by resting on an unsound rewrite, and that is the whole of why this had not been noticed.What it needs
A case split on the sign of
a, which the library can express —Piecewiseis there, and the solver already producesProvidedfconditions elsewhere. Something of the shapeUntil then the honest answer for a symbolic coefficient is arguably the unevaluated inequality rather than an interval that is right half the time.
The concrete cases are unaffected either way:
(x - 2)(x + 2) <= 0gives[-2; 2]and> 0gives(-oo; -2) \/ (2; +oo), both correct, because a numeric coefficient has a known sign.Note
SolveInequality.Testpins[a; -a], so this issue is what that test was really recording. It is updated alongside #752 to the new output with a comment pointing here, rather than being quietly deleted — the expectation was evidence, and it is still evidence, just of something other than correctness.