computable division by non-zero real

Stream: maths

[Kevin Buzzard]

If I have a proof that r : ℝ is non-zero, can I make def f : ℝ → ℝ := λ x, x / r computable?

[Mario Carneiro]

if you have r^-1, then it's just multiplication

[Kevin Buzzard]

I ask because Luca has a bunch of these, and he's ended up making his entire file noncomputable theory to shut Lean up, with the result that we're going to end up with a noncomputable fundamental group. Is that inevitable though?

[Mario Carneiro]

but a proof that r is nonzero is not sufficient to compute a Cauchy sequence, you need a rational lower bound

[Kevin Buzzard]

His definition of the topology on [0,1] was noncomputable -- that didn't look like a good start

[Mario Carneiro]

topologies are trivially computable

[Kevin Buzzard]

I feel like we could fix all this because he wrote a bunch of stuff for general closed intervals [r,s]with only the hypothesis s>r, however his applications tend to be [0,1/2] or [0,1/4]

[Mario Carneiro]

if you give me a noncomputable definition of a topology, I can define a computable topology that is defeq

[Mario Carneiro]

because topologies have no data

[Mario Carneiro]

Why is the fundamental group noncomputable?

[Mario Carneiro]

what are the steps of construction that are problematic

[Kevin Buzzard]

import analysis.topology.topological_space
import analysis.real
import data.real.basic

def I01 := {x : ℝ | 0 ≤ x ∧ x ≤ 1}

instance : topological_space I01 := by unfold I01; apply_instance
-- definition 'I01.topological_space' is noncomputable, it depends on 'real.metric_space'

[Mario Carneiro]

real.metric_space is noncomputable?

[Mario Carneiro]

oh of course, the distance function is a max

[Mario Carneiro]

anyway it doesn't matter

[Kenny Lau]

why is Kevin worrying about computability?

[Mario Carneiro]

let the instance be noncomputable

[Mario Carneiro]

it won't cause any problems

[Kevin Buzzard]

The fundamental group is noncomputable currently because if you want a map from [0,1/2] to [0,1] you can either define it as lam x, 2 * x, or you can define a general map from [r,s] to [0,1] as lam x, (x-r)/(s-r), and use that function everywhere in your file, and fix all the noncomputable errors by writing noncomputable theory at the top, and nobody noticing until the file is 1000 lines long.

[Mario Carneiro]

none of that matters

[Kevin Buzzard]

oh great :-)

[Kevin Buzzard]

The definition of the multiplication on paths is noncomputable

[Mario Carneiro]

that checks out

[Kevin Buzzard]

So that's OK?

[Mario Carneiro]

you have to define it by cases on whether you are greater or less than 1/2

[Kevin Buzzard]

right

[Kevin Buzzard]

but Luca's implementation uses the map from [r,s] to [0,1] defined using division

[Kevin Buzzard]

with r=0 and s=1/2

[Kevin Buzzard]

and then with r=1/2 and s=1

[Mario Carneiro]

I often claim that when the function being defined is continuous you can do it without noncomputability, but in a general top space I'm not sure

[Mario Carneiro]

division by 2?

[Mario Carneiro]

I thought you meant real division - division by 2 is easy

[Kevin Buzzard]

why is Kevin worrying about computability?

I don't worry about it in general, I was just surprised to see it here. Were you virtually at my lecture a week last Monday? The example of G(3) made it clear to me what computability was.

[Kevin Buzzard]

we're dividing by s-r

[Kevin Buzzard]

using a general function which divides by s-r

[Kevin Buzzard]

in the special case where s-r=1/2

[Kevin Buzzard]

and when doing associativity s-r will be 1/4

[Mario Carneiro]

those could all be rationals

[Mario Carneiro]

just do your s-r trick where s and r are rationals

[Kevin Buzzard]

rofl

[Mario Carneiro]

But path multiplication will still be noncomputable because of the pasting you have to do

[Mario Carneiro]

if you have f g : [0,1] -> X and you want to concatenate them, you define (f * g) x = if x < 1/2 then f(2*x) else g(2*x-1)

[Kevin Buzzard]

aie you're right

[Mario Carneiro]

