Stream: Coq users

Topic: Working with primitive floats


view this post on Zulip Jason Gross (Jul 23 2023 at 01:37):

Are there any libraries (flocq?) that have conversions between Coq's primitive floats and Q, and prove theorems about the bounds on error in conversion?

view this post on Zulip Jason Gross (Jul 23 2023 at 01:53):

(More generally, what's the current best way to prove theorems about computations involving primitive floats?)

view this post on Zulip Guillaume Melquiond (Jul 23 2023 at 05:18):

You can use the lemma Bdiv_correct_aux from Flocq to compute the quotient of two arbitrary integers: https://flocq.gitlabpages.inria.fr/flocq/html/Flocq.IEEE754.BinarySingleNaN.html#Bdiv_correct_aux (As the name implies, it is supposed to be a private lemma, but CompCert already uses it for that exact same purpose.) Then you can use SF2Prim to get the actual primitive number. More generally, https://flocq.gitlabpages.inria.fr/flocq/html/Flocq.IEEE754.PrimFloat.html contains all the theorems needed to switch to Flocq(s formalism, and subsequently to errors bounds.

view this post on Zulip Jason Gross (Jul 27 2023 at 22:32):

Thank you!

view this post on Zulip Jason Gross (Jul 27 2023 at 22:33):

Is there a good place to ask questions about flocq? (There doesn't seem to be a stream for it)

view this post on Zulip Karl Palmskog (Jul 28 2023 at 09:01):

if there's no stream for something, this is the default stream where questions should go (unless it's related to Coq development)


Last updated: Jun 13 2024 at 19:02 UTC