# Zulip Chat Archive

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

#### Mario Carneiro (May 22 2019 at 07:03):

there's an issue about that

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