From 6909a8ac6749fe2b24733df2cea0f283650bbb5b Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Wed, 26 Aug 2026 17:23:46 +0000 Subject: [PATCH] Four `or`-with-equality rules gave the opposite comparison (#1077) `a < b or a = b` is `a <= b`. Written with the comparison the other way round it answers the other way round -- `b < a or a = b` is `a >= b` -- and four of the eight arms of `InequalityEqualityRules` that say this carried their neighbour's answer. Off the diagonal the result was the negation of the input: `(y < x) or (x = y)` simplified to `x <= y`, which at x = 3, y = 2 is False where the input is True. They are only reachable with both operands symbolic, which is why four wrong arms sat there. With a number on one side, the `Lessf(var @const, ...)` arm further down the same set rewrites `2 < x` to `x > 2` earlier in the pass, so the disjunction is only ever looked at with both halves written the same way round and one of the four correct arms matches. Every affected shape needs two symbols. The test evaluates both sides at sample points rather than reading the rewritten comparison, because a wrong rewrite here is a well-formed comparison -- a test that records the answer records whichever answer it was given. It fails 16 of its 48 cases without the fix. Its remark says why the points straddle the diagonal and why both operands are symbols, so neither can be simplified away later without noticing. Found by transcribing the set into `MatchedRules` for #746 tier 1. Writing a rule out as data makes the correspondence between its pattern and its replacement something you have to state, and four of these did not survive stating it -- the same way the branch-cut gap in the reciprocal-logarithm rules turned up (#1062). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd --- BREAKING-CHANGES.md | 31 ++++++++ .../Patterns/Patterns.EqualityInequality.cs | 18 ++++- .../PatternsTest/OrWithEqualityTest.cs | 73 +++++++++++++++++++ 3 files changed, 118 insertions(+), 4 deletions(-) create mode 100644 Sources/Tests/UnitTests/PatternsTest/OrWithEqualityTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 166227a0f..bd05cf724 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -21,6 +21,7 @@ read first. | Silent? | What | Was | Is | |---|---|---|---| +| **Silent** | `"(y < x) or (x = y)".ToEntity().Simplify()`, and three more disjunctions of a comparison with an equality written the other way round | `x <= y` — False at `x = 3, y = 2` where the input is True | `x >= y` | | **Silent** | `"x6 + x y + 1 = 0".ToEntity().Solve("x")`, and every equation no solver settles | `{ }` — there are no roots | `{ x : 1 + x ^ 6 + x * y = 0 }` — these are the roots, whichever they are | | **Silent** | `"(x - 1) * (x6 + x y + 1) = 0".ToEntity().Solve("x")` | `{ 1 }` | `{ 1 } \/ { x : 1 + x ^ 6 + x * y = 0 }` | | **Silent** | `"x6 + x y + 1 = 0 and x - 1 = 0".ToEntity().Solve("x")` | `{ }` | `{ x : x ^ 6 + x * y + 1 = 0 and x - 1 = 0 }` | @@ -309,6 +310,36 @@ bracketing for. The change only ever adds `\left(`/`\right)` groups, which CShar parses, so nothing downstream needs a matching change ([#822](https://github.com/asc-community/AngouriMath/issues/822)). +### Four `or`-with-equality rules gave the opposite comparison + +`a < b or a = b` is `a <= b`. Written with the comparison the other way round it answers the other +way round: `b < a or a = b` is `a >= b`. Four of the eight arms of `InequalityEqualityRules` that +say this carried their neighbour's answer, so the result was the negation of the input everywhere +off the diagonal. + +| | before | now | +|---|---|---| +| `RewriteRules.InequalityEquality.ApplyOnce("(y < x) or (x = y)")` | `x <= y` | `x >= y` | +| `RewriteRules.InequalityEquality.ApplyOnce("(y > x) or (x = y)")` | `x >= y` | `x <= y` | +| `RewriteRules.InequalityEquality.ApplyOnce("(x = y) or (y < x)")` | `x <= y` | `x >= y` | +| `RewriteRules.InequalityEquality.ApplyOnce("(x = y) or (y > x)")` | `x >= y` | `x <= y` | +| `RewriteRules.InequalityEquality.ApplyOnce("(x < y) or (x = y)")` | `x <= y` | `x <= y` — this half was right | +| `RewriteRules.InequalityEquality.ApplyOnce("(x > y) or (x = y)")` | `x >= y` | `x >= y` — and so was this | + +`Simplify` moves with it: `"(y < x) or (x = y)".ToEntity().Simplify()` was `x <= y` and is `x >= y`. +At `x = 3, y = 2` the input is True and the old answer is False. + +**Only reachable with both operands symbolic**, which is why it survived. With a number on one side, +the `Lessf(var @const, ...)` arm further down the same set rewrites `2 < x` to `x > 2` earlier in the +pass, so the disjunction is only ever looked at with both halves written the same way round and one +of the four *correct* arms matches — `"(2 < x) or (x = 2)".ToEntity().Simplify()` was and is `x >= 2`. + +Found by transcribing the set into `MatchedRules` for +[#746](https://github.com/asc-community/AngouriMath/issues/746) tier 1: writing a rule out as data +makes the correspondence between its pattern and its replacement something you have to state, and +four of these did not survive stating it +([#1077](https://github.com/asc-community/AngouriMath/issues/1077)). + ### A reciprocal inside a logarithm is no longer moved out unconditionally `ln(1/b) = -ln(b)` is false on the negative reals, because the principal argument does not negate diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs index 1f368e9d2..2e7dea3a1 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs @@ -99,14 +99,24 @@ private static Entity BothHold(Entity left, Entity right) [AddressableRules] internal static Entity InequalityEqualityRules(Entity x) => x switch { + // `a < b or a = b` is `a <= b`, and the four arms below it are the same law with the + // comparison written the other way round -- so they answer the other way round too. + // `b < a or a = b` is `a >= b`, not `a <= b`: at a = 1, b = 2 the disjunction is + // False and `a <= b` is True. Four of these eight carried their neighbour's answer. + // + // They are only reachable with both operands symbolic. With a number on one side, + // the `Lessf(var @const, ...)` arm further down rewrites `2 < x` to `x > 2` earlier + // in the same pass, so the disjunction is always looked at with both halves written + // the same way round and one of the four correct arms matches. + // https://github.com/asc-community/AngouriMath/issues/1077 Orf(Lessf(var any1, var any2), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 <= any2, - Orf(Lessf(var any2, var any1), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 <= any2, + Orf(Lessf(var any2, var any1), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 >= any2, Orf(Greaterf(var any1, var any2), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 >= any2, - Orf(Greaterf(var any2, var any1), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 >= any2, + Orf(Greaterf(var any2, var any1), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 <= any2, Orf(Equalsf(var any1a, var any2a), Lessf(var any1, var any2)) when any1 == any1a && any2 == any2a => any1 <= any2, - Orf(Equalsf(var any1a, var any2a), Lessf(var any2, var any1)) when any1 == any1a && any2 == any2a => any1 <= any2, + Orf(Equalsf(var any1a, var any2a), Lessf(var any2, var any1)) when any1 == any1a && any2 == any2a => any1 >= any2, Orf(Equalsf(var any1a, var any2a), Greaterf(var any1, var any2)) when any1 == any1a && any2 == any2a => any1 >= any2, - Orf(Equalsf(var any1a, var any2a), Greaterf(var any2, var any1)) when any1 == any1a && any2 == any2a => any1 >= any2, + Orf(Equalsf(var any1a, var any2a), Greaterf(var any2, var any1)) when any1 == any1a && any2 == any2a => any1 <= any2, Notf(Greaterf(var any1, var any2)) => any1 <= any2, Notf(Lessf(var any1, var any2)) => any1 >= any2, diff --git a/Sources/Tests/UnitTests/PatternsTest/OrWithEqualityTest.cs b/Sources/Tests/UnitTests/PatternsTest/OrWithEqualityTest.cs new file mode 100644 index 000000000..2187a3029 --- /dev/null +++ b/Sources/Tests/UnitTests/PatternsTest/OrWithEqualityTest.cs @@ -0,0 +1,73 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using System.Collections.Generic; +using AngouriMath; +using AngouriMath.Core.Transformations; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.PatternsTest +{ + /// + /// a < b or a = b is a <= b, and the same law written with the comparison + /// the other way round answers the other way round. Four of the eight arms that say this + /// carried their neighbour's answer. + /// #1077 + /// + /// + /// + /// Checked against the truth value at sample points rather than against an expected + /// string. A wrong rewrite here is a well-formed comparison, so a test that reads the answer + /// records whichever answer it was given; a test that evaluates both sides cannot. + /// + /// + /// Both operands are symbolic, which is the only way to reach these rules at all: with a + /// number on one side, 2 < x is rewritten to x > 2 earlier in the same + /// pass, so the disjunction is only ever seen with both halves written the same way round. + /// That is why four wrong arms survived — and why this test would have passed on them had it + /// used a numeric operand. + /// + /// + [Trait("Area", "Patterns")] + public sealed class OrWithEqualityTest + { + private static readonly string[] Shapes = + { + "(x < y) or (x = y)", "(y < x) or (x = y)", + "(x > y) or (x = y)", "(y > x) or (x = y)", + "(x = y) or (x < y)", "(x = y) or (y < x)", + "(x = y) or (x > y)", "(x = y) or (y > x)", + }; + + // Below, on and above the diagonal: a flipped comparison agrees on the diagonal, where + // both sides are True, and disagrees on either side of it. + private static readonly (string X, string Y)[] Points = + { + ("1", "2"), ("2", "2"), ("3", "2"), ("-1", "1"), ("0", "0"), ("5", "-5"), + }; + + public static IEnumerable Cases() + { + foreach (var shape in Shapes) + foreach (var (x, y) in Points) + yield return new object[] { shape, x, y }; + } + + [Theory] + [MemberData(nameof(Cases))] + public void TheDisjunctionKeepsItsTruthValue(string shape, string x, string y) + { + var original = shape.ToEntity(); + var rewritten = RewriteRules.InequalityEquality.ApplyOnce(original); + Assert.NotEqual(original, rewritten); + Assert.Equal( + original.Substitute("x", x.ToEntity()).Substitute("y", y.ToEntity()).EvalBoolean(), + rewritten.Substitute("x", x.ToEntity()).Substitute("y", y.ToEntity()).EvalBoolean()); + } + } +}