module InfinitePigeonLessEfficient where

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

-- 29 April -3rd May 2011.

-- We prove a theorem that involves the classical existential
-- quantifier K∃ (called pigeonhole below). The proof uses excluded
-- middle and classical countable choice (i.e. choice formulated with
-- the classical existential quantifier), which is implemented using
-- the K-shift (more commonly known as the double negation shift) in
-- the modules JK-Choice.agda and Infinite-JK-Shifts.agda.
--
-- In the module FinitePigeon.agda we derive a statement that uses the
-- intuitionistic quantifiers (and doesn't mention the double negation
-- modality K at all), using the classical result as a lemma. In the
-- module Examples.agda we run it.

-- This is the first version. Much improved ones are in other files.
-- Also, this proof switches the case analysis, and this causes funny
-- subsequences in some cases.


-- Definition 

Pigeonhole-Lemma : {R : Ω}  ₂ℕ  Ω
Pigeonhole-Lemma {R} α = 
   \(b : )   \(f :   )  ∀(n : )  K{R}(α(n + f n + 1)  b)


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

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

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

  case₀ : A  K(Pigeonhole-Lemma α)
  case₀ a = K-functor lemma₂ lemma₁
   where 
    lemma₁ : K∃ \(f :   )  ∀(n : )  K(α(n + f n + 1)  )
    lemma₁ = K-AC-ℕ  n  λ r  ∃-intro 0  p  r)) a

    lemma₂ : ( \(f :   )  ∀(n : )  K(α(n + f n + 1)  ))  
               \(b : )   \(f :   )  ∀(n : )  K(α(n + f n + 1)  b)
    lemma₂ = ∃-intro 

  case₁ : (A  R)  K(Pigeonhole-Lemma α)
  case₁ p = lemma₇  
   where 
    lemma₃ : 
      K∃ \(n : )  ( \(i : )  K(α(n + i + 1)  ))  R
    lemma₃ = not-forall-not-implies-K-exists p

    lemma₄-₁ :  
     ( \(n : )  ( \(i : )   K(α(n + i + 1)  ))  R)  
       \(n : )     (i : )  (K(α(n + i + 1)  ))  R
    lemma₄-₁ (∃-intro n e) = ∃-intro n (not-exists-implies-forall-not e)
  
    lemma₄ : 
      K∃ \(n : )  ∀(i : )  (K(α(n + i + 1)  ))  R
    lemma₄ = K-functor lemma₄-₁ lemma₃
 
    lemma₅-₁ : 
     ( \(n : )   (i : )  K(α(n + i + 1)    R))  
       \(n : )   (i : )  K(α(n + i + 1)  )
    lemma₅-₁ (∃-intro n f) = 
             ∃-intro n  i  not-1-must-be-0 (α(n + i + 1)) (f i))

    lemma₅ : 
      K∃ \(n : )  ∀(i : )  K(α(n + i + 1)  )
    lemma₅ = K-functor lemma₅-₁ lemma₄
 
    lemma₆-₁ : 
     ( \(n : )  ∀(i : )  K(α(n + i + 1)  ))  
       \(n : )  ∀(i : )  K(α(i + n + 1)  )
    lemma₆-₁ (∃-intro n h) = ∃-intro n  i  K-functor(lemma₆-₁-₁ i)(h i))
      where 
       lemma₆-₁-₁ : ∀(i : )  α(n + i + 1)    α(i + n + 1)  
       lemma₆-₁-₁ i r = two-things-equal-to-a-third-are-equal lemma₆-₁-₁-₁ r
         where 
          lemma₆-₁-₁-₁ : α(n + i + 1)  α(i + n + 1)
          lemma₆-₁-₁-₁ = 
            compositionality  k  α(k + 1)) (addition-commutativity n i)
 
    lemma₆ : 
      K∃ \(i : )  ∀(n : )  K(α(n + i + 1)  )
    lemma₆ = K-functor lemma₆-₁ lemma₅

    lemma₇-₁ : 
     ( \(i : )  ∀(n : )  K(α(n + i + 1)  ))  
       \(b : )   \(f :   )  ∀(n : )  K{R}(α(n + f n + 1)  b)
    lemma₇-₁ (∃-intro i a) = ∃-intro  (∃-intro  n  i) a)

    lemma₇ : K(Pigeonhole-Lemma α)
    lemma₇ = K-functor lemma₇-₁ lemma₆

  
-- Definition 

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


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

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

pigeonhole {R} α = K-functor lemma₀ (pigeonhole-lemma {R} α)
 where 
  lemma₀ : 
    ( \(b : )   \(f :   )  ∀(n : )  K(α(n + f n + 1)  b)) 
      \(b : )   \(g :   )  ∀(n : )  g n < g(n + 1)  K {R}(α(g n)  b)
  lemma₀ (∃-intro b (∃-intro f h)) = 
          ∃-intro b (∃-intro g λ n  ∧-intro (lemma₁ n) (lemma₂ n))
   where g :    
         g 0 = 0 + f 0 + 1
         g(succ n) = let m = g n in m + f m + 1

         lemma₁ : ∀(n : )  g n < g(n + 1)
         lemma₁ n = less-proof(f(g n))

         lemma₂ : ∀(n : )  K(α(g n)  b)
         lemma₂ 0 = h 0
         lemma₂ (succ n) = h(g n)