A negation is no longer answered with the empty set (#1127)

BREAKING-CHANGES.md

@@ -59,6 +59,8 @@ read first.
 | **Silent** | `"-1 * (y mod z)".ToEntity().Stringize()` | `-y mod z` | `-(y mod z)` |
 | | any expression mixing a number with a `Complex` argument, `Compile`d in a NativeAOT app — `"x + 1".Compile<Complex, Complex>("x")` | `UncompilableNodeException: ... The binary operator Add is not defined for the types 'System.Numerics.Complex' and 'System.Numerics.Complex'` | the compiled function, answering as it does under the JIT |
 | | `Compile` to a nullable integral return type in a NativeAOT app | `AngouriBugException: IsNaN method expected for type System.Double`, which took the process down | the compiled function |
+| **Silent** | `"not (x = 1)".ToEntity().Solve("x")`, and every negation | `{  }` — no value satisfies it | `{ x : not x = 1 }` |
+| **Silent** | `"not (x > 1)".ToEntity().Solve("x")`, and every negated comparison | `{  }` | `(-oo; 1]` |
 | **Silent** | `"(x = 1) implies (x = 2)".ToEntity().Solve("x")`, and every implication | `{ 2 } \/ BB` — truth values in the solution set of a numeric question | `{ x : not x = 1 }` |
 | | `"domain((-oo; +oo), Any) = RR".ToEntity().Solve("x")`, and every unbounded interval widened to `Any` | `NotSufficientlySupportedException: There is no special set for domain Any` | `{  }` |
 | **Silent** | an app publishing with `PublishTrimmed` or NativeAOT | `AngouriMath.dll` was copied in whole, being unmarked | it is trimmed with the rest, since the assembly now declares `IsTrimmable` |
@@ -307,6 +309,42 @@ was nothing to take.
 `Transformation.NumericContentExtraction` is the step on its own, and `Transformation.Factorization`'s
 `Name` gains it — a chain names its parts.
 
+### A negation is no longer answered with the empty set
+
+`StatementSolver.Solve` had arms for equality, the connectives, the four comparisons, membership,
+`provided` and `piecewise` — and none for `not`, so every negation fell through to `Set.Empty`.
+The empty set is a positive claim, *no x satisfies this*, and it was false of all of them
+([#1127](https://github.com/asc-community/AngouriMath/issues/1127)). This is the defect
+[#1036](https://github.com/asc-community/AngouriMath/issues/1036) fixed for equations, left
+standing for negation.
+
+**Was** — every one of these, and 1 is not a solution of the first while 0 is:
+
+```
+"not (x = 1)".ToEntity().Solve("x")             {  }
+"not (x > 1)".ToEntity().Solve("x")             {  }
+"not (x >= 1)".ToEntity().Solve("x")            {  }
+"not not (x = 1)".ToEntity().Solve("x")         {  }
+"not (x > 1 or x < -1)".ToEntity().Solve("x")   {  }
+"not (x in RR)".ToEntity().Solve("x")           {  }
+```
+
+**Is** — the negation pushed inward as far as there is an arm for it, and named as a set-builder
+where there is not:
+
+```
+"not (x = 1)".ToEntity().Solve("x")             { x : not x = 1 }
+"not (x > 1)".ToEntity().Solve("x")             (-oo; 1]
+"not (x >= 1)".ToEntity().Solve("x")            (-oo; 1)
+"not not (x = 1)".ToEntity().Solve("x")         { 1 }
+"not (x > 1 or x < -1)".ToEntity().Solve("x")   [-1; 1]
+"not (x in RR)".ToEntity().Solve("x")           { x : not x in RR }
+```
+
+A negated comparison is answered as the comparison it is, which is what
+`RewriteRules.InequalityEquality` already says; a negated connective is pushed inward by De Morgan,
+which is the direction that reaches an arm. What neither reaches is answered as written.
+
 ### An implication is solved without naming a universe
 
 `Solve` answered `a implies b` with `Codomain \ solve(a) \/ solve(b)`, taking the complement

Sources/.editorconfig

@@ -134,3 +134,6 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed
 
 [Tests/UnitTests/Core/Sets/DomainAnyIsNotAUniversalSetTest.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/SolveTest/NegationIsNotTheEmptySetTest.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/Continuous/Solvers/EquationSolver/SolveStatement.cs

@@ -148,6 +148,55 @@ private static EDecimal LargestTerm(Entity substituted)
             return largest;
         }
 
+        /// <summary>
+        /// What <c>not a</c> is as a statement about <paramref name="x"/>: the negation pushed
+        /// inward as far as there is an arm for it, and named as a set-builder where there is not.
+        /// </summary>
+        /// <remarks>
+        /// <para>
+        /// There was no arm for <see cref="Notf"/> at all, so every negation fell to
+        /// <see cref="Set.Empty"/> — <c>not (x = 1)</c>, <c>not (x &gt; 1)</c> and
+        /// <c>not (x in RR)</c> each answered "no x satisfies this", which is a positive claim and
+        /// false of all three. That is the defect
+        /// <a href="https://github.com/asc-community/AngouriMath/issues/1036">#1036</a> fixed for
+        /// equations, left standing for negation.
+        /// <a href="https://github.com/asc-community/AngouriMath/issues/1127">#1127</a>
+        /// </para>
+        /// <para>
+        /// Pushing the negation inward is unambiguous <i>here</i> in a way it is not in the
+        /// simplifier, which is why it is done here and not as a rule: this switch has arms for
+        /// the connectives and for the comparisons and none for <c>not</c>, so inward is the
+        /// direction that reaches one. A negated comparison is a comparison, and
+        /// <see cref="Core.Transformations.RewriteRules.InequalityEquality"/> is where that is
+        /// already written down — asking it rather than restating it keeps the two from drifting.
+        /// </para>
+        /// <para>
+        /// What is left over is answered as written rather than as nothing: <c>not (x in RR)</c>
+        /// is <c>{ x : not x in RR }</c>, which names the non-real complex numbers exactly and
+        /// asserts of them only that they are what the statement says.
+        /// </para>
+        /// </remarks>
+        private static Set Negation(Entity statement, Entity operand, Variable x)
+        {
+            switch (operand)
+            {
+                // not not a = a
+                case Notf(var inner):
+                    return Solve(inner, x);
+                // De Morgan, in the direction that reaches an arm.
+                case Andf(var left, var right):
+                    return (Set)MathS.Union(Solve(!left, x), Solve(!right, x));
+                case Orf(var left, var right):
+                    return Conjunction(Solve(!left, x), Solve(!right, x), statement, x);
+            }
+
+            var asAComparison = Core.Transformations.RewriteRules.InequalityEquality.ApplyOnce(statement);
+            if (asAComparison is not Notf)
+                return Solve(asAComparison, x);
+
+            return new ConditionalSet(x, statement);
+        }
+
         /// <summary>
         /// <c>a implies b</c> holds where <c>a</c> fails or where <c>b</c> holds, and the first
         /// half of that is a set-builder rather than a complement.
@@ -216,6 +265,7 @@ internal static Set Solve(Entity expr, Variable x)
                 Orf(var left, var right) => 
                     MathS.Union(Solve(left, x), Solve(right, x)),
                 Impliesf(var left, var right) => Implication(left, right, x),
+                Notf(var operand) => Negation(expr, operand, x),
 
                 Greaterf(var left, var right) => 
                     AnalyticalInequalitySolver.Solve(Minus(left, right), x),

Sources/Tests/UnitTests/Algebra/SolveTest/NegationIsNotTheEmptySetTest.cs

@@ -0,0 +1,107 @@
+//
+// 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;
+using static AngouriMath.Entity.Set;
+
+namespace AngouriMath.Tests.Algebra.SolveTest
+{
+    /// <summary>
+    /// The statement solver had no arm for <see cref="Notf"/>, so every negation fell to
+    /// <see cref="Set.Empty"/> — a positive claim that no value satisfies the statement.
+    /// <a href="https://github.com/asc-community/AngouriMath/issues/1127">#1127</a>
+    /// </summary>
+    /// <remarks>
+    /// These assert what the answers <b>mean</b> — which values are in the set and which are not
+    /// — rather than the shape they are written in, so that a later rewrite that says the same
+    /// thing better does not fail them.
+    /// </remarks>
+    [Trait("Area", "Algebra")]
+    public sealed class NegationIsNotTheEmptySetTest
+    {
+        private static Set Solve(string statement) => statement.ToEntity().Solve("x");
+
+        /// <summary>The defect: none of these is unsatisfiable, so none of them is empty.</summary>
+        [Theory]
+        [InlineData("not (x = 1)")]
+        [InlineData("not (x > 1)")]
+        [InlineData("not (x >= 1)")]
+        [InlineData("not (x < 1)")]
+        [InlineData("not (x in RR)")]
+        [InlineData("not not (x = 1)")]
+        [InlineData("not (x = 1 and x = 2)")]
+        [InlineData("not (x = 1 or x = 2)")]
+        public void ASatisfiableNegationIsNotTheEmptySet(string statement)
+        {
+            var solutions = Solve(statement);
+            Assert.False(solutions.IsSetEmpty, $"{statement} has solutions");
+            Assert.NotEqual((Entity)Set.Empty, (Entity)solutions);
+        }
+
+        /// <summary>
+        /// A negated comparison is a comparison, and answering it as one is what
+        /// <see cref="Core.Transformations.RewriteRules.InequalityEquality"/> already says.
+        /// </summary>
+        [Theory]
+        [InlineData("not (x > 1)", "x <= 1")]
+        [InlineData("not (x >= 1)", "x < 1")]
+        [InlineData("not (x < 1)", "x >= 1")]
+        [InlineData("not (x <= 1)", "x > 1")]
+        [InlineData("not not (x = 1)", "x = 1")]
+        public void ANegatedComparisonIsSolvedAsTheComparisonItIs(string negated, string same)
+            => Assert.Equal(Solve(same), Solve(negated));
+
+        /// <summary>
+        /// De Morgan, in the direction that reaches an arm: the negation of a conjunction is the
+        /// union of the negations, and of a disjunction the intersection.
+        /// </summary>
+        [Theory]
+        [InlineData("not (x > 1 or x < -1)", "x <= 1 and x >= -1")]
+        [InlineData("not (x > 1 and x > 2)", "x <= 1 or x <= 2")]
+        public void ANegatedConnectiveIsPushedInward(string negated, string same)
+            => Assert.Equal(Solve(same), Solve(negated));
+
+        /// <summary>
+        /// And the answers are right about individual values, which is what "not empty" alone
+        /// does not establish.
+        /// </summary>
+        [Theory]
+        [InlineData("not (x = 1)", 2, true)]
+        [InlineData("not (x = 1)", 1, false)]
+        [InlineData("not (x > 1)", 0, true)]
+        [InlineData("not (x > 1)", 5, false)]
+        [InlineData("not (x > 1)", 1, true)]
+        [InlineData("not (x >= 1)", 1, false)]
+        [InlineData("not (x > 1 or x < -1)", 0, true)]
+        [InlineData("not (x > 1 or x < -1)", 3, false)]
+        [InlineData("not (x = 1 or x = 2)", 3, true)]
+        [InlineData("not (x = 1 or x = 2)", 2, false)]
+        public void ANegationsAnswerDecidesTheRightValues(string statement, int value, bool expected)
+        {
+            Assert.True(Solve(statement).TryContains(value, out var contains),
+                $"membership of {value} in the answer to {statement} is decidable");
+            Assert.Equal(expected, contains);
+        }
+
+        /// <summary>
+        /// What no arm reaches is answered as written rather than as nothing:
+        /// <c>{ x : not x in RR }</c> names the non-real complex numbers exactly.
+        /// </summary>
+        [Fact]
+        public void AnUnreachedNegationIsAnsweredAsWritten()
+        {
+            var solutions = Solve("not (x in RR)");
+            Assert.IsType<ConditionalSet>(solutions);
+            Assert.True(solutions.TryContains("i".ToEntity(), out var nonReal) && nonReal);
+            Assert.True(solutions.TryContains(3, out var real));
+            Assert.False(real);
+        }
+    }
+}