How do you convert between Floats and reals?

Stream: mathlib4

[Robert Joseph]

I was just wondering how does one convert a Float value into reals and vice versa in mathlib? I couldn't find any accompanying function. I understand that in mathlib that you cant do computations with the reals, but what if I have a float value say 1.2 which is also the reals? i just want to convert it into the reals to say prove some theorems about it or use it as part of a theorem and not convert the whole theorem to use floats.

[Andrew Yang]

Is docs#OfScientific what you are looking for?
I don’t think it is possible to go the other way around though, unless there is some unsafe way that I am not aware of.

[Jireh Loreaux]

There's docs#Float.toRat0 and docs#Rat.toFloat, but I'm not sure even those will be useful to you.

[Martin Dvořák]

FYI reals are Cauchy sequences. I don't think you can convert it to a Float. The other direction should be possible.

[Robert Maxton]

Martin Dvořák said:

FYI reals are Cauchy sequences. I don't think you can convert it to a Float. The other direction should be possible.

I mean, you can certainly talk about the nearest Float to a real; you just need to know the convergence rate of the real so you know how many terms you need to sum

[Robert Maxton]

But yeah that's an approximation ofc

[Andrew Yang]

I don't see how you can know the convergence rate of a cauchy sequence. For example let $a_n =$ "if all even numbers up to $n$ is a sum of two primes then $0$ else $1$", which is perfectly "computable" in mathlib reals. Can you tell me if the closest float it converges to is 0 or 1?

[Aaron Liu]

Robert Maxton said:

Martin Dvořák said:

FYI reals are Cauchy sequences. I don't think you can convert it to a Float. The other direction should be possible.

I mean, you can certainly talk about the nearest Float to a real; you just need to know the convergence rate of the real so you know how many terms you need to sum

But the mathlib reals don't have to tell you their convergence rate!

[Robert Maxton]

... Ah. Right. Yes, I was looking at the exists in docs#IsCauSeq and forgetting "right, you can't actually computably extract the relevant i". ^.^;

[Robert Joseph]

Thanks everyone for the comments! I will look into the suggestions you made: )