(3.7 : ℝ)

Stream: maths

[Kevin Buzzard]

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]

3.7 is sugar for 37/10

[Chris Hughes]

division of reals is noncomputable

[Kenny Lau]

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

[Chris Hughes]

the ring structure is computable

[Kevin Buzzard]

But 3.7 is just sugar for 37/10

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

(3.7 : \Q)

[Kenny Lau]

or #1038

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Is $e$ computable?

[Kevin Buzzard]

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]

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]

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]

Why do you want it to be computable?

[Johan Commelin]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Kenny Lau]

I thought Kevin just writes noncomputable theory in every file

[Kevin Buzzard]

I forgot and then I wondered what was going on

[Kevin Buzzard]

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]

Every explicit real number i mean

[Gabriel Ebner]

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]

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]

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

[Chris Hughes]

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]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Reid Barton]

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

[Reid Barton]

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