module InfinitePigeon where

----------------------------------------------------------------------
--
-- Running a classical proof with choice in Agda.
-- 
----------------------------------------------------------------------
-- Martin Escardo & Paulo Oliva. 
-- Version of 12th May 2011, slightly simplified 19th May 2011.
--
----------------------------------------------------------------------
--     Theorem (Pigeonhole Principle). 
--
--             Every infinite boolean sequence has a constant infinite
--             subsequence.
----------------------------------------------------------------------
--
-- We give a proof that uses excluded middle and countable choice.
--
-- In the module FinitePigeon.agda we derive a corollary that we run
-- in the module Examples.agda, namely that every infinite sequence
-- has constant subsequences of arbitrary length. The point is to
-- illustrate in Agda how we can get witnesses from classical proofs
-- that use countable choice. The finite pigeonhole principle has a
-- simple constructive proof, of course, and hence this is really for
-- illustration purposes only.

-- We work with Friedman's A-translation, which prefixes the
-- generalized double-negation modality K in front of existential
-- quantifiers, disjunctions and equations, where KA = ((A→R)→R) is
-- defined in the module JK-Monads.agda. The proposition R is
-- arbitrary in the proofs of this module, but carefully chosen in the
-- main theorem of the module FinitePigeon.agda, by an application of
-- Friedman's trick. We don't work strictly with the A-translation:
-- when we can get away with it, we place fewer K's than the
-- formal definition of the translation demands.
--
-- Because ⊥ (false) is the empty disjunction, it gets translated to 
-- K ⊥, which is equivalent to R. So think of R as ⊥ in the proofs
-- below. Of course, it is not true that R→A for any A (ex falso
-- quodlibet, or ⊥-elimination). But this does hold for any A in the
-- image of the translation.
--
-- Classical countable choice (i.e. choice formulated with the
-- classical existential quantifier) is given a proof term via the
-- K-shift (more commonly known as the double negation shift) in the
-- module K-AC-N.agda and K-Shift.agda. We use either of (1) the
-- Berardi-Bezem-Coquand functional (1998), (2) Berger-Oliva's
-- modified bar recursion (2005), (3) Escardo-Oliva's countable
-- product of selection functions (2010).
--
-- References.
--
--    S. Berardi, M. Bezem, and T. Coquand.  On the Computational
--    Content of the Axiom of Choice.  J. Symbolic Logic, Volume 63,
--    Issue 2 (1998), 600-622.
--    
--    U. Berger and P. Oliva. Modified bar recursion.  Mathematical
--    Structures in Computer Science, 16(2):163-183, 2006
--
--    U. Berger and P.Oliva. Modified bar recursion and classical
--    dependent choice. Lecture Notes in Logic, 20:89-107, 2005
--
--    M. Escardo and P. Oliva.  Selection functions, bar recursion,
--    and backward induction.  Mathematical Structures in Computer
--    Science, Volume 20, Issue 2, 2010, Cambridge University Press.
--
--    M. Escardo and P. Oliva.  The Peirce translation and the double
--    negation shift. CiE 2010, Springer LNCS.
--
--    M. Escardo and P. Oliva.  What Sequential Games, the Tychonoff
--    Theorem and the Double-Negation Shift have in Common. ACM
--    SIGPLAN MSFP 2010.
--
-----------------------------------------------------------------------
-- Navigate the automatically generated html version of this set of
-- files by clicking at any word or symbol, to be taken to where it is
-- defined.
-----------------------------------------------------------------------


open import Logic
open import LogicalFacts
open import Two
open import Naturals
open import Addition
open import Order
open import Cantor
open import JK-Monads
open import Equality
open import K-AC-N
open import JK-LogicalFacts


Pigeonhole : {R : Ω}  ₂ℕ  Ω
Pigeonhole {R} α = 
    \(b : )   \(g :   ) 
   ∀(i : )  g i < g(i + 1)  K {R} (α(g i)  b)


pigeonhole : {R : Ω}  
----------

    ∀(α : ₂ℕ)  K(Pigeonhole α)

pigeonhole {R} α = K-∨-elim case₀ case₁ K-Excluded-Middle
 where 
  A : Ω
  A =  \(n : )  ∀(i : )  K(α(n + i)  )

  case₀ : A  K(Pigeonhole α)
  case₀ = ηK  lemma₁
   where
    lemma₁ : A  Pigeonhole α
    lemma₁ (∃-intro n h) = 
            ∃-intro  (∃-intro  i  n + i) 
                                λ i  (∧-intro (less-proof 0) (h i)))

  case₁ : (A  R)  K(Pigeonhole α)
  case₁ assumption =  K-functor lemma₇ lemma₆
   where
    lemma₂ : ∀(n : )  (∀(i : )  K(α(n + i)  ))  R
    lemma₂ = not-exists-implies-forall-not assumption

    lemma₃ : ∀(n : )  K∃ \(i : )  K(α(n + i)  )
    lemma₃ = lemma₄ lemma₂
     where 
      lemma₄ : (∀(n : )  (∀(i : )  K(α(n + i)  ))  R) 
               (∀(n : )  K∃ \(i : )  K(α(n + i)  ))
      lemma₄ h n = K-functor lemma₅ (not-forall-not-implies-K-exists(h n))
       where 
        lemma₅ : ( \(i : )  α(n + i)    R)   \(i : )  K(α(n + i)  )
        lemma₅ (∃-intro i r) = (∃-intro i (two-equality-cases (α(n + i)) r))

    lemma₆ : K∃ \(f :   )  ∀(n : )  K(α(n + f n)  )
    lemma₆ = K-AC-ℕ efqs lemma₃
     where efqs : ∀(n : )  R   \(i : )  K(α(n + i)  )
           efqs n r = ∃-intro 0  p  r)

    lemma₇ : ( \(f :   )  ∀(n : )  K(α(n + f n)  ))  Pigeonhole α
    lemma₇ (∃-intro f h) = 
            ∃-intro  (∃-intro g λ i  (∧-intro (fact₀ i) (fact₁ i)))
     where 
      g :    
      g 0 = 0 + f 0
      g(succ i) = let j = g i + 1 in  j + f j

      fact₀ : ∀(i : )  g i < g(i + 1)
      fact₀ i = let n = f(g i + 1)
                in ∃-intro n (trivial-addition-rearrangement (g i) n 1)
 
        
      fact₁ : ∀(i : )  K(α(g i)  )
      fact₁ 0 = h 0
      fact₁ (succ i) = h(g i + 1)