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