```module DrinkerParadox where

-- By Martin Escardo, 2 September 2011.
---
-- We prove Theorem-3·6 of the paper
-- http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf

open import Logic
open import Equality
open import Naturals
open import Two
open import Cantor
open import GenericConvergentSequence

-- The following is the Drinker paradox for the set ℕ∞ defined in the
-- module GenericConvergentSequence: In every pub there is a person x
-- such that if x drinks then everybody drinks.
--
-- Here p x ≡ ₁ means that x drinks, and the people in the pub are the
-- members of the set ℕ∞. In general the DP is non-constructive, as
-- for example for the pub with set of costumers ℕ, this would amount
-- to LPO (limited principle of omniscience).  But it is constructive
-- for the larger pub with set of costumers ℕ∞, which is what we show
-- in this module.
--
-- (Continuity axioms and the fan principle are not assumed.)

Theorem-3·6 :
-----------------------------------------------
∀(p : ₂ℕ → ₂) → extensional p →
∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧
(p x ≡ ₁ → ∀(y : ₂ℕ) → y ∈ ℕ∞ → p y ≡ ₁)
-----------------------------------------------
Theorem-3·6 p extensionality-of-p = ∃-intro x (∧-intro Lemma₀ Lemma₁)
where
x : ₂ℕ
x 0       = p(underline 0)
x(succ n) = min (x n) (p(underline(succ n)))

Lemma₀ : x ∈ ℕ∞
Lemma₀ i = Lemma[minab≤a]

Dagger₀ : ∀(n : ℕ) → x ≣ underline n → p(underline n) ≡ ₀
Dagger₀ 0 r = r 0
Dagger₀ (succ n) r = transitivity u t
where s : x n ≡ ₁
s = transitivity (r n) (Lemma[underline-1] n)

t : x(succ n) ≡ ₀
t = transitivity (r(succ n)) (Lemma[underline-0] n)

u : p(underline(succ n)) ≡ x(succ n)
u = symmetry(extensionality(λ a → min a (p(underline(succ n)))) s)

Dagger₁ : x ≣ ∞ → ∀(n : ℕ) → p(underline n) ≡ ₁
Dagger₁ r 0 = r 0
Dagger₁ r (succ n) = transitivity u t
where s : x n ≡ ₁
s = r n

t : x(succ n) ≡ ₁
t = r(succ n)

u : p(underline(succ n)) ≡ x(succ n)
u = symmetry(extensionality(λ a → min a (p(underline(succ n)))) s)

Claim₀ : p x ≡ ₁ → ∀(n : ℕ) → ¬(x ≣ underline n)
Claim₀ r n s = Lemma[b≡₁→b≠₀] r (Lemma s)
where Lemma : x ≣ underline n → p x ≡ ₀
Lemma r = transitivity (extensionality-of-p r) (Dagger₀ n r)

Claim₁ : p x ≡ ₁ → x ≣ ∞
Claim₁ r = Lemma[ℕ∞∖underline[ℕ]⊆[∞]] x Lemma₀ (Claim₀ r)

Claim₂ : p x ≡ ₁ → ∀(n : ℕ) → p(underline n) ≡ ₁
Claim₂ r = Dagger₁(Claim₁ r)

Claim₃ : p x ≡ ₁ → p ∞ ≡ ₁
Claim₃ r = fact r (extensionality-of-p(Claim₁ r))
where fact : ∀{a b : ₂} → a ≡ ₁ → a ≡ b → b ≡ ₁
fact refl refl = refl

Lemma₁ : p x ≡ ₁ →  ∀(y : ₂ℕ) → y ∈ ℕ∞ → p y ≡ ₁
Lemma₁ r = Lemma[density] p extensionality-of-p (Claim₂ r) (Claim₃ r)
```