Prove that floating point addition is not associative. We have:

>>> prove assocPlus
Falsifiable. Counter-example:
  s0 = -7.888609e-31 :: SFloat
  s1 = 3.944307e-31 :: SFloat
  s2 = NaN :: SFloat

Indeed:

>>> let i = 0/0 :: Float
>>> ((-7.888609e-31 + 3.944307e-31) + i) :: Float
NaN
>>> (-7.888609e-31 + (3.944307e-31 + i)) :: Float
NaN

But keep in mind that NaN does not equal itself in the floating point world! We have:

>>> let nan = 0/0 :: Float in nan == nan
False

Prove that addition is not associative, even if we ignore NaN/Infinity values. To do this, we use the predicate isFPPoint, which is true of a floating point number (SFloat or SDouble) if it is neither NaN nor Infinity. (That is, it's a representable point in the real-number line.)

We have:

>>> assocPlusRegular
Falsifiable. Counter-example:
  x = -3.7777752e22 :: SFloat
  y = -1.180801e18 :: SFloat
  z = 9.4447324e21 :: SFloat

Indeed, we have:

>>> ((-3.7777752e22 + (-1.180801e18)) + 9.4447324e21) :: Float
-2.83342e22
>>> (-3.7777752e22 + ((-1.180801e18) + 9.4447324e21)) :: Float
-2.8334201e22

Note the loss of precision in the first expression.

Demonstrate that a+b = a does not necessarily mean b is 0 in the floating point world, even when we disallow the obvious solution when a and b are Infinity. We have:

>>> nonZeroAddition
Falsifiable. Counter-example:
  a = 2.1474839e10 :: SFloat
  b = -7.275957e-11 :: SFloat

Indeed, we have:

>>> 2.1474839e10 + (-7.275957e-11) == (2.1474839e10 :: Float)
True

But:

>>> -7.275957e-11 == (0 :: Float)
False

The last example illustrates that a * (1/a) does not necessarily equal 1. Again, we protect against division by 0 and NaN/Infinity.

We have:

>>> multInverse
Falsifiable. Counter-example:
  a = 1.2354518252390238e308 :: SDouble

Indeed, we have:

>>> let a =  1.2354518252390238e308 :: Double
>>> a * (1/a)
0.9999999999999998