Pattern matching on float

Stream: lean4

[Andrés Goens]

I tried pattern matching on floats and it seems to fail. I presume it's because Float is opaque. Is there anything I could do to make this go through?

def Float.isZero : Float -> Bool
  | 0 => true
  | _ => false
/-
dependent elimination failed, type mismatch when solving alternative with type
  motive (Float.ofScientific 0 false 0)
but expected
  motive x
-/

[Martin Dvořák]

I am not surprised because = doesn't work on floats either.

[Tomas Skrivan]

Is Float.isZero -0 true or false? :) Yeah Float is a bit messed up here and there is a reason no decidable equality is defined on Float. For "deciding" float equality x = y I'm using x ≤ y && y ≤ x.

[Martin Dvořák]

Does x ≤ y && y ≤ x ever give a different result than x == y on Floats?

[Tomas Skrivan]

:man_facepalming: I didn't notice that Float has BEq

[Henrik Böving]

Martin Dvořák said:

Does x ≤ y && y ≤ x ever give a different result than x == y on Floats?

I would ask that the IEEE standard

[Henrik Böving]

knowing how funky said standard can be my bet is: yes

[MangoIV]

What does it give on NaN and NaN

[Ruben Van de Velde]

false

[Mario Carneiro]

Henrik Böving said:

Martin Dvořák said:

Does x ≤ y && y ≤ x ever give a different result than x == y on Floats?

I would ask that the IEEE standard

I think that one is actually true (that is, there are no such counterexamples)