make assume behave more consistently and catch inconsistent assumptions

[zimmermann6]

sage: assume(x > 0)
sage: sqrt(x^2)
x
sage: assume(x < 0)
sage: sqrt(x^2)
x

Maybe it is not allowed to make two assumptions on the same variable, without any forget inbetween, anyway the documentation should be clear about this, or a warning should be issued.
Also, is there a way to know which assumptions were made on a given variable (like about in
Maple)?

CC: @burcin @robertwb @jasongrout @robert-marik

Component: calculus

Author: Karl-Dieter Crisman

Reviewer: Jason Grout, Robert Marik

Merged: sage-4.3.alpha0

Issue created by migration from https://trac.sagemath.org/ticket/1163

[jasongrout]

comment:1

A couple of notes:

The "assumptions()" command lists assumptions. See assumptions? for documentation.

It seems that the order in which the assumptions are made matters (only the first assumption is used below).

Should assume complain if we say that x>0 and x<0?

sage: assumptions()
[]
sage: assume(x<0)
sage: sqrt(x^2)
-x
sage: assume(x>0)
sage: sqrt(x^2)
-x
sage: assumptions()
[x < 0, x > 0]
sage: forget()
sage: assumptions()
[]
sage: assume(x>0)
sage: assume(x<0)
sage: assumptions()
[x > 0, x < 0]
sage: sqrt(x^2)
x

[zimmermann6]

comment:2

Sorry I did not know about the assumptions() command. Maybe assume? should point to it.
Is a SEE ALSO section possible in the documentation? Also consider (from Wester's test suite):

sage: assume(x>=y, y>=z,z>=x)
sage: assumptions()
[x >= y, y >= z, z >= x]
sage: print bool(x==z)
False

Yes assume should complain if we say that x>0 and x<0 (at least if it can lead to wrong results).

[zimmermann6]

comment:3

More strange results:

sage: assume(x > 0)
sage: bool (x <> 1)
True

and:

sage: assume(x <= 1, x >= 1)
sage: bool(x==1)
False

[jasongrout]

comment:4

Those are some unsettling results. I don't know if this is the easiest route, but it seems like QEPCAD could handle some of these if it were integrated into SAGE. For example, we can ask QEPCAD the following questions. In these, (Ex) means "there exists an x" and (Ax) means "For all x" and "/=" means "not equal".

• (Ex)(Ey)(Ez) [ x>=y /\ y>=z /\ z>=x /\ x/=z] (returns False)
• (Ex) [ x>0 /\ x/= 1] (returns True)
• (Ex) [ x>0 /\ x=1] (returns True)
• (Ex) [ x<=1 /\ x>=1 /\ x /= 1] (returns False)

Here's another example:

• (Ax)(Ay) [x<sup>2+y</sup>2>=0] (returns True).

We could ask much more general questions too.

I've been (very slowly) working on interfacing QEPCAD to SAGE, but lack of time and the learning process of making an interface is slowing me down. Also, we need to follow up on the license issue. For progress in this interface, see #772 )

[jasongrout]

comment:5

Apparently Maxima complains (behind the scenes?):

Maxima 5.12.0 http://maxima.sourceforge.net
Using Lisp GNU Common Lisp (GCL) GCL 2.6.7 (aka GCL)
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
This is a development version of Maxima. The function bug_report()
provides bug reporting information.
(%i1) assume(x<0);
(%o1)                               [x < 0]
(%i2) assume(x>0);
(%o2)                           [inconsistent]

[jasongrout]

comment:6

More results from Maxima:

Maxima 5.12.0 http://maxima.sourceforge.net
Using Lisp GNU Common Lisp (GCL) GCL 2.6.7 (aka GCL)
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
This is a development version of Maxima. The function bug_report()
provides bug reporting information.
(%i1) assume(x>=y,y>=z,z>=x);
(%o1)                      [x >= y, y >= z, z >= x]
(%i2) is(x=z);
(%o2)                                false

Maxima 5.12.0 http://maxima.sourceforge.net
Using Lisp GNU Common Lisp (GCL) GCL 2.6.7 (aka GCL)
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
This is a development version of Maxima. The function bug_report()
provides bug reporting information.
(%i1) assume(x>0);
(%o1)                               [x > 0]
(%i2) is(x#1);
(%o2)                                true

and

Maxima 5.12.0 http://maxima.sourceforge.net
Using Lisp GNU Common Lisp (GCL) GCL 2.6.7 (aka GCL)
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
This is a development version of Maxima. The function bug_report()
provides bug reporting information.
(%i1) assume(x<=1);
(%o1)                              [x <= 1]
(%i2) assume(x>=1);
(%o2)                              [x >= 1]
(%i3) is(x=1);
(%o3)                                false

So it seems like the problem is the Maxima assumptions engine. According to the documentation at http://maxima.sourceforge.net/docs/manual/en/maxima_11.html

Maxima's deduction mechanism is not very strong; there are many obvious consequences which cannot be determined by is. This is a known weakness.

[jasongrout]

comment:7

One more note:

QEPCAD also simplifies the expression [x>=y /\ y>=z /\ z>= x] to [y-x=0 /\ z-y = 0].

[kcrisman]

comment:9

At the very least this ticket should upgrade the documentation for assume? and assumptions? to point out that one should always forget() before assuming something new about a variable.

A related ticket is #3277, which would implement a block to automatically call assume and forget if desired. Also, #772 is now an experimental spkg.