Unfounded (floating point) compiler optimizations

These are from Xavier Leroy's POPL 2011 talk.

Thou shalt not assume…	although you can assume…
x == x	x == y ⇔ x - y == 0
x <= y ⇔ ¬(x > y)	x <= y ⇔ x < y ∨ x == y
x == y ⇒ 1/x == 1/y	x == y ⇒ 1 + x == 1 + y
x / 10 == x * 0.1	x / 8 == x * 0.125
x + (y + z) == (x + y) + z	x + y = y + x
x * (y * z) == x	x * y = y * x
rnd64(rnd80(op)) == rnd64(op)	rnd32(rnd64(op)) == rnd32(op)