Showing (head . init ) = head in Agda

Question

I'm trying to prove a simple lemma in Agda, which I think is true.

If a vector has more than two elements, taking its head following taking the init is the same as taking its head immediately.

I have formulated it as follows:

lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l)))
                    -> head (init xs) ≡ head xs
lem-headInit (x ∷ xs) = ?

Which gives me;

.l : ℕ
x  : ℕ
xs : Vec ℕ (suc .l)
------------------------------
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x

as a response.

I do not entirely understand how to read the (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) component. I suppose my questions are; is it possible, how and what does that term mean.

Many thanks.

Answer 1

Ok. I've got this one by cheating and I'm hoping somebody has a better solution. I threw away all the extra information you get from init being defined in terms of initLast and created my own naive version.

initLazy : ∀{A l} → Vec A (suc l) → Vec A l
initLazy (x ∷ []) = []
initLazy (x ∷ (y ∷ ys)) = x ∷ (initLazy (y ∷ ys))

Now the lemma is trivial.

Any other offers?