0 | module Data.List.Elem.Extra
 1 |
 2 | import Data.List
 3 | import Data.List.Elem
 4 |
 5 | %default total
 6 |
 7 | ||| Proof that an element is still inside a list if we append to it.
 8 | public export
 9 | elemAppLeft : (xs, ys : List a) -> (prf : Elem x xs) -> Elem x (xs ++ ys)
10 | elemAppLeft (x :: xs) ys Here = Here
11 | elemAppLeft (x :: xs) ys (There prf2) = There $ elemAppLeft xs ys prf2
12 |
13 |
14 | ||| Proof that an element is still inside a list if we prepend to it.
15 | public export
16 | elemAppRight :  (ys, xs : List a) -> (prf : Elem x xs) -> Elem x (ys ++ xs)
17 | elemAppRight [] xs prf = prf
18 | elemAppRight (y :: ys) xs prf = There $ elemAppRight ys xs prf
19 |
20 | ||| Proof that membership on append implies membership in left or right sublist.
21 | public export
22 | elemAppLorR : (xs, ys : List a)
23 |            -> (prf : Elem k (xs ++ ys))
24 |            -> Either (Elem k xs) (Elem k ys)
25 | elemAppLorR [] [] prf = absurd prf
26 | elemAppLorR [] _ prf = Right prf
27 | elemAppLorR (x :: xs) [] prf =
28 |   Left $ rewrite sym $ appendNilRightNeutral xs in prf
29 | elemAppLorR (x :: xs) _ Here = Left Here
30 | elemAppLorR (x :: xs) ys (There prf) = mapFst There $ elemAppLorR xs ys prf
31 |
32 |
33 | ||| Proof that x is not in (xs ++ ys) implies proof that x is not in xs.
34 | public export
35 | notElemAppLeft : (xs, ys : List a)
36 |               -> (prf : Not (Elem x (xs ++ ys)))
37 |               -> Not (Elem x xs)
38 | notElemAppLeft xs ys prf = prf . elemAppLeft xs ys
39 |
40 | ||| Proof that x is not in (xs ++ ys) implies proof that x is not in ys.
41 | public export
42 | notElemAppRight : (ys, xs : List a)
43 |                -> (prf : Not (Elem x (xs ++ ys)))
44 |                -> Not (Elem x ys)
45 | notElemAppRight ys xs prf = prf . elemAppRight xs ys
46 |