OK, so those techniques would work equally well on arbitrarily complicated and intractable code examples -- which is useful in practice but not in the spirit of a formal determination of equality.

From the perspective of an Agda-phobe: The "2*x vs x+x" example could be a case of a general question about arithmetic expressions, or it could even just be about multiplication and addition. Since multiplication of integers can be defined as repeated addition, proving equality in that particular case for any numeric type just takes a rewrite of both sides in terms of addition only. If the coefficient ("2") was not a natural number, things would be a little more complicated (as other comments mention, you'd have to introduce some way of getting things into a canonical form). I guess that would be an "intensional" approach.

The best story I have about extensional definitions is a true one. At a class on bike repair, somebody asked what a fixed-wheel bike was. The instructor started to give an extensional definition: "It's like... a unicycle." Presumably he could have followed this with other examples such as a Penny Farthing -- but the audience seemed satisfied. It would obviously have been more helpful to give an intensional definition ("no gears".)

> I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not.

It would work with Coq's real number type but as the same properties wouldn't always hold with hardware float types, you may have trouble running the program if you extracted it to e.g. Haskell (as your example shows)?

The QuickCheck tests would pass if you allowed a small difference between them to account for floating point inaccuracies I imagine.

In IEEE 2 * x == x + x, which follows from the basic premise that these operations are correct to the nearest float.