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

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.

This tells you that the value init (x ∷ xs) depends on the value of everything to the right of the |. When you prove something about in a function in Agda your proof will have to have the structure of the original definition.

In this case you have to case on the result of initLast because the definition of initLast does this before producing any results.

init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
init xs         with initLast xs
                --  ⇧  The first thing this definition does is case on this value
init .(ys ∷ʳ y) | (ys , y , refl) = ys

So here is how we write the lemma.

module inithead where

open import Data.Nat
open import Data.Product
open import Data.Vec
open import Relation.Binary.PropositionalEquality

lem-headInit : {A : Set} {n : ℕ} (xs : Vec A (2 + n))
             → head (init xs) ≡ head xs

lem-headInit (x ∷ xs) with initLast xs
lem-headInit (x ∷ .(ys ∷ʳ y)) | ys , y , refl = refl

I took the liberty of generalizing your lemma to Vec A since the lemma doesn't depend on the contents of the vector.

Answer 2

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?