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