Martin Escardo and Paulo Oliva 2011

\begin{code}

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

module InfinitePigeon.J-FinitePigeon where

open import InfinitePigeon.Addition
open import InfinitePigeon.Cantor
open import InfinitePigeon.Equality
open import InfinitePigeon.Finite
open import InfinitePigeon.J-InfinitePigeon
open import InfinitePigeon.JK-LogicalFacts
open import InfinitePigeon.JK-Monads
open import InfinitePigeon.Logic
open import InfinitePigeon.LogicalFacts
open import InfinitePigeon.Naturals
open import InfinitePigeon.Order
open import InfinitePigeon.Two

\end{code}

We use the classical, infinite pigeonhole principle (in another
module) to derive a finite one:

\begin{code}

Finite-Pigeonhole : ₂ℕ → ℕ → Ω
Finite-Pigeonhole α m =
 ∃ \(b : ₂) → ∃ \(s : smaller(m + ) → ℕ) →
                 (∀(n : smaller m) → s(coerce n) < s(fsucc n))
               ∧ (∀(n : smaller(m + )) → α(s n) ≡ b)

\end{code}

Before proving this in the theorem below, we prove it prefixed by K
in the following lemma, where some sublemmas have K deep inside,
prefixing the equation:

\begin{code}

Finite-Pigeonhole-K : {R : Ω} → ₂ℕ → ℕ → Ω
Finite-Pigeonhole-K {R} α m =
    ∃ \(b : ₂) → ∃ \(s : smaller(m + ) → ℕ) →
                    (∀(n : smaller m) → s(coerce n) < s(fsucc n))
                  ∧ (∀(n : smaller(m + )) → K{R}(α(s n) ≡ b))

postulate conjecture : {A : Set} → A

finite-pigeonhole-lemma : {R : Ω}
                          (α : ₂ℕ)
                          (m : ℕ)
                        → K{R} (Finite-Pigeonhole α m)
finite-pigeonhole-lemma {R} α m =  K-extend lemma₂ lemma₁
 where
  lemma₀ : Pigeonhole α → Finite-Pigeonhole-K {R} α m
  lemma₀ (∃-intro b (∃-intro g h)) =
   ∃-intro b (∃-intro s (∧-intro fact₁ fact₃))
    where
      s : smaller(m + ) → ℕ
      s = restriction g

      fact₀ : ∀(n : smaller m) → g(embed n) ≡ s(coerce n)
      fact₀ n = compositionality g embed-coerce-lemma

      fact₁ : ∀(n : smaller m) → s(coerce n) < s(fsucc n)
      fact₁ n = binary-predicate-compositionality {ℕ} {ℕ} {_<_}
                  (fact₀ n) reflexivity (∧-elim₀(h(embed n)))

      fact₂ : ∀(n : smaller(m + )) → α(g(embed n)) ≡ b → α(s n) ≡ b
      fact₂ n = two-things-equal-to-a-third-are-equal reflexivity

      fact₃ : ∀(n : smaller(m + )) → K(α(s n) ≡ b)
      fact₃ n = K-functor (fact₂ n) (∧-elim₁(h(embed n)))

  lemma₁ : K(Finite-Pigeonhole-K α m)
  lemma₁ = K-functor lemma₀ (J-K(pigeonhole α))

  lemma₂ : Finite-Pigeonhole-K α m → K(Finite-Pigeonhole α m)
  lemma₂ (∃-intro b (∃-intro s (∧-intro h k))) =
         (K-∃-shift(∃-intro b (K-∃-shift(∃-intro s
            (K-strength(∧-intro h (fK-∀-shift k)))))))

Theorem : ∀(α : ₂ℕ) → ∀(m : ℕ) → Finite-Pigeonhole α m
Theorem α m = finite-pigeonhole-lemma {Finite-Pigeonhole α m} α m id

\end{code}