问题描述
我正在尝试证明以下说法
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
所以我看了last
中的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
并注意到with
子句,以为我会尝试使用with
进行证明。
我还在https://agda.readthedocs.io/en/v2.6.1.1/language/with-abstraction.html?highlight=with#generalisation中看到了一个使用filter
的证明示例(涉及with
)。
所以我想尝试一下
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
解决方法
这是一个可能的解决方案,我将您的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)