Zulip Chat Archive

Stream: new members

Topic: has_to_string real


view this post on Zulip 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?

view this post on Zulip Jalex Stark (May 31 2020 at 05:07):

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

view this post on Zulip Jalex Stark (May 31 2020 at 05:07):

why do you want to use eval on your structure?

view this post on Zulip Jalex Stark (May 31 2020 at 05:07):

are there actually going to be concrete reals in there?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 31 2020 at 05:13):

It is not possible to write real.to_string computably

view this post on Zulip Mario Carneiro (May 31 2020 at 05:14):

unless it prints "this is a real" on any input

view this post on Zulip Mario Carneiro (May 31 2020 at 05:15):

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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 31 2020 at 05:16):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Patrick Stevens (May 31 2020 at 05:19):

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

view this post on Zulip 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

view this post on Zulip Charlie Conneen (May 31 2020 at 05:20):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 31 2020 at 05:28):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 31 2020 at 10:05):

Too bad... it was 37

view this post on Zulip Kevin Buzzard (May 31 2020 at 10:09):

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


Last updated: May 15 2021 at 00:39 UTC