Stuck on lean book example

Stream: new members

[Tom Cheng]

Hello. I'm working through the lean theorem proving book, and I'm on chapter 4: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html

The book provides examples. I'm stuck trying to prove this example:

example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := sorry

Specifically, trying to prove it right-to-left.

I'm not even sure it's true intuitively:

Does (∀ x, p x) → r imply (∃ x, p x → r)?

I don't even know how to approach it. We have a already, so we know that an example of x exists - we just need to prove that p x -> r. (∀ x, p x) → r doesn't help with that, it's completely irrelevant, I can never show that ∀ x, p x.

I'm beginning to think this example is a typo, and it shouldn't be an IFF.

Can anyone solve it?

[Riccardo Brasca]

Can you please provide a #mwe?

[Tom Cheng]

Sure, i've rewritten it to be the side I care about:

open Classical

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example (a : α) : ((∀ x, p x) → r) → (∃ x, p x → r) := sorry

[Tom Cheng]

The book mentions you might need classical logic for some examples, but doesn't tell you which examples need it

[Matt Diamond]

Oh, this looks like it's related to the Drinker paradox

[Matt Diamond]

I was able to prove it, so it's not a typo... a bit tricky though

[Matt Diamond]

Here's a hint:

example (a : α) : ((∀ x, p x) → r) → (∃ x, p x → r) :=
by
  intro h1
  by_cases h2 : ∀ x, p x
  · sorry
  · push_neg at h2
    sorry

[Riccardo Brasca]

Yes I was also confused at the beginning, but it is ok. I more or less did something like: if r is true than there is nothing to prove (using a). If r is false, then ∀ x, p x must be false, so, there must be b such that ¬ p b. Now we have p b → r, since p b is false so it implies everything.

[Tom Cheng]

Thanks. This is the route I went before @Matt Diamond , but thought I'd missed something because I got stuck here on the \not \forall x, p x case - I just don't understand how you can use that.

example (a : α) : ((∀ x, p x) → r) → (∃ x, p x → r) := by
  intro h1
  by_cases h2 : ∀ x, p x
  case pos =>
    apply Exists.intro a
    intro hp
    exact h1 h2
  case neg =>

My cursor is at the bottom, and the state is:

α : Type
p q : α → Prop
r : Prop
a : α
h1 : (∀ (x : α), p x) → r
h2 : ¬∀ (x : α), p x
⊢ ∃ x, p x → r

but h2 means that there's no point using h1, right? so we're left trying to prove p x -> r from the first 4 statements, which is impossible.

So there must be a trick I'm missing?

[Tom Cheng]

oh hang on i missed your push_neg, i ahven't seen that before, 2s

[Riccardo Brasca]

you can also use simp at h2 to get the existence statement

[Riccardo Brasca]

push_neg needs some import, but what you need is docs#Classical.not_forall

[Matt Diamond]

good point... I have a habit of adding import Mathlib so I forgot to mention that it won't work out of the box

[Tom Cheng]

Hmmm I must still be missing something.

So with Classical.not_forall I've got

h1 : (∀ (x : α), p x) → r
h2 : ∃ x, ¬p x
⊢ ∃ x, p x → r

I still don't intuitively understand how this can work. Could I see your solution?

[Tom Cheng]

oh wait i see

[Matt Diamond]

yeah, you just use cases' h2 with b hb (or something similar) and derive a contradiction

[Tom Cheng]

Ok thanks, I got it; if there's an x where \not p x, then p x can imply anything

[Tom Cheng]

It's funny: whenever there's a proof involving false like this, it's hard to understand intuitively, and much easier to reach by just moving symbols about

Thanks again :)

[Matt Diamond]

No problem!

[Riccardo Brasca]

For example

open Classical

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example (a : α) : ((∀ x, p x) → r) → (∃ x, p x → r) := by
  intro h1
  by_cases h2 : ∀ x, p x
  case pos =>
    apply Exists.intro a
    intro hp
    exact h1 h2
  case neg =>
    simp at h2
    obtain ⟨b, hb⟩ := h2
    apply Exists.intro b
    intro h
    contradiction

[Bulhwi Cha]

#tpil explains tactics in Chapter 5, so I made a term proof of the example:

open Classical

theorem exists_imp_of_forall_imp_self {α : Sort u} {p : α → Prop} {r : Prop} (a : α) :
    ((∀ x, p x) → r) → ∃ x, (p x → r) :=
  fun h ↦ byCases
    (fun hr : r ↦ ⟨a, fun _ ↦ hr⟩)
    (fun hnr : ¬r ↦
      have hnap : ¬∀ x, p x := mt h hnr
      have hexnp : ∃ x, ¬p x := not_forall.mp hnap
      let ⟨b, hnp⟩ := hexnp
      ⟨b, fun hp ↦ absurd hp hnp⟩)

[Bulhwi Cha]

Matt Diamond said:

Oh, this looks like it's related to the Drinker paradox

Here's a Lean proof of the paradox:

open Classical

theorem drinker_paradox {Pub : Sort u} {IsDrinking : Pub → Prop} [Inhabited Pub] :
    ∃ x, (IsDrinking x → ∀ y, IsDrinking y) :=
  byCases
    (fun h : ∀ y, IsDrinking y ↦ ⟨default, fun _ ↦ h⟩)
    (fun h : ¬∀ y, IsDrinking y ↦
      have hexnd : ∃ y, ¬IsDrinking y := not_forall.mp h
      let ⟨a, hnd⟩ := hexnd
      ⟨a, fun hd ↦ absurd hd hnd⟩)

The paradox is a corollary of the example discussed in this thread.

Alternative proofs

theorem drinker_paradox' {Pub : Sort u} {IsDrinking : Pub → Prop} [Inhabited Pub] :
    ∃ x, (IsDrinking x → ∀ y, IsDrinking y) :=
  exists_imp_of_forall_imp_self default id

theorem drinker_paradox'' {Pub : Sort u} {IsDrinking : Pub → Prop} [Inhabited Pub] :
    ∃ x, (IsDrinking x → ∀ y, IsDrinking y) := by
  by_cases h : ∀ y, IsDrinking y
  · exists default
    simp [h]
  · have hexnd := not_forall.mp h
    let ⟨a, hnd⟩ := hexnd
    exists a
    intro hd
    contradiction

20241118_11h49m28s_drinker-paradox.png