From 8c1e96fbbbd7bf565323ba07a0979d6842f422a7 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 13 Nov 2026 15:37:59 +0000 Subject: [PATCH 1/4] Gather a quotient of powers with a whole exponent factor only where it holds a^n / b^(c*n) -> (a / b^c)^n and its mirror had no guard. The gathering is a^n / b^n -> (a/b)^n with b^c for a base, so it holds on that rule's condition from #802: n whole, or both bases positive reals. Unguarded, x^n / y^(2n) became (x / y^2)^n, which is 1 at x = 1, y = -1, n = 1/2, where the quotient is -1. Both the data rule and its switch arm now ask the same guard. Found by the v3 definedness specification (work/v3-spec); no issue filed. Co-Authored-By: Claude Opus 5.5 --- BREAKING-CHANGES.md | 14 +++++ .../Transformations/Matching/MatchedRules.cs | 12 +++++ .../Simplification/Patterns/Patterns.Power.cs | 15 +++++- ...entOfPowersWithAWholeExponentFactorTest.cs | 54 +++++++++++++++++++ 4 files changed, 93 insertions(+), 2 deletions(-) create mode 100644 Sources/Tests/UnitTests/Common/QuotientOfPowersWithAWholeExponentFactorTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index a70ca6bd5..c7481e4b4 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -57,6 +57,20 @@ divisor answers at once. A two-sided limit is not changed. Found by limitcheck; | `"arcsin(-x * log(-1, x))".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `limitright(arcsin(-x * log(-1, x)), x, 0)` | `0` | | `"x * log(2 + x, x)".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `0` after 27 s | `0` in 0.25 s | +### A quotient of powers whose exponents differ by a whole factor is gathered only where that holds + +**Silent: `a^n / b^(c*n)` and `a^(c*n) / b^n` are no longer gathered into one power unless `n` is whole or both +bases are positive reals**, the condition `a^n / b^n -> (a/b)^n` has carried since +[#802](https://github.com/asc-community/AngouriMath/issues/802). The two rules gathering a whole factor `c` had no +guard. At `x = 1, y = -1, n = 1/2` the quotient `x^n / y^(2n)` is `1 / (-1)^1 = -1`, while the gathered +`(x / y^2)^n` is `1`. Found by the v3 definedness specification; no issue was filed. + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"x^n/y^(2*n)".ToEntity().Simplify()` | `(x / y ^ 2) ^ n` | `x ^ n / y ^ (2 * n)` | +| `"x^(2*n)/y^n".ToEntity().Simplify()` | `(x ^ 2 / y) ^ n` | `x ^ (2 * n) / y ^ n` | +| `"2^n/3^(2*n)".ToEntity().Simplify()` | `(2/9) ^ n` | `(2/9) ^ n`, unchanged | + ### A product with a power for a factor is read by the power's exponent's limit in a one-sided limit **Silent: a one-sided limit of a product whose factors tend to 0 and to an infinity, one of them a power `u^v` whose diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index f60717747..fae97d122 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -3086,6 +3086,13 @@ is var (divided, remainder) MatchPattern.Any("n")))), bound => new Powf(bound["a"] / new Powf(bound["b"], bound["c"]), bound["n"]), Soundness.SoundUnderAssumptions, + // The guard of the quotient rule above, for the same reason: b ^ (c * n) is + // (b ^ c) ^ n, and a ^ n / (b ^ c) ^ n is (a / b ^ c) ^ n, only for a whole n or + // positive real bases. At a = 1, b = -1, n = 1/2 the quotient is + // 1 / (-1) ^ 1 = -1 and the gathered power (1 / 1) ^ (1/2) = 1. + when: bound => bound["n"] is Integer + || (bound["a"].Evaled is Real { IsPositive: true } + && bound["b"].Evaled is Real { IsPositive: true }), description: "a ^ n / b ^ (c * n) = (a / b ^ c) ^ n, for a positive whole c", // The exponent is matched twice and written once, and one power node goes: the delta // is -(1 + |n|), at most -2 and further the larger the exponent is. @@ -3102,6 +3109,11 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("n"))), bound => new Powf(new Powf(bound["a"], bound["c"]) / bound["b"], bound["n"]), Soundness.SoundUnderAssumptions, + // Guarded as its mirror is: at a = -1, b = 1, n = 1/2 the quotient is -1 and the + // gathered power ((-1) ^ 2 / 1) ^ (1/2) is 1. + when: bound => bound["n"] is Integer + || (bound["a"].Evaled is Real { IsPositive: true } + && bound["b"].Evaled is Real { IsPositive: true }), description: "a ^ (c * n) / b ^ n = (a ^ c / b) ^ n, for a positive whole c", // The exponent is matched twice and written once, and one power node goes with it: // the delta is -(1 + |n|), the mirror of the rule that takes it into the divisor. diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs index 5f7f862bd..4b04c2bfe 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs @@ -154,10 +154,21 @@ internal static bool IsWholeOrAnOddRoot(Number n) => // These read that pair back. Restricted to a whole c so that nothing gains a // root it did not have -- b^c goes into the base, rather than the exponent // being divided. https://github.com/asc-community/AngouriMath/issues/740 + // And guarded as the rule above is, since gathering the exponent is the same move: + // at {1} = 1, {2} = -1, n = 1/2 the quotient is 1 / (-1) ^ 1 = -1 and the gathered + // power (1 / 1) ^ (1/2) is 1. Divf(Powf(var any1, var any3), Powf(var any2, Mulf(Integer { IsPositive: true } const1, var any3a))) - when any3 == any3a => new Powf(any1 / new Powf(any2, const1), any3), + when any3 == any3a + && (any3 is Integer + || (any1.Evaled is Real { IsPositive: true } + && any2.Evaled is Real { IsPositive: true })) + => new Powf(any1 / new Powf(any2, const1), any3), Divf(Powf(var any1, Mulf(Integer { IsPositive: true } const1, var any3)), Powf(var any2, var any3a)) - when any3 == any3a => new Powf(new Powf(any1, const1) / any2, any3), + when any3 == any3a + && (any3 is Integer + || (any1.Evaled is Real { IsPositive: true } + && any2.Evaled is Real { IsPositive: true })) + => new Powf(new Powf(any1, const1) / any2, any3), // x / x^n Divf(var any1, Powf(var any1a, var any2)) when any1 == any1a => new Powf(any1, 1 - any2), diff --git a/Sources/Tests/UnitTests/Common/QuotientOfPowersWithAWholeExponentFactorTest.cs b/Sources/Tests/UnitTests/Common/QuotientOfPowersWithAWholeExponentFactorTest.cs new file mode 100644 index 000000000..645b22bb1 --- /dev/null +++ b/Sources/Tests/UnitTests/Common/QuotientOfPowersWithAWholeExponentFactorTest.cs @@ -0,0 +1,54 @@ +// +// 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 AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Common +{ + /// + /// a^n / b^(c n) -> (a / b^c)^n and its mirror gather an exponent as + /// a^n / b^n -> (a / b)^n does, and hold on the same condition: a whole n, or + /// positive real bases (https://github.com/asc-community/AngouriMath/issues/802). The pair + /// had no guard, so x^n / y^(2 n) became (x / y^2)^n, which is 1 at + /// x = 1, y = -1, n = 1/2 where the quotient is -1. + /// + [Trait("Area", "Common")] + public sealed class QuotientOfPowersWithAWholeExponentFactorTest + { + private static System.Numerics.Complex ValueAt(Entity expr, string x, string y, string n) + { + var value = expr.Substitute("x", x.ToEntity()).Substitute("y", y.ToEntity()) + .Substitute("n", n.ToEntity()).EvalNumerical(); + return new(value.RealPart.EDecimal.ToDouble(), value.ImaginaryPart.EDecimal.ToDouble()); + } + + [Theory] + [InlineData("x ^ n / y ^ (2 * n)", "1", "-1", "1/2")] + [InlineData("x ^ n / y ^ (2 * n)", "2", "-3", "1/3")] + [InlineData("x ^ n / y ^ (3 * n)", "1 + i", "-1 + 2i", "1/2")] + [InlineData("x ^ (2 * n) / y ^ n", "-1", "1", "1/2")] + [InlineData("x ^ (2 * n) / y ^ n", "-2", "3", "3/4")] + [InlineData("x ^ (3 * n) / y ^ n", "-1 + 2i", "1 - i", "1/2")] + public void SimplifyingKeepsTheValueOffThePositiveReals(string expr, string x, string y, string n) + { + var original = expr.ToEntity(); + var simplified = original.Simplify(); + var before = ValueAt(original, x, y, n); + var after = ValueAt(simplified, x, y, n); + Assert.True((before - after).Magnitude < 1e-9, + $"{expr} simplified to {simplified.Stringize()}: {before} became {after}"); + } + + // Where the bases are positive reals the identity holds, and the gathering is kept. + [Theory] + [InlineData("2 ^ n / 3 ^ (2 * n)", "(2/9) ^ n")] + [InlineData("2 ^ (2 * n) / 3 ^ n", "(4/3) ^ n")] + public void PositiveRealBasesStillGather(string expr, string gathered) + => Assert.Equal(gathered.ToEntity(), expr.ToEntity().Simplify()); + } +} From 60be67966092c5c7d8cef0857245ddf2ffdc025c Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 13 Nov 2026 15:42:15 +0000 Subject: [PATCH 2/4] Decide a chain of comparisons by transitivity only where its operands are ordered (a > b and b > c) implies a > c was simplified to True, carrying the operands' domains but not that they are ordered. At a = i, b = 1, c = 0 the implication is NaN. The ordered condition cannot be attached as x > x attaches it (#876): at a = i, b = 0, c = 1 the conjunction is false and the implication is True, which True provided a in RR is not. So both rules, and their switch arms, fire only where every operand is known ordered: the real reading, or a known-real operand. Two BooleanSimplify rows pinned True for symbols over the complex plane; they now assert it over the reals, where it holds. Over the complex plane the input is left as written. Found by the v3 definedness specification (work/v3-spec); no issue filed. Co-Authored-By: Claude Opus 5.5 --- BREAKING-CHANGES.md | 16 ++++++ .../Transformations/Matching/MatchedRules.cs | 9 ++++ .../Patterns/Patterns.EqualityInequality.cs | 12 ++++- ...ComparisonsIsTransitiveWhereOrderedTest.cs | 51 +++++++++++++++++++ .../UnitTests/PatternsTest/BooleanSimplify.cs | 14 ++++- 5 files changed, 98 insertions(+), 4 deletions(-) create mode 100644 Sources/Tests/UnitTests/Common/AChainOfComparisonsIsTransitiveWhereOrderedTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index c7481e4b4..ffb2de4ee 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -85,6 +85,22 @@ limitcheck; no issue was filed. | `"(tan(x) + 1)^(x^(x - 1))".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `limitright((tan(x) + 1) ^ x ^ (x - 1), x, 0)` | `e` | | `"tan(x) * x^(x - 1)".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `1` after 11 s | `1` in 0.21 s | +### A chain of comparisons is decided by transitivity only where its operands are ordered + +**Silent: `(a > b and b > c) implies a > c`, and the same with `<`, is no longer simplified to `True` for symbols +over the complex plane.** An order comparison has no truth value off the real line, so at `a = i, b = 1, c = 0` +the implication is `NaN`, and the answer `True` gave it one. It is still `True` over the reals +(`MathS.Settings.Codomain` set to `Domain.Real`) and for operands known to be real. A condition `a in RR` cannot be +attached instead, as `x > x` attaches it ([#876](https://github.com/asc-community/AngouriMath/issues/876)): at +`a = i, b = 0, c = 1` the conjunction is false and the implication is `True`. Found by the v3 definedness +specification; no issue was filed. + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"((a > b) and (b > c)) implies (a > c)".ToEntity().Simplify()` | `True` | `a > b and b > c implies a > c` | +| `"((a < b) and (b < c)) implies (a < c)".ToEntity().Simplify()` | `True` | `a < b and b < c implies a < c` | +| the same over `Domain.Real` | `True` | `True`, unchanged | + ### A derivative keeps an exponent that is not rational exact **Silent: the power rule writes a constant exponent that is not rational as it is, where it wrote its decimal diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index fae97d122..93a7f82ab 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -2548,17 +2548,26 @@ is var (divided, remainder) bound => Functions.Patterns.PushNotInside(Orf.LinearChildren((Orf)bound["chain"]), disjoin: false), Soundness.Sound, description: "not (a or b or ...) = (not a) and (not b) and ..."), + // Transitivity is a fact about an order, so the pair below fires only where the + // three operands are known to be ordered. Elsewhere the implication need not have a + // truth value -- at a = i, b = 1, c = 0 it is NaN -- and the ordered condition cannot + // be attached instead, as its siblings attach it: a comparison with no truth value + // inside a conjunction that is already false leaves the implication true, so at + // a = i, b = 0, c = 1 the chain of greaters is True and `True provided a in RR` is + // not. https://github.com/asc-community/AngouriMath/issues/876 new MatchedRule( "a-chain-of-greaters-implies-its-own-ends", MatchPattern.Node(MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("c"))), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("c"))), bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(bound["b"].DomainCondition).Provided(bound["c"].DomainCondition), Soundness.SoundUnderAssumptions, + when: bound => Functions.Patterns.AreOrdered(bound["a"], bound["b"], bound["c"]), description: "(((a > b) and (b > c)) implies (a > c)) = True"), new MatchedRule( "a-chain-of-lesss-implies-its-own-ends", MatchPattern.Node(MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("c"))), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("c"))), bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(bound["b"].DomainCondition).Provided(bound["c"].DomainCondition), Soundness.SoundUnderAssumptions, + when: bound => Functions.Patterns.AreOrdered(bound["a"], bound["b"], bound["c"]), description: "(((a < b) and (b < c)) implies (a < c)) = True"), new MatchedRule( "a-equals-with-zero-on-the-left-turns-round", diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs index 79fd0c2ee..6d9ac23b1 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs @@ -136,6 +136,14 @@ internal static Entity OrderedConditionOf(Entity comparison, int operand) /// internal static Entity OrderedConditionFor(Entity entity) => OrderedCondition(entity); + /// + /// Whether every operand is known to be ordered, so that a chain of comparisons between + /// them can be decided by transitivity. Asked rather than attached: see the rule + /// a-chain-of-greaters-implies-its-own-ends. + /// + internal static bool AreOrdered(params Entity[] operands) + => operands.All(operand => OrderedCondition(operand) == True); + /// /// Whether pushing a not through this conjunction or disjunction leaves the /// expression no more complex: at most one operand may be something other than a @@ -195,10 +203,10 @@ internal static Entity PushNotInside(IEnumerable operands, bool disjoin) => PushNotInside(Orf.LinearChildren(a), disjoin: false), Impliesf(Andf(Greaterf(var any1, var any2), Greaterf(var any2a, var any3)), Greaterf(var any1a, var any3a)) - when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), + when any1 == any1a && any2 == any2a && any3 == any3a && AreOrdered(any1, any2, any3) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), Impliesf(Andf(Lessf(var any1, var any2), Lessf(var any2a, var any3)), Lessf(var any1a, var any3a)) - when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), + when any1 == any1a && any2 == any2a && any3 == any3a && AreOrdered(any1, any2, any3) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), Equalsf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero.EqualTo(zero), Greaterf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero < zero, diff --git a/Sources/Tests/UnitTests/Common/AChainOfComparisonsIsTransitiveWhereOrderedTest.cs b/Sources/Tests/UnitTests/Common/AChainOfComparisonsIsTransitiveWhereOrderedTest.cs new file mode 100644 index 000000000..8415983cf --- /dev/null +++ b/Sources/Tests/UnitTests/Common/AChainOfComparisonsIsTransitiveWhereOrderedTest.cs @@ -0,0 +1,51 @@ +// +// 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 AngouriMath.Core; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Common +{ + /// + /// (a > b and b > c) implies a > c is true where the three operands are + /// ordered, and need not have a truth value where one is not: at a = i, b = 1, c = 0 + /// it is NaN. It was simplified to a bare True for any operands. It cannot carry + /// provided a in RR as the rules beside it do + /// (https://github.com/asc-community/AngouriMath/issues/876), because at + /// a = i, b = 0, c = 1 the conjunction is already false and the implication is + /// True; so it is decided only where the operands are known to be ordered. + /// + [Trait("Area", "Common")] + public sealed class AChainOfComparisonsIsTransitiveWhereOrderedTest + { + [Theory] + [InlineData("((a > b) and (b > c)) implies (a > c)", "i", "1", "0")] + [InlineData("((a > b) and (b > c)) implies (a > c)", "i", "0", "1")] + [InlineData("((a > b) and (b > c)) implies (a > c)", "3", "2", "1")] + [InlineData("((a < b) and (b < c)) implies (a < c)", "i", "0", "1")] + [InlineData("((a < b) and (b < c)) implies (a < c)", "i", "1", "0")] + [InlineData("((a < b) and (b < c)) implies (a < c)", "1", "2", "3")] + public void SimplifyingKeepsTheTruthValue(string input, string a, string b, string c) + { + Entity At(Entity e) => e.Substitute("a", a.ToEntity()) + .Substitute("b", b.ToEntity()).Substitute("c", c.ToEntity()).Evaled; + var original = input.ToEntity(); + Assert.Equal(At(original), At(original.Simplify())); + } + + // Where every operand is ordered, transitivity decides it. + [Theory] + [InlineData("((a > b) and (b > c)) implies (a > c)")] + [InlineData("((a < b) and (b < c)) implies (a < c)")] + public void OverTheRealsItIsTrue(string input) + { + using var _ = MathS.Settings.Codomain.Set(Domain.Real); + Assert.Equal(Entity.Boolean.True, input.ToEntity().Simplify()); + } + } +} diff --git a/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs b/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs index e21284253..8529630fc 100644 --- a/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs +++ b/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs @@ -103,14 +103,24 @@ public void Test(string expr, string expected) [InlineData("x ^ 0 = 0", "false provided not x = 0")] // The 'provided' describes the domain where the expression is valid (it is 'undefined' outside). It is incorrect to drop the predicate. [InlineData("x ^ -1 = 0", "false provided not x = 0")] [InlineData("x ^ -2 = 0", "false provided not x = 0")] - [InlineData("x > y > z -> x > z", "true")] - [InlineData("x < y < z -> x < z", "true")] public void TestInequality(string expr, string expected) { var exp = expected.ToEntity(); var act = expr.ToEntity(); Assert.Equal(exp, act.Simplify()); } + + // Transitivity is decided where the operands are ordered, which a symbol is over the + // reals. Over the complex plane x > y > z -> x > z need not have a truth value, and is + // left as written: see AChainOfComparisonsIsTransitiveWhereOrderedTest. + [Theory] + [InlineData("x > y > z -> x > z", "true")] + [InlineData("x < y < z -> x < z", "true")] + public void TestTransitivityOverTheReals(string expr, string expected) + { + using var _ = MathS.Settings.Codomain.Set(AngouriMath.Core.Domain.Real); + Assert.Equal(expected.ToEntity(), expr.ToEntity().Simplify()); + } [Theory] // InnerSimplified patterns [InlineData("false provided false", null)] From 3ed79e13f4cdbc100ae136b329fe4737c2200971 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 13 Nov 2026 15:44:14 +0000 Subject: [PATCH 3/4] Turn an inverse function of a numeric reciprocal only for a nonzero numerator arcsin(n / d) -> arccsc(d / n) and its three siblings read n / d as 1 / (d / n), which needs n nonzero. At n = 0 arcsin(0 / x), which is 0 wherever x is not, became arccsc(x / 0), which has no value: the narrowing soundcheck reports. The data rules and their switch arms now refuse a zero numerator. Simplify folds 0 / x before the rules are asked, so no Simplify answer changes; the rewrite is reachable through the public rule registry, Transformation.Rewriting(RewriteRules.Trigonometric), and the test asks it there. Found by the v3 definedness specification (work/v3-spec); no issue filed. Co-Authored-By: Claude Opus 5.5 --- BREAKING-CHANGES.md | 13 ++++++ .../Transformations/Matching/MatchedRules.cs | 11 +++-- .../Patterns/Patterns.Trigonometry.cs | 8 ++-- .../AnInverseOfANumericReciprocalTest.cs | 40 +++++++++++++++++++ 4 files changed, 64 insertions(+), 8 deletions(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/AnInverseOfANumericReciprocalTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index ffb2de4ee..dba95a802 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -117,6 +117,19 @@ rational exponent is still written as its value. Found by limitcheck; no issue w | `"x^(abs(x)^arctan(2))".ToEntity().Limit("x", 0, ApproachFrom.Left)` | unevaluated | `1` | | `"x^(abs(x)^arctan(2))".ToEntity().Limit("x", 0, ApproachFrom.Right)` | unevaluated | `1` | +### An inverse function of a zero over a symbol is not turned into its reciprocal function + +**Silent, through the rule registry only: `arcsin(0 / x)` is no longer rewritten to `arccsc(x / 0)` by +`RewriteRules.Trigonometric`, nor `arccos(0 / x)` to `arcsec(x / 0)`.** The rules read `n / d` as `1 / (d / n)`, +which needs a nonzero `n`; at `n = 0` the input is `0` (or `pi / 2`) wherever `x` is not `0`, and the answer has no +value. `Simplify` folds `0 / x` before the rules are asked, so its answers do not change. Found by the v3 +definedness specification; no issue was filed. + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `Transformation.Rewriting(RewriteRules.Trigonometric).ApplyOrKeep("arcsin(0/x)")` | `arccsc(x / 0)` | `arcsin(0 / x)` | +| `Transformation.Rewriting(RewriteRules.Trigonometric).ApplyOrKeep("arccos(0/x)")` | `arcsec(x / 0)` | `arccos(0 / x)` | + ### A two-sided limit whose sides are undecided is left unevaluated **Silent: a two-sided limit is left unevaluated, rather than `NaN`, where a side's limit stops at an indeterminate form diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 93a7f82ab..995937955 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -2057,12 +2057,15 @@ is var (divided, remainder) // larger the angle is. growth: RewriteRuleGrowth.Collects), + // The four rules below are the definitions arccsc(z) = arcsin(1 / z) and its siblings, + // read through n / d = 1 / (d / n), which holds for a nonzero n. At n = 0 the left + // side is arcsin(0) = 0 and the right arccsc(d / 0), which has no value. new MatchedRule( "an-arcsine-of-a-numeric-reciprocal-is-an-arccosecant", MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("d"))), bound => new Arccosecantf(bound["d"] / bound["n"]), Soundness.SoundUnderAssumptions, - when: bound => bound["n"] is Number && bound["d"] is not Number, + when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number, description: "arcsin(1 / c) = arccosec(c), for a numeric c", // One inverse function becomes another and the quotient stays a quotient with its // operands the other way round, so the two are the same size whatever they are. @@ -2073,7 +2076,7 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("d"))), bound => new Arcsecantf(bound["d"] / bound["n"]), Soundness.SoundUnderAssumptions, - when: bound => bound["n"] is Number && bound["d"] is not Number, + when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number, description: "arccos(1 / c) = arcsec(c), for a numeric c", // One inverse function becomes another and the quotient stays a quotient with its // operands the other way round, so the two are the same size whatever they are. @@ -2084,7 +2087,7 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("d"))), bound => new Arcsinf(bound["d"] / bound["n"]), Soundness.SoundUnderAssumptions, - when: bound => bound["n"] is Number && bound["d"] is not Number, + when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number, description: "arccosec(1 / c) = arcsin(c), for a numeric c", // One inverse function becomes another and the quotient stays a quotient with its // operands the other way round, so the two are the same size whatever they are. @@ -2095,7 +2098,7 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("d"))), bound => new Arccosf(bound["d"] / bound["n"]), Soundness.SoundUnderAssumptions, - when: bound => bound["n"] is Number && bound["d"] is not Number, + when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number, description: "arcsec(1 / c) = arccos(c), for a numeric c", // One inverse function becomes another and the quotient stays a quotient with its // operands the other way round, so the two are the same size whatever they are. diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Trigonometry.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Trigonometry.cs index c59fd8417..640ad3cf4 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Trigonometry.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Trigonometry.cs @@ -214,10 +214,10 @@ internal static bool WithinZeroAndPi(Entity argument, bool closed) // TODO: add more secant/cosecant patterns - Arcsinf(Divf(var number, var notNumber)) when number is Number && notNumber is not Number => new Arccosecantf(notNumber / number), - Arccosf(Divf(var number, var notNumber)) when number is Number && notNumber is not Number => new Arcsecantf(notNumber / number), - Arccosecantf(Divf(var number, var notNumber)) when number is Number && notNumber is not Number => new Arcsinf(notNumber / number), - Arcsecantf(Divf(var number, var notNumber)) when number is Number && notNumber is not Number => new Arccosf(notNumber / number), + Arcsinf(Divf(var number, var notNumber)) when number is Number && number != Integer.Zero && notNumber is not Number => new Arccosecantf(notNumber / number), + Arccosf(Divf(var number, var notNumber)) when number is Number && number != Integer.Zero && notNumber is not Number => new Arcsecantf(notNumber / number), + Arccosecantf(Divf(var number, var notNumber)) when number is Number && number != Integer.Zero && notNumber is not Number => new Arcsinf(notNumber / number), + Arcsecantf(Divf(var number, var notNumber)) when number is Number && number != Integer.Zero && notNumber is not Number => new Arccosf(notNumber / number), _ => x }; diff --git a/Sources/Tests/UnitTests/Core/Transformations/AnInverseOfANumericReciprocalTest.cs b/Sources/Tests/UnitTests/Core/Transformations/AnInverseOfANumericReciprocalTest.cs new file mode 100644 index 000000000..efe351a62 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/AnInverseOfANumericReciprocalTest.cs @@ -0,0 +1,40 @@ +// +// 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 AngouriMath.Core.Transformations; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// arcsin(n / d) -> arccsc(d / n) for a numeric n, and its three siblings, read + /// n / d as 1 / (d / n), which holds for a nonzero n. At n = 0 it + /// took arcsin(0 / x), which is 0 wherever x is not, to + /// arccsc(x / 0), which has no value. Simplify folds 0 / x before the rule + /// is asked, so the rule set is applied here as a caller of the public registry applies it. + /// + [Trait("Area", "Core")] + public sealed class AnInverseOfANumericReciprocalTest + { + private static Entity Rewritten(string input) + => Transformation.Rewriting(RewriteRules.Trigonometric).ApplyOrKeep(input.ToEntity()); + + [Theory] + [InlineData("arcsin(0 / x)")] + [InlineData("arccos(0 / x)")] + public void AZeroNumeratorKeepsItsValue(string input) + => Assert.Equal(input.ToEntity().Substitute("x", 2).Evaled, + Rewritten(input).Substitute("x", 2).Evaled); + + [Theory] + [InlineData("arcsin(2 / x)", "arccsc(x / 2)")] + [InlineData("arccos(2 / x)", "arcsec(x / 2)")] + public void ANonzeroNumeratorStillTurnsTheFunction(string input, string expected) + => Assert.Equal(expected.ToEntity(), Rewritten(input)); + } +} From 6178967a9f46c81f3b4369b5a4300d4eb8cfd1b5 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 13 Nov 2026 15:46:08 +0000 Subject: [PATCH 4/4] Cancel a sign times a thing over its absolute value only for a real operand sgn(a) * (b * a) / abs(a) -> b provided not a = 0 holds for a real a. The library's sgn(a) is a / abs(a), so off the real line the left side is b * a^2 / abs(a)^2, which is -1 at a = i, b = 1. Realness is a reading, not a condition on where a side is defined, so the rule and its switch arm decide it as the comparison rules do (the real reading, or an operand known real) and do not fire otherwise. Simplify sorts the product before Common is asked and the nested product never reaches the rule, so no Simplify answer changes; the rewrite is reachable through Transformation.Rewriting(RewriteRules.Common), and the test asks it there. Found by the v3 definedness specification (work/v3-spec); no issue filed. Co-Authored-By: Claude Opus 5.5 --- BREAKING-CHANGES.md | 13 +++++ .../Transformations/Matching/MatchedRules.cs | 7 ++- .../Patterns/Patterns.Common.cs | 3 +- .../ASignOverAnAbsoluteValueTest.cs | 47 +++++++++++++++++++ 4 files changed, 68 insertions(+), 2 deletions(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/ASignOverAnAbsoluteValueTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index dba95a802..c0e68a410 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -157,6 +157,19 @@ limit is still `NaN`. Found by limitcheck; no issue was filed. | `"1 / log(x^2, cos(x))".ToEntity().Limit("x", 0)` | `-oo` | `limit(1 / log(x ^ 2, cos(x)), x, 0)` | | `"1 / (x * arccot(x))".ToEntity().Limit("x", 0)` | `NaN` | `limit(1 / (x * arccotan(x)), x, 0)` | +### A sign times a thing over its absolute value cancels only for a real operand + +**Silent, through the rule registry only: `sgn(x) * (y * x) / abs(x)` is no longer rewritten to +`y provided not x = 0` by `RewriteRules.Common` for an `x` not known to be real.** `sgn(x)` is `x / abs(x)`, so the +quotient is `y * x^2 / abs(x)^2`, which is `-y` at `x = i`. Over the reals (`MathS.Settings.Codomain` set to +`Domain.Real`) and for an operand known to be real it still cancels. `Simplify` sorts the product before the rule is +asked, so its answers do not change. Found by the v3 definedness specification; no issue was filed. + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `Transformation.Rewriting(RewriteRules.Common).ApplyOrKeep("sgn(x)*(y*x)/abs(x)")` | `y provided not x = 0` | `sgn(x) * y * x / abs(x)` | +| the same over `Domain.Real` | `y provided not x = 0` | `y provided not x = 0`, unchanged | + ### A limit at the jump of a step function is not answered by substitution **Silent: a limit of an expression built on `floor`, `ceil`, `round` or `sgn`, where the step's argument arrives on one diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 995937955..6d46b7cc6 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -4041,7 +4041,12 @@ is var (divided, remainder) MatchPattern.Node(MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("a"))), MatchPattern.Node(MatchPattern.Any("a"))), bound => bound["b"].Provided(!bound["a"].EqualTo(Integer.Zero)), Soundness.SoundUnderAssumptions, - description: "(sgn(a) * (b * a)) / abs(a) = b, provided a is not zero", + // sgn(a) is a / abs(a), so sgn(a) * a / abs(a) is a^2 / abs(a)^2: 1 for a real a and + // not otherwise -- at a = i it is -1. Realness is a reading, not a condition on + // where either side is defined, so it is decided here, as the comparison rules + // decide it, and the rule does not fire on an operand not known to be real. + when: bound => Functions.Patterns.OrderedConditionFor(bound["a"]) == Entity.Boolean.True, + description: "(sgn(a) * (b * a)) / abs(a) = b, for a real a, provided a is not zero", // Three copies of a go and one comes back inside the condition; the sign, the // absolute value, the quotient and two products go against the three nodes the // condition and its attachment add: the delta is -1 - 2|a|, at most -3. diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Common.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Common.cs index f05deea3a..98ba11865 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Common.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Common.cs @@ -263,7 +263,8 @@ internal static Integer DenominatorOf(Entity entity) Mulf(Absf(var any1), Absf(var any2)) => new Absf(any1 * any2), Divf(Absf(var any1), Absf(var any2)) => new Absf(any1 / any2), - Divf(Mulf(Signumf(var any1), Mulf(var any2, var any1a)), Absf(var any1b)) when any1 == any1a && any1a == any1b => any2.Provided(!any1.EqualTo(Integer.Zero)), + // sgn(a) * a / abs(a) is 1 only for a real a: at a = i it is -1. + Divf(Mulf(Signumf(var any1), Mulf(var any2, var any1a)), Absf(var any1b)) when any1 == any1a && any1a == any1b && OrderedCondition(any1) == Entity.Boolean.True => any2.Provided(!any1.EqualTo(Integer.Zero)), Mulf(Signumf(var any1), Absf(var any1a)) when any1 == any1a => any1, Mulf(Absf(var any1a), Signumf(var any1)) when any1 == any1a => any1, diff --git a/Sources/Tests/UnitTests/Core/Transformations/ASignOverAnAbsoluteValueTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ASignOverAnAbsoluteValueTest.cs new file mode 100644 index 000000000..7a9480f69 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/ASignOverAnAbsoluteValueTest.cs @@ -0,0 +1,47 @@ +// +// 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 AngouriMath.Core; +using AngouriMath.Core.Transformations; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// sgn(a) * (b * a) / abs(a) -> b holds for a real a. The library's sgn(a) + /// is a / abs(a), so off the real line the left side is b * a^2 / abs(a)^2: at + /// a = i, b = 1 it is -1. Simplify sorts the product before + /// Common is asked, and the rule's nested product does not survive that, so the rule + /// set is applied here as a caller of the public registry applies it. + /// + [Trait("Area", "Core")] + public sealed class ASignOverAnAbsoluteValueTest + { + private static Entity Rewritten(string input) + => Transformation.Rewriting(RewriteRules.Common).ApplyOrKeep(input.ToEntity()); + + [Theory] + [InlineData("i")] + [InlineData("1 + i")] + [InlineData("-2")] + [InlineData("3")] + public void TheRewriteKeepsTheValue(string at) + { + const string input = "sgn(x) * (y * x) / abs(x)"; + Entity At(Entity e) => e.Substitute("x", at.ToEntity()).Substitute("y", 1).Evaled; + Assert.Equal(At(input.ToEntity()), At(Rewritten(input))); + } + + [Fact] + public void OverTheRealsItCancels() + { + using var _ = MathS.Settings.Codomain.Set(Domain.Real); + Assert.Equal("y provided not x = 0".ToEntity(), Rewritten("sgn(x) * (y * x) / abs(x)")); + } + } +}