List.agda 2.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384
  1. module Lib.List where
  2. open import Lib.Prelude
  3. open import Lib.Id
  4. infix 30 _∈_
  5. infixr 40 _::_ _++_
  6. infix 45 _!_
  7. data List (A : Set) : Set where
  8. [] : List A
  9. _::_ : A -> List A -> List A
  10. {-# COMPILE GHC List = data [] ([] | (:)) #-}
  11. {-# BUILTIN LIST List #-}
  12. {-# BUILTIN NIL [] #-}
  13. {-# BUILTIN CONS _::_ #-}
  14. _++_ : {A : Set} -> List A -> List A -> List A
  15. [] ++ ys = ys
  16. (x :: xs) ++ ys = x :: (xs ++ ys)
  17. foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
  18. foldr f z [] = z
  19. foldr f z (x :: xs) = f x (foldr f z xs)
  20. map : {A B : Set} -> (A -> B) -> List A -> List B
  21. map f [] = []
  22. map f (x :: xs) = f x :: map f xs
  23. map-id : forall {A}(xs : List A) -> map id xs ≡ xs
  24. map-id [] = refl
  25. map-id (x :: xs) with map id xs | map-id xs
  26. ... | .xs | refl = refl
  27. data _∈_ {A : Set} : A -> List A -> Set where
  28. hd : forall {x xs} -> x ∈ x :: xs
  29. tl : forall {x y xs} -> x ∈ xs -> x ∈ y :: xs
  30. data All {A : Set}(P : A -> Set) : List A -> Set where
  31. [] : All P []
  32. _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)
  33. head : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> P x
  34. head (x :: xs) = x
  35. tail : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> All P xs
  36. tail (x :: xs) = xs
  37. _!_ : forall {A}{P : A -> Set}{x xs} -> All P xs -> x ∈ xs -> P x
  38. xs ! hd = head xs
  39. xs ! tl n = tail xs ! n
  40. tabulate : forall {A}{P : A -> Set}{xs} -> ({x : A} -> x ∈ xs -> P x) -> All P xs
  41. tabulate {xs = []} f = []
  42. tabulate {xs = x :: xs} f = f hd :: tabulate (f ∘ tl)
  43. mapAll : forall {A B}{P : A -> Set}{Q : B -> Set}{xs}(f : A -> B) ->
  44. ({x : A} -> P x -> Q (f x)) -> All P xs -> All Q (map f xs)
  45. mapAll f h [] = []
  46. mapAll f h (x :: xs) = h x :: mapAll f h xs
  47. mapAll- : forall {A}{P Q : A -> Set}{xs} ->
  48. ({x : A} -> P x -> Q x) -> All P xs -> All Q xs
  49. mapAll- {xs = xs} f zs with map id xs | map-id xs | mapAll id f zs
  50. ... | .xs | refl | r = r
  51. infix 20 _⊆_
  52. data _⊆_ {A : Set} : List A -> List A -> Set where
  53. stop : [] ⊆ []
  54. drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
  55. keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys
  56. ⊆-refl : forall {A}{xs : List A} -> xs ⊆ xs
  57. ⊆-refl {xs = []} = stop
  58. ⊆-refl {xs = x :: xs} = keep ⊆-refl
  59. _∣_ : forall {A}{P : A -> Set}{xs ys} -> All P ys -> xs ⊆ ys -> All P xs
  60. [] ∣ stop = []
  61. (x :: xs) ∣ drop p = xs ∣ p
  62. (x :: xs) ∣ keep p = x :: (xs ∣ p)