I want to know whether the equation : a-b+b = a is always true for a, b belongs to double precision floating-point number and |a|>=|b|.
If the equation is true, how can I proof it?
If not, what precondition can make the equation right?
A counterexample shows the equation is not true, so I now want to know, the inequality |((a-b)+b)-a|<=ulp(a) is true or not, how can I proof the inequality?
I have tested the python code below for half hours, the inequality |a-b+b-a|<=ulp(a) seems hold.
def getulp(x):
x = float(x)
k = frexp(x)[1]-1
if x == 0.0:
return pow(2, -1074)
if (k<1023)&(k>-1022):
return pow(2,k-52)
else:
return pow(2,-1074)
while 1> 0:
k = np.random.randint(-100, 100)
ub = np.float_power(2,k-1)
db = np.float_power(2,k)
j = np.random.randint(-100, 100)
ub2 = np.float_power(2, j - 1)
db2 = np.float_power(2, j)
x = np.random.uniform(ub,db,1)
y = np.random.uniform(ub2,db2,1)
if x>y:
temp = x-y+y
if np.fabs(temp-x)>getulp(x):
print x
print y
print "The inequality false"
else:
temp = y-x+x
if np.fabs(temp-y)>getulp(y):
print x
print y
print "The inequality false"
Thanks for the counterexample by @Kirill, I will explain why I need to proof the equation. I want to proof, image the a, b are two end points of a line, then if I know the value b and a-b, I want to proof that I can get the value of a without error larger than one ULP(a) error. So I can give the condition |a|>=|b| or |a|<=|b|, but I can not limit their actual value.
a=3.9999999981380427, b=1.0000000000000016, (a-b)+b=3.999999998138043≠a
is a counterexample. I also want to point out that the question of what precondition would make it hold is really broad. For example, $2>a>b>1$ is sufficient (I checked with an SMT solver), but is that even helpful? It might help if you said why it is important to you that $(a-b)+b=a$ should hold, that would really narrow down the question. $\endgroup$