diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index a70ca6bd5..c0e68a410 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 @@ -71,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 @@ -87,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 @@ -114,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 f60717747..6d46b7cc6 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. @@ -2548,17 +2551,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", @@ -3086,6 +3098,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 +3121,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. @@ -4017,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/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/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/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/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/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()); + } +} 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)")); + } + } +} 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)); + } +} 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)]