open import Paths
open import Arith::Fin
open import Algebra::Formula

open data List (A : Type) : Type
| nil
| infixr :< A (List A)
  tighter =

variable A B C : Type

def length (l : List A) : Nat
| nil ⇒ 0
| _ :< l ⇒ suc (length l)

def infix !! (l : List A) (i : Fin (length l)) : A
| a :< _, fzero ⇒ a
| _ :< l, fsuc i ⇒ l !! i

overlap def infixr ++ : BinOp (List A)
| nil, ys ⇒ ys
| xs, nil ⇒ xs
| a :< xs, ys ⇒ a :< (xs ++ ys)
tighter =

def concat (l : List (List A)) : List A
| nil ⇒ nil
| xs :< xss ⇒ xs ++ concat xss

private def ++-assoc-lemma : Associative {A := List A} (++)
| nil, _, _ ⇒ idp
| x :< xs, _, _ ⇒ pmap (x :<) ++-assoc
inline def ++-assoc {xs ys zs : List A} ⇒ ++-assoc-lemma xs ys zs

def ++nil {l : List A} : l ++ nil = l
| {A}, {nil} ⇒ idp
| {A}, {a :< l} ⇒ pmap (a :<) ++nil

def map (f : A → B) (l : List A) : List B
| f, nil ⇒ nil
| f, a :< l ⇒ f a :< map f l

def lengthMap (f : A → B) (l : List A) : length (map f l) = length l
| f, nil ⇒ idp
| f, a :< l ⇒ pmap suc (lengthMap f l)

def mapComp (g : B → C) (f : A → B) (l : List A) : map (\x ⇒ g (f x)) l = map g (map f l)
| _, _, nil ⇒ idp
| g, f, a :< l ⇒ pmap (g _ :<) (mapComp g f l)

def mapId (l : List A) : map (\x ⇒ x) l = l
| nil ⇒ idp
| a :< l ⇒ pmap (a :<) (mapId l)

def headDef (x : A) (xs : List A) : A
| x, nil ⇒ x
| _, a :< _ ⇒ a

def splitAt (n : Nat) (l : List A) : Σ (List A) ** (List A)
| 0, l ⇒ (nil, l)
| suc n, nil ⇒ (nil, nil)
| suc n, a :< l ⇒ let
  // No pattern let yet, sorry!
  | t := splitAt n l
  in (a :< t.1, t.2)

def take (n : Nat) (l : List A) ⇒ (splitAt n l).1

def drop (n : Nat) (l : List A) ⇒ (splitAt n l).2

def replace (l : List A) (i s : Nat) (r : List A) ⇒
  let
  | t := splitAt i l
  in t.1 ++ r ++ drop s t.2

def splitAt-appendLem (n : Nat) (l : List A) : take n l ++ drop n l = l
| 0, l ⇒ idp
| suc n, nil ⇒ idp
| suc n, a :< l ⇒ pmap (a :<) (splitAt-appendLem n l)

def slice (l : List A) (i s : Nat) ⇒ take s (drop i l)

def slice-appendLem (l : List A) (i s : Nat)
   : take i l ++ (slice l i s ++ drop s (drop i l)) = l
| l, 0, s ⇒ splitAt-appendLem s l
| nil, suc i, 0 ⇒ idp
| nil, suc i, suc s ⇒ idp
| a :< l, suc i, s ⇒ pmap (a :<) (slice-appendLem l i s)