## Stream: new members

### Topic: Eliminate classical.some

#### Joe (May 22 2019 at 04:33):

variables {α : Type*} {β : Type*}

def foo (x : α) (p : α → Prop) (f : α → β) (he : ∃ x, p x)
(ha : ∀ x y, p x ∧ p y → f x = f y) : β := f (classical.some he)


How do I construct the same thing without using classical.some? I think it is possible because ha says f doesn't care which x is chosen as long as p x is satisfied.

#### Mario Carneiro (May 22 2019 at 04:39):

it's not possible

#### Mario Carneiro (May 22 2019 at 04:39):

this is called unique choice, and there isn't a way to get it without using choice or making your own axiom

#### Mario Carneiro (May 22 2019 at 04:40):

as far as lean is concerned, it's just as "nonconstructive" because the exists doesn't tell you how to find such an element

#### Mario Carneiro (May 22 2019 at 04:42):

For example, you could use this to compute the busy beaver function

#### Jesse Michael Han (May 22 2019 at 05:50):

are lean's constructive reals the same as the computable reals? another example could be definable but noncomputable reals

#### Mario Carneiro (May 22 2019 at 05:58):

Oh, wait, what's that (x : α) doing there? It's not used in the definition

#### Mario Carneiro (May 22 2019 at 05:59):

I will assume that's a typo. Here's how everything becomes computable using (computable) unique choice:

variables {α : Type*} {β : Type*}

def unique_choice (p : α → Prop) (f : α → β) (he : ∃ x, p x)
(ha : ∀ x y, p x ∧ p y → f x = f y) : β := sorry

def choice' {α} : nonempty α → α :=
unique_choice (eq classical.choice) id ⟨_, rfl⟩ \$ λ x y h, h.1.symm.trans h.2


#### Kevin Buzzard (May 22 2019 at 06:40):

The problem is that even if f : α → β is a function which is computable and which you can prove is a bijection, there might be no algorithm to compute the inverse function (the proof might just be an abstract existence proof rather than a construction). Going from ∃ x, p x to x is going from the Prop universe to the Type universe and sometimes this is not possible constructively.

#### Kevin Buzzard (May 22 2019 at 06:41):

are lean's constructive reals the same as the computable reals? another example could be definable but noncomputable reals

Does Lean even have constructive reals?

#### Neil Strickland (May 22 2019 at 08:28):

It's also worth pointing out that you can avoid classical.some if α and β are finite with decidable equality. I think that this is in mathlib with a non-obvious name that I do not remember. There is a more extensive set of similar results here. This will need some work before it can go into mathlib, but I hope to do that at some point.

#### Kevin Buzzard (May 22 2019 at 11:07):

Even if alpha is infinite I guess you could get away with it, as long as it has decidable equality and can be computably enumerated (e.g. nat, for which there is even some explicit function that does it IIRC, nat.some or something? Not at Lean right now).

Can someone remind me of a computable bijection (on the reals, or the power set of the naturals or something) with no computable inverse?

#### Kevin Buzzard (May 22 2019 at 11:09):

There is a more extensive set of similar results here.

Is this one of these situations where the trunc trick can somehow help? I didn't understand this trick in the past but it's getting to the point where the next time that someone explains it to me, I'll probably get it.

#### Mario Carneiro (May 22 2019 at 11:14):

Yes. If you replace \ex x, p x with trunc {x // p x} then it's definable

#### Mario Carneiro (May 22 2019 at 11:18):

The proof of this is just the literal construction -

import data.quot

variables {α : Type*} {β : Type*}

def unique_choice (p : α → Prop) (f : α → β) (he : trunc {x // p x})
(ha : ∀ x y, p x ∧ p y → f x = f y) : β :=
trunc.lift (λ a:{x//p x}, f a.1) (λ a b, ha _ _ ⟨a.2, b.2⟩) he


but the meaning explanation is that trunc contains data that can be used in further computation, because it lives in Type instead of Prop. So when the VM wants to execute this function it just takes f and applies it to the value stored in he

#### Mario Carneiro (May 22 2019 at 11:18):

You can't do this with the exists version because he isn't storing anything in that case

#### Mario Carneiro (May 22 2019 at 11:22):

I guess the canonical function from option A to roption A is a bijection with no computable inverse

#### Neil Strickland (May 22 2019 at 11:31):

I guess that the coercion bool → Prop is also a bijection without computable inverse.

#### Kevin Buzzard (May 22 2019 at 11:42):

I guess that the coercion bool → Prop is also a bijection without computable inverse.

I'm not sure it is provably a bijection in Lean, is it?

#### Kevin Buzzard (May 22 2019 at 11:44):

I guess the canonical function from option A to roption A is a bijection with no computable inverse

We could also consider the function from functions to bool sending f to true iff f is canonical

#### Mario Carneiro (May 22 2019 at 11:50):

both are provably bijections assuming choice

#### Mario Carneiro (May 22 2019 at 11:52):

If you don't assume choice then it's a very different problem... In this case you are purely intuitionistic and so from the existence property from a closed proof that the function is bijective you can reconstruct a function that was the existential witness

#### Wojciech Nawrocki (Jun 06 2019 at 16:26):

Is it an orthogonal issue that possibly multiple instances of nonempty α could exist and any function which tries to compute (h: nonempty α) -> α := choice α h would have to choose one nondeterministically? Or is this more or less the same problem?

#### Keeley Hoek (Jun 07 2019 at 08:14):

This cannot happen, since nonempty α is defined to live in Prop. Hence every term of type nonempty α is equal to every other. Thus applying choice to any two such terms gives the same result.

Last updated: May 16 2021 at 20:13 UTC