Opened 3 years ago

Last modified 2 years ago

#22022 new enhancement

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

Reported by: pelegm 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:

Description

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

Change History (4)

comment:1 Changed 3 years ago by pelegm

  • Keywords ceil added

Clearly, a similar idea should probably work for ceil.

comment:2 follow-up: Changed 3 years ago by rws

  • Milestone changed from sage-7.5 to sage-wishlist

comment:3 in reply to: ↑ 2 Changed 2 years ago by aashu12

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 2 years ago by rws

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 https://github.com/pynac/pynac/issues/227 and https://github.com/pynac/pynac/issues/234.

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

Note: See TracTickets for help on using tickets.