## Stream: maths

### Topic: (3.7 : ℝ)

#### 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$ and $3.7$ -- they're both "obviously real numbers". What is going on here?

#### Kenny Lau (May 20 2020 at 10:01):

3.7 is sugar for 37/10

#### Chris Hughes (May 20 2020 at 10:01):

division of reals is noncomputable

#### Kenny Lau (May 20 2020 at 10:01):

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

#### Chris Hughes (May 20 2020 at 10:01):

the ring structure is computable

#### Kevin Buzzard (May 20 2020 at 11:34):

But 3.7 is just sugar for 37/10

#### Kevin Buzzard (May 20 2020 at 11:34):

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

#### Kevin Buzzard (May 20 2020 at 11:35):

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

#### Kenny Lau (May 20 2020 at 11:35):

(3.7 : \Q)

or #1038

#### 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?

#### Kevin Buzzard (May 20 2020 at 11:37):

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

#### Kevin Buzzard (May 20 2020 at 11:37):

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

#### 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 $\pi/4=1/1-1/3+1/5-1/7+\dots$ are we done?

#### Kevin Buzzard (May 20 2020 at 11:39):

Is $e$ computable?

#### 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.

#### 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.

#### 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.

#### Reid Barton (May 20 2020 at 11:51):

Why do you want it to be computable?

#### Johan Commelin (May 20 2020 at 12:06):

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

#### 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 ℝ.

#### 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.

#### 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

#### Kenny Lau (May 20 2020 at 12:54):

I thought Kevin just writes noncomputable theory in every file

#### Kevin Buzzard (May 20 2020 at 14:02):

I forgot and then I wondered what was going on

#### 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

#### Kevin Buzzard (May 20 2020 at 14:03):

Every explicit real number i mean

#### 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.

#### 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.

#### Johan Commelin (May 20 2020 at 14:42):

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

#### 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


#### 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).

#### 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.

#### Reid Barton (May 20 2020 at 14:59):

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

#### Mario Carneiro (May 20 2020 at 15:29):

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

#### Gabriel Ebner (May 20 2020 at 15:32):

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

#### 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?

#### 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