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