Agda: proof about `Vec` `last` using `with`

Question

I'm trying to prove the following statement

vecNat : ∀ {n} (xs : Vec ℕ n) → last (xs ∷ʳ 1) ≡ 1

But I get confused the (x ∷ xs) case.

vecNat5 : ∀ {n} (xs : Vec ℕ n) → last (xs ∷ʳ 1) ≡ 1
vecNat5 []       = refl
vecNat5 (x ∷ xs) = {!  0!}

The goal is

?0 : last ((x ∷ xs) ∷ʳ 1) ≡ 1

I first tried this using begin

vecNat5 : ∀ {n} (xs : Vec ℕ n) → last (xs ∷ʳ 1) ≡ 1
vecNat5 []       = refl
vecNat5 (x ∷ xs) =
  begin
    last ((x ∷ xs) ∷ʳ 1)
  ≡⟨⟩
    1
  ∎

but then got this error:

1 !=
(last (x ∷ (xs ∷ʳ 1))
 | (initLast (x ∷ (xs ∷ʳ 1)) | initLast (xs ∷ʳ 1)))
of type ℕ
when checking that the expression 1 ∎ has type
last ((x ∷ xs) ∷ʳ 1) ≡ 1

so I looked at the definition of last in agda-stdlib/src/Data/Vec/Base.agda

last : ∀ {n} → Vec A (1 + n) → A
last xs         with initLast xs
last .(ys ∷ʳ y) | (ys , y , refl) = y

and noticed the with clause so thought I would try a proof using with. I also saw in https://agda.readthedocs.io/en/v2.6.1.1/language/with-abstraction.html?highlight=with#generalisation an example of a proof (involving filter) using with.

So I thought of trying this

vecNat : ∀ {n} (xs : Vec ℕ n) → last (xs ∷ʳ 1) ≡ 1
vecNat []       = refl
vecNat (x ∷ xs) with last (xs ∷ʳ 1)
...                 | r = {!  0!}

and I get as goal:

?0 : (last (x ∷ (xs ∷ʳ 1))
     | (initLast (x ∷ (xs ∷ʳ 1)) | initLast (xs ∷ʳ 1)))
    ≡ 1

I'm confused as how to go forward here. Or did I start out in a wrong direction?

Thanks!

EDIT

When I try

vecNat : ∀ {n} (xs : Vec ℕ n) → last (xs ∷ʳ 1) ≡ 1
vecNat []                               = refl
vecNat (x ∷ xs)         with initLast (xs ∷ʳ 1)
...                         | (xs , x , refl) = ?

I get:

I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  xs ∷ʳ 1 ≟ xs₁ ∷ʳ 1
when checking that the pattern refl has type xs ∷ʳ 1 ≡ xs₁ ∷ʳ 1

not too sure why there is now xs₁ and why it's not just xs

Answer 1

Here is a possible solution, where I changed your 1 into any a, and made the type of the vector generic:

First, some imports:

module Vecnat where

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

Then a simple but very important property which states that adding an element at the head of a list does not change its last element:

prop : ∀ {a} {A : Set a} {n x} (xs : Vec A (suc n)) → last (x ∷ xs) ≡ last xs
prop xs with initLast xs
... | _ , _ , refl = refl

Finally the proof you are looking for:

vecNat5 : ∀ {a} {A : Set a} {l n} (xs : Vec A n) → last (xs ∷ʳ l) ≡ l
vecNat5 [] = refl
vecNat5 (_ ∷ xs) = trans (prop (xs ∷ʳ _)) (vecNat5 xs)