Opened 9 years ago

Last modified 7 years ago

#11309 closed defect

Sage sees -x +y > 0, -y + x >= 0, and x -y > 0 as equivalent — at Version 37

Reported by: tnv Owned by: burcin
Priority: major Milestone: sage-5.1
Component: symbolics Keywords: inequality equality relational sd31 __richcmp__ sd40.5
Cc: kini, kcrisman, tnv Merged in:
Authors: Keshav Kini, Burcin Erocal Reviewers: Karl-Dieter Crisman, ThanhVu Nguyen
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Description (last modified by kini)

-x + y > 0 and x - y > 0 are treated the same in Sage.

sage: version()
'Sage Version 4.6.2, Release Date: 2011-02-25'

sage: (-x +y < 0) in [x -y < 0] 
True 

Set([-x +y >= 0,x -y >= 0]) 
{-x + y >= 0} 

and they have the same Hash

sage: var('x,y') 
(x, y) 
sage: hash(-x + y > 0 )
1221566266
sage: hash(-x + y >= 0 )
1221566266
sage: hash(x - y >= 0 )
1221566266
sage: hash(-y + x >= 0 )
1221566266
sage: hash(x - y > 0 )
1221566266

It seems to me that Sage treats >, >=, and == the same (see #7660). If this is true then it's a serious problem and needs to be addressed.

Apply:

  1. trac_11309-fix-comparison-of-comparisons.patch
  2. trac_11309-equate-flipped-comparisons.patch

Change History (38)

comment:1 Changed 9 years ago by tnv

  • Description modified (diff)

comment:2 Changed 9 years ago by kini

  • Cc kini added

comment:3 Changed 8 years ago by kini

  • Description modified (diff)

comment:4 Changed 8 years ago by kini

  • Authors set to Keshav Kini, Burcin Erocal
  • Status changed from new to needs_review

Ready for review! Thanks to Burcin for walking me through the Cython code.

comment:5 Changed 8 years ago by tnv

Thanks for creating the patch!!

I don't know how to apply this patch though - if you can walk me through it then I can test.

But in the mean time, what are the result for these commands ? If the results are different than the defected version above and as expected then probably the patch is correct.

sage: (-x +y < 0) in [x -y < 0]

Set([-x +y >= 0,x -y >= 0])

sage: var('x,y') (x, y) sage: hash(-x + y > 0 ) sage: hash(-x + y >= 0 ) sage: hash(x - y >= 0 ) sage: hash(-y + x >= 0 ) sage: hash(x - y > 0 )

comment:6 Changed 8 years ago by kini

I've changed the patch a little bit just now, by the way.

To apply the patch, go to devel/sage/ inside your sage directory, and type sage -hg qimport http://trac.sagemath.org/sage_trac/raw-attachment/ticket/11309/trac_11309-fix-comparison-of-comparisons.patch, type sage -hg qpush, type sage -b, and finally launch sage to test the patch!

Your examples are fixed, yes. You can see them listed inside the patch, where I added some more examples in the documentation of the function I changed.

comment:7 Changed 8 years ago by kini

Oh, by the way, I didn't fix the hashes. They're screwed up anyway, so this solution avoids using them to decide anything about whether expressions are the same or not. We might fix that in a later ticket...

comment:8 Changed 8 years ago by tnv

Thanks for the info.

Which Sage version do I apply the patch to ? the latest 4.7 ? I'll do that tomorrow at work

if they still give the same hashes then (-x +y < 0) in [x -y < 0] still gives True and Set([-x +y >= 0,x -y >= 0]) still eliminates one of them . Correct ?

comment:9 Changed 8 years ago by kini

No, incorrect, because I changed the code to not use the hashes at all when doing the comparison. The hashes are now irrelevant to this operation. However kcrisman found a bug in my patch so I will update it again in just a second...

comment:10 Changed 8 years ago by kini

  • Status changed from needs_review to needs_work

OK, this looks like it's going to take a little while, I'm getting some unexpected doctest errors... I'll fix it in the morning :)

comment:11 Changed 8 years ago by kini

  • Status changed from needs_work to needs_review

Never mind, ready for review again!

comment:12 Changed 8 years ago by kini

  • Cc kcrisman added
  • Owner changed from burcin to (none)

comment:13 Changed 8 years ago by kini

  • Owner changed from (none) to burcin

burcin got deleted from this ticket... that trac bug is annoying!

comment:14 Changed 8 years ago by kcrisman

Code is correct (corner cases discussed in person, so that e.g. (x < y) != x is True.

GEx e seems far from where it comes from.

comment:15 Changed 8 years ago by kini

fixed! (sorry, that was left over from when I was doing something that made cython not like that declaration where it was)

comment:16 Changed 8 years ago by kini

  • Keywords relational sd31 __richcmp__ added

comment:17 Changed 8 years ago by kcrisman

This looks good. Passing relevant tests.

comment:18 Changed 8 years ago by kcrisman

  • Status changed from needs_review to positive_review

comment:19 Changed 8 years ago by jdemeyer

  • Reviewers set to Karl-Dieter Crisman

comment:20 Changed 8 years ago by tnv

It now can tell that -x +y >0 is different than -y + x >= 0 but it says that -x+y >0 is not the same as y > x ---

or may be this is another problem ?

sage: ( -x+y >0 ) == (y > x )
False

sage: (-x + y < 0)  ==  (-x < -y)
False
sage: (x + y == 0)  ==  (x == -y)
False
sage: (x - y == 0)  ==  (x == y)
False
sage: (- x + y == 0)  ==  (0 == -x + y)
False
sage: (x < y)  ==  (y > x)
False
sage: (x == y) == (-x == -y)
False
sage: (x + y < 1 )  ==  (x + y -1 < 0)
False

comment:21 Changed 8 years ago by tnv

  • Status changed from positive_review to needs_work

This patch *breaks* the following

{{ Sage 4.7 (prepatched)

sage: (- x + y == 0) == (0 == -x + y) True sage: (-x + y == 0) == (0 == -x + y) True sage: (x < y) == (y > x) True

Sage 4.7 (postpatched)

sage: (- x + y == 0) == (0 == -x + y) False sage: (-x + y == 0) == (0 == -x + y) False sage: (x < y) == (y > x) False

}}}

comment:22 Changed 8 years ago by kcrisman

Sage 4.7 (prepatched)

sage: (- x + y == 0) == (0 == -x + y) True sage: (-x + y == 0) == (0 == -x + y) True sage: (x < y) == (y > x) True

Sage 4.7 (postpatched)

sage: (- x + y == 0) == (0 == -x + y) False sage: (-x + y == 0) == (0 == -x + y) False sage: (x < y) == (y > x) False

comment:23 Changed 8 years ago by kcrisman

{{ Sage 4.7 (prepatched)

sage: (- x + y == 0) == (0 == -x + y) True sage: (-x + y == 0) == (0 == -x + y) True sage: (x < y) == (y > x) True

Sage 4.7 (postpatched)

sage: (- x + y == 0) == (0 == -x + y) False sage: (-x + y == 0) == (0 == -x + y) False sage: (x < y) == (y > x) False

}}}

