IEEE floats

Stream: Is there code for X?

[Geoffrey Irving]

Has anyone formalized the IEEE float rounding semantics in Lean?

I’m specifically interested in whether one could prove the correctness of interval arithmetic and expansion arithmetic routines written in Lean using Lean’s float, then use code extraction to get straight line routines for use in high performance contexts.

[Eric Wieser]

docs#fp.float is the closest thing I'm aware of in Lean 3.

[Eric Wieser]

It's not possible to prove anything useful about the builtin docs#native.float (because it's meta) or docs4#Float (because it's opaque and secretly an alias for Unit!)

[Eric Wieser]

See also this thread in #lean4

[Geoffrey Irving]

But that doesn’t have any of the rounding theorems, right? I.e., “rounded x * y is the closest float to x * y”?

[Geoffrey Irving]

Thanks! That Lean4 thread is a good summary.

[Eric Wieser]

Worse than that, the * that docs#fp.float has is meta (there is a TODO in the source) so you can't even prove anything about it!

[Geoffrey Irving]

Sure, though to clarify I meant fp.float didn’t have those theorems about the non-meta type.

Edit: Ah, I see what you mean.

[Mario Carneiro]

In case it wasn't clear, fp.float is absolutely not supposed to actually be meta, it just was not a high priority to finish those theorems because no one wanted to see it completed

[Mario Carneiro]

So I wouldn't say "you can't prove anything about it", it's rather the other way around - if you prove things about it then it won't need to be meta anymore

[Eric Wieser]

I guess what would be more accurate would be to say is "you can't prove things about the current * without first redefining * to contain the currently missing proofs"?