module FinitePigeon where

open import InfinitePigeon
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 JK-LogicalFacts
open import Finite

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

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

-- 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:

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

finite-pigeonhole-lemma : {R : Ω}  

 ∀(α : ₂ℕ)  ∀(m : )  K(Finite-Pigeonhole α m)

finite-pigeonhole-lemma {R} α m =  K-extend lemma₂ lemma₁
  lemma₀ : Pigeonhole α  Finite-Pigeonhole-K {R} α m
  lemma₀ (∃-intro b (∃-intro g h)) = 
          ∃-intro b (∃-intro s (∧-intro fact₁ fact₃))
      s : smaller(m + 1)  
      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 + 1))  α(g(embed n))  b  α(s n)  b
      fact₂ n = two-things-equal-to-a-third-are-equal reflexivity

      fact₃ : ∀(n : smaller(m + 1))  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))))))

-- 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.

Theorem :  

 ∀(α : ₂ℕ)  ∀(m : )  Finite-Pigeonhole α m

Theorem α m = finite-pigeonhole-lemma {Finite-Pigeonhole α m} α m id

-- NB. If we remove the implicit parameter in this call to
-- finite-pigeonhole-lemma, Agda infers the required R.