Exercise 4.2.6.4: incorrect simplification of weakest precondition

[qsantos]

In the penultimate step of the correction for exercise 4.2.6.4, we have:

(x < 0 ==> y <  0 ==> -15 <= 0 + 5 - y <= 25) &&
(x < 0 ==> y >= 0 ==> -15 <= 0 - 5 - y <= 25) &&
(x >= 0 ==> y <  0 ==> -15 <= x + 5 - y <= 25) &&
(x >= 0 ==> y >= 0 ==> -15 <= x - 5 - y <= 25) --> (* Simpl *)

(x < 0 ==> y <  0 ==> -20 <= y <= 20) &&
(x < 0 ==> y >= 0 ==> -20 <= y <= 20) &&
(x >= 0 ==> y <  0 ==> -20 <= x - y <= 20) &&
(x >= 0 ==> y >= 0 ==> -20 <= x - y <= 20)

Shouldn't that be:

(x < 0 ==> y <  0 ==> -15 <= 0 + 5 - y <= 25) &&
(x < 0 ==> y >= 0 ==> -15 <= 0 - 5 - y <= 25) &&
(x >= 0 ==> y <  0 ==> -15 <= x + 5 - y <= 25) &&
(x >= 0 ==> y >= 0 ==> -15 <= x - 5 - y <= 25) --> (* Simpl *)

(x < 0 ==> y <  0 ==> -20 <= y <= 20) &&
(x < 0 ==> y >= 0 ==> -30 <= y <= 10) &&
(x >= 0 ==> y <  0 ==> -20 <= x - y <= 20) &&
(x >= 0 ==> y >= 0 ==> -10 <= x - y <= 30)

?

This can then only be simplified to:

(x < 0 ==> -20 <= -y <= 10) &&
(x >= 0 ==> y <  0 ==> x - y <= 20) &&
(x >= 0 ==> y >= 0 ==> -10 <= x - y <= 30)

[AllanBlanchard]

You're right, I missed the minus in both wrong expressions. I'll fix that.

Thank you :)

[AllanBlanchard]

Fixed on master (note that I did not include the last simplification).