\import Algebra.Group.Symmetric (symmetric-rec)
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Semiring
\import Arith.Fin (FinLinearOrder)
\import Arith.Nat \using (NatSemiring, pred \as pred')
\import Data.Bool
\import Data.Fin (fpred, fsuc, fsuc/=, nat_fin_=)
\import Data.Or
\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence
\import Function
\import Function.Meta ($) \import HLevel \import Logic \import Logic.Classical \import Logic.Meta \import Meta \import Order.LinearOrder \import Order.PartialOrder \import Order.StrictOrder \import Paths \import Paths.Meta \import Set \import Set.Fin.KFin \import Set.Fin.Pigeonhole \open LinearlyOrderedAbMonoid(<=_+) \class FinSet \extends KFinSet, Choice, DecSet { | finEq : TruncP (Equiv {Fin finCard} {E}) | finSurj => TruncP.map finEq \lam (e : Equiv {Fin finCard} {E}) => (e, isSurjMap {ESEquiv.fromEquiv e}) | choice {B} => \case finEq \with { | inP e => (rewrite (Equiv-to-= e) in finiteAC {finCard}) {B} } \default decideEq x y => \case finEq \with { | inP (e : Equiv) => \case decideEq {FinLinearOrder.FinLinearOrderInst} (e.ret x) (e.ret y) \with { | yes q => yes (Equiv.isInj {symQEquiv e} q) | no q => no \lam p => q (pmap e.ret p) } } | # => /= | nonEqualApart p => p | #-irreflexive p => p idp | #-symmetric => /=-sym | #-comparison x y z x/=z => \case decideEq x y \with { | yes x=y => byRight (\lam y=z => x/=z (x=y *> y=z)) | no x/=y => byLeft x/=y } | tightness {x} {y} x//=y => \case decideEq x y \with { | yes x=y => x=y | no x/=y => absurd (x//=y x/=y) } } \where { \use \level levelProp {A : \Set} (X Y : FinSet A) : X = Y => ext (\case X.finEq, Y.finEq \with { | inP Xcard=A, inP Ycard=A => FinCardBij (Xcard=A transEquiv symQEquiv Ycard=A) }) \lemma finiteAC {n : Nat} {A : Fin n -> \Type} (f : \Pi (i : Fin n) -> TruncP (A i)) : TruncP (\Pi (i : Fin n) -> A i) \elim n | 0 => inP (\case __) | suc n => \case f 0, finiteAC (\lam i => f (suc i)) \with { | inP a0, inP aS => inP \case \elim __ \with { | 0 => a0 | suc i => aS i } } \func searchFin {n : Nat} (A : Fin n -> \Prop) (d : \Pi (j : Fin n) -> Dec (A j)) : Or (\Sigma (j0 : Fin n) (A j0) (\Pi (j : Fin n) -> A j -> (j0 : Nat) <= j)) (\Pi (j : Fin n) -> Not (A j)) \elim n | 0 => inr (\case __) | suc n => \case d 0, searchFin _ (\lam j => d (suc j)) \with { | yes e, _ => inl (0, e, \lam j _ => zero<=_) | no e, inl (j0,Aj0,u) => inl (suc j0, Aj0, \case \elim __ \with { | 0 => \lam A0 => absurd (e A0) | suc j => \lam Aj+1 => suc<=suc (u j Aj+1) }) | no e, inr f => inr \case \elim __ \with { | 0 => e | suc j => f j } } \func searchFin-equiv {B : \Type} {n : Nat} (e : Equiv {Fin n} {B}) (A : B -> \Prop) (d : \Pi (b : B) -> Dec (A b)) : Or (\Sigma (b : B) (A b)) (\Pi (b : B) -> Not (A b)) => \case searchFin (\lam j => A (e j)) (\lam j => d (e j)) \with { | inl p => inl (e p.1, p.2) | inr q => inr \lam b Ab => q (e.ret b)$ transportInv A (e.f_ret b) Ab
}

\lemma searchFin-unique {n : Nat} (A : Fin n -> \Prop) (d : \Pi (j : Fin n) -> Dec (A j)) (c : ∃ (j : Fin n) (A j))
: Contr (\Sigma (j0 : Fin n) (A j0) (\Pi (j : Fin n) -> A j -> (j0 : Nat) <= j))
=> \case \elim c \with {
| inP (j,Aj) => isProp=>isContr (\lam t s => ext $nat_fin_=$ <=-antisymmetric (t.3 s.1 s.2) (s.3 t.1 t.2)) \case searchFin A d \with {
| inl r => r
| inr e => absurd (e j Aj)
}
}

\func pred {n : Nat} (x : Fin (suc (suc n))) : Fin (suc n) \elim x
| 0 => 0
| suc x => x

\lemma suc-isInj {n : Nat} (x y : Fin n) (p : suc x = suc y) : x = y \elim n
| suc n => pmap pred p

\lemma FinCardBij {n m : Nat} (p : Equiv {Fin n} {Fin m}) : n = m =>
\have | e  : ESEquiv => p
| e' : ESEquiv => ESEquiv.fromEquiv (symQEquiv p)
\in <=-antisymmetric (FinCardInj e  (\lam {x} {y} => sec {e.isEmb  x y}))
(FinCardInj e' (\lam {x} {y} => sec {e'.isEmb x y}))

