Skip to content

Four or-with-equality rules give the opposite comparison for symbolic operands #1077

Description

@Rafael-SOWNet

What happens

"(y < x) or (x = y)".ToEntity().Simplify()   // x <= y

y < x or x = y is x >= y. The answer is the negation of it away from the diagonal:

x y (y < x) or (x = y) Simplify()'s x <= y
1 2 False True
2 2 True True
3 2 True False

Four rules in Patterns.InequalityEqualityRules are affected — the ones whose comparison
is written with its operands in the opposite order to the equality beside it:

Orf(Lessf(var any2, var any1),    Equalsf(var any1a, var any2a)) ... => any1 <= any2,   // should be >=
Orf(Greaterf(var any2, var any1), Equalsf(var any1a, var any2a)) ... => any1 >= any2,   // should be <=
Orf(Equalsf(var any1a, var any2a), Lessf(var any2, var any1))    ... => any1 <= any2,   // should be >=
Orf(Equalsf(var any1a, var any2a), Greaterf(var any2, var any1)) ... => any1 >= any2,   // should be <=

Their four neighbours, where the comparison and the equality are written the same way
round, are correct and stay as they are.

Why it has not been seen

With a numeric operand it never fires. Lessf(var @const, var anyButConst) when @const is Number rewrites 2 < x to x > 2 further down the same pass, so by the time the
disjunction is looked at both halves are written the same way round and one of the four
correct rules matches:

"(2 < x) or (x = 2)".ToEntity().Simplify()   // x >= 2, correct

Two symbols are what reach it, and every affected shape needs both operands symbolic.

How it was found

Transcribing the set into MatchedRules for
#746 tier 1 — the same way the
branch-cut gap in the reciprocal-logarithm rules turned up (#1062). Writing a rule out as
data makes the correspondence between its pattern and its replacement something you have
to state, and four of these do not survive stating it.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions