Main.idr

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