Discrepancy in assumptions and assume

[Duc Trung Ha]

Hola,

would anybody be so kind and explain to me the mechanism behind "assume(sth)"?

I strive to understand (without success, unfortunaly) following behavior:

sage: assume(x-2 <= 0)
sage: assumptions()      
[x - 2 <= 0]
sage: assume(x-1 <= 0)
sage: assumptions()  
[x - 2 <= 0]

"x-1 <= 0" is not redundant here, is it?

sage: assume(x<= 1)  
sage: assumptions()
[x - 2 <= 0, x <= 1]

...and now it works, with equivalent form "x <= 1". Is there some sort of
"elite category" of "correct forms" explaining such a vast superiority of "x-1
<= 0" over "x <= 1" form??

sage: assume(x-1<=0)
sage: assumptions()
[x - 2 <= 0, x <= 1]

...just proves the equivalence of aforementioned forms...

sage: forget(x-1<=0)
sage: assumptions()
[x <= 1]

...where [x <= 2] should be the correct list of assumptions. This completely
undermines my understanding of mathematics :-(

What am I doing incorrectly/wrong? Most likely I must have just missed some
tiny yet important detail...

Duc Trung Ha
Sage Version 4.8, Release Date: 2012-01-20
Intel(R) Core(TM) i5-2410M CPU @ 2.30GHz
Ubuntu 12.04

[John H Palmieri]

On Thursday, May 10, 2012 2:41:07 PM UTC-7, Duc Trung Ha wrote:

Hola,

would anybody be so kind and explain to me the mechanism behind "assume(sth)"?

The mechanism seems to be broken. Actually, the mechanism that compares boolean expressions seems to be broken, which means that assumptions don't work right, either.

    sage: a = (x - 2 <= 0)
    sage: b = (x <= 2)
    sage: c = (x - 1 <= 0)
    sage: a == b
    False
    sage: a == c
    True
    sage: b == c
    False

The first two claimed equalities are a bit troubling...

--
John

[Duc Trung Ha]

Is there any way to fix it (at least by yourself, in Sage's source code) ?

[kcrisman]

Remember, False = we didn't/couldn't prove it was True, so the first one is annoying but technically ok.

As to the original post, we must be preprocessing things not quite right. Maxima:

(%i1) assume(x-2<=0);

(%o1)                              [x <= 2]

(%i2) assume(x-1<=0);

(%o2)                              [x <= 1]

(%i3) assumptions;

(%o3)                             assumptions

(%i4) facts();

(%o4)                          [2 >= x, 1 >= x]

And indeed

sage: c = (x-2<=0)

sage: maxima.assume(c._maxima_init_assume_())

[x<=2]

sage: c = (x-2<=0)

sage: maxima.assume(c._maxima_init_assume_())

[redundant]

But we don't use "facts()" per se, we instead append the relation x-2<=0 directly to the assumption list.

sage: a = (x-1<=0)

sage: sage.symbolic.assumptions._assumptions

[x - 2 <= 0]

sage: if a in sage.symbolic.assumptions._assumptions:

    print 'yes'

....:     

yes

Aack!  Something horrible is happening here.  Okay, John, now I understand your somewhat cryptic post; since 

sage: a == c

True

assumptions thinks this is already in the list.  And this is already true in a Sage from two years ago (4.4.4).  Why on earth is a == c True?   Apparently Ginac thinks so?

cdef int _cmp_c_impl(left, Element right) except -2:

return left._gobj.compare((<Expression>right)._gobj)

I must be missing something here.  Burcin, any ideas - maybe this is already on some ticket that should have been merged but got hung up on a technicality, there was some stuff about symbolic expression comparisons a while back.

Sorry I had to go through all this - hopefully it clarifies things a little for the original poster.  

[Keshav Kini]

John H Palmieri <jhpalm...@gmail.com> writes:
> The mechanism seems to be broken. Actually, the mechanism that compares boolean
> expressions seems to be broken, which means that assumptions don't work right,
> either.

Relevant: #11309, a ticket I worked on a bit at a Sage Days last year
with Burcin. http://trac.sagemath.org/sage_trac/ticket/11309

-Keshav

----
Join us in #sagemath on irc.freenode.net !

[kcrisman]

On Friday, May 11, 2012 2:39:55 AM UTC-4, Keshav Kini wrote:

> The mechanism seems to be broken. Actually, the mechanism that compares boolean
> expressions seems to be broken, which means that assumptions don't work right,
> either.

Relevant: #11309, a ticket I worked on a bit at a Sage Days last year
with Burcin. http://trac.sagemath.org/sage_trac/ticket/11309

Ah, I knew there was something.  And it still applies...

 Yes, it seems to fix this issue.

sage: c = (x-2<=0)

sage: assume(c)

sage: a = (x-1<=0)

sage:  if a in sage.symbolic.assumptions._assumptions:

....:     print 'yes'

....:     

sage: assumptions()

[x - 2 <= 0]

sage: assume(a)

sage: assumptions()

[x - 2 <= 0, x - 1 <= 0]

I've updated the ticket with this.  There is still some discussion there, a year old, about nested expressions... once again, the perfect has become the enemy of fixing at all.

- kcrisman

[Michael Orlitzky]

On 05/11/12 09:23, kcrisman wrote:
>
> I've updated the ticket with this. There is still some discussion
> there, a year old, about nested expressions... once again, the perfect
> has become the enemy of fixing at all.
>

I haven't looked at this closely, but why not just open another ticket
for the complicated stuff? Copy/paste a few test cases, and fix the easy
ones in the original ticket.

People like to solve easy problems for big returns, and avoid the
opposite. It's also easier to review two small tickets than it is one
big one.

[kcrisman]

I don't think you are contradicting me.  I'm sorry if it wasn't clear that this was sort of my point :( but I didn't want to overrule people who actually know something about symbolic expressions in general. 

[Keshav Kini]

kcrisman <kcri...@gmail.com> writes:
> I've updated the ticket with this. There is still some discussion there, a
> year old, about nested expressions... once again, the perfect has become the
> enemy of fixing at all.

You're absolutely right. Let's make another ticket for nested comparison
expressions instead.

[Keshav Kini]

kcrisman <kcri...@gmail.com> writes:
> I've updated the ticket with this. There is still some discussion there, a
> year old, about nested expressions... once again, the perfect has become the
> enemy of fixing at all.

The ticket should now be ready for review, preferably by someone who
knows more about Sage's symbolics than I do.