DecidableEq for Float?

Stream: lean4

[Geoffrey Irving]

It looks like Float doesn't have a DecidableEq instance. Is that right, and is it intentional if so? I realize it can't have LawfulBEq due to NaN, but that doesn't seem like it should block DecidableEq.

[Geoffrey Irving]

I suppose it would be easy to accidentally use = instead of == if DecidableEq existed, with resulting different behavior.

[Ruben Van de Velde]

If it did, it would have to NaN = NaN, right?

[Geoffrey Irving]

Yes, by rfl.

[Eric Wieser]

DecidableEq is impossible for Float because you can't prove anything at all about float

[Geoffrey Irving]

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Float.html#Float.decLt

[Geoffrey Irving]

Are you thinking of Lean 3?

[Eric Wieser]

Oh, I guess that's not quite true; you can prove everything that's in docs#FloatSpec

[Eric Wieser]

So it is indeed weird that DecidableEq is not in that structure, when everything else is

[Geoffrey Irving]

I think the foot canon of = vs. == when writing Float code might explain it. I think it may be weird formally but not weird in practice because of that.

[Henrik Böving]

Geoffrey Irving said:

I think the foot canon of = vs. == when writing Float code might explain it. I think it may be weird formally but not weird in practice because of that.

But how would you treat the NaN case? NaN is not supposed to be equal to itself.

[Eric Wieser]

Sure, but plenty of languages fail at that anyway

[Geoffrey Irving]

We're not talking about changing any semantics: it has to be true that NaN = NaN and NaN != NaN.

[Geoffrey Irving]

And it is also true as a meta-mathematical fact that = is decidable over Float.

[Geoffrey Irving]

The only question is whether to make that fact available to programmers.

[Eric Wieser]

Eric Wieser said:

Sure, but plenty of languages fail at that anyway

To elaborate, python has a stronger version of == that sometimes surfaces from behind the scenes:

>>> nan = float('nan')
>>> d = {nan: 'oh no'}
>>> d[nan]
'oh no'
>>> d[float('nan')]
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
KeyError: nan
>>>

[Eric Wieser]

If we want to guard against the = footgun on floats, that presumably can be handled by a linter; I don't think it is useful to cripple the = notation (by making it need open Classical, as it does today)

[Eric Wieser]

Here's a hack in the meantime that avoids needing to change core:

import Mathlib.Logic.Basic

unsafe def instDecidableEqFloatStupid : DecidableEq Float := fun f g => if toString f == toString g then .isTrue lcProof else .isFalse lcProof

@[instance, implemented_by instDecidableEqFloatStupid]
opaque instDecidableEqFloat : DecidableEq Float := Classical.decEq _

[Eric Wieser]

(it would be great if https://github.com/pygments/pygments/pull/2618 could land so that unsafe and opaque got highlighted there...)

[Geoffrey Irving]

How does that work? I don't think Float.toString is injective.

[Geoffrey Irving]

And of course, if we implement this, we do want the fast native version.

[Eric Wieser]

Geoffrey Irving said:

How does that work? I don't think Float.toString is injective.

Ah, I guess we're in trouble because of how many different NaNs there are, which indeed share a toString.

[Geoffrey Irving]

Well, that's one problem...

#eval (1e-10 : Float).toString
-- "0.000000"

[Eric Wieser]

Oh, I naively assumed that Lean would be using something like dragon4 for unambiguous (finite) float printing like NumPy does

[Geoffrey Irving]

That would be better, I agree. Though unrelated to DecidableEq which maps to a single assembly instruction.

[Geoffrey Irving]

I would certainly prefer it if 1e-10 didn't show up as 0, as it makes unit tests slightly harder to debug.

[Eric Wieser]

At risk of further derailment; is there any builtin way to print 1e-10 at higher precision?

[Geoffrey Irving]

printf("%.17g", x) is (mostly) injective in C, so if we have access to format strings then yes.

[Mario Carneiro]

@Eric Wieser There is an implementation of toStringFull either in zulip or in std (std4#282)

[Mario Carneiro]

My understanding of the lean model of Float is that it identifies all NaNs (sign included) and otherwise distinguishes all bit patterns (including 0 vs -0)