Jason Gross (Jul 23 2023 at 01:37): 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?
Jason Gross (Jul 23 2023 at 01:53):(More generally, what's the current best way to prove theorems about computations involving primitive floats?)
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.
Jason Gross (Jul 27 2023 at 22:32):Thank you!
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)
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: Oct 13 2024 at 01:02 UTC