證明的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

有趣的方法。我想知道是否可以使用epsilon-delta的極限定義，並在Z3中做更直接的證明。我使用Haskell綁定到Z3對它進行了編碼：http://gist.github.com/LeventErkok/5516651

不幸的是，Z3爲生成的查詢返回「未知」，由於需要量詞，這並不奇怪。如果z3能夠證明這一點真的很好。

我已經發布了哈希克爾生成的查詢的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）正用於自動計算並證明/解除非正式證明的某些步驟。沒有什麼不對，但我們不應該聲稱這是一個形式化的證明，就像使用Coq執行的那樣，每一步都在系統中形式化。