diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index c96fee704..fa9a66e74 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -401,18 +401,34 @@ over the rationals with rational solutions or had fewer equations and was linear system is now eliminated one unknown at a time, and an unknown that nothing is left to constrain becomes a parameter, `t_1`, as in the linear case. Every row is substituted back into every equation and kept only where each simplifies to 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)). Code that caught the -exception around `Solve` to detect a non-square system no longer sees it. +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 +sees it. | Input | Was (2.6.0) | Now | |---|---|---| | `MathS.Equations("x^2 + y^2 - 1").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[t_1, sqrt(-(t_1 ^ 2 + -1))], [t_1, -sqrt(-(t_1 ^ 2 + -1))]]` | | `MathS.Equations("a*x + y - 1").Solve("x", "y")` | `WrongNumberOfArgumentsException` | `[[t_1, -(a * t_1 + -1)]]` | | `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("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 + +**Silent: a statement quantified over whole numbers is decided where it was left as written.** Where the quantifiers +around a sine, a cosine, a secant or a cosecant establish that a term of its argument is a whole multiple of `2 pi`, +or of `pi` for a tangent or a cotangent, the term is taken out, as `Complex.sin_add_int_mul_two_pi` and +`Complex.tan_add_int_mul_pi` have it. Nothing changes outside a quantifier, and `sin(x + pi n)` keeps its `pi n` +([#212](https://github.com/asc-community/AngouriMath/issues/212)). + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"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 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 8285c80fe..f2e2a9b0a 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -402,6 +402,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [Tests/UnitTests/Core/FloorByFactsTest.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/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 + [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 3ccdda17a..d0ade8b60 100644 --- a/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs +++ b/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs @@ -76,7 +76,8 @@ private sealed class Frame /// internal static (Entity? Verdict, Entity Body)? Decide(Quantifiers.Kind kind, Entity var, Entity over, Entity body, bool isExact) { - if (var is not Variable x || over is not Set set || !body.Nodes.Any(Reads)) + if (var is not Variable x || over is not Set set + || !body.Nodes.Any(node => Reads(node) || set is SpecialSet whole && Quantifiers.IsIntegerSet(whole) && IsPeriodic(node))) return null; var renamed = Variable.CreateVariableUnchecked($"{x.Name}'{Interlocked.Increment(ref lastRenamed)}"); var mark = ProofRecording.Mark(); @@ -450,6 +451,46 @@ internal static bool PrimeDividesByTheBinomialTheorem(Entity p, Entity d) return null; } + /// + /// The function of with each term of it that is a whole number of + /// periods by the facts in scope taken out, or : sin(x + 2 pi n) is + /// sin(x) for a whole n, as Complex.sin_add_int_mul_two_pi has it. The period is + /// times pi: two for the sine, the cosine, the secant and the + /// cosecant, and one for the tangent and the cotangent, as Complex.tan_add_int_mul_pi has it. + /// https://github.com/asc-community/AngouriMath/issues/212 + /// + internal static Entity? WithoutWholePeriods(Entity argument, int halfTurns, System.Func function, string lemma) + { + if (top is null || argument is Number || !MentionsARenamedName(argument)) + return null; + // A term of the argument, or of its multiple of pi where it is gathered into one, + // such as pi * (2 n + 1/6). + var kept = new List(); + Entity? periods = null; + foreach (var term in Sumf.LinearChildren(argument)) + { + if (!MentionsARenamedName(term) || MathS.UnsafeAndInternal.DivideByEntityStrict(term, MathS.pi) is not { } multiple) + { + kept.Add(term); + continue; + } + var parts = Sumf.LinearChildren(multiple); + foreach (var part in parts) + if (MentionsARenamedName(part) && IsWholeNumber(Rational.Create(1, halfTurns) * part)) + periods = periods is null ? part * MathS.pi : periods + part * MathS.pi; + else + kept.Add(parts.Count == 1 ? term : part * MathS.pi); + } + if (periods is null) + return null; + var rest = kept.Count == 0 ? Integer.Zero : kept.Aggregate((left, right) => left + right); + return Recorded(function(argument), function(rest), $"{periods} is a whole number of periods", lemma); + } + + /// 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); + /// , with the step from recorded where a proof is. private static Entity Recorded(Entity from, Entity to, string rule, string lemma) { diff --git a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs index 4f8b648e6..b28c5d8f4 100644 --- a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs +++ b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/NonSquareSystemSolver.cs @@ -66,13 +66,16 @@ Variable ParameterFor(int index) if (Eliminate(equations, variables, variables.Length, ParameterFor, ledger) is not { Count: > 0 } families) return null; + var own = new HashSet(equations.SelectMany(equation => equation.Vars)); foreach (var family in families) foreach (var equation in equations) { var substituted = equation; for (var index = 0; index < variables.Length; index++) substituted = substituted.Substitute(variables[index], family[index]); - if (!Vanishes(substituted)) + // 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)) return null; } return families; @@ -183,7 +186,7 @@ Variable ParameterFor(int index) /// private static bool? Holds(Entity equation) { - if (Vanishes(equation)) + if (Vanishes(equation, System.Array.Empty())) return true; if (equation.Vars.Any() || equation.Evaled is not Complex value || value.IsNaN) return null; @@ -201,30 +204,50 @@ Variable ParameterFor(int index) /// 0 provided not c = 0 for a c that is zero without being written /// 0, such as (a + 1)^2 - a^2 - 2a - 1. /// - private static bool Vanishes(Entity expression) + /// + /// A symbol in stands for every whole number, so it is pinned at + /// one, and the expression is zero where it is zero for each: sin(pi/6 + 2 pi n_1) - 1/2 + /// is decided as forall n_1 in ZZ : sin(pi/6 + 2 pi n_1) - 1/2 = 0, which takes the + /// whole periods out. https://github.com/asc-community/AngouriMath/issues/212 + /// + private static bool Vanishes(Entity expression, IReadOnlyList whole) { if (expression.InnerSimplified.Evaled is Complex { IsZero: true }) return true; // Away from zero at a point is not zero everywhere, which settles most without // simplifying. - if (Pinned(expression).Evaled is Complex { IsNaN: false } atAPoint + if (Pinned(expression, whole).Evaled is Complex { IsNaN: false } atAPoint && ((Real)atAPoint.Abs()).EDecimal.ToDouble() > 1e-9) return false; + if (whole.Count > 0) + { + Entity statement = expression.EqualTo(Integer.Zero); + foreach (var name in whole) + statement = MathS.ForAll(name, MathS.Sets.Z, statement); + if (statement.Simplify() == Entity.Boolean.True) + return true; + } return expression.Simplify() switch { Providedf(var simplified, var condition) => - simplified.Evaled is Complex { IsZero: true } && Pinned(condition).Evaled is Entity.Boolean { Value: true }, + simplified.Evaled is Complex { IsZero: true } && Pinned(condition, whole).Evaled is Entity.Boolean { Value: true }, var simplified => simplified.Evaled is Complex { IsZero: true }, }; } - /// with each of its symbols at a fixed value. - private static Entity Pinned(Entity expression) + /// + /// with each of its symbols at a fixed value, a whole one for + /// a symbol in . + /// + private static Entity Pinned(Entity expression, IReadOnlyList whole) { var values = new[] { 1.37, 0.61, 2.23, 1.91, 0.83, 1.13 }; - var index = 0; + var wholeValues = new[] { 2, -1, 3 }; + var (index, wholeIndex) = (0, 0); foreach (var symbol in expression.Vars.ToList()) - expression = expression.Substitute(symbol, values[index++ % values.Length]); + expression = whole.Contains(symbol) + ? expression.Substitute(symbol, wholeValues[wholeIndex++ % wholeValues.Length]) + : expression.Substitute(symbol, values[index++ % values.Length]); return expression; } } diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Trigonometry.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Trigonometry.Classes.cs index d10128d31..5f8d48127 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Trigonometry.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Continuous/Evaluation.Continuous.Trigonometry.Classes.cs @@ -48,6 +48,7 @@ protected override Entity InnerSimplify(bool isExact) => { Complex n when !isExact => Number.Sin(n), { Evaled: Complex n } arg when isExact && TrigonometryTableValues.PullSin(n, out var res) => res, + _ when Functions.Boolean.QuantifierFacts.WithoutWholePeriods(a, 2, static x => new Sinf(x), "Complex.sin_add_int_mul_two_pi") is { } reduced => reduced.InnerSimplified(isExact), _ => null }, (@this, a) => ((Sinf)@this).New(a), isExact); @@ -63,6 +64,7 @@ protected override Entity InnerSimplify(bool isExact) => { Complex n when !isExact => Number.Cos(n), { Evaled: Complex n } when isExact && TrigonometryTableValues.PullCos(n, out var res) => res, + _ when Functions.Boolean.QuantifierFacts.WithoutWholePeriods(a, 2, static x => new Cosf(x), "Complex.cos_add_int_mul_two_pi") is { } reduced => reduced.InnerSimplified(isExact), _ => null }, (@this, a) => ((Cosf)@this).New(a), isExact); @@ -83,6 +85,7 @@ protected override Entity InnerSimplify(bool isExact) => ? (1 / res).InnerSimplified : null : Secant(n), + _ when Functions.Boolean.QuantifierFacts.WithoutWholePeriods(a, 2, static x => new Secantf(x), "Complex.cos_add_int_mul_two_pi") is { } reduced => reduced.InnerSimplified(isExact), _ => null }, (@this, a) => ((Secantf)@this).New(a), isExact); @@ -103,6 +106,7 @@ protected override Entity InnerSimplify(bool isExact) => ? (1 / res).InnerSimplified : null : Cosecant(n), + _ when Functions.Boolean.QuantifierFacts.WithoutWholePeriods(a, 2, static x => new Cosecantf(x), "Complex.sin_add_int_mul_two_pi") is { } reduced => reduced.InnerSimplified(isExact), _ => null }, (@this, a) => ((Cosecantf)@this).New(a), isExact); @@ -157,6 +161,7 @@ protected override Entity InnerSimplify(bool isExact) => isExact ? TrigonometryTableValues.PullTan(n, out var res) ? res : null : Number.Tan(n), + _ when Functions.Boolean.QuantifierFacts.WithoutWholePeriods(a, 1, static x => new Tanf(x), "Complex.tan_add_int_mul_pi") is { } reduced => reduced.InnerSimplified(isExact), _ => null }, (@this, a) => ((Tanf)@this).New(a), isExact); @@ -175,6 +180,7 @@ protected override Entity InnerSimplify(bool isExact) => isExact ? TrigonometryTableValues.PullTan(n, out var res) ? (1 / res).InnerSimplified : null : Number.Cotan(n), + _ when Functions.Boolean.QuantifierFacts.WithoutWholePeriods(a, 1, static x => new Cotanf(x), "Complex.tan_add_int_mul_pi") is { } reduced => reduced.InnerSimplified(isExact), _ => null }, (@this, a) => ((Cotanf)@this).New(a), isExact); diff --git a/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs b/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs index 311a57b01..3cd65db58 100644 --- a/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs +++ b/Sources/Tests/UnitTests/Algebra/SolveTest/NonSquareSystemTest.cs @@ -30,11 +30,13 @@ public sealed class NonSquareSystemTest /// Each row, substituted into each equation, is zero at several values of the parameters /// and symbols left in it, negative ones among them. That is checked numerically rather /// than by simplifying, which is how the solver checks it: sqrt(t^2) - t is zero at - /// every positive t and at no negative one. + /// every positive t and at no negative one. An n_1, which a periodic root + /// brings and which stands for a whole number, is sampled at whole numbers. /// private static void HoldsAtSampledValues(string[] equations, string[] variables, Entity.Matrix solutions) { var samples = new[] { 1.37, -1.7, 2.3, -0.61 }; + var wholeSamples = new[] { 2, -1, 3, 0 }; for (var row = 0; row < solutions.RowCount; row++) foreach (var text in equations) { @@ -46,7 +48,9 @@ private static void HoldsAtSampledValues(string[] equations, string[] variables, { var pinned = residual; for (var i = 0; i < symbols.Count; i++) - pinned = pinned.Substitute(symbols[i], samples[(shift + i) % samples.Length]); + pinned = symbols[i].Name.StartsWith("n_") && !equations.Any(equation => equation.ToEntity().Vars.Contains(symbols[i])) + ? pinned.Substitute(symbols[i], wholeSamples[(shift + i) % wholeSamples.Length]) + : pinned.Substitute(symbols[i], samples[(shift + i) % samples.Length]); var value = Assert.IsAssignableFrom(pinned.Evaled); Assert.False(value.IsNaN, $"{residual} at {pinned}"); Assert.True(((Entity.Number.Real)value.Abs()).EDecimal.ToDouble() < 1e-9, $"{residual} at {pinned} is {value}"); @@ -74,6 +78,25 @@ public void AShortSystemIsAFamily(string[] equations, string[] variables, int ro HoldsAtSampledValues(equations, variables, solutions); } + /// + /// A family a periodic root brings a whole-number parameter to, n_1, which holds for + /// every whole n_1 and is answered: sin(x) = 1/2 in x and y is + /// the two families (pi/6 + 2 pi n_1, t_1) and (pi - pi/6 + 2 pi n_1, t_1). + /// + [Theory] + [InlineData(new[] { "sin(x) - 1/2" }, new[] { "x", "y" }, 2)] + [InlineData(new[] { "cos(x) - 1" }, new[] { "x", "y" }, 1)] + [InlineData(new[] { "tan(x) - 1" }, new[] { "x", "y" }, 1)] + [InlineData(new[] { "sin(x) - 1/2", "y - x" }, new[] { "x", "y", "z" }, 2)] + public void AFamilyWithAWholeNumberParameterIsAnswered(string[] equations, string[] variables, int rows) + { + var solutions = Solve(equations, variables); + Assert.NotNull(solutions); + Assert.Equal(rows, solutions!.RowCount); + Assert.Contains(solutions.Vars, name => name.Name.StartsWith("n_")); + HoldsAtSampledValues(equations, variables, solutions); + } + /// /// More equations than unknowns, which the triangularisation does not take because they /// are not polynomial. The last drops x = -1, where sin(-pi/2) - 1 is -2. diff --git a/Sources/Tests/UnitTests/Core/PeriodByFactsTest.cs b/Sources/Tests/UnitTests/Core/PeriodByFactsTest.cs new file mode 100644 index 000000000..a94898ddb --- /dev/null +++ b/Sources/Tests/UnitTests/Core/PeriodByFactsTest.cs @@ -0,0 +1,49 @@ +// +// 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 +{ + /// + /// A whole number of periods taken out of a trigonometric function's argument, where the + /// quantifiers around it establish that the multiple is whole: sin(x + 2 pi n) is + /// sin(x) for every whole n. + /// + /// + [Trait("Area", "Core")] + public sealed class PeriodByFactsTest + { + [Theory] + [InlineData("forall n in ZZ : sin(x + 2 pi n) = sin(x)")] + [InlineData("forall n in ZZ : cos(x - 4 pi n) = cos(x)")] + [InlineData("forall n in ZZ : cos(2 pi n) = 1")] + [InlineData("forall n in ZZ : sin(pi/6 + 2 pi n) - 1/2 = 0")] + [InlineData("forall n in ZZ : tan(pi/4 + pi n) = 1")] + [InlineData("forall n in ZZ : sec(2 pi n) = 1")] + [InlineData("forall n in ZZ : forall m in ZZ : sin(x + 2 pi n - 2 pi m) = sin(x)")] + public void DecidedByWhatTheQuantifiersEstablish(string statement) + => Assert.Equal(Boolean.True, statement.ToEntity().Simplify()); + + [Theory] + // pi is half a period of the sine: false at n = 1 for x = pi/2. + [InlineData("forall n in ZZ : sin(x + pi n) = sin(x)")] + // n is not whole, so 2 pi n is not a period: false at n = 1/4. + [InlineData("forall n in RR : sin(2 pi n) = 0")] + // pi/2 is half a period of the tangent: undefined at n = 1. + [InlineData("forall n in ZZ : tan(pi/4 + pi n / 2) = 1")] + public void NotClaimedWhereTheFactsDoNotHold(string statement) + => Assert.NotEqual(Boolean.True, statement.ToEntity().Simplify()); + + [Fact] + public void OutsideAQuantifierNothingIsAssumed() + => Assert.Contains(MathS.Var("n"), "sin(x + 2 pi n)".ToEntity().Simplify().Vars); + } +}