comment:24 Changed 8 years ago by kcrisman

Finally used preview...

Sage 4.7 (prepatched)

sage: (- x + y == 0) == (0 == -x + y) 
True 
sage: (-x + y == 0) == (0 == -x + y) 
True 
sage: (x < y) == (y > x) 
True

Sage 4.7 (postpatched)

sage: (- x + y == 0) == (0 == -x + y) 
False 
sage: (-x + y == 0) == (0 == -x + y) 
False 
sage: (x < y) == (y > x) 
False

comment:25 Changed 8 years ago by kcrisman

-x+y >0 is not the same as y > x

Correct. We use the philosophy (used elsewhere) that a comparison is True if you can prove it is True, and that otherwise it is False. False means that we can't prove it's True, and in general these kinds of simplifications are super hard. So all your examples need to be False, sadly.

As for the thing that breaks... I agree that is a problem. Great catch! Can you put your (real) name as a reviewer? (You should also feel free to add yourself to the main Trac page as a developer/contributor.

comment:26 follow-up: Changed 8 years ago by tnv

  • Cc tnv added
  • Reviewers changed from Karl-Dieter Crisman to Karl-Dieter Crisman, ThanhVu Nguyen

just put my name as reviewer -- thanks.

From your msg, would it be reasonable to add a SMT theorem prover package to Sage ? So that it can show equivalence of expressions (at least under some specific theories).

comment:27 Changed 8 years ago by kcrisman

There are some tickets open for things like this, I think, or something related, but I don't really know. Keshav or Burcin may know more.

comment:28 Changed 8 years ago by kini

Hm. In order to eventually solve #2778 and other such things, I think we need to allow nested relations after all. I talked to Burcin on IRC and he agrees. So we would plan to have all of these return an output which is the same as the input. If you wanted to force it to resolve, you could run bool() on them, and you would always get false, except when comparing x < y and y > x, x <= y and y >= x, x == y and y == x, and x != y and y != x, for symbolic expressions x and y (on kcrisman's insistence :) ). I'll need to implement this and figure out how it influences existing doctests (probably severely), so I'm leaving this as "needs_work" for now...

comment:29 Changed 8 years ago by kini

Sorry, I meant #2744, not #2778.

comment:30 in reply to: ↑ 26 ; follow-up: Changed 8 years ago by burcin

Replying to tnv:

From your msg, would it be reasonable to add a SMT theorem prover package to Sage ? So that it can show equivalence of expressions (at least under some specific theories).

Sage is really large as it is. While I'd be really interested to have this capability in Sage, I don't know how many others would want it in the standard distribution. The first step is to start with an optional package/prototype. We can see where it goes from there. :)

