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?

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

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.

Thank you!

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

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