List.agda

module Lib.List where

open import Lib.Prelude
open import Lib.Id

infix  30 _∈_
infixr 40 _::_ _++_
infix  45 _!_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

{-# COMPILED_DATA List [] [] (:) #-}
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}

_++_ : {A : Set} -> List A -> List A -> List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f z [] = z
foldr f z (x :: xs) = f x (foldr f z xs)

map : {A B : Set} -> (A -> B) -> List A -> List B
map f [] = []
map f (x :: xs) = f x :: map f xs

map-id : forall {A}(xs : List A) -> map id xs ≡ xs
map-id [] = refl
map-id (x :: xs) with map id xs | map-id xs
... | .xs | refl = refl

data _∈_ {A : Set} : A -> List A -> Set where
  hd : forall {x xs}   ->           x ∈ x :: xs
  tl : forall {x y xs} -> x ∈ xs -> x ∈ y :: xs

data All {A : Set}(P : A -> Set) : List A -> Set where
  []   : All P []
  _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)

head : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> P x
head (x :: xs) = x

tail : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> All P xs
tail (x :: xs) = xs

_!_ : forall {A}{P : A -> Set}{x xs} -> All P xs -> x ∈ xs -> P x
xs ! hd   = head xs
xs ! tl n = tail xs ! n

tabulate : forall {A}{P : A -> Set}{xs} -> ({x : A} -> x ∈ xs -> P x) -> All P xs
tabulate {xs = []}      f = [] 
tabulate {xs = x :: xs} f = f hd :: tabulate (f ∘ tl)

mapAll : forall {A B}{P : A -> Set}{Q : B -> Set}{xs}(f : A -> B) ->
         ({x : A} -> P x -> Q (f x)) -> All P xs -> All Q (map f xs)
mapAll f h [] = []
mapAll f h (x :: xs) = h x :: mapAll f h xs

mapAll- : forall {A}{P Q : A -> Set}{xs} ->
          ({x : A} -> P x -> Q x) -> All P xs -> All Q xs
mapAll- {xs = xs} f zs with map id xs | map-id xs | mapAll id f zs
... | .xs | refl | r = r

infix 20 _⊆_

data _⊆_ {A : Set} : List A -> List A -> Set where
  stop : [] ⊆ []
  drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
  keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys

⊆-refl : forall {A}{xs : List A} -> xs ⊆ xs
⊆-refl {xs = []}      = stop
⊆-refl {xs = x :: xs} = keep ⊆-refl

_∣_ : forall {A}{P : A -> Set}{xs ys} -> All P ys -> xs ⊆ ys -> All P xs
[]        ∣ stop   = []
(x :: xs) ∣ drop p = xs ∣ p
(x :: xs) ∣ keep p = x :: (xs ∣ p)