Carry the condition an order comparison is decided under (#876), and read a set-builder's predicate inside its binder (#878)

Sources/AngouriMath/Core/Entity/Omni/Entity.Omni.Classes.cs

@@ -447,8 +447,19 @@ public override bool TryContains(Entity entity, out bool contains)
                         contains = substituted.EvalBoolean();
                         return true;
                     }
-                    else
+                    // A predicate that is False where its condition holds, and has no truth
+                    // value where it does not, is not membership either way -- so this much is
+                    // decided even though the condition is not. `x = a and x > a` at x := a is
+                    // False for real a and undefined for the rest of the plane, and a is not a
+                    // member of the set on any of it.
+                    // https://github.com/asc-community/AngouriMath/issues/878
+                    var core = substituted;
+                    while (core is Providedf(var inner, _))
+                        core = inner;
+                    if (!core.EvaluableBoolean)
                         return false;
+                    bool held = core.EvalBoolean();
+                    return !held;
                 }
 
                 internal Entity New(Entity var, Entity predicate)

Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs

@@ -46,15 +46,46 @@ partial record ConditionalSet
                 private protected override Entity IntrinsicCondition => Boolean.True;
                 /// <inheritdoc/>
                 protected override Entity InnerSimplify(bool isExact)
-                    => ExpandOnTwoAndTArguments(Var, Predicate, Codomain,
-                        (a, b, cod) => (a, b, cod) switch
-                        {
-                            (_, { Evaled: Boolean(true) }, var codom) => codom,
-                            (_, { Evaled: Boolean(false) }, var codom) => Empty,
-                            _ => null
-                        },
-                        (@this, @var, pred, _) => ((ConditionalSet)@this).New(@var, pred), isExact, propagateSet: false
-                        );
+                {
+                    // Deliberately not ExpandOnTwoAndTArguments: this node binds Var, and that
+                    // helper lifts a Providedf out of an argument onto the whole expression.
+                    // A predicate's condition is a statement about the bound variable, so
+                    // lifting it puts Var outside its own binder -- `{ x : 1/x = 0 }` came back
+                    // as `{ } provided not x = 0`, where the x named in the condition is no
+                    // longer the x the set ranges over.
+                    // https://github.com/asc-community/AngouriMath/issues/878
+                    var predicate = Predicate.InnerSimplified(isExact);
+
+                    // `expr provided a provided b` is what the rules build where two operands
+                    // each need a condition, so the chain is read to the end rather than one
+                    // layer down.
+                    var condition = (Entity)Boolean.True;
+                    var core = predicate;
+                    while (core is Providedf(var inner, var predicated))
+                    {
+                        condition = condition == Boolean.True ? predicated : condition & predicated;
+                        core = inner;
+                    }
+
+                    // Membership is the predicate holding, so anything short of True admits
+                    // nothing: a predicate that is False where it is defined and undefined
+                    // elsewhere -- which is what a condition on False says -- has no members.
+                    // Where the predicate is True under a condition, the members are exactly
+                    // the points the condition admits, and it becomes the predicate rather than
+                    // escaping to the outside of the set.
+                    return core.Evaled switch
+                    {
+                        Boolean(false) => Empty,
+                        Boolean(true) when condition != Boolean.True => New(Var, condition),
+                        // No set names every value a symbol could take, so a predicate that
+                        // holds everywhere is left as written rather than asking for the set of
+                        // Domain.Any, which does not exist.
+                        Boolean(true) => Codomain is AngouriMath.Core.Domain.Any
+                            ? New(Var, Boolean.True)
+                            : SpecialSet.Create(Codomain),
+                        _ => New(Var, predicate)
+                    };
+                }
             }
 
             partial record SpecialSet

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

@@ -27,10 +27,14 @@ private static bool IsLogic(Entity a, Entity b, Entity c)
             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,
+            // Excluded middle needs the proposition to have a truth value, which an order
+            // comparison over the complex plane does not: `i < 0` is NaN, and answering True
+            // there made Simplify disagree with substituting first.
+            // https://github.com/asc-community/AngouriMath/issues/876
+            Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True.Provided(TruthCondition(any1)),
             // The same law with the operands the other way round. `or` is commutative, so
             // leaving this out made the answer depend on which side the negation was written.
-            Orf(var any1a, Notf(var any1)) when any1 == any1a && IsLogic(any1) => True,
+            Orf(var any1a, Notf(var any1)) when any1 == any1a && IsLogic(any1) => True.Provided(TruthCondition(any1)),
             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,

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

