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 + ) → ℕ) →
                    (∀(n : smaller m) → s(coerce n) < s(fsucc n))
                  ∧ (∀(n : smaller(m + )) → α(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 + ) → ℕ) →
                    (∀(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))))))


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