Drinker's Paradox in Formaloversum Game

Stream: new members

[Thomas Preu]

Hi
I think I mostly understood how you prove statements in propositional logic in lean4 through Kevin Buzzard's NNG and I tried to work through the introduction to predicate logic in the Formaloversum (in German).

I am stuck with the Drinker's paradox. The hints say to use "by_cases" and "push_neg at h". I could resolve one of the two cases, but I don't know how to do the second. This is what I tried so far:

by_cases h:∀ (y:People), isDrinking y
use default
intro hd
assumption
push_neg at h

Any help or hints how to proceed are greatly appreciated.

[Kevin Buzzard]

Can you please
(1) post fully working code (right now we can't even see the formal statement you're trying to prove, and there are many ways to formalise the Drinker's paradox); see #mwe for more information
(2) enclose your code in backticks; see #backticks for more information.

[Thomas Preu]

OK, sorry. Thank you for your patience.
Copying from the Webpage the statement is printed in several lines for better readability (not sure if line breaks are important)

example {People : Type} [Inhabited People] (isDrinking : People → Prop) :
  ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by

This is given on the web site. And here's what I tried so far

by_cases h:∀ (y:People), isDrinking y
use default
intro hd
assumption
push_neg at h

[Luigi Massacci]

Do you have a paper proof, and your problem is only the translation to lean, or do you not know how to prove it at all?

[Kevin Buzzard]

Just to expand on what Luigi said -- right now Lean does not do magic; you have to know the proof on paper before you can formalise it. (But you are going along the right lines)

[Dan Velleman]

After push_neg at h, your assumption h is the existential statement ∃ (y : People), ¬isDrinking y. A good proof-writing guideline is: if you know something exists, give it a name. So it would be helpful to introduce a name for a person who isn't drinking. Do you know a tactic for doing that?

[Kevin Buzzard]

Actually I stand corrected: Lean does do magic:

import Mathlib
import LeanCopilot

example {People : Type} [Inhabited People] (isDrinking : People → Prop) :
    ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by
  by_cases h:∀ (y:People), isDrinking y
  use default
  intro hd
  assumption
  push_neg at h
  search_proof -- works

[Thomas Preu]

After a long break I found some time to give it another shot. Thanks to all the people trying to give a helping hand.
Kevin Buzzard's suggestion is OK, if you work in an unrestricted environment. However, the Robo-game (as it has been renamed by now) is supposed to be played and won with limited resources. Here's a proof that works with the current version of the game:

example {People : Type} [h_nonempty : Nonempty People] (isDrinking : People → Prop) :
    ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by

  by_cases h : ∀ (y : People), isDrinking y
  obtain ⟨ d ⟩ := h_nonempty
  use d
  intro g
  assumption
  push_neg at h
  obtain ⟨z,f⟩ := h
  use z
  intro e
  contradiction

I hope this helps out other people who get stuck at that spot.