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)