从Semantic多项式求导[#83]

本例把坐标与多项式作为Semantic值构造，然后调用只接受Semantic输入的核心API：

$x^3+2x$的求导结果是 $3x^2+2$。

◆:coordinate同时携带变量身份和独立坐标声明，所以#:assumptions (list x)足以告诉计算器对哪个量求导。math-differentiate先产生形式导数，再交给化简pass。结果是3*x^2 + 2。

查看执行结构，而不是猜测内部做了什么：

passes: (differentiate simplify)ncomplete: #t

计算报告还分别保留三种核验结果：证书边是否可重放、求导契约是否通过，以及Proof IR是否能把每条边解释为已证明的规则应用。

用math-report-audit可以从求导或积分的报告中取得这一组独立结果。重放检查逐条边是否符合记录的规则；契约检查用独立的多项式算法语义核对输入与终值；Proof IR检查所用规则是否有可核验的定理和前提。三个字段回答不同问题，不能压成一个“已验证”布尔值。报告本身的math-report-status仍回答计算是否完成或触及限制；例如一个可重放的前缀不代表它已经算出了满足契约的结果。

各层状态也要分别读：重放以布尔值表示证书是否通过；契约状态semantically-checked表示契约成立，rejected表示证据与契约冲突，unsupported表示检查器不能判断该对象；Proof IR的checked表示整条等式推理链有已检查的依据，unsupported表示至少有一步还没有这样的依据。因而此例的Proof IR为unsupported不表示求导结果错误，而是表示现有定理库尚未为若干求导算法规则提供证明。

遇到步数上限时，报告仍附有当前证书的audit；读者可以区分“已有前缀可重放”与“求导尚未完成”：

calculation: cutoff; replay: #t; contract: unsupported

replay: #t; contract: semantically-checked; Proof IR: unsupported (("the rule is outside the rational-polynomial checker" "the rule is outside the rational-polynomial checker" "the rule is outside the rational-polynomial checker" "the rule is outside the rational-polynomial checker" "the rule is outside the rational-polynomial checker" "the rule is outside the rational-polynomial checker" "rule has no fixed RuleSpec to elaborate"))

第一行列出报告经过的pass，第二行说明结果是否完整。求导项的生成和代数化简是不同工作，所以保留为不同pass。