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()); + } + } +}