@@ -42,6 +42,60 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right)
             return false;
         }
 
+        /// Two comparisons of one pair of operands that between them leave no case. Exactly one
+        /// of a < b, a = b and a > b holds on an ordered field, so a disjunction covering
+        /// all three is valid there -- and `<` with `>=` is how excluded middle for an
+        /// order comparison is usually written.
+        private static bool ExhaustiveSigns(ComparisonSign left, ComparisonSign right)
+        {
+            if (left is Lessf)
+                return right is GreaterOrEqualf;
+            if (left is LessOrEqualf)
+                return right is Greaterf or GreaterOrEqualf;
+            if (left is Greaterf)
+                return right is LessOrEqualf;
+            if (left is GreaterOrEqualf)
+                return right is Lessf or LessOrEqualf;
+            return false;
+        }
+
+        // Whether the ordering is there to be read at this operand. A node's declared codomain
+        // is the only thing that can say so for a symbol: a Variable is Domain.Any until it is
+        // told otherwise.
+        private static bool IsKnownReal(Entity entity)
+            => entity.Codomain is AngouriMath.Core.Domain.Integer
+                              or AngouriMath.Core.Domain.Rational
+                              or AngouriMath.Core.Domain.Real;
+
+        /// The condition under which an order comparison against <paramref name="entity"/> has
+        /// a truth value. Over the complex plane it need not have one -- <c>i &lt; 0</c> is
+        /// <c>NaN</c>, since the complex numbers are not ordered -- so a rule that decides a
+        /// conjunction or a disjunction of comparisons has to carry the condition rather than
+        /// help itself to it. <see cref="Entity.Provided(Entity)"/> drops the condition when it
+        /// is <c>True</c>, so nothing is attached where the operands are already known real or
+        /// where the reading is real-valued to begin with.
+        /// https://github.com/asc-community/AngouriMath/issues/876
+        private static Entity OrderedCondition(Entity entity)
+            => MathS.Settings.Codomain.Value is AngouriMath.Core.Domain.Real || IsKnownReal(entity)
+                ? True
+                : entity.In(AngouriMath.Core.Domain.Real);
+
+        /// The condition under which <paramref name="statement"/> has a truth value at all.
+        /// Equality and set membership have one everywhere on the complex plane; an order
+        /// comparison has one only where both of its operands are real.
+        /// https://github.com/asc-community/AngouriMath/issues/876
+        internal static Entity TruthCondition(Entity statement) => statement switch
+        {
+            Equalsf => True,
+            ComparisonSign sign =>
+                BothHold(OrderedCondition(sign.DirectChildren[0]), OrderedCondition(sign.DirectChildren[1])),
+            _ => True
+        };
+
+        // `True & c` is an Andf and not True, which would stop Provided from dropping it.
+        private static Entity BothHold(Entity left, Entity right)
+            => left == True ? right : right == True ? left : left & right;
+
         internal static Entity InequalityEqualityRules(Entity x) => x switch
         {
             Orf(Lessf(var any1, var any2), Equalsf(var any1a, var any2a)) when any1 == any1a && any2 == any2a => any1 <= any2,
@@ -87,7 +141,20 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right)
             Andf(ComparisonSign left, ComparisonSign right) when
             left.DirectChildren[0] == right.DirectChildren[0] &&
             left.DirectChildren[1] == right.DirectChildren[1] &&
-            OppositeSigns(left, right) => False,
+            OppositeSigns(left, right) =>
+                False.Provided(OrderedCondition(left.DirectChildren[0]))
+                     .Provided(OrderedCondition(left.DirectChildren[1])),
+
+            // The other half of the same law. The unsatisfiable conjunction above was decided
+            // and the valid disjunction was not, so the library was taking the half of excluded
+            // middle that needs the operands to be real and skipping the half that needs the
+            // same thing. https://github.com/asc-community/AngouriMath/issues/876
+            Orf(ComparisonSign left, ComparisonSign right) when
+            left.DirectChildren[0] == right.DirectChildren[0] &&
+            left.DirectChildren[1] == right.DirectChildren[1] &&
+            ExhaustiveSigns(left, right) =>
+                True.Provided(OrderedCondition(left.DirectChildren[0]))
+                    .Provided(OrderedCondition(left.DirectChildren[1])),
 
             Equalsf(Powf(var any1, var rePo), var zero) when IsRealPositive(rePo) && IsZero(zero) => any1.EqualTo(zero),
             Equalsf(Divf(Integer(1), var expr), var zero) when IsZero(zero) => new Providedf(false, !expr.EqualTo(0)),
