Agda: Aynı uzunluktaki vektörlerin çifti

Question

Agda'da, aynı uzunlukta olması gereken bir çift vektörü nasıl tanımlayabilirim? Eğer türünde bir parçası olarak uzunluğunu tutmak istiyorsanız

-- 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

, sadece aynı boyutta indeksi iki vektör toparlanıp gerekir. İlk Gerekli ithalat:

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

Hiçbir şey ekstra fantezi: Eğer boyutu n sizin sıradan vektör yazıyormuş gibi, bunu yapabilirsiniz:

olduğunu

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

, 2Vec A n çiftlerinin türüdür A s vektörlerinin her ikisi de n elemanlarıyla. Örneğin, evrendeki evren düzeyine genelleme fırsatı aldığımı unutmayın - bu, örneğin, Set s vektörlerine sahip olabileceğiniz anlamına gelir.

Dikkat edilmesi gereken ikinci yararlı şey, sıradan bağımlı olmayan bir çift olan _×_ kullanmış olmasıdır. Σ açısından, ikinci bileşenin ilk değere bağlı olmadığı özel bir durum olarak tanımlanmıştır. Eğer çalıştıklarında Agda haklı şikayet olduğunu

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

kontrol edebilirsiniz:

Ve biz gizli boyutunu tutmak istiyorum örneğe geçmeden önce

, burada bu tip bir değere ilişkin bir örnek Bu çifte eşit olmayan büyüklükte iki vektör.

Gizleme indisleri bağımlı çift için tam olarak uygun iştir. Bir başlangıç ​​olarak, burada bir vektörün uzunluğunu gizlemek istiyorum nasıl:

boyut indeksi tipi imzasının dışında tutulması, bu nedenle ancak etkili bir (vektör içine bazı bilinmeyen boyutta olduğundan biliyorum

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

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

size bir liste veriyor). Tabii ki, bir indeksi gizlemek için ihtiyacımız olan her zaman yeni bir veri türü yazmak yorucu olacaktır, bu yüzden standart kütüphane bize Σ'u verir.

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 ∷ [] 

Şimdi, kolayca yukarıda verilen tip 2Vec bunu uygulayabilirsiniz:

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

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

---

copumpkin mükemmel bir noktayı gündeme getiriyor: Sadece çiftlerinin listesini kullanarak aynı garantisi alabilirsiniz . Bu iki gösterim tam olarak aynı bilgiyi kodlar, bir bakalım.

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₂ 

: Bir listeye iki vektörden gidiyor

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 

birlikte iki vektör sıkıştırma meselesidir: Burada

, biz ad çatışmaları önlemek için farklı bir ithalat listesi kullanacağız Hayır

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 

: çiftlerinin listesini alıp listelerin bir çift üreten - dönersek sadece Ayıklama edilir Bir temsilden diğerine nasıl geçeceğini biliyoruz, ama yine de bu iki gösterimin bize aynı bilgiyi verdiğini göstermeliyiz. Öncelikle, eğer bir liste alırsak, onu vektöre (list⟶vec aracılığıyla) dönüştürüp sonra da (vec⟶list aracılığıyla) listeye geri dönersek, aynı listeyi geri aldığımızı gösteririz.

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

Ve sonra tam tersi: İlk vektör listelemek için ve sonra vektöre listelemek:

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

Biz ettik: Eğer cong ne merak ediyor halinde

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

vec⟶list ile birlikte list⟶vec, List (A × A) vearasında bir izomorfizması oluşturduğunu göstermiştir., bu iki temsilin izomorfik olduğu anlamına gelir.