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?)
On the ml side, there is
Float64.to_string. On the vernacular side, I don't think there is anything.
Not even in master ?
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.
Hmm, no printing for now then :)
Shall I add a feature request ?
Do you expect it would be difficult to use the Decimal support ?
If it works for primitive integers, that should be rather easily feasible. How do you handle primitive integers?
Going through Decimal
I might get into a problem later with extraction due to dreaded https://github.com/coq/coq/issues/7017 though...
Also, I don't see much of theory on Floats, e.g. SpecFloat.SFeqb has no associated lemmas showing it decides equality does it?
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
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).
Ok, I'll do that, just showing decidable equality is easy.
Hmm SFeqb does not reflect leibniz equality, it ignores the boolean arguments of
S754_zero for example
Is that actually right?
FloatAxioms.eqb_spec : forall x y : PrimFloat.float, PrimFloat.eqb x y = SpecFloat.SFeqb (FloatOps.Prim2SF x) (FloatOps.Prim2SF y)
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.
I see, I just shouldn't use SpecFloat.SFeqb
Would you consider adding a
repr_eqb function though or is that somehow ill-defined?
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