在线使用Z3Py证明x ^ 2的导数是2x

Question

证明的代码是

x, d = Reals('x d')
t = (simplify(simplify(((x + d)**2 - x**2)/d, som = True), mul_to_power=True))
print t
prove(Implies(d != 0, t == 2*x + d))
prove(Implies(d == 0, 2 * x + d == 2*x))

而输出是

(2·d·x + d2)/d
proved
proved

如果你知道使用Z3Py的更紧凑的证据,请告诉我.非常感谢.

Answer 1

你不需要打电话simplify.你可以写

x, d = Reals('x d')
t = ((x + d)**2 - x**2)/d
print t
prove(Implies(d != 0, t == 2*x + d))
prove(Implies(d == 0, 2 * x + d == 2*x))

它也可以在这里尝试在线.

顺便说一句,我们不应该有一个正式的证明的衍生混淆这个脚本x^2是2x.这种证明可以在像Coq这样的证明助手中进行.在那里,您定义了例如衍生物是什么.

您的脚本是一个非正式的证明(参数),由自动化工具(Z3)辅助.助手(Z3)用于自动计算并证明/解除非正式证明的一些步骤.这没有任何问题,但我们不应该声称这是一个正式的证据,就像使用Coq执行的那样,其中每个步骤都在系统中形式化.