SF[2477795] "assume":problems with fractions or multiples of %pi and %e



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

>One?problem?for?me?is,?that?it?seems?to?be?necessary?to?write?code?with
>low?level?database?functions.?I?have?tried?several?times?to?understand
>the?code?of?the?database,?but?I?have?no?idea?how?it?really?works.

>Because I have problems to understand the code of the database, I have
>no idea how to start to improve the database.

The fact database would benefit if it contained more information:

 (a) the facts as input by the user,

 (b) upper and lower bounds for all assumed variables (would make some
     sign queries super fast),

 (c) a flag that indicates if Maxima knows for *certain* that the
     facts are consistent (Maxima doesn't complain when it should: Maxima
     has no way to know if assume(bessel_j(a,a^2 -b) > 0, cos(a + b) > a-b)
     is consistent, for example)

 (d) a processed form (possibly Fourier elimination for linear assumptions)
 for the facts

I don't know how much of this data is in the fact database. When I wrote
the Fourier elimination
code, I tried this:

(%i1) load("mysign.mac")$
(%i2) assume(a < %pi/2);
(%o2) [%pi/2>a]

(%i4) mysign(%pi - a);
(%o4) pos

(%i5) sign(%pi - a);
(%o5) pnz

The code is super inefficient (and completely untested). We also have
simplex code
as well.

load(fourier_elim);

inequation_facts() :=  subset(setify(facts()), lambda([s], not(mapatom(s))
                             and
                             member(op(s), ["<", "<=", "=", "#",">", ">=",
                             'equal])));

mysign(e,[f]) := block([listconstvars : false, v, s_z, s_p, s_pz, s_nz,
s_n, s_pn],

  f : listify(union(setify(f), inequation_facts())),
  f : subst('equal = "=", f),
  v : listify(setify(append(listofvars(e),listofvars(f)))),

  if 'emptyset = fourier_elim(f,v) then (print("emtpy assume"), return
  ('pnz)),

  s_z  : fourier_elim(cons(e # 0, f), v),
  if s_z = 'emptyset then return('zero),

  s_p  : fourier_elim(cons(e <= 0, f), v),
  if s_p = 'emptyset then return('pos),

  s_pz : fourier_elim(cons(e < 0, f), v),
  if s_pz = 'emptyset then return('pz),

  s_nz :  fourier_elim(cons(e >= 0, f), v),
  if s_nz = 'emptyset then return('neg),

  s_n  : fourier_elim(cons(e > 0, f), v),
  if s_n = 'emptyset then return('nz),

  s_pn : fourier_elim(cons(e = 0, f), v),
  if s_pn = 'emptyset then return('pn),

  'pnz);

Barton