\import Algebra.Meta
\import Arith.Nat
\import Data.Bool
\import Data.Fin
\import Data.List(List, length)
\import Data.Maybe
\import Data.Or
\import Function
\import Function.Meta ($)
\import Logic
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin

\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',  => 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 = ) : 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 cong_:: {A : \Type} {a a' : A} (p : a = a') {l l' : Array A} (q : l = l') : a :: l = a' :: l'
  => path \lam i => p i :: q i

\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 map2_++' {A B C : \Type} (f : A -> B -> C) {n : Nat} {l1 : Array A n} {l2 : Array B n} {m : Nat} {l1' : Array A m} {l2' : Array B m}
  : mkArray (\lam j => f (++' l1 l1' j) (++' l2 l2' j)) = mkArray (\lam j => f (l1 j) (l2 j)) ++' mkArray (\lam j => f (l1' j) (l2' j)) \elim n, l1, l2
  | , nil, nil => idp
  | suc n, a1 :: l1, a2 :: l2 => path (\lam i => f a1 a2 :: map2_++' 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 $ (fin_< i) NatSemiring.<∘l rewrite (inv index-left-nat *> p *> index-right-nat) (NatSemiring.<=_+ <=-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 ++-all {A : \Type} {P : A -> \Type} {l l' : Array A} (Pl : \Pi (i : Fin l.len) -> P (l i)) (Pl' : \Pi (i : Fin l'.len) -> P (l' i)) (j : Fin (l ++ l').len) : P ((l ++ l') j)
      => \case ++.split-index j \with {
        | inl (i,p) => rewrite (p,++_index-left) (Pl i)
        | inr (i,p) => rewrite (p,++_index-right) (Pl' 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} {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 ) $ 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 ) $ 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,  => 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 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,  => 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 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,  => 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,  => (,idp)
        | yes e, suc i => \let t => preimage i \in (suc t., t.)
        | no q, 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 {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 _, , , q => idp
        | yes s, , suc j, q => \let t => preimage j \in \case p {} {suc t.} (q *> t.)
        | yes _, suc i, , q => \let t => preimage i \in \case p {suc t.} {} (inv t. *> 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 )) $ 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 )) $ 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,  => 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  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, , 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 {
        | , p => mcases \with {
          | yes e => absurd (p e)
          | no q => (,idp)
        }
        | suc j, p => mcases \with {
          | yes e => element p
          | no q => \let t => element p
                    \in (suc t., t.)
        }
      }

    \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 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 )) $ 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)
  }

\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 =  \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
  | , 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_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 {} {suc (nub-preimage j).} $ p *> (nub-preimage j).) *> 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,  => 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 NatOrder

    \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)

\func count {A : DecSet} (l : Array A) (a : A) : Nat \elim l
  | nil => 
  | 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 Nat.+ 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 (_ Nat.+) 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 ) $ 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 =  \elim l
  | nil => idp
  | x :: l => rewrite (decideEq/=_reduce $ /=-sym $ p ) $ 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
  }

\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 NatOrder.< 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 (NatOrder.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))
  => \case find (EqualityDecide A __ a) l \with {
       | inl p => inl (p.,p.)
       | inr q => inr \lam p => q p.
     }

\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 NatOrder.< 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, NatOrder.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 NatOrder.< 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, NatOrder.suc<suc p => fit_<' _ p

\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 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 NatOrder.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 NatOrder.zero<suc)
  | suc n, a :: l,  => idp
  | suc n, a :: l, suc j => take-index

\func singleAt {A : \Type} {n : Nat} (j : Fin n) (value def : A) : Array A n \cowith
  | at i => \case decideEq j i \with {
    | yes _ => value
    | no _ => def
  }
  \where \protected {
    \func alt {A : \Type} {n : Nat} (j : Fin n) (value def : A) : Array A n \elim n, j
      | suc n,  => value :: replicate n def
      | suc n, suc j => def :: alt j value def

    \sfunc char {A : \Type} {n : Nat} {j : Fin n} {value def : A} : singleAt j value def = alt j value def \elim n, j
      | suc n,  => idp
      | suc n, suc j => exts (\case \elim __ \with {
        |  => idp
        | suc k => mcases {} \with {
          | yes p => rewrite (decideEq=_reduce $ pmap fsuc p) idp
          | no q => rewrite (decideEq/=_reduce $ fsuc/= q) idp
        }
      }) *> pmap {Array A n} (def :: __) char
  }