From df10f73efa44cb39354ac2db0c8d0f0f2ca16bc2 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Mon, 21 Sep 2026 06:01:27 +0000 Subject: [PATCH] Solve reads a membership, and no longer answers the empty set for a statement it cannot read "x^2 in (0; 1)".Solve("x") was {} -- and so was every f(x) in S with anything but a bare x on the left, and every statement the solver had no arm for: the arm at the end of the dispatch answered the empty set, a claim that there is no such x. A membership is solved now: the members of a listed set each as an equation, an interval as its bounds, each strict or not as the end is; and a statement that is not read is the set of x with the property, left as written, which is not a claim. A quantifier that put the negated body to the solver read that emptiness as a proof: forall x in RR : x^2 in ZZ was True, and is False, by the witness 1/2. On the way, the subset decision reads membership of a union, an intersection and a difference as the connectives they are, so that the solver's answer to x^2 in (0; 1), ((-oo; 0) \/ (0; +oo)) /\ (-1; 1), is compared with (-1; 0) \/ (0; 1) as a set. The reference's pre-images (Sullivan and Mackey, Ex 7.3.10) are the rows; the book prints (-1, 1) for the pre-image of (0, 1) under x^2, which is wrong at 0. https://github.com/asc-community/AngouriMath/issues/1409 Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- BREAKING-CHANGES.md | 18 +++++ Sources/.editorconfig | 3 + .../Entity/Omni/Sets/SetOperators.Subset.cs | 7 ++ .../Solvers/EquationSolver/SolveStatement.cs | 45 +++++++++++- .../Algebra/MembershipSolvingTest.cs | 69 +++++++++++++++++++ 5 files changed, 140 insertions(+), 2 deletions(-) create mode 100644 Sources/Tests/UnitTests/Algebra/MembershipSolvingTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 0f49076de..3b5554cf4 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -656,6 +656,24 @@ with the multiplier gathered from the whole product in the exponent | `"e^(2*acoth(2*x))*(3 - 12*x^2)^2".Integrate("x")` | `integral(…)` — left unevaluated | `(144 * x ^ 5 / 5 + 144 * x ^ 4 / 4 + (-36) * x ^ 2 / 2 + (-9) * x provided not 2 * x + -1 = 0) + C` | | `"e^(1/3*acoth(x))*x^2".Integrate("x")` | `integral(…)` — left unevaluated | an antiderivative in `((x + 1)/(x - 1))^(1/6)` | +### `Solve` no longer answers the empty set for a statement it cannot read + +**Wrong answer fixed.** `"x^2 in (0; 1)".Solve("x")` was `{}` — and so was every `f(x) in S` with +anything but a bare `x` on the left, and every statement the solver had no arm for: the arm at the +end of the dispatch answered the empty set, which claims there is no such `x`. A membership is +solved now — the members of a listed set each as an equation, an interval as its bounds, each +strict or not as the end is — and a statement that is not read is the set of `x` with the +property, left as written. A quantifier that put the negated body to the solver read that +emptiness as a proof: `forall x in RR : x^2 in ZZ` was `True` +([#1409](https://github.com/asc-community/AngouriMath/issues/1409), the reference's pre-images). + +| Input | Was (2.5.0) | Now | +|---|---|---| +| `"x^2 in (0; 1)".Solve("x")` | `{}` — wrong | `((-oo; 0) \/ (0; +oo)) /\ (-1; 1)` | +| `"x^2 in {1, 4}".Solve("x")` | `{}` — wrong | `{ 1, -1, 2, -2 }` | +| `"x^2 in ZZ".Solve("x")` | `{}` — wrong | `{ x : x ^ 2 in ZZ }`, left as written | +| `forall x in RR : x^2 in ZZ` | `UnhandledParseException` (quantifiers are new since) | `False` | + ### `binomial(n, k)` is a function **Addition, not silent.** The binomial coefficient is a node, `Entity.Binomialf`, spelled diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 07869921d..047575201 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -291,6 +291,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [AngouriMath/Functions/NumberTheory/ResidueClasses.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/Algebra/MembershipSolvingTest.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/Sets/IndexedSetOperationTest.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/Core/Entity/Omni/Sets/SetOperators.Subset.cs b/Sources/AngouriMath/Core/Entity/Omni/Sets/SetOperators.Subset.cs index 623d7412b..475b4098a 100644 --- a/Sources/AngouriMath/Core/Entity/Omni/Sets/SetOperators.Subset.cs +++ b/Sources/AngouriMath/Core/Entity/Omni/Sets/SetOperators.Subset.cs @@ -223,6 +223,13 @@ internal static partial class SetOperators var over = sub is ConditionalSet { DeclaredMembership: (var declared, _) } ? declared as Set : sub; switch (super) { + // The operators are the connectives: x in A \/ B is x in A or x in B. + case Unionf(Set a, Set b): + return MembershipAsComparison(x, a, sub) is { } inA && MembershipAsComparison(x, b, sub) is { } inB ? inA | inB : null; + case Intersectionf(Set a, Set b): + return MembershipAsComparison(x, a, sub) is { } inBoth && MembershipAsComparison(x, b, sub) is { } andIn ? inBoth & andIn : null; + case SetMinusf(Set a, Set b): + return MembershipAsComparison(x, a, sub) is { } inLeft && MembershipAsComparison(x, b, sub) is { } notIn ? inLeft & !notIn : null; case ConditionalSet { DeclaredMembership: (var declaredOfSuper, var rest), Var: Variable y } builder when declaredOfSuper is Set declaredSet: // x in { y in S : p } is x in S and p(x); the first conjunct is read the diff --git a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs index 77af2804d..2c73f591d 100644 --- a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs +++ b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs @@ -12,6 +12,7 @@ using PeterO.Numbers; using AngouriMath.Functions.Continuous.Solvers.SetSolver; using static AngouriMath.Entity; +using static AngouriMath.Entity.Number; using static AngouriMath.Entity.Set; namespace AngouriMath.Functions.Algebra.AnalyticalSolving @@ -319,6 +320,11 @@ internal static Set Solve(Entity expr, Variable x) Variable when expr == x => new FiniteSet(true), Inf(var var, Set set) when var == x => set, + // f(x) in S: the members of a listed S each as an equation, an interval as its + // two bounds, and anything else left as the set of x with the property, since + // a solver that answered "no x" here was answering wrongly -- x^2 in (0; 1) was + // the empty set. https://github.com/asc-community/AngouriMath/issues/1409 + Inf(var member, Set set) when member.ContainsNode(x) => Membership(member, set, x) ?? new ConditionalSet(x, expr), // a x + b = c (mod n): one residue class, or none, by the gcd; a congruence of // higher degree by the residues that satisfy it, where the modulus is small @@ -328,8 +334,43 @@ internal static Set Solve(Entity expr, Variable x) Providedf(var e, var predicate) => Solve(e, x).Filter(predicate, x), Piecewise p => EquationSolver.SolvePiecewise(p, x, Solve), - // TODO: Although piecewise needed? - _ => Set.Empty + // A statement the solver has no arm for is the set of x with the property, left + // as written -- not the empty set, which claims there is no such x. A statement + // that does not mention x is one of everything or of nothing, and the set + // builder over it evaluates to that. + _ => new ConditionalSet(x, expr) }; + + /// + /// The x with f(x) in a set: for a listed set, the union of the equations + /// f(x) = s; for an interval, the conjunction of its bounds, each strict or not as + /// the end is; for a set that is neither. + /// + private static Set? Membership(Entity member, Set set, Variable x) + { + switch (set) + { + case FiniteSet listed: + Set? union = null; + foreach (var element in listed) + { + var solutions = Solve(member.Equalizes(element), x); + union = union is null ? solutions : MathS.Union(union, solutions); + } + return union ?? Set.Empty; + case Interval interval: + Entity? condition = null; + if (interval.Left.Evaled != Real.NegativeInfinity) + condition = interval.LeftClosed ? member >= interval.Left : member > interval.Left; + if (interval.Right.Evaled != Real.PositiveInfinity) + { + var upper = interval.RightClosed ? member <= interval.Right : member < interval.Right; + condition = condition is null ? upper : condition & upper; + } + return condition is null ? MathS.Sets.R : Solve(condition, x); + default: + return null; + } + } } } diff --git a/Sources/Tests/UnitTests/Algebra/MembershipSolvingTest.cs b/Sources/Tests/UnitTests/Algebra/MembershipSolvingTest.cs new file mode 100644 index 000000000..93a66654d --- /dev/null +++ b/Sources/Tests/UnitTests/Algebra/MembershipSolvingTest.cs @@ -0,0 +1,69 @@ +// +// 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.Algebra +{ + /// + /// Solve of f(x) in S: the members of a listed S each as an equation, + /// an interval as its bounds. It answered the empty set for every one of these, and + /// for every statement it had no arm for -- a claim that no x exists, made about + /// x^2 in (0; 1). A statement the solver cannot read is the set of x with the + /// property now, left as written. The reference's pre-images (Sullivan and Mackey, + /// Ex 7.3.10, §7.3.5 Try 1) are this. + /// + /// + [Trait("Area", "Algebra")] + public sealed class MembershipSolvingTest + { + private static Set Solved(string statement) => statement.ToEntity().Solve("x"); + + /// Ex 7.3.10: the pre-images of x^2; the book prints (-1, 1) for the last, which is wrong at 0. + [Theory] + [InlineData("x^2 in {1}", "{-1, 1}")] + [InlineData("x^2 in {1, 4}", "{-2, -1, 1, 2}")] + [InlineData("x^2 in (-oo; 0)", "{}")] + [InlineData("x^2 in [0; +oo)", "RR")] + [InlineData("x^2 in (0; 1)", "(-1; 0) \\/ (0; 1)")] + [InlineData("x + 1 in [2; 3]", "[1; 2]")] + [InlineData("2 x in (0; 4]", "(0; 2]")] + public void APreImageIsSolvedThroughTheMembersOrTheBounds(string statement, string expected) + { + // Compared at points rather than as printed forms: the solver writes a union of + // intervals in its own order, and the same set two ways is the same set. + var solved = Solved(statement); + var wanted = (Set)expected.ToEntity().Evaled; + foreach (var at in new[] { -3.0, -2.0, -1.0, -0.5, 0.0, 0.5, 1.0, 1.5, 2.0, 3.0 }) + { + var point = (Entity)at; + Assert.True(solved.TryContains(point, out var got), $"{solved} does not decide {at}"); + Assert.True(wanted.TryContains(point, out var want), $"{wanted} does not decide {at}"); + Assert.True(got == want, $"{statement} solved as {solved}: {at} is {(got ? "in" : "out")}, and should be {(want ? "in" : "out")}"); + } + } + + /// A statement with no arm is the set of x with the property, not the empty set. + [Fact] + public void WhatIsNotReadIsLeftAsWritten() + { + Assert.Equal("{ x : x^2 in ZZ }".ToEntity(), Solved("x^2 in ZZ")); + Assert.Equal("{ x : x^2 in QQ }".ToEntity(), Solved("x^2 in QQ")); + // And a quantifier that asked the solver no longer reads that emptiness as a proof: + // forall x in RR : x^2 in ZZ was True. + Assert.Equal(Boolean.False, "forall x in RR : x^2 in ZZ".ToEntity().Evaled); + } + + /// The trigonometric equation's family is the pre-image of {0} under the sine. + [Fact] + public void AMemberEquationKeepsItsFamily() + => Assert.Contains("n_1", Solved("sin(x) in {0}").Stringize()); + } +}