Martin Escardo and Paulo Oliva 2011

\begin{code}

{-# OPTIONS --without-K #-}

module InfinitePigeon.InfinitePigeonLessEfficient where

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

\end{code}

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 InfinitePigeon.K-AC-N and InfinitePigeon.K-Shift.

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 the modules
InfinitePigeon.InfinitePigeonOriginal, InfinitePigeon.InfinitePigeon2011-05-12
and InfinitePigeon.InfinitePigeon. Also, this proof switches the case
analysis, and this causes funny subsequences in some cases.

Definition:

\begin{code}

Pigeonhole-Lemma : {R : Ω} → ₂ℕ → Ω
Pigeonhole-Lemma {R} α =
  ∃ \(b : ₂) → ∃ \(f : ℕ → ℕ) → ∀(n : ℕ) → K{R}(α(n + f n + ) ≡ 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 + ) ≡ ₁)

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

    lemma₂ : (∃ \(f : ℕ → ℕ) → ∀(n : ℕ) → K(α(n + f n + ) ≡ ₁)) →
              ∃ \(b : ₂) → ∃ \(f : ℕ → ℕ) → ∀(n : ℕ) → K(α(n + f n + ) ≡ b)
    lemma₂ = ∃-intro ₁

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

    lemma₄-₁ :
     (∃ \(n : ℕ) → (∃ \(i : ℕ) →  K(α(n + i + ) ≡ ₁)) → R) →
      ∃ \(n : ℕ) →  ∀  (i : ℕ) → (K(α(n + i + ) ≡ ₁)) → R
    lemma₄-₁ (∃-intro n e) = ∃-intro n (not-exists-implies-forall-not e)

    lemma₄ :
      K∃ \(n : ℕ) → ∀(i : ℕ) → (K(α(n + i + ) ≡ ₁)) → R
    lemma₄ = K-functor lemma₄-₁ lemma₃

    lemma₅-₁ :
     (∃ \(n : ℕ) → ∀ (i : ℕ) → K(α(n + i + ) ≡ ₁ → R)) →
      ∃ \(n : ℕ) → ∀ (i : ℕ) → K(α(n + i + ) ≡ ₀)
    lemma₅-₁ (∃-intro n f) =
             ∃-intro n (λ i → not-1-must-be-0 (α(n + i + )) (f i))

    lemma₅ :
      K∃ \(n : ℕ) → ∀(i : ℕ) → K(α(n + i + ) ≡ ₀)
    lemma₅ = K-functor lemma₅-₁ lemma₄

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

    lemma₆ :
      K∃ \(i : ℕ) → ∀(n : ℕ) → K(α(n + i + ) ≡ ₀)
    lemma₆ = K-functor lemma₆-₁ lemma₅

    lemma₇-₁ :
     (∃ \(i : ℕ) → ∀(n : ℕ) → K(α(n + i + ) ≡ ₀)) →
      ∃ \(b : ₂) → ∃ \(f : ℕ → ℕ) → ∀(n : ℕ) → K{R}(α(n + f n + ) ≡ b)
    lemma₇-₁ (∃-intro i a) = ∃-intro ₀ (∃-intro (λ n → i) a)

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

\end{code}

Definition:

\begin{code}

Pigeonhole : {R : Ω} → ₂ℕ → Ω
Pigeonhole {R} α =
   ∃ \(b : ₂) → ∃ \(g : ℕ → ℕ) →
   ∀(i : ℕ) → g i < g(i + ) ∧ 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 + ) ≡ b))
   → ∃ \(b : ₂) → ∃ \(g : ℕ → ℕ) → ∀(n : ℕ) → g n < g(n + ) ∧ K {R}(α(g n) ≡ b)
  lemma₀ (∃-intro b (∃-intro f h)) =
          ∃-intro b (∃-intro g λ n → ∧-intro (lemma₁ n) (lemma₂ n))
   where
    g : ℕ → ℕ
    g  =  + f  + 
    g(succ n) = let m = g n in m + f m + 

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

    lemma₂ : ∀(n : ℕ) → K(α(g n) ≡ b)
    lemma₂  = h 
    lemma₂ (succ n) = h(g n)

\end{code}