\import Arith.Fin
\import Arith.Nat
\import Data.Fin
\import Data.Or
\import Equiv
\import Function
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Order.LinearOrder
\import Order.StrictOrder
\import Paths
\import Set
\import Set.Fin
\import Set.Fin.DFin
\open FinLinearOrder

\class PigeonholeSet \extends BaseSet {
  | pigeonhole (f : Nat -> E) : ∃ (i j : Nat) (i /= j) (f i = f j)

  \lemma pigeonhole< (f : Nat -> E) : ∃ (i j : Nat) (i < j) (f i = f j)
    => TruncP.map (pigeonhole f) \lam t => \case LinearOrder.trichotomy t. t. \with {
      | less c => (t., t., c, t.)
      | equals c => absurd (t. c)
      | greater c => (t., t., c, inv t.)
    }

  \lemma isEquiv (f : E -> E) (inj : isInj f) : Equiv f
    => isDFin.isEquiv (isDFin.fromPigeonhole \this) f inj
}

\class BoundedPigeonholeSet \extends PigeonholeSet {
  | finCard : Nat
  | boundedPigeonhole (f : Fin (suc finCard) -> E) : ∃ (i j : Fin (suc finCard)) (i /= j) (f i = f j)
  | pigeonhole f => TruncP.map (boundedPigeonhole (\lam j => f j)) \lam t => (t., t., fin_nat_/= t., t.)

  \lemma boundedPigeonhole< (f : Fin (suc finCard) -> E) : ∃ (i j : Fin (suc finCard)) (i < j) (f i = f j)
    => TruncP.map (boundedPigeonhole f) \lam t => \case LinearOrder.trichotomy t. t. \with {
      | less c => (t., t., c, t.)
      | equals c => absurd (t. c)
      | greater c => (t., t., c, inv t.)
    }
}

\lemma pigeonhole-surj (A : BoundedPigeonholeSet) {B : \Set} (f : A -> B) (s : isSurj f) : BoundedPigeonholeSet B A.finCard \cowith
  | boundedPigeonhole g =>\have | (inP t) => FinSet.finiteAC (\lam j => s (g j))
                          | (inP r) => boundedPigeonhole (\lam j => (t j).)
                    \in inP (r., r., r., inv (t r.). *> pmap f r. *> (t r.).)

\lemma pigeonhole-fin {n m : Nat} (f : Fin m -> Fin n) (p : n < m) : ∃ (i j : Fin m) (i /= j) (f i = f j)
  => aux f \lam inj => <-irreflexive $ p <∘l FinSet.FinCardInj f inj
  \where {
    \lemma search-pair {n : Nat} {A : DecSet} (f : Fin n -> A) : Dec (∃ (i j : Fin n) (i /= j) (f i = f j))
      => \have t i : Dec (∃ (j : Fin n) (i /= j) (f i = f j)) => \case FinSet.searchFin (\lam j => \Sigma (i /= j) (f i = f j)) (\lam j => decide) \with {
           | inl (j,p,_) => yes (inP (j, p., p.))
           | inr q => no \lam (inP (j, s, p)) => q j (s,p)
         }
         \in \case FinSet.searchFin _ t \with {
          | inl (i,p,_) => yes $ TruncP.map p (\lam q => (i, q., q., q.))
          | inr q => no \lam (inP (i,j,e,p)) => q i (inP (j, e, p))
        }

    \lemma aux {n : Nat} {A : DecSet} (f : Fin n -> A) (p : Not (isInj f)) : ∃ (i j : Fin n) (i /= j) (f i = f j)
      => \case search-pair f \with {
        | yes e => e
        | no q => absurd $ p \lam {i} {j} p => \case decideEq i j \with {
          | yes e => e
          | no r => absurd $ q $ inP (i, j, r, p)
        }
      }
  }