\import Algebra.Group.Symmetric
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Fin
\import Arith.Nat
\import Data.Bool
\import Data.Fin
\import Data.Maybe
\import Data.Or
\import Equiv
\import Function
\import Function.Meta ($) \import Logic \import Logic.Meta \import Meta \import Order.LinearOrder \import Order.PartialOrder \import Order.StrictOrder \import Paths \import Paths.Meta \import Relation.Equivalence \import Set \import Set.Fin \import Set.Fin.DFin \func mkArray {A : \Type} {n : Nat} (f : Fin n -> A) => \new Array A n f \func arrayExt {A : \Type} {n : Nat} {l l' : Array A n} (p : \Pi (j : Fin n) -> l j = l' j) : l = l' => path (\lam i => \new Array A n (\lam j => p j i)) \func tail {A : \Type} (l : Array A) : Array A \elim l | nil => nil | _ :: a => a \func taild {n : Nat} {A : Fin (suc n) -> \Type} (a : DArray A) : DArray (\lam j => A (suc j)) \elim a | _ :: a => a \func array-unext {A : \Type} {n : Nat} {l l' : Array A n} (p : l = {Array A} l') (j : Fin n) : l j = l' j \elim n, l, l', j | suc n, a :: l, a1 :: l', 0 => unhead p | suc n, a :: l, a1 :: l', suc j => array-unext (pmap tail p) j \func len=0 {A : \Type} {l : Array A} (p : l.len = 0) : l = nil \elim l | nil => idp \func map {A B : \Type} (f : A -> B) (as : Array A) : Array B \cowith | len => as.len | at i => f (as i) \func map_:: {A B : \Type} {f : A -> B} {a : A} {l : Array A} : map f (a :: l) = f a :: map f l => idp \func \infixr 5 ++' {A : \Type} (xs : Array A) {n : Nat} (ys : Array A n) : Array A (xs.len Nat.+ n) \elim xs | nil => ys | a :: xs => a :: xs ++' ys \where { \func ++'_index-left {A : \Type} {l : Array A} {n : Nat} {m : Array A n} {i : Fin l.len} : (l ++' m) (fin-inc i) = l i \elim l, i | a :: l, 0 => idp | a :: l, suc i => ++'_index-left \func ++'_index-right {A : \Type} {l : Array A} {n : Nat} {m : Array A n} {i : Fin n} : (l ++' m) (fin-raise i) = m i \elim l | nil => idp | a :: l => ++'_index-right \func split-index {n m : Nat} (i : Fin (n Nat.+ m)) : Or (\Sigma (j : Fin n) (i = fin-inc j)) (\Sigma (j : Fin m) (i = fin-raise j)) => rewriteI (OrFin.aux.ret_f i)$ cases (OrFin.aux.f i) \with {
| inl j => inl (j,idp)
| inr j => inr (j,idp)
}
}

\func ++'-split {A : \Type} {n m : Nat} {l : Array A (n Nat.+ m)} : l = (\new Array A n \lam i => l (fin-inc i)) ++' (\new Array A m \lam j => l (fin-raise j)) \elim n, l
| 0, l => idp
| suc n, a :: l => cong ++'-split

\func map_++' {A B : \Type} (f : A -> B) {l : Array A} {n : Nat} {l' : Array A n} : map f (l ++' l') = map f l ++' map f l' \elim l
| nil => idp
| :: a l =>  path (\lam i => f a :: map_++' f i)

\func \infixr 5 ++ {A : \Type} (xs ys : Array A) : Array A \elim xs
| nil => ys
| :: a xs => a :: xs ++ ys
\where {
\func index-left {A : \Type} {l m : Array A} (i : Fin l.len) : Fin (DArray.len {l ++ m}) \elim l, i
| a :: l, 0 => 0
| a :: l, suc i => suc (index-left i)

\func ++_index-left {A : \Type} {l m : Array A} (i : Fin l.len) : (l ++ m) (index-left i) = l i \elim l, i
| a :: l, 0 => idp
| a :: l, suc i => ++_index-left i

\lemma index-left-nat {A : \Type} {l m : Array A} {i : Fin l.len} : index-left {A} {l} {m} i = {Nat} i \elim l, i
| a :: l, 0 => idp
| a :: l, suc i => pmap suc index-left-nat

\lemma index-left-inj {A : \Type} {l m : Array A} : isInj (index-left {A} {l} {m})
=> \lam p => nat_fin_= $inv index-left-nat *> p *> index-left-nat \func index-right {A : \Type} {l m : Array A} (i : Fin m.len) : Fin (DArray.len {l ++ m}) \elim l | nil => i | a :: l => suc (index-right i) \func ++_index-right {A : \Type} {l m : Array A} {i : Fin m.len} : (l ++ m) (index-right i) = m i \elim l | nil => idp | a :: l => ++_index-right \lemma index-right-nat {A : \Type} {l m : Array A} {i : Fin m.len} : index-right {A} {l} i = {Nat} l.len Nat.+ i \elim l | nil => idp | a :: l => pmap suc index-right-nat \lemma index-right-inj {A : \Type} {l m : Array A} : isInj (index-right {A} {l} {m}) => \lam p => nat_fin_=$ NatSemiring.cancel-left l.len $inv index-right-nat *> p *> index-right-nat \lemma index-left/=right {A : \Type} {l m m' : Array A} {i : Fin l.len} {j : Fin m'.len} : index-left {A} {l} {m} i /= {Nat} index-right {A} {l} j => \lam p => NatSemiring.<-irreflexive$ (fin_< i) <∘l rewrite (inv index-left-nat *> p *> index-right-nat) (LinearlyOrderedSemiring.<=_+ <=-refl zero<=_)

\func split-index {A : \Type} {l m : Array A} (i : Fin (DArray.len {l ++ m}))
: Or (\Sigma (j : Fin l.len) (i = index-left j)) (\Sigma (j : Fin m.len) (i = index-right j)) \elim l, i
| nil, i => inr (i,idp)
| a :: l, 0 => inl (0,idp)
| a :: l, suc i => \case split-index i \with {
| inl r => inl (suc r.1, \lam i => suc (r.2 i))
| inr r => inr (r.1, \lam i => suc (r.2 i))
}

\func index-big {A : \Type} {ls : Array (Array A)} (i : Fin ls.len) (j : Fin (DArray.len {ls i})) : Fin (DArray.len {Big (++) nil ls}) \elim ls, i
| l :: ls, 0 => index-left j
| l :: ls, suc i => index-right (index-big i j)

\func Big++-index {A : \Type} {ls : Array (Array A)} {i : Fin ls.len} {j : Fin (DArray.len {ls i})} : Big (++) nil ls (index-big i j) = ls i j \elim ls, i
| ls :: l, 0 => ++_index-left j
| ls :: l, suc i => ++_index-right *> Big++-index
}

\func ++_++' {A : \Type} {l : Array A} {n : Nat} {l' : Array A n} : l ++ l' = l ++' l' \elim l
| nil => idp
| a :: l => pmap (a ::) ++_++'

\func map_++ {A B : \Type} (f : A -> B) {l l' : Array A} : map f (l ++ l') = map f l ++ map f l' \elim l
| nil => idp
| :: a l => pmap (f a ::) (map_++ f)

\func ++_nil {A : \Type} {l : Array A} : l ++ nil = l \elim l
| nil => idp
| :: a l => pmap (a ::) ++_nil

\lemma len_++ {A : \Type} {l l' : Array A} : DArray.len {l ++ l'} = l.len Nat.+ l'.len \elim l
| nil => idp
| a :: l => pmap suc len_++

\func unhead {A : \Type} {a a' : A} {l l' : Array A} (p : a :: l = a' :: l') : a = a'
\where
\func headDef {A : \Type} (def : A) (l : Array A) : A \elim l
| nil => def
| a :: _ => a

