Is IEEE 754 float arithmetic associative, commutative, distributive, etc? Why?

Does the associative/commutative/distributive/etc property hold for arithmetic performed with IEEE 754 floats?

Obviously the answer is no to most of those questions, but do any of the properties of standard arithmetic hold? How can one formulate proofs (or at least proof-like statements) explaining why any particular property does or does not hold?

The IEEE 754 standard defines exactly how floating-point arithmetic is performed. For many interesting theorems, you will need to examine the exact definition. For some less interesting ones, like a+b = b+a or ab = ba, all you need to know that IEEE 754 always calculates the exact result, rounded in a deterministic way. For non-theorems, like (a+b)+c = a+(b+c), which is false, all you need is a counterexample which is usually easy to find.

StackExchange Computer Science Q#90859, answer score: 5