integralRules

The data-driven table of integrals: rewrite rules run through the Rewrite engine.

Every rule here is a RewriteRule, not a compiled case arm. That is the whole point of the hybrid: this table is expected to keep growing, one entry at a time, and a rule added here needs no change to integrate's match.

The integration variable is a pattern variable named v. A rule is written over the integrand, and the binder is matched like any other hole — so ∫ tan(v) dv is the pattern Tg(?v).

?v may bind a linear function of the integration variable, not only the variable itself. A pattern matches a shape, so Tg(?v) alone would cover ∫ tan(x) dx and not ∫ tan(2x) dx — yet the compiled tiers have handled a linear inner argument since the beginning by dividing through by the slope, and there is no reason for the table to be weaker. applyTo therefore requires ?v to bind some a·x + b with a ≠ 0 and divides the instantiated result by a. Every rule in the table gains its chain-rule case from that one place.

That requirement subsumes the "is it the right variable?" check this table needed before: ∫ tan(y) dx binds ?v to y, whose derivative in x is zero, so no rule fires. A non-linear argument (∫ tan(x²) dx) is rejected the same way, which keeps it correctly unsolved rather than wrongly solved.

Consulted only after every compiled arm has declined, so adding a rule cannot change an integral that already works. The corollary is that nothing here duplicates a compiled rule: 1/(1+v²), 1/√(1-v²), v·eᵛ, ln v, sinⁿ v, √v and the rational tier all close earlier, and a second definition of the same fact is only a way for the two to disagree.

Products and sums are matched in the order written. Unification is structural, so Product(Exp(?v), Sin(?v)) does not match sin(x)·exp(x); the commuted spelling of a commutative operand pair is a separate entry, because a user types either one.

Inventory (by section): the base entries (tan, cot, sec, csc, sec·tan, sin·cos, the hyperbolics sinh…csch·coth, ln²v, ln(v)/v, 1/(v·ln v), eᵛ/(1+eᵛ), the cyclic eᵛ·sin v/eᵛ·cos v); the special-integral connections (Si/Ci/Ei/li/erf/Fresnel); and the bulk transcription — symbolic-slope hyperbolics (sinh(a·v) …), the standalone inverse functions (asin … atanh), the remaining hyperbolics (sech, csch, tanh², coth²), the symbolic-a algebraic and radical family (1/(a²−v²), 1/√(a²±v²), 1/√(v²−a²)), the product-to-sum trio (sin(a·v)·cos(b·v) …), the general e^(a·v)·sin/cos(b·v) pair, v·aᵛ and vᵃ — every one verified by the IntegralTableTest harness, which differentiates each rule's rhs back against its lhs at expression level.