Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# david-christiansen/Main.idr

Created Feb 13, 2016
 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
to join this conversation on GitHub. Already have an account? Sign in to comment