\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.1 t.2 \with { | less c => (t.1, t.2, c, t.4) | equals c => absurd (t.3 c) | greater c => (t.2, t.1, c, inv t.4) } \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.1, t.2, fin_nat_/= t.3, t.4) \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.1 t.2 \with { | less c => (t.1, t.2, c, t.4) | equals c => absurd (t.3 c) | greater c => (t.2, t.1, c, inv t.4) } } \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).1) \in inP (r.1, r.2, r.3, inv (t r.1).2 *> pmap f r.4 *> (t r.2).2) \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.1, p.2))
| 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.1, q.2, q.3)) | 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)
}
}
}