diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index fa9a66e74..9d3709ea1 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -403,7 +403,8 @@ system is now eliminated one unknown at a time, and an unknown that nothing is l zero. Where one does not, or where a branch cannot be decided, the system is declined as `null`, which `Solve` documents as no solution found ([#212](https://github.com/asc-community/AngouriMath/issues/212)). A family with an `n_1` from a periodic root, which stands for every whole number, is kept where it is zero for each, as -`forall n_1 in ZZ` decides it. Code that caught the exception around `Solve` to detect a non-square system no longer +`forall n_1 in ZZ` decides it, and a family that says where it holds, as a root's inverse does, is kept where it is +zero wherever that holds. Code that caught the exception around `Solve` to detect a non-square system no longer sees it. | Input | Was (2.6.0) | Now | @@ -413,7 +414,7 @@ sees it. | `MathS.Equations("sin(x)", "x").Solve("x")` | `WrongNumberOfArgumentsException` | `[0]` | | `MathS.Equations("sin(x) - 1/2").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[pi / 6 + 2 * pi * n_1, t_1], [pi - pi / 6 + 2 * pi * n_1, t_1]]` | | `MathS.Equations("sin(x) - y", "cos(x) - y", "x - pi/4").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[pi / 4, 1/2 * sqrt(2)]]` | -| `MathS.Equations("sqrt(y) - x").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `null`: `y = x^2` is no solution where `x` is negative | +| `MathS.Equations("sqrt(y) - x").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[t_1, t_1 ^ 2 provided t_1 = 0 or -1/2 * pi < arg(t_1) and arg(t_1) <= 1/2 * pi]]`: `y = x^2` is a solution only where `sqrt` takes `x` as a value | | `MathS.Equations("x + y - a", "x - y - b", "x - c").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `null`: there are solutions only where `a + b = 2c` | ### A whole number of periods comes out of a trigonometric function under a quantifier @@ -429,6 +430,18 @@ or of `pi` for a tangent or a cotangent, the term is taken out, as `Complex.sin_ | `"forall n in ZZ : sin(x + 2 pi n) = sin(x)".ToEntity().Simplify()` | `forall n in ZZ : sin(2 * n * pi + x) = sin(x)` | `True` | | `"forall n in ZZ : tan(pi/4 + pi n) = 1".ToEntity().Simplify()` | `forall n in ZZ : tan(pi * (1/4 + n)) = 1` | `True` | +### A principal root of a power is read with what the quantifiers establish + +**Silent: a quantified statement about `(t^n)^(1/n)` is decided where it was left as written.** Where the quantifiers +around a principal `n`-th root of an `n`-th power, for a whole `n >= 2`, establish that `t` is `0` or in the sector +`-pi/n < arg(t) <= pi/n` where that root takes its values, or that `t >= 0`, the root is `t`, as +`Complex.pow_cpow_nat_inv` has it. Nothing changes outside a quantifier, and `sqrt(t^2)` is not `t` +([#212](https://github.com/asc-community/AngouriMath/issues/212)). + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"forall t in RR : t >= 0 implies sqrt(t^2) = t".ToEntity().Simplify()` | `forall t in RR : t >= 0 implies sqrt(t ^ 2) = t` | `True` | + ### A system is not answered with a copy of one of its rows **Silent: a repeated row goes.** Two branches of an elimination can reach one solution, and each was answered: two diff --git a/Sources/.editorconfig b/Sources/.editorconfig index f2e2a9b0a..cb1b7bac9 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -405,6 +405,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [Tests/UnitTests/Core/PeriodByFactsTest.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n +[Tests/UnitTests/Core/RootByFactsTest.cs] +file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n + [AngouriMath/Core/Entity/Continuous/Number/ErrorFunctions.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n diff --git a/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs b/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs index d0ade8b60..60a5e50ee 100644 --- a/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs +++ b/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs @@ -242,6 +242,8 @@ internal static Entity Renamed(Entity expression, Variable from, Variable to) Dividesf(not Number, _) or Congruentf(_, _, not Number) => true, Equalsf(Modf(_, var modulus), Modf(_, var other)) => modulus is not Number && modulus == other, Floorf(not Number) or Ceilf(not Number) => true, + // A principal root of a whole power, which PrincipalPowerOfAPower reads. + Powf(Powf(not Number, Integer), Rational) => true, _ => false }; @@ -487,6 +489,61 @@ internal static bool PrimeDividesByTheBinomialTheorem(Entity p, Entity d) return Recorded(function(argument), function(rest), $"{periods} is a whole number of periods", lemma); } + /// + /// z for the principal root (z^n)^(1/n) of a whole n >= 2, where the facts in + /// scope put z where that root takes its values, or : at 0 or in + /// the sector -pi/n < arg(z) <= pi/n, which is how the power's inversion states it, or on + /// the half-line z >= 0, as Complex.pow_cpow_nat_inv has it. So sqrt(t^2) is + /// t where t = 0 or -pi/2 < arg(t) <= pi/2. + /// https://github.com/asc-community/AngouriMath/issues/212 + /// + internal static Entity? PrincipalPowerOfAPower(Entity z, Entity inner, Entity exponent) + { + if (top is null || !MentionsARenamedName(z) + || inner is not Integer { EInteger: var n } || n.CompareTo(2) < 0 + || exponent is not Rational { ERational: var p } || p.CompareTo(ERational.Create(EInteger.One, n)) != 0) + return null; + foreach (var fact in InScope()) + if (IsOnTheHalfLine(fact, z) || IsInTheSector(fact, z, exponent)) + return Recorded(MathS.Pow(MathS.Pow(z, inner), exponent), z, + $"{z} is where the principal {inner}-th root takes its values", "Complex.pow_cpow_nat_inv"); + return null; + + static bool IsOnTheHalfLine(Entity fact, Entity z) + => fact switch + { + GreaterOrEqualf(var left, Integer { IsZero: true }) => left == z, + Greaterf(var left, Integer { IsZero: true }) => left == z, + LessOrEqualf(Integer { IsZero: true }, var right) => right == z, + Lessf(Integer { IsZero: true }, var right) => right == z, + _ => false + }; + + // z = 0 or (-p pi < arg(z) and arg(z) <= p pi), the two sides of each in either order. + static bool IsInTheSector(Entity fact, Entity z, Entity p) + { + if (fact is not Orf(var either, var other)) + return false; + var (zero, sector) = IsZero(either, z) ? (either, other) : (other, either); + if (!IsZero(zero, z) || sector is not Andf(var first, var second)) + return false; + var bound = p * MathS.pi; + return Below(first, -bound) && Above(second, bound) || Below(second, -bound) && Above(first, bound); + + bool Below(Entity side, Entity lower) + => side is Lessf(var low, Argf(var of)) && of == z && Same(low, lower) + || side is Greaterf(Argf(var on), var low2) && on == z && Same(low2, lower); + bool Above(Entity side, Entity upper) + => side is LessOrEqualf(Argf(var of), var high) && of == z && Same(high, upper) + || side is GreaterOrEqualf(var high2, Argf(var on)) && on == z && Same(high2, upper); + } + static bool IsZero(Entity statement, Entity z) + => statement is Equalsf(var left, var right) && (left == z && right == 0 || right == z && left == 0); + // The bounds are multiples of pi, so they are compared by value. + static bool Same(Entity a, Entity b) + => !a.Vars.Any() && (a - b).Evaled is Complex difference && ((Real)difference.Abs()).EDecimal.ToDouble() < 1e-12; + } + /// A function takes whole periods out of, of anything but a number. private static bool IsPeriodic(Entity node) => node is Sinf(not Number) or Cosf(not Number) or Tanf(not Number) or Cotanf(not Number) or Secantf(not Number) or Cosecantf(not Number); diff --git a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs index b28c5d8f4..ad8b1c12c 100644 --- a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs +++ b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs @@ -25,10 +25,11 @@ namespace AngouriMath.Functions.Algebra.AnalyticalSolving /// /// /// An answer is given only where it is shown to hold. The elimination trusts each solve - /// it makes, and a solve can answer for a case its equation does not cover: sqrt(y) = x - /// is solved for y as x^2, which is no solution where x is negative. So - /// each family is kept only where every equation, with the family substituted, simplifies to - /// 0. sqrt(t^2) - t does not, and that system is declined. + /// it makes, and a solve can answer for a case its equation does not cover. So each family is + /// kept only where every equation, with the family substituted, simplifies to 0. A family + /// that says where it holds is checked there: sqrt(y) = x is solved for y as + /// x^2 provided x is where sqrt takes its values, and sqrt(t^2) - t + /// is zero wherever that holds. /// /// /// A decline declines the whole system. An equation left with no unknown in it is zero, @@ -68,16 +69,22 @@ Variable ParameterFor(int index) return null; var own = new HashSet(equations.SelectMany(equation => equation.Vars)); foreach (var family in families) + { + // A family that says where it holds, as y = t^2 provided t is where sqrt takes its + // values, is checked there and nowhere else. + var condition = family.OfType().Select(entry => entry.Predicate).Aggregate((Entity?)null, (all, one) => all is null ? one : all & one); + var bare = family.Select(entry => entry is Providedf(var value, _) ? value : entry).ToList(); foreach (var equation in equations) { var substituted = equation; for (var index = 0; index < variables.Length; index++) - substituted = substituted.Substitute(variables[index], family[index]); + substituted = substituted.Substitute(variables[index], (condition is null ? family : bare)[index]); // An n_1 a family brings from a periodic root stands for every whole number. var whole = substituted.Vars.Where(name => !own.Contains(name) && name.Name.StartsWith("n_")).Distinct().ToList(); - if (!Vanishes(substituted, whole)) + if (!Vanishes(substituted, whole) && (condition is null || !VanishesWhere(substituted, condition, whole))) return null; } + } return families; } @@ -235,6 +242,22 @@ private static bool Vanishes(Entity expression, IReadOnlyList whole) }; } + /// + /// Whether is zero wherever holds, + /// decided as a statement for every value of its symbols, a whole one for a symbol in + /// : sqrt(t^2) - t is zero where + /// t = 0 or -pi/2 < arg(t) <= pi/2, which is + /// forall t in CC : (t = 0 or -pi/2 < arg(t) <= pi/2) implies sqrt(t^2) - t = 0. + /// https://github.com/asc-community/AngouriMath/issues/212 + /// + private static bool VanishesWhere(Entity expression, Entity condition, IReadOnlyList whole) + { + Entity statement = new Impliesf(condition, expression.EqualTo(Integer.Zero)); + foreach (var name in statement.Vars.Distinct().ToList()) + statement = MathS.ForAll(name, whole.Contains(name) ? MathS.Sets.Z : MathS.Sets.C, statement); + return statement.Simplify() == Entity.Boolean.True; + } + /// /// with each of its symbols at a fixed value, a whole one for /// a symbol in . diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs index b168e9d6a..c2f8e8f43 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Arithmetics.Classes.cs @@ -407,6 +407,7 @@ x.Evaled is Complex c // https://github.com/asc-community/AngouriMath/issues/281 (Rational radicand, Rational exponent) when RootExtraction.PullOutOfRadical(radicand, exponent) is { } pulled => pulled.InnerSimplified(isExact), + (Powf(var z, var inner), var exponent) when Functions.Boolean.QuantifierFacts.PrincipalPowerOfAPower(z, inner, exponent) is { } root => root, _ => null }, (@this, a, b) => ((Powf)@this).New(a, b), isExact); diff --git a/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs b/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs index 3cd65db58..55aee0a80 100644 --- a/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs +++ b/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs @@ -116,14 +116,36 @@ public void AnOverdeterminedSystemIsSolved(string[] equations, string[] variable } /// - /// What the elimination finds and cannot show to hold. sqrt(y) = x is solved for - /// y as x^2, no solution where x is negative. The coefficient of - /// y in the second is zero without being written so, and dividing by it gives a - /// family that Simplify calls zero provided it is not zero. The third has solutions - /// only where a + b = 2c. + /// A family that says where it holds is checked there. sqrt(y) = x is solved for + /// y as x^2 where x is 0 or in the half-plane sqrt takes + /// its values in, so the family is (t_1, t_1^2) under that condition. It holds at + /// each t_1 in the sector, i/2 on its edge among them, and is not claimed + /// at a negative one, where sqrt(t_1^2) is -t_1. + /// + [Fact] + public void AFamilyThatSaysWhereItHoldsIsCheckedThere() + { + var solutions = Solve(new[] { "sqrt(y) - x" }, new[] { "x", "y" }); + Assert.NotNull(solutions); + Assert.Equal(1, solutions!.RowCount); + var y = Assert.IsType(solutions[0, 1]); + var t = Assert.IsType(solutions[0, 0]); + foreach (var at in new Entity[] { 2, "1.3 + 0.7i", "i/2", 0 }) + { + Assert.Equal(Entity.Boolean.True, y.Predicate.Substitute(t, at).Evaled); + var residual = ("sqrt(y) - x".ToEntity().Substitute("y", y.Expression).Substitute("x", t)).Substitute(t, at); + Assert.True(((Entity.Number.Real)((Entity.Number.Complex)residual.Evaled).Abs()).EDecimal.ToDouble() < 1e-12, $"{residual}"); + } + Assert.Equal(Entity.Boolean.False, y.Predicate.Substitute(t, -2).Evaled); + } + + /// + /// What the elimination finds and cannot show to hold. The coefficient of y in the + /// first is zero without being written so, and dividing by it gives a family that + /// Simplify calls zero provided it is not zero. The second has solutions only where + /// a + b = 2c. /// [Theory] - [InlineData(new[] { "sqrt(y) - x" }, new[] { "x", "y" })] [InlineData(new[] { "x^2 - ((a + 1)^2 - a^2 - 2*a - 1)*y" }, new[] { "x", "y" })] [InlineData(new[] { "x + y - a", "x - y - b", "x - c" }, new[] { "x", "y" })] public void WhatCannotBeShownToHoldIsDeclined(string[] equations, string[] variables) diff --git a/Sources/Tests/UnitTests/Core/RootByFactsTest.cs b/Sources/Tests/UnitTests/Core/RootByFactsTest.cs new file mode 100644 index 000000000..c1bfa6683 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/RootByFactsTest.cs @@ -0,0 +1,46 @@ +// +// 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; +using AngouriMath.Extensions; +using Xunit; +using static AngouriMath.Entity; + +namespace AngouriMath.Tests.Core +{ + /// + /// The principal n-th root of an n-th power, read with what the quantifiers establish: (z^n)^(1/n) + /// is z where z is 0 or in the sector -pi/n < arg(z) <= pi/n, which is how + /// the power's inversion states where its solution holds, or where z >= 0. + /// + /// + [Trait("Area", "Core")] + public sealed class RootByFactsTest + { + [Theory] + [InlineData("forall t in CC : (t = 0 or -1/2 * pi < arg(t) and arg(t) <= 1/2 * pi) implies sqrt(t^2) = t")] + [InlineData("forall t in CC : (arg(t) <= pi/2 and -pi/2 < arg(t) or t = 0) implies sqrt(t^2) = t")] + [InlineData("forall t in CC : (t = 0 or -1/3 * pi < arg(t) and arg(t) <= 1/3 * pi) implies (t^3)^(1/3) = t")] + [InlineData("forall t in RR : t >= 0 implies sqrt(t^2) = t")] + public void DecidedByWhatTheQuantifiersEstablish(string statement) + => Assert.Equal(Boolean.True, statement.ToEntity().Simplify()); + + [Theory] + // False at t = -1. + [InlineData("forall t in RR : sqrt(t^2) = t")] + // The sector of the square root is half of this: false at t = -1. + [InlineData("forall t in CC : (-pi < arg(t) and arg(t) <= pi) implies sqrt(t^2) = t")] + // The square root's sector, not the cube root's: false at t = i, where (i^3)^(1/3) is e^(-i pi/6). + [InlineData("forall t in CC : (t = 0 or -1/2 * pi < arg(t) and arg(t) <= 1/2 * pi) implies (t^3)^(1/3) = t")] + public void NotClaimedWhereTheFactsDoNotHold(string statement) + => Assert.NotEqual(Boolean.True, statement.ToEntity().Simplify()); + + [Fact] + public void OutsideAQuantifierNothingIsAssumed() + => Assert.NotEqual(MathS.Var("t"), "sqrt(t^2)".ToEntity().Simplify()); + } +}