RFC: add definitions for Float and Float32

[Rob23oba]

Proposal

Add some definitions for simple floating point operations like additions, multiplication, division, etc.
I have a simple draft here: https://github.com/Rob23oba/lean4/blob/float-definitions/src/Init/Data/Float.lean
I decided to do an RFC first instead of immediately a PR though because this might be controversial.
The reason you'd want to have this is to in general allow reasoning about floats, even if we don't actually define any theorems in Init directly: without such definitions, reasoning about floats is completely impossible unless you add auxiliary axioms that declare that the floating point numbers work as expected (which is not preferable). Floats actually do have capabilities for approximate reasoning (e.g. if floats a and b are at most 1 ulp away from rational numbers x and y respectively then a + b is at most 3 ulps away from x + y) and to get access to such reasoning you would otherwise need to redefine your own floats which is also weird because then you'd have two types for the same thing!
An example of something I would find this useful for is the formalization of video games (or of course programs in general).
I don't expect the theorems or whatever to be in Init or core lean in general though, they'd probably live in some part of batteries or mathlib instead, this is just supposed to be a simple definition of the functions that would be used externally.
I am aware that this creates some kind of maintainability problem though because changes to these definitions would also need to be accompanied by changes to any kind of proof infrastructure on batteries or mathlib or whereever. My hope is that the definitions won't need to be changed after being written but that obviously means that they need to be correct and that there's nothing about the definitions worth changing. Because of that, I'm very much okay with any kind of small improvement suggestions and, of course, "bug reports" on the definitions (e.g. any special cases I missed?).
In general, feedback and discussion is very much appreciated.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

Hi, thanks for creating this RFC. Float specs are a delicate issue, what we would need to see here at minimum to consider inclusion is a full-featured, robust implementation out of core with references to the literature and prior work. Then a new RFC for upstreaming this work could be opened.

[digama0]

I am in favor of developing a flocq port as part of batteries with an eye to upstreaming it eventually.

[Rob23oba]

How do you think should the floating point definitions be integrated into Lean? The coq implementation (and flocq indirectly) defines the native floating point operations by axiomatically asserting that they are equivalent to the definitions in their spec float definition. I don't think this approach would fit for Lean though because pretty much everything only uses 3 axioms and axiomatically declaring the behavior of floats is anyways not necessary because you can't even use hardware floats in proofs (without ofReduceBool or similar).
Also, I used UInt64 directly as the representation of Float because then you don't need much compiler support, ofBits and toBits exist already. flocq instead chooses an inductive as the representation of floats - that would require much more compiler support though because then you'd need to be able to compile a match on a float specifically (unless you don't which creates its own problems).
It would also be nice to know what you think about my definition - I used some slightly different approaches than flocq and in particular tried to make the definitions as simple as possible, I'm not sure whether that makes these definitions more usable in proofs though and I'm still not entirely sure whether these definitions are correct. Obviously these definitions cause problems though because you'd need to redefine them for Float32.

[digama0]

This discussion should probably move to batteries.

• Regarding additional axioms: Yes, it's possible that this will require axioms, this is probably fine since we know that this can be eliminated if and when it is upstreamed. There are a variety of ways to ensure we don't introduce inconsistency in the process, as well as some options for doing it without axioms depending on how much we want to integrate with lean's Float.
• Regarding representation: It is important that lean's compiler sees Float and not UInt64 or an inductive type since this has a different representation in compiled code. I would recommend having the inductive type as an explicit representation of the float which is connected to Float via a decoding function, which is axiomatized to be bijective and commute appropriately with float operations.
• Also be aware that there is prior work on this space at Data.FP.Basic, although it is very old (8 years!) and probably needs significant update/cleanup.