# Zulip Chat Archive

## Stream: general

### Topic: classical.choice_elim

#### Kevin Buzzard (Sep 19 2019 at 13:13):

I had a brain freeze and couldn't remember the name of the function `(∃ (x : α), p x) → α`

. I tried `library_search`

:

example : Π {α : Sort u} {p : α → Prop}, (∃ (x : α), p x) → α := by library_search -- fails

but it failed! Is this a bug in `library_search`

or is the issue that it's not a theorem? With my tail between my legs I opened up TPIL for the first time in a long time, and went to the section on choice. I learnt `classical.choice : Π {α : Sort u_1}, nonempty α → α`

and thought "oh I can take it from here". I used `library_search`

to discover

`nonempty_of_exists : (∃ (x : α), p x) → nonempty α`

and so I just defined my function to be `classical.choice (nonempty_of_exists h)`

and moved on.

A bit later I needed that the `x`

provided by my function actually satisfied `p x`

, and I took one look at that problem and thought "Oh -- that's `classical.some_spec`

". I *then* remembered that the function I wanted but couldn't find was called `classical.some`

and I figured that this would be no problem because the definition of `classical.some`

will boil down to what I wrote. So I tried to prove this:

example (α : Type) (p : α → Prop) (h : (∃ (x : α), p x)) : classical.choice (nonempty_of_exists h) = classical.some h := sorry

with `rfl`

, but it didn't work! Here is me unwinding what went wrong:

