Wish: provide a better lemma for rounding error on add and sub for floats
The lemmas round_bound
ieee_float.Float32
and ieee_float.Float64
are providing bounds on rounding arbitrary real number. Lemmas round_bound_ne
are a bit more precise for the NE rounding mode.
Better lemmas should be provided in the case the operand is the addition or subtraction of two floats. In such a case the eta
constant, either 0x1p-149
for 32-bits or 0x1p-1074
for 64-bits, could be made equal to 0.
The proof is already present in Flocq so the realization of such addition lemmas should be easy.