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)和之間，這意味着這兩個表示是同構。