5

在 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))
4

1 回答 1

9

如果你想保持长度作为类型的一部分，你只需要打包两个具有相同大小索引的向量。首先需要导入：

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

没什么特别的：就像你写普通的 size 向量一样n，你可以这样做：

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

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

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

在我转到我们希望隐藏大小的示例之前，这里有一个此类值的示例：

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

当您尝试将两个大小不均匀的向量填充到这对向量中时，您可以检查 Agda 是否正确地抱怨。

隐藏索引是完全适合依赖对的工作。首先，下面是隐藏一个向量长度的方法：

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

现在，我们知道如何从一种表示到另一种表示，但我们仍然必须证明这两种表示给我们提供了相同的信息。

首先，我们证明如果我们获取一个列表，将其转换为向量（via list⟶vec），然后再转换回列表（via 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)∃2Vec A

于 2013-03-16T03:36:30.387 回答