Eliminate classical.some

Stream: new members

[Joe]

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]

it's not possible

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Jesse Michael Han]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

there's an issue about that

[Neil Strickland]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Neil Strickland]

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

[Kevin Buzzard]

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]

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]

both are provably bijections assuming choice

[Mario Carneiro]

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]

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]

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.