david-christiansen · February 13, 2016 19:47
diff --git a/Main.idr b/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
	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