## 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₁,
end


:(

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

Propext makes the whole world blow up when you add kevin_ax

nooo!

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

but it's true in the VM!

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)


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,

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: May 15 2021 at 02:11 UTC