Display not equals in Latexise, simplify Notf(Andf) and Notf(Orf)

Sources/AngouriMath/Convenience/MathS.cs

@@ -5575,7 +5575,7 @@ public sealed record NewtonSetting
                         // Weigh provided predicates much less but nested provideds heavy
                         Providedf(var inner, var predicate) =>
                             DefaultCriteria(inner) + 0.1 * DefaultCriteria(predicate) + ExtraHeavyWeight * (inner.Nodes.Count(n => n is Providedf) + predicate.Nodes.Count(n => n is Providedf)),
-                        Entity.Piecewise { Cases: var cases } =>
+                        Piecewise { Cases: var cases } =>
                             cases.Sum(@case =>
                                 DefaultCriteria(@case.Expression) + 0.1 * DefaultCriteria(@case.Predicate) + ExtraHeavyWeight * (@case.Expression.Nodes.Count(n => n is Providedf) + @case.Predicate.Nodes.Count(n => n is Providedf))),
                         Variable => Weight, // Number of variables
@@ -5586,6 +5586,7 @@ public sealed record NewtonSetting
                         Phif => ExtraHeavyWeight + expr.DirectChildren.Sum(DefaultCriteria), // Number of phi functions
                         Real { IsNegative: true } => MajorWeight + expr.DirectChildren.Sum(DefaultCriteria), // Number of negative reals
                         ComparisonSign when expr.DirectChildren[0] == 0 => Weight + expr.DirectChildren.Sum(DefaultCriteria), // 0 < x is bad. x > 0 is good.
+                        Notf (Equalsf eq) => -Weight + DefaultCriteria(eq), // (not x = 0) is equally complex as (x = 0)
                         _ => expr.DirectChildren.Sum(DefaultCriteria)
                     } + Weight; // Number of nodes
                     return DefaultCriteria(expr);

Sources/AngouriMath/Functions/Output/Latex/Latex.Discrete.Classes.cs

