Proof that 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(有关详细信息，请参阅等式(。

因此，你需要一个比_≡_更理想的等式，并且有多种选择(免责声明：我从未广泛使用过这些选项(。

1. 使用异构等式：

   module Heterogeneous where
   open import Relation.Binary.HeterogeneousEquality
   open import Data.Nat.Properties
   ++[]₁ : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> vec ++ [] ≅ vec
   ++[]₁ []      = refl
   ++[]₁ (x ∷ v) = icong (Vec _) (+-identityʳ _) (_∷_ x) (++[]₁ v)
   

然而，正如你所看到的，这需要有∀ n -> n + 0 ≡ n的证明，这很尴尬，也是一个不必要的复杂性。

2. 您可以有一个自定义关系，例如标准库使用的关系：

   data Pointwise {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) :
   ∀ {m n} (xs : Vec A m) (ys : Vec B n) → Set (a ⊔ b ⊔ ℓ)
   where
   []  : Pointwise _∼_ [] []
   _∷_ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n}
   (x∼y : x ∼ y) (xs∼ys : Pointwise _∼_ xs ys) →
   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

这是一个很好的解决方案，但需要为每个索引数据类型提供一个专用的关系(加上命题等式之间的转换函数等(，所以它相当重。

3. 使用"；异索引的"；相等：

   module Heteroindexed where
   infix 4 [_]_≅_
   data [_]_≅_ {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : ∀ {j} -> A j -> Set where
   refl : [ A ] x ≅ x
   cong
   : ∀ {ι κ α β} {I : Set ι} {K : Set κ}
   {A : I -> Set α} {B : K -> Set β}
   {f : I -> K} {i j : I} {x : A i} {y : A j}
   -> (h : {k : I} -> (z : A k) -> B (f k))
   -> [ A ] x ≅ y
   -> [ B ] h x ≅ h y
   cong _ refl = refl
   ++[]₃ : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> [ Vec A ] vec ++ [] ≅ vec
   ++[]₃ []      = refl
   ++[]₃ (x ∷ v) = cong (_∷_ x) (++[]₃ v)
   

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

4. 使用"；伸缩式"；相等：

   module Telescopic where
   open import Relation.Binary.PropositionalEquality
   open import Data.Product
   ++[]₄ : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> _≡_ {A = ∃ (Vec A)} (_ , vec ++ []) (_ , vec)
   ++[]₄ []      = refl
   ++[]₄ (x ∷ v) = cong (Data.Product.map _ (_∷_ x)) (++[]₄ v)
   

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