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        = p(underline )
  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₀  r = r 
  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  = r 
  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)