Further code to improve the assume database

We have the known bug ID: 1045920 "a>1 and b>1, is a+b>2?" 

(%i2) assume(a>1,b>1);
(%o2) [a > 1,b > 1]

(%i3) sign(a+b-2);
(%o3) pnz

I have a routine sign-shift which will correct this result:

(%i4) load("sign-shift.lisp");
(%o4) "sign-shift.lisp"

(%i5) sign(a+b-2);
(%o5) pos

It will work for a lot of more cases too:

(%i8) assume(a > 1,b > 1,c > 2)$

(%i2) is(b+a > 2)
(%o2) true

(%i4) is(b+2*a > 3)
(%o4) true

(%i6) is(c^2+b+2*a > 7)
(%o6) true

It works for negative bounds too:

(%i8) assume(x < -1,y < -2,z < -2)$

(%i10) is(y+x < -3)
(%o10) true

(%i12) is(y+2*x < -4)
(%o12) true

z^2 is positive and the following sign is unknown:

(%i14) is(z^2+y+2*x < -7)
(%o14) unknown

z^3 is negative and the test will give true again:

(%i16) is(z^3+y+2*x < -12)
(%o16) true

I have no problems with the testsuite and the share_testsuite with the
exception of one example:

********************** Problem 40 ***************
Input:
fourier_elim(fourier_elim(eqs, [y, x, z]), [z, y, x])


Result:
[0 < z, z < min(4, - y - x + 4), 0 < y, y < 1, 0 < x, x < 1]

This differed from the expected result:
[0 < z, z < 4 - x - y, 0 < y, y < 1, 0 < x, x < 1]

124/125 tests passed (not counting 5 expected errors).


I know nothing about the code of fourier_elim. My question is, if the
new result is really an error or if we can accept it. Perhaps
fourier_elim can be improved to take advantage of the extended
functionality of $sign?

This is the code of sign-shift:

(defun sign-shift (expr)
  (do ((l (append (cdr (facts1 '$learndata)) (cdr (facts1 $context)))
(cdr l))
       (e expr)
       (flag) (fact) (num))
      ((null l) (if flag ($expand e) expr))
    (setq fact (car l))
    (when (eq (caar fact) 'mgreaterp)
      ;; Do we have something like a>2 or a<-1 on the list of facts?
      (cond ((and (symbolp (cadr fact))
                  (not ($freeof (cadr fact) e))
                  (not (member (cadr fact) '($%pi $%e $%gamma $%phi)))
                  (mnump (setq num (caddr fact)))
                  (not (zerop1 num)))
             (setq flag t)
             (if (mminusp num) (setq num (mul -1 num)))
             (setq e (maxima-substitute (add (cadr fact) num) (cadr
fact) e)))
            ((and (symbolp (caddr fact))
                  (not ($freeof (caddr fact) e))
                  (not (member (caddr fact) '($%pi $%e $%gamma $%phi)))
                  (mnump (setq num (cadr fact)))
                  (not (zerop1 num)))
             (setq flag t)
             (if (mminusp num) (setq num (mul -1 num)))
             (setq e (maxima-substitute
                       (sub (caddr fact) num) (caddr fact) e)))))))


The routine sign-shift has to be called in the routine signsum in
compar.lisp:

(defun signsum (x)
  (setq x (sign-shift x))
  ;; x might be simplified to an atom in sign-shift
  (when (atom x) (setq x (cons '(mplus) (list x))))


Dieter Kaiser