Zulip Chat Archive

Stream: general

Topic: classical.choice_elim


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Sep 19 2019 at 13:27):

:(

view this post on Zulip Keeley Hoek (Sep 19 2019 at 13:29):

Propext makes the whole world blow up when you add kevin_ax

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 13:35):

nooo!

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 13:35):

but it's true in the VM!

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 13:35):

or something

view this post on Zulip Keeley Hoek (Sep 19 2019 at 13:41):

Could you have this without a contradiction?

view this post on Zulip Keeley Hoek (Sep 19 2019 at 13:41):

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

view this post on Zulip Keeley Hoek (Sep 19 2019 at 13:42):

I'm very afraid

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Sep 19 2019 at 13:52):

all hope is lost Kevin

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 14:10):

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

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 14:10):

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

view this post on Zulip Reid Barton (Sep 19 2019 at 14:19):

I would argue you should "never" use choice

view this post on Zulip Reid Barton (Sep 19 2019 at 14:19):

where "never" = of course there are exceptions

view this post on Zulip Reid Barton (Sep 19 2019 at 14:20):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 19 2019 at 14:28):

I guess that falls under the category unique_choice.

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 14:30):

I need to import Reid's head.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 19 2019 at 15:53):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Sep 20 2019 at 14:28):

Definitely user_command parsing respects spaces in the token name.

view this post on Zulip 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