How to prove ((x :: xs) = (y :: ys)) given (x = y) & (xs = ys)

I am learning Idris and I have a bit of a noob question.

I am doing exercise 2 of chapter 8.3 of the book on type driven development with Idris. The point is to implement DecEq for your own Vector. This is how far I got:

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 elem
  (::) : elem -> Vect n elem -> Vect (S n) elem

headUnequal : {xs : Vect n a} -> {ys : Vect n a} -> (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

tailsUnequal : {xs : Vect n a} -> {ys : Vect n a} -> (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailsUnequal contra Refl = contra Refl

headAndTailEq : {xs : Vect n a} -> {ys : Vect n a} -> (xEqY : x = y) -> (xsEqYs : xs = ys) -> ((x :: xs) = (y :: ys))
headAndTailEq xEqY xsEqYs = ?hole

implementation DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes xEqY => case decEq xs ys of
        No xsNeqYs => No $ tailsUnequal xsNeqYs
        Yes xsEqYs => Yes $ headAndTailEq xEqY xsEqYs

How do I fill ?hole?

I've seen the solution on https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter8/Exercises/ex_8_3.idr. With that knowledge I can make my solution work:

implementation DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes Refl => case decEq xs ys of
        No xsNeqYs => No $ tailsUnequal xsNeqYs
        Yes Refl => Yes Refl

But honestly, why does this work? Why does the final Yes Refl only work if I don't name the proofs?

Thank you!

Solution

The important difference is the value matching in the case-blocks, not the naming of the proofs. If you inspect the first case with

  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes Refl => ?hole

you will see, that the ?hole only needs Dec (x :: xs = x :: ys). In your version on the other hand, ?hole is Dec (x :: xs = y :: ys):

  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes xEqY => ?hole

Here, xEqY : x = y. Idris has no special understanding of =, so this simply means, that there is a value xEqY that has the type x = y (and there is no further inspection on what xEqY could be). If you match on Refl, Idris can unify x and y, because Refl is a constructor for x = x - the values are the same. Thus you gain more information with pattern matching; instead of an opaque variable name, you get a concrete value. As a rule of thumb: always pattern match until you have enough information on the right hand side.

With this, your proof can also be implemented easily:

headAndTailEq : {xs : Vect n a} -> {ys : Vect n a} -> (xEqY : x = y) -> (xsEqYs : xs = ys) -> ((x :: xs) = (y :: ys))
headAndTailEq Refl Refl = Refl