@@ -20,62 +20,58 @@ partial record Notf
         {
             /// <inheritdoc/>
             public override string Latexise()
-                => $@"\neg{{{Argument.Latexise(Argument.Priority < Priority)}}}";
+                => Argument is Equalsf(var left, var right)
+                   ? $@"{left.Latexise(left.Priority <= Priority.Equal)} \neq {right.Latexise(right.Priority <= Priority.Equal)}"
+                   : $@"\neg{{{Argument.Latexise(Argument.Priority < Priority)}}}";
         }
 
         partial record Andf
         {
             /// <inheritdoc/>
             public override string Latexise()
             {
-                // Detect patterns like (a < b) ∧ (b < c) ∧ (c < d) and returns the chain of comparisons
-                List<ComparisonSign>? comparisons = null;
-                void GatherComparisons(Entity e) // Recursively gather all comparisons connected by AND
+                var result = new System.Text.StringBuilder();
+                Entity? left = null;
+                bool first = true;
+                foreach (var child in LinearChildren(this))
                 {
-                    switch (e)
+                    switch (child)
                     {
-                        case Andf(var left, var right):
-                            GatherComparisons(left);
-                            GatherComparisons(right);
+                        // Detect chained comparisons like (a < b) ∧ (b < c) ∧ (c < d) and display as a < b < c < d
+                        case ComparisonSign:
+                            var renew = left != child.DirectChildren[0];
+                            if (!first && renew) result.Append(@" \land ");
+                            first = false;
+                            if (first || renew) result.Append(child.DirectChildren[0].Latexise(child.DirectChildren[0].Priority <= child.Priority));
+                            renew = false;
+                            result.Append(child switch {
+                                Equalsf => " = ",
+                                Greaterf => " > ",
+                                GreaterOrEqualf => @" \geq ",
+                                Lessf => " < ",
+                                LessOrEqualf => @" \leq ",
+                                _ => throw new Core.Exceptions.AngouriBugException("Unexpected comparison sign in Andf.Latexise")
+                            }).Append(child.DirectChildren[1].Latexise(child.DirectChildren[1].Priority <= child.Priority));
+                            left = child.DirectChildren[1];
                             break;
-                        case ComparisonSign comp:
-                            comparisons ??= [];
-                            comparisons.Add(comp);
+                        case Notf (Equalsf eq):
+                            renew = left != eq.Left;
+                            if (!first && renew) result.Append(@" \land ");
+                            first = false;
+                            if (first || renew) result.Append(eq.Left.Latexise(eq.Left.Priority <= eq.Priority));
+                            renew = false;
+                            result.Append(@" \neq ").Append(eq.Right.Latexise(eq.Right.Priority <= eq.Priority));
+                            left = eq.Right;
+                            break;
+                        default:
+                            if (!first) result.Append(" \\land ");
+                            left = null;
+                            first = false;
+                            result.Append(child.Latexise(child.Priority < Priority));
                             break;
                     }
                 }
-                GatherComparisons(this);
-
-                // Check if comparisons form a valid chain: right side of each must equal left side of next
-                if (comparisons is { Count: >= 2 })
-                    for (int i = 0; i < comparisons.Count - 1; i++)
-                        if (comparisons[i].DirectChildren[1] != comparisons[i + 1].DirectChildren[0])
-                            goto fallback; // Not a valid chain
-
-                // Try to detect chained comparisons: (a < b) ∧ (b < c) → a < b < c
-                if (comparisons is { Count: > 1 } chain)
-                {
-                    var result = new System.Text.StringBuilder(chain[0].DirectChildren[0].Latexise(chain[0].DirectChildren[0].Priority < chain[0].Priority));
-                    foreach (var comparison in chain)
-                    {
-                        var op = comparison switch
-                        {
-                            Equalsf => " = ",
-                            Greaterf => " > ",
-                            GreaterOrEqualf => @" \geq ",
-                            Lessf => " < ",
-                            LessOrEqualf => @" \leq ",
-                            _ => null
-                        };
-                        if (op is null)
-                            goto fallback;
-                        result.Append(op).Append(comparison.DirectChildren[1].Latexise(comparison.DirectChildren[1].Priority < comparison.Priority));
-                    }
-                    return result.ToString();
-                }
-
-            fallback:
-                return $@"{Left.Latexise(Left.Priority < Priority)} \land {Right.Latexise(Right.Priority < Priority)}";
+                return result.ToString();
             }
         }
 

Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs

@@ -5,6 +5,7 @@
 // Website: https://am.angouri.org.
 //
 
+using HonkSharp.Functional;
 using static AngouriMath.Entity;
 using static AngouriMath.Entity.Boolean;
 
@@ -13,7 +14,7 @@ namespace AngouriMath.Functions
     internal static partial class Patterns
     {
         private static bool IsLogic(Entity a)
-            => a is Statement or Variable;
+            => a is Statement or Variable or Providedf;
 
         private static bool IsLogic(Entity a, Entity b)
             => IsLogic(a) && IsLogic(b);
@@ -23,19 +24,19 @@ private static bool IsLogic(Entity a, Entity b, Entity c)
 
         internal static Entity BooleanRules(Entity x) => x switch
         {
-            Impliesf(var ass, _) when ass == False && IsLogic(ass) => True,
+            Impliesf(var ass, var other) when ass == False && IsLogic(other) => True.Provided(other.DomainCondition),
             Andf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 | any2),
             Orf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 & any2),
             Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True,
             Orf(Notf(var any1), var any2) when IsLogic(any1, any2) => any1.Implies(any2),
             Andf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
             Orf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
             Impliesf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => True,
-            Xorf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => False,
+            Xorf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => False.Provided(any1.DomainCondition),
             Notf(Notf(var any1)) when IsLogic(any1) => any1,
 
