[Maxima-bugs] [ maxima-Bugs-1041570 ] assume(abs(x)<1) should imply x<1 and x>-1

[SourceForge.net <no...@so...>]

Bugs item #1041570, was opened at 2004-10-06 18:05
Message generated for change (Comment added) made by crategus
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=104933&aid=1041570&group_id=4933

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: Lisp Core - Assume
Group: Includes proposed fix
>Status: Closed
>Resolution: Fixed
Priority: 5
Private: No
Submitted By: Stavros Macrakis (macrakis)
Assigned to: Nobody/Anonymous (nobody)
Summary: assume(abs(x)<1) should imply x<1 and x>-1

Initial Comment:
assume(abs(x)<1)$

sign(x-1) => doesn't know (should be NEG)
sign(1-x) => doesn't know (should be POS)

assume(x>1) => doesn't notice contradiction

The easy fix is of course to make the original
assumption add x<1 and x>-1 to the database, but how do
you ensure that they get *removed* if you remove
(forget) the original assertion.  And what if x<1 has
been explicitly added in the meantime?

Same problem in the reverse direction:

assume(y<1,y>-1)$
sign(abs(y)-1) => PNZ (should be NEG)


----------------------------------------------------------------------

>Comment By: Dieter Kaiser (crategus)
Date: 2009-05-22 13:05

Message:
The suggested extension (with some modifications) has been implemented. The
examples assume(abs(x)<1), forget(abs(x)<1), sign(x-1), sign(1-x) work as
expected. assume(x>1) will give inconsistent. More general cases will work
too.

The reverse direction is not implemented.

Closing this bug report as fixed, because the introducing problem now
works.

Dieter Kaiser

----------------------------------------------------------------------

Comment By: Dieter Kaiser (crategus)
Date: 2009-05-08 18:13

Message:
I think the handling of the abs funtion is a missing feature of assume.

This would be some code to add this feature in a way assume can handle
it:

;; This function is like isinop, but returns in addition
;; the expression with the operator and not only T or NIL

(defmfun is-op-in-expr-p (exp var)
  (let ((tmp nil))
  (cond ((atom exp) nil)
	((and (eq (caar exp) var) 
              (not (member 'array (cdar exp) :test #'eq)))
         (setq tmp exp))
	(t 
         (do ((exp (cdr exp) (cdr exp))) ((null exp))
	   (cond ((setq tmp (is-op-in-expr-p (car exp) var))
                  (return tmp))))))))

;; The modified routine assume

(defmfun assume (pat)
  (if (and (not (atom pat))
	   (eq (caar pat) 'mnot)
	   (eq (caaadr pat) '$equal))
      (setq pat `(($notequal) ,@(cdadr pat))))
  (let (tmp)
    ;; Look for mabs in the expression, check the bounds and substitute
    ;; accordingly, e. g. abs(x)<1 --> x<1 and -x<1
    (when (and (setq tmp (is-op-in-expr-p pat 'mabs))
               (or (and (eq (caar pat) 'mlessp)
                        (is-op-in-expr-p (cadr pat) 'mabs)
                        (member ($sign (caddr pat)) '($pos $pz)))
                   (and (eq (caar pat) 'mgreaterp)
                        (member ($sign (cadr pat)) '($pos $pz))
                        (is-op-in-expr-p (caddr pat) 'mabs))))
      (let ((pat1 ($substitute (cadr tmp) tmp pat))
            (pat2 ($substitute (mul -1 (cadr tmp)) tmp pat)))
        (assume pat1)
        (assume pat2))))
  (let ((dummy (let ($assume_pos) (car (mevalp1 pat)))))
    (cond ((eq dummy t) '$redundant)
	  ((null dummy) '$inconsistent)
	  ((atom dummy) '$meaningless)
	  (t (learn pat t)))))

;; The modified routine forget

(defmfun forget (pat)
  (cond (($listp pat)
	 (cons '(mlist simp) (mapcar #'forget1 (cdr pat))))
	(t         
         (let (tmp)
           (when (setq tmp (is-op-in-expr-p pat 'mabs))
             (let ((pat1 ($substitute (cadr tmp) tmp pat))
                   (pat2 ($substitute (mul -1 (cadr tmp)) tmp pat)))
               (forget1 pat1)
               (forget1 pat2))))
         (forget1 pat))))

With this 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]

This does not sovlve the problem for the reverse direction. This feature
might be added to the $sign-function.

Dieter Kaiser

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=104933&aid=1041570&group_id=4933