#5699 assume((x+1)^3 > 0) adds x+1 > 0, but is() and forget() do not see it

[David Scherfgen]

By Claude:

assume((x+1)^3 > 0) says it added x+1 > 0, and facts() lists that fact, but is and sign cannot use it, and forget(x+1 > 0) cannot remove it:

(%i1) display2d : false$
(%i2) assume((x+1)^3 > 0);
(%o2) [x+1 > 0]
(%i3) is(x+1 > 0);
(%o3) unknown
(%i4) is(x > -1);
(%o4) unknown
(%i5) sign(x+1);
(%o5) pnz
(%i6) forget(x+1 > 0);
(%o6) [redundant]
(%i7) facts();
(%o7) [x+1 > 0]

(%o3), (%o4) and (%o5) should be true, true and pos, and forget should remove the fact. Only forget((x+1)^3 > 0) does. The same happens with a reciprocal, an odd root, two variables and notequal, and an answer to asksign is lost the same way:

(%i8) assume(1/(a-1) > 0, (b-c)^3 > 0, (1-d)^(1/3) < 0, notequal((k-2)^3, 0));
(%o8) [a-1 > 0,b-c > 0,1-d < 0,notequal(k-2,0)]
(%i9) [is(a > 1), is(b > c), is(d > 1), is(notequal(k, 2))];
(%o9) [unknown,unknown,unknown,unknown]
(%i10) forget(a > 1, b > c, d > 1, notequal(k, 2));
(%o10) [redundant,redundant,redundant,redundant]
(%i11) [asksign(1/(u-1)), sign(u-1)];
Is 1/(u-1) positive or negative?
pos;
(%o11) [pos,pnz]

With a symbol as the base, or with the base itself assumed, everything works:

(%i12) assume(y^3 > 0, z+1 > 0);
(%o12) [y > 0,z > -1]
(%i13) [is(y > 0), is(z+1 > 0)];
(%o13) [true,true]

assume returns the facts it added to the database, so the database should be able to answer exactly those facts, and forget should be able to remove them. (%o12) hints at why it cannot: assumed directly, z+1 > 0 comes back as z > -1, so the x+1 > 0 from (%i2) is stored in another form. Bug #5177 was the same kind of problem for the sub-facts of notequal.

[David Scherfgen]

Fixed by commit [b61fbd].