阿格达:关于"维奇""最后"使用"with"的证明

Question

我试图证明以下语句

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

所以我看了agda-stdlib/src/Data/Vec/Base.agda中last的定义

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

注意到with子句，所以我想尝试使用with进行证明。我也在https://agda.readthedocs.io/en/v2.6.1.1/language/with-abstraction.html?highlight=with#generalisation使用CCD_ 8的证明(涉及CCD_。

所以我想试试这个

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

Answer 1

这里有一个可能的解决方案，我将您的1更改为任何a，并使向量的类型通用：

首先，一些进口：

module Vecnat where
open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Data.Product

然后是一个简单但非常重要的属性，它指出在列表的开头添加一个元素不会改变它的最后一个元素：

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

最后，你正在寻找的证据：

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