証明のコードは
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を使ったよりコンパクトな証明をご存知でしたら教えてください。どうもありがとう。
への呼び出しは必要ありません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 を使用して実行されるような形式的な証明であると主張するべきではありません。
興味深いアプローチ。Z3 で極限のイプシロン デルタ定義を使用して、より直接的な証明を行うことができるかどうか疑問に思いました。ここで Z3 への Haskell バインディングを使用してコーディングしました: http://gist.github.com/LeventErkok/5516651
残念ながら、Z3 は生成されたクエリに対して "Unknown" を返しますが、量指定子が必要なため驚くことではありません。z3 がこれを証明できたら、本当に良かったです。
Haskell で生成されたクエリの SMT-Lib 翻訳をここに投稿しました。(機械翻訳は人間が読めるものではありませんが、十分に目を凝らせば、その論理に従うことができます。特に Haskell のソースと比較する場合はそうです。)