\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.List(List, Sort, headDef, length)
\import Data.Maybe
\import Data.Or
\import Equiv
\import Function
\import Function.Meta ($)
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\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 array-unext {A : \Type} {n : Nat} {l l' : Array A n} (p : l = {Array A} l') (j : Fin n) : l j = l' j \elim p
  | idp => idp

\func tail {n : Nat} {A : Fin (suc n) -> \Type} (a : DArray A) : DArray (\lam j => A (suc j)) \elim a
  | _ :: a => a

\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  ++' {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,  => 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
  | , 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  ++ {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,  => 
      | 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,  => 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,  => 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 $ <-transitive-left (fin_< i) $ 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,  => inl (,idp)
      | a :: l, suc i => \case split-index i \with {
        | inl r => inl (suc r., \lam i => suc (r. i))
        | inr r => inr (r., \lam i => suc (r. 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,  => 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,  => ++_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'
  => pmap (headDef a) p
  \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 {} {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
  |  => 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, (, e) => (, 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,  => q
    | true, q, suc i => filter-sat p l i
  }

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

\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,  => rewrite px (, 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 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,  => rewrite p (,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 element {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,  => e
        | yes e, suc i => element D
        | no n, i => element D
      }

    \func all-elements {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 )) $ pmap (a ::) $ all-elements \lam j => p (suc j)

    \func no-elements {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 )) $ no-elements (\lam j => p (suc j))

    \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,  => (,idp)
        | yes e, suc i => \let t => preimage i \in (suc t., t.)
        | no q, i => \let t => preimage i \in (suc t., t.)
      }
  }

\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, , p => q p
        | no q, suc i, p => no-element D p
      }

    \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., t.)
        | no q,  => (,idp)
        | no q, suc i => \let t => preimage i \in (suc t., t.)
      }

    \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 _, , , q => idp
        | no s, , suc j, q => \let t => preimage j \in \case p {} {suc t.} (q *> t.)
        | no _, suc i, , q => \let t => preimage i \in \case p {suc t.} {} (inv t. *> 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 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)
  }

\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
  | , 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
  | , b :: l => \case i
  | suc n, b :: l => mcases \with {
    | yes p => (suc i, idp)
    | no q => \case \elim i \with {
      |  => (, idp)
      | suc i => \have t => remove1-surj a l i \in (suc t., t.)
    }
  }