@@ -139,10 +206,13 @@ 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.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),
+            // The DomainCondition is about singularities and says nothing about where the
+            // ordering is defined, so both conditions are needed: `x < x` is False on the real
+            // line and NaN at x = i.
+            Greaterf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition).Provided(OrderedCondition(any1)),
+            Lessf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition).Provided(OrderedCondition(any1)),
+            GreaterOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition).Provided(OrderedCondition(any1)),
+            LessOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition).Provided(OrderedCondition(any1)),
 
             _ => x
         };

Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs

@@ -6,6 +6,7 @@
 //
 
 using AngouriMath;
+using AngouriMath.Core;
 using AngouriMath.Extensions;
 using PeterO.Numbers;
 using System.Linq;
@@ -442,13 +443,14 @@ public void ExpandCancelsAQuotientOfFactorialsRatherThanLeavingIt(string input)
         // `(x < 0) or not (x < 0)` was left as written. A bare variable hid it, because the
         // boolean minimiser reduces those whichever way round they are — it takes a
         // comparison, which the minimiser does not treat as an atom, to see it.
+        //
+        // The rows here are the propositions that hold unconditionally, which is why they can
+        // be pinned to True outright: equality and set membership are decided everywhere on
+        // the complex plane, and a boolean variable stands for something with a truth value.
+        // The order comparisons that were also listed here moved to
+        // <see cref="AnExhaustivePairOfComparisonsHoldsOverTheReals"/>, because `i < 0` has no
+        // truth value and True is not their answer over the default codomain.
         [Theory]
-        [InlineData("not (x < 0) or (x < 0)")]
-        [InlineData("(x < 0) or not (x < 0)")]
-        [InlineData("not (x > 0) or (x > 0)")]
-        [InlineData("(x > 0) or not (x > 0)")]
-        [InlineData("not (x <= 0) or (x <= 0)")]
-        [InlineData("(x <= 0) or not (x <= 0)")]
         [InlineData("not (a = b) or (a = b)")]
         [InlineData("(a = b) or not (a = b)")]
         [InlineData("not (x in RR) or (x in RR)")]
@@ -457,5 +459,67 @@ public void ExpandCancelsAQuotientOfFactorialsRatherThanLeavingIt(string input)
         [InlineData("p or not p")]
         public void ExcludedMiddleHoldsWhicheverOperandCarriesTheNegation(string input)
             => Assert.Equal(Entity.Boolean.True, input.ToEntity().Simplify());
+
+        // https://github.com/asc-community/AngouriMath/issues/876 §2
+        // An order comparison need not have a truth value: the default codomain is
+        // Domain.Complex and `i < 0` is NaN. The rules that decide two comparisons of the same
+        // pair of operands did not say so — `x < 0 and x >= 0` reduced to False, which is the
+        // answer over the reals, while at x = i the statement is NaN. So Simplify did not
+        // commute with Substitute, silently. The reduction is right; what was missing is the
+        // condition it holds under.
+        //
+        // This is asserted as a commutation rather than against a printed form so that it
+        // holds whatever shape the condition takes.
+        [Theory]
+        [InlineData("x < 0 and x >= 0")]
+        [InlineData("x > 0 and x <= 0")]
+        [InlineData("x < 0 and x = 0")]
+        [InlineData("x < 0 or x >= 0")]
+        [InlineData("x <= 0 or x > 0")]
+        [InlineData("x < x")]
+        [InlineData("x >= x")]
+        [InlineData("not (x < 0) or (x < 0)")]
+        [InlineData("(x < 0) or not (x < 0)")]
+        public void DecidingAPairOfComparisonsKeepsItsValueOffTheRealLine(string input)
+        {
+            var original = input.ToEntity();
+            var atI = original.Substitute("x", "i").Evaled;
+            // Stated rather than assumed: the whole point is that there is nothing to decide
+            // here, so a change that gave `i < 0` a truth value would make this test vacuous.
+            Assert.Equal(MathS.NaN, atI);
+            Assert.Equal(atI, original.Simplify().Substitute("x", "i").Evaled);
+        }
+
+        // https://github.com/asc-community/AngouriMath/issues/876 §3
+        // The unsatisfiable conjunction was decided and the valid disjunction was not, so the
+        // library took the half of excluded middle that is unsound off the real line and
+        // skipped the half that is sound on it. Over the reals both are decided outright, and
+        // nothing else in the library read MathS.Settings.Codomain to find that out.
+        [Theory]
+        [InlineData("x < 0 or x >= 0")]
+        [InlineData("x <= 0 or x > 0")]
+        [InlineData("x <= 0 or x >= 0")]
+        [InlineData("x > 0 or x <= 0")]
+        [InlineData("x >= x")]
+        [InlineData("not (x < 0) or (x < 0)")]
+        [InlineData("(x < 0) or not (x < 0)")]
+        [InlineData("not (x <= 0) or (x <= 0)")]
+        [InlineData("(x <= 0) or not (x <= 0)")]
+        public void AnExhaustivePairOfComparisonsHoldsOverTheReals(string input)
+        {
+            using var _ = MathS.Settings.Codomain.Set(Domain.Real);
+            Assert.Equal(Entity.Boolean.True, input.ToEntity().Simplify());
+        }
+
+        [Theory]
+        [InlineData("x < 0 and x >= 0")]
+        [InlineData("x > 0 and x <= 0")]
+        [InlineData("x < 0 and x = 0")]
+        [InlineData("x < x")]
+        public void AContradictoryPairOfComparisonsFailsOverTheReals(string input)
+        {
+            using var _ = MathS.Settings.Codomain.Set(Domain.Real);
+            Assert.Equal(Entity.Boolean.False, input.ToEntity().Simplify());
+        }
     }
 }

