I have done some work on the code of $sign in compar.lisp to look for more
support of Complex expressions and have added some code for debugging. By the
way I have detected that we have a known bug in this code SF [1045920] "a>1 and
b>1, is a+b>2?". I think that it is not really a bug but a missing feature. The
routine signsum does not take into account the shift of an interval by the given
rules for symbols.
We can get more correct results adding the shift of the values (+1 for a and +1
for b) to the left side of the equation and do compare (-2)+(+2)+a+b>0. This can
be generalized with a routine which takes all known numerically bounds of the
symbols and substitute them into the expression. I have writen a subroutine
sign-shift:
(defun sign-shift (expr)
(do ((l ($facts) (cdr l))
(e expr)
(flag) (fact) (num))
((null l) (if flag ($expand e) expr))
(setq fact (car l))
(cond
((or (eq (caar fact) 'mgreaterp)
(eq (caar fact) 'mgeqp))
(cond
((and (symbolp (cadr fact))
(not (member (cadr fact) '($%pi $%e $%gamma $%phi)))
(mnump (caddr fact))
(setq num (caddr fact))
(not (zerop1 num))
(not ($freeof (cadr fact) e)))
(setq flag t)
(if (mminusp num) (setq num (mul -1 num)))
(setq e ($substitute (add (cadr fact) num) (cadr fact) e)))
((and (symbolp (caddr fact))
(not (member (caddr fact) '($%pi $%e $%gamma $%phi)))
(mnump (cadr fact))
(setq num (cadr fact))
(not (zerop1 num))
(not ($freeof (caddr fact) e)))
(setq flag t)
(if (mminusp num) (setq num (mul -1 num)))
(setq e
($substitute (sub (caddr fact) num) (caddr fact) e))))))))
In the routine sigsum two lines of code has to be added:
(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))))
...
With this routine we get:
/* That is the correct result for the reported bug */
(%i2) assume(a>1,b>1);
(%o2) [a > 1,b > 1]
(%i3) is(a+b>2);
(%o3) true
/* It works for more complicated cases too */
(%i4) is(2*a+b>3);
(%o4) true
(%i5) assume(c>2);
(%o5) [c > 2]
(%i6) is(2*a+b+c^2>7);
(%o6) true
/* The same for negative values */
(%i9) assume(x<-1,y<-2,z<-2);
(%o9) [x < -1,y < -2,z < -2]
(%i10) is(x+y<-2);
(%o10) true
(%i11) is(2*x+y<-3);
(%o11) true
/* z^2 is positive and the result is unknown */
(%i12) is(2*x+y+z^2<-7);
(%o12) unknown
/* But z^3 is negative */
(%i15) is(2*x+y+z^3<-12);
(%o15) true
I have tested it for Float, Bigfloat and Rational numbers, too. Not included are
the constants %e, %pi, ... It is possible to extend the code for the constants.
To do this the numerical values of the constants have to be substituted into the
expression by sign-shift.
There still remain open problems when we have values which have positive and
negative values like a > -10. Also intervals like 3 < a < 5 are not correctly
and completly handled.
The testsuite has no problems. Only Problem 84 in rtest_sign.mac gives an
unexpected correct answer.
Do you think we should include the above code in Maxima?
Dieter Kaiser