rewrite Expression.__nonzero__()

[rwst]

Symbolic expressions may be part of type-neutral computations, e.g. matrices, polynomials. Developers do not expect proof machinery to crank up when writing if x!=0, but this is just what happens. So bool(x1!=x2) should be changed to mean not (x1-x2).is_trivial_zero() for symbolic x. The ticket should provide a different interface for cases requiring simplification/proof:

• bool(rel) equivalent to (not)(LHS-RHS).is_trivial_zero() for ==,!= ; and for <, >, <=, >= the result follows alpha order of lhs and rhs
• satisfiable(rel) attempting simplification/proof, returning (Yes,example)/False/Undefined
• solve(rel) in case of satisfiable=Yes returning the full solution set
• holds(rel), quick alias of satisfiable (later without giving an example)
• ex.is_zero(simplify=False) (default) calling the fast bool(ex==0)
• ex.is_zero(simplify=True) attempting simplification/proof by calling ex==0.holds()
• prove(rel) showing more or less steps of simplification (which is out of reach for the moment)

This ticket will implement the new behaviour of bool(rel) and put all other functionality of ex.__nonzero__() into holds() and ex.is_zero(simplify=True).

See also #19162.

CC: @nexttime @behackl @kcrisman @eviatarbach

Component: symbolics

Issue created by migration from https://trac.sagemath.org/ticket/19040

[videlec]

comment:1

Be careful that in a lot of Sage place there are

def my_generic_function(x):
    if not x:
        ...
    else:
        ...

or with not x replaced by x.is_zero().

So this change would also implies to change all of these in a uniform way.

[rwst]

comment:2

Replying to @videlec:

if not x:

bool(not x) calls PyObject_IsTrue which calls Expression.__nonzero__ which atm tries to prove that x is nonzero

or with not x replaced by x.is_zero().

This calls PyObject_IsTrue as well.

So this change would also implies to change all of these in a uniform way.

Right, Expression.__nonzero__ will then call x.is_trivial_zero() and everyone who wants a proof needs a dfferent method.

[rwst]

comment:3

It's not too bad. Catching != and == in __nonzero__ and comparing trivially yields only a few dozen doctest fails in symbolic and calculus, mainly from bool(...). No fail in src/doc.

[videlec]

comment:4

I agree that the change would be actually good (for the reason why you created this ticket).

Thoug, for symbolic expression we want to create equations and check their validity

sage: cos(x)**2 + sin(x)**2 == 1
cos(x) == sin(x)
sage: bool(_)
True

The above will not be enough anymore. What would be the new way of checking? This needs to be emphasized a lot in the documentation as it is backward incompatible. And I guess it is worth a thread on sage-devel. Not necessarily right now, it is always good to have concrete propositions.