Which prover are you thinking of? What would this let us do in Sage? Perhaps you should write a message to sage-devel about this.

comment:31 in reply to: ↑ 30 ; follow-up: Changed 8 years ago by tnv

Which prover are you thinking of? What would this let us do in Sage? Perhaps you should write a message to sage-devel about this.

I am thinking about the optional package too. Someone told me qepcad (not exactly SMT but can be used for many similar purpose) already in Sage as an optional package.

The good thing about these SMT solvers is that most of them support a standard language (smtlib) and therefore you can use any of the SMT's out there with a single interface. SMT can be used to show if something (a set of expressions or constraints) is valid or satisfiable under different types of theories (not just boolean), or simplify a set of expression, etc. I rely on these for implications on my project-- to see if 2 sets of expressions are equi-satisfiable .

So all the above examples of whether if exp1 == exp2 should be easily answered with SMT.

comment:32 in reply to: ↑ 31 Changed 8 years ago by burcin

Replying to tnv:

So all the above examples of whether if exp1 == exp2 should be easily answered with SMT.

I'd really like to see Sage have it's own framework to handle assumptions (see assume? -- this relies completely on maxima right now), so I'm really interested in this. I'd be glad to help with the first steps of making a package, writing an interface, etc. We should have this conversation in sage-devel instead of this ticket though. ;)

comment:33 Changed 8 years ago by kcrisman

This still applies, and fixes another 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]

Before, the second assumption didn't obtain, because currently

sage: c = (x-2<=0)
sage: L = [c]
sage: L
[x - 2 <= 0]
sage: a = (x-1<=0)
sage: a in L
True

which is not good. See this sage-support thread.

comment:34 Changed 8 years ago by kcrisman

Since #2744 is on sage-wishlist, would it suffice to do some sort of "switch lhs and rhs" check as a last branch in the code to fix tnv's point in comment:21 (formatted in comment:24)? It would be nice to finally resolve this at the upcoming Bug Days.

comment:35 Changed 8 years ago by ppurka

In the patch, why is this evaluated to True?

+            sage: (x < y) != (y > x)
+            True

EDIT: Oops. I should have read the earlier comments. Sorry.

Last edited 8 years ago by ppurka (previous) (diff)

comment:36 Changed 8 years ago by kini

kcrisman: OK, I'll try to implement those minimal checks for now, and we can do nesting expressions later.

comment:37 Changed 8 years ago by kini

  • Description modified (diff)
  • Status changed from needs_work to needs_review

Added a new patch. Burcin, can you look over it to make sure I'm doing this the right way? In particular are those operator comparisons optimizable somehow?

Note: See TracTickets for help on using tickets.