Further code to improve the assume database

-----maxima-bounces at math.utexas.edu wrote: -----


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

The new result isn't wrong, but the old answer is better, isn't it? Since
0 < x < 1 and 0 < y < 1, we have -y - x + 4 < 4. So min(4, - y - x + 4)
should simplify to -y - x + 4. There is a source code comment in
Fourier elimination code: (What is the story with dosimp?)

;; Without the post-fourier-elim-simp, we get

;; (%i2) eqs : [0 < x, x<1, 0 < y, y <1, x+y+z < 4, z > 0]$
;; (%i3) fourier_elim(eqs,[z,y,x]);
;; (%o3) [0<z,z<-y-x+4,0<y,y<min(1,4-x),0<x,x<1]

;; Since 0 < x < 1, Maxima should be able to deduce that min(1,4-x) = 1. So
(%o3)
;; should simplify to [0<z,z<-y-x+4,0<y,y<1,0<x,x<1].
;; To do this simplification, it's necessary to set dosimp to true--why, I
don't
;; know (alternatively, use ($expand e 0 0)).

(defun post-fourier-elim-simp (pos)
  (let ((save-context $context) (new-context (gensym)))

    ;; (a) Declare a new context (b) put every member of the CL list
    ;; pos into the fact database (c) simplify each member of pos
    ;; (d) kill the new context and restore the old context.

    (unwind-protect
 (progn
   ($newcontext new-context)
   (mapcar #'(lambda (s) (mfuncall '$assume s)) pos)
   (let ((dosimp t))
     (setq pos (mapcar #'(lambda (s) (simplifya s nil)) pos))
     (delete-if #'(lambda (s) (equal t (standardize-inequality s))) pos)))

      (if ($member new-context $contexts) ($killcontext new-context))
      (setq $context save-context))))


Currently:

(%i8) load(fourier_elim)$
(%i9) eqs : [0 < x, x < 1, 0 < y, y < 1, 0 < z, x+y+z < 4];

(%o9) [0<x,x<1,0<y,y<1,0<z,z+y+x<4]
(%i10) fourier_elim(eqs,[y,x,z]);
(%o10) [0<y,y<min(1,-z-x+4),0<x,x<min(1,4-z),0<z,z<4]

(%i11) fourier_elim(%,[z,y,x]);
(%o11) [0<z,z<-y-x+4,0<y,y<1,0<x,x<1]

(%i12) fourier_elim(eqs,[z,y,x]);
(%o12) [0<z,z<-y-x+4,0<y,y<1,0<x,x<1]