Simplify drops a condition the answer's own domain condition states, read in the codomain

BREAKING-CHANGES.md

@@ -307,17 +307,66 @@ either now; and the secant quotient was simplified to `cos/(b^(5/2) d)` through
 `(1/cos)^(3/2) = cos^(-3/2)`, which is wrong for every negative cosine and cancelled against the
 same wrong step on the denominator. On the 1774-problem independent suites this is 1707 to 1705, the two `asin` rows, with the sign error gone.
 
+### A rational function of a sine over a symbolic quadratic in it is integrated over the two roots
+
+**Improvement, not silent.** `sin(x)/(a + b sin(x) + c sin(x)^2)` and everything rational in
+`sin(x)` and `cos(x)^2` over that quadratic came back unevaluated, or ran past any budget:
+under the half-angle the quadratic in the sine is a quartic in `t` with a symbol in every
+coefficient, which nothing factors, and the substitution `u = sin(x)` wants a cosine above the
+bar that an even power does not give. Written in `s = sin(x)` the integrand is a rational function
+of `s`, divided down and split over the written factors as any is, and the piece over the
+quadratic is taken by the two roots `r = (-b ± sqrt(b^2 - 4ac))/(2c)`, each
+`1/(sin(x) - r)` being `-2 atan((r tan(x/2) - 1)/sqrt(r^2 - 1))/sqrt(r^2 - 1)` for any complex
+`r` — a form checked by differentiation, not a piecewise on the sign of a root, which has no
+value for the conjugate pair the ordinary coefficients give. The cosine the same way, with
+`-2 atan(tan(x/2)/σ)/((1 + r) σ)`, `σ = sqrt((r - 1)/(r + 1))`. On each interval between the
+poles of `tan(x/2)`, as every half-angle answer.
+
+| | Was | Is |
+|---|---|---|
+| `"1/(a+b*sin(x)+c*sin(x)^2)".Integrate("x")` | unevaluated | the two arctangents over `sqrt(b^2 - 4ac)` |
+| `"sin(x)^4/(a+b*sin(x)+c*sin(x)^2)".Integrate("x")` | unevaluated after more than three minutes | `(x - sin(2x)/2)/(2c) + b cos(x)/c^2 + (b^2 c - a c^2) x/c^4 + …` in 70 ms |
+| `"csc(x)^2/(a+b*sin(x)+c*sin(x)^2)".Integrate("x")`, `"sec(x)^2/…"` | unevaluated | `-cot(x)/a + …`, the blocks over `sin^2` and `1 - sin^2` beside the two roots |
+| `"1/(a+b*cos(x)+c*cos(x)^2)".Integrate("x")` | unevaluated | the cosine form |
+
+### A function comes out of a fractional power of its even power with its sign
+
+**Improvement, not silent.** The entry two above made `(sin(x)^2)^(3/2)` the modulus `|sin(x)|^3`
+and left three of Rubi's integrands unevaluated for it, and answered two more in powers of the
+modulus through the substitutions. The modulus is the function times its sign, and the sign is a
+constant between the function's zeros: `(a sin(x)^2)^(5/2)` is `a^(5/2) sgn(sin(x)) sin(x)^5`, the
+sign comes out in front of the integral, and what is left is a whole power any rule reads. An even
+power of a real function is not negative, so `(c q)^p = c^p q^p` holds for the principal powers
+whatever `c` is, and nothing is assumed about the constant — checked at `a = -3` as well as
+`a = 2`. Whole products of the exponents only, at the top of the integration only, and after the
+rule that does the same for a polynomial under a square root, whose answers are as they were.
+[#1387](https://github.com/asc-community/AngouriMath/issues/1387)
+
+| | Was | Is |
+|---|---|---|
+| `"x*sqrt(sin(x)^2)".Integrate("x")` | unevaluated | `sgn(sin(x)) (sin(x) - x cos(x))` |
+| `"(csc(x)^2)^(3/2)".Integrate("x")`, `"1/(csc(x)^2)^(7/2)".Integrate("x")` | unevaluated | `sgn(csc(x))` times the integral of `csc^3`, of `sin^7` |
+| `"(sin(x)^2)^(3/2)".Integrate("x")` | `(2/3 tan(x/2)^5 + 2 tan(x/2)^3) ((2 tan(x/2))^2)^(1/2)/((tan(x/2)^2 + 1)^3)` | `sgn(sin(x)) (cos(x)^3/3 - cos(x))` |
+| `"(a*sin(x)^2)^(5/2)".Integrate("x")` | `sgn(sin(x)) a^(5/2) (...)` in `(1 - abs(sin(x))^2)^(1/2)` over `sgn(cos(x))` | `sgn(sin(x)) a^(5/2) (2 cos(x)^3/3 - cos(x) - cos(x)^5/5)` |
+| `"1/sqrt(a*cot(x)^2)".Integrate("x")` | `-sgn(tan(x)) ln(1/sqrt(1 + abs(tan(x))^2))/sqrt(a)` | `sgn(cot(x)) ln(1 + tan(x)^2)/(2 sqrt(a))` |
+| `"(b*tan(x)^2)^(5/2)".Integrate("x")` | `sgn(tan(x)) b^(5/2) ((abs(tan(x))^2)^2/2 - abs(tan(x))^2 + ln(abs(tan(x))^2 + 1))/2` | the same with `tan(x)` for `abs(tan(x))` |
+
 ### A condition the answer states on its own is no longer repeated beside it
 
 **Improvement, not silent.** `Simplify` returned `(1 - ln(x))/x^2 provided not x = 0` for the
 derivative of `ln(x)/x`, and `(1 + ln(x)) x^x provided not x = 0` for that of `x^x`. The quotient
 by `x^2`, the `ln(x)` and the `0^0` are each undefined at zero already, so the condition excluded
 a point the expression never reached and said twice what the expression says once. A `provided`
-whose condition the expression proves on its own — a quotient by `d`, a negative power of `d`, a
-logarithm of `d` or to the base `d`, `d^f` with `f` vanishing too, for `d` the condition's `e`,
-a positive power of it, a product holding it, a polynomial in the variable `e` is with no constant
-term, or a polynomial that is zero at the root of a linear `e` — comes back without that
-conjunct. Only the answer is read this way, and only its top: inside a piecewise a predicate
+whose condition the expression proves on its own — whose own domain condition, read in the
+ambient codomain (`DomainConditionIn`), already excludes the zeros of the condition's `e`: a
+conjunct `not d = 0` or `d > 0` with `d` being `e` itself, a positive power of it, a product
+holding it, a sine, tangent, arcsine or arctangent of such a thing, a polynomial in the variable
+`e` is with no constant term, or a polynomial that is zero at the root of a linear `e`, or a
+disjunction every side of which does, as `x^x`'s `not x = 0 or x > 0` — comes back without that
+conjunct. Decided by the domain condition rather than by the shape of the node, so it follows
+the codomain: when [#217](https://github.com/asc-community/AngouriMath/issues/217) gives `1/0`
+a value under the codomains that admit a complex infinity, the quotient's domain condition
+changes there and the condition beside `1/x` stops being redundant, with no change to the rule. Only the answer is read this way, and only its top: inside a piecewise a predicate
 decides which case is taken and stays; inside the simplifier's own search a `provided` is what
 rules read as "this candidate needs a condition" and stays too. A condition the expression does
 not state is kept — `x/x` simplifies to `1 provided not x = 0` as before, since `1` no longer
@@ -329,6 +378,7 @@ says it. [#1394](https://github.com/asc-community/AngouriMath/issues/1394)
 | `"x^x".Differentiate("x").Simplify()` | `(1 + ln(x)) x^x provided not x = 0` | `(1 + ln(x)) x^x` |
 | `"x^n".Differentiate("x").Simplify()` | `x^n n/x provided not x = 0` | `x^n n/x` |
 | `"1/(x^2 + x) provided not x = 0 and not x + 1 = 0".Simplify()` | unchanged | `1/(x^2 + x)` |
+| `"tan(x) provided not cos(x) = 0".Simplify()`, `"sin(x)/x provided not x = 0".Simplify()` | unchanged | `tan(x)`, `sin(x)/x` |
 | `"(x + sin(x))/x".Limit("x", "+oo")` | unevaluated | `1`, by the squeeze theorem on `sin(x)/x` once the division no longer carries the condition between the terms |
 
 ### The Pythagorean pair is found anywhere in a sum

Sources/AngouriMath/Docs/Contributing/SimplificationContract.md

@@ -79,15 +79,22 @@ use it rather than invent a test.
 
 ### `Providedf` — a condition carried on the value
 
-`expr provided condition` says: this equals `expr` where `condition` holds, and is undefined
+`expr provided condition` says: this equals `expr` where `condition` holds, and has no value
 otherwise. `Simplify` already produces it — `x/x` gives `1 provided not x = 0` — and `Entity.Provided`
 drops the condition when it is `True`, so nothing is attached where nothing is needed.
 
-Two costs to know before reaching for it. A condition **competes on complexity**, because `Simplify`
-ranks candidates by node count, so attaching one can make a better form lose. And a condition
-**travels**: it propagates outward and can escape a binder
-([#878](https://github.com/asc-community/AngouriMath/issues/878)), and a single `NaN` condition inside
-a `Piecewise` collapses the whole node.
+**A condition the expression's own domain condition already states is redundant, and `Simplify`
+drops it.** `x^x provided not x = 0` is `x^x` and `1/x provided not x = 0` is `1/x`: what an
+expression accepts under a codomain is what `DomainConditionIn` says — a nonzero divisor, a
+nonzero base or a positive exponent, a nonzero antilogarithm over the complex plane and a positive
+one over the reals — and a `provided` that only excludes points that condition already excludes
+says nothing. The decision is made against the domain condition read in the ambient codomain, not
+against the shape of the node, so it follows the codomain: when
+[#217](https://github.com/asc-community/AngouriMath/issues/217) gives `1/0` a value under the
+codomains that admit a complex infinity, the quotient's domain condition changes there and the
+`provided` beside `1/x` stops being redundant, with no change to the rule. A condition the
+expression does not state stays: `x/x` becomes `1 provided not x = 0`, and `1` says nothing about
+zero ([#1394](https://github.com/asc-community/AngouriMath/issues/1394)).
 
 ## 3. Four things that are not the same
 

Sources/AngouriMath/Docs/Usage/Comparison.md

@@ -110,6 +110,11 @@ library answers `x + 1 provided not x - 1 = 0`. Same for `x/x + 0*y`. Carrying a
 singularity costs the shorter output on those rows and is deliberate — see
 [SimplificationContract.md](../Contributing/SimplificationContract.md), which is where a rewrite's
 right to attach or drop such a condition is set out.
+The two differentiation rows are the other
+half of the same trade, and they no longer carry the condition: the quotient by `x^2` and the
+`0^0` each exclude zero by their own domain condition, so a `provided not x = 0` beside them said
+what the expression already says, and `Simplify` drops a condition its answer's domain condition
+already states.
 
 The two equal-length rows differ by collection and ordering: `1 + 3 * x ^ 2 + 4 * x` against
 `1 + 4*x + 3*x^2` is the same polynomial written in a different order.

Sources/AngouriMath/Functions/PredicateEntailment.cs

@@ -154,26 +154,30 @@ private static bool TryRead(Entity predicate, out Entity subject, out bool above
         /// </summary>
         /// <remarks>
         /// <para>
-        /// <c>(1 - ln(x))/x^2 provided not x = 0</c> is <c>(1 - ln(x))/x^2</c>: the quotient is
-        /// undefined at zero, so the condition excludes a point the expression does not reach,
-        /// and a reader is told twice what the expression says once. The same for
-        /// <c>(1 + ln(x)) x^x provided not x = 0</c>, where <c>ln(0)</c> and <c>0^0</c> are both
-        /// undefined. https://github.com/asc-community/AngouriMath/issues/1394
+        /// <c>(1 + ln(x)) x^x provided not x = 0</c> is <c>(1 + ln(x)) x^x</c>: <c>0^0</c> has no
+        /// value, so the condition excludes a point the expression does not reach, and a reader
+        /// is told twice what the expression says once.
+        /// https://github.com/asc-community/AngouriMath/issues/1394
         /// </para>
         /// <para>
-        /// <b>Sound whichever way "undefined" is read.</b> A <c>provided</c> says the expression
-        /// has no value where its condition fails; dropping it changes nothing where the
-        /// expression already has no value there, whether that absence is written <c>NaN</c> or
-        /// a complex infinity (https://github.com/asc-community/AngouriMath/issues/217). What has
-        /// to be proven is that the expression <em>is</em> undefined at every zero of <c>e</c>,
-        /// and it is proven only structurally: a quotient by <c>d</c>, a negative power of
-        /// <c>d</c>, a logarithm of <c>d</c> or to the base <c>d</c>, or <c>d^f</c> with <c>f</c>
-        /// vanishing too, where <c>d</c> is <c>e</c> itself, a positive power of it, a product
-        /// holding it, or a polynomial in the variable <c>e</c> is with no constant term. Every
-        /// such node is undefined at the zeros of <c>e</c>, and an undefined operand makes the
-        /// whole expression undefined, since no operation here absorbs one. Anything not proven
-        /// keeps its condition: a false negative is a redundant clause, a false positive would
-        /// claim a value at a point.
+        /// <b>Decided by the expression's own domain condition, under the codomain.</b> A
+        /// <c>provided</c> says where the expression has a value, so a condition is redundant
+        /// exactly where the expression has none in the codomain the question is asked in --
+        /// and what an expression accepts under a codomain is what
+        /// <see cref="Entity.DomainConditionIn"/> already says: a quotient accepts a nonzero
+        /// divisor, a power a nonzero base or a positive exponent, a logarithm a nonzero
+        /// antilogarithm over the complex plane and a positive one over the reals, and so on
+        /// through every node. The condition is redundant where that domain condition already
+        /// excludes the zeros of <c>e</c>: a conjunct <c>not d = 0</c> or <c>d &gt; 0</c> with
+        /// <c>d</c> vanishing at them -- <c>d</c> being <c>e</c> itself, a positive power of it, a
+        /// product holding it, a sine, tangent, arcsine or arctangent of such a thing, or a
+        /// polynomial in the variable <c>e</c> is with no constant term -- or a disjunction every
+        /// side of which does. Nothing here decides what a node accepts; that stays with the
+        /// node, and when a complex infinity is written
+        /// (https://github.com/asc-community/AngouriMath/issues/217) and a quotient's domain
+        /// condition changes under the codomains that admit it, this follows. Anything not
+        /// proven keeps its condition: a false negative is a redundant clause, a false positive
+        /// would claim a value at a point.
         /// </para>
         /// <para>
         /// Decided on the expression as it stands, which matters: <c>x/x provided not x = 0</c>
@@ -216,27 +220,41 @@ private static Entity Without(Entity expression, Entity predicate)
             };
 
         /// <summary>
-        /// Whether <paramref name="expression"/> has a node that is undefined wherever
-        /// <paramref name="e"/> is zero.
+        /// Whether <paramref name="expression"/> has no value wherever <paramref name="e"/> is
+        /// zero, by its own domain condition read in the ambient codomain
+        /// (<see cref="Entity.DomainConditionIn"/>): the condition excludes the zeros of
+        /// <paramref name="e"/> where a conjunct <c>not d = 0</c> or <c>d &gt; 0</c> has <c>d</c>
+        /// vanishing with <c>e</c>, or a disjunction has every side excluding them --
+        /// <c>x^x</c>'s <c>not x = 0 or x &gt; 0</c>.
         /// </summary>
         private static bool IsUndefinedAtTheZerosOf(Entity expression, Entity e)
-            => expression.Nodes.Any(node => node switch
+            => ExcludesTheZerosOf(expression.DomainConditionIn(MathS.Settings.Codomain), e);
+
+        private static bool ExcludesTheZerosOf(Entity condition, Entity e)
+            => condition switch
             {
-                Divf(_, var d) => VanishesWith(d, e),
-                Powf(var d, var power) => VanishesWith(d, e) && (power.Evaled is Real { IsNegative: true } || VanishesWith(power, e)),
-                Logf(var @base, var antilogarithm) => VanishesWith(antilogarithm, e) || VanishesWith(@base, e),
+                Andf(var left, var right) => ExcludesTheZerosOf(left, e) || ExcludesTheZerosOf(right, e),
+                Orf(var left, var right) => ExcludesTheZerosOf(left, e) && ExcludesTheZerosOf(right, e),
+                Notf(Equalsf(var d, var zero)) when zero.Evaled is Complex { IsZero: true } => VanishesWith(d, e),
+                Notf(Equalsf(var zero, var d)) when zero.Evaled is Complex { IsZero: true } => VanishesWith(d, e),
+                Greaterf(var d, var zero) when zero.Evaled is Complex { IsZero: true } => VanishesWith(d, e),
                 _ => false,
-            });
+            };
 
         /// <summary>
         /// Whether <paramref name="d"/> is zero wherever <paramref name="e"/> is: <c>d</c> is
-        /// <c>e</c>, a positive power of it, a product with such a factor, or -- for a variable
-        /// <c>e</c> -- a polynomial in it without a constant term.
+        /// <c>e</c>, a positive power of it, a product with such a factor, a sine, tangent,
+        /// arcsine or arctangent of such a thing, or -- for a variable <c>e</c> -- a polynomial
+        /// in it without a constant term.
         /// </summary>
         private static bool VanishesWith(Entity d, Entity e)
         {
             if (d == e)
                 return true;
+            // A function that is zero at zero, of something that vanishes: `sin(x)/x` is `0/0`
+            // at zero.
+            if (d is Sinf or Tanf or Arcsinf or Arctanf)
+                return VanishesWith(d.DirectChildren[0], e);
             if (d is Powf(var @base, var power) && power.Evaled is Real { IsPositive: true })
                 return VanishesWith(@base, e);
             if (d is Mulf)

Sources/Tests/UnitTests/Core/ProvidedImpliedByTheExpressionTest.cs

@@ -13,10 +13,10 @@ namespace AngouriMath.Tests.Core
 {
     /// <summary>
     /// A <c>provided</c> condition the expression states on its own is dropped: <c>1/x provided
-    /// not x = 0</c> is <c>1/x</c>, since the quotient has no value at zero whether or not a
-    /// condition says so. Only where the expression proves it -- a quotient, a negative power, a
-    /// logarithm, <c>0^0</c> -- and on the expression as it stands after simplification, so that
-    /// <c>x/x</c>, which becomes <c>1</c>, keeps the condition it can no longer state.
+    /// not x = 0</c> is <c>1/x</c>, since the quotient's own domain condition, read in the
+    /// ambient codomain, already excludes zero. Only where that domain condition proves it, and
+    /// on the expression as it stands after simplification, so that <c>x/x</c>, which becomes
+    /// <c>1</c>, keeps the condition it can no longer state.
     /// https://github.com/asc-community/AngouriMath/issues/1394
     /// </summary>
     [Trait("Area", "Core")]
@@ -28,6 +28,8 @@ public sealed class ProvidedImpliedByTheExpressionTest
         [InlineData("1/x provided not x = 0", "1/x")]
         [InlineData("x^(-2) provided not x = 0", "1/x^2")]
         [InlineData("ln(x) provided not x = 0", "ln(x)")]
+        [InlineData("sin(x)/x + x^x provided not x = 0 and not y = 0", "sin(x)/x + x^x provided not y = 0")]
+        [InlineData("tan(x) provided not cos(x) = 0", "tan(x)")]
         [InlineData("1/(x * y) provided not x = 0 and not y = 0", "1/(x * y)")]
         [InlineData("1/(x^2 + x) provided not x = 0 and not x + 1 = 0", "1/(x^2 + x)")]
         [InlineData("1/(x^2 + x) provided not x = 0 and not y = 0", "1/(x^2 + x) provided not y = 0")]
@@ -49,8 +51,8 @@ public void ADerivativeStatesItsOwnDomain(string function, string derivative)
 
         /// <summary>
         /// A condition the expression does not state stays: the one on a quotient that has
-        /// cancelled, and one about a symbol the expression no longer holds, and one about a
-        /// factor beside the one the quotient is by.
+        /// cancelled, one about a symbol the expression no longer holds, and one about a factor
+        /// beside the one the quotient is by.
         /// </summary>
         [Theory]
         [InlineData("x / x provided not x = 0")]