ASKSAGE: Sage Q&A Forum - Individual question feedhttp://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Fri, 18 Aug 2017 16:51:17 -0500Why does assume() mess with equality checks?http://ask.sagemath.org/question/38562/why-does-assume-mess-with-equality-checks/I ran into this interesting behaviour just now:
sage: bool(10 == log(282475249)/log(7))
True
sage: assume(282475249 == 7^x)
sage: bool(10 == log(282475249)/log(7))
False
Is this a bug? `assume(7^x == 282475249)` doesn't trigger the weird behaviour, but I'd expect those two assumptions to be equivalent.
I'm running `SageMath version 8.0, Release Date: 2017-07-21`Thu, 17 Aug 2017 16:05:29 -0500http://ask.sagemath.org/question/38562/why-does-assume-mess-with-equality-checks/Comment by dan_fulea for <p>I ran into this interesting behaviour just now:</p>
<pre><code>sage: bool(10 == log(282475249)/log(7))
True
sage: assume(282475249 == 7^x)
sage: bool(10 == log(282475249)/log(7))
False
</code></pre>
<p>Is this a bug? <code>assume(7^x == 282475249)</code> doesn't trigger the weird behaviour, but I'd expect those two assumptions to be equivalent.</p>
<p>I'm running <code>SageMath version 8.0, Release Date: 2017-07-21</code></p>
http://ask.sagemath.org/question/38562/why-does-assume-mess-with-equality-checks/?comment=38572#post-id-38572Well, try `assume` the other way around:
sage: assume( 7^x == 282475249 )
sage: bool(10 == log(282475249)/log(7))
True
to add a new question inside the question. I love such questions on a system written to highly serve higher mathematics. (And there is skew proportion of them w.r.t. questions involving e.g. elliptic curves...) Probably that the `assume` tries to replace the LHS every time it can do it, then the `bool` has to check for `10 == log(7^x)/log(7)`, and even if gets the simplified version `bool( 10 == x )` it may stop here, delivering a false. This `False` means `sage` **can not prove** (without (further) help) that the assertion is true. It delivers a `True` iff it can.
Note: `assume` does not get all the best of the assumption in *most cases*. How could it?Fri, 18 Aug 2017 16:51:17 -0500http://ask.sagemath.org/question/38562/why-does-assume-mess-with-equality-checks/?comment=38572#post-id-38572