# Zulip Chat Archive

## Stream: new members

### Topic: has_to_string real

#### Charlie Conneen (May 31 2020 at 05:03):

I have a type defined which is dependent on `list real`

, and I would like to be able to use the `#eval`

command on it. The issue is, reals don't have a way of converting them to strings, at least not that Lean could find when I typed out the following code:

```
instance : has_repr R3 := ⟨λ x : R3, x.1.to_string⟩
```

What is the solution to this? There are reals we can't write down, but all the ones we can write down can be represented by at least the corresponding equivalence class of Cauchy sequences in `rat`

. Is there a way to define `real.to_string`

in a nice way?

#### Jalex Stark (May 31 2020 at 05:07):

how do you propose writing down an equivalence class of cauchy sequences in `rat`

?

#### Jalex Stark (May 31 2020 at 05:07):

why do you want to use `eval`

on your structure?

#### Jalex Stark (May 31 2020 at 05:07):

are there actually going to be concrete reals in there?

#### Charlie Conneen (May 31 2020 at 05:10):

Eventually I plan to take floats from real-world data, cut them off at some digit, and map them to rationals. So realistically I'll only be using the rationals, but would like the generalization to the reals for the purposes of my example.

#### Charlie Conneen (May 31 2020 at 05:13):

For writing down the equivalence class, if I were to construct a real number as an equivalence class, could I not just do it formally by giving it a sequence in `rat`

? So we could just print the real number as that sequence in some way

#### Mario Carneiro (May 31 2020 at 05:13):

It is not possible to write `real.to_string`

computably

#### Mario Carneiro (May 31 2020 at 05:14):

unless it prints `"this is a real"`

on any input

#### Mario Carneiro (May 31 2020 at 05:15):

There are no computable non-constant functions `real -> bool`

#### Charlie Conneen (May 31 2020 at 05:15):

I suppose that makes sense. To make `real.to_string`

, one would have to take in an arbitrary real number and have an algorithm which outputs a string. But there are countably many strings :)

#### Mario Carneiro (May 31 2020 at 05:16):

Even so, the representative of a real number is a cauchy sequence, which *eventually* converges to x but doesn't have to get there in a hurry

#### Mario Carneiro (May 31 2020 at 05:16):

There is a cauchy sequence for pi that starts 0,0,0,0,0,...,0 with n 0's

#### Mario Carneiro (May 31 2020 at 05:16):

same thing for e and sqrt 2 and every other real number

#### Mario Carneiro (May 31 2020 at 05:17):

so you can ask questions about the sequence all day and still have no idea what real number is being described

#### Bryan Gin-ge Chen (May 31 2020 at 05:18):

We do have an open issue about computable reals: #1038 but I don't think anyone is working on it right now.

#### Mario Carneiro (May 31 2020 at 05:18):

What I would recommend is using rationals, or floats or some other similar type that makes the approximation process explicit

#### Patrick Stevens (May 31 2020 at 05:19):

Well, you could do slightly better - you could say "this might be the real number 0, but we don't know", or "we were unable even to guess what this real might be"

#### Patrick Stevens (May 31 2020 at 05:19):

If the user has defined their real in any "normal" way, they might find this useful

#### Charlie Conneen (May 31 2020 at 05:20):

Ok, that's fair. Is there a way to do something like `real.to_debug_string`

? Just, anything that's a little better than the thousands of lines of code I get when Lean spits out the internal representation

#### Charlie Conneen (May 31 2020 at 05:20):

If not, I think just temporarily using the rationals will be the plan

#### Mario Carneiro (May 31 2020 at 05:20):

The reason this doesn't work is because `real`

is a quotient, which means that you are *required* to prove that your answer is not dependent on the sequence chosen from the equivalence class. Something like a function that returns "it looks like 0" if you see a bunch of 0's is not stable under equivalence

#### Mario Carneiro (May 31 2020 at 05:22):

It is possible to have a type that is classically equivalent to `real`

but has more useful computational content (I believe that's what #1038 is about). The simplest thing is to have an explicit modulus of convergence, for example asserting that the n'th element of the sequence is within 2^-n of x

#### Mario Carneiro (May 31 2020 at 05:23):

You can also cheat and use `quot.unquot`

to escape the quotient computably but unsoundly, for diagnostic purposes. Then you can just print `the sequence starts 0,1,1.5,1.75,1.875`

and let the user decide what to do with this info

#### Charlie Conneen (May 31 2020 at 05:25):

That's very interesting. I think then for now I'll just use rationals when I want to do any computation. I'll probably look more into computational formalisms soon enough...

#### Mario Carneiro (May 31 2020 at 05:28):

If you care about performance, I would not suggest trying out computational reals unless you know what you are doing. Because functions are values here it becomes very haskell-ish and you have to be careful to memoize stuff to get reasonable performance

#### Mario Carneiro (May 31 2020 at 05:28):

rational numbers or fixed point arithmetic is much easier to reason about

#### Reid Barton (May 31 2020 at 08:40):

Another option is to work over an arbitrary ordered field (say) as far as possible, and then specialize to `real`

for proving, and to `rat`

for calculating

#### Kevin Buzzard (May 31 2020 at 10:03):

Mario Carneiro said:

You can also cheat and use

`quot.unquot`

to escape the quotient computably but unsoundly, for diagnostic purposes. Then you can just print`the sequence starts 0,1,1.5,1.75,1.875`

and let the user decide what to do with this info

ooh ooh I bet it's 2

#### Johan Commelin (May 31 2020 at 10:05):

Too bad... it was `37`

#### Kevin Buzzard (May 31 2020 at 10:09):

These questions are so hard. That one isn't even in OEIS

Last updated: Dec 20 2023 at 11:08 UTC