证明Vec ++ [] == Vec？

Question

是否有方便的证据证明：

++[] : ∀ {ℓ} {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。(我认为这是不言而喻的。)如果这个证据在那里，我找不到它，所以它的名字将是这个问题的一个很好的答案。

Answer 1

的确是这样

open import Relation.Binary.PropositionalEquality

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

由于_≡_期望两个定义相同类型的值，并且n + 0 = n仅在命题上而不是在定义上(详见平等 )，所以不会输入n。

因此，您需要的不仅仅是_≡_，还有多个选项(免责声明:我从来没有广泛使用过这些选项)。

1. 使用异构等式： 模块异构，其中开放导入Relation.Binary.HeterogeneousEquality开放导入Data.Nat.Properties ++ []₁：∀{ℓ} {A : Setℓ} {n} (v: vec n) -> vec ++ []≅Vec ++[]₁[]= refl ++[]₁(x∷v) = icong (Vec _) (+-identityʳ_) (_∷_ x) (++[]₁v)

但是，正如您所看到的，这需要有一个∀ n -> n + 0 ≡ n的证据，这是一个尴尬和不必要的复杂。

1. 您可以有一个自定义关系，例如标准库使用的一： 数据点{a bℓ} {A : Set a} {B : Set b} (_∼_：REL A Bℓ)：∀{m n} (xs : Vec m) (ys : Vec n)→Set (a⊔b⊔ℓ)其中[]：Pointwise _∼_ _∷_：∀{m x y} { Vec m){ys : Vec } (x _∼_ y:x∼y) ( xs∼ys : Pointwise _∼_ xs)→Pointwise _∼_(x∷xs) (y∷ys)

有了这个Pointwise _≡_，您就平等了：

module Pointwise where
  open import Data.Vec.Relation.Binary.Pointwise.Inductive
  open import Relation.Binary.PropositionalEquality
 
  ++[]₂ : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> Pointwise _≡_ (vec ++ []) vec
  ++[]₂ []      = []
  ++[]₂ (x ∷ v) = _≡_.refl ∷ ++[]₂ v

这是一个很好的解决方案，但是对于每种索引数据类型都需要一个专用的关系(加上与命题相等的转换函数等等)，所以非常重。

1. 使用“杂合索引”相等： 模块异索引，其中infix 4 __≅_ data __≅_ {ια} {I : Setι} {i} (A :i -> Setα) (x :a i)：∀{j} a j ->集，其中refl :a x≅x cong：∀{ικαβ} {I : Setι} {K : Setκ} {A :I -> Setα}{B :K -> Setβ} {f :i -> K} {i j: I} {x }{ i} {y :a j} -> (h：{k : I} -> (z :a k) -> B (f k)) -> A x≅y -> B x≅h y cong _ refl = refl ++[]₃：∀{ℓ} {A：集合ℓ} {n} (vec : vec n) -> vec ++ []≅Vec ++ []₃[]= refl ++[]₃(x∷v) = cong (_∷_ x) (++[]₃v)

这很好，但是cong非常复杂，这个解决方案只适用于具有单个索引的数据类型。如果您有另一种数据类型，但这一次有两个索引，那么您将不得不定义另一个版本的[_]_≅_，这一次更加尴尬，并且使用更加复杂的cong。

1. 使用“望远镜”相等： 模块伸缩，其中开放导入Relation.Binary.PropositionalEquality开放导入Data.Product ++ []₄：∀{ℓ} {A : Setℓ} {n} (vec : Vec n) -> _≡_ {A =∃(Vec A)} (_，vec ++ []) (_，++ []₄[]= refl ++[]₄(x∷v) = cong (Data.Product.map _ (_∷_ x)) (++[]₄v)

这个程序不需要任何设置，所以这很好，但是您仍然需要引入一些名称，因为多次使用_≡_ {A = ∃ (Vec A)}太笨重了，不太实用。