-            Orf(var any1, var any2) when (any1 == True || any2 == True) && IsLogic(any1, any2) => True,
-            Andf(var any1, var any2) when (any1 == False || any2 == False) && IsLogic(any1, any2) => False,
+            Orf(var any1, var any2) when (any1 == True || any2 == True) && IsLogic(any1, any2) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition),
+            Andf(var any1, var any2) when (any1 == False || any2 == False) && IsLogic(any1, any2) => False.Provided(any1.DomainCondition).Provided(any2.DomainCondition),
 
             Orf(Andf(var any1, var any2), Andf(var any1a, var any3)) when any1 == any1a && IsLogic(any1, any2, any3) => any1 & (any2 | any3),
             Andf(Orf(var any1, var any2), Orf(var any1a, var any3)) when any1 == any1a && IsLogic(any1, any2, any3) => any1 | (any2 & any3),

Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs

@@ -5,8 +5,10 @@
 // Website: https://am.angouri.org.
 //
 
+using System;
 using static AngouriMath.Entity;
 using static AngouriMath.Entity.Boolean;
+using static Antlr4.Runtime.Atn.SemanticContext;
 
 namespace AngouriMath.Functions
 {
@@ -55,12 +57,20 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right)
             Notf(Lessf(var any1, var any2)) => any1 >= any2,
             Notf(GreaterOrEqualf(var any1, var any2)) => any1 < any2,
             Notf(LessOrEqualf(var any1, var any2)) => any1 > any2,
+            // If we have a bunch of comparison operators combined with AND/OR and NOT outside, we can push the NOT inside and flip all the operators.
+            // For complexity to not increase, maximum one AND/OR component can be something other than a comparison operator to propagate NOT into.
+            // e.g. not (a > b and b = c) becomes (a <= b or not b = c)
+            // Note that Notf(Equalsf) has the same complexity as Equalsf in ComplexityCriteria, so it can be treated as a comparison operator here.
+            Notf(Andf a) when Andf.LinearChildren(a).Count(n => n is not (ComparisonSign or Notf or Orf)) <= 1 =>
+                Andf.LinearChildren(a).Select(e => InequalityEqualityRules(e switch { Notf(var n) => n, var n => new Notf(n) })).Aggregate((a, b) => a | b),
+            Notf(Orf a) when Orf.LinearChildren(a).Count(n => n is not (ComparisonSign or Notf or Andf)) <= 1 =>
+                Orf.LinearChildren(a).Select(e => InequalityEqualityRules(e switch { Notf(var n) => n, var n => new Notf(n) })).Aggregate((a, b) => a & b),
 
             Impliesf(Andf(Greaterf(var any1, var any2), Greaterf(var any2a, var any3)), Greaterf(var any1a, var any3a))
-                when any1 == any1a && any2 == any2a && any3 == any3a => True,
+                when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),
 
             Impliesf(Andf(Lessf(var any1, var any2), Lessf(var any2a, var any3)), Lessf(var any1a, var any3a))
-                when any1 == any1a && any2 == any2a && any3 == any3a => True,
+                when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),
 
             Equalsf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero.Equalizes(zero),
             Greaterf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero < zero,
@@ -129,10 +139,10 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right)
             // a! = 0
             Equalsf(Factorialf({ DomainCondition: var condition }), var zeroEnt) when IsZero(zeroEnt) => False.Provided(condition),
 
-            Greaterf(var any1, var any1a) when any1 == any1a => false,
-            Lessf(var any1, var any1a) when any1 == any1a => false,
-            GreaterOrEqualf(var any1, var any1a) when any1 == any1a => true,
-            LessOrEqualf(var any1, var any1a) when any1 == any1a => true,
+            Greaterf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition),
+            Lessf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition),
+            GreaterOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition),
+            LessOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition),
 
             _ => x
         };

Sources/Tests/UnitTests/Convenience/LatexTest.cs

@@ -49,7 +49,7 @@ void TestSimplify(string expected, Entity actual) =>
         [Fact] public void MultiplySimplify() => TestSimplify("{x}^{2}", x * x);
         [Fact] public void Divide() => Test(@"\frac{x}{x}", x / x);
         [Fact] public void DivideDivide() => Test(@"\frac{\frac{x}{x}}{x}", x / x / x);
