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是As 的向量对的类型,两者都有n元素.请注意,我借此机会将其推广到仲裁Universe级别 - 这意味着您可以使用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

现在,我们知道如何从一个表示到另一个表示,但我们仍然必须表明这两个表示给我们相同的信息.

首先,我们展示如果我们获取一个列表,将其转换为vector(via list?vec)然后返回list(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,这意味着这两个表示是同构的.