Agda list last of a generic list of naturals concatenated with a list of 1

Question

I have the function:

natListLast : List ℕ → ℕ
natListLast []            = 0
natListLast nats@(x ∷ xs) = v.last (v.fromList nats)

When I do

_ : natListLast (2 l.∷ l.[] l.++ 1 l.∷ l.[]) ≡ 1
_ = refl

I don't get any error.

But when I try to generalize this to an arbitrary List nat like so:

natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
natListConcatLast [] = refl
natListConcatLast nats@(x ∷ xs) = ?

I'm not sure what to replace ? with.

I tried starting with begin:

natListConcatLast : (nats : List ℕ) → natListLast (nats l.++ 1 l.∷ l.[]) ≡ 1
natListConcatLast [] = refl
natListConcatLast nats@(x ∷ xs) =
  begin
    natListLast (nats l.++ 1 l.∷ l.[])
  ≡⟨⟩
    v.last (v.fromList ((x l.∷ xs) l.++ 1 l.∷ l.[]))
  ≡⟨⟩
    ?
  ≡⟨⟩
    1
  ∎

but I get this error:

1 !=
(last (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[]))
 | initLast (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[])))
of type ℕ
when checking that the expression 1 ∎ has type
last (fromList ((x List.∷ xs) l.++ 1 List.∷ List.[])) ≡ 1

I'm not sure how to interpret this error. I'm not sure how to deal with | initLast.

Thanks!

Answer 1

I suggest the following solution:

open import Data.List
open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

natListLast : List ℕ → ℕ
natListLast [] = 0
natListLast (x ∷ []) = x
natListLast (_ ∷ y ∷ l) = natListLast (y ∷ l)

natListConcatLast : ∀ l → natListLast (l ++ [ 1 ]) ≡ 1
natListConcatLast [] = refl
natListConcatLast (_ ∷ []) = refl
natListConcatLast (_ ∷ _ ∷ l) = natListConcatLast (_ ∷ l)