Complete proof that if last list element not in list, prepending will not be making it so

Question

Having done exercise 9.1 of the book Type Driven Development with Idris I can not get one of my proofs to be complete. The exercise is to make the isLast function work. It should return a proof of that a value is the last value of a List. It works, but unfortunately notLastInTailEqNotLast is not total.

data Last : List a -> a -> Type where
     LastOne : Last [value] value
     LastCons : (prf : Last xs value) -> Last (x :: xs) value

lastNotNil : Last [] value -> Void
lastNotNil _ impossible

lastNotEq : (contra : (lastValue = value) -> Void) -> Last [lastValue] value -> Void
lastNotEq contra LastOne = contra Refl
lastNotEq _ (LastCons LastOne) impossible
lastNotEq _ (LastCons (LastCons _)) impossible

notLastInTailEqNotLast : (notLastInTail : Last xs value -> Void) ->
                         Last (y :: xs) value -> Void
notLastInTailEqNotLast notLastInTail LastOne = ?hole
notLastInTailEqNotLast notLastInTail (LastCons prf) = notLastInTail prf


isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No lastNotNil
isLast [lastValue] value = case decEq lastValue value of
  Yes Refl => Yes LastOne
  No contra => No (lastNotEq contra)
isLast (x :: xs) value = case isLast xs value of
  Yes last => Yes (LastCons last)
  No notLastInTail => No (notLastInTailEqNotLast notLastInTail)

How can I fill ?hole?

I have seen the solution here: https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter9/Exercises/ex_9_1.idr. I understand how that works around my problem using lastNotCons and I can my solution to work that way, but it seems like a workaround. The proof I want to provide seems trivial to me: if I have proof that an element is not the last element in a list then another list with that list appended will still not have that element as the last element in the list (i.e. notLastInTailEqNotLast).

Help is much appreciated.

Anton Trunov Anton Trunov · Accepted Answer · 2018-08-04T20:44:39

It's not a possible to prove notLastInTailEqNotLast, because it is not correct. Here is a counter example: 0 is not the last element of the empty list [], but if you prepend 0 to the empty list you suddenly get that 0 is the last element of the new list.

Another way to see it is when you are trying to fill in ?hole, you have Void as your goal, so that must mean you should have a contradiction in your context, but the context looks like so

`--   phTy : Type
      value : phTy
      notLastInTail : Last [] value -> Void
     ---------------------------------------

But your only candidate for contradiction is notLastInTail. If you squint at its type you'll see that it's simply your lastNotNil theorem, i.e. it's not contradictory.

Complete proof that if last list element not in list, prepending will not be making it so

1 Answers