{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude
open import Recursion
open import List
open import Nat

module ListProps where


-- Properties of Lists on a Specific Set --

module ListPropsAux {A : Set} where

  ∷-inj : Injective2 {A} _∷_
  ∷-inj refl = refl , refl

  ∷-cong : Congruent2 {A} _∷_
  ∷-cong = cong2 _∷_

  ∷-congL : Congruent2L {A} _∷_
  ∷-congL = cong2L _∷_

  ∷-congR : Congruent2R {A} _∷_
  ∷-congR = cong2R _∷_

  ++assoc : {bs cs : List A}  (as : List A)  (as ++ bs) ++ cs  as ++ bs ++ cs
  ++assoc = listrec refl ∷-congL

  ++[]' : (as : List A)  as ++ []  as
  ++[]' = listrec refl ∷-congL

  ++[] : {as : List A}  as ++ []  as
  ++[] {as} = ++[]' as

  import Monoid
  open Monoid _++_  {as}  ++assoc as) [] refl ++[] public

  import SemiGroup
  open SemiGroup _++_  {as}  ++assoc as) public

  listIdem : {f : A  A}  ({a : A}  f (f a)  f a)  (as : List A)  map f (map f as)  map f as
  listIdem eIdem = listrec refl (∷-cong eIdem)

  ++length : {bs : List A}  (as : List A)  length (as ++ bs)  length as + length bs
  ++length = listrec refl (cong S)

  ++lengthC : {bs : List A}  (as : List A)  length as + length bs  length (as ++ bs)
  ++lengthC = sym ∘' ++length

  +++length : {cs : List A}  (as bs : List A)  length (as ++ bs ++ cs)  length as + length bs + length cs
  +++length as bs =  trans2 (cong length (assocR {as})) (++length (as ++ bs)) (cong2 _+_ (++length as) refl)

  +++lengthC : {cs : List A}  (as bs : List A)  length as + length bs + length cs  length (as ++ bs ++ cs) 
  +++lengthC as bs = sym (+++length as bs)


  lengthZero : {as : List A}  length as  O  as  []
  lengthZero {[]} _ = refl
  lengthZero {_  _} ()

  mapId' : (as : List A)  map id as  as
  mapId' = listrec refl ∷-congL

  mapId : {as : List A}  map id as  as
  mapId {as} = mapId' as

  -- might need something else (other than just listrec) for ++rev, not sure

  ++rev : {as : List A}  (bs : List A)  rev as bs  reverse bs ++ as
  ++rev []       = refl
  ++rev (b  bs) = trans2 (++rev bs) (assocR {reverse bs}) (cong2R _++_ (sym (++rev bs)))

  slowReverse : List A  List A
  slowReverse [] = []
  slowReverse (a  as) = slowReverse as ++ [ a ]

  reversesEq : (as : List A)  reverse as  slowReverse as
  reversesEq = listrec' refl  _ as hyp  trans (++rev as) (cong2R _++_ hyp))

  ++reverseAux : {a : A}  {bs : List A}  (as : List A)  reverse (a  as ++ bs)  (reverse (as ++ bs)) ++ [ a ]
  ++reverseAux {a} {bs} as = trans (reversesEq (a  as ++ bs)) (cong2R _++_ (sym (reversesEq (as ++ bs))))

  ++reverse : {bs : List A}  (as : List A)  reverse (as ++ bs)  reverse bs ++ reverse as
  ++reverse {bs} = listrec' (sym ++[])  _ as hyp  trans3 (++reverseAux as) (cong2R _++_ hyp) (++assoc (reverse bs)) (cong (_++_ (reverse bs)) (sym (++rev as))))

  revrev' : (as : List A)  reverse (reverse as)  as 
  revrev' = listrec' refl  a as hyp  trans2 (cong reverse (reversesEq (a  as))) (++reverse (slowReverse as)) (cong (_∷_ a) (trans (cong reverse (sym (reversesEq as))) hyp)))

  revrev : {as : List A}  reverse (reverse as)  as
  revrev {as} = revrev' as

  reverseEq : {as bs : List A}  reverse as  reverse bs  as  bs 
  reverseEq eq = trans2 (sym revrev) (cong reverse eq) revrev

  ++reverseAuxR : {as bs : List A}  {b : A}  reverse as ++ b  bs  rev [ b ] as ++ bs
  ++reverseAuxR {as} {bs} = trans (assocR {rev [] as}) (cong (flip _++_ bs) (sym (++rev as)))

  ++cancL : {bs cs : List A}  (as : List A)  as ++ bs  as ++ cs  bs  cs
  ++cancL = listrec id (_⋙_ (snd  ∷-inj))

  ++cancR : {bs cs : List A}  (as : List A)  as ++ cs  bs ++ cs  as  bs
  ++cancR {bs} {cs} as eq = reverseEq (++cancL (reverse cs) (trans2 (sym (++reverse as)) (cong reverse eq) (++reverse bs)))

  import Cancellative
  open Cancellative _++_  {as}  ++cancL as)  {as}  ++cancR as) public

  ++eq[] : {as bs : List A}  as ++ bs  []  as  [] × bs  []
  ++eq[] {[]} eq = refl , eq
  ++eq[] {_  _} ()

  concatMapWrap' : (as : List A)  concat (map wrap as)  as
  concatMapWrap' = listrec refl ∷-congL

  concatMapWrap : {as : List A}  concat (map wrap as)  as
  concatMapWrap {as} = concatMapWrap' as

  concat++ : {bs : List (List A)}  (as : List (List A))  concat (as ++ bs)  concat as ++ concat bs
  concat++ = listrec' refl  a _ hyp  trans (cong (_++_ a) hyp) (assocR {a}))


  -- Prefixes -------------------------------------------------

  data Prefix (ls rs  : List A) : Set where
    prefixB : ls  rs                        Prefix ls rs
    prefixL : {xs : List A}  ls ++ xs  rs  Prefix ls rs
    prefixR : {xs : List A}  rs ++ xs  ls  Prefix ls rs

  addToPrefix : {ls rs : List A}  (a : A)  Prefix ls rs  Prefix (a  ls) (a  rs)
  addToPrefix a (prefixB refl) = prefixB refl
  addToPrefix a (prefixL refl) = prefixL refl
  addToPrefix a (prefixR refl) = prefixR refl

  comparePrefix : {xs ys : List A}  (ls rs : List A)  ls ++ xs  rs ++ ys  Prefix ls rs
  comparePrefix [] [] eq = prefixB refl
  comparePrefix [] rs eq = prefixL refl
  comparePrefix ls [] eq = prefixR refl
  comparePrefix (a  ls) (_   rs) eq with ∷-inj eq
  comparePrefix (a  ls) (.a  rs) eq | refl , eqls = addToPrefix a (comparePrefix ls rs eqls)


  -- Suffixes -------------------------------------------------------------

  data Suffix (ls rs : List A) : Set where
    suffixB : ls  rs                        Suffix ls rs
    suffixL : (xs : List A)  xs ++ ls  rs  Suffix ls rs
    suffixR : (xs : List A)  xs ++ rs  ls  Suffix ls rs

  reverseAux : {bs cs : List A}  (as : List A)  reverse as ++ bs  reverse cs  reverse bs ++ as  cs
  reverseAux {bs} as eq = reverseEq (trans2 (++reverse (reverse bs)) (cong (_++_ (reverse as)) revrev) eq)

  compareSuffix : {xs ys : List A}  (ls rs : List A)  xs ++ ls  ys ++ rs  Suffix ls rs
  compareSuffix {xs} {ys} ls rs eq with comparePrefix (reverse ls) (reverse rs) (trans2 (sym (++reverse xs)) (cong reverse eq) (++reverse ys))
  ... | prefixB eq2 = suffixB (reverseEq eq2)
  ... | prefixL {xls} eq2 = suffixL (reverse xls) (reverseAux ls eq2)
  ... | prefixR {xrs} eq2 = suffixR (reverse xrs) (reverseAux rs eq2)


  -- Element of -----------------------------------------------------------

  infix 3 _∈_ 

  data _∈_ (a : A) : List A  Set where
    hd : {as : List A}  a  a  as
    tl : {b : A}  {as : List A}  a  as  a  b  as

  index : {a : A}  {as : List A}  a  as  
  index hd = O
  index (tl el) = S (index el)

  data Lookup (as : List A) :   Set where
    inside  : (a : A)  (el : a  as)  Lookup as (index el)
    outside : (n : )  Lookup as (length as + n)

  _!_ : (as : List A)  (n : )  Lookup as n
  [] ! n = outside n
  (a  as) ! O = inside a hd
  (a  as) ! S n with as ! n
  (a  as) ! S .(index el)      | inside b el = inside b (tl el)
  (a  as) ! S .(length as + n) | outside n   = outside n


---------------------------------------------------------------------------

open ListPropsAux public

-- Properties of lists over several sets --

lengthMap : {A B : Set}  {f : A  B}  (as : List A)  length (map f as)  length as
lengthMap = listrec refl (cong S)

map++ : {A B : Set}  {f : A  B}  {as₂ : List A}  (as₁ : List A)  map f (as₁ ++ as₂)  map f as₁ ++ map f as₂
map++ = listrec refl ∷-congL

mapmap : {A B C : Set}  {f : B  C}  {g : A  B}  (as : List A)  map f (map g as)  map (f  g) as
mapmap = listrec refl (∷-cong refl)