Sage: Ticket #22022: floor of real x should be known to be at most x
https://trac.sagemath.org/ticket/22022
<p>
Check this:
</p>
<div class="wiki-code"><div class="code"><pre>sage<span class="p">:</span> assume<span class="p">(</span>x<span class="p">,</span> <span class="s">'real'</span><span class="p">)</span>
sage<span class="p">:</span> <span class="nb">bool</span><span class="p">(</span>floor<span class="p">(</span>x<span class="p">)</span> <span class="o"><=</span> x<span class="p">)</span>
<span class="bp">False</span>
</pre></div></div><p>
This is how it works in Sympy:
</p>
<div class="wiki-code"><div class="code"><pre>In <span class="p">[</span><span class="mi">2</span><span class="p">]:</span> x <span class="o">=</span> Symbol<span class="p">(</span><span class="s">'x'</span><span class="p">,</span> real<span class="o">=</span><span class="bp">True</span><span class="p">)</span>
In <span class="p">[</span><span class="mi">3</span><span class="p">]:</span> floor<span class="p">(</span>x<span class="p">)</span> <span class="o"><=</span> x
Out<span class="p">[</span><span class="mi">3</span><span class="p">]:</span> <span class="bp">True</span>
In <span class="p">[</span><span class="mi">4</span><span class="p">]:</span> floor<span class="p">(</span>x<span class="p">)</span> <span class="o">>=</span> x
Out<span class="p">[</span><span class="mi">4</span><span class="p">]:</span> floor<span class="p">(</span>x<span class="p">)</span> <span class="o">>=</span> x
In <span class="p">[</span><span class="mi">5</span><span class="p">]:</span> floor<span class="p">(</span>x<span class="p">)</span> <span class="o">></span> x
Out<span class="p">[</span><span class="mi">5</span><span class="p">]:</span> <span class="bp">False</span>
</pre></div></div>en-usSagehttps://trac.sagemath.org/chrome/site/logo_sagemath_trac.png
https://trac.sagemath.org/ticket/22022
Trac 1.1.6pelegmSun, 04 Dec 2016 20:26:04 GMTkeywords changed
https://trac.sagemath.org/ticket/22022#comment:1
https://trac.sagemath.org/ticket/22022#comment:1
<ul>
<li><strong>keywords</strong>
<em>ceil</em> added
</li>
</ul>
<p>
Clearly, a similar idea should probably work for <code>ceil</code>.
</p>
TicketrwsMon, 05 Dec 2016 14:37:04 GMTmilestone changed
https://trac.sagemath.org/ticket/22022#comment:2
https://trac.sagemath.org/ticket/22022#comment:2
<ul>
<li><strong>milestone</strong>
changed from <em>sage-7.5</em> to <em>sage-wishlist</em>
</li>
</ul>
Ticketaashu12Thu, 09 Mar 2017 20:18:32 GMT
https://trac.sagemath.org/ticket/22022#comment:3
https://trac.sagemath.org/ticket/22022#comment:3
<p>
I am interested in solving this. How do I solve this?(Implementation). Do I need to change the function body in expression.pyx here?
</p>
TicketrwsFri, 10 Mar 2017 07:08:09 GMT
https://trac.sagemath.org/ticket/22022#comment:4
https://trac.sagemath.org/ticket/22022#comment:4
<p>
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 <code>bool(expression)</code> calls the <code>__nonzero__()</code> 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 <code>bool(floor(x)<x)</code> 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 <a class="ext-link" href="https://github.com/pynac/pynac"><span class="icon"></span>https://github.com/pynac/pynac</a>.
</p>
<p>
Now recognizing that <code>floor(x)<x</code> is true could be easy but what about <code>4*floor<4*x</code>? Or even <code>4*y*floor(x)<4*y</code> with <code>assume(y>0)</code>? As you don't want simple text recogition you need a system that can solve whole classes of such expressions, see <a class="new ticket" href="https://trac.sagemath.org/ticket/19000" title="enhancement: SMT-solve metaticket (new)">#19000</a>. The interface to it would be in ticket <a class="new ticket" href="https://trac.sagemath.org/ticket/19162" title="enhancement: symbolic relations metaticket (new)">#19162</a>. It seems possible with much less work to get some of the functionality in Pynac, see the tickets <a class="ext-link" href="https://github.com/pynac/pynac/issues/227"><span class="icon"></span>https://github.com/pynac/pynac/issues/227</a> and <a class="ext-link" href="https://github.com/pynac/pynac/issues/234"><span class="icon"></span>https://github.com/pynac/pynac/issues/234</a>.
</p>
<p>
Because this all is quite far away I have marked this ticket as "on the wishlist".
</p>
Ticket