如何在x = 1時使用Z3RCF-Py來證明diff（x^2，x）= 2？

Question

我使用以下代碼：

eps = MkInfinitesimal() 
print(((1 + eps)**2- 1**2)/eps < 2.00000000001) 
print(((1 + eps)**2- 1**2)/eps > 2) 

並且輸出是：

True 
True 

其他例如：這證明了DIFF（X^2，X）= 2 * PI當x = pi和差異（X^2，X）= 2 * E當x = E

代碼：

eps1 = MkInfinitesimal() 
eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 
pi = Pi() 
e = E() 
print(((pi + eps2)**2- pi**2)/eps2 < 2*pi + eps1) 
print(((pi + eps2)**2- pi**2)/eps2 > 2*pi) 
print(((e + eps2)**2- e**2)/eps2 < 2*e + eps1) 
print(((e + eps2)**2- e**2)/eps2 > 2*e) 

輸出：

True 
True 
True 
True 

其他示例：證明當x = e或x = pi時，diff（x^3，x）= 3 * x^2。

代碼：

eps1 = MkInfinitesimal() 
eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 
pi = Pi() 
e = E() 
print(((pi + eps2)**3- pi**3)/eps2 < 3*pi**2 + eps1) 
print(((pi + eps2)**3- pi**3)/eps2 > 3*pi**2) 
print(((e + eps2)**3- e**3)/eps2 < 3*e**2 + eps1) 
print(((e + eps2)**3- e**3)/eps2 > 3*e**2) 

輸出：

True 
True 
True 
True 

其它示例：

代碼：

[x] = MkRoots([-1, -1, 0, 0, 0, 1]) 
[y] = MkRoots([-197, 3131, -31*x**2, 0, 0, 0, 0, x]) 
[z] = MkRoots([-735*x*y, 7*y**2, -1231*x**3, 0, 0, y]) 
print(x.decimal(10)) 
print(y.decimal(10)) 
print(z.decimal(10)) 
eps1 = MkInfinitesimal() 
eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 
print(((x + eps2)**2- x**2)/eps2 < 2*x + eps1) 
print(((x + eps2)**2- x**2)/eps2 > 2*x) 
print(((y + eps2)**2- y**2)/eps2 < 2*y + eps1) 
print(((y + eps2)**2- y**2)/eps2 > 2*y) 
print(((z + eps2)**2- z**2)/eps2 < 2*z + eps1) 
print(((z + eps2)**2- z**2)/eps2 > 2*z) 

輸出：

1.1673039782? 
0.0629726948? 
31.4453571397? 
True 
True 
True 
True 
True 
True 

這個證明是正確的？如果你知道更好的證據，請告訴我。非常感謝。

Answer 1

這是一個很好的例子。 Z3RCF API將在Z3Py的下一個正式版本中提供。

順便說一句，你可以在Z3RCF中創建許多無窮小。 每一個都比以前創建的無限小。這裏是同樣的例子，但它通過使用兩個不同的無窮小（它也可用於here）來避免2.0000000001。

eps1 = MkInfinitesimal() 
eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 
print(((1 + eps2)**2- 1**2)/eps2 < 2 + eps1) 
print(((1 + eps2)**2- 1**2)/eps2 > 2)