You should also have a look to sage/tests/* where I am sure some of the things are broken.

[rwst]

comment:5

Replying to @videlec:

Thoug, for symbolic expression we want to create equations and check their validity

sage: cos(x)**2 + sin(x)**2 == 1
cos(x) == sin(x)
sage: bool(_)
True

The above will not be enough anymore. What would be the new way of checking?

sage: satisfiable(_)
True

This is a long-standing omission, and it would resolve conceptual problems of #17700. It would use #19000 and, if that finds no solution, Maxima as before. SMT solvers can also give a satisfying x in case of satisfiability, but no full solution which is the task of solve.

This needs to be emphasized a lot in the documentation as it is backward incompatible. And I guess it is worth a thread on sage-devel. Not necessarily right now, it is always good to have concrete propositions.

You should also have a look to sage/tests/* where I am sure some of the things are broken.

Three fails.

[rwst]

comment:6

Replying to @rwst:

It would use #19000

Could. #19000 is not a necessity.

[rwst]

comment:7

Actually, proving equality would need quantifiers like:

sage: satisfiable(_, for_all(x))
True

[rwst]

Description changed:

--- 
+++ 
@@ -1 +1,6 @@
-Symbolics may be part of type-neutral computations, e.g. matrices, rings. Developers do not expect proof machinery to crank up when writing `if x!=0`, so `bool(x1!=x2)` should mean `not (x1-x2).is_trivial_zero()` for symbolic `x`. Instead of `Expression.__nonzero__` this ticket should provide a different interface for cases requiring simplification/proof.
+Symbolics may be part of type-neutral computations, e.g. matrices, rings. Developers do not expect proof machinery to crank up when writing `if x!=0`, so `bool(x1!=x2)` should mean `not (x1-x2).is_trivial_zero()` for symbolic `x`. This ticket should provide a different interface for cases requiring simplification/proof:
+* `bool(rel)` equivalent to `(not)(LHS-RHS).is_trivial_zero()` for ==,!= ; and an exception with maybe hint to the following for <,>,<=,>=
+* `satisfiable(rel)` returning `(Yes,example)/No/Undecidable/NotImplemented`
+* `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
+* `prove(rel)` showing more or less steps of simplification (which is out of reach for the moment)
+

[rwst]

Description changed:

--- 
+++ 
@@ -1,6 +1,7 @@
 Symbolics may be part of type-neutral computations, e.g. matrices, rings. Developers do not expect proof machinery to crank up when writing `if x!=0`, so `bool(x1!=x2)` should mean `not (x1-x2).is_trivial_zero()` for symbolic `x`. This ticket should provide a different interface for cases requiring simplification/proof:
 * `bool(rel)` equivalent to `(not)(LHS-RHS).is_trivial_zero()` for ==,!= ; and an exception with maybe hint to the following for <,>,<=,>=
 * `satisfiable(rel)` returning `(Yes,example)/No/Undecidable/NotImplemented`
+* `truth(rel, (x,S1), (y,S1)...)` equivalent to `satisfiable(rel)` for all `x,y...` in `S1,S2,...`
 * `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
 * `prove(rel)` showing more or less steps of simplification (which is out of reach for the moment)
 

[rwst]

Description changed:

--- 
+++ 
@@ -1,7 +1,8 @@
-Symbolics may be part of type-neutral computations, e.g. matrices, rings. Developers do not expect proof machinery to crank up when writing `if x!=0`, so `bool(x1!=x2)` should mean `not (x1-x2).is_trivial_zero()` for symbolic `x`. This ticket should provide a different interface for cases requiring simplification/proof:
+Symbolics may be part of type-neutral computations, e.g. matrices, rings. Developers do not expect proof machinery to crank up when writing `if x!=0`, so `bool(x1!=x2)` should mean `not (x1-x2).is_trivial_zero()` for symbolic `x`. We should provide a different interface for cases requiring simplification/proof:
 * `bool(rel)` equivalent to `(not)(LHS-RHS).is_trivial_zero()` for ==,!= ; and an exception with maybe hint to the following for <,>,<=,>=
 * `satisfiable(rel)` returning `(Yes,example)/No/Undecidable/NotImplemented`
 * `truth(rel, (x,S1), (y,S1)...)` equivalent to `satisfiable(rel)` for all `x,y...` in `S1,S2,...`
 * `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
 * `prove(rel)` showing more or less steps of simplification (which is out of reach for the moment)
 
+This ticket will implement the new behaviour of `bool(rel)` and put all other functionality of `ex.__nonzero__()` into `ex.satisfiable(rel)`.

[rwst]

Description changed:

--- 
+++ 
@@ -5,4 +5,6 @@
 * `solve(rel)` in case of `satisfiable=Yes` returning the full solution set
 * `prove(rel)` showing more or less steps of simplification (which is out of reach for the moment)
 
-This ticket will implement the new behaviour of `bool(rel)` and put all other functionality of `ex.__nonzero__()` into `ex.satisfiable(rel)`.
+This ticket will implement the new behaviour of `bool(rel)` and put all other functionality of `ex.__nonzero__()` into `ex.satisfiable()`.
+
+See also #19162.