Real to float translation

Stream: general

[Tomas Skrivan]

Alexander Bentkamp said:

We've done something like that here: https://github.com/verified-optimization/CvxLean/blob/main/CvxLean/Tactic/Solver/Float/RealToFloat.lean (cc Jeremy Avigad Ramon Fernández Mir )

The mechanism allows us to register various expressions about the reals and their corresponding expression on floats, so that we can convert a complex real expression into an expression on floats and then evaluate it.

I do not want to pollute the NSF CAREER thread as discussion about floats tend to spiral out of control.

Cool approach! I'm wondering how scalable approach this is i.e. you do not have to manually reimplement whole library with addRealToFloat commands.

It seems to work nice for a simple functions like

def rsquare (x : ℝ) := x*x

You can automatically generate commands

def rsquare.float_impl (x : Float) := x*x
addRealToFloat rsquare := rsquare.float_impl

However, you get into trouble with polymorphic functions

def square {α : Type} [Mul α] (a : α) := a*a

You would have to generate infinite number of new declarations

def square.float [Mul Float] (a : Float) := a * a
addRealToFloat @square Real := square.float
def square.prod_float_float [Mul (Float×Float)] (a : Float×Float) := a * a
addRealToFloat @square (Real×Real) := square.prod_float_float
...

It looks like that doing this automatically comes to implementing custom monomorphization compilation pass. This seems hard/lots of work. Any thought on this? Is there an existing monomorphization framework in Lean core that could be reused for this?

[Alexander Bentkamp]

I don't quite understand what you mean. The definition

def square {α : Type} [Mul α] (a : α) := a*a

does not depend on anything Real- or Float-specific. So I think it's enough to add

addRealToFloat @instMulFloat := @instMulReal

The constant square itself does not need to be replaced to make it work.

[Tomas Skrivan]

Ahh sorry most likely I completely misunderstood how the whole thing works, I should actually run your code and play around with it first.