Sources/Tests/UnitTests/Core/Sets/CSetAndCSet.cs

@@ -6,6 +6,7 @@
 //
 
 using AngouriMath;
+using AngouriMath.Extensions;
 using Xunit;
 using static AngouriMath.Entity;
 using static AngouriMath.Entity.Set;
@@ -43,5 +44,39 @@ private void TestArb(Entity actual, Entity expected)
         [Fact] public void Intersection2() => Test(A.Intersect(A1), new("x", "x > 0"));
         [Fact] public void Intersection3() => TestArb(A.Intersect(D).Simplify(), Set.Empty);
         [Fact] public void Intersection4() => TestArb(D.Intersect(A).Simplify(), Set.Empty);
+
+        // https://github.com/asc-community/AngouriMath/issues/878
+        // The predicate was passed to the argument-expanding helper, which lifts a Providedf
+        // out of an argument onto the whole expression. For a node that binds a variable that
+        // puts the bound variable outside its own binder: `{ x : 1/x = 0 }` came back as
+        // `{ } provided not x = 0`. Membership is the predicate holding, and a predicate that
+        // is False where its condition holds and undefined where it does not admits nothing,
+        // so the answer is the empty set with no condition to place anywhere.
+        [Theory]
+        [InlineData("{ x : 1/x = 0 }")]
+        [InlineData("{ x : x > 0 and x < 0 }")]
+        public void APredicateThatIsNeverTrueGivesTheEmptySetAndNoCondition(string input)
+            => Assert.Equal(Set.Empty, input.ToEntity().Simplify());
+
+        // Nothing may name the bound variable outside the set, whatever the answer turns out
+        // to be, so this is asserted on the shape rather than on one expected result.
+        [Theory]
+        [InlineData("{ x : 1/x = 0 }")]
+        [InlineData("{ x : x/x = 1 }")]
+        [InlineData("{ x : x > 0 and x < 0 }")]
+        [InlineData("{ x : x = a and x > a }")]
+        public void SimplifyingASetBuilderLeavesNoConditionOutsideTheBinder(string input)
+            => Assert.DoesNotContain(input.ToEntity().Simplify().DirectChildren, node => node is Providedf);
+
+        // For a predicate that holds everywhere InnerSimplify returned the node's Codomain,
+        // which is Domain.Any for a set-builder, and SpecialSet.Create has no case for Any --
+        // so it threw AngouriBugException out of Simplify on valid input rather than answering.
+        [Theory]
+        [InlineData("{ x : 1 = 1 }")]
+        [InlineData("{ x : x = x }")]
+        [InlineData("{ x : x/x = 1 }")]
+        [InlineData("{ x : x > 0 or x <= 0 }")]
+        public void APredicateThatHoldsEverywhereDoesNotThrow(string input)
+            => Assert.IsAssignableFrom<Set>(input.ToEntity().Simplify());
     }
 }