The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I have Coq proof created from a C source file where multiple roundings (from
casts) occur:

H0 : double_value y = round_double nearest_even x (* y : double, x : Z, 0 <= x
< 2^32 *)

What I need to have is an estimation (not necessarily a perfect one) of the
error, in other words I'd like to create a Hypothesis like
H1 : x - err <= y <= x + err
with a given exact err. err ~= 0.1 would, in my case, already be sufficient.

I started unfolding the definitions with
unfold round_double in H0.
unfold round_double_aux in H0.
unfold double_value in H0.
simpl in H0.

which resultet in

H0 : df y = RND_EvenClosest bdouble radix 53 x

Now I'm stuck, and I don't know how to handle the rounding to get what I need.

I hope somebody can explain to me how to handle floating point arithmetics 
like
these.

Sincerely,