-        [Fact] public void DivideSimplify() => TestSimplify(@"1 \quad \text{for} \quad \neg{x = 0}", x / x);
+        [Fact] public void DivideSimplify() => TestSimplify(@"1 \quad \text{for} \quad x \neq 0", x / x);
         [Fact] public void Greek1() => Test(@"\alpha", MathS.Var("alpha"));
         [Fact] public void Greek2() => Test(@"\beta", MathS.Var("beta"));
         [Fact] public void Greek3() => Test(@"a_{\beta}", MathS.Var("a_beta"));
@@ -631,13 +631,17 @@ [Fact] public void EqualityInequalityChain()
             => Test(@"x \geq y = z < w",
                 (x >= MathS.Var("y")) & (MathS.Var("y").Equalizes(MathS.Var("z"))) & (MathS.Var("z") < MathS.Var("w")));
         [Fact] public void EqualityInequalityChainAlt() => Test(@"x \geq y = z < w", (x >= "y").Equalizes("z") < "w");
-        [Fact] public void EqualityInequalityChainString() => Test(@"x \geq y = z < w", (Entity)"x>=y=z<w");
+        [Fact] public void EqualityInequalityChainString() => Test(@"x \geq y = z < w", (Entity)"(x>=y=z)<w");
+        [Fact] public void EqualityInequalityChainStringBug() => Test(@"x \geq y = \left(z < w\right)", (Entity)"x>=y=z<w"); // TODO: why does it parse this way? it's supposed to parse like the above test.
         [Fact] public void EqualityInequalityChainParenthesized() => Test(@"x \geq \left(y = \left(z < w\right)\right)", new Entity.GreaterOrEqualf(x, new Entity.Equalsf("y", (Entity)"z" < "w")));
         [Fact] public void ParenthesizedComparisons()
             => Test(@"\left(x < x\right) \geq \left(x > \left(\left(x = x\right) \leq x\right)\right)",
 #pragma warning disable 1718 // Disable self-comparison warning
                 new Entity.GreaterOrEqualf(x < x, (x > new Entity.LessOrEqualf(new Entity.Equalsf(x, x), x))));
 #pragma warning restore 1718
+        [Fact] public void NotEqual() => Test(@"1 \neq 2", (Entity)"not 1 = 2");
+        [Fact] public void ChainedNotEqual() => Test(@"1 \neq 2 \neq 3 = 4 \land 5", (Entity)"not 1 = 2 and not 2 = 3 and 3 = 4 and 5");
+        [Fact] public void MixedChainedComparison() => Test(@"1 \land 2 > 3 < 4 \land \left(\top  \lor \bot \right) \land 5 \neq x = x \land x", (Entity)"1 and 2 > 3 and 3 < 4 and (true or false) and not 5 = x and x = x and x");
         [Fact] public void ImpliesChain()
             => Test(@"\left(\left(x \to y\right) \to z\right) \to x \to y \to z", x.Implies("y").Implies("z").Implies(x.Implies(MathS.Var("y").Implies("z"))));
     }

Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs

@@ -127,5 +127,26 @@ public void TestProvided(string expr, string? expected)
             var act = expr.ToEntity();
             Assert.Equal(exp, act.Simplify());
         }
