I am working on exercise 2 in section 9.1 from Type-Driven Development with Idris, and I can't figure out how to fill the last hole (see notInTail, below).
I have read the answers to Implementing isLast with Idris, but I am stuck in a different place.
data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (prf : Last xs value) -> Last (x :: xs) value
notInNil : Last [] value -> Void
notInNil LastOne impossible
notInNil (LastCons _) impossible
notLast : (notHere : (x = value) -> Void) -> Last [x] value -> Void
notLast prf LastOne = absurd (prf Refl)
notLast prf (LastCons _) impossible
notInTail : (notThere : Last xs value -> Void) -> Last (x :: xs) value -> Void
notInTail notThere LastOne = ?hole
notInTail notThere (LastCons prf) = notThere prf
isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInNil
isLast (x :: []) value = case decEq x value of
Yes Refl => Yes LastOne
No notHere => No (notLast notHere)
isLast (_ :: xs) value = case isLast xs value of
Yes prf => Yes (LastCons prf)
No notThere => No (notInTail notThere)
Here's what Idris reports:
- + Main.hole [P]
`-- phTy : Type
value : phTy
notThere : Last [] value -> Void
-----------------------------------
Main.hole : Void
I don't think you can prove notInTail as written since it doesn't apply for empty lists. However it does apply for non-empty lists:
notInTail : (c : Last (y :: ys) value -> Void) -> Last (x :: (y :: ys)) value -> Void
notInTail c (LastCons prf) = c prf
The tail of the input list must be non-empty in the third case of isLast but you aren't specifying that. If you do then you can apply notInTail:
isLast (x :: (y :: xs)) value = case isLast (y :: xs) value of
Yes prf => Yes (LastCons prf)
No c => No (notInTail c)