Do we need these three theorems?

Stream: general

[Bulhwi Cha]

universe u

/-- A lemma for rewriting an existential statement. -/
theorem funext_propext {α : Sort u} {p q : α → Prop} (h : ∀ {x}, p x ↔ q x) :
    (fun x : α ↦ p x) = (fun x : α ↦ q x) :=
  funext (fun _ ↦ propext h)

theorem exists_or_left {α : Sort u} {p : α → Prop} {b : Prop} [Inhabited α] :
    (∃ x, b ∨ p x) ↔ b ∨ (∃ x, p x) :=
  Iff.intro
    (fun ⟨w, h⟩ ↦ h.elim Or.inl (fun hp ↦ Or.inr ⟨w, hp⟩))
    (fun h ↦ h.elim
      (fun hb ↦ ⟨default, Or.inl hb⟩)
      (fun ⟨w, hp⟩ ↦ ⟨w, Or.inr hp⟩))

theorem exists_or_right {α : Sort u} {p : α → Prop} {b : Prop} [Inhabited α] :
    (∃ x, p x ∨ b) ↔ (∃ x, p x) ∨ b :=
  Iff.intro
    (fun ⟨w, h⟩ ↦ h.elim (fun hp ↦ Or.inl ⟨w, hp⟩) Or.inr)
    (fun h ↦ h.elim
      (fun ⟨w, hp⟩ ↦ ⟨w, Or.inl hp⟩)
      (fun hb ↦ ⟨default, Or.inr hb⟩))

/-- A class for formalizing the drinker paradox. -/
class DrinkerParadox (Pub : Type) [Inhabited Pub] where
  IsDrinking : Pub → Prop

namespace DrinkerParadox

variable {Pub : Type} [Inhabited Pub] [DrinkerParadox Pub]

open Classical

/-- There is someone in the pub such that, if the person is drinking, then everyone in the pub is
drinking. -/
example : ∃ (x : Pub), IsDrinking x → ∀ (y : Pub), IsDrinking y := by
  rw [funext_propext Decidable.imp_iff_not_or, exists_or_right, ←not_forall, or_comm]
  apply em

end DrinkerParadox

1. Lean's core library already has docs#exists_and_left and docs#exists_and_right. Should we also add exists_or_left and exists_or_right to it?
2. I had to state and prove the theorem funext_propext so that I could rewrite an existential statement. Do you think this theorem should be included in the core library?

[Eric Wieser]

Those exists lemmas look reasonable to me, though they should use Nonempty not Inhabited

[Eric Wieser]

funext_propext shouldn't be needed, simp_rw should work fine

[Bhavik Mehta]

Note there are simpler proofs available:

theorem exists_or_right {α : Sort u} {p : α → Prop} {b : Prop} [Nonempty α] :
    (∃ x, p x ∨ b) ↔ (∃ x, p x) ∨ b := by
  rw [exists_or, exists_const]

theorem exists_or_left {α : Sort u} {p : α → Prop} {b : Prop} [Nonempty α] :
    (∃ x, b ∨ p x) ↔ b ∨ (∃ x, p x) := by
  rw [exists_or, exists_const]

[Bulhwi Cha]

Eric Wieser said:

funext_propext shouldn't be needed, simp_rw should work fine

Now, I finally understand when to use this tactic.

/-- There is someone in the pub such that, if the person is drinking, then everyone in the pub is
drinking. -/
theorem exists_isDrinking_imp_forall_isDrinking : ∃ (x : Pub), IsDrinking x → ∀ (y : Pub),
    IsDrinking y := by
  simp_rw [Decidable.imp_iff_not_or]
  rw [exists_or_right, ←not_forall, or_comm]
  apply em

Is there a possibility that simp_rw will be moved to the upstream in the future?

[Ruben Van de Velde]

What do you mean by upstream?

[Ruben Van de Velde]

Wait, it's in mathlib? Why isn't it in lean core?

[Ruben Van de Velde]

In any case, it's little more than a sequence of simp only, if you don't have mathlib

[Patrick Massot]

Bulhwi Cha said:

Eric Wieser said:

funext_propext shouldn't be needed, simp_rw should work fine

Now, I finally understand when to use this tactic.

I’m afraid this isn’t true. An isolated simp_rw is never more than a simp only. The suggestion to use simp_rw was a way to merge the first two lines of your code.

[Patrick Massot]

Or even put everything on one line probably.

[Bulhwi Cha]

/-- There is someone in the pub such that, if the person is drinking, then everyone in the pub is
drinking. -/
theorem exists_isDrinking_imp_forall_isDrinking' : ∃ (x : Pub), IsDrinking x → ∀ (y : Pub),
    IsDrinking y := by
  simp [Decidable.imp_iff_not_or, exists_or_right, ←not_forall, or_comm, em]

My bad. I must've deluded myself that I had already tried using simp.

[Violeta Hernández]

(this is not what the thread is about, but I think the drinker paradox would be a nice addition to Mathlib, stated in terms of an arbitrary predicate {p : α → Prop} instead)