In Chapter 9 of Type Driven Development with Idris, we are introduced to the Elem predicate with constructors Here and There for proving that an element is a member of a vector. e.g.
oneInVector : Elem 1 [1, 2, 3]
oneInVector = Here
twoInVector : Elem 2 [1, 2, 3]
twoInVector = There Here
I'm wondering how to show that an element is not in a vector. It should perhaps be by providing a solution to this type:
notThere : Elem 4 [1, 2, 3] -> Void
notThere = ?rhs
Expression/Proof search does not come up with the answer in this case, giving:
notThere : Elem 4 [1,2,3] -> Void
notThere = \__pi_arg => ?rhs1
Scanning through the library for Data.Vect, these definitions look useful (but I'm not sure how to connect the dots):
||| Nothing can be in an empty Vect
noEmptyElem : {x : a} -> Elem x [] -> Void
noEmptyElem Here impossible
Uninhabited (Elem x []) where
uninhabited = noEmptyElem
The Elem relation is Decidable (if the element type has Decidable Equality itself), using isElem:
isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
The idea is to use isElem 4 [1, 2, 3] to have Idris compute the proof of Not (Elem 4 [1, 2, 3]). We'll need to build up some machinery similar to Agda's Relation.Nullary.Decidable.toWitnessFalse so that we can extract proofs from (negative) Dec results:
fromFalse : (d : Dec p) -> {auto isFalse : decAsBool d = False} -> Not p
fromFalse (Yes _) {isFalse = Refl} impossible
fromFalse (No contra) = contra
and then we can use this in your notThere definition:
notThere : Not (Elem 4 [1, 2, 3])
notThere = fromFalse (isElem 4 [1, 2, 3])