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

[pelegm]

Check this:

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

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

Component: symbolics

Keywords: floor, ceil

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

[pelegm]

comment:1

Clearly, a similar idea should probably work for ceil.

[pelegm]

Changed keywords from floor to floor, ceil

[sagetrac-aashu12]

comment:3

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

[rwst]

comment:4

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 https://github.com/pynac/pynac.

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 pynac/pynac#227 and pynac/pynac#234.

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