diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 81b0af991..e06525646 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -1825,5 +1825,373 @@ is var (divided, remainder) node, bound["num"], bound["den"], level), Soundness.SoundUnderAssumptions, when: bound => bound["num"].Vars.Any() && bound["den"].Vars.Any())); + + /// + /// , as data. + /// + /// + /// + /// Sixty-five arms, and the set where transcription found a wrong answer: four of + /// the eight or-with-equality arms carried their neighbour's comparison, so + /// (y < x) or (x = y) simplified to x <= y — the negation of itself + /// off the diagonal. Fixed on its own before this + /// (#1077), so what + /// is here agrees with a switch that is right. + /// + /// + /// Three things this set needs that a pattern alone does not say. The two De Morgan arms + /// are a fold over a chain of any length rather than a shape, so the rule matches + /// the chain and the fold stays in Patterns.EqualityInequality.cs where both forms + /// ask it. The excluded-middle pair reads two bound comparisons against each other + /// — same operands, opposite or exhaustive signs — which is a when over the + /// bindings rather than a shape. And the conditions those two attach are about where the + /// ordering is defined at all, since i < 0 is NaN rather than false. + /// + /// + internal static MatchedRuleSet InequalityEquality { get; } = new( + nameof(InequalityEquality), + + new MatchedRule( + "a-less-than-or-equal-as-written-is-at-most", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] <= bound["b"], + Soundness.Sound), + new MatchedRule( + "a-less-than-or-equal-the-other-way-round-is-at-least", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("a")), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] >= bound["b"], + Soundness.Sound), + new MatchedRule( + "a-greater-than-or-equal-as-written-is-at-least", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] >= bound["b"], + Soundness.Sound), + new MatchedRule( + "a-greater-than-or-equal-the-other-way-round-is-at-most", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("a")), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] <= bound["b"], + Soundness.Sound), + new MatchedRule( + "an-equality-or-a-less-than-as-written-is-at-most", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] <= bound["b"], + Soundness.Sound), + new MatchedRule( + "an-equality-or-a-less-than-the-other-way-round-is-at-least", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("a"))), + bound => bound["a"] >= bound["b"], + Soundness.Sound), + new MatchedRule( + "an-equality-or-a-greater-than-as-written-is-at-least", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] >= bound["b"], + Soundness.Sound), + new MatchedRule( + "an-equality-or-a-greater-than-the-other-way-round-is-at-most", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("a"))), + bound => bound["a"] <= bound["b"], + Soundness.Sound), + new MatchedRule( + "the-negation-of-a-greater-turns-it-round", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] <= bound["b"], + Soundness.Sound), + new MatchedRule( + "the-negation-of-a-less-turns-it-round", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] >= bound["b"], + Soundness.Sound), + new MatchedRule( + "the-negation-of-a-greaterorequal-turns-it-round", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] < bound["b"], + Soundness.Sound), + new MatchedRule( + "the-negation-of-a-lessorequal-turns-it-round", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b"))), + bound => bound["a"] > bound["b"], + Soundness.Sound), + // De Morgan over a chain of any length, which is a fold rather than a shape -- so the rule + // matches the chain and the fold stays in `Patterns.EqualityInequality.cs`, asked by both + // forms. + new MatchedRule( + "a-negated-conjunction-becomes-a-disjunction-of-negations", + MatchPattern.Node(MatchPattern.Any("chain", chain => Functions.Patterns.MayPushNotInside(Andf.LinearChildren(chain), insideConjunction: true))), + bound => Functions.Patterns.PushNotInside(Andf.LinearChildren((Andf)bound["chain"]), disjoin: true), + Soundness.Sound), + new MatchedRule( + "a-negated-disjunction-becomes-a-conjunction-of-negations", + MatchPattern.Node(MatchPattern.Any("chain", chain => Functions.Patterns.MayPushNotInside(Orf.LinearChildren(chain), insideConjunction: false))), + bound => Functions.Patterns.PushNotInside(Orf.LinearChildren((Orf)bound["chain"]), disjoin: false), + Soundness.Sound), + new MatchedRule( + "a-chain-of-greaters-implies-its-own-ends", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("c"))), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("c"))), + bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(bound["b"].DomainCondition).Provided(bound["c"].DomainCondition), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-chain-of-lesss-implies-its-own-ends", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("c"))), MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("c"))), + bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(bound["b"].DomainCondition).Provided(bound["c"].DomainCondition), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-equals-with-zero-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one)), MatchPattern.Any("other", one => !Functions.Patterns.IsZeroReal(one))), + bound => bound["other"].EqualTo(bound["zero"]), + Soundness.Sound), + new MatchedRule( + "a-greater-with-zero-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one)), MatchPattern.Any("other", one => !Functions.Patterns.IsZeroReal(one))), + bound => bound["other"] < bound["zero"], + Soundness.Sound), + new MatchedRule( + "a-less-with-zero-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one)), MatchPattern.Any("other", one => !Functions.Patterns.IsZeroReal(one))), + bound => bound["other"] > bound["zero"], + Soundness.Sound), + new MatchedRule( + "a-greaterorequal-with-zero-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one)), MatchPattern.Any("other", one => !Functions.Patterns.IsZeroReal(one))), + bound => bound["other"] <= bound["zero"], + Soundness.Sound), + new MatchedRule( + "a-lessorequal-with-zero-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one)), MatchPattern.Any("other", one => !Functions.Patterns.IsZeroReal(one))), + bound => bound["other"] >= bound["zero"], + Soundness.Sound), + new MatchedRule( + "a-equals-with-a-number-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("other", one => one is not Number)), + bound => bound["other"].EqualTo(bound["c"]), + Soundness.Sound), + new MatchedRule( + "a-greater-with-a-number-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("other", one => one is not Number)), + bound => bound["other"] < bound["c"], + Soundness.Sound), + new MatchedRule( + "a-less-with-a-number-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("other", one => one is not Number)), + bound => bound["other"] > bound["c"], + Soundness.Sound), + new MatchedRule( + "a-greaterorequal-with-a-number-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("other", one => one is not Number)), + bound => bound["other"] <= bound["c"], + Soundness.Sound), + new MatchedRule( + "a-lessorequal-with-a-number-on-the-left-turns-round", + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("other", one => one is not Number)), + bound => bound["other"] >= bound["c"], + Soundness.Sound), + new MatchedRule( + "two-comparisons-of-one-pair-that-exclude-each-other-are-false", + MatchPattern.Node(MatchPattern.Any("left"), MatchPattern.Any("right")), + bound => Entity.Boolean.False.Provided(Functions.Patterns.OrderedConditionOf(bound["left"], 0)).Provided(Functions.Patterns.OrderedConditionOf(bound["left"], 1)), + Soundness.SoundUnderAssumptions, + when: bound => Functions.Patterns.SameOperands(bound["left"], bound["right"]) && Functions.Patterns.HaveOppositeSigns(bound["left"], bound["right"])), + // The other half of the same law. The unsatisfiable conjunction above was decided and the + // valid disjunction was not -- half of excluded middle. https://github.com/asc- + // community/AngouriMath/issues/876 + new MatchedRule( + "two-comparisons-of-one-pair-that-leave-no-case-are-true", + MatchPattern.Node(MatchPattern.Any("left"), MatchPattern.Any("right")), + bound => Entity.Boolean.True.Provided(Functions.Patterns.OrderedConditionOf(bound["left"], 0)).Provided(Functions.Patterns.OrderedConditionOf(bound["left"], 1)), + Soundness.SoundUnderAssumptions, + when: bound => Functions.Patterns.SameOperands(bound["left"], bound["right"]) && Functions.Patterns.HaveExhaustiveSigns(bound["left"], bound["right"])), + new MatchedRule( + "a-power-with-a-real-positive-exponent-is-zero-when-its-base-is", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("p", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(bound["zero"]), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-reciprocal-is-never-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Exact(Integer.Create(1)), MatchPattern.Any("e")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => new Providedf(false, !bound["e"].EqualTo(0)), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-positive-factor-first-drops-out-of-a-equals-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(Integer.Zero), + Soundness.Sound), + new MatchedRule( + "a-positive-factor-first-drops-out-of-a-greater-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] > Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-first-drops-out-of-a-greaterorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] >= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-first-drops-out-of-a-less-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] < Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-first-drops-out-of-a-lessorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] <= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-second-drops-out-of-a-equals-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(Integer.Zero), + Soundness.Sound), + new MatchedRule( + "a-positive-factor-second-drops-out-of-a-greater-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] > Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-second-drops-out-of-a-greaterorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] >= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-second-drops-out-of-a-less-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] < Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-factor-second-drops-out-of-a-lessorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] <= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-first-drops-out-of-a-equals-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(Integer.Zero), + Soundness.Sound), + new MatchedRule( + "a-negative-factor-first-drops-out-of-a-greater-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] < Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-first-drops-out-of-a-greaterorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] <= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-first-drops-out-of-a-less-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] > Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-first-drops-out-of-a-lessorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0)), MatchPattern.Any("a")), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] >= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-second-drops-out-of-a-equals-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(Integer.Zero), + Soundness.Sound), + new MatchedRule( + "a-negative-factor-second-drops-out-of-a-greater-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] < Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-second-drops-out-of-a-greaterorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] <= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-second-drops-out-of-a-less-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] > Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-factor-second-drops-out-of-a-lessorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] >= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-divisor-drops-out-of-a-equals-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(Integer.Zero), + Soundness.Sound), + new MatchedRule( + "a-positive-divisor-drops-out-of-a-greater-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] > Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-divisor-drops-out-of-a-greaterorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] >= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-divisor-drops-out-of-a-less-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] < Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-positive-divisor-drops-out-of-a-lessorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] <= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-divisor-drops-out-of-a-equals-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"].EqualTo(Integer.Zero), + Soundness.Sound), + new MatchedRule( + "a-negative-divisor-drops-out-of-a-greater-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] < Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-divisor-drops-out-of-a-greaterorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] <= Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-divisor-drops-out-of-a-less-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] > Integer.Zero, + Soundness.Sound), + new MatchedRule( + "a-negative-divisor-drops-out-of-a-lessorequal-with-zero", + MatchPattern.Node(MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("k", one => Functions.Patterns.IsRealAbove(one, 0) is false && Functions.Patterns.IsRealBelow(one, 0))), MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => bound["a"] >= Integer.Zero, + Soundness.Sound), + // The condition carried is the **argument's**, which is what the `switch` reads -- + // `Factorialf({ DomainCondition: var condition })` is a property pattern on the child, + // not on the factorial. Whether that is the right condition is a separate question and + // https://github.com/asc-community/AngouriMath/issues/1081 asks it; agreeing with the + // arms is this rule's job. + new MatchedRule( + "a-factorial-is-never-zero", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("arg")), + MatchPattern.Any("zero", one => Functions.Patterns.IsZeroReal(one))), + bound => Entity.Boolean.False.Provided(bound["arg"].DomainCondition), + Soundness.SoundUnderAssumptions), + // The `DomainCondition` is about singularities and says nothing about where the ordering is + // defined, so both are needed: `x < x` is False on the real line and NaN at x = i. + new MatchedRule( + "a-greater-of-a-thing-with-itself-is-decided", + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")), + bound => Entity.Boolean.False.Provided(bound["a"].DomainCondition).Provided(Functions.Patterns.OrderedConditionFor(bound["a"])), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-less-of-a-thing-with-itself-is-decided", + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")), + bound => Entity.Boolean.False.Provided(bound["a"].DomainCondition).Provided(Functions.Patterns.OrderedConditionFor(bound["a"])), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-greaterorequal-of-a-thing-with-itself-is-decided", + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")), + bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(Functions.Patterns.OrderedConditionFor(bound["a"])), + Soundness.SoundUnderAssumptions), + new MatchedRule( + "a-lessorequal-of-a-thing-with-itself-is-decided", + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")), + bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(Functions.Patterns.OrderedConditionFor(bound["a"])), + Soundness.SoundUnderAssumptions)); } } diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRules.cs b/Sources/AngouriMath/Core/Transformations/RewriteRules.cs index 462844052..5685d0ba1 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRules.cs +++ b/Sources/AngouriMath/Core/Transformations/RewriteRules.cs @@ -480,12 +480,20 @@ public static class RewriteRules /// /// Rules about equalities and inequalities. /// + /// + /// Run by the matcher rather than by the switch — + /// , where its sixty-five arms are + /// sixty-five rules: this set writes out shapes rather than orientations, so there is + /// nothing for a commutative pattern to collapse. What it gains instead is that the two + /// De Morgan folds and the two excluded-middle rules say what they need of the bindings, + /// which a switch arm says in a guard beside the shape. + /// public static RewriteRuleSet InequalityEquality { get; } = new( nameof(InequalityEquality), "Rearranges equalities and inequalities into their usual form.", TransformationRelation.Equivalence, Soundness.SoundUnderAssumptions, - Patterns.InequalityEqualityRules, + Matching.MatchedRules.InequalityEquality.ApplyHere, Patterns.InequalityEqualityRulesArms); /// diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs index 2e7dea3a1..0c21c27ba 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs @@ -6,6 +6,8 @@ // using System; +using System.Collections.Generic; +using System.Linq; using static AngouriMath.Entity; using static AngouriMath.Entity.Boolean; using static Antlr4.Runtime.Atn.SemanticContext; @@ -96,6 +98,64 @@ private static Entity OrderedCondition(Entity entity) private static Entity BothHold(Entity left, Entity right) => left == True ? right : right == True ? left : left & right; + /// + /// The predicates the rules key on, named so that MatchedRules.InequalityEquality + /// asks the same questions this switch asks rather than restating them. Where a + /// condition is about a branch or an ordering, two copies of it is how the two come to + /// disagree. + /// + internal static bool IsZeroReal(Entity entity) => IsZero(entity); + + /// + internal static bool IsRealAbove(Entity entity, int bound) => bound == 0 && IsRealPositive(entity); + + /// + internal static bool IsRealBelow(Entity entity, int bound) => bound == 0 && IsRealNegative(entity); + + /// Whether two comparisons are about the same pair of operands, in the same order. + internal static bool SameOperands(Entity left, Entity right) + => left is ComparisonSign && right is ComparisonSign + && left.DirectChildren[0] == right.DirectChildren[0] + && left.DirectChildren[1] == right.DirectChildren[1]; + + /// + internal static bool HaveOppositeSigns(Entity left, Entity right) + => OppositeSigns((ComparisonSign)left, (ComparisonSign)right); + + /// + internal static bool HaveExhaustiveSigns(Entity left, Entity right) + => ExhaustiveSigns((ComparisonSign)left, (ComparisonSign)right); + + /// The of one operand of a comparison, by index. + internal static Entity OrderedConditionOf(Entity comparison, int operand) + => OrderedCondition(comparison.DirectChildren[operand]); + + /// + internal static Entity OrderedConditionFor(Entity entity) => OrderedCondition(entity); + + /// + /// Whether pushing a not through this conjunction or disjunction leaves the + /// expression no more complex: at most one operand may be something other than a + /// comparison, since only a comparison absorbs the negation into itself. + /// + /// + /// Notf(Equalsf) has the same complexity as Equalsf in the cost model, so a + /// negation counts as a comparison here. + /// + internal static bool MayPushNotInside(IEnumerable operands, bool insideConjunction) + => operands.Count(one => one is not ComparisonSign and not Notf + && (insideConjunction ? one is not Orf : one is not Andf)) <= 1; + + /// + /// De Morgan: the negation of each operand, joined by the dual connective. Written once + /// and asked by both the switch and MatchedRules.InequalityEquality, because + /// it is a fold over a chain of any length rather than a shape, and a pattern says shapes. + /// + internal static Entity PushNotInside(IEnumerable operands, bool disjoin) + => operands + .Select(one => InequalityEqualityRules(one switch { Notf(var inner) => inner, var whole => new Notf(whole) })) + .Aggregate((left, right) => disjoin ? left | right : left & right); + [AddressableRules] internal static Entity InequalityEqualityRules(Entity x) => x switch { @@ -126,10 +186,10 @@ private static Entity BothHold(Entity left, Entity right) // 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), + Notf(Andf a) when MayPushNotInside(Andf.LinearChildren(a), insideConjunction: true) + => PushNotInside(Andf.LinearChildren(a), disjoin: true), + Notf(Orf a) when MayPushNotInside(Orf.LinearChildren(a), insideConjunction: false) + => PushNotInside(Orf.LinearChildren(a), disjoin: false), 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.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), diff --git a/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs b/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs index 7e11d70a7..b454dad2d 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs @@ -465,6 +465,44 @@ public void CommonDenominatorAsDataMatchesTheSwitch(int ordinal) MatchedRules.CommonDenominator(level), leastFirings: 50); } + /// + /// Sixty-five arms, and the set where transcription found a wrong answer. Four of + /// the eight `or`-with-equality arms carried their neighbour's comparison, so + /// `(y < x) or (x = y)` simplified to `x <= y` — its own negation off the diagonal. + /// That was fixed first (#1077), so this agrees with a `switch` that is right; had it been + /// transcribed faithfully instead, this test would have passed and recorded the defect. + /// + /// + /// The corpus needs comparisons, which the arithmetic grammar does not generate, so almost + /// all of the firings come from `extra` here. The `leastFirings` threshold is what keeps + /// that honest. + /// + [Fact] + public void InequalityEqualityAsDataMatchesTheSwitch() + => AssertAgrees("InequalityEquality", Patterns.InequalityEqualityRules, + MatchedRules.InequalityEquality, leastFirings: 60, extra: new[] + { + "(x < y) or (x = y)", "(y < x) or (x = y)", "(x > y) or (x = y)", + "(y > x) or (x = y)", "(x = y) or (x < y)", "(x = y) or (y < x)", + "(x = y) or (x > y)", "(x = y) or (y > x)", + "not (x > y)", "not (x < y)", "not (x >= y)", "not (x <= y)", + "not (x > y and y = z)", "not (x > y or y = z)", + "not (x > y and y < z and z = x)", "not (x > y or y < z or z = x)", + "(x > y and y > z) implies (x > z)", "(x < y and y < z) implies (x < z)", + "0 = x", "0 > x", "0 < x", "0 >= x", "0 <= x", + "2 = x", "2 > x", "2 < x", "2 >= x", "2 <= x", + "x < y and x > y", "x < y and x = y", "x >= y and x < y", + "x < y or x >= y", "x <= y or x > y", "x <= y or x >= y", + "x ^ 2 = 0", "x ^ (1/2) = 0", "1 / x = 0", + "2 * x = 0", "2 * x > 0", "2 * x >= 0", "2 * x < 0", "2 * x <= 0", + "x * 2 = 0", "x * 2 > 0", "x * 2 >= 0", "x * 2 < 0", "x * 2 <= 0", + "-2 * x = 0", "-2 * x > 0", "-2 * x >= 0", "-2 * x < 0", "-2 * x <= 0", + "x * (-2) = 0", "x * (-2) > 0", "x * (-2) < 0", + "x / 2 = 0", "x / 2 > 0", "x / 2 >= 0", "x / 2 < 0", "x / 2 <= 0", + "x / (-2) = 0", "x / (-2) > 0", "x / (-2) < 0", + "x! = 0", "x > x", "x < x", "x >= x", "x <= x", + }); + /// /// A predicate on a hole that is a mathematical property rather than a sign or a type. /// The corpus reaches it rarely, so the shapes are given here as well — a set that fires diff --git a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs index 6e201f0a1..c28ec8db7 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs @@ -131,6 +131,8 @@ public void EveryDataRuleIsClassifiedAsWritten() Assert.Equal( new[] { + "a-chain-of-greaters-implies-its-own-ends: ReplacementIsCode", + "a-chain-of-lesss-implies-its-own-ends: ReplacementIsCode", "a-common-factor-is-collected-out-of-a-whole-sum: ReplacementIsCode", "a-conditional-set-whose-condition-is-its-own-membership-is-that-set: ReplacementIsCode", "a-conjunction-absorbs-a-disjunction-it-shares-an-operand-with: ReplacementIsCode", @@ -155,21 +157,73 @@ public void EveryDataRuleIsClassifiedAsWritten() "a-disjunction-with-itself-is-itself: ReplacementIsCode", "a-double-negation-cancels: ReplacementIsCode", "a-doubled-sine-times-a-cosecant-is-twice-the-cosine: ReplacementIsCode", + "a-equals-with-a-number-on-the-left-turns-round: ReplacementIsCode", + "a-equals-with-zero-on-the-left-turns-round: ReplacementIsCode", "a-factor-shared-by-two-added-products-comes-out: ReplacementIsCode", "a-factor-shared-by-two-subtracted-products-comes-out: ReplacementIsCode", "a-factor-subtracted-from-a-product-it-is-in: ReplacementIsCode", + "a-factorial-is-never-zero: ReplacementIsCode", + "a-greater-of-a-thing-with-itself-is-decided: ReplacementIsCode", + "a-greater-than-or-equal-as-written-is-at-least: ReplacementIsCode", + "a-greater-than-or-equal-the-other-way-round-is-at-most: ReplacementIsCode", + "a-greater-with-a-number-on-the-left-turns-round: ReplacementIsCode", + "a-greater-with-zero-on-the-left-turns-round: ReplacementIsCode", + "a-greaterorequal-of-a-thing-with-itself-is-decided: ReplacementIsCode", + "a-greaterorequal-with-a-number-on-the-left-turns-round: ReplacementIsCode", + "a-greaterorequal-with-zero-on-the-left-turns-round: ReplacementIsCode", + "a-less-of-a-thing-with-itself-is-decided: ReplacementIsCode", + "a-less-than-or-equal-as-written-is-at-most: ReplacementIsCode", + "a-less-than-or-equal-the-other-way-round-is-at-least: ReplacementIsCode", + "a-less-with-a-number-on-the-left-turns-round: ReplacementIsCode", + "a-less-with-zero-on-the-left-turns-round: ReplacementIsCode", + "a-lessorequal-of-a-thing-with-itself-is-decided: ReplacementIsCode", + "a-lessorequal-with-a-number-on-the-left-turns-round: ReplacementIsCode", + "a-lessorequal-with-zero-on-the-left-turns-round: ReplacementIsCode", + "a-negated-conjunction-becomes-a-disjunction-of-negations: ReplacementIsCode", + "a-negated-disjunction-becomes-a-conjunction-of-negations: ReplacementIsCode", "a-negation-or-something-is-an-implication: ReplacementIsCode", "a-negative-added-is-subtracted: ReplacementIsCode", + "a-negative-divisor-drops-out-of-a-equals-with-zero: ReplacementIsCode", + "a-negative-divisor-drops-out-of-a-greater-with-zero: ReplacementIsCode", + "a-negative-divisor-drops-out-of-a-greaterorequal-with-zero: ReplacementIsCode", + "a-negative-divisor-drops-out-of-a-less-with-zero: ReplacementIsCode", + "a-negative-divisor-drops-out-of-a-lessorequal-with-zero: ReplacementIsCode", + "a-negative-factor-first-drops-out-of-a-equals-with-zero: ReplacementIsCode", + "a-negative-factor-first-drops-out-of-a-greater-with-zero: ReplacementIsCode", + "a-negative-factor-first-drops-out-of-a-greaterorequal-with-zero: ReplacementIsCode", + "a-negative-factor-first-drops-out-of-a-less-with-zero: ReplacementIsCode", + "a-negative-factor-first-drops-out-of-a-lessorequal-with-zero: ReplacementIsCode", "a-negative-factor-in-a-denominator-comes-out: ReplacementIsCode", "a-negative-factor-in-a-left-product-comes-out: ReplacementIsCode", "a-negative-factor-in-a-numerator-comes-out: ReplacementIsCode", "a-negative-factor-in-a-right-product-comes-out: ReplacementIsCode", "a-negative-factor-in-a-sum-becomes-a-difference: ReplacementIsCode", + "a-negative-factor-second-drops-out-of-a-equals-with-zero: ReplacementIsCode", + "a-negative-factor-second-drops-out-of-a-greater-with-zero: ReplacementIsCode", + "a-negative-factor-second-drops-out-of-a-greaterorequal-with-zero: ReplacementIsCode", + "a-negative-factor-second-drops-out-of-a-less-with-zero: ReplacementIsCode", + "a-negative-factor-second-drops-out-of-a-lessorequal-with-zero: ReplacementIsCode", "a-negative-integer-power-becomes-a-reciprocal: ReplacementIsCode", "a-negative-minuend-comes-out-in-front: ReplacementIsCode", "a-negative-subtracted-is-added: ReplacementIsCode", "a-numeric-coefficient-is-gathered-over-a-surd: ReplacementIsCode", "a-plain-factorial-times-the-next-term: ReplacementIsCode", + "a-positive-divisor-drops-out-of-a-equals-with-zero: ReplacementIsCode", + "a-positive-divisor-drops-out-of-a-greater-with-zero: ReplacementIsCode", + "a-positive-divisor-drops-out-of-a-greaterorequal-with-zero: ReplacementIsCode", + "a-positive-divisor-drops-out-of-a-less-with-zero: ReplacementIsCode", + "a-positive-divisor-drops-out-of-a-lessorequal-with-zero: ReplacementIsCode", + "a-positive-factor-first-drops-out-of-a-equals-with-zero: ReplacementIsCode", + "a-positive-factor-first-drops-out-of-a-greater-with-zero: ReplacementIsCode", + "a-positive-factor-first-drops-out-of-a-greaterorequal-with-zero: ReplacementIsCode", + "a-positive-factor-first-drops-out-of-a-less-with-zero: ReplacementIsCode", + "a-positive-factor-first-drops-out-of-a-lessorequal-with-zero: ReplacementIsCode", + "a-positive-factor-second-drops-out-of-a-equals-with-zero: ReplacementIsCode", + "a-positive-factor-second-drops-out-of-a-greater-with-zero: ReplacementIsCode", + "a-positive-factor-second-drops-out-of-a-greaterorequal-with-zero: ReplacementIsCode", + "a-positive-factor-second-drops-out-of-a-less-with-zero: ReplacementIsCode", + "a-positive-factor-second-drops-out-of-a-lessorequal-with-zero: ReplacementIsCode", + "a-power-with-a-real-positive-exponent-is-zero-when-its-base-is: ReplacementIsCode", "a-product-chain-is-sorted-and-grouped: ReplacementIsCode", "a-product-of-two-negatives-is-positive: ReplacementIsCode", "a-product-subtracted-from-its-own-factor: ReplacementIsCode", @@ -183,6 +237,7 @@ public void EveryDataRuleIsClassifiedAsWritten() "a-quotient-of-shifted-factorials: ReplacementIsCode", "a-quotient-of-symbolic-parts-is-grouped-pairwise: ReplacementIsCode", "a-quotient-of-two-negatives-is-positive: ReplacementIsCode", + "a-reciprocal-is-never-zero: ReplacementIsCode", "a-secant-times-a-cosine-of-one-angle-is-one: ReplacementIsCode", "a-set-less-itself-is-empty: ReplacementIsCode", "a-shifted-factorial-times-a-bare-term: ReplacementIsCode", @@ -213,6 +268,10 @@ public void EveryDataRuleIsClassifiedAsWritten() "an-arccosine-of-a-numeric-reciprocal-is-an-arcsecant: ReplacementIsCode", "an-arcsecant-of-a-numeric-reciprocal-is-an-arccosine: ReplacementIsCode", "an-arcsine-of-a-numeric-reciprocal-is-an-arccosecant: ReplacementIsCode", + "an-equality-or-a-greater-than-as-written-is-at-least: ReplacementIsCode", + "an-equality-or-a-greater-than-the-other-way-round-is-at-most: ReplacementIsCode", + "an-equality-or-a-less-than-as-written-is-at-most: ReplacementIsCode", + "an-equality-or-a-less-than-the-other-way-round-is-at-least: ReplacementIsCode", "an-exclusive-disjunction-chain-is-sorted-and-grouped: ReplacementIsCode", "an-implication-between-negations-turns-round: ReplacementIsCode", "an-intersection-chain-is-sorted-and-grouped: ReplacementIsCode", @@ -240,9 +299,15 @@ public void EveryDataRuleIsClassifiedAsWritten() "squared-sine-and-cosine-of-one-argument-sum-to-one: ReplacementDropsHoles", "the-arctangent-of-one-over-root-three: ReplacementIsCode", "the-arctangent-of-root-three: ReplacementIsCode", + "the-negation-of-a-greater-turns-it-round: ReplacementIsCode", + "the-negation-of-a-greaterorequal-turns-it-round: ReplacementIsCode", + "the-negation-of-a-less-turns-it-round: ReplacementIsCode", + "the-negation-of-a-lessorequal-turns-it-round: ReplacementIsCode", "the-two-truth-values-are-the-boolean-domain: ReplacementIsCode", "two-added-fractions-take-a-common-denominator: ReplacementIsCode", "two-arctangents-of-numbers-add-by-the-tangent-formula: ReplacementIsCode", + "two-comparisons-of-one-pair-that-exclude-each-other-are-false: ReplacementIsCode", + "two-comparisons-of-one-pair-that-leave-no-case-are-true: ReplacementIsCode", "two-powers-of-one-exponent-share-a-base: ReplacementIsCode", "two-subtracted-fractions-take-a-common-denominator: ReplacementIsCode", },