Order on Float

Stream: lean4

[Bjørn Kjos-Hanssen]

Some strange behavior here, is this by design and/or something that can be easily fixed?

example : (1 : Float) + (2 : Float) ≤ (3 : Float) := by native_decide
example : (1 : Float) + (2 : Float) ≥ (3 : Float) := by native_decide
example : (1 : Float) + (2 : Float) = (3 : Float) := by
        -- native_decide -- doesn't work
        sorry

[Aaron Liu]

example : (1 : Float) + (2 : Float) == (3 : Float) := by native_decide

[Aaron Liu]

while < and ≤ and == can be arbitrary relations, = is much more constrained

[Bjørn Kjos-Hanssen]

Thanks! While we're at it there's also this oddity:

#eval Float.exp ((7 / 144) - Float.exp (6 / 125)) * 100 -- 36.767365
#eval Float.exp ((7 / 144) - Float.exp (6 / 125)) * 100 == 36.767365 -- false

[Aaron Liu]

in particular, this means we can have

example : (0 / 0 : Float) = 0 / 0 := rfl
example : (0 / 0 : Float) != 0 / 0 := by native_decide

[Aaron Liu]

Bjørn Kjos-Hanssen said:

Thanks! While we're at it there's also this oddity:

#eval Float.exp ((7 / 144) - Float.exp (6 / 125)) * 100 -- 36.767365
#eval Float.exp ((7 / 144) - Float.exp (6 / 125)) * 100 == 36.767365 -- false

You need more precision

#eval Float.exp ((7 / 144) - Float.exp (6 / 125)) * 100 == 5174546658963455 / 140737488355328 -- true

[Bjørn Kjos-Hanssen]

Ah, so == isn't even reflexive

[Bjørn Kjos-Hanssen]

How did you find the rational number representation 517...?

[Aaron Liu]

docs#Float.toRat0

[Bjørn Kjos-Hanssen]

Ah, and 140737488355328 = 2^47. Nice!

[Jason Rute]

I think == is in Lean just to support float, so that it behaves like every other programming language (and follows the IEEE standard). I recently answered a question about it on PA.SX. https://proofassistants.stackexchange.com/questions/5212/why-is-boolean-equality-necessary-in-lean-4/5213#5213

[François G. Dorais]

Jason Rute said:

I think == is in Lean just to support float

There's a lot more uses of ==. Another common example: when comparing two Substring, plain = checks that they come from the same underlying string and that they start and end at the same position. This is not at all the most useful way to compare substrings.