+        [Theory]
+        [InlineData("not (not x)", "x")]
+        [InlineData("not (a = b and b = c)", "not a = b or not b = c")]
+        [InlineData("not (a <= b and b < c)", "a > b or b >= c")]
+        [InlineData("not (a > b and b >= c)", "a <= b or b < c")]
+        [InlineData("not (a <= b and b <= c and 1)", "not (1 and a <= b and b <= c)")]
+        [InlineData("not (a = b or b = c)", "not a = b and not b = c")]
+        [InlineData("not (a <= b or b < c)", "a > b and b >= c")]
+        [InlineData("not (a > b or b >= c)", "a <= b and b < c")]
+        [InlineData("not (a <= b or b <= c or 1)", "not (1 or a <= b or b <= c)")]
+        [InlineData("not (a < b or c > d and e = f)", "a >= b and (c <= d or not e = f)")]
+        [InlineData("not (not (a > b and b >= c) and y)", "a > b and b >= c or not y")]
+        [InlineData("not (not (a = b and b = c) and y)", "a = b and b = c or not y")]
+        [InlineData("not (not (not a = b and not b = c) and y)", "not ((a = b or b = c) and y)")]
+        [InlineData("not (a < b and b < c and not c = d and not d and not (e and not (f or g = h)))", "a >= b or b >= c or c = d or d or e and not f and not g = h")]
+        public void NestedNot(string expr, string expected)
+        {
+            var exp = expected.ToEntity();
+            var act = expr.ToEntity();
+            Assert.Equal(exp, act.Simplify());
+        }
     }
 }

Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs

@@ -48,7 +48,7 @@ [Fact] public void Patt2() => AssertSimplify(
         [Fact] public void Patt9() => AssertSimplify(MathS.Arccotan(x * 3) + MathS.Arctan(x * 6), MathS.Arccotan(3 * x) + MathS.Arctan(6 * x));
         [Fact] public void Patt10() => AssertSimplify(MathS.Arcsin(x * 3) + MathS.Arccos(x * 1), MathS.Arcsin(3 * x) + MathS.Arccos(x));
         [Fact] public void Patt11() => AssertSimplify(3 + x + 4 + x, 7 + 2 * x);
-        [Fact] public void Patt12() => AssertSimplify((x * y * a * b * c) / (c * b * a * x * x), "y / x provided not (c = 0 or a * b * c * x ^ 2 = 0)", 4);
+        [Fact] public void Patt12() => AssertSimplify((x * y * a * b * c) / (c * b * a * x * x), "y / x provided not c = 0 and not a * b * c * x ^ 2 = 0", 4);
         [Fact] public void Frac1() => AssertSimplify("x / (y / z)", "x * z / y");
         [Fact] public void Frac2() => AssertSimplify("x / y / z", "x / (y * z)");
         [Fact] public void Factorial2() => AssertSimplify(MathS.Factorial(2), 2);

Sources/Tests/UnitTests/PatternsTest/SortSimplifyTest.cs

@@ -21,7 +21,7 @@ public sealed class SortSimplifyTest
         // [InlineData("sin(arcsin(c x) + arccos(x c) + c)2 + a + b + sin(x) + 0 + cos(c - -arcsin(c x) - -arccos(-c x * (-1)))2", "1")]
         // [InlineData("sin(arcsin(c x) + arccos(x c) + c)2 + a + b + sin(x) + 0 + cos(c - -arcsin(c x) - -arccos(-c x * (-1)))2", ") ^ 2", false)]
         [InlineData("sec(x) + a + sin(x) + c + 1 + 0 + 3 + sec(x)", "4 + 2 * sec(x) + sin(x) + a + c")]
-        [InlineData("tan(x) * a * b / c / sin(h + 0.1) * cotan(x)", "a * b / (sin(h + 1/10) * c) provided not (sin(x) = 0 or cos(x) = 0)")]
+        [InlineData("tan(x) * a * b / c / sin(h + 0.1) * cotan(x)", "a * b / (sin(h + 1/10) * c) provided not sin(x) = 0 and not cos(x) = 0")]
         [InlineData("sin(x) * a * b / c / sin(h + 0.1) * cosec(x)", "a * b / (sin(h + 1/10) * c) provided not sin(x) = 0")]
         [InlineData("cos(x) * a * b / c / sin(h + 0.1) * sec(x)", "a * b / (sin(h + 1/10) * c) provided not cos(x) = 0")]
         [InlineData("sec(x) * a * b / c / sin(h + 0.1) * cos(x)", "a * b / (sin(h + 1/10) * c) provided not cos(x) = 0")]