The Coq mailing list

[Sylvie Boldo <sylvie.boldo AT inria.fr>]

Hello,

Welcome to my world!
The Frama-C/Why definition of rounding refers to a library of floating-point 
arithmetic definition and properties called PFF (that I maintain) that you must 
have installed. You may find more information in the references [1] and [2].
You can also browse the Coq files from its web page [3].

In your precise case, an integer between 0 and 2^32 is rounded exactly into a 
double precision number, so you can prove that y = x. (it works for any integer 
between -2^53 and 2^53). I made the proof to convince you :) [4].

In a more general case, if you know beforehand the range of your variables and 
if you want to bound their rounding error, I suggest using a tactic that 
automatically solves this kind of goals. J. C. Filliâtre, G. Melquiond and I 
developed this tactic [5] on top of the Gappa tool developped by G. Melquiond. I 
put an example of use at the end of [4].


Hope this helps,

Sylvie Boldo


[1] Marc Daumas, Laurence Rideau and Laurent Théry,
`A Generic Library for Floating-Point Numbers and its Application to Exact 
Computing', TPHOLs2001, LNCS 2152 pp 169-184.
http://hal.archives-ouvertes.fr/docs/00/15/72/85/PDF/DauRidThe01.pdf

[2] Sylvie Boldo. Preuves formelles en arithmétiques à virgule flottante. PhD 
thesis, École Normale Supérieure de Lyon, November 2004.
http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf

[3] http://lipforge.ens-lyon.fr/www/pff/

[4] http://www.lri.fr/~sboldo/TMP/toto_why.v

[5] Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining 
Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the 
Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of 
Lecture Notes in Artificial Intelligence, pages 59-74, Grand Bend, Canada, July 
2009. Springer.
http://www.lri.fr/~filliatr/publis/calculemus09.pdf



On 09/29/2010 08:16 PM, Michael wrote:
> 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,


--
Sylvie Boldo, projet ProVal, INRIA Saclay - Île-de-France
Parc Orsay Université - 4 rue Jacques Monod - 91893 ORSAY Cedex