agda - Agda：关于 `Vec` `last` 使用 `with` 的证明

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)