Answer a family with a whole-number parameter

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

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
 

Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs

@@ -76,7 +76,8 @@ private sealed class Frame
         /// </summary>
         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;
         }
 
+        /// <summary>
+        /// The function of <paramref name="argument"/> with each term of it that is a whole number of
+        /// periods by the facts in scope taken out, or <see langword="null"/>: <c>sin(x + 2 pi n)</c> is
+        /// <c>sin(x)</c> for a whole <c>n</c>, as <c>Complex.sin_add_int_mul_two_pi</c> has it. The period is
+        /// <paramref name="halfTurns"/> times <c>pi</c>: two for the sine, the cosine, the secant and the
+        /// cosecant, and one for the tangent and the cotangent, as <c>Complex.tan_add_int_mul_pi</c> has it.
+        /// https://github.com/asc-community/AngouriMath/issues/212
+        /// </summary>
+        internal static Entity? WithoutWholePeriods(Entity argument, int halfTurns, System.Func<Entity, Entity> 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>();
+            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);
+        }
+
+        /// <summary>A function <see cref="WithoutWholePeriods"/> takes whole periods out of, of anything but a number.</summary>
+        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);
+
         /// <summary><paramref name="to"/>, with the step from <paramref name="from"/> recorded where a proof is.</summary>
         private static Entity Recorded(Entity from, Entity to, string rule, string lemma)
         {

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<Variable>(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)
         /// </summary>
         private static bool? Holds(Entity equation)
         {
-            if (Vanishes(equation))
+            if (Vanishes(equation, System.Array.Empty<Variable>()))
                 return true;
             if (equation.Vars.Any() || equation.Evaled is not Complex value || value.IsNaN)
                 return null;
@@ -201,30 +204,50 @@ Variable ParameterFor(int index)
         /// <c>0 provided not c = 0</c> for a <c>c</c> that is zero without being written
         /// <c>0</c>, such as <c>(a + 1)^2 - a^2 - 2a - 1</c>.
         /// </summary>
-        private static bool Vanishes(Entity expression)
+        /// <remarks>
+        /// A symbol in <paramref name="whole"/> stands for every whole number, so it is pinned at
+        /// one, and the expression is zero where it is zero for each: <c>sin(pi/6 + 2 pi n_1) - 1/2</c>
+        /// is decided as <c>forall n_1 in ZZ : sin(pi/6 + 2 pi n_1) - 1/2 = 0</c>, which takes the
+        /// whole periods out. https://github.com/asc-community/AngouriMath/issues/212
+        /// </remarks>
+        private static bool Vanishes(Entity expression, IReadOnlyList<Variable> 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 },
             };
         }
 
-        /// <summary><paramref name="expression"/> with each of its symbols at a fixed value.</summary>
-        private static Entity Pinned(Entity expression)
+        /// <summary>
+        /// <paramref name="expression"/> with each of its symbols at a fixed value, a whole one for
+        /// a symbol in <paramref name="whole"/>.
+        /// </summary>
+        private static Entity Pinned(Entity expression, IReadOnlyList<Variable> 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;
         }
     }

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);

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: <c>sqrt(t^2) - t</c> is zero at
-        /// every positive <c>t</c> and at no negative one.
+        /// every positive <c>t</c> and at no negative one. An <c>n_1</c>, which a periodic root
+        /// brings and which stands for a whole number, is sampled at whole numbers.
         /// </summary>
         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<Entity.Number.Complex>(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);
         }
 
+        /// <summary>
+        /// A family a periodic root brings a whole-number parameter to, <c>n_1</c>, which holds for
+        /// every whole <c>n_1</c> and is answered: <c>sin(x) = 1/2</c> in <c>x</c> and <c>y</c> is
+        /// the two families <c>(pi/6 + 2 pi n_1, t_1)</c> and <c>(pi - pi/6 + 2 pi n_1, t_1)</c>.
+        /// </summary>
+        [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);
+        }
+
         /// <summary>
         /// More equations than unknowns, which the triangularisation does not take because they
         /// are not polynomial. The last drops <c>x = -1</c>, where <c>sin(-pi/2) - 1</c> is -2.