Agda：使用“with”证明“Vec”“last”

问：

我试图证明以下说法

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

但我对这个案子感到困惑。(x ∷ xs)

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

目标是

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

我首先尝试使用begin

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

但随后出现此错误：

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

所以我看了一下 in 的定义lastagda-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

并注意到该子句，所以以为我会尝试使用 . 我还在 https://agda.readthedocs.io/en/v2.6.1.1/language/with-abstraction.html?highlight=with#generalisation 中看到了一个使用证明（涉及）的例子。withwithfilterwith

所以我想尝试一下

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

我得到作为目标：

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

我对如何前进感到困惑。还是我一开始就走错了方向？

谢谢！

编辑

当我尝试时

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

我得到：

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

不太确定为什么现在有，为什么它不仅仅是xs₁xs