用Z3Py online证明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

有趣的方法。我想知道是否可以使用极限的ε-δ定义，并在Z3中做一个更直接的证明。

不幸的是，对于生成的查询，Z3返回"Unknown“，这并不奇怪，因为需要使用量词。

我已经在这里发布了Haskell生成的查询的SMT-Lib翻译：http://rise4fun.com/Z3/igAt，如果有人想看一下的话。(机器翻译不太容易读懂，但如果您仔细观察，就能理解它的逻辑；特别是当您将其与Haskell源代码进行比较时。)

Answer 2

您不需要调用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))

它也可以在here上在线试用。

顺便说一句，我们不应该将这个脚本与x^2的派生为2x的正式证明混淆。这种证明可以在像Coq这样的证明助手中执行。在这里，你可以定义，例如，导数是什么。

您的脚本是一个由自动化工具(Z3)辅助的非正式证明(论点)。该助手(Z3)用于自动计算和证明/解除您的非正式证明的某些步骤。