0

The code for the proof is

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))

and the output is

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

Please let me know if you know a more compact proof using Z3Py. Many thanks.

4

2 回答 2

5

您不需要调用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 执行的证明一样，其中每个步骤都在系统中进行了形式化。

于 2013-05-04T17:56:57.893 回答
3

有趣的方法。我想知道是否可以使用 epsilon-delta 限制的定义并在 Z3 中进行更直接的证明。我在这里使用与 Z3 的 Haskell 绑定对其进行了编码：http: //gist.github.com/LeventErkok/5516651

不幸的是，Z3 为生成的查询返回“未知”，由于需要量词，这并不奇怪。如果 z3 能够证明这一点，那就太好了。

我已经在这里发布了 Haskell 生成查询的 SMT-Lib 翻译：http ://rise4fun.com/Z3/igAt如果有人想看看的话。（机械翻译不太适合人类阅读，但如果你足够仔细地眯着眼睛，你可以遵循它的逻辑；特别是如果你将它与 Haskell 源代码进行比较。）

于 2013-05-04T07:35:14.840 回答