Why does assume() mess with equality checks?

asked 2017-08-17 23:05:54 +0100

tavianator gravatar image

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

edit retag flag offensive close merge delete

Comments

Well, 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 sagecan 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?

dan_fulea gravatar imagedan_fulea ( 2017-08-18 23:51:17 +0100 )edit
add a comment