I think if you wanted to do that computably, you could define it by that equation on rationals, then take the limit as the sequence of rationals approaches some real

[Mario Carneiro]

but then you have to have a computable limit operation on the target topological space

[Kevin Buzzard]

I think this is all too much for Luca's project, I think we might stick to noncomputable

[Kevin Buzzard]

I'm glad I mentioned this now, I can go back to thinking computable maths is all a bit silly for a while.

[Kevin Buzzard]

What I'm trying to do nowadays is to get some sort of feeling for when I am actually being noncomputable. Like when I was a PhD student and I got some sort of a feeling for when I was actually using the axiom of choice

[Kevin Buzzard]

or when I was a post-doc and I got some sort of a feeling for when I was actually using universes

[Mario Carneiro]

rule of thumb: if you use anything descendent from topological_space.lean or analysis/real.lean, just put noncomputable theory and don't attempt to get away from it

[Kevin Buzzard]

[answer: probably never, although it was difficult to find a reference sometimes]

[Mario Carneiro]

If all your imports are in data you should try to be computable

[Kevin Buzzard]

Well Luca's file uses lots of stuff from both of those files, so we'll have to be noncomputable for now. Kenny can fix it all up when he's finished

[Mario Carneiro]

topology is 100% classical maths

[Kevin Buzzard]

I'm surprised. I didn't realise that.

[Mario Carneiro]

and metric spaces and uniform spaces...

[Kevin Buzzard]

Metric spaces I can understand because they mention reals.

[Mario Carneiro]

it could conceivably be different but it would require a major rewrite of the library

[Mario Carneiro]

data.real.basic is computable, analysis.real is not

[Kevin Buzzard]

Metric spaces also often use countable dependent choice, because the two definitions of closure only coincide when you are able to choose a sequence of points in your space tending to a point in the closure, which involves choosing x_n at distance at most 1/n from the boundary point

[Mario Carneiro]

well, that's just first countable spaces in general

[Mario Carneiro]

but there I'm not so worried because all the claims are propositional anyway

[Mario Carneiro]

we make no attempt to avoid the axiom of choice in theorems

[Chris Hughes]

import data.real.basic

def computable_inv (x : ℝ) : x ≠ 0 → ℝ :=
quotient.hrec_on x
(λ x (hx : real.mk x ≠ 0), real.mk
  (cau_seq.inv x (mt real.mk_eq_zero.2 hx)))
  (λ a b h, begin
    have : real.mk a = real.mk b := quotient.sound h,
    refine function.hfunext (by rw this)
      (λ h₁ h₂ _, heq_of_eq _),
    refine (domain.mul_right_inj h₁).1 _,
    conv {to_rhs, congr, skip, rw this},
    refine quotient.sound _,
    refine setoid.trans (cau_seq.inv_mul_cancel (mt real.mk_eq_zero.2 h₁))
      (setoid.symm (cau_seq.inv_mul_cancel (mt real.mk_eq_zero.2 h₂)))
  end)

[Mario Carneiro]

Yeah, I double checked the proof in data.real.basic and it can definitely be defined... I'm not sure why I didn't try

[Chris Hughes]

lemma computable_inv_mul_cancel (x : ℝ) : Π hx : x ≠ 0,
  computable_inv x hx * x = 1 :=
quotient.induction_on x (λ x hx, quotient.sound (cau_seq.inv_mul_cancel _))

[Chris Hughes]

@Kevin Buzzard you still haven't explained why you care about computable reals?

[Mario Carneiro]

Oh, I found a counterexample for the computability claim. Let $X$ be a quotient of $\Bbb R$ identifying all points in $[1,2]$. Let $f(x)=x$ and $g(x)=x+2$; these are continuous functions on $[0,1]$ such that $f(1)=[1]=[2]=g(0)$, and both functions are computable. The path concatenation $f\ast g$ is discontinuous at $1/2$ (in the real topology), so it is not computably definable.

[Kevin Buzzard]

Because Luca was dividing by a positive real which I could prove was greater than 1/10 and so I realised that probably I could make some of his noncomputable code computable. I hence wondered whether it would be an easy fix to make his fundamental group computable. But as Mario pointed out, there are other problems with computability, and I've now decided not to worry about it.