0 | module Data.List.Elem
  1 |
  2 | import Data.Singleton
  3 | import Decidable.Equality
  4 | import Control.Function
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | -- List membership proof
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| A proof that some element is found in a list.
 13 | public export
 14 | data Elem : a -> List a -> Type where
 15 |      ||| A proof that the element is at the head of the list
 16 |      Here : Elem x (x :: xs)
 17 |      ||| A proof that the element is in the tail of the list
 18 |      There : Elem x xs -> Elem x (y :: xs)
 19 |
 20 | export
 21 | Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs = xs'} e) where
 22 |   uninhabited Refl impossible
 23 |
 24 | export
 25 | Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs = xs'}) where
 26 |   uninhabited Refl impossible
 27 |
 28 | export
 29 | Injective (There {x} {y} {xs}) where
 30 |   injective Refl = Refl
 31 |
 32 | export
 33 | DecEq (Elem x xs) where
 34 |   decEq Here Here = Yes Refl
 35 |   decEq (There this) (There that) = decEqCong $ decEq this that
 36 |   decEq Here (There later) = No absurd
 37 |   decEq (There later) Here = No absurd
 38 |
 39 | export
 40 | Uninhabited (Elem {a} x []) where
 41 |   uninhabited Here impossible
 42 |   uninhabited (There p) impossible
 43 |
 44 | export
 45 | Uninhabited (x = z) => Uninhabited (Elem z xs) => Uninhabited (Elem z $ x::xs) where
 46 |   uninhabited Here @{xz} = uninhabited Refl @{xz}
 47 |   uninhabited (There y) = uninhabited y
 48 |
 49 | ||| An item not in the head and not in the tail is not in the list at all.
 50 | export
 51 | neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
 52 | neitherHereNorThere xny _     Here        = xny Refl
 53 | neitherHereNorThere _   xnxs  (There xxs) = xnxs xxs
 54 |
 55 | ||| Check whether the given element is a member of the given list.
 56 | public export
 57 | isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
 58 | isElem x [] = No absurd
 59 | isElem x (y :: xs) with (decEq x y)
 60 |   isElem x (x :: xs) | Yes Refl = Yes Here
 61 |   isElem x (y :: xs) | No xny with (isElem x xs)
 62 |     isElem x (y :: xs) | No xny | Yes xxs = Yes (There xxs)
 63 |     isElem x (y :: xs) | No xny | No xnxs = No (neitherHereNorThere xny xnxs)
 64 |
 65 | ||| Get the element at the given position.
 66 | public export
 67 | get : (xs : List a) -> (p : Elem x xs) -> a
 68 | get (x :: _) Here = x
 69 | get (_ :: xs) (There p) = get xs p
 70 |
 71 | ||| Get the element at the given position, with proof that it is the desired element.
 72 | public export
 73 | lookup : (xs : List a) -> (p : Elem x xs) -> Singleton x
 74 | lookup (x :: _) Here = Val x
 75 | lookup (_ :: xs) (There p) = lookup xs p
 76 |
 77 | ||| Remove the element at the given position.
 78 | public export
 79 | dropElem : (xs : List a) -> (p : Elem x xs) -> List a
 80 | dropElem (_ :: ys)  Here     = ys
 81 | dropElem (x :: ys) (There p) = x :: dropElem ys p
 82 |
 83 | ||| Erase the indices, returning the numeric position of the element
 84 | public export
 85 | elemToNat : Elem x xs -> Nat
 86 | elemToNat  Here     = Z
 87 | elemToNat (There p) = S (elemToNat p)
 88 |
 89 | ||| Find the element with a proof at a given position, if it is valid
 90 | public export
 91 | indexElem : Nat -> (xs : List a) -> Maybe (x ** Elem x xs)
 92 | indexElem  _    []        = Nothing
 93 | indexElem  Z    (y :: _)  = Just (y ** Here)
 94 | indexElem (S n) (_ :: ys) = map (\(x ** p) => (x ** There p)) (indexElem n ys)
 95 |
 96 | ||| Lift the membership proof to a mapped list
 97 | export
 98 | elemMap : (0 f : a -> b) -> Elem x xs -> Elem (f x) (map f xs)
 99 | elemMap f  Here      = Here
100 | elemMap f (There el) = There $ elemMap f el
101 |