\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
  | , b :: l => \case j
  | suc n, b :: l => mcases \with {
    | yes p => \lam q => \case inj {suc j} {} (q *> p)
    | no q => \case \elim j \with {
      |  => \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
  | , 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 {
      | , , p => idp
      | , suc j, p => \have t => remove1-surj a l j \in \case inj {suc t.} {} $ inv (p *> t.)
      | suc i, , p => \have t => remove1-surj a l i \in \case inj {} {suc t.} $ inv p *> t.
      | 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,  => (,idp)
  | a :: l, suc i =>
    \case decideEq a (l i) \with {
      | yes e => (,e)
      | no q =>
        \have | t => nub-isSurj l i
              | s => remove-isSurj a (nub l) t. $ \lam p => q $ inv p *> t.
        \in (suc s., s. *> t.)
    }
  \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 {
          | , p => absurd $ p (inv e)
          | suc i, p => remove-isSurj a l i p
        }
        | no q => cases (i,p) \with {
          | , p => (,idp)
          | suc i, p => \let t => remove-isSurj a l i p \in (suc t., t.)
        }
      }
  }

\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,  => (, 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, ,  => idp
  | a :: l, , suc j => absurd $ remove.no-element (decideEq a) p
  | a :: l, suc i,  => 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.) l) (nub (map __. l))))
  => aux (nub (map __. l)) nub-isInj (later $ nub-isSurj (map __. 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).))
      : EPerm l (Big (++) nil (map (\lam b => keep (\lam s => decideEq b s.) l) bs)) \elim bs
      | nil => \case \elim l, \elim l<bs \with {
        | nil, _ => eperm-nil
        | s :: l, p => \case (p ).
      }
      | 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. \with {
                        | (, p) => absurd $ remove.no-element (\lam s => decideEq b s.) {l} $ inv (pmap __. t. *> inv p)
                        | (suc k, p) => (k, p *> inv (pmap __. t.))
                      })) $
                    EPerm.eperm-= $ pmap (Big (++) nil) $ exts \lam j => keep_remove=keep \lam p q => \case inj {} {suc j} (q *> inv 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,  => 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  = a :: l \elim n, l
  | , 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,  => idp
  | b :: l,  => 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,  => 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
      | _, ,  => absurd (p idp)
      | suc n, , suc i => i
      | suc n, suc j,  => 
      | 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
      | _, , , _, _ => absurd (pj idp)
      | _, , _, , _ => absurd (pk idp)
      | suc n, , suc j, suc k, suc<suc q => q
      | suc n, suc i, , 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
  | , a :: nil,  => exts \lam j => skip_0
  | suc n, a :: l,  => 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
  | , l, l',  => idp
  | suc n, a :: l, a' :: l',  => arrayExt $ \lam j => p (suc j) (\case __)
  | suc n, a :: l, a' :: l', suc k => pmap2 (::) (p  (\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  j = l (suc j) \elim n, l
  | , 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
  | , a :: l,  => idp
  | suc n, a :: l,  => 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,  => 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,  => 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, ,  => absurd (i/=j idp)
  | b :: l, , suc j => idp
  | b :: l, suc i,  => 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,  => idp
  | c :: l,  => 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
  | , b :: l,  => idp
  | suc n, b :: l,  => 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
  | _, _, ,  => absurd (p idp)
  | suc n, b :: l, , suc  => idp
  | suc n, b :: l, , suc (suc i) => idp
  | suc n, b :: l, suc j,  => 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
  | _, _, ,  => absurd (p idp)
  | suc n, a :: l, , suc j => idp
  | suc n, a :: l, suc i,  => 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
  | ,  => idp
  | suc n,  => 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,  => 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
  | , b :: nil,  => idp
  | suc n, b :: l,  => 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
  | , nil,  => idp
  | suc n, b :: l,  => 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,  => idp
  | b :: l,  => idp
  | b :: l, suc j => path (\lam i => f b :: map_insert f i)

\data Perm {A : \Type} {n : Nat} (l1 l2 : Array A n) \elim n, l1, l2
  | , 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
      | , 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
      | , 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
      | , nil, nil, perm-nil => 
      | suc n, x :: l3, y :: l4, perm-:: _ p => inversions p
      | suc (suc n), x :: (x' :: l3), y :: (y' :: l4), perm-swap p p1 p2 => 
      | 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
      | , 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
      | , nil, nil => idp
      | , 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}) =  \elim n, l
      | , 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
      | , 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
      | , a :: nil,  => perm-refl
      | suc n, l,  => 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
      |  => perm-nil
      |  => perm-:: (cases (l ) idp) perm-nil
      | suc (suc n) => aux2 {suc n} l l-inj 
      \where {
        \func aux {n : Nat} (l : Array (Fin (suc n)) n) (q : \Pi (j : Fin n) -> l j /= ) (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 
                   | remove/=0 i : remove1 (l j) l i /=  => 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)

    \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
      | , 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 idp => eperm-swap idp idp idp
      | 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), _ :: (_ :: _), eperm-swap idp idp idp => 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_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 idp => 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
      | , 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 {
          |  => inv p
          | suc j => f j
        })
      | x :: (x' :: (l : Array)), y :: (y' :: _), eperm-swap p1 p2 idp => (transposition1 ( : Fin (suc l.len)), \case \elim __ \with {
          |  => rewrite transposition1.transposition1-left (inv p2)
          |  => 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))

    \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 _ _ idp => idp
      | l, l', eperm-trans e1 e2 => EPerm_len e1 *> EPerm_len e2
  }

