[RFC] Piecewise conditions

[Chris Smith]

In PR #13204 I am proposing the following change to how Piecewise conditions behave:

```

    Booleans can contain Piecewise elements:

    >>> cond = (x < y).subs(x, Piecewise((2, x < 0), (3, True))); cond
    Piecewise((2, x < 0), (3, True)) < y

    The folded version of this results in a Piecewise whose
    expressions are Booleans:

    >>> folded_cond = piecewise_fold(cond); folded_cond
    Piecewise((2 < y, x < 0), (3 < y, True))

    When a Boolean containing Piecewise (like cond) or a Piecewise
    with Boolean expressions (like folded_cond) is used as a condition,
    it is converted to an equivalent ITE object:

    >>> Piecewise((1, folded_cond))
    Piecewise((1, ITE(x < 0, y > 2, y > 3)))

    When a condition is an ITE, it will be converted to a simplified
    Boolean expression:

    >>> piecewise_fold(_)
    Piecewise((1, ((x >= 0) | (y > 2)) & ((y > 3) | (x < 0))))

```

Technically, there is no need to convert the Piecewise-conditional to ITE.   It is good, however, to write the condition as an arbitrary BooleanFunction after folding so this step doesn't have to be done in any routine that uses folding to get an expression into shape for integration or solving, etc...

Does anyone have an objection to writing the condition of a Piecewise as a Boolean (ITE)?

/c

[Aaron Meurer]

The condition in a Piecewise is supposed to be a boolean, so I think
it's better to have it be a Boolean object if possible.

Whether or not an ITE is more readable than Ands and Ors probably
depends on the expression. I think the (simplified) dnf of a ITE is a
little easier to understand than the cnf ((x ≥ 0 ∧ y > 3) ∨ (y > 2 ∧ x
< 0)). Maybe something even simpler is possible using the fact that y
> 3 implies y > 2. We don't really have any functions in the logic
module to simplify expressions given a model, as far as I know.

Aaron Meurer

> --
> You received this message because you are subscribed to the Google Groups
> "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to sympy+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at https://groups.google.com/group/sympy.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sympy/8f8b2334-6075-4879-824c-b022e4cae90b%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Chris Smith]

There is the `simplify_logic` function, and I am proposing improvements to that for univariate expressions in #13204, too.

[Aaron Meurer]

Yes, I know about simplify_logic(), and it should be made smarter. But
the problem is that it only simplifies things as pure predicates.
ITE(x < 0, y > 2, y > 3) would be simplified as ITE(p, q, r). There
is an additional predicate that is always true, namely, Implies(y > 3,
y > 2), which could potentially result in a further simplification,
which might not be valid for the general ITE(p, q, r).

In logic, a set of expressions that are assumed to be true for a given
calculation are called a "model". Simplifying conditionals based on
models would require use of the assumptions system. The assumptions
system, particularly the new assumptions and satask, basically boils
down to building up a "model" of mathematically true facts which are
then used to possibly reduce a given predicate to "true" or "false".
ask(Q.real(x), Q.positive(x)) gives True because
Implies(Q.positive(x), Q.real(x)) is a predicate in the model. However
even if something doesn't reduce to "true" or "false", you could
potentially rewrite it, hopefully in a way that simplifies it. For
example And(x > 2, x > 3) can be rewritten as just x > 3 because
Implies(x > 3, x > 2) is true in a given model. It's been awhile since
I've studied this logic stuff so I can't say what the best
algorithm(s) are for doing this. For inequalities, we don't even have
support for them in ask() yet (they aren't part of the model), so that
would be the place to start.

This is a difficult problem, but one which I think would really help
many parts of SymPy (especially simplifying Piecewise conditionals).

Aaron Meurer

> https://groups.google.com/d/msgid/sympy/9c15cf3a-33dc-41bb-b3d9-24f4d0caf025%40googlegroups.com.