Agda：具有相同长度的一对向量

Question

在Agda中，如何定义一对必须具有相同长度的向量？

-- my first try, but need to have 'n' implicitly 
b : ∀ (n : ℕ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n) 
b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ []) 
b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ []) 
b _ = _ 

-- how can I define VecSameLength correctly? 
VecSameLength : Set 
VecSameLength = _ 

c : VecSameLength 
c = (1 ∷ 2 ∷ []) , (1 ∷ 2 ∷ []) 

d : VecSameLength 
d = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ []) 

-- another try 
VecSameLength : Set 
VecSameLength = Σ (Vec ℕ ?) (λ v → Vec ℕ (len v)) 

Answer 1

如果你想保留的长度作为类型的一部分，你只需要收拾两个向量与同样大小的索引。必要进口第一：

open import Data.Nat 
open import Data.Product 
open import Data.Vec 

没有什么额外的想象力吧，就像你写的大小n你的普通载体，你可以这样做：

2Vec : ∀ {a} → Set a → ℕ → Set a 
2Vec A n = Vec A n × Vec A n 

也就是说，2Vec A n是对的类型A s的载体，均具有n元素。请注意，我借此机会将其推广到任意的宇宙级别 - 这意味着例如您可以拥有Set s的矢量。

第二个有用的事情要注意的是，我用_×_，这是一个普通的非从属对。它根据Σ定义为第二个组件不依赖于第一个值的特殊情况。

我移动到哪里，我们想保持一定的尺寸隐藏的例子之前，这里是此类型的值的示例：

test₁ : 2Vec ℕ 3 
-- We can also infer the size index just from the term: 
-- test₁ : 2Vec ℕ _  
test₁ = 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ [] 

您可以检查，当你试图在阿格达理所当然地抱怨将两个尺寸不一的矢量插入这对。

隐藏索引是完全适合从属对的作业。作为首发，这里是你如何隐藏一个向量的长度：

data SomeVec {a} (A : Set a) : Set a where 
    some : ∀ n → Vec A n → SomeVec A 

someVec : SomeVec ℕ 
someVec = some _ (0 ∷ 1 ∷ []) 

大小指数保持在类型签名之外，所以我们只知道矢量内部有一些未知大小（有效给你一个清单）。当然，每次我们需要隐藏一个索引时编写一个新的数据类型会很麻烦，所以标准库给我们提供了Σ。现在

someVec : Σ ℕ λ n → Vec ℕ n 
-- If you have newer version of standard library, you can also write: 
-- someVec : Σ[ n ∈ ℕ ] Vec ℕ n 
-- Older version used unicode colon instead of ∈ 
someVec = _ , 0 ∷ 1 ∷ [] 

，我们可以很容易地将此​​应用到上面给出的类型2Vec：

∃2Vec : ∀ {a} → Set a → Set a 
∃2Vec A = Σ[ n ∈ ℕ ] 2Vec A n 

test₂ : ∃2Vec ℕ 
test₂ = _ , 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ [] 

---

copumpkin提出了一个良好的出发点：你可以通过对列表得到同样的保障。这两个表示法编码完全相同的信息，让我们来看看。

在这里，我们将使用不同的导入列表，防止名字冲突：

open import Data.List 
open import Data.Nat 
open import Data.Product as P 
open import Data.Vec as V 
open import Function 
open import Relation.Binary.PropositionalEquality 

从两个向量去一个列表是两个向量荏苒共同的问题：

vec⟶list : ∀ {a} {A : Set a} → ∃2Vec A → List (A × A) 
vec⟶list (zero , []  , [])  = [] 
vec⟶list (suc n , x ∷ xs , y ∷ ys) = (x , y) ∷ vec⟶list (n , xs , ys) 

-- Alternatively: 
vec⟶list = toList ∘ uncurry V.zip ∘ proj₂ 

回去只是解压缩 - 取一对清单并产生一对清单：

list⟶vec : ∀ {a} {A : Set a} → List (A × A) → ∃2Vec A 
list⟶vec [] = 0 , [] , [] 
list⟶vec ((x , y) ∷ xys) with list⟶vec xys 
... | n , xs , ys = suc n , x ∷ xs , y ∷ ys 

-- Alternatively: 
list⟶vec = ,_ ∘ unzip ∘ fromList 

否w，我们知道如何从一个表示到另一个表示，但是我们仍然必须证明这两个表示给了我们相同的信息。首先，我们显示如果我们拿一个列表，将它转换为矢量（通过list⟶vec），然后返回列表（通过vec⟶list），然后我们得到相同的列表。

pf₁ : ∀ {a} {A : Set a} (xs : List (A × A)) → vec⟶list (list⟶vec xs) ≡ xs 
pf₁ []  = refl 
pf₁ (x ∷ xs) = cong (_∷_ x) (pf₁ xs) 

然后周围的其他方法：第一个向量，列出，然后列出矢量：

pf₂ : ∀ {a} {A : Set a} (xs : ∃2Vec A) → list⟶vec (vec⟶list xs) ≡ xs 
pf₂ (zero , []  , [])  = refl 
pf₂ (suc n , x ∷ xs , y ∷ ys) = 
    cong (P.map suc (P.map (_∷_ x) (_∷_ y))) (pf₂ (n , xs , ys)) 

如果你想知道什么cong做：

cong : ∀ {a b} {A : Set a} {B : Set b} 
     (f : A → B) {x y} → x ≡ y → f x ≡ f y 
cong f refl = refl 

我们已经显示list⟶vec连同vec⟶list形成同构在List (A × A)和之间，这意味着这两个表示是同构。