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/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());
+ }
}
}
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());
}
}