Ask Your Question

Revision history [back]

Assumptions giving wrong boolean answer for simple expression

Let $a, b \in \mathbb{Z}$ with $a < 0$, then we can plainly see that $a b^2 = 0 \implies b = 0$ since $\mathbb{Z}$ is an integral domain.

sage: var("a b")
(a, b)
sage: assumptions()
[]
sage: assume(a, "integer")
sage: assume(b, "integer")
sage: assume(b^2 == 0)
sage: bool(b == 0)
True

But as soon as I introduce another non-zero variable in the expression, it cannot detect b is 0.

sage: var("a b")
(a, b)
sage: assumptions()
[]
sage: assume(a, "integer")
sage: assume(b, "integer")
sage: assume(a < 0)
sage: a != 0
a != 0
sage: bool(a != 0)
True
sage: assume(a*b^2 == 0)
sage: bool(b == 0)
False