-- By Martin Escardo, 2 September 2011.
-- (Rewritten December 2011 to define ℕ∞ as a type.)
--
-- We prove Theorem-3·6 of the paper
-- http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf
--
-- 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.)

module DrinkerParadox where

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

Theorem-3·6 :
----------------------------------------------------
  ∀(p : ℕ∞ → ₂) → extensional p →
  ∃ \(u : ℕ∞) → p u ≡ ₁ → ∀(v : ℕ∞) → p v ≡ ₁
----------------------------------------------------
Theorem-3·6 p extensionality-of-p = ∃-intro u Lemma
 where
  u : ℕ∞
  u = α || λ i → Lemma[minab≤a]
   where
    α : ₂ℕ
    α        = p(under )
    α(succ n) = min (α n) (p(under(succ n)))

  Dagger₀ : ∀(n : ℕ) → u ≣ under n → p(under n) ≡ ₀
  Dagger₀  r = r 
  Dagger₀ (succ n) r = transitivity w t
   where s : incl u n ≡ ₁
         s = transitivity (r n) (Lemma[bigger-1] n)

         t : incl u(succ n) ≡ ₀
         t = transitivity (r(succ n)) (Lemma[bigger-0] n)

         w : p(under(succ n)) ≡ incl u(succ n)
         w = symmetry(cong(λ a → min a (p(under(succ n)))) s)

  Dagger₁ : u ≣ ∞ → ∀(n : ℕ) → p(under n) ≡ ₁
  Dagger₁ r  = r 
  Dagger₁ r (succ n) = transitivity w t
   where s : incl u n ≡ ₁
         s = r n

         t : incl u(succ n) ≡ ₁
         t = r(succ n)

         w : p(under(succ n)) ≡ incl u(succ n)
         w = symmetry(cong(λ a → min a (p(under(succ n)))) s)

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

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

  Claim₂ : p u ≡ ₁ → ∀(n : ℕ) → p(under n) ≡ ₁
  Claim₂ r = Dagger₁(Claim₁ r)

  Claim₃ : p u ≡ ₁ → p ∞ ≡ ₁
  Claim₃ r = Lemma[x≡y→x≡z→z≡y] r (extensionality-of-p(Claim₁ r))

  Lemma : p u ≡ ₁ → ∀(v : ℕ∞) → p v ≡ ₁
  Lemma r = Lemma[density] p extensionality-of-p (Claim₂ r) (Claim₃ r)