\lemma FinCardInj {n m : Nat} (f : Fin n -> Fin m) (f-inj : isInj f) : n <= m \elim n, m
| 0, _ => zero<=_
| suc n, 0 => \case f 0
| suc n, suc m => suc<=suc (FinCardInj (\lam x => skip (f 0) (f (suc x)) (\lam f_0=f_suc => \case f-inj f_0=f_suc))
(\lam {x} {y} p => suc-isInj x y (f-inj (skip-isInj p))))

\func skip {n : Nat} (x0 x : Fin (suc n)) (d : x0 /= x) : Fin n \elim n, x0, x
| _, 0, 0 => absurd (d idp)
| _, 0, suc x => x
| suc n, suc x0, 0 => 0
| suc n, suc x0, suc x => suc (skip x0 x (\lam x0=x => d (pmap (suc __) x0=x)))

\lemma skip-isInj {n : Nat} {x0 x y : Fin (suc n)} {d : x0 /= x} {d' : x0 /= y} (p : skip x0 x d = skip x0 y d') : x = y \elim n, x0, x, y
| _, 0, 0, _ => absurd (d idp)
| _, 0, _, 0 => absurd (d' idp)
| _, _, 0, 0 => idp
| suc n, 0, suc x, suc y => pmap (suc __) p
| suc n, suc x0, 0, suc y => \case p
| suc n, suc x0, suc x, 0 => \case p
| suc n, suc x0, suc x, suc y => pmap (suc __) (skip-isInj (suc-isInj _ _ p))

\lemma sface_skip {n : Nat} {x0 x : Fin (suc n)} {d : x0 /= x} : sface x0 (skip x0 x d) = x \elim n, x0, x
| _, 0, 0 => absurd (d idp)
| suc n, 0, suc x => idp
| suc n, suc x0, 0 => idp
| suc n, suc x0, suc x => pmap fsuc sface_skip

\lemma skip_sface {n : Nat} {k : Fin (suc n)} {i : Fin n} {d : k /= sface k i} : skip k (sface k i) d = i \elim n, k, i
| suc n, 0, i => idp
| suc n, suc k, 0 => idp
| suc n, suc k, suc i => pmap fsuc skip_sface

\open NatSemiring(<,suc<suc,zero<suc)

\lemma skip_< {n : Nat} {x0 x x' : Fin (suc n)} {d : x0 /= x} {d' : x0 /= x'} (p : skip x0 x d < skip x0 x' d') : x < x' \elim n, x0, x, x', p
| _, 0, 0, _, _ => absurd (d idp)
| _, 0, _, 0, _ => absurd (d' idp)
| suc n, 0, suc x, suc x', p => suc<suc p
| suc n, suc x0, 0, suc x', p => zero<suc
| suc n, suc x0, suc x, suc x', suc<suc p => suc<suc (skip_< p)

\lemma <_skip {n : Nat} {x0 x x' : Fin (suc n)} {d : x0 /= x} {d' : x0 /= x'} (p : x < x') : skip x0 x d < skip x0 x' d' \elim n, x0, x, x', p
| _, 0, 0, _, _ => absurd (d idp)
| _, 0, _, 0, _ => absurd (d' idp)
| suc n, 0, suc x, suc x', suc<suc p => p
| suc n, suc x0, 0, suc x', p => zero<suc
| suc n, suc x0, suc x, suc x', suc<suc p => suc<suc (<_skip p)

\lemma skip-left {n : Nat} {x0 x : Fin (suc n)} {d : x0 /= x} (p : x < x0) : skip x0 x d = {Nat} x \elim n, x0, x, p
| 0, 0, 0, ()
| suc n, suc x0, 0, _ => idp
| suc n, suc x0, suc x, suc<suc p => pmap suc (skip-left p)

\lemma skip-right {n : Nat} {x0 x : Fin (suc n)} {d : x0 /= x} (p : x0 < x) : skip x0 x d = {Nat} pred' x \elim n, x0, x, p
| 0, 0, 0, ()
| suc n, 0, suc x, _ => idp
| suc n, suc x0, 0, _ => idp
| suc n, suc x0, suc x, suc<suc p => pmap suc (skip-right p) *> suc_pred (/=-sym $StrictPoset.<_/=$ zero<=_ <∘r p)

\lemma fromArray {A : \Set} (l : Array A) (p : \Pi (a : A) -> ∃ (i : Fin l.len) (l i = a)) (q : \Pi {i j : Fin l.len} -> l i = l j -> i = j) : FinSet A l.len \cowith
| finEq => inP (Equiv.fromInjSurj l q p)
}

\lemma finCard_Equiv {A B : FinSet} (e : Equiv {A} {B}) : A.finCard = B.finCard
=> \case A.finEq, B.finEq \with {
| inP e1, inP e2 => FinSet.FinCardBij $e1 transEquiv e transEquiv symQEquiv e2 } \lemma finCard_inj {A B : FinSet} (f : A -> B) (inj : isInj f) : A.finCard <= B.finCard => \case A.finEq, B.finEq \with { | inP (e1 : Equiv), inP (e2 : Equiv) => FinSet.FinCardInj (\lam x => e2.ret (f (e1 x))) \lam p => e1.isInj$ inj $Equiv.isInj {symQEquiv e2} p } \lemma transport_zero {n m : Nat} (p : n = m) : transport Fin (pmap suc p) 0 = 0 \elim p | idp => idp \lemma transport_suc {n m : Nat} (p : n = m) (x : Fin n) : transport Fin (pmap suc p) (suc x) = suc (transport Fin p x) \elim p | idp => idp \func fin-inc_<= {n m : Nat} (p : n <= m) (i : Fin n) : Fin m => toFin i (fin_< i <∘l p) \func fin-inc {n m : Nat} (i : Fin n) : Fin (n + m) \elim n, i | suc n, 0 => 0 | suc n, suc i => suc (fin-inc i) \where { \lemma char {n m : Nat} {i : Fin n} : fin-inc {n} {m} i = {Nat} i \elim n, i | suc n, 0 => idp | suc n, suc i => pmap suc char \lemma char_nat {n : Nat} (i : Nat) : fin-inc {suc i} {n} i = {Nat} i => char *> mod_< id<suc } \func fin-inc-right {n m : Nat} (i : Fin m) : Fin (n + m) => fin-inc_<= (<=_+ zero<=_ <=-refl) i \where { \lemma char_nat {n : Nat} (i : Nat) : fin-inc-right {n} {suc i} i = {Nat} i => toFin=id *> mod_< id<suc } \func fin-raise {n k : Nat} (i : Fin n) : Fin (k + n) \elim k | 0 => i | suc k => suc (fin-raise i) \func sface {n : Nat} (k : Fin (suc n)) (i : Fin n) : Fin (suc n) \elim n, k, i | suc n, 0, i => suc i | suc n, suc k, 0 => 0 | suc n, suc k, suc i => suc (sface k i) \lemma sface-skip {n : Nat} {k : Fin (suc n)} {i : Fin n} : sface k i /= k \elim n, k, i | suc n, 0, i => \case __ | suc n, suc k, 0 => \case __ | suc n, suc k, suc i => fsuc/= sface-skip \lemma sface-inj {n : Nat} {k : Fin (suc n)} {i i' : Fin n} (p : sface k i = sface k i') : i = i' \elim n, k, i, i' | suc n, 0, i, i' => pmap (fpred i) p | suc n, suc k, 0, 0 => idp | suc n, suc k, 0, suc i' => \case p | suc n, suc k, suc i, 0 => \case p | suc n, suc k, suc i, suc i' => pmap fsuc$ sface-inj $pmap (fpred k) p \func cyclePerm {n : Nat} (k : Fin n) : QEquiv {Fin n} {Fin n} \elim n | suc n => ret {symmetric-rec} (k,idEquiv) \instance EmptyFin : FinSet Empty | finCard => 0 | finEq => inP \new QEquiv { | f => \case __ | ret => \case __ | ret_f => \case __ | f_sec => \case __ } \instance UnitFin : FinSet (\Sigma) | finCard => 1 | finEq => inP \new QEquiv { | f _ => () | ret _ => 0 | ret_f (0) => idp | f_sec _ => idp } \instance BoolFin : FinSet Bool 2 | finEq => inP equiv \where \func equiv : QEquiv {Fin 2} {Bool} \cowith | f => \case __ \with { | 0 => true | 1 => false } | ret => \case __ \with { | true => 0 | false => 1 } | ret_f => \case \elim __ \with { | 0 => idp | 1 => idp } | f_sec => cases __ idp \instance FinFin (n : Nat) : FinSet (Fin n) | finCard => n | finEq => inP idEquiv | decideEq => FinLinearOrder.FinLinearOrderInst.decideEq \instance OrFin (S T : FinSet) : FinSet (Or S T) | finCard => S.finCard + T.finCard | finEq => \case S.finEq, T.finEq \with { | inP Se, inP Te => inP$ =-to-Equiv $QEquiv-to-= (aux {S.finCard} {T.finCard}) *> pmap2 Or (Equiv-to-= Se) (Equiv-to-= Te) } \where { \func aux {n m : Nat} : QEquiv {Fin (n + m)} {Or (Fin n) (Fin m)} \cowith | f (i : Fin (n + m)) : Or (Fin n) (Fin m) \elim n, i { | 0, i => inr i | suc n, 0 => inl 0 | suc n, suc i => Or.map (f i) fsuc id } | ret (e : Or (Fin n) (Fin m)) : Fin (n + m) \with { | inl s => fin-inc s | inr t => fin-raise t } | ret_f (i : Fin (n + m)) : ret (f i) = i \elim n, i { | 0, i => idp | suc n, 0 => idp | suc n, suc i => cases (f i arg addPath) \with { | inl s, p => \have q => inv (pmap ret p) *> ret_f i \in \case \elim n, \elim i, \elim s, \elim q \with { | suc n, i, s, q => pmap fsuc q } | inr t, p => pmap (\lam i => suc i) (inv (pmap ret p) *> ret_f i) } } | f_sec => \case \elim __ \with { | inl s => ret_inl-lem s | inr t => ret_inr-lem t } \lemma ret_inl-lem {n m : Nat} (i : Fin n) : OrFin.aux.f {n} {m} (fin-inc i) = inl i \elim n, i | suc n, 0 => idp | suc n, suc i => rewrite ret_inl-lem idp \lemma ret_inr-lem {n m : Nat} (t : Fin m) : aux.f (fin-raise {m} {n} t) = inr t \elim n | 0 => idp | suc n => rewrite (ret_inr-lem {n} t) idp } \lemma SigmaFin (S : FinSet) (Q : S -> FinSet) : FinSet (\Sigma (i : S) (Q i)) (AbMonoid.FinSum (\lam i => finCard {Q i})) => \case AbMonoid.FinSum_char (\lam i => finCard {Q i}) \with { | inP p => rewrite p.2 \new FinSet { | finEq => \case FinSet.finiteAC (\lam i => finEq {Q (p.1 i)}) \with { | inP d => inP$ aux transEquiv sigma-right d transEquiv sigma-left p.1
}
}
}
\where {

\func aux {n : Nat} {Q : Fin n -> Nat} : QEquiv {Fin (BigSum Q)} {\Sigma (i : Fin n) (Fin (Q i))} \cowith
| f (k : Fin (BigSum Q)) : \Sigma (i : Fin n) (Fin (Q i)) \elim n {
| suc n => \case OrFin.aux.f k \with {
| inl s => (0,s)
| inr t => \have (i,r) => f t \in (suc i, r)
}
}
| ret (p : \Sigma (i : Fin n) (Fin (Q i))) : Fin (BigSum Q) \elim n, p {
| 0, ((),_)
| suc n, (0, j) => fin-inc j
| suc n, (suc i, j) => fin-raise (ret (i,j))
}
| ret_f (k : Fin (BigSum Q)) : ret (f k) = k \elim n {
| suc n => mcases {_} {arg addPath} \with {
| inl s, p => inv (pmap OrFin.aux.ret p) *> OrFin.aux.ret_f k
| inr t, p => pmap fin-raise (ret_f t) *> inv (pmap OrFin.aux.ret p) *> OrFin.aux.ret_f k
}
}
| f_sec (p : \Sigma (i : Fin n) (Fin (Q i))) : f (ret p) = p \elim n, p {
| 0, ((),_)
| suc n, (0, j) => rewrite OrFin.ret_inl-lem idp
| suc n, (suc i, j) => rewrite OrFin.ret_inr-lem (rewrite (f_sec {n} {\lam i => Q (suc i)} (i,j)) idp)
}
}

