Opened 6 years ago

Last modified 6 years ago

#22022 new enhancement

floor of real x should be known to be at most x

Reported by: Peleg Michaeli Owned by:
Priority: major Milestone: sage-wishlist
Component: symbolics Keywords: floor, ceil
Cc: Merged in:
Authors: Reviewers:
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Status badges


Check this:

sage: assume(x, 'real')
sage: bool(floor(x) <= x)

This is how it works in Sympy:

In [2]: x = Symbol('x', real=True)

In [3]: floor(x) <= x
Out[3]: True

In [4]: floor(x) >= x
Out[4]: floor(x) >= x

In [5]: floor(x) > x
Out[5]: False

Change History (4)

comment:1 Changed 6 years ago by Peleg Michaeli

Keywords: ceil added

Clearly, a similar idea should probably work for ceil.

comment:2 Changed 6 years ago by Ralf Stephan

Milestone: sage-7.5sage-wishlist

comment:3 in reply to:  2 Changed 6 years ago by Ashutosh Ahelleya

I am interested in solving this. How do I solve this?(Implementation). Do I need to change the function body in expression.pyx here?

comment:4 Changed 6 years ago by Ralf Stephan

You need to know about how symbolic expressions are implemented in Sage. The Python interface uses the Pynac library for fast manipulation. Pynac is C++ and that's also why the expression member functions are often in Cython. Now bool(expression) calls the __nonzero__() member function where both Pynac and Maxima are used to determine the truth value---more or less successfully. While Maxima could be enhanced to do bool(floor(x)<x) it is an external library with a separate bug tracker, so you would need to report there and hope for the best, or enhance Maxima's Lisp code yourself. Pynac is in C++ and the maintainer reads this bug tracker. Pynac's github page is

Now recognizing that floor(x)<x is true could be easy but what about 4*floor<4*x? Or even 4*y*floor(x)<4*y with assume(y>0)? As you don't want simple text recogition you need a system that can solve whole classes of such expressions, see #19000. The interface to it would be in ticket #19162. It seems possible with much less work to get some of the functionality in Pynac, see the tickets and

Because this all is quite far away I have marked this ticket as "on the wishlist".

Note: See TracTickets for help on using tickets.