Martin Escardo and Paulo Oliva 2011

\begin{code}

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

module InfinitePigeon.FinitePigeon where

open import InfinitePigeon.Addition
open import InfinitePigeon.Cantor
open import InfinitePigeon.Equality
open import InfinitePigeon.Finite
open import InfinitePigeon.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))


finite-pigeonhole-lemma : {R : Ω}
                          (α : ₂ℕ)
                          (m : ℕ)
                        → K(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₀ (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))))))

\end{code}

We now apply Friedman's trick. For given α and m, we let R be the
proposition we want to prove, namely Finite-Pigeonhole α m. But we
have proved K{R}R in the above lemma. Because this is (R→R)→R, we
get R if we apply it to the proof id: R→R.

\begin{code}

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

\end{code}