\import Arith.Nat
\import Data.Array
\import Data.Or
\import Function
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Relation.Equivalence
\import Set
\import Set.Fin
\import Set.Fin.Pigeonhole

\class KFinSet \extends BoundedPigeonholeSet {
  | finSurj : ∃ (f : Fin finCard -> E) (isSurj f)
  | boundedPigeonhole => \case finSurj \with {
    | inP (f,s) => boundedPigeonhole {pigeonhole-surj (\new BoundedPigeonholeSet (Fin finCard) finCard (pigeonhole-fin __ id<suc)) f s}
  }

  \lemma search (A : E -> \Prop) (d : \Pi (e : E) -> Dec (A e)) : Dec (∃ (e : E) (A e))
    => \case finSurj \with {
      | inP (f,fs) => \case FinSet.searchFin (\lam j => A (f j)) (\lam j => d (f j)) \with {
        | inl a => yes (inP (f a., a.))
        | inr q => no \lam (inP t) => \case fs t. \with {
          | inP (j,p) => q j (transportInv A p t.)
        }
      }
    }

  \lemma search_yes_reduce {A : E -> \Prop} (d : \Pi (e : E) -> Dec (A e)) (e : ∃ (e : E) (A e)) : search A d = yes e
    => prop-pi

  \lemma search_no_reduce {A : E -> \Prop} (d : \Pi (e : E) -> Dec (A e)) (q : Not (∃ (e : E) (A e))) : search A d = no q
    => prop-pi

  \lemma dec : Dec (TruncP E)
    => cases (finCard,finSurj) \with {
      | , inP (f,fs) => no \lam (inP x) => \case fs x \with {
        | inP ((),_)
      }
      | suc n, inP (f,fs) => yes $ inP (f )
    }
} \where {
    \lemma fromArray {A : \Set} (l : Array A) (p : \Pi (a : A) -> ∃ (i : Fin l.len) (l i = a)) : KFinSet A l.len \cowith
      | finSurj => inP (l,p)

    \lemma toArray (A : KFinSet) : ∃ (l : Array A) ∀ a ∃ (i : Fin l.len) (l i = a)
      => TruncP.map A.finSurj \lam (f,p) => (f,p)

    \lemma KFin+Dec=>Fin {A : \Set} (k : KFinSet A) {d : DecSet A} : FinSet A
      => \case toArray k \with {
        | inP (l,q) =>
          \let l' => nub l
          \in FinSet.fromArray l' (\lam a => TruncP.map (q a) \lam p =>
              \let t => nub-isSurj l p.
              \in (t., t. *> p.)) nub-isInj
      }
}

\lemma QuotientKFin {A : KFinSet} {R : A -> A -> \Type} : KFinSet (Quotient R) A.finCard \cowith
  | finSurj => TruncP.map A.finSurj \lam s => (\lam j => in~ (s. j), \lam (in~ x) => TruncP.map (s. x) \lam r => (r., pmap in~ r.))