Substitution, derivatives, expansion, certificates, integrals and roots in lib/cas

Derivatives. cas_diff(e, x) is recursive over the store's DAG and memoized by node, so a shared subexpression is differentiated once. Sums, products and powers have their rules here; a function head takes its derivative from the table that grad.rs reads too, lib/cas/rules/derivatives.toml (through lib/cas/derivs): the adjoint with g = 1, u the argument and y the call itself, times the derivative of the argument. A head with no row is a refusal that names it; there is no silent zero (section 3.7.1).

Expansion. cas_expand(e) multiplies out products of sums and positive integer powers of sums. For a polynomial in any number of symbols, with other subexpressions as coefficients, the result is a canonical form: two equal polynomials expand to the same node.

Certificates. cas_certify_zero(d) shows that d is zero, or that it is not, and says how:

| verdict | means | |---|---| | proved | d is 0 in the normal form, or after expanding (canonical form) | | proved-modular | d is a rational function of its symbols and is 0 mod p = 67108859 at CERT_POINTS random points; a nonzero d of degree at most D passes with probability at most $(D/p{)}^k$ (Schwartz-Zippel) | | probable | d has functions in it; balls around it contain 0 at CERT_POINTS random points. Evidence, not a proof (Richardson's theorem rules out a general proof) | | refuted | a residue that is not 0, or a ball that excludes 0: a proof that d is not 0 | | unknown | no point gave an answer |

Assumptions are per symbol: an interval, set with cas_assume(x, lo, hi) (decision 7, per-symbol facts only). An integral from a to b assumes its variable is in [a, b], which decides whether $\int dx/x$ is $\ln x$ or $\ln (-x)$; with no interval the rule refuses rather than guess the sign. Certificates draw their points from the interval.

Integration is a set of rules, each tried in turn, and every antiderivative is checked by differentiating it before it is returned (cas_antiderivative): linearity; $x^n$ and $\int dx/x$; functions of a linear argument ($e^{ax+b}$, $\sin$, $\cos$, $\sinh$, $\cosh$, powers of $ax+b$); one over a quadratic ($\arctan$ or logarithms); $(c-a{x}^2{)}^{-1/2}$ ($\arcsin$); the Gaussian $e^{-k{x}^2}$ ($\mathrm{erf}$) and its moments $x^n{e}^{-k{x}^2}$; a polynomial times a function of a linear argument, by parts; and the substitution $\int g(u(x))u^{\prime }(x)dx$ when the integrand divided by $g(u)u^{\prime }$ is a constant. What none of them covers is a refusal that says so. This is stage 0 and the start of stage 3's rule set, not Risch.

Roots of a polynomial of degree 1, 2 or 3 with rational coefficients: exact rational roots by the rational root theorem; the quadratic formula, with the square root reduced to a square-free surd; and for a cubic with no rational root, Cardano's formula (one real root) or the trigonometric form (three real roots). Degree 4 and up is a refusal.

Used with import cas.calculus.