From ae8cad5a2708435579acb4d604c946b0eab1d05e Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Tue, 11 Aug 2026 10:24:39 +0000 Subject: [PATCH 1/2] Read a set-builder's predicate inside its binder (#878) ConditionalSet.InnerSimplify handed the predicate to the generic argument-expanding helper, which lifts a Providedf out of an argument and puts it on the whole expression. That is right for a function, whose arguments are values, and wrong for a node that binds a variable: `{ 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. Membership is the predicate holding, so the condition did not need hoisting anywhere. A predicate that is False where its condition holds and undefined where it does not admits nothing, and the answer is `{ }`. A predicate that is True under a condition admits exactly the points the condition admits, so the condition becomes the predicate and stays inside the binder -- `{ x : x/x = 1 }` is `{ x : not x = 0 }`. The other branch had never worked. For a predicate that holds everywhere the code returned the node's Codomain, a set-builder's Codomain is Domain.Any, and SpecialSet.Create has no case for Any -- so `{ x : 1 = 1 }`, `{ x : x = x }` and `{ x : x/x = 1 }` all threw AngouriBugException out of Simplify on valid input. No set names every value a symbol could take, which is why Any has none, so a predicate that holds everywhere is left as written; naming the universal set is a separate question. TryContains needed the same reading. At x := a the predicate of `{ x : x = a and x > a }` is False for real a and undefined for the rest of the plane, so a is not a member anywhere and membership is decided -- but the code read only EvaluableBoolean and gave up on a Providedf. Measured: 6253 tests pass, 0 fail; casbench 117/119 with every verdict and answer in coverage.md unchanged; propcheck, simpsweep and rootcheck clean. `{ x : 1/x = 0 }` -> `{ }`, `{ x : x/x = 1 }` -> `{ x : not x = 0 }`, `{ x : 1 = 1 }` -> `{ x : True }` instead of a crash. Co-Authored-By: Claude Opus 5 (1M context) --- .../Core/Entity/Omni/Entity.Omni.Classes.cs | 13 ++++- .../Evaluation.Omni.Classes.cs | 49 +++++++++++++++---- .../Tests/UnitTests/Core/Sets/CSetAndCSet.cs | 35 +++++++++++++ 3 files changed, 87 insertions(+), 10 deletions(-) diff --git a/Sources/AngouriMath/Core/Entity/Omni/Entity.Omni.Classes.cs b/Sources/AngouriMath/Core/Entity/Omni/Entity.Omni.Classes.cs index 25cd53eac..700e89336 100644 --- a/Sources/AngouriMath/Core/Entity/Omni/Entity.Omni.Classes.cs +++ b/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) diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs index fcb26f7a2..a9727bce6 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs @@ -46,15 +46,46 @@ partial record ConditionalSet private protected override Entity IntrinsicCondition => Boolean.True; /// 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 diff --git a/Sources/Tests/UnitTests/Core/Sets/CSetAndCSet.cs b/Sources/Tests/UnitTests/Core/Sets/CSetAndCSet.cs index d3f2c397f..ae5bbac25 100644 --- a/Sources/Tests/UnitTests/Core/Sets/CSetAndCSet.cs +++ b/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(input.ToEntity().Simplify()); } } From e70371ff0e75c27b12ddd69c0e101c05498d216c Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Tue, 11 Aug 2026 10:24:58 +0000 Subject: [PATCH 2/2] Carry the condition an order comparison is decided under (#876) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The complex numbers are not ordered, so `i < 0` is NaN and a comparison need not have a truth value. Three rules decided a pair of comparisons as though it always did: x < 0 and x >= 0 -> False at x := i the statement is NaN x < x -> False likewise not (x < 0) or (x < 0) -> True likewise So Simplify did not commute with Substitute, silently, and the default codomain is Domain.Complex. The reductions themselves are right -- they are the answers over the reals -- and what was missing is the condition they hold under. Each now carries it, and Provided drops a condition that is True, so nothing is attached where the operands are already real: `2 < 0 and 2 >= 0` and `abs(x) < abs(x)` still answer False outright, and under MathS.Settings.Codomain = Domain.Real so does `x < 0 and x >= 0`. Nothing outside the limit machinery read that setting before this. The disjunction was the other half of the same law and was missing entirely. The unsatisfiable conjunction was decided while the valid disjunction was not, so the library took the half of excluded middle that needs the operands to be real and skipped the half that needs exactly the same thing. ExhaustiveSigns is the mirror of OppositeSigns: `x < 0 or x >= 0` is True where x is real, and over the reals `piecewise(0 provided x < 0, 0 provided x >= 0)` now reaches 0, which #876 §3 gives as the consequence. DomainCondition is not the mechanism, despite the neighbouring rules using it: it records singularities -- division by zero, log poles -- and says nothing about where an order comparison is defined. Both are needed on `x < x`. The excluded-middle rules keep answering True unconditionally where the proposition has a truth value everywhere, which is why equality, set membership and a boolean variable are unaffected: `(a = b) or not (a = b)` is True with no condition. Only the order comparisons gained one. Measured: 6253 C# tests and 130 F# tests pass, 0 fail; casbench 117/119, 0 wrong, 0 error, 0 timeout, with every verdict and answer in coverage.md unchanged and only timings moved; propcheck 1340 checks, simpsweep 62778 point comparisons over 10463 expressions and rootcheck 596 cases all clean; boolmin unchanged at 6/9. Co-Authored-By: Claude Opus 5 (1M context) --- .../Patterns/Patterns.Boolean.cs | 8 +- .../Patterns/Patterns.EqualityInequality.cs | 80 +++++++++++++++++-- .../Common/SimplificationRegressionTest.cs | 76 ++++++++++++++++-- 3 files changed, 151 insertions(+), 13 deletions(-) diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs index 429243736..dbfb3d8e7 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs +++ b/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, diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs index 9d4e8d874..a51a5dc83 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs +++ b/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 has + /// a truth value. Over the complex plane it need not have one -- i < 0 is + /// NaN, 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. drops the condition when it + /// is True, 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 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 }; diff --git a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs index eecfaac8e..5c9753399 100644 --- a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs +++ b/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 + // , 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()); + } } }