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: |
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 6 years ago by
Keywords: | ceil added |
---|
comment:2 follow-up: 3 Changed 6 years ago by
Milestone: | sage-7.5 → sage-wishlist |
---|
comment:3 Changed 6 years ago by
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
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".
Clearly, a similar idea should probably work for
ceil
.