classical.choice_elim

Stream: general

[Kevin Buzzard]

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]

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]

:(

[Keeley Hoek]

Propext makes the whole world blow up when you add kevin_ax

[Kevin Buzzard]

nooo!

[Kevin Buzzard]

but it's true in the VM!

[Kevin Buzzard]

or something

[Keeley Hoek]

Could you have this without a contradiction?

[Keeley Hoek]

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

[Keeley Hoek]

I'm very afraid

[Keeley Hoek]

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]

all hope is lost Kevin

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

I would argue you should "never" use choice

[Reid Barton]

where "never" = of course there are exceptions

[Reid Barton]

Except as unique_choice, which I guess only exists in my head

[Kevin Buzzard]

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]

I guess that falls under the category unique_choice.

[Kevin Buzzard]

I need to import Reid's head.

[Chris Hughes]

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]

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]

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]

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]

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]

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]

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

[Floris van Doorn]

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]

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

gives

ambiguous overload, possible interpretations
  1
  0

[Keeley Hoek]

Definitely user_command parsing respects spaces in the token name.

[Keeley Hoek]

I assumed the same would be the case for a custom user_notation. Perhaps it is not.