# Is it possible to proof a-b+b = a for all double floating-point numbers?

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.

• The equation reduces to a=a, which is rather fundamental. Commented Jun 26, 2018 at 16:05
• a-b+b is not always equal to a, if a, b is floating-point number, for example, if a= 1, and b = 1e100, the results a-b+b = 0 while a = 1. Rounding error lead to the difference.
– Star
Commented Jun 26, 2018 at 16:09
• @Star I think the previous commenter was pointing you towards a subtle distinction; The equation is always trivially true. An implementation may or may not fail due to carry forward of round-off errors from subcalculations. Commented Jun 26, 2018 at 17:43
• 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. Commented Jun 26, 2018 at 17:51
• Thanks for the counterexample by @Kirill. The 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?
– Star
Commented Jun 26, 2018 at 23:26

You can sometimes prove such results (or get counterexamples) using an SMT solver such as Z3 that supports floating point arithmetic. Here is a proof of a version of your theorem that says $|((x+y)-y)-x| \leq 2^{-23}|x|$ when $x>y>1$ and $x+y\neq\infty_{32}$ in 32-bit floating point arithmetic:
λ> import Data.SBV