Hello,
I'm having some issues with a simple example of algebraic manipulation.
The two examples below mean the same thing mathematically, so it's strange that they get different results.
Example 1 correctly finds that the conclusion is true:
from sage.all import *
def main2():
n, b, x = var('n b x', domain='real')
premises = [
b != 1,
sqrt(log(n)/log(b)) == log(sqrt(n))/log(b),
b*log(n)/log(b) == log(b*n)/log(b),
#x == log(n)/log(b),
]
x = log(n)/log(b)
conclusion = sqrt(x) - x/2 == 0
with assuming(*premises):
result = conclusion.full_simplify()
bool_result = bool(result)
print(premises)
print(conclusion)
print(result)
print(bool_result)
Its output is:
[b != 1, sqrt(log(n)/log(b)) == log(sqrt(n))/log(b), b*log(n)/log(b) == log(b*n)/log(b)]
sqrt(log(n)/log(b)) - 1/2*log(n)/log(b) == 0
1/2*(2*sqrt(log(n)/log(b))*log(b) - log(n))/log(b) == 0
True
Example 2 (switching x = to x ==) fails:
from sage.all import *
def main2():
n, b, x = var('n b x', domain='real')
premises = [
b != 1,
sqrt(log(n)/log(b)) == log(sqrt(n))/log(b),
b*log(n)/log(b) == log(b*n)/log(b),
x == log(n)/log(b),
]
#x = log(n)/log(b)
conclusion = sqrt(x) - x/2 == 0
with assuming(*premises):
result = conclusion.full_simplify()
bool_result = bool(result)
print(premises)
print(conclusion)
print(result)
print(bool_result)
with this output:
[b != 1, sqrt(log(n)/log(b)) == log(sqrt(n))/log(b), b*log(n)/log(b) == log(b*n)/log(b), x == log(n)/log(b)]
-1/2*x + sqrt(x) == 0
-1/2*x + sqrt(x) == 0
False
Any ideas on what I'm doing wrong here?
Thanks,
Horst