\instance ProdFin (A B : FinSet) : FinSet (\Sigma A B) (A.finCard Nat.* B.finCard)
=> transport (FinSet _) Semiring.FinSum_replicate $SigmaFin A (\lam _ => B) \where { \func prod_equiv {n m : Nat} : Equiv {Fin (n Nat.* m)} {\Sigma (Fin n) (Fin m)} => transport (\lam x => Equiv {Fin x} {_}) Semiring.BigSum_replicate$ SigmaFin.aux {n} {\lam _ => m}
}

\func DecFin {P : \Prop} (d : Dec P) : FinSet P \cowith
| finCard => Dec.rec (\lam _ => 1) (\lam _ => 0) d
| finEq => inP $\case \elim d \with { | yes e => \new QEquiv { | f _ => e | ret _ => 0 | ret_f (0) => idp | f_sec => prop-isProp e } | no q => \new QEquiv { | f => \lam () | ret e => absurd (q e) | ret_f => \lam () | f_sec e => absurd (q e) } } \lemma fin_transport {n m : Nat} {j : Fin n} {p : n = m} : transport Fin p j = {Nat} j \elim p | idp => idp \func FunDec {A : FinSet} (B : A -> Decide) : Decide (\Pi (a : A) -> B a) \cowith | decide => \case A.finEq \with { | inP (e : Equiv) => \case fin-dec (\lam j => B (e j)) \with { | yes p => yes \lam a => transport (B __) (e.f_ret a)$ p (e.ret a)
| no q => no \lam f => q \lam j => f (e j)
}
}
\where {
\func fin-dec {n : Nat} (B : Fin n -> Decide) : Dec (\Pi (j : Fin n) -> B j) \elim n
| 0 => yes \case __
| suc n => \case decide {B 0}, fin-dec (\lam j => B (suc j)) \with {
| yes p, yes q => yes \case \elim __ \with {
| 0 => p
| suc j => q j
}
| _, no q => no \lam f => q \lam j => f (suc j)
| no p, _ => no \lam f => p (f 0)
}
}