\func untail {A : \Type} {a a' : A} {l l' : Array A} (p : a :: l = a' :: l') : l = l'
=> pmap (tailDef l) p
\where
\func tailDef {A : \Type} (def : Array A) (l : Array A) : Array A \elim l
| nil => def
| _ :: l => l

\func ++-cancel-left {A : \Type} {l l1 l2 : Array A} (p : l ++ l1 = l ++ l2) : l1 = l2 \elim l
| nil => p
| :: a l => ++-cancel-left (untail p)

\func ++-cancel-right {A : \Type} {l l1 l2 : Array A} (p : l1 ++ l = l2 ++ l) : l1 = l2 \elim l1, l2
| nil, nil => idp
| nil, :: a l2 => absurd (contr p)
| :: a l1, nil => absurd (contr (inv p))
| :: a1 l1, :: a2 l2 => path (\lam i => unhead p i :: ++-cancel-right (untail p) i)
\where
\lemma contr {A : \Type} {l l' : Array A} {a : A} (p : l = a :: l' ++ l) : Empty
=> \case NatSemiring.cancel-right {0} {suc l'.len} l.len (pmap (DArray.len {__}) p *> pmap suc len_++)

\func ++-assoc {A : \Type} {xs ys zs : Array A} : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) \elim xs
| nil => idp
| :: x xs => pmap (x ::) ++-assoc

\func replicate_+ {A : \Type} {n m : Nat} {a : A} : replicate (n Nat.+ m) a = replicate n a ++ replicate m a \elim n
| 0 => idp
| suc n => pmap (a ::) replicate_+

\func Index {A : \Type} (x : A) (l : Array A) => \Sigma (i : Fin l.len) (l i = x)

\func index-left {A : \Type} {x : A} {l l' : Array A} (i : Index x l) : Index x (l ++ l') \elim l, i
| nil, ((), _)
| :: y l, (0, e) => (0, e)
| :: y l, (suc i, e) => \have (j,p) => index-left (i, e) \in (suc j, p)

\func index-right {A : \Type} {x : A} {l l' : Array A} (i : Index x l') : Index x (l ++ l') \elim l
| nil => i
| :: y l => \have (j,p) => index-right i \in (suc j, p)

\func filter {A : \Type} (p : A -> Bool) (l : Array A) : Array A \elim l
| nil => nil
| :: a l => if (p a) (a :: filter p l) (filter p l)

\lemma filter-sat {A : \Type} (p : A -> Bool) (l : Array A) (i : Fin (DArray.len {filter p l})) : p (filter p l i) = true \elim l
| :: a l => cases (p a arg addPath, i) \with {
| false, _, i => filter-sat p l i
| true, q, 0 => q
| true, q, suc i => filter-sat p l i
}

\func filter_true {A : \Type} {p : A -> Bool} {l : Array A} (c : \Pi (j : Fin l.len) -> p (l j) = true) : filter p l = l \elim l
| nil => idp
| a :: l => rewrite (c 0) $pmap (a ::)$ filter_true \lam j => c (suc j)

\func filter_false {A : \Type} {p : A -> Bool} {l : Array A} (c : \Pi (j : Fin l.len) -> p (l j) = false) : filter p l = nil \elim l
| nil => idp
| a :: l => rewrite (c 0) $filter_false \lam j => c (suc j) \func filter-index {A : \Type} (p : A -> Bool) (l : Array A) (i : Fin l.len) (px : p (l i) = true) : Index (l i) (filter p l) \elim l, i | nil, () | :: a l, 0 => rewrite px (0, idp) | :: a l, suc i => mcases {if} \with { | true => \have (j,q) => filter-index p l i px \in (suc j, q) | false => filter-index p l i px } \func Big {A B : \Type} (op : A -> B -> B) (b : B) (l : Array A) : B \elim l | nil => b | :: a l => op a (Big op b l) \func Big++_map {A B : \Type} (f : A -> B) {ls : Array (Array A)} : Big (++) nil (map (map f) ls) = map f (Big (++) nil ls) \elim ls | nil => idp | l :: ls => pmap (_ ++) (Big++_map f) *> inv (map_++ f) \func Big++-split {A : \Type} {l : Array A} : l = Big (++) nil (map (:: nil) l) \elim l | nil => idp | a :: l => pmap (a ::) Big++-split \func filterMap {A B : \Type} (f : A -> Maybe B) (l : Array A) : Array B \elim l | nil => nil | :: a l => \case f a \with { | nothing => filterMap f l | just b => b :: filterMap f l } \func filterMap-index {A B : \Type} (f : A -> Maybe B) (l : Array A) {b : B} {j : Fin l.len} (p : f (l j) = just b) : Index b (filterMap f l) \elim l, j | :: a l, 0 => rewrite p (0,idp) | :: a l, suc j => mcases \with { | nothing => filterMap-index f l p | just _ => \have (i,q) => filterMap-index f l p \in (suc i, q) } \func indexed (l : DArray) : DArray (\lam j => \Sigma (Fin l.len) (l.A j)) \cowith | at j => (j, l j) \func indexed' (l : DArray) : Array (\Sigma (j : Fin l.len) (l.A j)) \cowith | len => l.len | at j => (j, l j) \func replicate {A : \Type} (n : Nat) (a : A) => \new Array A n (\lam _ => a) \func keep {A : \Type} {P : A -> \Prop} (D : \Pi (a : A) -> Dec (P a)) (l : Array A) : Array A \elim l | nil => nil | a :: l => \case D a \with { | yes _ => a :: keep D l | no _ => keep D l } \where { \lemma satisfies {A : \Type} {P : A -> \Prop} (D : \Pi (a : A) -> Dec (P a)) {l : Array A} {i : Fin (DArray.len {keep D l})} : P (keep D l i) \elim l | a :: l => cases (D a, i) \with { | yes e, 0 => e | yes e, suc i => satisfies D | no n, i => satisfies D } \func element {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} {j : Fin l.len} (p : P (l j)) : Index (l j) (keep D l) => rewrite keep=remove (remove.element$ later \lam q => q p)

\func preimage {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} (i : Fin (DArray.len {keep D l})) : \Sigma (j : Fin l.len) (keep D l i = l j) \elim l
| nil => (i,idp)
| a :: l => cases (D a, i) \with {
| yes e, 0 => (0,idp)
| yes e, suc i => \let t => preimage i \in (suc t.1, t.2)
| no q, i => \let t => preimage i \in (suc t.1, t.2)
}

\lemma no-repeats {A : \Type} {l : Array A} (p : \Pi {i j : Fin l.len} -> l i = l j -> i = j) {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {i j : Fin (DArray.len {keep D l})} (q : keep D l i = keep D l j) : i = j \elim l
| a :: l => cases (D a, i, j, q) \with {
| no _, i, j, q => no-repeats (\lam {i'} {j'} s => pmap (fpred i') $p {suc i'} {suc j'} s) q | yes _, 0, 0, q => idp | yes s, 0, suc j, q => \let t => preimage j \in \case p {0} {suc t.1} (q *> t.2) | yes _, suc i, 0, q => \let t => preimage i \in \case p {suc t.1} {0} (inv t.2 *> q) | yes s, suc i, suc j, q => pmap fsuc (no-repeats (\lam {i'} {j'} s => pmap (fpred i')$ p {suc i'} {suc j'} s) q)
}
}

\func keep_++ {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l l' : Array A} : keep D (l ++ l') = keep D l ++ keep D l' \elim l
| nil => idp
| a :: l => mcases \with {
| yes p => pmap (a ::) keep_++
| no n => keep_++
}

\func keep-all {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} (p : \Pi (j : Fin l.len) -> P (l j)) : keep D l = l \elim l
| nil => idp
| a :: l => rewrite (dec_yes_reduce (p 0)) $pmap (a ::)$ keep-all \lam j => p (suc j)

