Computable `Squash` but noncomputable type?

Stream: maths

[Daniel Weber]

Is there any type α such that we have a computable def a : Squash α (docs#Squash) but no computable def b : α?

[Eric Wieser]

With any constraints on a and b?

[Daniel Weber]

What do you mean? They need to be computable and use the standard axiom set (propext, Quot.sound, Classical.choice)

[Eric Wieser]

import Mathlib

def a : Squash ℝ := .mk 0
noncomputable def b : ℝ := √2 -- can't remove `noncomputable`

[Eric Wieser]

But Squash is a distraction in that example, hence my question

[Daniel Weber]

I meant no computable value, which isn't true for ℝ - you can have def b : ℝ := 0

[Edward van de Meent]

I don't think it's possible; you can compute the Squash value exactly when you can compute some value of the original type... I believe the reason for this is that lean treats Squash.mk as id when computing

[Edward van de Meent]

And in general lean does this for quotients

[Edward van de Meent]

(I may be confused with Trunc tho)

[Edward van de Meent]

Looking into it, these are effectively the same type (and possibly even defeq? Don't treat them as such tho)

[Kevin Buzzard]

(previous thread)

[Daniel Weber]

Edward van de Meent said:

I don't think it's possible; you can compute the Squash value exactly when you can compute some value of the original type... I believe the reason for this is that lean treats Sqaush.mk as id when computing

Yes, but maybe there's some difference between "computable" in the compiler sense and "computable" in the theoretical sense? I'm not sure

[Edward van de Meent]

if we care about computable in the theoretical sense, i suspect that any nonempty type has a computable element using choice?

[Edward van de Meent]

you can choose a partial encoding of the type, in such a way that 0 is the encoding of the first element, at which point decoding 0 is a computable definition of an element of the type.

[Edward van de Meent]

of course, this is kind of cheating, since the encoding we're using is not (necessarily) canonical, or even total for that matter.