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