Stream: CUDW 2020

Topic: Primitive Float print in 8.11


view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 09:45):

I'm wondering how to convert a PrimFloat.float to a string (in Coq 8.11), are there any support functions for that (@Pierre Roux maybe?)

view this post on Zulip Pierre Roux (Dec 04 2020 at 09:56):

On the ml side, there is Float64.to_string. On the vernacular side, I don't think there is anything.

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 09:56):

Not even in master ?

view this post on Zulip Pierre Roux (Dec 04 2020 at 10:01):

I don't think so. Something could probably be crafted by recovering the mantissa and exponent and maybe going through Z but that's a bit of work.

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:11):

Hmm, no printing for now then :)

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:11):

Shall I add a feature request ?

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:11):

Do you expect it would be difficult to use the Decimal support ?

view this post on Zulip Pierre Roux (Dec 04 2020 at 10:20):

If it works for primitive integers, that should be rather easily feasible. How do you handle primitive integers?

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:28):

Going through Decimal

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:29):

I might get into a problem later with extraction due to dreaded https://github.com/coq/coq/issues/7017 though...

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:30):

Also, I don't see much of theory on Floats, e.g. SpecFloat.SFeqb has no associated lemmas showing it decides equality does it?

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:31):

Context: I need to show decidable equality on primitive ints/floats to be able to formalize these types in MetaCoq. Only decidable equality will be needed I think

view this post on Zulip Pierre Roux (Dec 04 2020 at 10:38):

If you open an issue pointing to your primitive int implem, I'll try to offer a solution for floats (should be fairly easy).
Regarding the theory, indeed all the actual theory is in Flocq.
For equality, SpecFloat is a simple inductive type so maybe and Equality Scheme would do the job (providedd decidable equality on bool, positive and Z).

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:39):

Ok, I'll do that, just showing decidable equality is easy.

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:53):

Hmm SFeqb does not reflect leibniz equality, it ignores the boolean arguments of S754_zero for example

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 10:56):

Is that actually right?

FloatAxioms.eqb_spec :
forall x y : PrimFloat.float,
PrimFloat.eqb x y = SpecFloat.SFeqb (FloatOps.Prim2SF x) (FloatOps.Prim2SF y)

view this post on Zulip Guillaume Melquiond (Dec 04 2020 at 11:06):

Yes, this is expected. It is the equality as defined by the IEEE-754 standard. If you just want to distinguish two inductive values, using Equality Scheme as proposed by Pierre is the way to go.

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 11:13):

I see, I just shouldn't use SpecFloat.SFeqb

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 11:17):

Would you consider adding a repr_eqb function though or is that somehow ill-defined?

view this post on Zulip Pierre Roux (Dec 04 2020 at 11:22):

That does make sense, if it is properly documented (NaN being already ignored the sign of zero and nan = nan should be the only difference with the IEEE754 equality).


Last updated: Oct 16 2021 at 09:07 UTC