On Mar. 15, Stavros Macrakis wrote
--------------------------
>I was wondering why you assume both not equal (x,a) and x>a, since the
>second implies the first? Have you found problematic cases? If so, those
>should be reported as bugs.
---------------------------------------
You are correct that I found cases where I needed to insert both
assumptions to avoid integrate questions.
One case I can find quickly is (using 5.26.0gcl):
------------------------------------------------------
(%i1) display2d:false$
(%i2) facts();
(%o2) []
(%i3) assume ( x >= 0, x <= 1 )$
(%i4) integrate (integrate (log (x+y), y, 0, 1), x, 0, 1);
Is x - 1.0 negative or zero?
n;
(%o4) (4*log(2)-3)/2
(%i5) forget( x >= 0, x <= 1)$
(%i6) assume( x >= 0, x < 1, not equal (x, 1));
(%o6) [x >= 0, x < 1, redundant]
(%i7) facts();
(%o7) [ x >= 0, 1 > x]
(%i8) integrate (integrate (log (x+y), y, 0, 1), x, 0, 1);
(%o8) (4*log(2)-3)/2
(%i9) forget( x >= 0, x < 1, not equal (x,1));
(%o9) [ x >= 0, x < 1, notequal (x, 1)]
(%i10) facts();
(%o10) []
(%i11) assume (not equal (x,0), x > 0, x < 1, not equal (x, 1));
(%o11) [notequal (x, 0), x > 0, x < 1, redundant]
(%i12) facts();
(%o12) [notequal (x, 0), x > 0, 1 > x]
(%i13) integrate (integrate (log (x+y), y, 0, 1), x, 0, 1);
(%o13) (4*log(2)-3)/2
-----------------------------------------------
Although the code considered not equal(x,1) to be "redundant",
and it was not included in the list of facts(), the method
avoided the question from integrate.
Ted