\func pairs {A B C : \Type} (f : A -> B -> C) (l : Array A) (l' : Array B) : Array C \elim l
  | nil => nil
  | a :: l => map (f a) l' ++ pairs f l l'
  \where {
    \open EPerm

    \func pairs_nil {A B C : \Type} {f : A -> B -> C} {l : Array A} : pairs f l nil = nil \elim l
      | nil => idp
      | a :: l => pairs_nil

    \func pairs-flip {A B C : \Type} {f : A -> B -> C} {l : Array A} {l' : Array B} : EPerm (pairs f l l') (pairs (\lam b a => f a b) l' l) \elim l, l'
      | nil, nil => eperm-nil
      | nil, a :: l => pairs-flip
      | a :: l, nil => pairs-flip
      | a :: l, b :: l' => eperm-:: idp $ eperm-++-right pairs-flip `eperm-trans` transport2 EPerm ++-assoc ++-assoc (eperm-++ eperm-++-comm $ eperm-sym pairs-flip) `eperm-trans` eperm-++-right pairs-flip

    \func pairs_++-left {A B C : \Type} {f : A -> B -> C} {l1 l2 : Array A} {l : Array B} : pairs f (l1 ++ l2) l = pairs f l1 l ++ pairs f l2 l \elim l1
      | nil => idp
      | a :: l1 => pmap (_ ++) pairs_++-left *> inv ++-assoc

    \func pairs_++-right {A B C : \Type} {f : A -> B -> C} {l : Array A} {l1 l2 : Array B} : EPerm (pairs f l (l1 ++ l2)) (pairs f l l1 ++ pairs f l l2)
      => pairs-flip `eperm-trans` rewrite pairs_++-left (eperm-++ pairs-flip pairs-flip)

    \func pairs_map-left {A : \Type} {f : A -> A -> A} (p : \Pi {x y z : A} -> f (f x y) z = f x (f y z)) {a : A} {l l' : Array A}
      : pairs f (map (f a) l) l' = map (f a) (pairs f l l') \elim l
      | nil => idp
      | a' :: l => pmap2 (++) (arrayExt {_} {_} {map (f (f a a')) l'} $ \lam j => p) (pairs_map-left p) *> inv (map_++ (f a))

    \func pairs_map {A B : \Type} {f1 : A -> A -> A} {f2 : B -> B -> B} (g : A -> B)
                    (p : \Pi {a b : A} -> g (f1 a b) = f2 (g a) (g b)) {l l' : Array A}
      : map g (pairs f1 l l') = pairs f2 (map g l) (map g l') \elim l
      | nil => idp
      | a :: l => map_++ g *> pmap2 (++) (exts $ \lam j => p) (pairs_map _ p)

    \func pairs-assoc {A : \Type} {f : A -> A -> A} (p : \Pi {x y z : A} -> f (f x y) z = f x (f y z)) {l1 l2 l3 : Array A}
      : pairs f (pairs f l1 l2) l3 = pairs f l1 (pairs f l2 l3) \elim l1
      | nil => idp
      | a :: l => pairs_++-left *> pmap2 (++) (pairs_map-left p) (pairs-assoc p)

    \func pairs-index {A B C : \Type} {f : A -> B -> C} {l : Array A} {l' : Array B} (i : Fin l.len) (j : Fin l'.len)
      : \Sigma (k : Fin (DArray.len {pairs f l l'})) (pairs f l l' k = f (l i) (l' j)) \elim l, i
      | a :: l,  => (++.index-left {_} {map (f a) l'} j, ++.++_index-left {_} {map (f a) l'} j)
      | a :: l, suc i => \have t => pairs-index i j
                         \in (++.index-right t., ++.++_index-right *> t.)

    \lemma pairs-index-inj {A B C : \Type} {f : A -> B -> C} {l : Array A} {l' : Array B} {i i' : Fin l.len} {j j' : Fin l'.len} (p : (pairs-index {_} {_} {_} {f} i j). = (pairs-index i' j').) : \Sigma (i = i') (j = j') \elim l, i, i'
      | a :: l, ,  => (idp, nat_fin_= $ inv (later ++.index-left-nat) *> p *> ++.index-left-nat)
      | a :: l, , suc i' => absurd (++.index-left/=right p)
      | a :: l, suc i,  => absurd $ ++.index-left/=right (inv p)
      | a :: l, suc i, suc i' => \let t => pairs-index-inj (++.index-right-inj p)
                                 \in (pmap fsuc t., t.)

    \lemma pairs-index-surj {A B C : \Type} {f : A -> B -> C} {l : Array A} {l' : Array B}
      : isSurj (\lam (s : \Sigma (Fin l.len) (Fin l'.len)) => (pairs-index {_} {_} {_} {f} s. s.).) \elim l
      | nil => \case __
      | a :: l => \lam k => \case ++.split-index k \with {
        | inl r => inP ((, r.), inv r.)
        | inr r => TruncP.map (pairs-index-surj r.) $ \lam t => ((suc t.., t..), pmap ++.index-right t. *> inv r.)
      }

    \lemma pairs-index-equiv {A B C : \Type} {f : A -> B -> C} {l : Array A} {l' : Array B}
      : Equiv {\Sigma (Fin l.len) (Fin l'.len)} {Fin (DArray.len {pairs f l l'})} (\lam s => (pairs-index s. s.).)
      => Equiv.fromInjSurj _ (\lam p => ext (pairs-index-inj p)) pairs-index-surj

    \lemma pairs-distr {A : \Type} {R : Semiring} {f : A -> A -> A} (g : A -> R) {l l' : Array A} (p : \Pi {a b : A} -> g (f a b) = g a R.* g b)
      : R.BigSum (map g (pairs f l l')) = R.BigSum (map g l) R.* R.BigSum (map g l')
      => inv R.FinSum=BigSum *> R.FinSum_Equiv pairs.pairs-index-equiv *> pmap R.FinSum (ext $ \lam s => rewrite (pairs.pairs-index s. s.). p) *> inv R.FinSum-distr *> pmap2 (R.*) R.FinSum=BigSum R.FinSum=BigSum
  }

\func find {A : \Type} (P : A -> Decide) (l : Array A) : Or (\Sigma (j : Fin l.len) (P (l j)) (\Pi {i : Fin l.len} -> i NatSemiring.< j -> P (l i) -> Empty)) (\Pi {j : Fin l.len} -> P (l j) -> Empty) \elim l
  | nil => inr \lam {j} => \case j
  | a :: l => \case decide {P a} \with {
    | yes e => inl (, e, \case __)
    | no q => \case find P l \with {
      | inl e => inl (suc e., e., \lam {i} => \case \elim i \with {
        |  => \lam _ => q
        | suc i => \lam (NatSemiring.suc<suc p) => e. p
      })
      | inr p => inr \lam {j} => \case \elim j \with {
        |  => q
        | suc j => p
      }
    }
  }

\sfunc index-dec {A : DecSet} (l : Array A) (a : A) : Or (Index a l) (Not (Index a l)) \elim l
  | nil => inr $ \case __.
  | b :: l => \case decideEq b a \with {
    | yes e => inl (, e)
    | no q => \case index-dec l a \with {
      | inl e => inl (suc e., e.)
      | inr p => inr $ \case __ \with {
        | (, c) => q c
        | (suc i, c) => p (i,c)
      }
    }
  }

\func repeats-dec {A : DecSet} (l : Array A) : Or (\Sigma (i j : Fin l.len) (i /= j) (l i = l j)) (isInj l) \elim l
  | nil => inr $ \lam {i} => \case i
  | a :: l => \case index-dec l a \with {
    | inl e => inl (suc e., , (\case __), e.)
    | inr q => \case repeats-dec l \with {
      | inl e => inl (suc e., suc e., fsuc/= e., e.)
      | inr p => inr $ \lam {i} {j} => \case \elim i, \elim j \with {
        | ,  => \lam _ => idp
        | , suc j => \lam r => absurd $ q (j, inv r)
        | suc i,  => \lam r => absurd $ q (i, r)
        | suc i, suc j => \lam r => pmap fsuc (p r)
      }
    }
  }

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

\lemma forall-char {A : \Type} {p : A -> Bool} {l : Array A} (s : forall p l = true) (j : Fin l.len) : p (l j) = true \elim l, j
  | a :: l,  => (and.toSigma s).
  | a :: l, suc j => forall-char (and.toSigma s). j

\func fit {A : \Type} (a : A) {n : Nat} (l : Array A) : Array A n \elim n, l
  | , _ => nil
  | suc n, nil => replicate (suc n) a
  | suc n, b :: l => b :: fit a l

\func fit_< {A : \Type} {a : A} {n : Nat} (l : Array A) {j : Fin n} (p : j < l.len) : fit a l j = l (toFin j p) \elim n, l, j, p
  | suc n, b :: l, , _ => idp
  | suc n, b :: l, suc j, NatSemiring.suc<suc p => fit_< _ p

\func fit_>= {A : \Type} {a : A} {n : Nat} (l : Array A) {j : Fin n} (p : l.len <= j) : fit a l j = a \elim n, l, j
  | suc n, nil, j => idp
  | suc n, b :: l,  => absurd linarith
  | suc n, b :: l, suc j => fit_>= l (suc<=suc.conv p)

\func fit_<' {A : \Type} {a : A} {n : Nat} (l : Array A) {j : Fin l.len} (p : j < n) : fit a l (toFin j p) = l j \elim n, l, j, p
  | suc n, b :: l, , _ => idp
  | suc n, b :: l, suc j, NatSemiring.suc<suc p => fit_<' _ p

\lemma fit_BigSum {A : AddMonoid} {n : Nat} {l : Array A} (p : \Pi (j : Fin l.len) -> n <= j -> l j = ) : A.BigSum (fit  {n} l) = A.BigSum l \elim n, l
  | , l => inv $ A.BigSum_zro \lam j => p j zero<=_
  | suc n, nil => A.BigSum_replicate0 {suc n}
  | suc n, a :: l => pmap (a +) $ fit_BigSum \lam j n<=j => p (suc j) (suc<=suc n<=j)

\lemma fit-transpose {A : AddMonoid} {n m : Nat} (l : Array (Array A m) n) : A.BigSum (\lam j => fit A.zro (l j) j) = A.BigSum (\lam k => fit A.zro (l __ k) k) \elim n, m, l
  | , , nil => idp
  | , suc m, nil => inv $ A.BigSum_replicate0 {suc m}
  | suc n, , c :: l => A.BigSum_replicate0 {suc n}
  | suc n, suc m, c :: l => pmap (c  +) $ fit-transpose \lam i => \lam j => l i (suc j)

\func fit_map {A B : \Type} (f : A -> B) {a : A} {b : B} (p : f a = b) {n : Nat} {l : Array A} : map f (fit a {n} l) = fit b (map f l) \elim n, l
  | , l => idp
  | suc n, nil => pmap (replicate (suc n)) p
  | suc n, a' :: l => path (\lam i => f a' :: fit_map f p i)

\func array/= {A : DecSet} {n : Nat} {l l' : Array A n} (p : l /= l') : \Sigma (j : Fin n) (l j /= l' j) \elim n, l, l'
  | , nil, nil => absurd (p idp)
  | suc n, a :: l, a' :: l' => \case decideEq a a' \with {
    | yes a=a' => \have (j,q) => array/= (\lam s => p $ pmap2 (::) a=a' s)
                  \in (suc j, q)
    | no a/=a' => (, a/=a')
  }

\func toList {A : \Type} (l : Array A) : List A \elim l
  | nil => List.nil
  | a :: l => a List.:: toList l

\lemma toList_length {A : \Type} {l : Array A} : length (toList l) = l.len \elim l
  | nil => idp
  | a :: l => pmap suc toList_length

\func fromList {A : \Type} (l : List A) : Array A (length l) \elim l
  | List.nil => nil
  | a List.:: l => a :: fromList l

\func fromList_toList {A : \Type} {l : Array A} : fromList (toList l) = l \elim l
  | nil => idp
  | a :: l => pmap (a ::) fromList_toList

\func sort {A : LinearOrder.Dec} (l : Array A) : Array A l.len
  => transport (\lam n => Array A n) (inv (Sort.Perm.perm_length (Sort.Insertion.sort-perm _)) *> toList_length) $ fromList (Sort.Insertion.sort (toList l))
  \where {
    \func IsSorted {A : Preorder} (l : Array A) => \Pi {i j : Fin l.len} -> i NatSemiring.< j -> l i <= l j

    \lemma sorted_transport {A : Preorder} {n m : Nat} {l : Array A n} (p : n = m) (s : IsSorted l) : IsSorted (transport (\lam n => Array A n) p l) \elim p
      | idp => s

    \lemma list_sorted {A : Preorder} {l : List A} (s : Sort.Sorted l) : IsSorted (fromList l) \elim l, s
      | List.nil, Sort.sorted-nil => \lam {i} => \case i
      | x List.:: l, Sort.sorted-cons p s => \lam {i} {j} p => \case \elim i, \elim j, \elim p \with {
        | , suc j, NatSemiring.zero<suc => p <=∘ headDef_fromList s
        | suc i, suc j, NatSemiring.suc<suc p => list_sorted s p
      }
      \where {
        \lemma headDef_fromList {a : A} {l : List A} {j : Fin (length l)} (s : Sort.Sorted l) : headDef a l <= fromList l j \elim l, j, s
          | b List.:: l, , _ => <=-refl
          | b List.:: l, suc j, Sort.sorted-cons p s => p <=∘ headDef_fromList s
      }

    \lemma sorted_list {A : Preorder} {l : Array A} (s : IsSorted l) : Sort.Sorted (toList l) \elim l
      | nil => Sort.sorted-nil
      | a :: l => Sort.sorted-cons (\case \elim l, \elim s \with {
        | nil, s => <=-refl
        | b :: l, s => s {} {} NatSemiring.zero<suc
      }) $ sorted_list \lam p => s (NatSemiring.suc<suc p)

    \lemma sort-sorted {A : LinearOrder.Dec} {l : Array A} : IsSorted (sort l)
      => sorted_transport _ (list_sorted (Sort.Insertion.sort-sorted _))

    \sfunc sort-perm {A : LinearOrder.Dec} {n : Nat} {l : Array A n} : Perm l (sort l)
      => Perm.perm-sym $ EPerm.EPerm_Perm_transport (EPerm.eperm-sym sort-eperm) _
      \where {
        \func list_perm {A : \Type} {l l' : List A} (p : Sort.Perm l l') : EPerm (fromList l) (fromList l') \elim l, l', p
          | List.nil, List.nil, Sort.perm-nil => eperm-nil
          | x List.:: l, y List.:: l', Sort.perm-:: p q => eperm-:: p (list_perm q)
          | x List.:: (x' List.:: l), y List.:: (y' List.:: l'), Sort.perm-swap p1 p2 q => eperm-swap p1 p2 (pmap fromList q)
          | l, l', Sort.perm-trans p1 p2 => eperm-trans (list_perm p1) (list_perm p2)

        \func sort-eperm {A : LinearOrder.Dec} {l : Array A} : EPerm l (fromList (Sort.Insertion.sort (toList l)))
          => transport (EPerm __ _) fromList_toList $ list_perm (Sort.Insertion.sort-perm _)
      }

    \lemma perm_= {A : LinearOrder.Dec} {n : Nat} {l l' : Array A n} (p : Perm l l') (s : IsSorted l) (s' : IsSorted l') : l = l'
      => exts $ array-unext $ inv fromList_toList *> pmap fromList (inv (Sort.Insertion.sorted_sort (sorted_list s)) *> Sort.Insertion.perm_sort (Perm.perm_list p) *> Sort.Insertion.sorted_sort (sorted_list s')) *> fromList_toList
  }

\func take {A : \Type} (n : Nat) (l : Array A) (p : n <= l.len) : Array A n \elim n, l
  | , l => nil
  | suc n, nil => absurd (p NatSemiring.zero<suc)
  | suc n, a :: l => a :: take n l (suc<=suc.conv p)

\func take-index {A : \Type} {n : Nat} {l : Array A} {p : n <= l.len} {j : Fin n} : take n l p j = l (fin-inc_<= p j) \elim n, l, j
  | suc n, nil, j => absurd (p NatSemiring.zero<suc)
  | suc n, a :: l,  => idp
  | suc n, a :: l, suc j => take-index