Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
module Main
import Data.Vect
import Data.Fin
%default total
||| If a value is neither at the head of a Vect nor in the tail of
||| that Vect, then it is not in the Vect.
notHeadNotTail : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
notHeadNotTail notHead notTail Here = notHead Refl
notHeadNotTail notHead notTail (There tl) = notTail tl
||| Determine the first location of an element in a Vect. The types
||| guarantee that we find a valid index, but not that it's the first
||| occurrence.
find : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
find x [] = No absurd
find x (y :: xs) with (decEq x y)
find x (x :: xs) | Yes Refl = Yes Here
find x (y :: xs) | No notHead with (find x xs)
find x (y :: xs) | No notHead | Yes prf = Yes (There prf)
find x (y :: xs) | No notHead | No notTail =
No $ notHeadNotTail notHead notTail
||| Find a Fin giving a position in a Vect, instead of an Elem
findIndex : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (Fin n)
findIndex x [] = Nothing
findIndex x (y :: xs) =
case decEq x y of
Yes _ => pure FZ
-- the following could be written as:
-- No _ => do tailIdx <- findIndex x xs
-- pure (FS tailIdx)
-- but idiom brackets are a bit cleaner:
No _ => [| FS (findIndex x xs) |]
-- (that was like the Haskell FS <$> findIndex x xs)
-- Prove that the Fin version corresponds to the Elem
-- version. Correspondence here means that if a Fin is found, we can
-- construct an Elem proof, and if a Fin is not found, then it is
-- provably impossible to construct an Elem proof.
findIndexOk : DecEq a => (x : a) -> (xs : Vect n a) ->
case findIndex x xs of
Just i => Elem x xs
Nothing => Not (Elem x xs)
findIndexOk x [] = absurd -- this is proved in the library already! :-)
findIndexOk x (y :: xs) with (decEq x y)
findIndexOk x (x :: xs) | Yes Refl = Here
findIndexOk x (y :: xs) | No notHead with (findIndexOk x xs) -- get an induction hypothesis
findIndexOk x (y :: xs) | No notHead | ih with (findIndex x xs) -- split on the result of
-- the recursive call, to
-- reduce case expression
-- in the IH type
-- in this case, the induction hypothesis takes the second
-- branch in the case expression in the type, which tells us
-- that Not (Elem x xs)
findIndexOk x (y :: xs) | No notHead | ih | Nothing = notHeadNotTail notHead ih
-- in this case, the IH tells us that it was indeed in the tail,
-- so we wrap in There to make it valid for y :: xs instead of
-- just xs
findIndexOk x (y :: xs) | No notHead | ih | Just z = There ih
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment