如何证明Agda中Vec ++ [] ≡ Vec？类型报错求解

问题描述 #

是否有简便的方法证明以下Agda命题：

++[] : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> vec ++ [] ≡ vec

编写证明时遇到类型错误，报错信息如下：

n != n Nat.+ Nat.zero of type ℕ
when checking that the expression vec has type
Vec A (n Nat.+ Nat.zero)

补充说明：这不是作业题，提问前已查阅Data.Vec.Properties，若该证明存在于其中，烦请告知其名称。

解答 #

类型不匹配原因 #

报错核心是Agda类型检查严格区分n和n + 0——二者语义相等，但类型层面需要显式等式转换。vec ++ []的类型是Vec A (n + 0)，而目标类型是Vec A n，必须用自然数的+0等式引理衔接类型差异。

简便解决方式 #

1. 直接使用标准库已有证明
   你要找的证明在Data.Vec.Properties中，名称为++-right-identity，直接导入即可使用：

   open import Data.Vec.Properties using (++-right-identity)
   

   该引理就是你要证明的命题的标准实现。

2. 手动构造证明
   若要自行编写，需结合自然数的+0等式（Data.Nat.Properties中的+-right-identity）和rewrite语法完成类型转换：

   open import Data.Vec
   open import Data.Nat
   open import Data.Nat.Properties using (+-right-identity)
   open import Relation.Binary.PropositionalEquality
   
   ++[] : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> vec ++ [] ≡ vec
   ++[] vec rewrite +-right-identity n = refl
   

   rewrite会将目标类型中的n + 0替换为n，之后refl即可直接匹配相等关系。

内容的提问来源于stack exchange，提问作者Phoebe Goldman