Handling of assume(abs(x)<pos)



I have proposed an extension to assume and forget to handle expression like
abs(x)<pos, where pos is an positive expression. See the bug report on this
topic: "assume(abs(x)<1) should imply x<1 and x>-1" - ID: 1041570.

With the proposed extension we get:

(%i3) assume(abs(x)<1);
(%o3) [abs(x) < 1]
(%i4) facts();
(%o4) [1 > x,x > -1,1 > abs(x)]
(%i5) sign(x-1);
(%o5) neg
(%i6) sign(1-x);
(%o6) pos

An example with a positive symbol as an upper bound:

(%i1) assume(y>0);
(%o1) [y > 0]
(%i2) assume(abs(x)<y);
(%o2) [y > abs(x)]
(%i3) facts();
(%o3) [y > 0,y > x,y+x > 0,y > abs(x)]
(%i4) sign(y-x);
(%o4) pos
(%i5) sign(-x+y);
(%o5) pos
(%i6) sign(-x-y);
(%o6) neg
(%i7) sign(x-y);
(%o7) neg

This will work together with forget:

(%i2) assume(abs(x)<1)$
(%i3) facts();
(%o3) [1 > x,x > -1,1 > abs(x)]
(%i4) forget(abs(x)<1)$
(%i5) facts();
(%o5) []

The bound has to be a positive value:

(%i6) assume(abs(x)<-1);
(%o6) [inconsistent]

It works for positive expressions like 2*y+1, where y is declared to be
positive, too.

So, do you think it would be nice to have this extension?

Dieter Kaiser