Library Floats

Axiomatization of floating-point numbers.

In contrast with what we do with machine integers, we do not bother to formalize precisely IEEE floating-point arithmetic. Instead, we simply axiomatize a type float for IEEE double-precision floats and the associated operations.





Require Import Coqlib.

Require Import Integers.




Parameter float: Type.




Module Float.




Parameter zero: float.

Parameter one: float.




Parameter neg: float -> float.

Parameter abs: float -> float.

Parameter singleoffloat: float -> float.

Parameter intoffloat: float -> int.

Parameter intuoffloat: float -> int.

Parameter floatofint: int -> float.

Parameter floatofintu: int -> float.




Parameter add: float -> float -> float.

Parameter sub: float -> float -> float.

Parameter mul: float -> float -> float.

Parameter div: float -> float -> float.




Parameter cmp: comparison -> float -> float -> bool.




Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}.

Below are the only properties of floating-point arithmetic that we rely on in the compiler proof.





Axiom addf_commut: forall f1 f2, add f1 f2 = add f2 f1.




Axiom subf_addf_opp: forall f1 f2, sub f1 f2 = add f1 (neg f2).




Axiom singleoffloat_idem:

  forall f, singleoffloat (singleoffloat f) = singleoffloat f.




Axiom cmp_ne_eq:

  forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2).

Axiom cmp_le_lt_eq:

  forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2.

Axiom cmp_ge_gt_eq:

  forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2.




Axiom eq_zero_true: cmp Ceq zero zero = true.

Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false.




End Float.