Zulip Chat Archive

Stream: maths

Topic: (3.7 : ℝ)


view this post on Zulip Kevin Buzzard (May 20 2020 at 09:59):

example :  := -4 -- works fine
example :  := 3.7  -- definition '_example' is noncomputable, it depends on 'real.division_ring'

I'm a mathematician and I can't tell the difference between 4-4 and 3.73.7 -- they're both "obviously real numbers". What is going on here?

view this post on Zulip Kenny Lau (May 20 2020 at 10:01):

3.7 is sugar for 37/10

view this post on Zulip Chris Hughes (May 20 2020 at 10:01):

division of reals is noncomputable

view this post on Zulip Kenny Lau (May 20 2020 at 10:01):

-4 is sugar for -((1+1)+(1+1))

view this post on Zulip Chris Hughes (May 20 2020 at 10:01):

the ring structure is computable

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:34):

But 3.7 is just sugar for 37/10

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:34):

oh this is silly. Why can't this be fixed? What needs to be done?

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:35):

beyond "make division by certain reals (eg 10) computable"

view this post on Zulip Kenny Lau (May 20 2020 at 11:35):

(3.7 : \Q)

view this post on Zulip Kenny Lau (May 20 2020 at 11:36):

or #1038

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:36):

So I want a computable function div: R -> Q -> R and a proof that it commutes with real.div via the coercion?

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:37):

Then can I just tag it with norm_cast and it will all work magically?

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:37):

I'm only asking that normal decimals work. I'm not suggesting recurring decimals (yet)

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:38):

Presumably π\pi is also not computable? Can this be fixed? Just some crap theoretical definition? Is the problem here that we are missing a mathematical theorem? If we knew π/4=1/11/3+1/51/7+\pi/4=1/1-1/3+1/5-1/7+\dots are we done?

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:39):

Is ee computable?

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:40):

I'm not actually going to compute with it! I just want a proof that it's computable, not code that will ever run.

view this post on Zulip Kevin Buzzard (May 20 2020 at 11:42):

Wasn't it once said that no physicist could ever need π\pi to more than 30 decimal places? Well, I am wondering whether no proper mathematician ever needs π\pi to more than about 4 decimal places, and we have this in Lean already. People like my prestigious colleague Toby Gee who is an expert in the Langlands program probably never assumed anything about its value beyond possibly the fact that it was positive and finite.

view this post on Zulip Reid Barton (May 20 2020 at 11:50):

Being computable in Lean's sense (for the specific definition of ℝ that mathlib has) doesn't imply that you can calculate its digits in any sense.

view this post on Zulip Reid Barton (May 20 2020 at 11:51):

Why do you want it to be computable?

view this post on Zulip Johan Commelin (May 20 2020 at 12:06):

I think Kevin doesn't want to write noncomputable example.

view this post on Zulip Reid Barton (May 20 2020 at 12:12):

For example : ℝ := 3.7 I think that's impossible given the way 3.7 is elaborated and the type of /, even if you redefined .

view this post on Zulip Reid Barton (May 20 2020 at 12:14):

Haskell uses a different desugaring of fractional literals, basically Kenny's (3.7 : \Q), and that one would work.

view this post on Zulip Reid Barton (May 20 2020 at 12:17):

Constructively / can't be totalized and instead you need to provide a third argument y # 0, which is data

view this post on Zulip Kenny Lau (May 20 2020 at 12:54):

I thought Kevin just writes noncomputable theory in every file

view this post on Zulip Kevin Buzzard (May 20 2020 at 14:02):

I forgot and then I wondered what was going on

view this post on Zulip Kevin Buzzard (May 20 2020 at 14:03):

My main question was basically that every real number a mathematician uses is computable so why do we even have to switch it on

view this post on Zulip Kevin Buzzard (May 20 2020 at 14:03):

Every explicit real number i mean

view this post on Zulip Gabriel Ebner (May 20 2020 at 14:10):

One option is to define cauchy sequences as an equivalence class (i.e a subtype of set (ℕ → ℚ)) instead of a quotient. Or we could do Dedeking reals.

view this post on Zulip Chris Hughes (May 20 2020 at 14:39):

I don't know why everyone gets so hung up about the noncomputable tag. The tag is only an approximation to what noncomputable actually means. It's just some tag to make programming in Lean a bit easier that's irrelevant for types that you're not actually going to compute with. The idea of defining something to be a set just because someone made some decision that sets don't have to be marked noncomputable even though they're not really computable just seems silly to me. Sets are outside of the domain of the noncomputable predicate really, and calling them computable is just some junk value it returns outside the domain.

view this post on Zulip Johan Commelin (May 20 2020 at 14:42):

Why is Kevin even interested in 3.7? You shouldn't divide junk by 10!

view this post on Zulip Chris Hughes (May 20 2020 at 14:54):

Here's a nice "computable" ring.

import data.int.basic ring_theory.ideals

def X : Type := classical.choice ⟨ℤ⟩

instance Z : comm_ring (X  ) := by apply_instance

view this post on Zulip Reid Barton (May 20 2020 at 14:58):

Along these lines, what if we just map real into set real by singleton sets, then transfer everything there. Now it's "computable" (because there is no computational content whatsoever).

view this post on Zulip Reid Barton (May 20 2020 at 14:58):

I guess Gabriel's suggestion of Dedekind cuts has the same result, but that requires more work.

view this post on Zulip Reid Barton (May 20 2020 at 14:59):

Oh, also now I understand what he meant by equivalence classes too.

view this post on Zulip Mario Carneiro (May 20 2020 at 15:29):

There is an interface for this btw, erased real is exactly what you describe

view this post on Zulip Gabriel Ebner (May 20 2020 at 15:32):

So you're saying we should define real as erased Cauchy?

view this post on Zulip Reid Barton (May 20 2020 at 15:33):

Would this have any effect on unfolding? Could we somehow exploit this new definition to avoid having to use irreducible directly?

view this post on Zulip Reid Barton (May 20 2020 at 15:33):

For example, real.add could be an inductive proposition!


Last updated: May 12 2021 at 08:14 UTC