\func keep-none {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} (p : \Pi (j : Fin l.len) -> Not (P (l j))) : keep D l = nil \elim l
| nil => idp
| a :: l => rewrite (dec_no_reduce (p 0)) $keep-none (\lam j => p (suc j)) \func keep-unique {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} {j : Fin l.len} (Pj : P (l j)) (nPj : \Pi (i : Fin l.len) -> P (l i) -> i = j) : keep D l = l j :: nil \elim l, j | a :: l, 0 => rewrite (dec_yes_reduce Pj)$ pmap (a ::) {_} {nil} $keep-none \lam i Pi => \case nPj (suc i) Pi | a :: l, suc j => rewrite (dec_no_reduce \lam Pa => \case nPj 0 Pa)$ keep-unique Pj \lam i Pi => unfsuc $nPj (suc i) Pi \func remove {A : \Type} {P : A -> \Prop} (D : \Pi (a : A) -> Dec (P a)) (l : Array A) : Array A \elim l | nil => nil | a :: l => \case D a \with { | yes _ => remove D l | no _ => a :: remove D l } \where { \lemma no-element {A : \Type} {P : A -> \Prop} (D : \Pi (a : A) -> Dec (P a)) {l : Array A} {i : Fin (DArray.len {remove D l})} (p : P (remove D l i)) : Empty \elim l | nil => \case i | a :: l => cases (D a, i, p) \with { | yes e, i, p => no-element D p | no q, 0, p => q p | no q, suc i, p => no-element D p } \func element {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} {j : Fin l.len} (p : Not (P (l j))) : Index (l j) (remove D l) \elim l | a :: l => \case \elim j, \elim p \with { | 0, p => mcases \with { | yes e => absurd (p e) | no q => (0,idp) } | suc j, p => mcases \with { | yes e => element p | no q => \let t => element p \in (suc t.1, t.2) } } \func preimage {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} (i : Fin (DArray.len {remove D l})) : \Sigma (j : Fin l.len) (remove D l i = l j) \elim l | nil => (i,idp) | a :: l => cases (D a, i) \with { | yes e, i => \let t => preimage i \in (suc t.1, t.2) | no q, 0 => (0,idp) | no q, suc i => \let t => preimage i \in (suc t.1, t.2) } \lemma no-repeats {A : \Type} {l : Array A} (p : \Pi {i j : Fin l.len} -> l i = l j -> i = j) {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {i j : Fin (DArray.len {remove D l})} (q : remove D l i = remove D l j) : i = j \elim l | nil => \case i | a :: l => cases (D a, i, j, q) \with { | yes _, i, j, q => no-repeats (\lam {i'} {j'} s => pmap (fpred i')$ p {suc i'} {suc j'} s) q
| no _, 0, 0, q => idp
| no s, 0, suc j, q => \let t => preimage j \in \case p {0} {suc t.1} (q *> t.2)
| no _, suc i, 0, q => \let t => preimage i \in \case p {suc t.1} {0} (inv t.2 *> q)
| no s, suc i, suc j, q => pmap fsuc (no-repeats (\lam {i'} {j'} s => pmap (fpred i') $p {suc i'} {suc j'} s) q) } \func equals {A : \Type} {P Q : A -> \Prop} (pq : \Pi {a : A} -> P a -> Q a) (qp : \Pi {a : A} -> Q a -> P a) {DP : \Pi (a : A) -> Dec (P a)} {DQ : \Pi (a : A) -> Dec (Q a)} {l : Array A} : remove DP l = remove DQ l \elim l | nil => idp | a :: l => cases (DP a) \with { | yes e => rewrite (dec_yes_reduce (pq e)) (equals pq qp) | no p => rewrite (dec_no_reduce \lam q => p (qp q))$ pmap (a ::) (equals pq qp)
}
}

\func remove-none {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} (p : \Pi (j : Fin l.len) -> Not (P (l j))) : remove D l = l \elim l
| nil => idp
| a :: l => rewrite (dec_no_reduce (p 0)) $pmap (a ::)$ remove-none \lam j => p (suc j)

\func remove_map {A B : \Type} (f : A -> B) {P : B -> \Prop} {D : \Pi (b : B) -> Dec (P b)} {l : Array A} : remove D (map f l) = map f (remove (\lam a => D (f a)) l) \elim l
| nil => idp
| a :: l => mcases \with {
| yes p => remove_map f
| no q => pmap (f a ::) (remove_map f)
}

\func keep=remove {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} : keep D l = remove (\lam a => NotDec (D a)) l \elim l
| nil => idp
| a :: l => cases (D a) \with {
| yes e => rewrite (dec_no_reduce $later \lam p => p e)$ pmap (a ::) keep=remove
| no q => rewrite (dec_yes_reduce q) keep=remove
}

\func remove=keep {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} : remove D l = keep (\lam a => NotDec (D a)) l \elim l
| nil => idp
| a :: l => cases (D a) \with {
| yes e => rewrite (dec_no_reduce $later \lam p => p e)$ remove=keep
| no q => rewrite (dec_yes_reduce q) $pmap (a ::) remove=keep } \func remove_remove {A : \Type} {P Q : A -> \Prop} {DP : \Pi (a : A) -> Dec (P a)} {DQ : \Pi (a : A) -> Dec (Q a)} {l : Array A} : remove DP (remove DQ l) = remove (\lam a => Dec_|| (DP a) (DQ a)) l \elim l | nil => idp | a :: l => mcases \with { | yes q, yes _x => remove_remove | yes q, no p => absurd$ p (byRight q)
| no q, yes e => mcases \with {
| yes p => remove_remove
| no p => absurd $||.rec' p q e } | no q, no r => mcases \with { | yes p => absurd$ r (byLeft p)
| no n => pmap (a ::) remove_remove
}
}

\func remove-swap {A : \Type} {P Q : A -> \Prop} {DP : \Pi (a : A) -> Dec (P a)} {DQ : \Pi (a : A) -> Dec (Q a)} {l : Array A}
: remove DP (remove DQ l) = remove DQ (remove DP l)
=> remove_remove *> remove.equals (\lam {a} => ||.rec' byRight byLeft) (\lam {a} => ||.rec' byRight byLeft) *> inv remove_remove

\func keep_remove=keep {A : \Type} {P Q : A -> \Prop} {DP : \Pi (a : A) -> Dec (P a)} {DQ : \Pi (a : A) -> Dec (Q a)} (PQ : \Pi {a : A} -> P a -> Q a -> Empty) {l : Array A} : keep DP (remove DQ l) = keep DP l \elim l
| nil => idp
| a :: l => mcases \with {
| yes q, yes p => absurd (PQ p q)
| yes q, no n => keep_remove=keep PQ
| no n, yes p => rewrite (dec_yes_reduce p) $pmap (a ::) (keep_remove=keep PQ) | no n, no n1 => rewrite (dec_no_reduce n1) (keep_remove=keep PQ) } \func keep_remove-split {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} : EPerm l (keep D l ++ remove D l) \elim l | nil => eperm-nil | a :: l => mcases \with { | yes p => eperm-:: idp (keep_remove-split {_} {_} {D}) | no n => eperm-trans (eperm-:: idp (keep_remove-split {_} {_} {D})) (EPerm.eperm-sym EPerm.EPerm_++-swap) } \lemma remove<= {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} : DArray.len {remove D l} <= l.len \elim l | nil => <=-refl | a :: l => mcases \with { | yes p => remove<= <=∘ id<=suc | no n => suc<=suc remove<= } \lemma count_remove_yes {A : DecSet} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} {a : A} (Pa : P a) : count (remove D l) a = 0 \elim l | nil => idp | x :: l => mcases \with { | yes p => count_remove_yes Pa | no q => mcases \with { | yes p => absurd$ q $transport P p Pa | no _ => count_remove_yes Pa } } \lemma count_remove_no {A : DecSet} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l : Array A} {a : A} (Pa : Not (P a)) : count (remove D l) a = count l a \elim l | nil => idp | x :: l => mcases \with { | yes p, yes q => absurd$ Pa $transportInv P q p | yes p, no q => count_remove_no Pa | no p, yes q => rewrite (decideEq=_reduce q)$ pmap suc $count_remove_no Pa | no p, no q => rewrite (decideEq/=_reduce q)$ count_remove_no Pa
}

\lemma count_remove {A : DecSet} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l l' : Array A} {a : A} (p : count l a = count l' a)
: count (remove D l) a = count (remove D l') a
=> \case D a \with {
| yes Pa => count_remove_yes Pa *> inv (count_remove_yes Pa)
| no Pa => count_remove_no Pa *> p *> inv (count_remove_no Pa)
}

\func removeElem {A : DecSet} (a : A) (l : Array A) : Array A
=> remove (decideEq a) l

\func remove1 {A : DecSet} (a : A) {n : Nat} (l : Array A (suc n)) : Array A n \elim n, l
| 0, l => nil
| suc n, a' :: l => \case decideEq a a' \with {
| yes _ => l
| no _ => a' :: remove1 a l
}

\func remove1-surj {A : DecSet} (a : A) {n : Nat} (l : Array A (suc n)) (i : Fin n) : \Sigma (j : Fin (suc n)) (remove1 a l i = l j) \elim n, l
| 0, b :: l => \case i
| suc n, b :: l => mcases \with {
| yes p => (suc i, idp)
| no q => \case \elim i \with {
| 0 => (0, idp)
| suc i => \have t => remove1-surj a l i \in (suc t.1, t.2)
}
}

\lemma remove1/= {A : DecSet} {a : A} {n : Nat} {l : Array A (suc n)} (inj : isInj l) {j : Fin n} : remove1 a l j /= a \elim n, l
| 0, b :: l => \case j
| suc n, b :: l => mcases \with {
| yes p => \lam q => \case inj {suc j} {0} (q *> p)
| no q => \case \elim j \with {
| 0 => \lam p => q (inv p)
| suc j => remove1/= \lam {i} {j} p => pmap (fpred i) $inj {suc i} {suc j} p } } \lemma remove1-inj {A : DecSet} {a : A} {n : Nat} {l : Array A (suc n)} (inj : isInj l) {i j : Fin n} (p : remove1 a l i = remove1 a l j) : i = j \elim n, l | 0, b :: l => \case i | suc n, b :: l => cases (decideEq a b, p) \with { | yes _, p => pmap (fpred i)$ inj {suc i} {suc j} p
| no q, p => \case \elim i, \elim j, \elim p \with {
| 0, 0, p => idp
| 0, suc j, p => \have t => remove1-surj a l j \in \case inj {suc t.1} {0} $inv (p *> t.2) | suc i, 0, p => \have t => remove1-surj a l i \in \case inj {0} {suc t.1}$ inv p *> t.2
| suc i, suc j, p => pmap fsuc $remove1-inj (\lam {i} {j} p => pmap (fpred i)$ inj {suc i} {suc j} p) p
}
}

\func nub {A : DecSet} (l : Array A) : Array A \elim l
| nil => nil
| a :: l => a :: removeElem a (nub l)

\func nub-isSurj {A : DecSet} (l : Array A) (i : Fin l.len) : \Sigma (j : Fin (DArray.len {nub l})) (nub l j = l i) \elim l, i
| a :: l, 0 => (0,idp)
| a :: l, suc i =>
\case decideEq a (l i) \with {
| yes e => (0,e)
| no q =>
\have | t => nub-isSurj l i
| s => remove-isSurj a (nub l) t.1 \lam p => q $inv p *> t.2 \in (suc s.1, s.2 *> t.2) } \where { \func remove-isSurj {A : DecSet} (a : A) (l : Array A) (i : Fin l.len) (p : l i /= a) : \Sigma (j : Fin (DArray.len {removeElem a l})) (removeElem a l j = l i) \elim l | nil => \case i | a' :: l => unfold removeElem$ mcases \with {
| yes e => cases (i,p) \with {
| 0, p => absurd $p (inv e) | suc i, p => remove-isSurj a l i p } | no q => cases (i,p) \with { | 0, p => (0,idp) | suc i, p => \let t => remove-isSurj a l i p \in (suc t.1, t.2) } } } \func nub-preimage {A : DecSet} {l : Array A} (j : Fin (DArray.len {nub l})) : \Sigma (i : Fin l.len) (nub l j = l i) \elim l, j | a :: l, 0 => (0, idp) | a :: l, suc j => \have | (k,p) => remove.preimage j | (i,q) => nub-preimage k \in (suc i, p *> q) \lemma nub-isInj {A : DecSet} {l : Array A} {i j : Fin (DArray.len {nub l})} (p : nub l i = nub l j) : i = j \elim l, i, j | a :: l, 0, 0 => idp | a :: l, 0, suc j => absurd$ remove.no-element (decideEq a) p
| a :: l, suc i, 0 => absurd (remove.no-element (decideEq a) (inv p))
| a :: l, suc i, suc j => pmap fsuc $remove.no-repeats nub-isInj p \func nub-split {A : \Type} {B : DecSet} {l : Array (\Sigma A B)} : EPerm l (Big (++) nil (map (\lam b => keep (\lam s => decideEq b s.2) l) (nub (map __.2 l)))) => aux (nub (map __.2 l)) nub-isInj (later$ nub-isSurj (map __.2 l))
\where
\func aux {A : \Type} {B : DecSet} {l : Array (\Sigma A B)} (bs : Array B) (inj : isInj bs) (l<bs : \Pi (j : Fin l.len) -> \Sigma (k : Fin bs.len) (bs k = (l j).2))
: EPerm l (Big (++) nil (map (\lam b => keep (\lam s => decideEq b s.2) l) bs)) \elim bs
| nil => \case \elim l, \elim l<bs \with {
| nil, _ => eperm-nil
| s :: l, p => \case (p 0).1
}
| b :: bs => eperm-trans keep_remove-split $EPerm.eperm-++-right$
eperm-trans (aux bs (\lam p => unfsuc (inj p)) (\lam j =>
\have t => remove.preimage j
\in \case l<bs t.1 \with {
| (0, p) => absurd $remove.no-element (\lam s => decideEq b s.2) {l}$ inv (pmap __.2 t.2 *> inv p)
| (suc k, p) => (k, p *> inv (pmap __.2 t.2))
})) $EPerm.eperm-=$ pmap (Big (++) nil) $exts \lam j => keep_remove=keep \lam p q => \case inj {0} {suc j} (q *> inv p) \func nub_id {A : DecSet} {l : Array A} (inj : isInj l) : nub l = l \elim l | nil => idp | a :: l => pmap (a ::)$ remove-none (\lam j p => \case inj {0} {suc (nub-preimage j).1} $p *> (nub-preimage j).2) *> nub_id \lam p => unfsuc (inj p) \func insert {A : \Type} (a : A) (l : Array A) (j : Fin (suc l.len)) : Array A (suc l.len) \elim l, j | nil, j => a :: nil | b :: l, 0 => a :: b :: l | b :: l, suc j => b :: insert a l j \func insert_zro {A : \Type} {n : Nat} {a : A} {l : Array A n} : insert a l 0 = a :: l \elim n, l | 0, nil => idp | suc n, b :: l => idp \func insert-index {A : \Type} {a : A} {l : Array A} {j : Fin (suc l.len)} : insert a l j j = a \elim l, j | nil, 0 => idp | b :: l, 0 => idp | b :: l, suc j => insert-index \func skip {A : \Type} {n : Nat} (l : Array A (suc n)) (k : Fin (suc n)) : Array A n \elim n, l, k | n, _ :: l, 0 => l | suc n, a :: l, suc k => a :: skip l k \where { \func newIndex {n : Nat} {j i : Fin (suc n)} (p : i /= j) : Fin n \elim n, j, i | _, 0, 0 => absurd (p idp) | suc n, 0, suc i => i | suc n, suc j, 0 => 0 | suc n, suc j, suc i => suc$ newIndex (\lam q => p (pmap fsuc q))

\open NatSemiring

\lemma newIndex_< {n : Nat} {i j k : Fin (suc n)} {pj : j /= i} {pk : k /= i} (q : j < k) : newIndex pj < newIndex pk \elim n, i, j, k, q
| _, 0, 0, _, _ => absurd (pj idp)
| _, 0, _, 0, _ => absurd (pk idp)
| suc n, 0, suc j, suc k, suc<suc q => q
| suc n, suc i, 0, suc k, q => zero<suc
| suc n, suc i, suc j, suc k, suc<suc q => suc<suc (newIndex_< q)
}

\func skip_++' {A : \Type} {n m : Nat} {l : Array A (suc n)} {l' : Array A m} {k : Fin (suc n)} : skip (l ++' l') (fin-inc k) = skip l k ++' l' \elim n, l, k
| 0, a :: nil, 0 => exts \lam j => skip_0
| suc n, a :: l, 0 => idp
| suc n, a :: l, suc k => cong skip_++'

\func skipExt {A : \Type} {n : Nat} {l l' : Array A (suc n)} {k : Fin (suc n)} (p : \Pi (i : Fin (suc n)) -> i /= k -> l i = l' i) : skip l k = skip l' k \elim n, l, l', k
| 0, l, l', 0 => idp
| suc n, a :: l, a' :: l', 0 => arrayExt \lam j => p (suc j) (\case __)
| suc n, a :: l, a' :: l', suc k => pmap2 (::) (p 0 (\case __)) $skipExt \lam i q => p (suc i) (fsuc/= q) \func skip_0 {A : \Type} {n : Nat} {l : Array A (suc n)} {j : Fin n} : skip l 0 j = l (suc j) \elim n, l | 0, a :: l => idp | suc n, a :: l => idp \func skip_map {A B : \Type} (f : A -> B) {n : Nat} {l : Array A (suc n)} {k : Fin (suc n)} : map f (skip l k) = skip (map f l) k \elim n, l, k | 0, a :: l, 0 => idp | suc n, a :: l, 0 => idp | suc n, a :: l, suc k => path (\lam i => f a :: skip_map f i) \func replace {A : \Type} (l : Array A) (i : Fin l.len) (a : A) : Array A l.len \elim l, i | b :: l, 0 => a :: l | b :: l, suc i => b :: replace l i a \func replace-index {A : \Type} {l : Array A} {i : Fin l.len} {a : A} : replace l i a i = a \elim l, i | b :: l, 0 => idp | b :: l, suc i => replace-index \func replace-notIndex {A : \Type} {l : Array A} {i j : Fin l.len} (i/=j : i /= {Nat} j) {a : A} : replace l i a j = l j \elim l, i, j | b :: l, 0, 0 => absurd (i/=j idp) | b :: l, 0, suc j => idp | b :: l, suc i, 0 => idp | b :: l, suc i, suc j => replace-notIndex \lam p => i/=j (pmap suc p) \func replace_insert {A : \Type} {l : Array A} {i : Fin (suc l.len)} {a b : A} : replace (insert a l i) i b = insert b l i \elim l, i | nil, 0 => idp | c :: l, 0 => idp | c :: l, suc i => cong replace_insert \func skip_replace_= {A : \Type} {n : Nat} {l : Array A (suc n)} {i : Fin (suc n)} {a : A} : skip (replace l i a) i = skip l i \elim n, l, i | 0, b :: l, 0 => idp | suc n, b :: l, 0 => idp | suc n, b :: l, suc i => path (\lam i => b :: skip_replace_= i) \func skip_replace_/= {A : \Type} {n : Nat} {l : Array A (suc n)} {j i : Fin (suc n)} {a : A} (p : j /= i) : skip (replace l j a) i = replace (skip l i) (skip.newIndex p) a \elim n, l, j, i | _, _, 0, 0 => absurd (p idp) | suc n, b :: l, 0, suc 0 => idp | suc n, b :: l, 0, suc (suc i) => idp | suc n, b :: l, suc j, 0 => idp | suc n, b :: l, suc j, suc i => cong (skip_replace_/= _) \func skip-index {A : \Type} {n : Nat} {l : Array A (suc n)} {i j : Fin (suc n)} {p : j /= i} : skip l i (skip.newIndex p) = l j \elim n, l, i, j | _, _, 0, 0 => absurd (p idp) | suc n, a :: l, 0, suc j => idp | suc n, a :: l, suc i, 0 => idp | suc n, a :: l, suc i, suc j => skip-index \func skip_replicate {A : \Type} {n : Nat} (a : A) {k : Fin (suc n)} : skip (replicate (suc n) a) k = replicate n a \elim n, k | 0, 0 => idp | suc n, 0 => idp | suc n, suc k => path (\lam i => a :: skip_replicate a i) \func map_replace {A B : \Type} (f : A -> B) {l : Array A} {i : Fin l.len} {a : A} : map f (replace l i a) = replace (map f l) i (f a) \elim l, i | b :: l, 0 => idp | b :: l, suc i => path (\lam i => f b :: map_replace f i) \func insert_skip {A : \Type} {n : Nat} {l : Array A (suc n)} {k : Fin (suc n)} {a : A} : insert a (skip l k) k = replace l k a \elim n, l, k | 0, b :: nil, 0 => idp | suc n, b :: l, 0 => idp | suc n, b :: l, suc k => cong insert_skip \func skip_insert_= {A : \Type} {n : Nat} {a : A} {l : Array A n} {j : Fin (suc n)} : skip (insert a l j) j = l \elim n, l, j | 0, nil, 0 => idp | suc n, b :: l, 0 => idp | suc n, b :: l, suc j => cong skip_insert_= \func map_insert {A B : \Type} (f : A -> B) {a : A} {l : Array A} {j : Fin (suc l.len)} : map f (insert a l j) = insert (f a) (map f l) j \elim l, j | nil, 0 => idp | b :: l, 0 => idp | b :: l, suc j => path (\lam i => f b :: map_insert f i) \func count {A : DecSet} (l : Array A) (a : A) : Nat \elim l | nil => 0 | x :: l => \case decideEq a x \with { | yes _ => suc (count l a) | no _ => count l a } \lemma count<= {A : DecSet} {l : Array A} {a : A} : count l a <= l.len \elim l | nil => <=-refl | x :: l => mcases \with { | yes p => suc<=suc count<= | no q => count<= <=∘ id<=suc } \lemma count_++ {A : DecSet} {l l' : Array A} {a : A} : count (l ++ l') a = count l a + count l' a \elim l | nil => idp | x :: l => mcases \with { | yes p => pmap suc count_++ | no q => count_++ } \lemma count_Big++ {A : DecSet} {ls : Array (Array A)} {a : A} : count (Big (++) nil ls) a = NatSemiring.BigSum (map (count __ a) ls) \elim ls | nil => idp | l :: ls => count_++ *> pmap (_ +) count_Big++ \lemma count-all {A : DecSet} {l : Array A} {a : A} (p : \Pi (j : Fin l.len) -> l j = a) : count l a = l.len \elim l | nil => idp | x :: l => rewrite (decideEq=_reduce$ inv $p 0)$ pmap suc $count-all \lam j => p (suc j) \lemma count-none {A : DecSet} {l : Array A} {a : A} (p : \Pi (j : Fin l.len) -> l j /= a) : count l a = 0 \elim l | nil => idp | x :: l => rewrite (decideEq/=_reduce$ /=-sym $p 0)$ count-none \lam j => p (suc j)

\lemma keep_count {A : DecSet} {l : Array A} {a : A} : keep (decideEq a) l = replicate (count l a) a \elim l
| nil => idp
| x :: l => mcases \with {
| yes p => rewriteI p $pmap (a ::) keep_count | no q => keep_count } \data Perm {A : \Type} {n : Nat} (l1 l2 : Array A n) \elim n, l1, l2 | 0, nil, nil => perm-nil | suc n, :: x l1, :: y l2 => perm-:: (x = y) (Perm l1 l2) | suc (suc n), :: x (:: x' l1), :: y (:: y' l2) => perm-swap (x = y') (x' = y) (l1 = l2) | n, l1, l2 => perm-trans {l : Array A n} (Perm l1 l) (Perm l l2) \where { \func perm-refl {A : \Type} {n : Nat} {l : Array A n} : Perm l l \elim n, l | 0, nil => perm-nil | suc n, a :: l => perm-:: idp perm-refl \func perm-sym {A : \Type} {n : Nat} {l l' : Array A n} (p : Perm l l') : Perm l' l \elim n, l, l', p | 0, nil, nil, perm-nil => perm-nil | suc n, x :: l, y :: l', perm-:: p q => perm-:: (inv p) (perm-sym q) | suc (suc n), x :: (x' :: l), y :: (y' :: l'), perm-swap p1 p2 q => perm-swap (inv p2) (inv p1) (inv q) | n, l, l', perm-trans p1 p2 => perm-trans (perm-sym p2) (perm-sym p1) \func inversions {A : \Type} {n : Nat} {l1 l2 : Array A n} (p : Perm l1 l2) : Nat \elim n, l1, l2, p | 0, nil, nil, perm-nil => 0 | suc n, x :: l3, y :: l4, perm-:: _ p => inversions p | suc (suc n), x :: (x' :: l3), y :: (y' :: l4), perm-swap p p1 p2 => 1 | n, l3, l4, perm-trans p1 p2 => inversions p1 Nat.+ inversions p2 \lemma inversions_perm-:: {A : \Type} {n : Nat} {x y : A} {l1 l2 : Array A n} {q : x = y} {p : Perm l1 l2} : inversions (perm-:: q p) = inversions p \elim n, l1, l2 | 0, nil, nil => idp | suc n, a1 :: l1, a2 :: l2 => idp \lemma inversions_perm-trans {A : \Type} {n : Nat} {l1 l l2 : Array A n} {p1 : Perm l1 l} {p2 : Perm l l2} : inversions (perm-trans p1 p2) = inversions p1 Nat.+ inversions p2 \elim n, l1, l2 | 0, nil, nil => idp | 1, a1 :: l1, a2 :: l2 => idp | suc (suc n), a1 :: l1, a2 :: l2 => idp \lemma inversions_perm-refl {A : \Type} {n : Nat} {l : Array A n} : inversions (perm-refl {A} {n} {l}) = 0 \elim n, l | 0, nil => idp | suc n, a :: l => inversions_perm-:: *> inversions_perm-refl \func sign {R : Ring} {A : \Type} {n : Nat} {l1 l2 : Array A n} (p : Perm l1 l2) : R => R.pow -1 (inversions p) \func perm-map {A B : \Type} (f : A -> B) {n : Nat} {l1 l2 : Array A n} (p : Perm l1 l2) : Perm (map f l1) (map f l2) \elim n, l1, l2, p | 0, nil, nil, perm-nil => perm-nil | suc n, a1 :: l1, a2 :: l2, perm-:: p q => perm-:: (pmap f p) (perm-map f q) | suc (suc n), a1 :: (a1' :: l), a2 :: (a2' :: _), perm-swap p1 p2 idp => perm-swap (pmap f p1) (pmap f p2) idp | n, l1, l2, perm-trans p1 p2 => perm-trans (perm-map f p1) (perm-map f p2) \where \func conv {A B : \Set} (f : A -> B) (inj : isInj f) {n : Nat} {l1 l2 : Array A n} (p : Perm (map f l1) (map f l2)) : Perm l1 l2 => \have (e,f) => perm_equiv {_} {_} {map f l1} p \in transport (Perm l1) (exts \lam j => inj$ inv $f j) (equiv_perm e) \func perm-remove {A : DecSet} {n : Nat} (l : Array A (suc n)) (j : Fin (suc n)) : Perm l (l j :: remove1 (l j) l) \elim n, l, j | 0, a :: nil, 0 => perm-refl | suc n, l, 0 => rewrite (decideEq=_reduce idp) perm-refl | suc n, a :: l, suc j => mcases \with { | yes p => rewrite p perm-refl | no q => perm-trans (perm-:: idp (perm-remove l j)) (perm-swap idp idp idp) } \func perm-fin {n : Nat} (l : Array (Fin n) n) (l-inj : isInj l) : Perm l (\lam j => j) \elim n | 0 => perm-nil | 1 => perm-:: (cases (l 0) idp) perm-nil | suc (suc n) => aux2 {suc n} l l-inj 0 \where { \func aux {n : Nat} (l : Array (Fin (suc n)) n) (q : \Pi (j : Fin n) -> l j /= 0) (d : Fin n) (r : Perm (map (fpred d) l) (\lam j => j)) : Perm l (\lam j => suc j) => transport (Perm __ _) (arrayExt \lam j => fsuc_fpred (q j))$ perm-map fsuc {n} r

\func aux2 {n : Nat} (l : Array (Fin (suc n)) (suc n)) (l-inj : isInj l) (d : Fin n) : Perm l (\lam j => j)
=> \have | (j,lj=0) => isDFin.isSplit {Fin (suc n)} (isDFin.fromPigeonhole (FinFin _)) l l-inj 0
| remove/=0 i : remove1 (l j) l i /= 0 => rewrite lj=0 (remove1/= l-inj)
\in perm-trans (perm-remove l j) $perm-:: lj=0$ aux (remove1 (l j) l) remove/=0 d $perm-fin (map (fpred d) (remove1 (l j) l)) \lam {i} {j} p => remove1-inj l-inj$ inv (fsuc_fpred (remove/=0 i)) *> pmap fsuc p *> fsuc_fpred (remove/=0 j)
}

\func equiv_perm {A : \Type} {n : Nat} {l : Array A n} (e : Equiv {Fin n} {Fin n}) : Perm l (\lam j => l (e j))
=> perm-map l $perm-sym$ perm-fin (\lam j => e j) e.isInj

\func perm_equiv {A : \Type} {n : Nat} {l l' : Array A n} (p : Perm l l') : \Sigma (e : Equiv {Fin n} {Fin n}) (\Pi (j : Fin n) -> l' j = l (e j))
=> EPerm.eperm_equiv (EPerm.Perm_EPerm p)
\where {
\func conv {A : \Type} {n : Nat} {l l' : Array A n} (s : \Sigma (e : Equiv {Fin n} {Fin n}) (\Pi (j : Fin n) -> l' j = l (e j))) : Perm l l'
=> transportInv (Perm l) (exts s.2) (equiv_perm s.1)
}

\func perm_list {A : \Type} {n : Nat} {l l' : Array A n} (p : Perm l l') : Sort.Perm (toList l) (toList l') \elim n, l, l', p
| 0, nil, nil, perm-nil => Sort.perm-nil
| suc n, x :: l, y :: l', perm-:: p q => Sort.perm-:: p (perm_list q)
| suc (suc n), x :: (x' :: l), y :: (y' :: l'), perm-swap p1 p2 q => Sort.perm-swap p1 p2 (pmap toList q)
| n, l, l', perm-trans p1 p2 => Sort.perm-trans (perm_list p1) (perm_list p2)
}

\data EPerm {A : \Type} (l1 l2 : Array A) \elim l1, l2
| nil, nil => eperm-nil
| :: x l1, :: y l2 => eperm-:: (x = y) (EPerm l1 l2)
| :: x (:: x' l1), :: y (:: y' l2) => eperm-swap (x = y') (x' = y) (l1 = l2)
| l1, l2 => eperm-trans {l : Array A} (EPerm l1 l) (EPerm l l2)
\where {
\func eperm-refl {A : \Type} {l : Array A} : EPerm l l \elim l
| nil => eperm-nil
| a :: l => eperm-:: idp eperm-refl

\func eperm-= {A : \Type} {l l' : Array A} (p : l = l') : EPerm l l' \elim p
| idp => eperm-refl

\func eperm-sym {A : \Type} {l l' : Array A} (e : EPerm l l') : EPerm l' l \elim l, l', e
| nil, nil, eperm-nil => eperm-nil
| x :: l1, y :: l2, eperm-:: p e => eperm-:: (inv p) (eperm-sym e)
| x :: (x' :: l1), y :: (y' :: l2), eperm-swap p1 p2 q => eperm-swap (inv p2) (inv p1) (inv q)
| l, l', eperm-trans e1 e2 => eperm-trans (eperm-sym e2) (eperm-sym e1)

\func eperm-++-comm {A : \Type} {l l' : Array A} : EPerm (l ++ l') (l' ++ l) \elim l, l'
| nil, nil => eperm-nil
| nil, a :: l => rewrite ++_nil eperm-refl
| a :: l, nil => rewrite ++_nil eperm-refl
| a :: l, a' :: l' => mkcon eperm-trans {a :: a' :: l' ++ l} (eperm-:: idp eperm-++-comm) $mkcon eperm-trans {a' :: a :: l ++ l'} (mkcon eperm-trans {a' :: a :: l' ++ l} (eperm-swap idp idp idp)$ eperm-:: idp $eperm-:: idp$ eperm-sym $eperm-++-comm) (eperm-:: idp eperm-++-comm) \func eperm-++-left {A : \Type} {l1 l2 l : Array A} (e : EPerm l1 l2) : EPerm (l1 ++ l) (l2 ++ l) \elim l1, l2, e | nil, nil, eperm-nil => eperm-refl | x :: l1, y :: l2, eperm-:: p e => eperm-:: p (eperm-++-left e) | x :: (x' :: l1), y :: (y' :: l2), eperm-swap p1 p2 q => eperm-swap p1 p2 (pmap (++ l) q) | l1, l2, eperm-trans e1 e2 => eperm-trans (eperm-++-left e1) (eperm-++-left e2) \func eperm-++-right {A : \Type} {l l1 l2 : Array A} (e : EPerm l1 l2) : EPerm (l ++ l1) (l ++ l2) => eperm-++-comm eperm-trans eperm-++-left e eperm-trans eperm-++-comm \func eperm-++ {A : \Type} {l1 l1' l2 l2' : Array A} (e1 : EPerm l1 l1') (e2 : EPerm l2 l2') : EPerm (l1 ++ l2) (l1' ++ l2') => eperm-++-left e1 eperm-trans eperm-++-right e2 \func EPerm_map {A B : \Type} (f : A -> B) {l l' : Array A} (e : EPerm l l') : EPerm (map f l) (map f l') \elim l, l', e | nil, nil, eperm-nil => eperm-nil | x :: l, y :: l', eperm-:: p e => eperm-:: (pmap f p) (EPerm_map f e) | x :: (x' :: l), y :: (y' :: l'), eperm-swap idp idp q => eperm-swap idp idp$ pmap (map f) q
| l, l', eperm-trans e1 e2 => eperm-trans (EPerm_map f e1) (EPerm_map f e2)
\where
\func conv {A B : \Set} (f : A -> B) (inj : isInj f) {l l' : Array A} (e : EPerm (map f l) (map f l')) : EPerm l l'
=> aux f inj (EPerm_len e) e
\where
\private \func aux {A B : \Set} (f : A -> B) (inj : isInj f) {n m : Nat} (p : n = m) {l : Array A n} {l' : Array A m} (e : EPerm (map f l) (map f l')) : EPerm l l' \elim p
| idp => Perm_EPerm $Perm.perm-map.conv f inj$ EPerm_Perm {B} {_} {map f l} e

\func EPerm_keep {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l l' : Array A} (p : EPerm l l') : EPerm (keep D l) (keep D l') \elim l, l', p
| nil, nil, eperm-nil => eperm-nil
| x :: l, _ :: l', eperm-:: idp q => mcases \with {
| yes _ => eperm-:: idp (EPerm_keep q)
| no _ => EPerm_keep q
}
| x :: (x' :: l), _ :: (_ :: l'), eperm-swap idp idp r => rewrite r $mcases \with { | yes p, yes q => rewrite (dec_yes_reduce q, dec_yes_reduce p) (eperm-swap idp idp idp) | yes p, no q => rewrite (dec_yes_reduce p, dec_no_reduce q) eperm-refl | no p, yes q => rewrite (dec_no_reduce p, dec_yes_reduce q) eperm-refl | no p, no q => rewrite (dec_no_reduce p, dec_no_reduce q) eperm-refl } | l, l', eperm-trans p1 p2 => eperm-trans (EPerm_keep p1) (EPerm_keep p2) \func EPerm_remove {A : \Type} {P : A -> \Prop} {D : \Pi (a : A) -> Dec (P a)} {l l' : Array A} (p : EPerm l l') : EPerm (remove D l) (remove D l') \elim l, l', p | nil, nil, eperm-nil => eperm-nil | x :: l, y :: l', eperm-:: idp q => mcases \with { | yes p => EPerm_remove q | no n => eperm-:: idp (EPerm_remove q) } | x :: (x' :: l), _ :: (_ :: l'), eperm-swap idp idp r => rewrite r$ mcases \with {
| yes p, yes q => rewrite (dec_yes_reduce p, dec_yes_reduce q) eperm-refl
| yes p, no q => rewrite (dec_yes_reduce p, dec_no_reduce q) eperm-refl
| no p, yes q => rewrite (dec_no_reduce p, dec_yes_reduce q) eperm-refl
| no p, no q => rewrite (dec_no_reduce p, dec_no_reduce q) (eperm-swap idp idp idp)
}
| l, l', eperm-trans p1 p2 => eperm-trans (EPerm_remove p1) (EPerm_remove p2)

\func EPerm_nub {A : DecSet} {l l' : Array A} (p : EPerm l l') : EPerm (nub l) (nub l') \elim l, l', p
| nil, nil, eperm-nil => eperm-nil
| x :: l, _ :: l', eperm-:: idp q => eperm-:: idp $EPerm_remove (EPerm_nub q) | x :: (x' :: l), _ :: (_ :: l'), eperm-swap idp idp r => rewrite r$ mcases contradiction \with {
| yes p, yes _ => eperm-:: p (eperm-= remove-swap)
| no q, no _ => eperm-swap idp idp remove-swap
}
| l, l', eperm-trans p1 p2 => eperm-trans (EPerm_nub p1) (EPerm_nub p2)

\func eperm-remove {A : DecSet} {l : Array A} (inj : isInj l) (j : Fin l.len) : EPerm l (l j :: removeElem (l j) l) \elim l, j
| a :: l, 0 => eperm-= $pmap (a ::)$ later $rewrite (decideEq=_reduce idp)$ inv $remove-none \lam j p => \case inj {0} {suc j} p | a :: l, suc j => unfold removeElem$ mcases \with {
| yes p => \case inj {suc j} {0} p
| no q => mkcon eperm-trans {a :: l j :: removeElem (l j) l} (eperm-:: idp $eperm-remove (\lam p => unfsuc$ inj p) j) (eperm-swap idp idp idp)
}

\func EPerm_filter {A : \Type} (f : A -> Bool) {l l' : Array A} (e : EPerm l l') : EPerm (filter f l) (filter f l') \elim l, l', e
| nil, nil, eperm-nil => eperm-nil
| x :: l, _ :: l', eperm-:: idp e => cases (f x) \with {
| false => EPerm_filter f e
| true => eperm-:: idp (EPerm_filter f e)
}
| x :: (x' :: l), _ :: (_ :: l'), eperm-swap idp idp r => rewrite r $cases (f x, f x') eperm-refl \with { | true, true => eperm-swap idp idp idp } | l, l', eperm-trans e1 e2 => eperm-trans (EPerm_filter f e1) (EPerm_filter f e2) \func EPerm_++-swap {A : \Type} {l l' : Array A} {a : A} : EPerm (l ++ a :: l') (a :: l ++ l') \elim l | nil => eperm-refl | a' :: l => mkcon eperm-trans {a' :: a :: l ++ l'} (eperm-:: idp EPerm_++-swap) (eperm-swap idp idp idp) \func Perm_EPerm {A : \Type} {n : Nat} {l l' : Array A n} (p : Perm l l') : EPerm l l' \elim n, l, l', p | 0, nil, nil, perm-nil => eperm-nil | suc n, x :: l, y :: l', perm-:: p q => eperm-:: p (Perm_EPerm q) | suc (suc n), x :: (x' :: l), y :: (y' :: l'), perm-swap p1 p2 q => eperm-swap p1 p2 q | n, l, l', perm-trans p1 p2 => eperm-trans (Perm_EPerm p1) (Perm_EPerm p2) \func EPerm_Perm {A : \Type} {n : Nat} {l l' : Array A n} (p : EPerm l l') : Perm l l' => \have (e,f) => eperm_equiv p \in transport (Perm l) (exts \lam j => inv (f j)) (Perm.equiv_perm e) \func EPerm_Perm_transport {A : \Type} {n m : Nat} {l : Array A n} {l' : Array A m} (e : EPerm l l') (p : n = m) : Perm (transport (\lam n => Array A n) p l) l' \elim p | idp => EPerm_Perm e \func eperm_equiv {A : \Type} {l l' : Array A} (p : EPerm l l') : \Sigma (e : Equiv {Fin l'.len} {Fin l.len}) (\Pi (j : Fin l'.len) -> l' j = l (e j)) \elim l, l', p | nil, nil, eperm-nil => (idEquiv, \case __) | x :: l3, y :: l4, eperm-:: p q => \have (e,f) => eperm_equiv q \in (lift.aux e, \case \elim __ \with { | 0 => inv p | suc j => f j }) | x :: (x' :: (l : Array)), y :: (y' :: l'), eperm-swap p1 p2 q => transport (\lam (l'' : Array A) => \Sigma (e : Equiv {Fin (suc (suc l''.len))} {Fin (suc (suc l.len))}) (\Pi (j : Fin (suc (suc l''.len))) -> (y :: y' :: l'') j = (x :: x' :: l) (e j))) q (transposition1 (0 : Fin (suc l.len)), \case \elim __ \with { | 0 => rewrite transposition1.transposition1-left (inv p2) | 1 => rewrite transposition1.transposition1-right (inv p1) | suc (suc j) => rewrite (transposition1.transposition1_/= (later \case __) (later \case __)) idp }) | l, l', eperm-trans p1 p2 => \have | (e1,f1) => eperm_equiv p1 | (e2,f2) => eperm_equiv p2 \in (transEquiv e2 e1, \lam j => f2 j *> f1 (e2 j)) \where { \func conv {A : \Type} {l l' : Array A} (s : \Sigma (e : Equiv {Fin l'.len} {Fin l.len}) (\Pi (j : Fin l'.len) -> l' j = l (e j))) : EPerm l l' => transportInv (\lam n => \Pi (l' : Array A n) -> \Sigma (e : Equiv {Fin l'.len} {Fin l.len}) (\Pi (j : Fin l'.len) -> l' j = l (e j)) -> EPerm l l') (FinSet.FinCardBij s.1) (\lam l' s => Perm_EPerm {_} {l.len} {\new l} (Perm.perm_equiv.conv {_} {_} {\new l} s)) (\new l') s } \lemma EPerm_len {A : \Type} {l l' : Array A} (e : EPerm l l') : l.len = l'.len \elim l, l', e | nil, nil, eperm-nil => idp | x :: l, y :: l', eperm-:: p e => pmap suc (EPerm_len e) | x :: (x' :: l), y :: (y' :: l'), eperm-swap _ _ q => pmap (\lam x => suc (suc (DArray.len {x}))) q | l, l', eperm-trans e1 e2 => EPerm_len e1 *> EPerm_len e2 \func EPermDec {A : DecSet} {l l' : Array A} : Or (EPerm l l') (Not (EPerm l l')) => \case FinSet.searchFin-equiv {EquivFin (FinFin l'.len) (FinFin l.len)} (symQEquiv EquivFin.equiv_fin.2) (\lam e => \Pi (j : Fin l'.len) -> l' j = l (e j)) (\lam e => decide {FunDec \lam j => EqualityDecide A (l' j) (l (e j))}) \with { | inl p => inl (eperm_equiv.conv p) | inr q => inr \lam e => q (eperm_equiv e).1 (eperm_equiv e).2 } \lemma EPerm_count {A : DecSet} {l l' : Array A} (e : EPerm l l') (a : A) : count l a = count l' a \elim l, l', e | nil, nil, eperm-nil => idp | x :: l, _ :: l', eperm-:: idp e => mcases \with { | yes p => pmap suc (EPerm_count e a) | no n => EPerm_count e a } | x :: (x' :: l), _ :: (_ :: l'), eperm-swap idp idp r => rewrite r$ mcases \with {
| yes p, yes p' => rewrite (decideEq=_reduce p, decideEq=_reduce p') idp
| yes p, no p' => rewrite (decideEq=_reduce p, decideEq/=_reduce p') idp
| no p, yes p' => rewrite (decideEq/=_reduce p, decideEq=_reduce p') idp
| no p, no p' => rewrite (decideEq/=_reduce p, decideEq/=_reduce p') idp
}
| l, l', eperm-trans e1 e2 => EPerm_count e1 a *> EPerm_count e2 a

\func count_EPerm {A : DecSet} {l l' : Array A} (p : \Pi (a : A) -> count l a = count l' a) : EPerm l l'
=> aux id<suc p
\where \private \func aux {A : DecSet} {l l' : Array A} {n : Nat} (c : l.len < n) (p : \Pi (a : A) -> count l a = count l' a) : EPerm l l' \elim l, l', n
| nil, nil, _ => eperm-nil
| nil, x :: l, _ => \case rewrite (decideEq=_reduce idp) in p x
| x :: l, l', suc n =>
\let r => aux {A} {removeElem x (x :: l)} {removeElem x l'} {n} (unfold removeElem (rewrite (decideEq=_reduce idp) remove<=) <∘r NatSemiring.unsuc< c) \lam a => count_remove {_} {_} {decideEq x} {x :: l} (p a)
\in keep_remove-split {_} {_} {decideEq x} eperm-trans transport2 (\lam x y => EPerm (x ++ _) (y ++ _)) (inv \$ keep_count {_} {x :: l} *> pmap (replicate __ x) (p x)) (inv keep_count) (eperm-++-right r) eperm-trans eperm-sym (keep_remove-split {_} {_} {decideEq x})

\func EPerm-equivalence {A : \Set} : Equivalence (Array A) (\lam l l' => TruncP (EPerm l l')) \cowith
| ~-reflexive => inP EPerm.eperm-refl
| ~-symmetric (inP e) => inP (EPerm.eperm-sym e)
| ~-transitive (inP e1) (inP e2) => inP (eperm-trans e1 e2)
}

\func pairs {A B C : \Type} (f : A -> B -> C) (l : Array A) (l' :