set_option pp.proofs true example (α : Type) (p : α → Prop) (h : (∃ (x : α), p x)) : classical.choice (nonempty_of_exists h) = classical.some h := begin cases h with x hx, unfold classical.some, delta classical.indefinite_description, dsimp, -- changes the proofs! delta id_rhs, show classical.choice (nonempty_of_exists (Exists.intro x hx)) = (classical.choice (nonempty.intro (⟨x, hx⟩ : {d : α // p d}))).val, sorry end

The problem is that `classical.choice`

is not as functorial as you'd want -- I guess there is no eliminator. The goal ended up being

classical.choice (nonempty.intro x) = (classical.choice (nonempty.intro ⟨x, hx⟩)).val

This would be provable if we could prove this:

theorem classical.choice_elim (α : Type) (x : α) : classical.choice (nonempty.intro x) = x := sorry

But that can't be proved in Lean, right? Because classical.choice is just an axiom so you can't prove anything about it which doesn't boil down to `rfl`

in some sense. But OTOH the result is true in some funny sense, because the VM mumble mumble I don't know what I'm talking about stores it as x internally but the kernel forgets it or something. This is at the boundary of my understanding (I don't really understand the VM or the kernel but perhaps this example would help me understand them).

I was wondering whether it would be "safe" to add `classical.choice (nonempty.intro x) = x`

as an axiom to Lean? Or can it somehow already be proved and I'm barking up the wrong tree?

#### Keeley Hoek (Sep 19 2019 at 13:26):

axiom kevin_ax {α : Type} (x : α) : classical.choice (nonempty.intro x) = x theorem uh_oh_kevin : false := begin have h₀ : classical.choice (nonempty.intro 0) = 0 := kevin_ax _, have h₁ : classical.choice (nonempty.intro 1) = 1 := kevin_ax _, have : 0 = 1 := eq.trans h₀.symm h₁, contradiction end

#### Keeley Hoek (Sep 19 2019 at 13:27):

:(

#### Keeley Hoek (Sep 19 2019 at 13:29):

Propext makes the whole world blow up when you add `kevin_ax`

#### Kevin Buzzard (Sep 19 2019 at 13:35):

nooo!

#### Kevin Buzzard (Sep 19 2019 at 13:35):

but it's true in the VM!

#### Kevin Buzzard (Sep 19 2019 at 13:35):

or something

#### Keeley Hoek (Sep 19 2019 at 13:41):

Could you have this without a contradiction?

#### Keeley Hoek (Sep 19 2019 at 13:41):

axiom choice_commutes {α β : Type} (f : α → β) (h : nonempty α) : f (classical.choice h) = classical.choice (h.map f)

#### Keeley Hoek (Sep 19 2019 at 13:42):

I'm very afraid

#### Keeley Hoek (Sep 19 2019 at 13:52):

That's a negative

theorem uh_oh_keeley : false := begin let f : bool → bool := λ _, tt, let g : bool → bool := λ _, ff, let h : nonempty bool := nonempty.intro tt, have hv : f.map h = g.map h := rfl, have : tt = ff := calc tt = f (classical.choice h) : by cases classical.choice h; refl ... = classical.choice (h.map f) : choice_commutes _ _ ... = classical.choice (h.map g) : by rw hv ... = g (classical.choice h) : (choice_commutes _ _).symm ... = ff : by cases classical.choice h; refl, contradiction end

#### Keeley Hoek (Sep 19 2019 at 13:52):

all hope is lost Kevin

#### Kevin Buzzard (Sep 19 2019 at 14:10):

I can't deal with concepts that aren't functorial.

#### Kevin Buzzard (Sep 19 2019 at 14:10):

you can imagine why the HoTT people have trouble with choice...

#### Reid Barton (Sep 19 2019 at 14:19):

I would argue you should "never" use `choice`

#### Reid Barton (Sep 19 2019 at 14:19):

where "never" = of course there are exceptions

#### Reid Barton (Sep 19 2019 at 14:20):

Except as `unique_choice`

, which I guess only exists in my head

#### Kevin Buzzard (Sep 19 2019 at 14:25):

How do you avoid it in the following situation (a simplified version of where I was):

def next_to (a b : ℤ) := ∃ d ∈ ([-1, 1] : list ℤ), a + d = b lemma next_to.symm {a b : ℤ} (hab : next_to a b) : next_to b a := ⟨-classical.some hab, sorry⟩

#### Johan Commelin (Sep 19 2019 at 14:28):

I guess that falls under the category `unique_choice`

.

#### Kevin Buzzard (Sep 19 2019 at 14:30):

I need to import Reid's head.

#### Chris Hughes (Sep 19 2019 at 14:37):

import tactic def next_to (a b : ℤ) := ∃ d ∈ ([-1, 1] : list ℤ), a + d = b lemma next_to.symm {a b : ℤ} (hab : next_to a b) : next_to b a := by rcases hab with ⟨x, hx₁, hx₂⟩; exact ⟨-x, by simpa [eq_neg_iff_eq_neg, eq_comm, or_comm] using hx₁, by rw ← hx₂; simp⟩

#### Chris Hughes (Sep 19 2019 at 14:40):

Although I would be tempted to define `next_to`

as

inductive next_to : ℤ → ℤ → Prop | left : ∀ x, next_to x (x + 1) | right : ∀ x, next_to (x + 1) x

#### Reid Barton (Sep 19 2019 at 14:48):

You're proving a proposition and you only need to deconstruct a single existential, so as Chris says you don't need to use choice at all.

#### Kevin Buzzard (Sep 19 2019 at 15:12):

Regarding the definition: I went for that because that's what I was given in https://competition.isabelle.systems/competitions/contest/14/tasks/2/ . I agree another definition would be better for Lean.

#### Kevin Buzzard (Sep 19 2019 at 15:13):

I had a proof of what I needed in tactic mode and was considering transferring it to term mode, but then ran into this issue. I note that Chris' solution also uses tactics.

#### Keeley Hoek (Sep 19 2019 at 15:14):

Is there a way of defeating the GOAL notation by defining custom notation which includes a space in the token like `GOAL `

so it doesn't clash with `GOAL`

?

#### Mario Carneiro (Sep 19 2019 at 15:53):

I don't think you can declare notations with embedded spaces

#### Floris van Doorn (Sep 20 2019 at 04:01):

I'm quite sure that spaces in notation are only hints for the printer, not for the parser. For example ` + `

is declared with spaces around it, but writing `a+b`

still parses correctly.

#### Floris van Doorn (Sep 20 2019 at 04:02):

notation `GOAL` := 0 notation ` GOAL ` := 1 example : GOAL = 2 := _

gives

ambiguous overload, possible interpretations 1 0

#### Keeley Hoek (Sep 20 2019 at 14:28):

Definitely `user_command`

parsing respects spaces in the token name.

#### Keeley Hoek (Sep 20 2019 at 14:28):

I assumed the same would be the case for a custom `user_notation`

. Perhaps it is not.

Last updated: Dec 20 2023 at 11:08 UTC